(** %
\section{\label{sec:contexted_patches}Contexted patches}
% *)
Module Export contexted_patches.

Require Import Equality.
Require Import List.
Require Import util.
Require Import names.
Require Import patch_universes.

(** %
\begin{Idefinition}[contexted-patch]
For all patches $r \in \patches$, $:r$ is a \emph{contexted patch} of $r$.
For all contexted patches $\seq{q} : r$ and patches $p \in \patches$,
$p \seq{q} : r$ is a \emph{contexted patch} of $r$ if and only if
$\pair{p}{\seq{q} r} <-> \fail$ and $\seq{q} \ne p^ \seq{q}'$ for some
sequence $\seq{q}'$.

\begin{Iexplanation}
Sometimes we will want to keep a ``reference'' to a patch $p$.
However, for a patch to be useful we have to know what context it should
be applied in. The purpose of a contexted patch is to keep track of a
patch, and the context in which it applies.

The patch sequence before the colon is the context; the patch after the
colon is the patch that we are interested in.
\end{Iexplanation}
% *)

Class ContextedPatchOK {pu_type : NameSet -> NameSet -> Type}
                       {ppu : PartPatchUniverse pu_type pu_type}
                       {pui : PatchUniverseInv ppu ppu}
                       {pu : PatchUniverse pui}
                       {from mid to : NameSet}
                       (c : Sequence pu from mid)
                       (p : pu_type mid to)
    := {
            contextedPatchNotInContext : ~ SignedNameSetIn (pu_nameOf p) (sequenceContents c)
       }.
Implicit Arguments ContextedPatchOK [pu_type ppu pui pu from mid to].

Instance EmptyContextedPatchOK
    : forall {pu_type : NameSet -> NameSet -> Type}
             {ppu : PartPatchUniverse pu_type pu_type}
             {pui : PatchUniverseInv ppu ppu}
             {pu : PatchUniverse pui}
             {from to : NameSet}
             (p : pu_type from to),
      ContextedPatchOK [] p.
Proof.
intros.
constructor.
rewrite SequenceContentsNil.
signedNameSetDec.
Qed.

Inductive ContextedPatch {pu_type : (NameSet -> NameSet -> Type)}
                         {ppu : PartPatchUniverse pu_type pu_type}
                         {pui : PatchUniverseInv ppu ppu}
                         (pu : PatchUniverse pui)
                         (from : NameSet)
                       : Type
    := MkContextedPatch : forall {mid to : NameSet}
                                 (c : Sequence pu from mid)
                                 (p : pu_type mid to)
                                 {contextedPatchOK : ContextedPatchOK c p},
                 ContextedPatch pu from.
Implicit Arguments MkContextedPatch [pu_type ppu pui pu from mid to contextedPatchOK].

(* XXX Describe this in the latex: *)
Definition contextedPatch_name {pu_type : (NameSet -> NameSet -> Type)}
                               {ppu : PartPatchUniverse pu_type pu_type}
                               {pui : PatchUniverseInv ppu ppu}
                               {pu : PatchUniverse pui}
                               {from : NameSet}
                               (c : ContextedPatch pu from) : SignedName
 := match c with
    | MkContextedPatch _ _ _ p _ => pu_nameOf p
    end.

Definition contextedPatchContents
               {pu_type : NameSet -> NameSet -> Type}
               {ppu : PartPatchUniverse pu_type pu_type}
               {pui : PatchUniverseInv ppu ppu}
               {pu : PatchUniverse pui}
               {from : NameSet}
               (cp : ContextedPatch pu from)
             : SignedNameSet
 := match cp with
    | MkContextedPatch _ _ cxt p _ => SignedNameSetMod.add (pu_nameOf p) (sequenceContents cxt)
    end.

(** %
\end{Idefinition}

\begin{Idefinition}[patch-commute-past]
Given a patch $p$ and a contexted patch $\seq{q} : r$, we define $->$,
pronounced \emph{commute past}, thus:\\
$\begin{array}[t]{@{}l@{\quad}l@{}}
 \pair{p}{\seq{q} : r} -> \single{\seq{q}' : r'}&\textrm{if}~
 (\pair{p}{\seq{q}} <-> \pair{\seq{q}'}{p'}) \wedge
 (\pair{p'}{r} <-> \pair{r'}{p''})\\
 \pair{p}{\seq{q} : r} -> \fail&\textrm{otherwise}
 \end{array}$
% *)
Axiom cheat : forall {a}, a.

Inductive CommutePast {pu_type : (NameSet -> NameSet -> Type)}
                      {ppu : PartPatchUniverse pu_type pu_type}
                      {pui : PatchUniverseInv ppu ppu}
                      {pu : PatchUniverse pui}
                    : forall {from mid : NameSet},
                      pu_type from mid
                   -> ContextedPatch pu mid
                   -> ContextedPatch pu from
                   -> Prop
    := CommutePastNil :
                 forall (from mid mid' to : NameSet)
                        (p : pu_type from mid)
                        (ident : pu_type mid to)
                        (ident' : pu_type from mid')
                        (p' : pu_type mid' to)
                        (commute : <<p, ident>> <~> <<ident', p'>>),
                 CommutePast p
                             (MkContextedPatch [] ident)
                             (MkContextedPatch [] ident')
    |  CommutePastCons :
                 forall (* XXX (rsContains qRsContainsrs'Contains q'Rs'Contains : SignedNameSet) *)
                        (o op opq opqr opqrs oq oqr oqrs : NameSet)
                        (p : pu_type o op)
                        (contextQ : pu_type op opq)
                        (contextRs : Sequence pu opq opqr)
                        (ident : pu_type opqr opqrs)

                        (contextQ' : pu_type o oq)
                        (contextRs' : Sequence pu oq oqr)
                        (ident' : pu_type oqr oqrs)
                        (p' : pu_type oq opq)

                        (contextRsIdentOK : ContextedPatchOK contextRs ident)
                        (contextRs'Ident'OK : ContextedPatchOK contextRs' ident')

                        (commute : <<p, contextQ>> <~> <<contextQ', p'>>)
                        (H : CommutePast p'
                             (MkContextedPatch contextRs ident)
                             (MkContextedPatch contextRs' ident'))

                        (qRsConsOK : ConsOK contextQ contextRs)
                        (q'Rs'ConsOK : ConsOK contextQ' contextRs')

                        (contextQContextRsIdentOK : ContextedPatchOK (contextQ :> contextRs) ident)
                        (contextQ'ContextRs'Ident'OK : ContextedPatchOK (contextQ' :> contextRs') ident'),
                 CommutePast p
                             (MkContextedPatch (contextQ :> contextRs) ident)
                             (MkContextedPatch (contextQ' :> contextRs') ident').

Definition CommutePastable {pu_type : (NameSet -> NameSet -> Type)}
                           {ppu : PartPatchUniverse pu_type pu_type}
                           {pui : PatchUniverseInv ppu ppu}
                           {pu : PatchUniverse pui}
                           {from mid : NameSet}
                           (p : pu_type from mid)
                           (cp : ContextedPatch pu mid)
                         : Prop
 := (exists cp' : ContextedPatch pu from,
     CommutePast p cp cp').

Lemma CommutePastable_dec {pu_type : (NameSet -> NameSet -> Type)}
                          {ppu : PartPatchUniverse pu_type pu_type}
                          {pui : PatchUniverseInv ppu ppu}
                          {pu : PatchUniverse pui}
                          {from mid : NameSet}
                          (p : pu_type from mid)
                          (cp : ContextedPatch pu mid)
                        : {CommutePastable p cp} + {~CommutePastable p cp}.
Proof with auto.
intros.
destruct cp as [cxt1 cxt2 cxtPs cxtP cxtOK].
destruct cxtPs as [cxtPs cxtPsOK].

dependent induction cxtPs generalizing from p.
    destruct (commutable_dec p cxtP).
        destruct s.
        destruct s.
        destruct s.
        left.
        revert cxtOK.
        rewrite NilSeqToNil.
        intro.
        proofIrrel cxtOK (@EmptyContextedPatchOK pu_type ppu pui pu cxt cxt2 cxtP).
        exists (MkContextedPatch [] x0).
        apply (CommutePastNil _ _ _ _ _ _ _ _ c).
    right.
    intro.
    contradiction n.
    destruct H.
    dependent destruction H.
        exists mid'.
        exists ident'.
        exists p'...
    rewrite NilSeqToNil in x.
    contradiction (ConsEqNil x).
destruct (commutable_dec p0 p).
    destruct s as [mid2 s].
    destruct s as [q' s].
    destruct s as [p' commute].
    solveFirstIn IHcxtPs.
        constructor.
        destruct cxtPsOK.
        clear cxtOK.
        rewrite SequenceNoDupesCons in sequenceNoDupes0.
        destruct sequenceNoDupes0...
    specialize (IHcxtPs cxtP).
    solveFirstIn IHcxtPs.
        constructor.
        destruct cxtOK.
        consSeqToCons p cxtPs.
        rewrite SequenceContentsCons in contextedPatchNotInContext0.
        proofIrrel SFI psSequenceOK.
        remember (sequenceContents (MkSequence cxtPs psSequenceOK)) as X.
        signedNameSetDec.
    specialize (IHcxtPs mid2).
    specialize (IHcxtPs p').
    destruct IHcxtPs.
        left.
        revert cxtOK.
        consSeqToCons p cxtPs.
        intro.
        destruct c.
        destruct x.
        assert (q'cOK : ConsOK q' c).
            admit.
        assert (q'cp1OK : ContextedPatchOK (q' :> c) p1).
            admit.
        exists (MkContextedPatch (q' :> c) p1).
        assert (cp1OK : ContextedPatchOK c p1).
            admit.
        proofIrrel SFI psSequenceOK.
        apply (CommutePastCons _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ commute H _ _ _ _).
    right.
    intro.
    contradiction n.
    dependent destruction H.
    dependent destruction H.
    consSeqToCons p cxtPs.
    consEquality x.
    destruct (commuteUnique commute commute0) as [? [? ?]].
    subst.
    subst.
    exists (MkContextedPatch contextRs' ident').
    proofIrrel SFI psSequenceOK.
    proofIrrel SFI0 contextRsIdentOK...
right.
intro.
dependent destruction H.
dependent destruction H.
consSeqToCons p cxtPs.
consEquality x.
contradiction n.
exists oq.
exists contextQ'.
exists p'...
Qed.
(*
XXX
    destruct nilOK.
    remember (NameSetEquality nilFromEqTo0) as H.
    clear HeqH.
    subst.
    destruct (commutable_dec p p0).
        left.
        destruct c as [? [p0' [p' ?]]].
        assert (nilFromOK : NilOK from from SignedNameSetMod.empty).
            constructor.
                nameSetDec.
            signedNameSetDec.
        exists (MkContextedPatch pu from [] p0').
        (* XXX Tidy this up: *)
        apply (CommutePastNil
                   SignedNameSetMod.empty
                   contains
                   from
                   to0
                   x
                   to
                   p
                   p0
                   p0'
                   p'
                   H
                   _
                   _
                  ).
    right.
    admit. (* XXX *)
admit. (* XXX *)
Qed.
*)

Inductive CommuteManyPast {pu_type : (NameSet -> NameSet -> Type)}
                          {ppu : PartPatchUniverse pu_type pu_type}
                          {pui : PatchUniverseInv ppu ppu}
                          {pu : PatchUniverse pui}
                        : forall {from mid : NameSet},
                          Sequence pu from mid
                       -> ContextedPatch pu mid
                       -> ContextedPatch pu from
                       -> Prop
    := CommuteNilPast : forall (fromNilContains : SignedNameSet)
                               (from : NameSet)
                               (cp : ContextedPatch pu from),
                        CommuteManyPast [] cp cp
     | CommuteConsPast : forall (qsContains pQsContains : SignedNameSet)
                                (o op opq : NameSet)
                                (p : pu_type o op)
                                (qs : Sequence pu op opq)
                                (cp : ContextedPatch pu opq)
                                (cp' : ContextedPatch pu op)
                                (cp'' : ContextedPatch pu o)
                                (CommuteQsPast : CommuteManyPast qs cp cp')
                                (CommutePPast : CommutePast p cp' cp'')
                                (consOK : ConsOK p qs),
                         CommuteManyPast (p :> qs) cp cp''.

(*
Definition commutePast {pu : PatchUniverse}
                       {from mid : NameSet}
                       (p : (pu_type pu) from mid)
                       (c : ContextedPatch pu mid)
                     : option (ContextedPatch pu from)
 := match c with
    (* XXX Should have Nil = cContext *)
    | MkContextedPatch _ _ _ (Nil _) cPatch =>
          match (commutable_dec pu) p (cheat cPatch) with
          | left _ => None
          | right _ => None
          end
    | _ => None
    end.
*)

(** %
\end{Idefinition}

\begin{Idefinition}[patch-commute-past-set]
We extend $->$ to work on sets of contexted patches in the natural way,
{\ie} for any patch $p$ and set of contexted patches $S$:\\
$\pair{p}{S} -> \single{\mkset{(\seq{q}' : r')
                 \mid   (\seq{q} : r) \in S
                 \wedge \pair{p}{\seq{q} : r} -> \single{\seq{q}' : r'}}}$\\
if all the commute pasts succeed, and $\pair{p}{S} -> \fail$ otherwise.
\end{Idefinition}

From here on we assume that contexted patches magically maintain their
invariant,
{\ie} if we have a patch $p$ and a contexted patch $\seq{q} : r$ then
when we write $p \seq{q} : r$ what we mean is, if
$\pair{p}{\seq{q}:r} -> \single{\seq{q}':r'}$ then $\seq{q}':r'$,
otherwise $p \seq{q} : r$.
% *)
Definition addToContext {pu_type : (NameSet -> NameSet -> Type)}
                        {ppu : PartPatchUniverse pu_type pu_type}
                        {pui : PatchUniverseInv ppu ppu}
                        {pu : PatchUniverse pui}
                        {from mid : NameSet}
                        (p : pu_type from mid)
                        (c : ContextedPatch pu mid)
                      : ContextedPatch pu from
 := cheat.
(*
match c with
    | MkContextedPatch _ _ _ _ p => pu_nameOf _ p
    end.
*)

Program Fixpoint addSequenceBaseToContext
                     {pu_type : (NameSet -> NameSet -> Type)}
                     {ppu : PartPatchUniverse pu_type pu_type}
                     {pui : PatchUniverseInv ppu ppu}
                     {pu : PatchUniverse pui}
                     {from mid : NameSet}
                     (ps : SequenceBase pu from mid)
                     (c : ContextedPatch pu mid)
                   : ContextedPatch pu from
 := match ps with
    | Nil _ => c
    | Cons _ _ _ p ps' =>
          (addToContext p (addSequenceBaseToContext ps' c))
    end.

Definition addSequenceToContext
                     {pu_type : (NameSet -> NameSet -> Type)}
                     {ppu : PartPatchUniverse pu_type pu_type}
                     {pui : PatchUniverseInv ppu ppu}
                     {pu : PatchUniverse pui}
                     {from mid : NameSet}
                     (ps : Sequence pu from mid)
                     (c : ContextedPatch pu mid)
                     (notIn : SignedNameSetMod.Empty
                                  (SignedNameSetMod.inter
                                       (sequenceContents ps)
                                       (contextedPatchContents c)))
                   : ContextedPatch pu from
 := match ps with
    | MkSequence s _ => addSequenceBaseToContext s c
    end.

Program Definition addSequenceToContexts
                     {pu_type : (NameSet -> NameSet -> Type)}
                     {ppu : PartPatchUniverse pu_type pu_type}
                     {pui : PatchUniverseInv ppu ppu}
                     {pu : PatchUniverse pui}
                     {from mid : NameSet}
                     (ps : Sequence pu from mid)
                     (cs : list (ContextedPatch pu mid))
                     (notIn : Forall (
                                  fun c =>
                                      SignedNameSetMod.Empty
                                          (SignedNameSetMod.inter
                                               (sequenceContents ps)
                                               (contextedPatchContents c)))
                                  cs)
                   : list (ContextedPatch pu from)
 := inmap cs (fun c => fun H => addSequenceToContext ps c _).
Next Obligation.
rewrite Forall_forall in notIn.
specialize (notIn c).
specialize (notIn H).
auto.
Qed.

Lemma addSequenceToContexts_nil
                     {pu_type : (NameSet -> NameSet -> Type)}
                     {ppu : PartPatchUniverse pu_type pu_type}
                     {pui : PatchUniverseInv ppu ppu}
                     {pu : PatchUniverse pui}
                     {from mid : NameSet}
                     {ps : Sequence pu from mid}
                     {notIn : Forall (
                                  fun c =>
                                      SignedNameSetMod.Empty
                                          (SignedNameSetMod.inter
                                               (sequenceContents ps)
                                               (contextedPatchContents c)))
                                  nil}
                   : addSequenceToContexts ps nil notIn = nil.
Proof with auto.
unfold addSequenceToContexts...
Qed.

Lemma addSequenceToContexts_not_nil
                     {pu_type : (NameSet -> NameSet -> Type)}
                     {ppu : PartPatchUniverse pu_type pu_type}
                     {pui : PatchUniverseInv ppu ppu}
                     {pu : PatchUniverse pui}
                     {from mid : NameSet}
                     {ps : Sequence pu from mid}
                     {cs : list (ContextedPatch pu mid)}
                     {notIn : Forall (
                                  fun c =>
                                      SignedNameSetMod.Empty
                                          (SignedNameSetMod.inter
                                               (sequenceContents ps)
                                               (contextedPatchContents c)))
                                  cs}
                   : addSequenceToContexts ps cs notIn <> nil
                  -> cs <> nil.
Proof with auto.
intro ne.
intro X.
subst.
contradiction ne.
rewrite addSequenceToContexts_nil...
Qed.

Lemma addSequenceToContexts_not_nil2
                     {pu_type : (NameSet -> NameSet -> Type)}
                     {ppu : PartPatchUniverse pu_type pu_type}
                     {pui : PatchUniverseInv ppu ppu}
                     {pu : PatchUniverse pui}
                     {from mid : NameSet}
                     {ps : Sequence pu from mid}
                     {cs : list (ContextedPatch pu mid)}
                     {notIn : Forall (
                                  fun c =>
                                      SignedNameSetMod.Empty
                                          (SignedNameSetMod.inter
                                               (sequenceContents ps)
                                               (contextedPatchContents c)))
                                  cs}
                   : cs <> nil
                  -> addSequenceToContexts ps cs notIn <> nil.
Proof with auto.
intro ne.
intro X.
contradiction ne.
destruct cs.
    congruence.
unfold addSequenceToContexts in X.
simpl in X.
congruence.
Qed.

(** %
\begin{Idefinition}[contexted-patch-conflict]
We define $<X>$, pronounced ``does not conflict with'', such that
$(\seq{p} : q) <X> (\seq{r} : s)$ holds if
$\pair{q^}{\seq{p}^ \seq{r} : s} -> \single{\_}$, and does not hold
otherwise.

\begin{Iexplanation}
Here $\seq{p} : q$ and $\seq{r} : s$ are two contexted patches starting
from the same context. By inverting one of them we can put them into a
single patch sequence $q^ \seq{p}^ \seq{r} s$. By building the contexted
patch $\seq{p}^ \seq{r} : s$ if $\seq{p}$ and $\seq{r}$ both contain a
patch $t$, that patch will be removed (as contexted patches magically
maintain their invariant).

This is almost, but not quite the same thing as saying $\seq{p} q$ and
$\seq{r} s$ can be cleanly merged. For a counter-example, consider
$:t$ and $t:u$. Clearly $t$ and $tu$ can be cleanly merged, giving $tu$,
but $\pair{t^}{t:u} -> \fail$. Likewise, starting with the contexted
patches the other way round, we get $\pair{u^}{t^:t} -> \fail$.
\end{Iexplanation}
# XXX Proove that this is symmetric
\end{Idefinition}
% *)

Definition invertContextedPatch {pu_type : (NameSet -> NameSet -> Type)}
                                {ppu : PartPatchUniverse pu_type pu_type}
                                {pui : PatchUniverseInv ppu ppu}
                                {pu : PatchUniverse pui}
                                {from : NameSet}
                                (c : ContextedPatch pu from)
                              : ContextedPatch pu from
 := cheat.
(*
 := match c with
    | MkContextedPatch _ _ _ ps ident =>
          addSequenceToContext ps
              (addToContext ident
                   (MkContextedPatch _ _ [] (invert _ ident)))
    end.
*)

End contexted_patches.