From 97f84ccace4e634b4e02178a702818e69292dc9f Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Mon, 8 Jul 2024 22:01:42 +0200 Subject: implement top-level definitions --- src/nbe/Data.ml | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) (limited to 'src/nbe/Data.ml') diff --git a/src/nbe/Data.ml b/src/nbe/Data.ml index d2f94d3..8589ea5 100644 --- a/src/nbe/Data.ml +++ b/src/nbe/Data.ml @@ -1,9 +1,8 @@ open Bwd -(** Syntactic terms *) - type syn = | Var of int + | Def of Ident.t * value Lazy.t | Pi of Ident.local * syn * (* BINDS *) syn | Lam of Ident.local * (* BINDS *) syn | App of syn * syn @@ -23,10 +22,9 @@ type syn = scrut : syn; } -(** Semantic domain *) - -type value = +and value = | Neutral of ne + | Unfold of unfold | Pi of Ident.local * value * clo | Lam of Ident.local * clo | Sg of Ident.local * value * clo @@ -37,7 +35,13 @@ type value = | False and ne = ne_head * frm bwd -and ne_head = Var of int (* De Bruijn levels *) +and ne_head = + | Var of int (* De Bruijn levels *) + +and unfold = unfold_head * frm bwd * value Lazy.t +and unfold_head = + | Def of Ident.t * value Lazy.t + and frm = | App of value | Fst -- cgit 1.4.1