From 04d62df9fdd42c603fad7bb1b5e3fb49bf8550c1 Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Mon, 17 Jun 2024 17:41:38 +0200
Subject: implement typechecking

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

(limited to 'lib/Data.ml')

diff --git a/lib/Data.ml b/lib/Data.ml
new file mode 100644
index 0000000..19ca67d
--- /dev/null
+++ b/lib/Data.ml
@@ -0,0 +1,51 @@
+open Bwd
+
+(** Syntactic terms *)
+
+type syn =
+  | Var of int
+  | Pi of syn * (* BINDS *) syn
+  | Lam of (* BINDS *) syn
+  | App of syn * syn
+  | Sg of syn * (* BINDS *) syn
+  | Pair of syn * syn
+  | Fst of syn
+  | Snd of syn
+  | Type
+  | Bool
+  | True
+  | False
+  | BoolElim of {
+      motive : (* BINDS *) syn;
+      true_case : syn;
+      false_case : syn;
+      scrut : syn;
+    }
+
+(** Semantic domain *)
+
+type value =
+  | Neutral of ne
+  | Pi of value * clo
+  | Lam of clo
+  | Sg of value * clo
+  | Pair of value * value
+  | Type
+  | Bool
+  | True
+  | False
+
+and ne = ne_head * frm bwd
+and ne_head = Var of int (* De Bruijn levels *)
+and frm = 
+  | App of value
+  | Fst
+  | Snd
+  | BoolElim of {
+      cmot: clo;
+      vtrue: value;
+      vfalse: value;
+    }
+
+and env = value bwd
+and clo = Clo of { body : syn; env : env }
-- 
cgit 1.4.1