1 files changed, 41 insertions, 0 deletions

diff --git a/theories/dynlang/operational.v b/theories/dynlang/operational.v
new file mode 100644
index 0000000..34cca7b
--- /dev/null
+++ b/theories/dynlang/operational.v
@@ -0,0 +1,41 @@
+From mininix Require Export utils.
+From stdpp Require Import options.
+
+Module Import dynlang.
+
+Inductive expr :=
+  | EString (s : string)
+  | EId (ds : gmap string expr) (ex : expr)
+  | EAbs (ex e : expr)
+  | EApp (e1 e2 : expr).
+
+Fixpoint subst (ds : gmap string expr) (e : expr) : expr :=
+  match e with
+  | EString s => EString s
+  | EId ds' e => EId (ds ∪ ds') (subst ds e)
+  | EAbs ex e => EAbs (subst ds ex) (subst ds e)
+  | EApp e1 e2 => EApp (subst ds e1) (subst ds e2)
+  end.
+
+Reserved Infix "-->" (right associativity, at level 55).
+Inductive step : expr → expr → Prop :=
+  | Sβ x e1 e2 : EApp (EAbs (EString x) e1) e2 --> subst {[x:=e2]} e1
+  | SIdString ds x e : ds !! x = Some e → EId ds (EString x) --> e
+  | SAbsL ex1 ex1' e : ex1 --> ex1' → EAbs ex1 e --> EAbs ex1' e
+  | SAppL e1 e1' e2 : e1 --> e1' → EApp e1 e2 --> EApp e1' e2
+  | SId ds e1 e1' : e1 --> e1' → EId ds e1 --> EId ds e1'
+where "e1 --> e2" := (step e1 e2).
+
+Infix "-->*" := (rtc step) (right associativity, at level 55).
+
+Definition final (e : expr) : Prop :=
+  match e with
+  | EString _ => True
+  | EAbs (EString _) _ => True
+  | _ => False
+  end.
+
+Definition stuck (e : expr) : Prop :=
+  nf step e ∧ ¬final e.
+
+End dynlang.