Commit 621ef791 authored by Robbert Krebbers's avatar Robbert Krebbers

Typeclass for evaluation context based language.

parent 5c232f1e
...@@ -414,15 +414,15 @@ Section Language. ...@@ -414,15 +414,15 @@ Section Language.
- clear Hatomic. eapply reducible_not_value. do 3 eexists; eassumption. - clear Hatomic. eapply reducible_not_value. do 3 eexists; eassumption.
Qed. Qed.
(** We can have bind with arbitrary evaluation contexts **) Global Instance heap_lang_fill : Fill ectx expr := fill.
Lemma fill_is_ctx K: is_ctx (fill K). Global Instance heap_lang_ctx : CtxLanguage heap_lang ectx.
Proof. Proof.
split. split.
- intros ? Hnval. by eapply fill_not_value. - intros K ? Hnval. by eapply fill_not_value.
- intros ? ? ? ? ? (K' & e1' & e2' & Heq1 & Heq2 & Hstep). - intros K ? ? ? ? ? (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
exists (comp_ctx K K'), e1', e2'. rewrite -!fill_comp Heq1 Heq2. exists (comp_ctx K K'), e1', e2'. rewrite -!fill_comp Heq1 Heq2.
split; last split; reflexivity || assumption. split; last split; reflexivity || assumption.
- intros ? ? ? ? ? Hnval (K'' & e1'' & e2'' & Heq1 & Heq2 & Hstep). - intros K ? ? ? ? ? Hnval (K'' & e1'' & e2'' & Heq1 & Heq2 & Hstep).
destruct (step_by_value (σ:=σ1) Heq1) as [K' HeqK]. destruct (step_by_value (σ:=σ1) Heq1) as [K' HeqK].
+ do 3 eexists. eassumption. + do 3 eexists. eassumption.
+ assumption. + assumption.
......
...@@ -10,7 +10,7 @@ Implicit Types Q : val heap_lang → iProp heap_lang Σ. ...@@ -10,7 +10,7 @@ Implicit Types Q : val heap_lang → iProp heap_lang Σ.
(** Bind. *) (** Bind. *)
Lemma wp_bind {E e} K Q : Lemma wp_bind {E e} K Q :
wp E e (λ v, wp E (fill K (v2e v)) Q) wp E (fill K e) Q. wp E e (λ v, wp E (fill K (v2e v)) Q) wp E (fill K e) Q.
Proof. apply (wp_bind (K:=fill K)), fill_is_ctx. Qed. Proof. apply wp_bind. Qed.
(** Base axioms for core primitives of the language: Stateful reductions. *) (** Base axioms for core primitives of the language: Stateful reductions. *)
......
...@@ -57,9 +57,9 @@ Proof. ...@@ -57,9 +57,9 @@ Proof.
rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v. rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v.
rewrite (forall_elim v) pvs_impl_r -(pvs_intro E1) pvs_trans; solve_elem_of. rewrite (forall_elim v) pvs_impl_r -(pvs_intro E1) pvs_trans; solve_elem_of.
Qed. Qed.
Lemma ht_bind `(HK : is_ctx K) E P Q Q' e : Lemma ht_bind `{CtxLanguage Λ C} K E P Q Q' e :
({{ P }} e @ E {{ Q }} v, {{ Q v }} K (of_val v) @ E {{ Q' }}) ({{ P }} e @ E {{ Q }} v, {{ Q v }} fill K (of_val v) @ E {{ Q' }})
{{ P }} K e @ E {{ Q' }}. {{ P }} fill K e @ E {{ Q' }}.
Proof. Proof.
intros; apply (always_intro' _ _), impl_intro_l. intros; apply (always_intro' _ _), impl_intro_l.
rewrite (associative _ P) {1}/ht always_elim impl_elim_r. rewrite (associative _ P) {1}/ht always_elim impl_elim_r.
......
...@@ -52,14 +52,19 @@ Section language. ...@@ -52,14 +52,19 @@ Section language.
Qed. Qed.
Global Instance: Injective (=) (=) (@of_val Λ). Global Instance: Injective (=) (=) (@of_val Λ).
Proof. by intros v v' Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed. Proof. by intros v v' Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
Record is_ctx (K : expr Λ expr Λ) := IsCtx {
is_ctx_value e : to_val e = None to_val (K e) = None;
is_ctx_step_preserved e1 σ1 e2 σ2 ef :
prim_step e1 σ1 e2 σ2 ef prim_step (K e1) σ1 (K e2) σ2 ef;
is_ctx_step e1' σ1 e2 σ2 ef :
to_val e1' = None prim_step (K e1') σ1 e2 σ2 ef
e2', e2 = K e2' prim_step e1' σ1 e2' σ2 ef
}.
End language. End language.
Class Fill C E := fill : C E E.
Instance: Params (@fill) 3.
Arguments fill {_ _ _} !_ _ / : simpl nomatch.
Class CtxLanguage (Λ : language) (C : Type) `{Fill C (expr Λ)} := {
is_ctx_value K e :
to_val e = None to_val (fill K e) = None;
is_ctx_step_preserved K e1 σ1 e2 σ2 ef :
prim_step e1 σ1 e2 σ2 ef
prim_step (fill K e1) σ1 (fill K e2) σ2 ef;
is_ctx_step K e1' σ1 e2 σ2 ef :
to_val e1' = None prim_step (fill K e1') σ1 e2 σ2 ef
e2', e2 = fill K e2' prim_step e1' σ1 e2' σ2 ef
}.
...@@ -161,17 +161,17 @@ Proof. ...@@ -161,17 +161,17 @@ Proof.
* apply wp_frame_r; [auto|exists r2, rR; split_ands; auto]. * apply wp_frame_r; [auto|exists r2, rR; split_ands; auto].
eapply uPred_weaken with rR n; eauto. eapply uPred_weaken with rR n; eauto.
Qed. Qed.
Lemma wp_bind `(HK : is_ctx K) E e Q : Lemma wp_bind `{CtxLanguage Λ C} E K e Q :
wp E e (λ v, wp E (K (of_val v)) Q) wp E (K e) Q. wp E e (λ v, wp E (fill K (of_val v)) Q) wp E (fill K e) Q.
Proof. Proof.
intros r n; revert e r; induction n as [n IH] using lt_wf_ind; intros e r ?. intros r n; revert e r; induction n as [n IH] using lt_wf_ind; intros e r ?.
destruct 1 as [|n r e ? Hgo]; [|constructor]; auto using is_ctx_value. destruct 1 as [|n r e ? Hgo]; [|constructor]; auto using is_ctx_value.
intros rf k Ef σ1 ???; destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto. intros rf k Ef σ1 ???; destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
split. split.
{ destruct Hsafe as (e2&σ2&ef&?). { destruct Hsafe as (e2&σ2&ef&?).
by exists (K e2), σ2, ef; apply is_ctx_step_preserved. } by exists (fill K e2), σ2, ef; apply is_ctx_step_preserved. }
intros e2 σ2 ef ?. intros e2 σ2 ef ?.
destruct (is_ctx_step _ HK e σ1 e2 σ2 ef) as (e2'&->&?); auto. destruct (is_ctx_step K e σ1 e2 σ2 ef) as (e2'&->&?); auto.
destruct (Hstep e2' σ2 ef) as (r2&r2'&?&?&?); auto. destruct (Hstep e2' σ2 ef) as (r2&r2'&?&?&?); auto.
exists r2, r2'; split_ands; try eapply IH; eauto. exists r2, r2'; split_ands; try eapply IH; eauto.
Qed. 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