(** %
\section{\label{sec:canonical_order}Canonical Order}
% *)
Module Export canonical_order.

Require Import Equality.

Require Import names.
Require Import patch_universes.

(** %

XXX
This is a hack to make conflictor equality be real = equality.
For example, if a conflictor's effect is "es", then we need "es" to be in a
canonical order, so that [es, cs p] = [es', cs p].

% *)

Program Definition castPatchFrom {pu_type : NameSet -> NameSet -> Type}
                                 {from from' to : NameSet}
                                 (HeqFrom : from = from')
                                 (p : pu_type from to)
                               : pu_type from' to
    := p.

(* XXX This ought to be an OnrderedType lemma or something *)
Lemma lt_dec (x y : SignedName) : {SignedName_compare x y = Lt} + {~(SignedName_compare x y = Lt)}.
Proof with auto.
destruct (SignedName_compare x y).
        right.
        intro.
        congruence.
    left...
right.
intro.
congruence.
Qed.

Program Fixpoint insertBaseLoop {pu_type : NameSet -> NameSet -> Type}
                                {ppu : PartPatchUniverse pu_type pu_type}
                                {pui : PatchUniverseInv ppu ppu}
                                {pu : PatchUniverse pui}
                                {from mid to : NameSet}
                                (p : pu_type from mid)
                                (qs : SequenceBase pu mid to)
                              : option (SequenceBase pu from to)
    := match qs with
       | Nil _ => None
       | Cons mid' mid2' to' q qs' =>
           match commutable_dec p (castPatchFrom _ q) with
           | inleft (existT _ (existT q' (existT p' _))) =>
               match insertBaseLoop p' qs' with
               | Some pqs' => Some (Cons q' pqs')
               | None =>
                   if lt_dec (pu_nameOf p) (pu_nameOf q)
                   then None
                   else Some (Cons q' (Cons p' qs'))
               end
           | inright _ => None
           end
       end.

Definition insertBase {pu_type : NameSet -> NameSet -> Type}
                                {ppu : PartPatchUniverse pu_type pu_type}
                                {pui : PatchUniverseInv ppu ppu}
                                {pu : PatchUniverse pui}
                                {from mid to : NameSet}
                                (p : pu_type from mid)
                                (qs : SequenceBase pu mid to)
                              : SequenceBase pu from to
    := match insertBaseLoop p qs with
       | Some pqs' => pqs'
       | None => Cons p qs
       end.

Fixpoint canonicaliseBase {pu_type : NameSet -> NameSet -> Type}
                          {ppu : PartPatchUniverse pu_type pu_type}
                          {pui : PatchUniverseInv ppu ppu}
                          {pu : PatchUniverse pui}
                          {from to : NameSet}
                          (ps : SequenceBase pu from to)
                        : SequenceBase pu from to
    := match ps with
       | Nil _ => Nil
       | Cons _ _ _ p ps' => insertBase p (canonicaliseBase ps')
       end.

Program Definition canonicalise {pu_type : NameSet -> NameSet -> Type}
                                {ppu : PartPatchUniverse pu_type pu_type}
                                {pui : PatchUniverseInv ppu ppu}
                                {pu : PatchUniverse pui}
                                {from to : NameSet}
                                (ps : Sequence pu from to)
                              : Sequence pu from to
    := match ps with
       MkSequence ps _ =>
           MkSequence (canonicaliseBase ps) _
       end.
Next Obligation.
admit.
Qed.

Program Fixpoint CanonicallyOrderedOne {pu_type : NameSet -> NameSet -> Type}
                                       {ppu : PartPatchUniverse pu_type pu_type}
                                       {pui : PatchUniverseInv ppu ppu}
                                       {pu : PatchUniverse pui}
                                       {from mid to : NameSet}
                                       (p : pu_type from mid)
                                       (qs : SequenceBase pu mid to)
                                     : Prop
    := match qs with
       | Nil _ => True
       | Cons _ _ _ q qs' =>
           match commutable_dec p (castPatchFrom _ q) with
           | inleft (existT _ (existT q' (existT p' _))) =>
               (SignedName_compare (pu_nameOf p) (pu_nameOf q) = Lt) /\
               CanonicallyOrderedOne p' qs'
           | inright _ =>
               True
           end
       end.

Fixpoint CanonicallyOrderedBase {pu_type : NameSet -> NameSet -> Type}
                                {ppu : PartPatchUniverse pu_type pu_type}
                                {pui : PatchUniverseInv ppu ppu}
                                {pu : PatchUniverse pui}
                                {from to : NameSet}
                                (ps : SequenceBase pu from to)
                              : Prop
    := match ps with
       | Nil _ => True
       | Cons _ _ _ p ps' => CanonicallyOrderedOne p ps' /\ CanonicallyOrderedBase ps'
       end.

Definition CanonicallyOrdered {pu_type : NameSet -> NameSet -> Type}
                              {ppu : PartPatchUniverse pu_type pu_type}
                              {pui : PatchUniverseInv ppu ppu}
                              {pu : PatchUniverse pui}
                              {from to : NameSet}
                              (ps : Sequence pu from to)
                            : Prop
    := match ps with
       | MkSequence ps' _ => CanonicallyOrderedBase ps'
       end.

Lemma CanonicaliseUnique  {pu_type : NameSet -> NameSet -> Type}
                          {ppu : PartPatchUniverse pu_type pu_type}
                          {pui : PatchUniverseInv ppu ppu}
                          {pu : PatchUniverse pui}
                          {from to : NameSet}
                          {ps  : Sequence pu from to}
                          {ps' : Sequence pu from to}
                          (transitiveCommute : <<ps>> <~~>* <<ps'>>)
                        : canonicalise ps = canonicalise ps'.
Proof with auto.
admit.
Qed.

Lemma CanonicallyOrderedUnique  {pu_type : NameSet -> NameSet -> Type}
                                {ppu : PartPatchUniverse pu_type pu_type}
                                {pui : PatchUniverseInv ppu ppu}
                                {pu : PatchUniverse pui}
                                {from to : NameSet}
                                {ps  : Sequence pu from to}
                                {ps' : Sequence pu from to}
                                (psCanonicallyOrdered : CanonicallyOrdered ps)
                                (ps'CanonicallyOrdered : CanonicallyOrdered ps')
                                (transitiveCommute : <<ps>> <~~>* <<ps'>>)
                              : ps = ps'.
Proof with auto.
admit.
Qed.

(** %

XXX

% *)
End canonical_order.