(** %
\section{\label{sec:hunks}Hunks}
% *)
Module Export hunks.
(** %

End-to-end proof for hunks.

% *)

Require Import Arith.
Require Import Compare_dec.
Require Import Setoid.

Require Import unnamed_patches.
Require Import names.
Require Import named_patches.
Require Import patch_universes.
Require Import invertible_patchlike.
Require Import invertible_patch_universe.

(* The offset, remove and add values are the number of lines
   the hunk skips over, removes and adds respectively. *)
Inductive Hunk : Set
    := MkHunk : forall (offset remove add : nat), Hunk.

Definition hunkInverse (x : Hunk) : Hunk :=
    match x with
    MkHunk xOff xRemove xAdd => MkHunk xOff xAdd xRemove
    end.
Notation "p ^u" := (hunkInverse p).

(* This isn't the best definition of hunk commute that we can make,
   but it is a simple and consistent definition *)
Definition hunkCommute (x y y' x' : Hunk) : Prop :=
    match x, y, y', x' with
    MkHunk xOff  xRemove  xAdd,  MkHunk yOff  yRemove  yAdd,
    MkHunk yOff' yRemove' yAdd', MkHunk xOff' xRemove' xAdd' =>
    (xRemove = xRemove') /\ (xAdd = xAdd') /\
    (yRemove = yRemove') /\ (yAdd = yAdd') /\
    (
        (
            (xOff + xAdd < yOff) /\
            (xOff' = xOff) /\
            (yOff' = yOff - xAdd + xRemove)
        )
        \/
        (
            (yOff + yRemove < xOff) /\
            (xOff' = xOff - yRemove + yAdd) /\
            (yOff' = yOff)
        )
    )
    end.
Notation "<< p , q >> <~>u << q' , p' >>" := (hunkCommute p q q' p').

Definition HunkCommutable : Hunk -> Hunk -> Prop
 := fun (p : Hunk) => fun (q : Hunk) =>
    (exists q' : Hunk, exists p' : Hunk,
    <<p, q>> <~>u <<q', p'>>).
Notation "p <~?~>u q" := (HunkCommutable p q).

Lemma HunkCommuteUnique :
      forall (p   : Hunk) (q   : Hunk)
             (p'  : Hunk) (q'  : Hunk)
             (p'' : Hunk) (q'' : Hunk),
      <<p, q>> <~>u <<q', p'>>
   -> <<p, q>> <~>u <<q'', p''>>
   -> (p' = p'') /\ (q' = q'').
Proof.
intros.
unfold hunkCommute in H.
unfold hunkCommute in H0.
destruct p.
destruct q.
destruct p'.
destruct q'.
destruct p''.
destruct q''.
destruct H as [H1 H2].
split; f_equal; omega.
Qed.

Lemma HunkCommutable_dec :
      forall (p : Hunk) (q : Hunk),
      { q' : Hunk &
      { p' : Hunk &
      <<p, q>> <~>u <<q', p'>> }}
      +
      {~(p <~?~>u q)}.
Proof with auto.
intros.
unfold HunkCommutable.
destruct p as [pOff pRemove pAdd].
destruct q as [qOff qRemove qAdd].
unfold hunkCommute.
case (le_gt_dec qOff (pOff + pAdd)).
    case (le_gt_dec pOff (qOff + qRemove)).
        (* This is the "do not commute" case *)
        right.
        intro.
        destruct H as [p' [q' H]].
        destruct p'.
        destruct q'.
        omega.
    (* Commute option 2 *)
    left.
    exists (MkHunk qOff qRemove qAdd).
    exists (MkHunk (pOff - qRemove + qAdd) pRemove pAdd).
    split...
    split...
    split...
(* Commute option 1 *)
left.
exists (MkHunk (qOff - pAdd + pRemove) qRemove qAdd).
exists (MkHunk pOff pRemove pAdd).
split...
split...
split...
Qed.

Lemma HunkCommuteSelfInverseOneWay :
      forall (p  : Hunk) (q  : Hunk)
             (p' : Hunk) (q' : Hunk),
      (<<p,  q>>  <~>u <<q', p'>>) ->
      (<<q', p'>> <~>u <<p,  q>>).
Proof with auto.
intros.
destruct p.
destruct q.
destruct p'.
destruct q'.
unfold hunkCommute in H.
unfold hunkCommute.
omega.
Qed.

Lemma HunkCommuteSelfInverse :
      forall (p  : Hunk) (q  : Hunk)
             (p' : Hunk) (q' : Hunk),
      (<<p,  q>>  <~>u <<q', p'>>) <->
      (<<q', p'>> <~>u <<p,  q>>).
Proof.
intros.
split; apply HunkCommuteSelfInverseOneWay.
Qed.

Lemma HunkCommuteSquare :
      forall (p  : Hunk) (q  : Hunk)
             (p' : Hunk) (q' : Hunk),
      <<p, q>> <~>u <<q', p'>> ->
      << q'^u, p>> <~>u <<p', q^u>>.
Proof.
intros.
destruct p.
destruct q.
destruct p'.
destruct q'.
unfold hunkCommute in H.
unfold hunkCommute.
unfold hunkInverse.
omega.
Qed.

Lemma HunkCommuteConsistent1 :
      forall (p1 : Hunk)
             (q1 : Hunk)
             (r1 : Hunk)
             (q2 : Hunk)
             (r2 : Hunk)
             (q3 : Hunk)
             (r3 : Hunk)
             (p3 : Hunk)
             (p5 : Hunk),
      <<q1, r1>> <~>u <<r2, q2>>
   -> <<p1, q1>> <~>u <<q3, p5>>
   -> <<p5, r1>> <~>u <<r3, p3>>
   -> exists r4 : Hunk,
      exists q4 : Hunk,
      exists p6 : Hunk,
      <<q3, r3>> <~>u <<r4, q4>> /\
      <<p1, r2>> <~>u <<r4, p6>> /\
      <<p6, q2>> <~>u <<q4, p3>>.
Proof with auto.
intros.
destruct p1 as [p1Offset p1Remove p1Add].
destruct q1 as [q1Offset q1Remove q1Add].
destruct r1 as [r1Offset r1Remove r1Add].
destruct q2 as [q2Offset q2Remove q2Add].
destruct r2 as [r2Offset r2Remove r2Add].
destruct p3 as [p3Offset p2Remove p2Add].
destruct q3 as [q3Offset q3Remove q3Add].
destruct r3 as [r3Offset r3Remove r3Add].
destruct p5 as [p5Offset p5Remove p5Add].
unfold hunkCommute in *.
intuition.

(* Case 1: p changes before q, q changes before r *)
exists (MkHunk (r3Offset - q3Add + q3Remove) r3Remove r3Add).
exists (MkHunk q3Offset q3Remove q3Add).
exists (MkHunk p1Offset p1Remove p1Add).
subst.
intuition.

(* Case 3: q changes before p, p changes before r *)
exists (MkHunk (r3Offset - q3Add + q3Remove) r3Remove r3Add).
exists (MkHunk q3Offset q3Remove q3Add).
exists (MkHunk p1Offset p1Remove p1Add).
subst.
intuition.

(* Case 4: q changes before r, r changes before p *)
exists (MkHunk (r3Offset - q3Add + q3Remove) r3Remove r3Add).
exists (MkHunk q3Offset q3Remove q3Add).
exists (MkHunk (p1Offset - r1Remove + r1Add) p1Remove p1Add).
subst.
intuition.

(* Case 5: p changes before r, r changes before q *)
exists (MkHunk r3Offset r3Remove r3Add).
exists (MkHunk (q3Offset - r3Remove + r3Add) q3Remove q3Add).
exists (MkHunk p1Offset p1Remove p1Add).
subst.
intuition.

(* Case 6: r changes before p, p changes before q *)
exists (MkHunk r3Offset r3Remove r3Add).
exists (MkHunk (q3Offset - r3Remove + r3Add) q3Remove q3Add).
exists (MkHunk (p1Offset - r1Remove + r1Add) p1Remove p1Add).
subst.
intuition.

(* Case 8: r changes before q, q changes before p *)
exists (MkHunk r3Offset r3Remove r3Add).
exists (MkHunk (q3Offset - r3Remove + r3Add) q3Remove q3Add).
exists (MkHunk (p1Offset - r1Remove + r1Add) p1Remove p1Add).
subst.
intuition.
Qed.

Lemma HunkCommuteConsistent2 :
      forall (p3 : Hunk)
             (q3 : Hunk)
             (r3 : Hunk)
             (q4 : Hunk)
             (r4 : Hunk)
             (q1 : Hunk)
             (r1 : Hunk)
             (p1 : Hunk)
             (p5 : Hunk),
      <<q3, r3>> <~>u <<r4, q4>>
   -> <<r3, p3>> <~>u <<p5, r1>>
   -> <<q3, p5>> <~>u <<p1, q1>>
   -> exists r2 : Hunk,
      exists q2 : Hunk,
      exists p6 : Hunk,
      <<q1, r1>> <~>u <<r2, q2>> /\
      <<q4, p3>> <~>u <<p6, q2>> /\
      <<r4, p6>> <~>u <<p1, r2>>.
Proof with auto.
intros.
destruct p3 as [p3Offset p3Remove p3Add].
destruct q3 as [q3Offset q3Remove q3Add].
destruct r3 as [r3Offset r3Remove r3Add].
destruct q4 as [q4Offset q4Remove q4Add].
destruct r4 as [r4Offset r4Remove r4Add].
destruct p1 as [p1Offset p1Remove p1Add].
destruct q1 as [q1Offset q1Remove q1Add].
destruct r1 as [r1Offset r1Remove r1Add].
destruct p5 as [p5Offset p5Remove p5Add].
unfold hunkCommute in *.
intuition.

(* Case 1: q changes before r, r changes before p *)
exists (MkHunk (r1Offset - q1Add + q1Remove) r1Remove r1Add).
exists (MkHunk q1Offset q1Remove q1Add).
exists (MkHunk (p3Offset - q4Add + q4Remove) p1Remove p1Add).
subst.
intuition.

(* Case 3: q changes before p, p changes before r *)
exists (MkHunk (r1Offset - q1Add + q1Remove) r1Remove r1Add).
exists (MkHunk q1Offset q1Remove q1Add).
exists (MkHunk (p3Offset - q4Add + q4Remove) p1Remove p1Add).
subst.
intuition.

(* Case 4: p changes before q, q changes before r *)
exists (MkHunk (r1Offset - q1Add + q1Remove) r1Remove r1Add).
exists (MkHunk q1Offset q1Remove q1Add).
exists (MkHunk p1Offset p1Remove p1Add).
subst.
intuition.

(* Case 5: r changes before q, q changes before p *)
exists (MkHunk r1Offset r1Remove r1Add).
exists (MkHunk (q1Offset - r1Remove + r1Add) q1Remove q1Add).
exists (MkHunk (p3Offset - q4Add + q4Remove) p1Remove p1Add).
subst.
intuition.

(* Case 6: r changes before p, p changes before q *)
exists (MkHunk r1Offset r1Remove r1Add).
exists (MkHunk (q1Offset - r1Remove + r1Add) q1Remove q1Add).
exists (MkHunk p3Offset p1Remove p1Add).
subst.
intuition.

(* Case 8: p changes before r, r changes before q *)
exists (MkHunk r1Offset r1Remove r1Add).
exists (MkHunk (q1Offset - r1Remove + r1Add) q1Remove q1Add).
exists (MkHunk p1Offset p1Remove p1Add).
subst.
intuition.
Qed.

Lemma hunkInverseInverse : forall (p : Hunk), (p ^u)^u = p.
Proof.
intros.
destruct p.
unfold hunkInverse.
auto.
Qed.

Definition HunkUnnamedPatch : UnnamedPatch :=
    mkUnnamedPatch
        Hunk
        hunkInverse
        hunkInverseInverse
        hunkCommute
        HunkCommuteUnique
        HunkCommutable_dec
        HunkCommuteSelfInverse
        HunkCommuteSquare
        HunkCommuteConsistent1
        HunkCommuteConsistent2.

Instance HunkPartPatchUniverse : PartPatchUniverse (NamedPatch HunkUnnamedPatch) (NamedPatch HunkUnnamedPatch) := NamedPartPatchUniverse HunkUnnamedPatch.
Instance HunkPatchUniverseInv : PatchUniverseInv (NamedPartPatchUniverse HunkUnnamedPatch) (NamedPartPatchUniverse HunkUnnamedPatch) := NamedPatchUniverseInv HunkPartPatchUniverse.
Instance HunkPatchUniverse :
             PatchUniverse (NamedPatchUniverseInv HunkPartPatchUniverse)
      := NamedPatchUniverse HunkPatchUniverseInv.
Instance HunkInvertiblePatchlike : InvertiblePatchlike (NamedPatch HunkUnnamedPatch) := NamedInvertiblePatchlike HunkUnnamedPatch.
Instance HunkInvertiblePatchUniverse :
             InvertiblePatchUniverse (NamedPatchUniverse HunkPatchUniverseInv)
                                     (NamedInvertiblePatchlike HunkUnnamedPatch)
      := NamedInvertiblePatchUniverse.

Lemma hunkCommuteInSequenceConsistent :
    forall {o oq oqr oqrs ou our ours : NameSet}
           {qs : Sequence HunkPatchUniverse o oq}
           {r : NamedPatch HunkUnnamedPatch oq oqr}
           {s : NamedPatch HunkUnnamedPatch oqr oqrs}
           (* ts omitted for now *)
           {us : Sequence HunkPatchUniverse o ou}
           {r' : NamedPatch HunkUnnamedPatch ou our}
           {s' : NamedPatch HunkUnnamedPatch our ours}
           {vs : Sequence HunkPatchUniverse ours oqrs}

           (s_NilConsOK : ConsOK s [])
           (r_s_NilConsOK : ConsOK r (s :> []))
           (qs_r_s_NilAppendOK : AppendOK qs (r :> s :> []))

           (s'_vsConsOK : ConsOK s' vs)
           (r'_s'_vsConsOK : ConsOK r' (s' :> vs))
           (us_r'_s'_vsAppendOK : AppendOK us (r' :> (s' :> vs))),
    (<<qs :+> r :> s :> []>> <~~>* <<us :+> r' :> s' :> vs>>)
 -> (pu_nameOf r = pu_nameOf r')
 -> (pu_nameOf s = pu_nameOf s')
 -> (r <~?~> s)
 -> (r' <~?~> s').
Proof.
apply (@commuteInSequenceConsistent
           (NamedPatch HunkUnnamedPatch)
           HunkPartPatchUniverse
           HunkPatchUniverseInv
           HunkPatchUniverse).
Qed.

End hunks.