Add a notion of a language based on evaluation context items

and show that this is an instance of evaluation contexts

heap_lang/lang.v

-From iris.program_logic Require Export ectx_language.
+From iris.program_logic Require Export ectx_language ectxi_language.
 From iris.prelude Require Export strings.
 From iris.prelude Require Import gmap.
 
@@ -171,8 +171,6 @@ Inductive ectx_item :=
   | CasMCtx (v0 : val) (e2 : expr [])
   | CasRCtx (v0 : val) (v1 : val).
 
-Notation ectx := (list ectx_item).
-
 Definition fill_item (Ki : ectx_item) (e : expr []) : expr [] :=
   match Ki with
   | AppLCtx e2 => App e e2
@@ -196,7 +194,6 @@ Definition fill_item (Ki : ectx_item) (e : expr []) : expr [] :=
   | CasMCtx v0 e2 => CAS (of_val v0) e e2
   | CasRCtx v0 v1 => CAS (of_val v0) (of_val v1) e
   end.
-Definition fill (K : ectx) (e : expr []) : expr [] := fold_right fill_item e K.
 
 (** Substitution *)
 (** We have [subst' e BAnon v = e] to deal with anonymous binders *)
@@ -432,17 +429,9 @@ Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
 Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
 
-Instance fill_inj K : Inj (=) (=) (fill K).
-Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
-
-Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
-Proof.
-  intros [v' Hv']; revert v' Hv'.
-  induction K as [|[]]; intros; simplify_option_eq; eauto.
-Qed.
-
-Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
-Proof. rewrite !eq_None_not_Some; eauto using fill_val. Qed.
+Lemma fill_item_val Ki e :
+  is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
+Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
 
 Lemma val_stuck e1 σ1 e2 σ2 ef :
   head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
@@ -457,12 +446,6 @@ Proof.
     repeat (case_match || contradiction); eauto.
 Qed.
 
-Lemma atomic_fill K e : atomic (fill K e) → to_val e = None → K = [].
-Proof.
-  destruct K as [|Ki K]; [done|].
-  rewrite eq_None_not_Some=> /= ? []; eauto using atomic_fill_item, fill_val.
-Qed.
-
 Lemma atomic_step e1 σ1 e2 σ2 ef :
   atomic e1 → head_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
 Proof.
@@ -484,22 +467,6 @@ Proof.
     end; auto.
 Qed.
 
-(* When something does a step, and another decomposition of the same expression
-has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
-other words, [e] also contains the reducible expression *)
-Lemma step_by_val K K' e1 e1' σ1 e2 σ2 ef :
-  fill K e1 = fill K' e1' → to_val e1 = None → head_step e1' σ1 e2 σ2 ef →
-  exists K'', K' = K ++ K''. (* K `prefix_of` K' *)
-Proof.
-  intros Hfill Hred Hnval; revert K' Hfill.
-  induction K as [|Ki K IH]; simpl; intros K' Hfill; first by eauto.
-  destruct K' as [|Ki' K']; simplify_eq/=.
-  { exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
-      eauto using fill_not_val, head_ctx_step_val. }
-  cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
-  eauto using fill_item_no_val_inj, val_stuck, fill_not_val.
-Qed.
-
 Lemma alloc_fresh e v σ :
   let l := fresh (dom _ σ) in
   to_val e = Some v → head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
@@ -553,23 +520,19 @@ Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
 End heap_lang.
 
 (** Language *)
-Program Instance heap_ectx_lang :
-  EctxLanguage
-    (heap_lang.expr []) heap_lang.val heap_lang.ectx heap_lang.state := {|
+Program Instance heap_ectxi_lang :
+  EctxiLanguage
+    (heap_lang.expr []) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
   of_val := heap_lang.of_val; to_val := heap_lang.to_val;
-  empty_ectx := []; comp_ectx := (++); fill := heap_lang.fill; 
+  fill_item := heap_lang.fill_item; 
   atomic := heap_lang.atomic; head_step := heap_lang.head_step;
 |}.
 Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
   heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step,
-  heap_lang.fill_not_val, heap_lang.atomic_fill,
-  heap_lang.step_by_val, fold_right_app, app_eq_nil.
-
-Canonical Structure heap_lang := ectx_lang heap_ectx_lang.
+  heap_lang.fill_item_val, heap_lang.atomic_fill_item,
+  heap_lang.fill_item_no_val_inj, heap_lang.head_ctx_step_val.
 
-Global Instance heap_lang_ctx_item Ki :
-  LanguageCtx heap_lang (heap_lang.fill_item Ki).
-Proof. change (LanguageCtx heap_lang (heap_lang.fill [Ki])). apply _. Qed.
+Canonical Structure heap_lang := ectx_lang (heap_lang.expr []).
 
 (* Prefer heap_lang names over ectx_language names. *)
 Export heap_lang.

heap_lang/lifting.v

@@ -9,7 +9,6 @@ Section lifting.
 Context {Σ : iFunctor}.
 Implicit Types P Q : iProp heap_lang Σ.
 Implicit Types Φ : val → iProp heap_lang Σ.
-Implicit Types K : ectx.
 Implicit Types ef : option (expr []).
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
@@ -17,6 +16,11 @@ Lemma wp_bind {E e} K Φ :
   WP e @ E {{ λ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
 Proof. exact: wp_ectx_bind. Qed.
 
+Lemma wp_bindi {E e} Ki Φ :
+  WP e @ E {{ λ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
+     WP fill_item Ki e @ E {{ Φ }}.
+Proof. exact: weakestpre.wp_bind. Qed.
+
 (** Base axioms for core primitives of the language: Stateful reductions. *)
 Lemma wp_alloc_pst E σ e v Φ :
   to_val e = Some v →

program_logic/ectx_language.v

 (** An axiomatization of evaluation-context based languages, including a proof
     that this gives rise to a "language" in the Iris sense. *)
 From iris.algebra Require Export base.
-From iris.program_logic Require Export language.
+From iris.program_logic Require Import language.
 
 (* We need to make thos arguments indices that we want canonical structure
    inference to use a keys. *)
@@ -137,4 +137,4 @@ Section ectx_language.
   Qed.
 End ectx_language.
 
-Arguments ectx_lang {_ _ _ _} _.
+Arguments ectx_lang _ {_ _ _ _}.

program_logic/ectx_weakestpre.v

@@ -5,8 +5,8 @@ From iris.program_logic Require Import ownership.
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
 Context {Σ : iFunctor}.
-Implicit Types P : iProp (ectx_lang Λ) Σ.
-Implicit Types Φ : val → iProp (ectx_lang Λ) Σ.
+Implicit Types P : iProp (ectx_lang expr) Σ.
+Implicit Types Φ : val → iProp (ectx_lang expr) Σ.
 Implicit Types v : val.
 Implicit Types e : expr.
 Hint Resolve head_prim_reducible head_reducible_prim_step.

program_logic/ectxi_language.v

+(** An axiomatization of languages based on evaluation context items, including
+    a proof that these are instances of general ectx-based languages. *)
+From iris.algebra Require Export base.
+From iris.program_logic Require Import language ectx_language.
+
+(* We need to make thos arguments indices that we want canonical structure
+   inference to use a keys. *)
+Class EctxiLanguage (expr val ectx_item state : Type) := {
+  of_val : val → expr;
+  to_val : expr → option val;
+  fill_item : ectx_item → expr → expr;
+  atomic : expr → Prop;
+  head_step : expr → state → expr → state → option expr → Prop;
+
+  to_of_val v : to_val (of_val v) = Some v;
+  of_to_val e v : to_val e = Some v → of_val v = e;
+  val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef → to_val e1 = None;
+
+  fill_item_inj Ki :> Inj (=) (=) (fill_item Ki);
+  fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e);
+  fill_item_no_val_inj Ki1 Ki2 e1 e2 :
+    to_val e1 = None → to_val e2 = None →
+    fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2;
+
+  head_ctx_step_val Ki e σ1 e2 σ2 ef :
+    head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e);
+
+  atomic_not_val e : atomic e → to_val e = None;
+  atomic_step e1 σ1 e2 σ2 ef :
+    atomic e1 →
+    head_step e1 σ1 e2 σ2 ef →
+    is_Some (to_val e2);
+  atomic_fill_item e Ki :
+    atomic (fill_item Ki e) → is_Some (to_val e)
+}.
+
+Arguments of_val {_ _ _ _ _} _.
+Arguments to_val {_ _ _ _ _} _.
+Arguments fill_item {_ _ _ _ _} _ _.
+Arguments atomic {_ _ _ _ _} _.
+Arguments head_step {_ _ _ _ _} _ _ _ _ _.
+
+Arguments to_of_val {_ _ _ _ _} _.
+Arguments of_to_val {_ _ _ _ _} _ _ _.
+Arguments val_stuck {_ _ _ _ _} _ _ _ _ _ _.
+Arguments fill_item_val {_ _ _ _ _} _ _ _.
+Arguments fill_item_no_val_inj {_ _ _ _ _} _ _ _ _ _ _ _.
+Arguments head_ctx_step_val {_ _ _ _ _} _ _ _ _ _ _ _.
+Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.
+Arguments atomic_not_val {_ _ _ _ _} _ _.
+Arguments atomic_step {_ _ _ _ _} _ _ _ _ _ _ _.
+Arguments atomic_fill_item {_ _ _ _ _} _ _ _.
+
+Section ectxi_language.
+  Context {expr val ectx_item state}
+          {Λ : EctxiLanguage expr val ectx_item state}.
+  Implicit Types (e : expr) (Ki : ectx_item).
+  Notation ectx := (list ectx_item).
+
+  Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.
+
+  Instance fill_inj K : Inj (=) (=) (fill K).
+  Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
+
+  Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
+  Proof.
+    induction K; simpl; first done. intros ?%fill_item_val. eauto.
+  Qed.
+
+  Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
+  Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
+
+  Lemma atomic_fill K e : atomic (fill K e) → to_val e = None → K = [].
+  Proof.
+    destruct K as [|Ki K]; [done|].
+    rewrite eq_None_not_Some=> /= ? []; eauto using atomic_fill_item, fill_val.
+  Qed.
+
+  (* When something does a step, and another decomposition of the same expression
+  has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
+  other words, [e] also contains the reducible expression *)
+  Lemma step_by_val K K' e1 e1' σ1 e2 σ2 ef :
+    fill K e1 = fill K' e1' → to_val e1 = None → head_step e1' σ1 e2 σ2 ef →
+    exists K'', K' = K ++ K''. (* K `prefix_of` K' *)
+  Proof.
+    intros Hfill Hred Hnval; revert K' Hfill.
+    induction K as [|Ki K IH]; simpl; intros K' Hfill; first by eauto.
+    destruct K' as [|Ki' K']; simplify_eq/=.
+    { exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
+      eauto using fill_not_val, head_ctx_step_val. }
+    cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
+    eauto using fill_item_no_val_inj, val_stuck, fill_not_val.
+  Qed.
+
+  Global Program Instance : EctxLanguage expr val ectx state :=
+    (* For some reason, Coq always rejects the record syntax claiming I
+       fixed fields of different records, even when I did not. *)
+    Build_EctxLanguage expr val ectx state of_val to_val [] (++) fill atomic head_step _ _ _ _ _ _ _ _ _ _ _ _.
+  Solve Obligations with eauto using to_of_val, of_to_val, val_stuck,
+    atomic_not_val, atomic_step, fill_not_val, atomic_fill,
+    step_by_val, fold_right_app, app_eq_nil.
+
+  Global Instance ectxi_lang_ctx_item Ki :
+    LanguageCtx (ectx_lang expr) (fill_item Ki).
+  Proof. change (LanguageCtx _ (fill [Ki])). apply _. Qed.
+
+End ectxi_language.
+
+
+
+