work on language interface

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.
+