blob: f0922e8c85904ef12275f825f7f4c12afd1ffe9c (
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 Name.local * t * clo
| Lam of Name.local * clo
| Sg of Name.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 Name.t * t Lazy.t
and frm = Data.frm =
| App of t
| Fst
| Snd
| BoolElim of {
motive_var : Name.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)
|