Initialize repository

1 files changed, 140 insertions, 0 deletions

diff --git a/theories/evallang/operational.v b/theories/evallang/operational.v
new file mode 100644
index 0000000..79174dd
--- /dev/null
+++ b/theories/evallang/operational.v
@@ -0,0 +1,140 @@
+From Coq Require Import Ascii.
+From mininix Require Export utils.
+From stdpp Require Import options.
+
+Module Import evallang.
+
+Inductive expr :=
+  | EString (s : string)
+  | EId (ds : option expr) (x : string)
+  | EEval (ds : gmap string expr) (ee : expr)
+  | EAbs (ex e : expr)
+  | EApp (e1 e2 : expr).
+
+Module parser.
+  Inductive token :=
+    | TId (s : string)
+    | TString (s : string)
+    | TColon
+    | TExclamation
+    | TParenL
+    | TParenR.
+
+  Inductive token_state :=
+    TSString (s : string) | TSId (s : string) | TSOther.
+
+  Definition token_state_push (st : token_state) (k : list token) : list token :=
+    match st with
+    | TSId s => TId (String.rev s) :: k
+    | _ => k
+    end.
+
+  Fixpoint tokenize_go (sin : string) (st : token_state)
+      (k : list token) : option (list token) :=
+    match sin, st with
+    | "", TSString _ => None (* no closing "" *)
+    | "", _ => Some (reverse (token_state_push st k))
+    | String "\" (String """" sin), TSString s =>
+        tokenize_go sin (TSString (String """" s)) k
+    | String """" sin, TSString s =>
+        tokenize_go sin TSOther (TString (String.rev s) :: k)
+    | String a sin, TSString s => tokenize_go sin (TSString (String a s)) k
+    | String ":" sin, _ => tokenize_go sin TSOther (TColon :: token_state_push st k)
+    | String "!" sin, _ => tokenize_go sin TSOther (TExclamation :: token_state_push st k)
+    | String "(" sin, _ => tokenize_go sin TSOther (TParenL :: token_state_push st k)
+    | String ")" sin, _ => tokenize_go sin TSOther (TParenR :: token_state_push st k)
+    | String """" sin, _ => tokenize_go sin (TSString "") k
+    | String a sin, TSOther =>
+       if Ascii.is_space a then tokenize_go sin TSOther k
+       else tokenize_go sin (TSId (String a EmptyString)) k
+    | String a sin, TSId s =>
+       if Ascii.is_space a then tokenize_go sin TSOther (TId (String.rev s) :: k)
+       else tokenize_go sin (TSId (String a s)) k
+    end.
+  Definition tokenize (sin : string) : option (list token) :=
+    tokenize_go sin TSOther [].
+
+  Inductive stack_item :=
+    | SExpr (e : expr)
+    | SAbsR (e : expr)
+    | SEval
+    | SParenL.
+
+  Definition stack_push (e : expr) (k : list stack_item) : list stack_item :=
+    match k with
+    | SExpr e1 :: k => SExpr (EApp e1 e) :: k
+    | SEval :: k => SExpr (EEval ∅ e) :: k
+    | _ => SExpr e :: k
+    end.
+
+  Fixpoint stack_pop_go (e : expr)
+      (k : list stack_item) : option (expr * list stack_item) :=
+    match k with
+    | SAbsR e1 :: k => stack_pop_go (EAbs e1 e) k
+    | _ => Some (e, k)
+    end.
+
+  Definition stack_pop (k : list stack_item) : option (expr * list stack_item) :=
+    match k with
+    | SExpr e :: k => stack_pop_go e k
+    | _ => None
+    end.
+
+  Fixpoint parse_go (ts : list token) (k : list stack_item) : option expr :=
+    match ts with
+    | [] => '(e, k) ← stack_pop k; guard (k = []);; Some e
+    | TString x :: ts => parse_go ts (stack_push (EString x) k)
+    | TId "eval" :: TExclamation :: ts => parse_go ts (SEval :: k)
+    | TId x :: TColon :: ts => parse_go ts (SAbsR (EString x) :: k)
+    | TId x :: ts => parse_go ts (stack_push (EId None x) k)
+    | TColon :: ts =>
+       '(e, k) ← stack_pop k;
+       parse_go ts (SAbsR e :: k)
+    | TParenL :: ts => parse_go ts (SParenL :: k)
+    | TParenR :: ts =>
+       '(e, k) ← stack_pop k;
+       match k with
+       | SParenL :: k => parse_go ts (stack_push e k)
+       | _ => None
+       end
+    | _ => None
+    end.
+
+  Definition parse (sin : string) : option expr :=
+    ts ← tokenize sin; parse_go ts [].
+End parser.
+
+Definition parse := parser.parse.
+
+Fixpoint subst (ds : gmap string expr) (e : expr) : expr :=
+  match e with
+  | EString s => EString s
+  | EId ds' x => EId (ds !! x ∪ ds') x
+  | EEval ds' ee => EEval (ds ∪ ds') (subst ds ee)
+  | 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
+  | SId e x : EId (Some e) x --> e
+  | SEvalString ds s e : parse s = Some e → EEval ds (EString s) --> subst ds 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
+  | SEval ds e1 e1' : e1 --> e1' → EEval ds e1 --> EEval 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 evallang.