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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
type ident = Name.t Asai.Range.located
type local_name = Name.local Asai.Range.located
type arg = local_name * expr
and raw_expr =
| Var of Name.t
| Check of expr * expr
| Pi of arg * expr
| Fun of expr * expr
| Lam of local_name * expr
| App of expr * expr
| Sg of arg * expr
| Prod of expr * expr
| Pair of expr * expr
| Fst of expr
| Snd of expr
| Type
| Bool
| True
| False
| BoolElim of {
motive_var : local_name;
motive_body : expr;
true_case : expr;
false_case : expr;
scrut : expr;
}
and expr = raw_expr Asai.Range.located
type item =
| Def of {
name : ident;
tp : expr;
tm : expr;
}
type file = item List.t
let dump_ident fmt ({ value; _ } : ident) = Name.pp fmt value
let dump_local_name fmt ({ value; _ } : local_name) = match value with
| Some name -> Format.pp_print_string fmt name
| None -> Format.pp_print_char fmt '_'
let rec dump_arg fmt ((name, tp) : arg) =
Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_local_name name dump_expr tp
and dump_raw_expr fmt = function
| Var name -> Format.fprintf fmt "Var @[%a@]" Name.pp name
| Check (tm, tp) -> Format.fprintf fmt "@[%a@] : @[%a@]" dump_expr tm dump_expr tp
| Bool -> Format.pp_print_string fmt "Bool"
| True -> Format.pp_print_string fmt "True"
| False -> Format.pp_print_string fmt "False"
| BoolElim { motive_var; motive_body; true_case; false_case; scrut } ->
Format.fprintf fmt
"@[<10>BoolElim (@[%a@] ->@ @[%a@],@ @[%a@],@ @[%a@],@ @[%a@])@]"
dump_local_name motive_var
dump_expr motive_body
dump_expr true_case
dump_expr false_case
dump_expr scrut
| Pi (dom, cod) ->
Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" dump_arg dom dump_expr cod
| Fun (dom, cod) ->
Format.fprintf fmt "@[<5>Fun (@[%a@],@ @[%a@])@]" dump_expr dom dump_expr cod
| Lam (var, body) ->
Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" dump_local_name var dump_expr body
| App (fn, arg) ->
Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" dump_expr fn dump_expr arg
| Sg (fst, snd) ->
Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" dump_arg fst dump_expr snd
| Prod (fst, snd) ->
Format.fprintf fmt "@[<6>Prod (@[%a@],@ @[%a@])@]" dump_expr fst dump_expr snd
| Pair (fst, snd) ->
Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" dump_expr fst dump_expr snd
| Fst p -> Format.fprintf fmt "@[<5>Fst (@[%a@])@]" dump_expr p
| Snd p -> Format.fprintf fmt "@[<5>Snd (@[%a@])@]" dump_expr p
| Type -> Format.pp_print_string fmt "Type"
and dump_expr fmt ({ value; _ } : expr) = dump_raw_expr fmt value
|