From 621ef7916c3e93419899641782b020de8eb3ad64 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 1 Feb 2016 13:01:32 +0100
Subject: [PATCH] Typeclass for evaluation context based language.

---
 barrier/heap_lang.v | 10 +++++-----
 barrier/lifting.v   |  2 +-
 iris/hoare.v        |  6 +++---
 iris/language.v     | 23 ++++++++++++++---------
 iris/weakestpre.v   |  8 ++++----
 5 files changed, 27 insertions(+), 22 deletions(-)

diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index f58ee88c0..d579636ee 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -414,15 +414,15 @@ Section Language.
     - clear Hatomic. eapply reducible_not_value. do 3 eexists; eassumption.
   Qed.
 
-  (** We can have bind with arbitrary evaluation contexts **)
-  Lemma fill_is_ctx K: is_ctx (fill K).
+  Global Instance heap_lang_fill : Fill ectx expr := fill.
+  Global Instance heap_lang_ctx : CtxLanguage heap_lang ectx.
   Proof.
     split.
-    - intros ? Hnval. by eapply fill_not_value.
-    - intros ? ? ? ? ? (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
+    - intros K ? Hnval. by eapply fill_not_value.
+    - intros K ? ? ? ? ? (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
       exists (comp_ctx K K'), e1', e2'. rewrite -!fill_comp Heq1 Heq2.
       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].
       + do 3 eexists. eassumption.
       + assumption.
diff --git a/barrier/lifting.v b/barrier/lifting.v
index 704c29a9a..44bb7d593 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -10,7 +10,7 @@ Implicit Types Q : val heap_lang → iProp heap_lang Σ.
 (** Bind. *)
 Lemma wp_bind {E e} K 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. *)
 
diff --git a/iris/hoare.v b/iris/hoare.v
index edfc9e54f..a54afed2f 100644
--- a/iris/hoare.v
+++ b/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 `(HK : is_ctx K) E P Q Q' e :
-  ({{ P }} e @ E {{ Q }} ∧ ∀ v, {{ Q v }} K (of_val v) @ E {{ Q' }})
-  ⊑ {{ P }} K e @ E {{ Q' }}.
+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' }}.
 Proof.
   intros; apply (always_intro' _ _), impl_intro_l.
   rewrite (associative _ P) {1}/ht always_elim impl_elim_r.
diff --git a/iris/language.v b/iris/language.v
index 9bb0fca56..d9c9ef1e8 100644
--- a/iris/language.v
+++ b/iris/language.v
@@ -52,14 +52,19 @@ Section language.
   Qed.
   Global Instance: Injective (=) (=) (@of_val Λ).
   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.
 
+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
+}.
diff --git a/iris/weakestpre.v b/iris/weakestpre.v
index 8acb0c293..af6ea2e3b 100644
--- a/iris/weakestpre.v
+++ b/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 `(HK : is_ctx K) E e Q :
-  wp E e (λ v, wp E (K (of_val v)) Q) ⊑ wp E (K e) Q.
+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.
 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 is_ctx_value.
   intros rf k Ef σ1 ???; destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
   split.
   { 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 ?.
-  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.
   exists r2, r2'; split_ands; try eapply IH; eauto.
 Qed.
-- 
GitLab