From ba61dfd69504ec6263a9dee9931d93adeb6f3142 Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Mon, 7 Jul 2025 21:52:08 +0200
Subject: Initialize repository

---
 theories/evallang/interp.v | 52 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 theories/evallang/interp.v

(limited to 'theories/evallang/interp.v')

diff --git a/theories/evallang/interp.v b/theories/evallang/interp.v
new file mode 100644
index 0000000..d98b87f
--- /dev/null
+++ b/theories/evallang/interp.v
@@ -0,0 +1,52 @@
+From mininix Require Export res evallang.operational_props.
+From stdpp Require Import options.
+
+Module Import evallang.
+Export evallang.
+
+Inductive thunk := Thunk { thunk_env : gmap string thunk; thunk_expr : expr }.
+Add Printing Constructor thunk.
+Notation env := (gmap string thunk).
+
+Inductive val :=
+  | VString (s : string)
+  | VClo (x : string) (E : env) (e : expr).
+
+Global Instance maybe_VString : Maybe VString := λ v,
+  if v is VString s then Some s else None.
+Global Instance maybe_VClo : Maybe3 VClo := λ v,
+  if v is VClo x E e then Some (x, E, e) else None.
+
+Definition interp1 (interp : env → expr → res val) (E : env) (e : expr) : res val :=
+  match e with
+  | EString s =>
+      mret (VString s)
+  | EId ds x =>
+      t ← Res $ (E !! x) ∪ (Thunk ∅ <$> ds);
+      interp (thunk_env t) (thunk_expr t)
+  | EEval ds e =>
+      v ← interp E e;
+      s ← Res $ maybe VString v;
+      e ← Res $ parse s;
+      interp (E ∪ (Thunk ∅ <$> ds)) e
+  | EAbs ex e =>
+      v ← interp E ex;
+      x ← Res $ maybe VString v;
+      mret (VClo x E e)
+  | EApp e1 e2 =>
+      v1 ← interp E e1;
+      '(x, E', e') ← Res (maybe3 VClo v1);
+      interp (<[x:=Thunk E e2]> E') e'
+  end.
+
+Fixpoint interp (n : nat) (E : env) (e : expr) : res val :=
+  match n with
+  | O => NoFuel
+  | S n => interp1 (interp n) E e
+  end.
+
+Global Opaque interp.
+
+End evallang.
+
+Add Printing Constructor evallang.thunk.
-- 
cgit v1.2.3