Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0

barrier/heap_lang.v

@@ -135,8 +135,10 @@ Definition ectx_item_fill (Ki : ectx_item) (e : expr) : expr :=
   | CasRCtx v0 v1 => Cas (of_val v0) (of_val v1) e
   end.
 
-Instance ectx_fill : Fill ectx expr :=
-  fix go K e := let _ : Fill _ _ := @go in
+Fixpoint fill K e :=
+  (* FIXME RJ: This really is fold_left, but if I use that all automation breaks:
+       fold_left (fun e Ki => ectx_item_fill Ki e).
+     Or maybe we even have a combinator somewhere to swap the arguments? *)
   match K with [] => e | Ki :: K => ectx_item_fill Ki (fill K e) end.
 
 (** The stepping relation *)
@@ -305,16 +307,18 @@ Program Canonical Structure heap_lang : language := {|
   of_val := heap_lang.of_val; to_val := heap_lang.to_val;
   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,
   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.
   split.
   * 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.
-  * 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
       K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto.
     rewrite heap_lang.fill_app in Heq1; apply (injective _) in Heq1.

iris/hoare.v

@@ -57,9 +57,9 @@ Proof.
   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.
 Qed.
-Lemma ht_bind `{CtxLanguage Λ C} K E P Q Q' e :
-  ({{ P }} e @ E {{ Q }} ∧ ∀ v, {{ Q v }} fill K (of_val v) @ E {{ Q' }})
-  ⊑ {{ P }} fill K e @ E {{ Q' }}.
+Lemma ht_bind `{LanguageCtx Λ K} E P Q Q' e :
+  ({{ P }} e @ E {{ Q }} ∧ ∀ v, {{ Q v }} K (of_val v) @ E {{ Q' }})
+  ⊑ {{ P }} K e @ E {{ Q' }}.
 Proof.
   intros; apply (always_intro' _ _), impl_intro_l.
   rewrite (associative _ P) {1}/ht always_elim impl_elim_r.

iris/language.v

@@ -52,17 +52,13 @@ Section language.
   Proof. by intros v v' Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
 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 Λ)} := {
-  fill_not_val K e :
-    to_val e = None → to_val (fill K e) = None;
-  fill_step K e1 σ1 e2 σ2 ef :
+Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
+  fill_not_val e :
+    to_val e = None → to_val (K e) = None;
+  fill_step e1 σ1 e2 σ2 ef :
     prim_step e1 σ1 e2 σ2 ef →
-    prim_step (fill K e1) σ1 (fill K e2) σ2 ef;
-  fill_step_inv 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
+    prim_step (K e1) σ1 (K e2) σ2 ef;
+  fill_step_inv 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
 }.

iris/weakestpre.v

@@ -161,17 +161,17 @@ Proof.
   * apply wp_frame_r; [auto|exists r2, rR; split_ands; auto].
     eapply uPred_weaken with rR n; eauto.
 Qed.
-Lemma wp_bind `{CtxLanguage Λ C} E K e Q :
-  wp E e (λ v, wp E (fill K (of_val v)) Q) ⊑ wp E (fill K e) Q.
+Lemma wp_bind `{LanguageCtx Λ K} E e Q :
+  wp E e (λ v, wp E (K (of_val v)) Q) ⊑ wp E (K e) Q.
 Proof.
   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.
   intros rf k Ef σ1 ???; destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
   split.
   { 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 ?.
-  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.
   exists r2, r2'; split_ands; try eapply IH; eauto.
 Qed.