Require Import List Vbase Varith Vlist extralib.
Require Import Classical ClassicalDescription IndefiniteDescription.
Require Import permission fslassn.
Require Import GpsSepAlg.

Set Implicit Arguments.

Definition assn_mod PS PSg := { P : assn PS PSg | assn_norm P = P }.

Inductive HeapLabel :=
  | HLnormal
  | HLtriangle
  | HLnabla.

Inductive HeapLabelCombination :=
  | HLCnormal
  | HLCtriangle
  | HLCnabla
  | HLCdiamond
  | HLCtriangledot
  | HLCnabladot
  | HLCdiamonddot.

Coercion label_to_combination (lbl: HeapLabel) :=
  match lbl with
    | HLnormal ⇒ HLCnormal
    | HLtriangle ⇒ HLCtriangle
    | HLnabla ⇒ HLCnabla
  end.

Coercion label_to_combination_option (lbl: HeapLabel) := Some (label_to_combination lbl).

Definition is_basic lbl := lbl = HLCnormal ∨ lbl = HLCtriangle ∨ lbl = HLCnabla.

Definition is_normal lbl := lbl = HLCnormal ∨ lbl = HLCtriangledot ∨ lbl = HLCnabladot ∨ lbl = HLCdiamonddot.

Definition is_triangle lbl := lbl = HLCtriangle ∨ lbl = HLCtriangledot ∨ lbl = HLCdiamond ∨ lbl = HLCdiamonddot.

Definition is_nabla lbl := lbl = HLCnabla ∨ lbl = HLCnabladot ∨ lbl = HLCdiamond ∨ lbl = HLCdiamonddot.

Definition is_normalO olbl :=
  match olbl with
    | Some lbl ⇒ is_normal lbl
    | None ⇒ False
  end.

Definition HLleq lbl1 lbl2 :=
  match lbl1, lbl2 with
    | HLCnormal , _ ⇒ is_normal lbl2
    | HLCtriangle , _ ⇒ is_triangle lbl2
    | HLCnabla , _ ⇒ is_nabla lbl2
    | HLCdiamond , _ ⇒ lbl2 = HLCdiamond ∨ lbl2 = HLCdiamonddot
    | HLCtriangledot, _ ⇒ lbl2 = HLCtriangledot ∨ lbl2 = HLCdiamonddot
    | HLCnabladot , _ ⇒ lbl2 = HLCnabladot ∨ lbl2 = HLCdiamonddot
    | HLCdiamonddot , _ ⇒ lbl2 = HLCdiamonddot
  end.

Definition oHLleq (olbl1 olbl2: option HeapLabelCombination) :=
  match olbl1, olbl2 with
    | None, _ ⇒ True
    | Some lbl1, Some lbl2 ⇒ HLleq lbl1 lbl2
    | _, _ ⇒ False
  end.

Definition permissionsOK (PS : Permission) (x y z: PS) := << PSUMdef: x ## y ## z ≠ Pundef PS >> ∧
                                                            << PSUMnonzero: x ## y ## z ≠ Pzero PS >>.
Arguments permissionsOK [PS] _ _ _.

Inductive HeapVal PS PSg :=
  | HVnone
  | HVuval (lbl: HeapLabel)
  | HVval (v: val) (Perm: Permission) (pNormal pTriangle pNabla : Perm)
                   (WFperm: permissionsOK pNormal pTriangle pNabla)
  | HVra (RR QQ: val → assn_mod PS PSg) (isrmwflag: bool) (permlbl: option HeapLabelCombination)
          (init: option HeapLabelCombination).

Arguments HVnone {PS} {PSg}.

Arguments HVuval [PS] [PSg] _.

Arguments HVval [PS] [PSg] _ _ _ _ _ _.

Arguments HVra [PS] [PSg] _ _ _ _ _.

Program Definition lvalue PS PSg Perm v := @HVval PS PSg v Perm (Pfull Perm) (Pzero Perm) (Pzero Perm) _.
Next Obligation. split; pplus_zero_simpl; eauto using Pfull_is_not_Pzero, Pfull_is_not_Pundef. Qed.

Inductive heap PS PSg :=
  | Hundef
  | Hdef (hf: val → HeapVal PS PSg) (g : ghost_resource).

Definition HVlabeled PS PSg (hv : HeapVal PS PSg) (lbl : HeapLabel) :=
  match hv with
    | HVnone ⇒ True
    | HVuval lbl' ⇒ lbl' = lbl
    | HVval _ Perm pNormal pTriangle pNabla _ ⇒ match lbl with
                                                   | HLnormal ⇒ pNormal ≠ Pzero Perm
                                                   | HLtriangle ⇒ pTriangle ≠ Pzero Perm
                                                   | HLnabla ⇒ pNabla ≠ Pzero Perm
                                                 end
    | HVra _ _ _ None None ⇒ False
    | HVra _ _ _ (Some permlbl) None ⇒ HLleq lbl permlbl
    | HVra _ _ _ None (Some initlbl) ⇒ HLleq lbl initlbl
    | HVra _ _ _ (Some permlbl) (Some initlbl) ⇒ HLleq lbl permlbl ∨ HLleq lbl initlbl
  end.

Definition HFlabeled PS PSg (hf : val → HeapVal PS PSg) lbl := ∀ (l: val) , HVlabeled (hf l) lbl.

Definition Hlabeled PS PSg (h : heap PS PSg) lbl := ∃ hf g, h = Hdef hf g ∧ HFlabeled hf lbl.

Definition HVlabeledExact PS PSg (hv: HeapVal PS PSg) (lbl: HeapLabel) :=
  match hv with
    | HVnone ⇒ True
    | HVuval lbl' ⇒ lbl' = lbl
    | HVval _ Perm pNormal pTriangle pNabla _ ⇒
              match lbl with
                | HLnormal ⇒ pTriangle = Pzero Perm ∧ pNabla = Pzero Perm
                | HLtriangle ⇒ pNormal = Pzero Perm ∧ pNabla = Pzero Perm
                | HLnabla ⇒ pNormal = Pzero Perm ∧ pTriangle = Pzero Perm
              end
    | HVra _ _ _ None None ⇒ True
    | HVra _ _ _ (Some permlbl) None ⇒ permlbl = lbl
    | HVra _ _ _ None (Some initlbl) ⇒ initlbl = lbl
    | HVra _ _ _ (Some permlbl) (Some initlbl) ⇒ permlbl = lbl ∧ initlbl = lbl
  end.

Definition HFlabeledExact PS PSg (hf: val → HeapVal PS PSg) lbl := ∀ (l: val), HVlabeledExact (hf l) lbl.

Definition HlabeledExact PS PSg (h: heap PS PSg) lbl := ∃ hf g, h = Hdef hf g ∧ HFlabeledExact hf lbl.

Definition HVlabeledR PS PSg (hv: HeapVal PS PSg) (lbl: HeapLabel) :=
  match hv with
    | HVnone ⇒ False
    | HVuval _ ⇒ False
    | HVval _ Perm pNormal pTriangle pNabla _ ⇒ match lbl with
                                                   | HLnormal ⇒ pNormal ≠ Pzero Perm
                                                   | HLtriangle ⇒ pTriangle ≠ Pzero Perm
                                                   | HLnabla ⇒ pNabla ≠ Pzero Perm
                                                 end
    | HVra _ _ _ _ (Some initlbl) ⇒ HLleq lbl initlbl
    | _ ⇒ False
  end.

Definition HLCsim (lbl1 lbl2: option HeapLabelCombination) :=
  match lbl1, lbl2 with
    | None, None ⇒ True
    | (Some _), (Some _) ⇒ True
    | _, _ ⇒ False
  end.

Definition HVsim PS PSg (hv hv': HeapVal PS PSg) :=
  match hv, hv' with
    | HVnone, HVnone ⇒ True
    | HVuval _, HVuval _ ⇒ True
    | HVval v Perm pNormal pTriangle pNabla _, HVval v' Perm' pNormal' pTriangle' pNabla' _
                 ⇒ match excluded_middle_informative (Perm = Perm') return Prop with
                      | right _ ⇒ False
                      | left EQ ⇒ v = v' ∧
                                   (eq_rect Perm (fun x ⇒ x) pNormal Perm' EQ)
                                   ## (eq_rect Perm (fun x ⇒ x) pTriangle Perm' EQ)
                                   ## (eq_rect Perm (fun x ⇒ x) pNabla Perm' EQ)
                                   = pNormal' ## pTriangle' ## pNabla'
                    end
    | HVra RR QQ isrmwflag permlbl init, HVra RR' QQ' isrmwflag' permlbl' init'
                 ⇒ RR = RR' ∧ QQ = QQ' ∧ isrmwflag = isrmwflag' ∧ HLCsim permlbl permlbl' ∧ HLCsim init init'
    | _, _ ⇒ False
  end.

Definition HFsim PS PSg (hf hf': val → HeapVal PS PSg) := ∀ (l: val), HVsim (hf l) (hf' l).

Definition Hsim PS PSg (h h': heap PS PSg) := ∃ hf hf' g, h = Hdef hf g ∧ h' = Hdef hf' g ∧ HFsim hf hf'.

Program Definition lupd PS PSg (h: heap PS PSg) lbl :=
  match h return heap PS PSg with
    | Hundef _ _⇒ Hundef PS PSg
    | Hdef hf g ⇒ Hdef (fun l ⇒
                          match hf l return HeapVal PS PSg with
                            | HVnone ⇒ @HVnone PS PSg
                            | HVuval _ ⇒ @HVuval PS PSg lbl
                            | HVval v Perm pNormal pTriangle pNabla _
                                ⇒ match lbl return HeapVal PS PSg with
                                   | HLnormal
                                       ⇒ @HVval PS PSg v
                                                 Perm (pNormal ## pTriangle ## pNabla) (Pzero Perm) (Pzero Perm) _
                                   | HLtriangle
                                       ⇒ @HVval PS PSg v
                                                 Perm (Pzero Perm) (pNormal ## pTriangle ## pNabla) (Pzero Perm) _
                                   | HLnabla
                                       ⇒ @HVval PS PSg v
                                                 Perm (Pzero Perm) (Pzero Perm) (pNormal ## pTriangle ## pNabla) _
                                   end
                            | HVra PP QQ isrmw None None ⇒ HVra PP QQ isrmw None None
                            | HVra PP QQ isrmw (Some _) None ⇒ HVra PP QQ isrmw lbl None
                            | HVra PP QQ isrmw None (Some _) ⇒ HVra PP QQ isrmw None lbl
                            | HVra PP QQ isrmw (Some _) (Some _) ⇒ HVra PP QQ isrmw lbl lbl
                          end) g
  end.
Next Obligation. by red; rewrite ?permission_plus_zero_r, ?permission_plus_zero_l. Qed.
Next Obligation. by red; rewrite ?permission_plus_zero_r, ?permission_plus_zero_l. Qed.
Next Obligation. by red; rewrite ?permission_plus_zero_r, ?permission_plus_zero_l. Qed.

Arguments Hundef {PS} {PSg}.

Definition is_lvalue PS PSg (v: HeapVal PS PSg) :=
  match v with
    | HVuval lbl ⇒ lbl = HLnormal
    | HVval _ Perm pNormal _ _ _ ⇒ pNormal = Pfull Perm
    | _ ⇒ False
  end.

Definition is_rvalue PS PSg (v: HeapVal PS PSg) :=
  match v with
    | HVval _ Perm pNormal _ _ _ ⇒ pNormal ≠ Pzero Perm
    | _ ⇒ False
  end.

Definition is_rvalueV PS PSg (hv: HeapVal PS PSg) v :=
  match hv with
    | HVval v' Perm pNormal _ _ _ ⇒ v = v' ∧ pNormal ≠ Pzero Perm
    | _ ⇒ False
  end.

Definition has_value PS PSg (hv: HeapVal PS PSg) v :=
  match hv with
    | HVval v' _ _ _ _ _ ⇒ v' = v
    | _ ⇒ False
  end.

Definition is_nonatomic PS PSg (hv: HeapVal PS PSg) :=
  match hv with
    | HVval _ _ _ _ _ _ ⇒ true
    | HVuval _ ⇒ true
    | _ ⇒ false
  end.

Definition is_atomic PS PSg (hv: HeapVal PS PSg) :=
  match hv with
    | HVra _ _ _ _ _ ⇒ true
    | _ ⇒ false
  end.

Definition mk_assn_mod PS PSg (P: assn PS PSg) : assn_mod PS PSg := exist _ _ (assn_norm_idemp P).

Definition hemp {PS} {PSg} := Hdef (fun v ⇒ @HVnone PS PSg) gres_emp.

Definition Acombinable PS PSg (P Q : assn PS PSg) :=
  P = Afalse ∨ Q = Afalse ∨ P = Q.

Definition hv_rval PS PSg isrmw (P: assn PS PSg) :=
  match isrmw with
    | true ⇒ P
    | false ⇒ Aemp
  end.

Definition hv_acq_def PS PSg isrmw1 Q1 isrmw2 Q2 :=
  hv_rval isrmw2 Q1 = hv_rval isrmw1 Q2
  ∨ Q1 = (@Afalse PS PSg) ∧ Q2 = (@Afalse PS PSg).

Definition hvplusDEF PS PSg (hv hv' : HeapVal PS PSg) : Prop :=
  match hv, hv' return Prop with
    | HVnone, _ ⇒ True
    | _, HVnone ⇒ True
    | HVuval _, HVuval _ ⇒ False
    | HVval v Perm pNormal pTriangle pNabla _, HVval v' Perm' pNormal' pTriangle' pNabla' _ ⇒
        match excluded_middle_informative (Perm = Perm') return Prop with
          | right _ ⇒ False
          | left EQ ⇒ v = v' ∧
                       permissionsOK ((eq_rect Perm (fun x ⇒ x) pNormal Perm' EQ) ## pNormal')
                                     ((eq_rect Perm (fun x ⇒ x) pTriangle Perm' EQ) ## pTriangle')
                                     ((eq_rect Perm (fun x ⇒ x) pNabla Perm' EQ) ## pNabla')
        end
    | HVra RR1 QQ1 isrmw1 permlbl1 init1, HVra RR2 QQ2 isrmw2 permlbl2 init2 ⇒
        (∀ v, hv_acq_def isrmw1 (sval (QQ1 v)) isrmw2 (sval (QQ2 v))) ∧
        (∀ v, Acombinable (sval (RR1 v)) (sval (RR2 v)))
    | _, _ ⇒ False
  end.

Definition hlplus lbl1 lbl2 :=
  match lbl1, lbl2 with
    | HLCdiamonddot , _ ⇒ HLCdiamonddot
    | _ , HLCdiamonddot ⇒ HLCdiamonddot
    | HLCnabladot , HLCtriangledot ⇒ HLCdiamonddot
    | HLCnabladot , HLCdiamond ⇒ HLCdiamonddot
    | HLCnabladot , HLCtriangle ⇒ HLCdiamonddot
    | HLCnabladot , _ ⇒ HLCnabladot
    | HLCtriangledot , HLCnabladot ⇒ HLCdiamonddot
    | HLCtriangledot , HLCdiamond ⇒ HLCdiamonddot
    | HLCtriangledot , HLCnabla ⇒ HLCdiamonddot
    | HLCtriangledot , _ ⇒ HLCtriangledot
    | HLCdiamond , HLCnabladot ⇒ HLCdiamonddot
    | HLCdiamond , HLCtriangledot ⇒ HLCdiamonddot
    | HLCdiamond , HLCnormal ⇒ HLCdiamonddot
    | HLCdiamond , _ ⇒ HLCdiamond
    | HLCnabla , HLCnabladot ⇒ HLCnabladot
    | HLCnabla , HLCtriangledot ⇒ HLCdiamonddot
    | HLCnabla , HLCdiamond ⇒ HLCdiamond
    | HLCnabla , HLCnabla ⇒ HLCnabla
    | HLCnabla , HLCtriangle ⇒ HLCdiamond
    | HLCnabla , HLCnormal ⇒ HLCnabladot
    | HLCtriangle , HLCnabladot ⇒ HLCdiamonddot
    | HLCtriangle , HLCtriangledot ⇒ HLCtriangledot
    | HLCtriangle , HLCdiamond ⇒ HLCdiamond
    | HLCtriangle , HLCnabla ⇒ HLCdiamond
    | HLCtriangle , HLCtriangle ⇒ HLCtriangle
    | HLCtriangle , HLCnormal ⇒ HLCtriangledot
    | HLCnormal , HLCnabladot ⇒ HLCnabladot
    | HLCnormal , HLCtriangledot ⇒ HLCtriangledot
    | HLCnormal , HLCdiamond ⇒ HLCdiamonddot
    | HLCnormal , HLCnabla ⇒ HLCnabladot
    | HLCnormal , HLCtriangle ⇒ HLCtriangledot
    | HLCnormal , HLCnormal ⇒ HLCnormal
  end.

Definition ohlplus lbl1 lbl2 :=
  match lbl1, lbl2 with
    | None, lbl ⇒ lbl
    | lbl, None ⇒ lbl
    | (Some lbl1'), (Some lbl2') ⇒ Some (hlplus lbl1' lbl2')
  end.

Program Definition hvplus PS PSg (hv hv' : HeapVal PS PSg) : HeapVal PS PSg :=
  match hv, hv' return HeapVal PS PSg with
    | HVnone, _ ⇒ hv'
    | _, HVnone ⇒ hv
    | HVval v Perm pNormal pTriangle pNabla _, HVval v' Perm' pNormal' pTriangle' pNabla' _ ⇒
        match excluded_middle_informative (Perm = Perm') return HeapVal PS PSg with
          | right _ ⇒ @HVval PS PSg 0 Perm' (Pfull Perm') (Pzero Perm') (Pzero Perm') _
          | left EQ ⇒ if excluded_middle_informative
                            (permissionsOK ((eq_rect Perm (fun x ⇒ x) pNormal Perm' EQ) ## pNormal')
                                           ((eq_rect Perm (fun x ⇒ x) pTriangle Perm' EQ) ## pTriangle')
                                           ((eq_rect Perm (fun x ⇒ x) pNabla Perm' EQ) ## pNabla'))
                       then @HVval PS PSg v Perm' ((eq_rect Perm (fun x ⇒ x) pNormal Perm' EQ) ## pNormal')
                                                  ((eq_rect Perm (fun x ⇒ x) pTriangle Perm' EQ) ## pTriangle')
                                                  ((eq_rect Perm (fun x ⇒ x) pNabla Perm' EQ) ## pNabla') _
                       else @HVval PS PSg 0 Perm' (Pfull Perm') (Pzero Perm') (Pzero Perm') _
        end
    | HVra RR1 QQ1 isrmw1 permlbl1 init1, HVra RR2 QQ2 isrmw2 permlbl2 init2 ⇒
        HVra (fun v ⇒ if excluded_middle_informative (sval (RR1 v) = Afalse) then RR2 v else RR1 v)
              (if isrmw1 then QQ1
                else if isrmw2 then QQ2
                else fun v ⇒ mk_assn_mod (Astar (sval (QQ1 v)) (sval (QQ2 v))))
              (isrmw1 || isrmw2)
              (ohlplus permlbl1 permlbl2)
              (ohlplus init1 init2)
    | _, _ ⇒ hv
  end.
Next Obligation.
  split; rewrite !permission_plus_zero_r; [apply Pfull_is_not_Pundef | apply Pfull_is_not_Pzero].
Qed.
Next Obligation.
  split; rewrite !permission_plus_zero_r; [apply Pfull_is_not_Pundef | apply Pfull_is_not_Pzero].
Qed.

Definition resources_compatible PS PSg (hf1 hf2: val → HeapVal PS PSg) (g1 g2 : ghost_resource) :=
  excluded_middle_informative (
     << HEAPcompat: ∀ v, hvplusDEF (hf1 v) (hf2 v) >> ∧
     << GHOSTcompat: gres_plus g1 g2 ≠ None>> ).

Definition hplus PS PSg (h1 h2: heap PS PSg) : heap PS PSg :=
  match h1, h2 with
    | Hundef, _ ⇒ Hundef
    | _, Hundef ⇒ Hundef
    | Hdef hf1 g1, Hdef hf2 g2 ⇒
      if resources_compatible hf1 hf2 g1 g2 then
        Hdef (fun v ⇒ hvplus (hf1 v) (hf2 v)) (gres_plus_total g1 g2)
      else Hundef
  end.

Definition hsum PS PSg (l: list (heap PS PSg)) := foldr (@hplus PS PSg) l hemp.

Definition hupd B (h : nat → B) y z := fun x ⇒ if x == y then z else h x.

Notation hsingl PS PSg l v := (Hdef (hupd (fun _ ⇒ @HVnone PS PSg) l v) gres_emp).

Notation gsingl PS PSg l g := (Hdef (fun _ : val ⇒ @HVnone PS PSg) (gres_one l g)).

Notation gheap PS PSg g := (Hdef (fun _ ⇒ @HVnone PS PSg) g).

Definition initialize PS PSg (h: val → HeapVal PS PSg) l :=
  hupd h l (match h l with
              | HVra PP QQ permlbl isrmw init ⇒ HVra PP QQ permlbl isrmw (ohlplus init (Some HLCnormal))
              | _ ⇒ h l end).

Global Opaque hplus.

Definition Wemp {PS} {PSg} : val → assn_mod PS PSg := fun _ ⇒ mk_assn_mod Afalse.
Definition Remp {PS} {PSg} : val → assn_mod PS PSg := fun _ ⇒ mk_assn_mod Aemp.

Lemma equal_exist:
  ∀ (U : Type) (P : U → Prop) (x y : U) (p : P x) (q : P y),
  x = y → exist P x p = exist P y q.
Proof.
  ins; desf; f_equal; apply proof_irrelevance.
Qed.

Program Fixpoint assn_sem PS PSg (P : assn PS PSg) (h : heap PS PSg) :=
  match P with
    | Afalse ⇒ False
    | Aemp ⇒ h = hemp
    | Aimplies P Q ⇒ h ≠ Hundef ∧ (assn_sem P h → assn_sem Q h)
    | Aforall PP ⇒ ∀ x, assn_sem (PP x) h
    | Apt Perm _ p _ E E' ⇒ h = hsingl PS PSg E (@HVval PS PSg E' Perm p (Pzero Perm) (Pzero Perm) _)
    | Aptu E ⇒ h = hsingl PS PSg E (@HVuval PS PSg HLnormal)
    | Astar P Q ⇒ ∃ h1 h2, h ≠ Hundef ∧ hplus h1 h2 = h ∧ assn_sem P h1 ∧ assn_sem Q h2
    | Arainit E ⇒ h = hsingl PS PSg E (HVra Wemp Remp false None (Some HLCnormal))
    | Arel E P ⇒ h = hsingl PS PSg E (HVra (fun x ⇒ mk_assn_mod (P x)) Remp false (Some HLCnormal) None)
    | Aacq E Q ⇒ h = hsingl PS PSg E (HVra Wemp (fun x ⇒ mk_assn_mod (Q x)) false None None)
    | Armwacq E Q ⇒ h = hsingl PS PSg E (HVra Wemp (fun x ⇒ mk_assn_mod (Q x)) true (Some HLCnormal) None)
    | Atriangle Q ⇒ HlabeledExact h HLtriangle ∧
                       ∃ h', assn_sem Q h' ∧ Hsim h h' ∧ HlabeledExact h' HLnormal
    | Anabla Q ⇒ HlabeledExact h HLnabla ∧
                       ∃ h', assn_sem Q h' ∧ Hsim h h' ∧ HlabeledExact h' HLnormal
    | Aghost PCM _ E g ⇒ h = gsingl PS PSg E (Some (existT (fun m : salg_mod ⇒ m) PCM g))
end.
Next Obligation. by red; rewrite !permission_plus_zero_r. Qed.

Definition implies PS PSg (P Q: assn PS PSg) := ∀ h, assn_sem P h → assn_sem Q h.

Definition precise PS PSg (P: assn PS PSg) :=
  ∀ hP (SEM: assn_sem P hP) hP' (SEM': assn_sem P hP')
         hF (DEF: hplus hP hF ≠ Hundef) hF' (EQ: hplus hP hF = hplus hP' hF'),
  hP = hP' ∧ hF = hF'.

Definition normalizable PS PSg (P: assn PS PSg) :=
  ∀ h, assn_sem P h → ∃ hN h', assn_sem P hN ∧ HlabeledExact hN HLnormal ∧ h = hplus hN h'.

Definition Anot PS PSg (P: assn PS PSg) := Aimplies P Afalse.
Definition Adisj PS PSg (P Q: assn PS PSg) := Aimplies (Anot P) Q.
Definition Aconj PS PSg (P Q: assn PS PSg) := Anot (Adisj (Anot P) (Anot Q)).
Definition Aexists PS PSg (PP: val → assn PS PSg) := Anot (Aforall (fun x ⇒ Anot (PP x))).