blob: bf5ed90f95b3554e7bfc00be63b98638e10e09f8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
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
| 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 unfold = Data.unfold
and unfold_head = Data.unfold_head =
| Def of Ident.t * t Lazy.t
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, Emp)
let def p v = Unfold (Def (p, v), Emp, v)
|