Commit 149ef27a authored by Léon Gondelman 's avatar Léon Gondelman

add support for substitution of variables in the heaplang expressions

parent 7f8cc205
......@@ -99,4 +99,4 @@ Ltac vcg_continue :=
| apply _ (* ListOfMapsto Γls (E_old ++ E_new) ps *)
| apply _ (* IntoDVal (E_old ++ E_new) v dv *)
| done (* ps is well-formed *)
| simpl ].
| simpl; simpl_subst ].
......@@ -56,36 +56,38 @@ Section vcg.
end.
(** substitution *)
Fixpoint de_subst (x: string) (dv : dval) (de: dexpr) : dexpr :=
Fixpoint de_subst
(E: known_locs) (x: string) (dv : dval) (de: dexpr) : dexpr :=
match de with
| dEVal _ => de
| dEVar y => if decide (x = y) then dEVal dv else de
| dEPair de1 de2 => dEPair (de_subst x dv de1) (de_subst x dv de2)
| dEFst de1 => dEFst (de_subst x dv de1)
| dESnd de1 => dESnd (de_subst x dv de1)
| dEUnknown _ => de
| dEPair de1 de2 => dEPair (de_subst E x dv de1) (de_subst E x dv de2)
| dEFst de1 => dEFst (de_subst E x dv de1)
| dESnd de1 => dESnd (de_subst E x dv de1)
| dEUnknown e => dEUnknown (subst x (dval_interp E dv) e)
end.
Fixpoint dce_subst (x: string) (dv : dval) (dce : dcexpr) : dcexpr :=
Fixpoint dce_subst (E: known_locs)
(x: string) (dv : dval) (dce : dcexpr) : dcexpr :=
match dce with
| dCRet de1 => dCRet (de_subst x dv de1)
| dCRet de1 => dCRet (de_subst E x dv de1)
| dCBind y de1 de2 =>
if decide (x = y)
then dCBind y (dce_subst x dv de1) de2
else dCBind y (dce_subst x dv de1) (dce_subst x dv de2)
| dCAlloc de1 de2 => dCAlloc (dce_subst x dv de1) (dce_subst x dv de2)
| dCLoad de1 => dCLoad (dce_subst x dv de1)
| dCStore de1 de2 => dCStore (dce_subst x dv de1) (dce_subst x dv de2)
then dCBind y (dce_subst E x dv de1) de2
else dCBind y (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCAlloc de1 de2 => dCAlloc (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCLoad de1 => dCLoad (dce_subst E x dv de1)
| dCStore de1 de2 => dCStore (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCBinOp op de1 de2 =>
dCBinOp op (dce_subst x dv de1) (dce_subst x dv de2)
dCBinOp op (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCPreBinOp op de1 de2 =>
dCPreBinOp op (dce_subst x dv de1) (dce_subst x dv de2)
| dCUnOp op de1 => dCUnOp op (dce_subst x dv de1)
| dCSeq de1 de2 => dCSeq (dce_subst x dv de1) (dce_subst x dv de2)
| dCPar de1 de2 => dCPar (dce_subst x dv de1) (dce_subst x dv de2)
| dCInvoke v de1 => dCInvoke v (dce_subst x dv de1)
| dCUnknown _ => dce
dCPreBinOp op (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCUnOp op de1 => dCUnOp op (dce_subst E x dv de1)
| dCSeq de1 de2 => dCSeq (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCPar de1 de2 => dCPar (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCInvoke v de1 => dCInvoke v (dce_subst E x dv de1)
| dCUnknown e => dCUnknown (subst x (dval_interp E dv) e)
end.
......@@ -99,7 +101,7 @@ Section vcg.
| dCBind x de1 de2, S p =>
''(ms1, mNew1, dv1) vcg_sp E ms de1 p;
''(ms2, mNew2, dv2)
vcg_sp E (mNew1 :: ms1) (dce_subst x dv1 de2) p;
vcg_sp E (mNew1 :: ms1) (dce_subst E x dv1 de2) p;
''(ms3, mNew3) popstack ms2;
Some (ms3, denv_merge mNew2 mNew3, dv2)
| dCLoad de1, S p =>
......@@ -256,12 +258,7 @@ Section vcg.
(cl C[LLvl] w - vcg_wp_continuation E Φ v))
end%I.
Definition vcg_wp_bind (E : known_locs) (dv: dval) (m : denv)
(Φ : known_locs denv dval iProp Σ) : iProp Σ :=
mapsto_wand_list E m (vcg_wp_continuation E Φ ((dval_interp E dv)))%I.
Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
(R : iProp Σ) (Φ : known_locs denv dval iProp Σ) (n: nat) {struct n}: iProp Σ :=
match de, n with
| dCRet de', _ =>
......@@ -271,7 +268,7 @@ Section vcg.
end
| dCBind x de1 de2, S p =>
vcg_wp E m de1 R (λ E m' dv1,
vcg_wp E m' (dce_subst x dv1 de2) R Φ p) p
vcg_wp E m' (dce_subst E x dv1 de2) R Φ p) p
| dCAlloc de1 de2, S p =>
match vcg_sp' E m de1 with
| Some (m', mNew, dv1) =>
......@@ -1130,4 +1127,3 @@ Arguments vcg_wp_store _ _ _ _ _ _ _ /.
Arguments vcg_wp_bin_op _ _ _ _ _ _ _ _ /.
Arguments vcg_wp_un_op _ _ _ _ _ _ _ /.
Arguments vcg_wp_pre_bin_op _ _ _ _ _ _ _ _ /.
Arguments vcg_wp_bind _ _ _ _ _ _ /.
\ 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