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/Domain.ml | 34 ++++++++++++++++------------------
 1 file changed, 16 insertions(+), 18 deletions(-)

(limited to 'lib/Domain.ml')

diff --git a/lib/Domain.ml b/lib/Domain.ml
index 88560c2..67ac4ae 100644
--- a/lib/Domain.ml
+++ b/lib/Domain.ml
@@ -1,31 +1,29 @@
 open Bwd
 
-type value =
+type t = Data.value =
   | Neutral of ne
-  | Pi of value * clos
-  | Lam of clos
-  | Sg of value * clos
-  | Pair of value * value
+  | Pi of t * clo
+  | Lam of clo
+  | Sg of t * clo
+  | Pair of t * t
   | 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
+and ne = Data.ne
+and ne_head = Data.ne_head = Var of int (* De Bruijn levels *)
+and frm = Data.frm =
+  | App of t
   | Fst
   | Snd
+  | BoolElim of {
+      cmot: clo;
+      vtrue: t;
+      vfalse: t;
+    }
 
-and env = value bwd
-and clos = Clos of { body : Syntax.tm; env : env }
-
-type cell = { tm : value; tp : value }
+and env = Data.env
+and clo = Data.clo = Clo of { body : Data.syn; env : env }
 
 let var i = Neutral (Var i, Bwd.Emp)
-- 
cgit 1.4.1