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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
|
open Bwd
open Bwd.Infix
type t = Data.syn =
| Var of int
| Pi of Ident.local * t * (* BINDS *) t
| Lam of Ident.local * (* BINDS *) t
| App of t * t
| Sg of Ident.local * t * (* BINDS *) t
| Pair of t * t
| Fst of t
| Snd of t
| Type
| Bool
| True
| False
| BoolElim of {
motive_var : Ident.local;
motive : (* BINDS *) t;
true_case : t;
false_case : t;
scrut : t;
}
module Pretty =
struct
module Internal =
struct
type env = {
names : Ident.local bwd;
prec : int;
}
module Eff = Algaeff.Reader.Make (struct type nonrec t = env end)
let bind (name : Ident.local) f fmt x =
let update env = { env with names = env.names <: name } in
Eff.scope update (fun () -> f fmt x)
let with_prec (prec : int) (inner : 'a Fmt.t) (fmt : Format.formatter) (v : 'a) =
Eff.scope (fun env -> { env with prec; }) (fun () -> inner fmt v)
let delimited inner = with_prec 0 inner
let parenthesize (prec : int) : 'a Fmt.t -> 'a Fmt.t =
if (Eff.read()).prec > prec then
Fmt.parens
else
Fun.id
let lassoc (prec : int)
(pp_left : 'l Fmt.t)
?(sep = " ")
(pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t =
parenthesize prec @@ fun fmt v ->
Fmt.pf fmt "@[%a@]%s@[%a@]"
(with_prec prec pp_left) (fst v)
sep
(with_prec (prec + 1) pp_right) (snd v)
let rassoc (prec : int)
(pp_left : 'l Fmt.t)
?(sep = " ")
(pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t =
parenthesize prec @@ fun fmt v ->
Fmt.pf fmt "@[%a@]%s@[%a@]"
(with_prec (prec + 1) pp_left) (fst v)
sep
(with_prec prec pp_right) (snd v)
let pp_local_name fmt name =
Fmt.string fmt @@ Option.value ~default:"_" name
let pp_var fmt ix =
let names = (Eff.read()).names in
match Bwd.nth_opt names ix with
(* the variable has a bound name which has not been shadowed *)
| Some ((Some name) as id) when Bwd.find_index ((=) id) names = Some ix -> Fmt.string fmt name
(* the variable does not have a bound name or its bound name has been shadowed *)
| Some _ -> Fmt.pf fmt "%@%d" ix
| None -> Reporter.bug "index out of range in pp_var"
let rec pp_pair fmt = (delimited @@ fun fmt (a, b) -> Fmt.pf fmt "@[(@[%a@], @[%a@])@]" pp a pp b) fmt
and pp_bool_elim fmt =
(delimited @@ fun fmt (motive_var, motive, true_case, false_case, scrut) -> Fmt.pf fmt
"@[bool-elim @[%a@] at @[%a@] -> @[%a@] [ true => @[%a@], false => @[%a@] ]@]"
pp scrut pp_local_name motive_var (bind motive_var pp) motive pp true_case pp false_case
) fmt
and pp_arg fmt (name, tp) =
Fmt.pf fmt "(@[%a@] : @[%a@])" pp_local_name name pp tp
(* TODO: improve indentation *)
and pp fmt = function
| Var ix -> pp_var fmt ix
| Pi (name, base, fam) -> rassoc 1 pp_arg ~sep:" -> " (bind name pp) fmt ((name, base), fam)
| Lam (name, body) -> Fmt.pf fmt "@[\\@[%a@] -> @[%a@]@]" pp_local_name name (bind name pp) body
| Sg (name, base, fam) -> rassoc 2 pp_arg ~sep:" * " (bind name pp) fmt ((name, base), fam)
| App (a, b) -> lassoc 3 pp pp fmt (a, b)
| Pair (a, b) -> pp_pair fmt (a, b)
| Fst a -> lassoc 3 Fmt.string pp fmt ("fst", a)
| Snd a -> lassoc 3 Fmt.string pp fmt ("snd", a)
| Type -> Fmt.string fmt "type"
| Bool -> Fmt.string fmt "bool"
| True -> Fmt.string fmt "true"
| False -> Fmt.string fmt "false"
| BoolElim { motive_var; motive; true_case; false_case; scrut }
-> pp_bool_elim fmt (motive_var, motive, true_case, false_case, scrut)
end
let pp fmt (tm, names) =
let env : Internal.env = { names; prec = 0; } in
Internal.Eff.run ~env (fun () -> Internal.pp fmt tm)
end
|