diff options
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) |