Work on denv.

theories/vcgen/denv.v

@@ -5,13 +5,11 @@ From iris_c.lib Require Import U locking_heap.
 From iris_c.c_translation Require Import monad.
 From iris.algebra Require Import frac.
 
-
 (* Questions :
    - Should we extend denv_{exhale|inhale_frac|inhale_full} to (dLocUnknown l) (in which case it would
    immediately return None) ?
 *)
 Section denv.
-
   Definition locs := list loc.
 
   Record denv_item := DenvItem {
@@ -20,92 +18,100 @@ Section denv.
     denv_dval  : dval
   }.
 
-  Definition denv := list (option (denv_item)).
+  Definition denv := list (option denv_item).
 
-  Definition denv_item_opt_merge (dio1 dio2: option denv_item) : option denv_item :=
+  Definition denv_item_opt_merge (dio1 dio2 : option denv_item) : option denv_item :=
     match dio1, dio2 with
     | None, dio | dio, None => dio
     | Some di1, Some di2 =>
       Some (DenvItem (denv_level di1) ((denv_frac di1) + (denv_frac di2)) (denv_dval di1))
     end.
 
-  Fixpoint denv_merge (m1 m2: denv) : denv :=
+  Fixpoint denv_merge (m1 m2 : denv) : denv :=
     match m1, m2 with
     | m, [] | [], m => m
     | dio1 :: m1', dio2 :: m2' => denv_item_opt_merge dio1 dio2 :: denv_merge m1' m2'
     end.
 
-  Fixpoint denv_exhale_aux (i : nat) (x: level) (q: frac) (dv: dval) : denv :=
+  Fixpoint denv_singleton (i : nat) (lv : level) (q : frac) (dv : dval) : denv :=
     match i with
-    | O => [Some (DenvItem x q dv)]
-    | S i => None :: denv_exhale_aux i x q dv
+    | O => [Some (DenvItem lv q dv)]
+    | S i => None :: denv_singleton i lv q dv
     end.
 
   Fixpoint denv_exhale (i : nat) (x: level) (q: frac) (dv: dval) (m: denv) : denv :=
     match m with
-    | [] => denv_exhale_aux i x q dv
+    | [] => denv_singleton i x q dv
     | dio :: m' =>
       match i with
       | O => match dio with
-            | None => Some (DenvItem x q dv) :: m'
-            | Some di => Some (DenvItem x ((denv_frac di) + q) dv) :: m'
-            end
+             | None => Some (DenvItem x q dv) :: m'
+             | Some di => Some (DenvItem x ((denv_frac di) + q) dv) :: m'
+             end
       | S i => dio :: denv_exhale i x q dv m'
       end
     end.
 
-  Fixpoint denv_inhale_frac (i: nat) (m: denv) : option (frac * dval * denv) :=
+  Fixpoint denv_inhale_frac (i : nat) (m : denv) : option (frac * dval * denv) :=
     match m with
     | [] => None
     | dio :: m' =>
       match i with
-      | O   => di ← dio ; Some (denv_frac di, denv_dval di, m')
+      | O   =>
+         ''(DenvItem lv q dv) ← dio;
+         guard (lv = ULvl);
+         Some ((q / 2)%Qp, dv, Some (DenvItem lv (q / 2) dv) :: m')
       | S i => ''(q, dv, m') ← denv_inhale_frac i m; Some (q, dv, dio :: m')
       end
     end.
 
-
-  Fixpoint denv_inhale_full (i: nat) (m: denv) : option (dval * denv) :=
+  Fixpoint denv_inhale_full_aux (i : nat) (m : denv) : option (frac * dval * denv) :=
     match m with
     | [] => None
     | dio :: m' =>
       match i with
-      | O => di ← dio ; if (bool_decide (denv_frac di = 1%Qp)) then Some (denv_dval di, m') else None
-      | S i => ''(dv, mf) ← denv_inhale_full i m'; Some (dv, dio :: mf)
+      | O =>
+         ''(DenvItem lv q dv) ← dio;
+         guard (lv = ULvl);
+         Some (q, dv, None :: m')
+      | S i => ''(q, dv, mf) ← denv_inhale_full_aux i m'; Some (q, dv, dio :: mf)
       end
     end.
+  Definition denv_inhale_full (i : nat) (m : denv) : option (dval * denv) :=
+    ''(q,dv,m') ← denv_inhale_full_aux i m;
+    guard (q = 1)%Qp;
+    Some (dv,m').
 
   Definition denv_unlock (m: denv) : denv :=
-    map (fun dio => di ← dio; Some (DenvItem ULvl (denv_frac di) (denv_dval di))) m.
-
+    map (λ dio, ''(DenvItem _ q dv) ← dio; Some (DenvItem ULvl q dv)) m.
+
+  Definition denv_inhale_frac_2 (i : nat) (m1 m2 : denv) : option (denv * denv * frac * dval) :=
+    match denv_inhale_frac i m1 with
+    | Some (q, dv, m1') => Some (m1', m2, q, dv)
+    | None =>
+       match denv_inhale_frac i m2 with
+       | Some (q, dv, m2') => Some (m1, m2', q, dv)
+       | None => None
+       end
+    end.
 
-  Definition denv_inhale_frac_2 (m1 m2: denv) i : option (denv * denv * (frac * dval)) :=
-    match denv_inhale_frac i m1, denv_inhale_frac i m2 with
-    | None, Some (q, dv, m2') => Some (m1, m2', (q, dv))
-    | Some (q, dv, m1'), None => Some (m1', m2, (q, dv))
-    | Some (q1, dv, m1'), Some (q2, _, m2') => Some (m1', m2', (Qp_plus q1 q2, dv))
+  Definition denv_inhale_full_2 (i : nat) (m1 m2: denv) : option (denv * denv * dval) :=
+    match denv_inhale_full_aux i m1, denv_inhale_full_aux i m2 with
+    | None, Some (q, dv, m2') => guard (q = 1)%Qp; Some (m1, m2', dv)
+    | Some (q, dv, m1'), None => guard (q = 1)%Qp; Some (m1', m2, dv)
+    | Some (q1, dv, m1'), Some (q2, _, m2') => guard (q1 + q2 = 1)%Qp; Some (m1', m2', dv)
     | _, _ => None
     end.
-
-
 End denv.
 
 Section denv_spec.
-
  Context `{amonadG Σ}.
 
   Notation "l ↦( x , q ) v" :=
-    (mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l  ↦( x , q )  v").
-
-   Definition denv_item_interp (L: locs) dl (p: denv_item) : iProp Σ :=
-     dloc_interp L dl ↦(denv_level p, denv_frac p) (dval_interp L (denv_dval p)).
-
-
-   Definition denv_interp (L: locs) (m : denv) : iProp Σ :=
-   ([∗ list] l ↦ po ∈ m,
-     match po with
-     | Some p => denv_item_interp L (dLoc l) p
-     | None => True
-     end)%I.
+    (mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l  ↦( x , q )  v") : bi_scope.
 
-End denv_spec.
\ No newline at end of file
+   Definition denv_interp (L : locs) (m : denv) : iProp Σ :=
+     ([∗ list] i ↦ dio ∈ m,
+         from_option (λ '(DenvItem lv q dv),
+           dloc_interp L (dLoc i) ↦(lv, q) dval_interp L dv) True dio)%I.
+End denv_spec.

theories/vcgen/splitenv.v

@@ -8,6 +8,15 @@ From iris.algebra Require Import frac.
 Section splitenv.
   Context `{amonadG Σ}.
 
+(* TODO: use
+  Record env_item := DenvItem {
+    denv_level : level;
+    denv_frac  : frac;
+    denv_dval  : val
+  }.
+  Definition env := list (option env_item).
+*)
+
   Notation "l ↦( x , q ) v" :=
      (mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l  ↦( x , q )  v").