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/Domain.ml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'src/nbe/Domain.ml') diff --git a/src/nbe/Domain.ml b/src/nbe/Domain.ml index 6f5e11c..bf5ed90 100644 --- a/src/nbe/Domain.ml +++ b/src/nbe/Domain.ml @@ -2,6 +2,7 @@ open Bwd type t = Data.value = | Neutral of ne + | Unfold of unfold | Pi of Ident.local * t * clo | Lam of Ident.local * clo | Sg of Ident.local * t * clo @@ -12,7 +13,13 @@ type t = Data.value = | False and ne = Data.ne -and ne_head = Data.ne_head = Var of int (* De Bruijn levels *) +and ne_head = Data.ne_head = + | Var of int (* De Bruijn levels *) + +and unfold = Data.unfold +and unfold_head = Data.unfold_head = + | Def of Ident.t * t Lazy.t + and frm = Data.frm = | App of t | Fst @@ -27,4 +34,5 @@ and frm = Data.frm = and env = Data.env and clo = Data.clo = Clo of { body : Data.syn; env : env } -let var i = Neutral (Var i, Bwd.Emp) +let var i = Neutral (Var i, Emp) +let def p v = Unfold (Def (p, v), Emp, v) -- cgit 1.4.1