Commit 6df33dac authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

More consistent naming for `pure_exec`.

parent 5e472be6
...@@ -82,49 +82,49 @@ Qed. ...@@ -82,49 +82,49 @@ Qed.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto. Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step. Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pureexec := Local Ltac solve_pure_exec :=
repeat lazymatch goal with repeat lazymatch goal with
| H: IntoVal ?e _ |- _ => rewrite -(of_to_val e _ into_val); clear H | H: IntoVal ?e _ |- _ => rewrite -(of_to_val e _ into_val); clear H
| H: AsRec _ _ _ _ |- _ => rewrite H; clear H | H: AsRec _ _ _ _ |- _ => rewrite H; clear H
end; end;
apply det_head_step_pureexec; [ solve_exec_safe | solve_exec_puredet ]. apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
Global Instance pure_rec f x (erec e1 e2 : expr) (v2 : val) Global Instance pure_rec f x (erec e1 e2 : expr) (v2 : val)
`{!IntoVal e2 v2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} : `{!IntoVal e2 v2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)). PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
Proof. solve_pureexec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_unop op e v v' `{!IntoVal e v} : Global Instance pure_unop op e v v' `{!IntoVal e v} :
PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v'). PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
Proof. solve_pureexec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} : Global Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v'). PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v').
Proof. solve_pureexec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_if_true e1 e2 : Global Instance pure_if_true e1 e2 :
PureExec True (If (Lit (LitBool true)) e1 e2) e1. PureExec True (If (Lit (LitBool true)) e1 e2) e1.
Proof. solve_pureexec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_if_false e1 e2 : Global Instance pure_if_false e1 e2 :
PureExec True (If (Lit (LitBool false)) e1 e2) e2. PureExec True (If (Lit (LitBool false)) e1 e2) e2.
Proof. solve_pureexec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_fst e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} : Global Instance pure_fst e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} :
PureExec True (Fst (Pair e1 e2)) e1. PureExec True (Fst (Pair e1 e2)) e1.
Proof. solve_pureexec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_snd e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} : Global Instance pure_snd e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} :
PureExec True (Snd (Pair e1 e2)) e2. PureExec True (Snd (Pair e1 e2)) e2.
Proof. solve_pureexec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} : Global Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
PureExec True (Case (InjL e0) e1 e2) (App e1 e0). PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
Proof. solve_pureexec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} : Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
PureExec True (Case (InjR e0) e1 e2) (App e2 e0). PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
Proof. solve_pureexec. Qed. Proof. solve_pure_exec. Qed.
(** Heap *) (** Heap *)
Lemma wp_alloc E e v : Lemma wp_alloc E e v :
......
...@@ -151,7 +151,7 @@ Section ectx_language. ...@@ -151,7 +151,7 @@ Section ectx_language.
econstructor; eauto. econstructor; eauto.
Qed. Qed.
Lemma det_head_step_pureexec (P : Prop) e1 e2 : Lemma det_head_step_pure_exec (P : Prop) e1 e2 :
( σ, P head_reducible e1 σ) ( σ, P head_reducible e1 σ)
( σ1 e2' σ2 efs, ( σ1 e2' σ2 efs,
P head_step e1 σ1 e2' σ2 efs σ1 = σ2 e2=e2' efs = []) P head_step e1 σ1 e2' σ2 efs σ1 = σ2 e2=e2' efs = [])
......
...@@ -101,7 +101,7 @@ Section language. ...@@ -101,7 +101,7 @@ Section language.
P prim_step e1 σ1 e2' σ2 efs σ1 = σ2 e2 = e2' efs = []; P prim_step e1 σ1 e2' σ2 efs σ1 = σ2 e2 = e2' efs = [];
}. }.
Lemma hoist_pred_pureexec (P : Prop) (e1 e2 : expr Λ) : Lemma hoist_pred_pure_exec (P : Prop) (e1 e2 : expr Λ) :
(P PureExec True e1 e2) (P PureExec True e1 e2)
PureExec P e1 e2. PureExec P e1 e2.
Proof. intros HPE. split; intros; eapply HPE; eauto. Qed. Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
......
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