diff options
| author | Malte Voos <git@mal.tc> | 2024-07-08 22:01:42 +0200 |
|---|---|---|
| committer | Malte Voos <git@mal.tc> | 2024-07-08 22:01:42 +0200 |
| commit | 97f84ccace4e634b4e02178a702818e69292dc9f (patch) | |
| tree | 9cef95c62e3fa078db256c7fe657732fecef40a8 /src/nbe/Domain.ml | |
| parent | 57de10d8728f51942f676b68f1f3ea29d9b78e6e (diff) | |
| download | toytt-97f84ccace4e634b4e02178a702818e69292dc9f.tar.gz toytt-97f84ccace4e634b4e02178a702818e69292dc9f.zip | |
implement top-level definitions
Diffstat (limited to 'src/nbe/Domain.ml')
| -rw-r--r-- | src/nbe/Domain.ml | 12 |
1 files changed, 10 insertions, 2 deletions
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) |