diff options
| author | Malte Voos <git@mal.tc> | 2024-06-23 23:31:59 +0200 |
|---|---|---|
| committer | Malte Voos <git@mal.tc> | 2024-06-24 00:16:55 +0200 |
| commit | 5d227bcd0055d02e1d49a3dcd27e80a756923d5b (patch) | |
| tree | da468ad3a8f3caf709b731ca2678c86a5a015990 /src/nbe/Domain.ml | |
| parent | 8d40541003736d5319ec981278338e8c8c66daf6 (diff) | |
| download | toytt-5d227bcd0055d02e1d49a3dcd27e80a756923d5b.tar.gz toytt-5d227bcd0055d02e1d49a3dcd27e80a756923d5b.zip | |
split code into smaller libraries and make a better repl
Diffstat (limited to 'src/nbe/Domain.ml')
| -rw-r--r-- | src/nbe/Domain.ml | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/src/nbe/Domain.ml b/src/nbe/Domain.ml new file mode 100644 index 0000000..6f5e11c --- /dev/null +++ b/src/nbe/Domain.ml @@ -0,0 +1,30 @@ +open Bwd + +type t = Data.value = + | Neutral of ne + | Pi of Ident.local * t * clo + | Lam of Ident.local * clo + | Sg of Ident.local * t * clo + | Pair of t * t + | Type + | Bool + | True + | False + +and ne = Data.ne +and ne_head = Data.ne_head = Var of int (* De Bruijn levels *) +and frm = Data.frm = + | App of t + | Fst + | Snd + | BoolElim of { + motive_var : Ident.local; + motive : clo; + true_case : t; + false_case: t; + } + +and env = Data.env +and clo = Data.clo = Clo of { body : Data.syn; env : env } + +let var i = Neutral (Var i, Bwd.Emp) |