blob: 2f6536d6a09631c214a64f71e7d5c11a938b4ad7 (
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
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
|
type raw_ident = Yuujinchou.Trie.path
type ident = raw_ident Asai.Range.located
type raw_arg = { name : ident; ty : expr }
and arg = raw_arg Asai.Range.located
and raw_expr =
| Var of raw_ident
| Pi of arg * expr
| Lam of ident * expr
| App of expr * expr
| Sg of arg * expr
| Pair of expr * expr
| Fst of expr
| Snd of expr
| Type
| Bool
| True
| False
| BoolElim of {
motive_var : ident;
motive_body : expr;
true_case : expr;
false_case : expr;
scrut : expr;
}
and expr = raw_expr Asai.Range.located
let pp_raw_ident fmt (id : raw_ident) = Format.pp_print_list
~pp_sep:(fun fmt () -> Format.pp_print_char fmt '.')
Format.pp_print_string fmt id
let pp_ident fmt ({ value; _ } : ident) = pp_raw_ident fmt value
let rec pp_raw_arg fmt ({ name; ty } : raw_arg) =
Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" pp_ident name pp_expr ty
and pp_arg fmt ({ value; _ } : arg) = pp_raw_arg fmt value
and pp_raw_expr fmt = function
| Var id -> Format.fprintf fmt "Var @[%a@]" pp_raw_ident id
| 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@])@]"
pp_ident motive_var
pp_expr motive_body
pp_expr true_case
pp_expr false_case
pp_expr scrut
| Pi (dom, cod) ->
Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" pp_arg dom pp_expr cod
| Lam (var, body) ->
Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" pp_ident var pp_expr body
| App (fn, arg) ->
Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" pp_expr fn pp_expr arg
| Sg (fst, snd) ->
Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" pp_arg fst pp_expr snd
| Pair (fst, snd) ->
Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" pp_expr fst pp_expr snd
| Fst p -> Format.fprintf fmt "@[<5>Fst (@[%a@])@]" pp_expr p
| Snd p -> Format.fprintf fmt "@[<5>Snd (@[%a@])@]" pp_expr p
| Type -> Format.pp_print_string fmt "Type"
and pp_expr fmt ({ value; _ } : expr) = pp_raw_expr fmt value
|