Commit 9d31584e authored by Léon Gondelman's avatar Léon Gondelman
Browse files

rename dCVal -> dCRet

parent 4b231c02
......@@ -215,14 +215,14 @@ From iris_c.c_translation Require Import monad translation proofmode.
(* Add "Unknown" constructor *)
Inductive dcexpr : Type :=
| dCVal : dval dcexpr
| dCRet : dval dcexpr
| dCLoad : dcexpr dcexpr
| dCStore : dcexpr dcexpr dcexpr
| dCBinOp : bin_op dcexpr dcexpr dcexpr.
Fixpoint dcexpr_interp (E: list loc) (d: dcexpr) : expr :=
match d with
| dCVal dv => a_ret (dval_interp E dv)
| dCRet dv => a_ret (dval_interp E dv)
| dCLoad d1 => a_load (dcexpr_interp E d1)
| dCStore d1 d2 => a_store (dcexpr_interp E d1) (dcexpr_interp E d2)
| dCBinOp op d1 d2 => a_bin_op op (dcexpr_interp E d1) (dcexpr_interp E d2)
......@@ -231,9 +231,9 @@ From iris_c.c_translation Require Import monad translation proofmode.
Class IntoDCexpr (E: list loc) (e: expr) (de: dcexpr) :=
into_dcexpr : e = dcexpr_interp E de.
Global Instance into_dcexpr_val E v dv:
Global Instance into_dcexpr_ret E v dv:
IntoDVal E v dv
IntoDCexpr E (a_ret v) (dCVal dv).
IntoDCexpr E (a_ret v) (dCRet dv).
Proof. by rewrite /IntoDCexpr=> ->. Qed.
Global Instance into_dcexpr_load E e de:
......
Supports Markdown
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