Commit 4aeb0a86 authored by Ralf Jung's avatar Ralf Jung
Browse files

iris/language: do not tie evaluation contexts to have a syntactical representation

parent 9b141597
...@@ -135,8 +135,8 @@ Definition ectx_item_fill (Ki : ectx_item) (e : expr) : expr := ...@@ -135,8 +135,8 @@ Definition ectx_item_fill (Ki : ectx_item) (e : expr) : expr :=
| CasRCtx v0 v1 => Cas (of_val v0) (of_val v1) e | CasRCtx v0 v1 => Cas (of_val v0) (of_val v1) e
end. end.
Instance ectx_fill : Fill ectx expr := Fixpoint fill K e :=
fix go K e := let _ : Fill _ _ := @go in (* FIXME RJ: This really is fold_left, but if I use that all automation breaks. *)
match K with [] => e | Ki :: K => ectx_item_fill Ki (fill K e) end. match K with [] => e | Ki :: K => ectx_item_fill Ki (fill K e) end.
(** The stepping relation *) (** The stepping relation *)
...@@ -305,16 +305,18 @@ Program Canonical Structure heap_lang : language := {| ...@@ -305,16 +305,18 @@ Program Canonical Structure heap_lang : language := {|
of_val := heap_lang.of_val; to_val := heap_lang.to_val; of_val := heap_lang.of_val; to_val := heap_lang.to_val;
atomic := heap_lang.atomic; prim_step := heap_lang.prim_step; atomic := heap_lang.atomic; prim_step := heap_lang.prim_step;
|}. |}.
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val, Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
heap_lang.values_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step. heap_lang.values_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step.
Global Instance heap_lang_ctx : CtxLanguage heap_lang heap_lang.ectx. Import heap_lang.
Global Instance heap_lang_ctx K :
LanguageCtx heap_lang (heap_lang.fill K).
Proof. Proof.
split. split.
* eauto using heap_lang.fill_not_val. * eauto using heap_lang.fill_not_val.
* intros K ????? [K' e1' e2' Heq1 Heq2 Hstep]. * intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
by exists (K ++ K') e1' e2'; rewrite ?heap_lang.fill_app ?Heq1 ?Heq2. by exists (K ++ K') e1' e2'; rewrite ?heap_lang.fill_app ?Heq1 ?Heq2.
* intros K e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep]. * intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
destruct (heap_lang.step_by_val destruct (heap_lang.step_by_val
K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto. K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto.
rewrite heap_lang.fill_app in Heq1; apply (injective _) in Heq1. rewrite heap_lang.fill_app in Heq1; apply (injective _) in Heq1.
......
...@@ -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 `{CtxLanguage Λ C} K E P Q Q' e : Lemma ht_bind `{LanguageCtx Λ K} E P Q Q' e :
({{ P }} e @ E {{ Q }} v, {{ Q v }} fill K (of_val v) @ E {{ Q' }}) ({{ P }} e @ E {{ Q }} v, {{ Q v }} K (of_val v) @ E {{ Q' }})
{{ P }} fill K e @ E {{ Q' }}. {{ P }} 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,17 +52,13 @@ Section language. ...@@ -52,17 +52,13 @@ Section language.
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.
End language. End language.
Class Fill C E := fill : C E E. Class LanguageCtx (Λ : language) (K : expr Λ expr Λ) := {
Instance: Params (@fill) 3. fill_not_val e :
Arguments fill {_ _ _} !_ _ / : simpl nomatch. to_val e = None to_val (K e) = None;
fill_step e1 σ1 e2 σ2 ef :
Class CtxLanguage (Λ : language) (C : Type) `{Fill C (expr Λ)} := {
fill_not_val K e :
to_val e = None to_val (fill K e) = None;
fill_step K e1 σ1 e2 σ2 ef :
prim_step e1 σ1 e2 σ2 ef prim_step e1 σ1 e2 σ2 ef
prim_step (fill K e1) σ1 (fill K e2) σ2 ef; prim_step (K e1) σ1 (K e2) σ2 ef;
fill_step_inv K e1' σ1 e2 σ2 ef : fill_step_inv e1' σ1 e2 σ2 ef :
to_val e1' = None prim_step (fill K e1') σ1 e2 σ2 ef to_val e1' = None prim_step (K e1') σ1 e2 σ2 ef
e2', e2 = fill K e2' prim_step e1' σ1 e2' σ2 ef e2', e2 = 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 `{CtxLanguage Λ C} E K e Q : Lemma wp_bind `{LanguageCtx Λ K} E e Q :
wp E e (λ v, wp E (fill K (of_val v)) Q) wp E (fill K e) Q. wp E e (λ v, wp E (K (of_val v)) Q) wp E (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 fill_not_val. destruct 1 as [|n r e ? Hgo]; [|constructor]; auto using fill_not_val.
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 (fill K e2), σ2, ef; apply fill_step. } by exists (K e2), σ2, ef; apply fill_step. }
intros e2 σ2 ef ?. intros e2 σ2 ef ?.
destruct (fill_step_inv K e σ1 e2 σ2 ef) as (e2'&->&?); auto. destruct (fill_step_inv 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