Merge branch 'vcgen' of gitlab.science.ru.nl:lgg/iris-c-monad into vcgen

_CoqProject

@@ -11,6 +11,7 @@ theories/c_translation/translation.v
 theories/c_translation/derived.v
 theories/vcgen/dcexpr.v
 theories/vcgen/env.v
+theories/vcgen/denv.v
 theories/vcgen/splitenv.v
 theories/vcgen/vcgen.v
 # theories/vcgen/test.v

theories/vcgen/denv.v

+From iris.proofmode Require Import environments coq_tactics.
+Import env_notations.
+From iris_c.vcgen Require Import dcexpr.
+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 {
+    denv_level : level;
+    denv_frac  : frac;
+    denv_dval  : dval
+  }.
+
+  Definition denv := list (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 :=
+    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 :=
+    match i with
+    | O => [Some (DenvItem x q dv)]
+    | S i => None :: denv_exhale_aux i x 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
+    | 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
+      | S i => dio :: denv_exhale i x q dv m'
+      end
+    end.
+
+  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')
+      | 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) :=
+    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)
+      end
+    end.
+
+  Definition denv_unlock (m: denv) : denv :=
+    map (fun dio => di ← dio; Some (DenvItem ULvl (denv_frac di) (denv_dval di))) m.
+
+
+  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))
+    | _, _ => 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.
+
+End denv_spec.
\ No newline at end of file