Commit 231c868e authored by Robbert Krebbers's avatar Robbert Krebbers

Use W.expr in reification.

parent bdb99e79
......@@ -9,7 +9,7 @@ Inductive dloc :=
| dLoc : nat nat dloc (* index * offset *)
| dLocUnknown : cloc dloc.
Global Instance dloc_decision : EqDecision dloc.
Global Instance dloc_eq_dec : EqDecision dloc.
Proof. solve_decision. Defined.
(* This data type is kind of redundant, as long as we don't have symbolic
......@@ -20,7 +20,7 @@ Inductive dbase_lit : Type :=
| dLitUnit : dbase_lit
| dLitUnknown : base_lit dbase_lit.
Global Instance dlit_decision : EqDecision dbase_lit.
Global Instance dbase_lit_eq_dec : EqDecision dbase_lit.
Proof. solve_decision. Defined.
Inductive dval : Type :=
......@@ -29,7 +29,7 @@ Inductive dval : Type :=
| dLocV : dloc dval
| dValUnknown : val dval.
Global Instance dval_EqDecision : EqDecision dval.
Global Instance dval_eq_dec : EqDecision dval.
Proof. solve_decision. Defined.
Definition dloc_interp (E : known_locs) (dl : dloc) : cloc :=
......@@ -184,7 +184,7 @@ Inductive dexpr : Type :=
| dEPair : dexpr dexpr dexpr
| dEFst : dexpr dexpr
| dESnd : dexpr dexpr
| dEUnknown (e : expr) (*`{!Closed [] e}*) : dexpr.
| dEUnknown (e : W.expr) : dexpr.
Fixpoint dexpr_interp (E: known_locs) (de: dexpr) : expr :=
match de with
......@@ -193,20 +193,9 @@ Fixpoint dexpr_interp (E: known_locs) (de: dexpr) : expr :=
| dEPair de1 de2 => (dexpr_interp E de1, dexpr_interp E de2)
| dEFst de => Fst (dexpr_interp E de)
| dESnd de => Snd (dexpr_interp E de)
| dEUnknown e => e
| dEUnknown e => W.to_expr e
end.
Fixpoint dexpr_free_vars (E: known_locs) (de: dexpr) : list string :=
match de with
| dEVal dv => []
| dEVar x => [x]
| dEPair de1 de2 => dexpr_free_vars E de1 ++ dexpr_free_vars E de2
| dEFst de => dexpr_free_vars E de
| dESnd de => dexpr_free_vars E de
| dEUnknown e => [] (*should we search for free vars here ?*)
end.
(** DCexpr *)
Inductive dcexpr : Type :=
| dCRet : dexpr dcexpr
......@@ -220,7 +209,7 @@ Inductive dcexpr : Type :=
| dCSeq : dcexpr dcexpr dcexpr
| dCPar : dcexpr dcexpr dcexpr
| dCInvoke (f: val) (de: dcexpr)
| dCUnknown (e : expr) (* `{!Closed [] e} *).
| dCUnknown (e : W.expr).
Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
match de with
......@@ -236,11 +225,10 @@ Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
| dCSeq de1 de2 => dcexpr_interp E de1 ; dcexpr_interp E de2
| dCPar de1 de2 => dcexpr_interp E de1 ||| dcexpr_interp E de2
| dCInvoke fv de => call (fv, dcexpr_interp E de)
| dCUnknown e1 => e1
| dCUnknown e1 => W.to_expr e1
end.
(** Well-foundness of dcexpr w.r.t. known_locs *)
(** Well-formedness of dcexpr w.r.t. known_locs *)
Fixpoint dloc_wf (E: known_locs) (dl : dloc) : bool :=
match dl with
| dLoc i _ => bool_decide (is_Some (E !! i))
......@@ -260,7 +248,7 @@ Fixpoint dexpr_wf (X: list string) (E: known_locs) (de: dexpr) : bool :=
| dEVar x => bool_decide (x X)
| dEFst de | dESnd de => dexpr_wf X E de
| dEPair de1 de2 => dexpr_wf X E de1 && dexpr_wf X E de2
| dEUnknown e => bool_decide (Closed X e)
| dEUnknown e => W.is_closed X e
end.
Fixpoint dcexpr_wf (X: list string) (E: known_locs) (de: dcexpr) : bool :=
......@@ -271,7 +259,7 @@ Fixpoint dcexpr_wf (X: list string) (E: known_locs) (de: dcexpr) : bool :=
| dCAlloc de1 de2 | dCStore de1 de2 | dCBinOp _ de1 de2
| dCPreBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 =>
dcexpr_wf X E de1 && dcexpr_wf X E de2
| dCUnknown e => bool_decide (Closed X e)
| dCUnknown e => W.is_closed X e
end.
......@@ -322,7 +310,7 @@ Proof.
simpl. unfold dptr_plus_eval. repeat case_match; naive_solver.
Qed.
(** / Well-foundness of dcexpr w.r.t. known_locs *)
(** / Well-formedness of dcexpr w.r.t. known_locs *)
Lemma dloc_interp_mono (E E': known_locs) (i j: nat) :
dloc_wf E (dLoc i j) E `prefix_of` E'
......@@ -474,109 +462,113 @@ Global Instance into_dval_default E v : IntoDVal E v (dValUnknown v) | 1000.
Proof. done. Qed.
(** ** IntoDExpr *)
Class IntoDExpr (E: known_locs) (e: expr) (de: dexpr) :=
{ into_dexpr : e = dexpr_interp E de;
into_dexpr_wf : dexpr_wf (dexpr_free_vars E de) E de }.
Class IntoDExpr (E: known_locs) (e: expr) (de: dexpr) :=
into_dexpr : e = dexpr_interp E de.
Global Instance into_dexpr_val E e dv :
ExprIntoDVal E e dv
IntoDExpr E e (dEVal dv) | 5.
Proof. intros [-> ?]; split; auto. Qed.
Proof. by intros [-> ?]. Qed.
Global Instance into_dexpr_var E x :
IntoDExpr E (Var x) (dEVar x) | 5.
Proof. split; auto. simpl. case_bool_decide; first done. set_solver. Qed.
Proof. done. Qed.
Global Instance into_dexpr_pair E e1 e2 de1 de2 :
IntoDExpr E e1 de1 IntoDExpr E e2 de2
IntoDExpr E (Pair e1 e2) (dEPair de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto.
Admitted.
Proof. by rewrite /IntoDExpr=> -> ->. Qed.
Global Instance into_dexpr_fst E e de:
IntoDExpr E e de
IntoDExpr E (Fst e) (dEFst de).
Proof. intros [-> ?]; split; auto. Qed.
Proof. by rewrite /IntoDExpr=> ->. Qed.
Global Instance into_dexpr_snd E e de:
IntoDExpr E e de
IntoDExpr E (Snd e) (dESnd de).
Proof. intros [-> ?]; split; auto. Qed.
Proof. by rewrite /IntoDExpr=> ->. Qed.
Lemma into_dexpr_unknown {E e} de :
e = W.to_expr de
IntoDExpr E e (dEUnknown de).
Proof. by intros ->. Qed.
Global Instance into_dexpr_unknown E e (* `{Closed [] e} *):
IntoDExpr E e (dEUnknown e) | 100.
Proof. Admitted.
Hint Extern 100 (IntoDExpr _ ?e _) =>
let e' := W.of_expr e in
apply (into_dexpr_unknown e'); reflexivity : typeclass_instances.
(** ** IntoDCExpr *)
Class IntoDCExpr (E: known_locs) (e: expr) (de: dcexpr) :=
{ into_dcexpr : e = dcexpr_interp E de;
into_dcexpr_wf : dcexpr_wf [] (*should be fixed*) E de }.
into_dcexpr : e = dcexpr_interp E de.
Global Instance into_dcexpr_ret E e de:
IntoDExpr E e de
IntoDCExpr E (a_ret e) (dCRet de).
Proof. intros [-> ?]; split; auto. Admitted.
Proof. by rewrite /IntoDExpr=> ->. Qed.
Global Instance into_dcexpr_bind E x e1 e2 de1 de2:
IntoDCExpr E e1 de1
IntoDCExpr E e2 de2
IntoDCExpr E (BNamed x ←ᶜ e1 ;; e2) (dCBind x de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Admitted.
Proof. by rewrite /IntoDCExpr=> -> ->. Qed.
Global Instance into_dcexpr_alloc E e1 e2 de1 de2 :
IntoDCExpr E e1 de1 IntoDCExpr E e2 de2
IntoDCExpr E (a_alloc e1 e2) (dCAlloc de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Admitted.
Proof. by rewrite /IntoDCExpr=> -> ->. Qed.
Global Instance into_dcexpr_load E e de:
IntoDCExpr E e de
IntoDCExpr E (a_load e) (dCLoad de).
Proof. intros [-> ?]; split; auto. Qed.
Proof. by rewrite /IntoDCExpr=> ->. Qed.
Global Instance into_dcexpr_store E e1 e2 de1 de2:
IntoDCExpr E e1 de1
IntoDCExpr E e2 de2
IntoDCExpr E (a_store e1 e2) (dCStore de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Proof. by rewrite /IntoDCExpr=> -> ->. Qed.
Global Instance into_dcexpr_binop E e1 e2 op de1 de2:
IntoDCExpr E e1 de1
IntoDCExpr E e2 de2
IntoDCExpr E (a_bin_op op e1 e2) (dCBinOp op de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Proof. by rewrite /IntoDCExpr=> -> ->. Qed.
Global Instance into_dcexpr_prebinop E e1 e2 op de1 de2:
IntoDCExpr E e1 de1
IntoDCExpr E e2 de2
IntoDCExpr E (a_pre_bin_op op e1 e2) (dCPreBinOp op de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Proof. by rewrite /IntoDCExpr=> -> ->. Qed.
Global Instance into_dcexpr_unop E e op de:
IntoDCExpr E e de
IntoDCExpr E (a_un_op op e) (dCUnOp op de).
Proof. intros [-> ?]; split; auto. Qed.
Proof. by rewrite /IntoDCExpr=> ->. Qed.
Global Instance into_dcexpr_sequence E e1 e2 de1 de2:
IntoDCExpr E e1 de1
IntoDCExpr E e2 de2
IntoDCExpr E (e1 ; e2) (dCSeq de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Proof. by rewrite /IntoDCExpr=> -> ->. Qed.
Global Instance into_dcexpr_par E e1 e2 de1 de2:
IntoDCExpr E e1 de1
IntoDCExpr E e2 de2
IntoDCExpr E (e1 ||| e2) (dCPar de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Proof. by rewrite /IntoDCExpr=> -> ->. Qed.
Global Instance into_dcexpr_invoke e1 E ef f `{!IntoVal ef f} de1 :
Global Instance into_dcexpr_invoke e1 E ef f de1 :
IntoVal ef f ->
IntoDCExpr E e1 de1
IntoDCExpr E (call (ef, e1)) (dCInvoke f de1).
Proof.
intros HC. unfold IntoVal in *. simplify_eq /=.
split; simpl; auto; f_equal; apply HC.
Qed.
Proof. by rewrite /IntoVal /IntoDCExpr=> <- ->. Qed.
Lemma into_dcexpr_unknown {E e} de :
e = W.to_expr de
IntoDCExpr E e (dCUnknown de).
Proof. by intros ->. Qed.
Global Instance into_dcexpr_unknown E e (* `{Closed [] e} *):
IntoDCExpr E e (dCUnknown e) | 100.
Proof. Admitted.
Hint Extern 100 (IntoDCExpr _ ?e _) =>
let e' := W.of_expr e in
apply (into_dcexpr_unknown e'); reflexivity : typeclass_instances.
......@@ -351,10 +351,8 @@ End vcg.
Section vcg_spec.
Context `{amonadG Σ}.
Arguments subst _ _ !_ /.
Lemma de_subst_subst_comm E x de dv :
(dexpr_interp E (de_subst E x dv de)) =
(subst x (dval_interp E dv) (dexpr_interp E de)).
......@@ -380,7 +378,7 @@ Section vcg_spec.
Arguments subst : simpl never.
Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
mapsto_wand_list_aux E m Φ k -
([ list] ndio m, from_option
(λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
......@@ -520,12 +518,12 @@ Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
Lemma vcg_sp_correct' E de ms ms' mNew dv R n :
vcg_sp E ms de n = Some (ms', mNew, dv)
(* dcexpr_wf X E de → (*where free_vars de ⊆ X*) *)
dcexpr_wf [] E de (*where free_vars de ⊆ X*) *)
(denv_stack_interp ms ms' E
(awp (dcexpr_interp E de) R
(λ v, v = dval_interp E dv denv_interp E mNew)))%I.
Proof.
revert de ms ms' mNew dv. induction n.
revert de ms ms' mNew dv. induction n as [|n IH].
(* Base Case *)
- iIntros (de ms ms' mNew dv Hsp); simplify_eq/=.
destruct de; simplify_option_eq.
......
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