Commit bdb99e79 authored by Léon Gondelman 's avatar Léon Gondelman

wip on env of vars

parent d6c74d53
......@@ -196,6 +196,17 @@ Fixpoint dexpr_interp (E: known_locs) (de: dexpr) : expr :=
| dEUnknown e => 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
......@@ -243,26 +254,27 @@ Fixpoint dval_wf (E: known_locs) (dv : dval) : bool :=
| _ => true
end.
Fixpoint dexpr_wf (E: known_locs) (de: dexpr) : bool :=
Fixpoint dexpr_wf (X: list string) (E: known_locs) (de: dexpr) : bool :=
match de with
| dEVal dv => dval_wf E dv
| dEVar x => true
| dEFst de | dESnd de => dexpr_wf E de
| dEPair de1 de2 => dexpr_wf E de1 && dexpr_wf E de2
| dEUnknown _ => true
| 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)
end.
Fixpoint dcexpr_wf (E: known_locs) (de: dcexpr) : bool :=
Fixpoint dcexpr_wf (X: list string) (E: known_locs) (de: dcexpr) : bool :=
match de with
| dCRet de => dexpr_wf E de
| dCBind x de1 de2 => dcexpr_wf E de1 && dcexpr_wf E de2
| dCLoad de1 | dCUnOp _ de1 | dCInvoke _ de1 => dcexpr_wf E de1
| dCRet de => dexpr_wf X E de
| dCBind x de1 de2 => dcexpr_wf (x :: X) E de1 && dcexpr_wf X E de2
| dCLoad de1 | dCUnOp _ de1 | dCInvoke _ de1 => dcexpr_wf X E de1
| dCAlloc de1 de2 | dCStore de1 de2 | dCBinOp _ de1 de2
| dCPreBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 =>
dcexpr_wf E de1 && dcexpr_wf E de2
| dCUnknown _ => true
dcexpr_wf X E de1 && dcexpr_wf X E de2
| dCUnknown e => bool_decide (Closed X e)
end.
(*TODO: Fuse wf_mono and interp_mono into one lemma for dval and dcexpr *)
Lemma dval_wf_mono (E E': known_locs) (dv: dval) :
dval_wf E dv E `prefix_of` E' dval_wf E' dv.
......@@ -279,17 +291,20 @@ Proof.
* specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver.
Qed.
Lemma dexpr_wf_mono (E E': known_locs) (de: dexpr) :
dexpr_wf E de E `prefix_of` E' dexpr_wf E' de.
Lemma dexpr_wf_mono (X: list string) (E E': known_locs) (de: dexpr) :
dexpr_wf X E de E `prefix_of` E' dexpr_wf X E' de.
Proof. induction de; simplify_eq /=; [apply dval_wf_mono|..]; naive_solver. Qed.
Lemma dcexpr_wf_mono (E E': known_locs) (de: dcexpr) :
dcexpr_wf E de E `prefix_of` E' dcexpr_wf E' de.
Lemma dcexpr_wf_mono (X: list string) (E E': known_locs) (de: dcexpr) :
dcexpr_wf X E de E `prefix_of` E' dcexpr_wf X E' de.
Proof.
revert X.
induction de; intros X; simplify_eq /=; [try apply dexpr_wf_mono|..];
naive_solver.
Qed.
Lemma dun_op_eval_Some_wf E dv u dw:
dval_wf E dv dun_op_eval E u dv = Some dw dval_wf E dw.
Proof. destruct u, dv; simpl; repeat case_match; naive_solver. Qed.
......@@ -345,8 +360,9 @@ Proof.
* specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver.
Qed.
Lemma dexpr_interp_mono (E E': known_locs) (de: dexpr) :
dexpr_wf E de E `prefix_of` E' dexpr_interp E de = dexpr_interp E' de.
Lemma dexpr_interp_mono (X: list string) (E E': known_locs) (de: dexpr) :
dexpr_wf X E de E `prefix_of` E' dexpr_interp E de = dexpr_interp E' de.
Proof.
induction de; simplify_eq /=; intros H Hpre;
try (by rewrite IHde ) ||
......@@ -356,16 +372,17 @@ Proof.
by rewrite (dval_interp_mono E E').
Qed.
Lemma dcexpr_interp_mono (E E': known_locs) (de: dcexpr) :
dcexpr_wf E de E `prefix_of` E' dcexpr_interp E de = dcexpr_interp E' de.
Lemma dcexpr_interp_mono (X: list string) (E E': known_locs) (de: dcexpr) :
dcexpr_wf X E de E `prefix_of` E' dcexpr_interp E de = dcexpr_interp E' de.
Proof.
induction de; simplify_eq /=; intros H Hpre;
try (by rewrite IHde ) ||
(apply andb_prop_elim in H as [H1 H2];
rewrite IHde2; [rewrite IHde1; done | done | done ];
by rewrite (IHde1 H1 Hpre (dcexpr_interp E de1))) || eauto.
by rewrite (dexpr_interp_mono E E').
Qed.
by rewrite (dexpr_interp_mono X E E').
Admitted.
(*
Global Instance dexpr_closed E de : Closed [] (dexpr_interp E de).
......@@ -459,7 +476,7 @@ 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 E de }.
into_dexpr_wf : dexpr_wf (dexpr_free_vars E de) E de }.
Global Instance into_dexpr_val E e dv :
ExprIntoDVal E e dv
......@@ -468,12 +485,13 @@ Proof. intros [-> ?]; split; auto. Qed.
Global Instance into_dexpr_var E x :
IntoDExpr E (Var x) (dEVar x) | 5.
Proof. split; auto. Qed.
Proof. split; auto. simpl. case_bool_decide; first done. set_solver. 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. Qed.
Proof. intros [-> ?] [-> ?]; split; simpl; auto.
Admitted.
Global Instance into_dexpr_fst E e de:
IntoDExpr E e de
......@@ -487,29 +505,29 @@ Proof. intros [-> ?]; split; auto. Qed.
Global Instance into_dexpr_unknown E e (* `{Closed [] e} *):
IntoDExpr E e (dEUnknown e) | 100.
Proof. done. Qed.
Proof. Admitted.
(** ** IntoDCExpr *)
Class IntoDCExpr (E: known_locs) (e: expr) (de: dcexpr) :=
{ into_dcexpr : e = dcexpr_interp E de;
into_dcexpr_wf : dcexpr_wf E de }.
into_dcexpr_wf : dcexpr_wf [] (*should be fixed*) 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. Qed.
Proof. intros [-> ?]; split; auto. Admitted.
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. Qed.
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Admitted.
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. Qed.
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Admitted.
Global Instance into_dcexpr_load E e de:
IntoDCExpr E e de
......@@ -561,4 +579,4 @@ Qed.
Global Instance into_dcexpr_unknown E e (* `{Closed [] e} *):
IntoDCExpr E e (dCUnknown e) | 100.
Proof. done. Qed.
Proof. Admitted.
......@@ -502,7 +502,7 @@ Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
Lemma vcg_eval_dexpr_wf E de dv :
vcg_eval_dexpr de = Some dv
dexpr_wf E de dval_wf E dv.
dexpr_wf [] E de dval_wf E dv.
Proof.
generalize dependent dv. induction de; intros dv Hdv; simplify_eq/=; eauto.
- simplify_option_eq. naive_solver.
......@@ -517,8 +517,10 @@ Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
(* THIS IS UGLY AF ^ *) simpl in IHde.
destruct_and!. auto.
Qed.
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*) *)
(denv_stack_interp ms ms' E
(awp (dcexpr_interp E de) R
(λ v, v = dval_interp E dv denv_interp E mNew)))%I.
......
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