GHeap.v 1.77 KB
Newer Older
charguer's avatar
charguer committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102


Set Implicit Arguments.

Record dynamic := dyn { 
  dyn_type : Type; 
  dyn_value : dyn_type }.

Definition loc := nat.

Definition heap := loc -> dynamic -> Prop.

(* isomorphic to:
Definition heap := loc -> option dynamic.
*)

Definition hprop := heap -> Prop.

Definition single id val : hprop :=
  fun (h:heap) => 
   (h = (fun id' val' => id = id' /\ val = val')).

Definition pure (P:Prop) : hprop :=
  fun (h:heap) => 
   (h = (fun id' val' => False)) /\ P.

Definition star (H1 H2:hprop) : hprop :=
  fun (h:heap) => H1 h /\ H2 h. (* should be star def *)

Definition heap_is_pack A (Hof : A -> hprop) : hprop := 
  fun h => exists x, Hof x h.

Notation "'Hexists' ( x1 : T ) , H" := (heap_is_pack (fun x1 : T => H))
  (at level 39, x1 ident, H at level 200).


Definition hpropsyntax := nat.

Parameter hpropsyntax_interp : hpropsyntax -> hprop.

Inductive lock_type : Type :=
  | lock : hpropsyntax -> lock_type. 

Definition islock id (H:hprop) : hprop :=
  Hexists (HS:hpropsyntax), 
  star (pure (H = hpropsyntax_interp HS))
       (single id (dyn (lock HS))).


Definition id0 := 0.
Definition H0 : hprop :=
  Hexists (H:hprop), islock id0 H.
 




















Set Implicit Arguments.

Record dynamic := dyn { 
  dyn_type : Type; 
  dyn_value : dyn_type }.

Definition loc := nat.

Definition heap := loc -> dynamic -> Prop.

(* isomorphic to:
Definition heap := loc -> option dynamic.
*)

Definition hprop := heap -> Prop.

Definition single id val : hprop :=
  fun (h:heap) => 
   (h = (fun id' val' => id = id' /\ val = val')).

(* if using Type, then H1 raises universe inconsistency *)
Inductive Lock : Prop := 
  | Lock_intro : hprop -> Lock.

Definition id0 := 0.
Definition H0 : hprop := single id0 (dyn 3).

Definition id1 := 1.
Definition H1 : hprop := single id1 (dyn (Lock_intro H0)).