Commit 0979a8f2 authored by Léon Gondelman's avatar Léon Gondelman

denv

parent 72a26f71
......@@ -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
......
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
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment