Source file print.ml
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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
(** Pretty-printing for the core AST.
The functions of this module are used for printing terms and other objects
defined in the {!module:Term} module. This is mainly used for displaying
log messages, and feedback in case of success or error while type-checking
terms or testing convertibility. *)
open Lplib open Base open Extra
open Timed
open Common open Debug
open Term
open Sig_state
(** Logging function for printing. *)
let log_prnt = Logger.make 'p' "prnt" "pretty-printing"
let log_prnt = log_prnt.pp
(** Current signature state. *)
let sig_state : sig_state ref = ref Sig_state.dummy
(** [notation_of s] returns the notation of symbol [s] or [None]. *)
let notation_of : sym -> float Sign.notation option = fun s ->
SymMap.find_opt s !sig_state.notations
(** Flag for printing the domains of λ-abstractions. *)
let print_domains : bool ref = Console.register_flag "print_domains" false
(** Flag for printing implicit arguments. *)
let print_implicits : bool ref = Console.register_flag "print_implicits" false
(** Flag for printing the type of uninstanciated metavariables. Remark: this
does not generate parsable terms; use for debug only. *)
let print_meta_types : bool ref =
Console.register_flag "print_meta_types" false
(** Flag for printing contexts in unification problems. *)
let print_contexts : bool ref = Console.register_flag "print_contexts" false
(** Flag for printing metavariable arguments. *)
let print_meta_args : bool ref = Console.register_flag "print_meta_args" false
let assoc : Pratter.associativity pp = fun ppf assoc ->
match assoc with
| Neither -> ()
| Left -> out ppf " left"
| Right -> out ppf " right"
let notation : 'a pp -> 'a Sign.notation pp = fun elt ->
let rec notation ppf = function
| Sign.Prefix(p) -> out ppf "prefix %a" elt p
| Infix(a,p) -> out ppf "infix%a %a" assoc a elt p
| Postfix(p) -> out ppf "postfix %a" elt p
| Succ (Some n) -> notation ppf n
| Quant -> out ppf "quantifier"
| _ -> ()
in notation
let uid : string pp = string
let path : Path.t pp = Path.pp
let prop : prop pp = fun ppf p ->
match p with
| AC true -> out ppf "left associative commutative "
| AC false -> out ppf "associative commutative "
| Assoc true -> out ppf "left associative "
| Assoc false -> out ppf "associative "
| Const -> out ppf "constant "
| Commu -> out ppf "commutative "
| Defin -> ()
| Injec -> out ppf "injective "
let expo : expo pp = fun ppf e ->
match e with
| Privat -> out ppf "private "
| Protec -> out ppf "protected "
| Public -> ()
let match_strat : match_strat pp = fun ppf s ->
match s with
| Eager -> ()
| Sequen -> out ppf "sequential "
let do_not_qualify = ref false
let without_qualifying f =
let saved = !do_not_qualify in
do_not_qualify := true ;
let res = f () in
do_not_qualify := saved ;
res
let sym : sym pp = fun ppf s ->
if !print_implicits && s.sym_impl <> [] then out ppf "@";
let ss = !sig_state and n = s.sym_name and p = s.sym_path in
if !do_not_qualify || Path.Set.mem p ss.open_paths then uid ppf n
else
match Path.Map.find_opt p ss.path_alias with
| None ->
if n <> "" && let c = n.[0] in c = '$' || c = '?' then uid ppf n
else out ppf "%a.%a" path p uid n
| Some alias -> out ppf "%a.%a" uid alias uid n
let var : 'a Bindlib.var pp = fun ppf x -> uid ppf (Bindlib.name_of x)
(** Exception raised when trying to convert a term into a nat. *)
exception Not_a_nat
let builtin name =
try StrMap.find name (!sig_state).builtins with Not_found -> raise Not_a_nat
(** [nat_of_term t] converts a term into a natural number.
@raise Not_a_nat if this is not possible. *)
let nat_of_term : term -> int = fun t ->
let zero = builtin "nat_zero" and succ = builtin "nat_succ" in
let rec nat acc = fun t ->
match get_args t with
| (Symb s, [u]) when s == succ -> nat (acc+1) u
| (Symb s, []) when s == zero -> acc
| _ -> raise Not_a_nat
in nat 0 t
(** [pos_of_term t] converts a term into a positive number.
@raise Not_a_nat if this is not possible. *)
let pos_of_term : term -> int = fun t ->
let one = builtin "pos_one" and dbl = builtin "pos_double"
and suc_dbl = builtin "pos_succ_double" in
let rec pos acc = fun t ->
match get_args t with
| (Symb s, [u]) when s == dbl -> pos (2*acc) u
| (Symb s, [u]) when s == suc_dbl -> pos (2*acc+1) u
| (Symb s, []) when s == one -> acc
| _ -> raise Not_a_nat
in pos 1 t
(** [int_of_term t] converts a term into a positive number.
@raise Not_a_nat if this is not possible. *)
let int_of_term : term -> int = fun t ->
let zero = builtin "int_zero" and pos = builtin "int_positive"
and neg = builtin "int_negative" in
match get_args t with
| (Symb s, [u]) when s == pos -> pos_of_term u
| (Symb s, [u]) when s == neg -> - (pos_of_term u)
| (Symb s, []) when s == zero -> 0
| _ -> raise Not_a_nat
(** [are_quant_args args] returns [true] iff [args] has only one argument
that is an abstraction. *)
let are_quant_args : term list -> bool = fun args ->
match args with
| [b] -> is_abst b
| _ -> false
(** The possible priority levels are [`Func] (top level, including abstraction
and product), [`Appl] (application) and [`Atom] (smallest priority). *)
type priority = [`Func | `Appl | `Atom]
let rec meta : meta pp = fun ppf m ->
if !print_meta_types then
out ppf "(?%d:%a)" m.meta_key term !(m.meta_type)
else out ppf "?%d" m.meta_key
and typ : term pp = fun ppf a ->
if !print_domains then out ppf ": %a" term a
and term : term pp = fun ppf t ->
let rec atom ppf t = pp `Atom ppf t
and appl ppf t = pp `Appl ppf t
and func ppf t = pp `Func ppf t
and pp p ppf t =
let (h, args) = get_args t in
let pp_appl h args =
match args with
| [] -> head (p <> `Func) ppf h
| args ->
if p = `Atom then out ppf "(";
head true ppf h;
List.iter (out ppf " %a" atom) args;
if p = `Atom then out ppf ")"
in
let postfix h s args =
match args with
| l::args ->
if p <> `Func then out ppf "(";
if args = []
then out ppf "%a %a" appl l sym s
else out ppf "(%a %a)" appl l sym s;
List.iter (out ppf " %a" appl) args;
if p <> `Func then out ppf ")"
| [] ->
out ppf "("; head true ppf h; out ppf ")"
in
match h with
| Symb(s) ->
if !print_implicits && s.sym_impl <> [] then pp_appl h args
else
let number f t =
try out ppf "%i" (f t) with Not_a_nat -> pp_appl h args in
let args = LibTerm.remove_impl_args s args in
begin match notation_of s with
| Some Quant when are_quant_args args ->
if p <> `Func then out ppf "(";
quantifier s args;
if p <> `Func then out ppf ")"
| Some (Postfix _) -> postfix h s args
| Some (Infix _) ->
begin
match args with
| l::r::args ->
if p <> `Func then out ppf "(";
if args = []
then out ppf "%a %a %a" appl l sym s appl r
else out ppf "(%a %a %a)" appl l sym s appl r;
List.iter (out ppf " %a" appl) args;
if p <> `Func then out ppf ")"
| [] ->
out ppf "("; head true ppf h; out ppf ")"
| _ ->
if p = `Atom then out ppf "(";
out ppf "("; head true ppf h; out ppf ")";
List.iter (out ppf " %a" atom) args;
if p = `Atom then out ppf ")"
end
| Some (Zero|IntZero) -> out ppf "0"
| Some (Succ (Some (Postfix _))) ->
(try out ppf "%i" (nat_of_term t)
with Not_a_nat -> postfix h s args)
| Some (Succ _) -> number nat_of_term t
| Some PosOne -> out ppf "1"
| Some (PosDouble|PosSuccDouble) -> number pos_of_term t
| Some (IntPos|IntNeg) -> number int_of_term t
| _ -> pp_appl h args
end
| _ -> pp_appl h args
and quantifier s args =
match args with
| [b] ->
begin
match unfold b with
| Abst(a,b) ->
let (x,p) = Bindlib.unbind b in
out ppf "`%a %a%a, %a" sym s var x typ a func p
| _ -> assert false
end
| _ -> assert false
and head wrap ppf t =
let env ppf ts =
if Array.length ts > 0 then out ppf ".[%a]" (Array.pp func ";") ts in
let term_env ppf te =
match te with
| TE_Vari(m) -> var ppf m
| _ -> assert false
in
match unfold t with
| Appl(_,_) -> assert false
| Wild -> out ppf "_"
| TRef(r) ->
(match !r with
| None -> out ppf "<TRef>"
| Some t -> atom ppf t)
| Vari(x) -> var ppf x
| Type -> out ppf "TYPE"
| Kind -> out ppf "KIND"
| Symb(s) -> sym ppf s
| Meta(m,e) ->
if !print_meta_args then out ppf "%a%a" meta m env e else meta ppf m
| Plac(_) -> out ppf "_"
| Patt(_,n,e) -> out ppf "$%a%a" uid n env e
| TEnv(t,e) -> out ppf "$%a%a" term_env t env e
| Abst(a,b) ->
if wrap then out ppf "(";
let (x,t) = Bindlib.unbind b in
out ppf "λ %a" bvar (b,x);
if !print_domains then out ppf ": %a, %a" func a func t
else abstractions ppf t;
if wrap then out ppf ")"
| Prod(a,b) ->
if wrap then out ppf "(";
let (x,t) = Bindlib.unbind b in
if Bindlib.binder_occur b then
out ppf "Π %a: %a, %a" var x appl a func t
else out ppf "%a → %a" appl a func t;
if wrap then out ppf ")"
| LLet(a,t,b) ->
if wrap then out ppf "(";
out ppf "let ";
let (x,u) = Bindlib.unbind b in
bvar ppf (b,x);
if !print_domains then out ppf ": %a" atom a;
out ppf " ≔ %a in %a" func t func u;
if wrap then out ppf ")"
and bvar ppf (b,x) =
if Bindlib.binder_occur b then out ppf "%a" var x else out ppf "_"
and abstractions ppf t =
match unfold t with
| Abst(_,b) ->
let (x,t) = Bindlib.unbind b in
out ppf " %a%a" bvar (b,x) abstractions t
| t -> out ppf ", %a" func t
in
func ppf t
let term : term pp = fun ppf t -> term ppf (cleanup t)
let term_in : Bindlib.ctxt -> term pp = fun c ppf t ->
term ppf (cleanup ~ctxt:c t)
let rec prod : (term * bool list) pp = fun ppf (t, impl) ->
match unfold t, impl with
| Prod(a,b), true::impl ->
let x, b = Bindlib.unbind b in
out ppf "Π [%a: %a], %a" var x term a prod (b, impl)
| Prod(a,b), false::impl ->
let x, b = Bindlib.unbind b in
out ppf "Π %a: %a, %a" var x term a prod (b, impl)
| _ -> term ppf t
let sym_rule : sym_rule pp = fun ppf r ->
out ppf "%a ↪ %a" term (lhs r) term (rhs r)
let rule_of : sym -> rule pp = fun s ppf r -> sym_rule ppf (s,r)
let unif_rule : rule pp = rule_of Unif_rule.equiv
let rules_of : sym pp = fun ppf s -> D.list (rule_of s) ppf !(s.sym_rules)
let ctxt : ctxt pp = fun ppf ctx ->
if !print_contexts then
begin
let def ppf t = out ppf " ≔ %a" term t in
let decl ppf (x,a,t) = out ppf "%a%a%a" var x typ a (Option.pp def) t in
out ppf "%a%s⊢ "
(List.pp decl ", ") (List.rev ctx)
(if ctx <> [] then " " else "")
end
let typing : constr pp = fun ppf (ctx, t, u) ->
out ppf "@[<h>%a%a : %a@]" ctxt ctx term t term u
let constr : constr pp = fun ppf (ctx, t, u) ->
out ppf "@[<h>%a%a ≡ %a@]" ctxt ctx term t term u
let constrs : constr list pp = List.pp constr "; "
let metaset : MetaSet.t pp =
D.iter ~sep:(fun fmt () -> out fmt ",@ ") MetaSet.iter meta
let problem : problem pp = fun ppf p ->
out ppf
"{ recompute=%b;@ metas={%a};@ to_solve=[%a];@ unsolved=[%a] }"
!p.recompute metaset !p.metas constrs !p.to_solve constrs
!p.unsolved