diff options
Diffstat (limited to 'src/nbe/Data.ml')
| -rw-r--r-- | src/nbe/Data.ml | 16 |
1 files changed, 10 insertions, 6 deletions
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 |