From 8d40541003736d5319ec981278338e8c8c66daf6 Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Sun, 23 Jun 2024 01:36:48 +0200
Subject: keep track of bound names everywhere to be able to output names
 instead of de bruijn indices

---
 lib/Data.ml | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

(limited to 'lib/Data.ml')

diff --git a/lib/Data.ml b/lib/Data.ml
index 19ca67d..d2f94d3 100644
--- a/lib/Data.ml
+++ b/lib/Data.ml
@@ -4,10 +4,10 @@ open Bwd
 
 type syn =
   | Var of int
-  | Pi of syn * (* BINDS *) syn
-  | Lam of (* BINDS *) syn
+  | Pi of Ident.local * syn * (* BINDS *) syn
+  | Lam of Ident.local * (* BINDS *) syn
   | App of syn * syn
-  | Sg of syn * (* BINDS *) syn
+  | Sg of Ident.local * syn * (* BINDS *) syn
   | Pair of syn * syn
   | Fst of syn
   | Snd of syn
@@ -16,6 +16,7 @@ type syn =
   | True
   | False
   | BoolElim of {
+      motive_var : Ident.local;
       motive : (* BINDS *) syn;
       true_case : syn;
       false_case : syn;
@@ -26,9 +27,9 @@ type syn =
 
 type value =
   | Neutral of ne
-  | Pi of value * clo
-  | Lam of clo
-  | Sg of value * clo
+  | Pi of Ident.local * value * clo
+  | Lam of Ident.local * clo
+  | Sg of Ident.local * value * clo
   | Pair of value * value
   | Type
   | Bool
@@ -42,9 +43,10 @@ and frm =
   | Fst
   | Snd
   | BoolElim of {
-      cmot: clo;
-      vtrue: value;
-      vfalse: value;
+      motive_var : Ident.local;
+      motive: clo;
+      true_case: value;
+      false_case: value;
     }
 
 and env = value bwd
-- 
cgit 1.4.1