From 407a2a4a0a440c41adc19fbe8b67283b7b7c65ab Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Mon, 19 Feb 2024 12:57:26 +0100
Subject: core syntax, semantic domain, evaluation

---
 lib/Domain.ml | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 lib/Domain.ml

(limited to 'lib/Domain.ml')

diff --git a/lib/Domain.ml b/lib/Domain.ml
new file mode 100644
index 0000000..cf07a4b
--- /dev/null
+++ b/lib/Domain.ml
@@ -0,0 +1,27 @@
+open Bwd
+
+type value =
+  | Neutral of ne
+  | Pi of value * clos
+  | Lam of clos
+  | Sg of value * clos
+  | Pair of value * value
+  | Type
+  | Bool
+  | True
+  | False
+
+and ne = ne_head * frame bwd
+and ne_head = Var of int (* De Bruijn levels *)
+and frame = 
+  | BoolElim of {
+      cmot: clos;
+      vtrue: value;
+      vfalse: value;
+    }
+  | App of value
+  | Fst
+  | Snd
+
+and env = value bwd
+and clos = Clos of { body : Syntax.tm; env : env }
-- 
cgit 1.4.1