From 4d5ff4eb5f003c737a78276144b3f9305322edf4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 5 Jan 2016 19:24:15 +0100
Subject: [PATCH] work on language interface

---
 iris/language.v | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

diff --git a/iris/language.v b/iris/language.v
index 83fa44297..7bbeb35b5 100644
--- a/iris/language.v
+++ b/iris/language.v
@@ -4,18 +4,18 @@ Class Language (E V S : Type) := {
   to_expr : V → E;
   of_expr : E → option V;
   atomic : E → Prop;
-  prim_step : (E * S) → (E * S) → option E → Prop;
+  prim_step : E → S → E → S → option E → Prop;
   of_to_expr v : of_expr (to_expr v) = Some v;
   to_of_expr e v : of_expr e = Some v → to_expr v = e;
-  values_stuck e σ s' ef : prim_step (e,σ) s' ef → of_expr e = None;
+  values_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → of_expr e = None;
   atomic_not_value e : atomic e → of_expr e = None;
   atomic_step e1 σ1 e2 σ2 ef :
     atomic e1 →
-    prim_step (e1,σ1) (e2,σ2) ef →
+    prim_step e1 σ1 e2 σ2 ef →
     is_Some (of_expr e2)
 }.
 
-Section foo.
+Section Lang.
   Context `{Language E V St}.
 
   Definition cfg : Type := (list E * St)%type.
@@ -23,9 +23,17 @@ Section foo.
     | step_atomic e1 σ1 e2 σ2 ef t1 t2 :
        ρ1 = (t1 ++ e1 :: t2, σ1) →
        ρ1 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
-       prim_step (e1, σ1) (e2, σ2) ef →
+       prim_step e1 σ1 e2 σ2 ef →
        step ρ1 ρ2.
 
   Definition steps := rtc step.
   Definition stepn := nsteps step.
-End foo.
\ No newline at end of file
+
+  Definition is_ctx (ctx : E -> E) : Prop :=
+    (forall e, is_Some (of_expr (ctx e)) -> is_Some (of_expr e)) /\
+    (forall e1 σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef -> prim_step (ctx e1) σ1 (ctx e2) σ2 ef) /\
+    (forall e1' σ1 e2 σ2 ef, of_expr e1' = None -> prim_step (ctx e1') σ1 e2 σ2 ef ->
+                            exists e2', e2 = ctx e2' /\ prim_step e1' σ1 e2' σ2 ef).
+
+End Lang.
+
-- 
GitLab