1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* Changed by (and thus parts copyright ©) by Lionel Elie Mamane <lionel@mamane.lu>
10
* on May-June 2006 for implementation of abstraction of pretty-printing of objects.
13
(* $Id: prettyp.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
37
print_inductive : mutual_inductive -> std_ppcmds;
38
print_constant_with_infos : constant -> std_ppcmds;
39
print_section_variable : variable -> std_ppcmds;
40
print_syntactic_def : kernel_name -> std_ppcmds;
41
print_module : bool -> Names.module_path -> std_ppcmds;
42
print_modtype : module_path -> std_ppcmds;
43
print_named_decl : identifier * constr option * types -> std_ppcmds;
44
print_leaf_entry : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds;
45
print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option;
46
print_context : bool -> int option -> Lib.library_segment -> std_ppcmds;
47
print_typed_value_in_env : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds;
48
print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds;
51
let gallina_print_module = print_module
52
let gallina_print_modtype = print_modtype
54
(*********************)
57
let print_basename sp = pr_global (ConstRef sp)
59
let print_closed_sections = ref false
61
let with_line_skip p = if ismt p then mt() else (fnl () ++ p)
63
(********************************)
64
(** Printing implicit arguments *)
66
let conjugate_to_be = function [_] -> "is" | _ -> "are"
68
let pr_implicit imp = pr_id (name_of_implicit imp)
70
let print_impl_args_by_name max = function
73
hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++
74
prlist_with_sep pr_coma pr_implicit impls ++ spc() ++
75
str (conjugate_to_be impls) ++ str" implicit" ++
76
(if max then strbrk " and maximally inserted" else mt())) ++ fnl()
78
let print_impl_args l =
79
let imps = List.filter is_status_implicit l in
80
let maximps = List.filter Impargs.maximal_insertion_of imps in
81
let nonmaximps = list_subtract imps maximps in
82
print_impl_args_by_name false nonmaximps ++
83
print_impl_args_by_name true maximps
85
(*********************)
86
(** Printing Scopes *)
88
let print_ref reduce ref =
89
let typ = Global.type_of_global ref in
92
let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ
93
in it_mkProd_or_LetIn ccl ctx
95
hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ) ++ fnl ()
97
let print_argument_scopes = function
98
| [Some sc] -> str"Argument scope is [" ++ str sc ++ str"]" ++ fnl()
99
| l when not (List.for_all ((=) None) l) ->
100
hov 2 (str"Argument scopes are" ++ spc() ++
102
prlist_with_sep spc (function Some sc -> str sc | None -> str "_") l ++
106
let need_expansion impl ref =
107
let typ = Global.type_of_global ref in
108
let ctx = fst (decompose_prod_assum typ) in
109
let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in
110
impl <> [] & List.length impl >= nprods &
111
let _,lastimpl = list_chop nprods impl in
112
List.filter is_status_implicit lastimpl <> []
116
| TransparentMaybeOpacified of Conv_oracle.level
118
let opacity env = function
119
| VarRef v when pi2 (Environ.lookup_named v env) <> None ->
120
Some(TransparentMaybeOpacified (Conv_oracle.get_strategy(VarKey v)))
122
let cb = Environ.lookup_constant cst env in
123
if cb.const_body = None then None
124
else if cb.const_opaque then Some FullyOpaque
126
(TransparentMaybeOpacified (Conv_oracle.get_strategy(ConstKey cst)))
129
let print_opacity ref =
130
match opacity (Global.env()) ref with
132
| Some s -> pr_global ref ++ str " is " ++
134
| FullyOpaque -> "opaque"
135
| TransparentMaybeOpacified Conv_oracle.Opaque ->
136
"basically transparent but considered opaque for reduction"
137
| TransparentMaybeOpacified lev when lev = Conv_oracle.transparent ->
139
| TransparentMaybeOpacified (Conv_oracle.Level n) ->
140
"transparent (with expansion weight "^string_of_int n^")"
141
| TransparentMaybeOpacified Conv_oracle.Expand ->
142
"transparent (with minimal expansion weight)") ++ fnl()
144
let print_name_infos ref =
145
let impl = implicits_of_global ref in
146
let scopes = Notation.find_arguments_scope ref in
147
let type_for_implicit =
148
if need_expansion impl ref then
149
(* Need to reduce since implicits are computed with products flattened *)
150
str "Expanded type for implicit arguments" ++ fnl () ++
151
print_ref true ref ++ fnl()
153
type_for_implicit ++ print_impl_args impl ++ print_argument_scopes scopes
155
let print_id_args_data test pr id l =
156
if List.exists test l then
157
str"For " ++ pr_id id ++ str": " ++ pr l
161
let print_args_data_of_inductive_ids get test pr sp mipv =
164
print_id_args_data test pr mip.mind_typename (get (IndRef (sp,i))) ++
167
print_id_args_data test pr idc (get (ConstructRef ((sp,i),j+1))))
171
let print_inductive_implicit_args =
172
print_args_data_of_inductive_ids
173
implicits_of_global is_status_implicit print_impl_args
175
let print_inductive_argument_scopes =
176
print_args_data_of_inductive_ids
177
Notation.find_arguments_scope ((<>) None) print_argument_scopes
179
(*********************)
180
(* "Locate" commands *)
183
| Term of global_reference
184
| Dir of global_dir_reference
185
| Syntactic of kernel_name
186
| ModuleType of qualid * module_path
187
| Undefined of qualid
189
let locate_any_name ref =
190
let module N = Nametab in
191
let (loc,qid) = qualid_of_reference ref in
192
try Term (N.locate qid)
194
try Syntactic (N.locate_syntactic_definition qid)
196
try Dir (N.locate_dir qid)
198
try ModuleType (qid, N.locate_modtype qid)
199
with Not_found -> Undefined qid
201
let pr_located_qualid = function
203
let ref_str = match ref with
204
ConstRef _ -> "Constant"
205
| IndRef _ -> "Inductive"
206
| ConstructRef _ -> "Constructor"
207
| VarRef _ -> "Variable" in
208
str ref_str ++ spc () ++ pr_sp (Nametab.sp_of_global ref)
210
str "Notation" ++ spc () ++ pr_sp (Nametab.sp_of_syntactic_definition kn)
212
let s,dir = match dir with
213
| DirOpenModule (dir,_) -> "Open Module", dir
214
| DirOpenModtype (dir,_) -> "Open Module Type", dir
215
| DirOpenSection (dir,_) -> "Open Section", dir
216
| DirModule (dir,_) -> "Module", dir
217
| DirClosedSection dir -> "Closed Section", dir
219
str s ++ spc () ++ pr_dirpath dir
220
| ModuleType (qid,_) ->
221
str "Module Type" ++ spc () ++ pr_sp (Nametab.full_name_modtype qid)
223
pr_qualid qid ++ spc () ++ str "not a defined object."
225
let print_located_qualid ref =
226
let (loc,qid) = qualid_of_reference ref in
227
let module N = Nametab in
228
let expand = function
230
Term ref, N.shortest_qualid_of_global Idset.empty ref
232
Syntactic kn, N.shortest_qualid_of_syndef Idset.empty kn in
233
match List.map expand (N.extended_locate_all qid) with
235
let (dir,id) = repr_qualid qid in
236
if dir = empty_dirpath then
237
str "No object of basename " ++ pr_id id
239
str "No object of suffix " ++ pr_qualid qid
243
hov 2 (pr_located_qualid o ++
245
spc() ++ str "(shorter name to refer to it in current context is " ++ pr_qualid oqid ++ str")"
249
(******************************************)
250
(**** Printing declarations and judgments *)
251
(**** Gallina layer *****)
253
let gallina_print_typed_value_in_env env (trm,typ) =
254
(pr_lconstr_env env trm ++ fnl () ++
255
str " : " ++ pr_ltype_env env typ ++ fnl ())
257
(* To be improved; the type should be used to provide the types in the
258
abstractions. This should be done recursively inside pr_lconstr, so that
259
the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u)
260
synthesizes the type nat of the abstraction on u *)
262
let print_named_def name body typ =
263
let pbody = pr_lconstr body in
264
let ptyp = pr_ltype typ in
265
let pbody = if isCast body then surround pbody else pbody in
266
(str "*** [" ++ str name ++ str " " ++
267
hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++
268
str ":" ++ brk (1,2) ++ ptyp) ++
271
let print_named_assum name typ =
272
str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]"
274
let gallina_print_named_decl (id,c,typ) =
275
let s = string_of_id id in
277
| Some body -> print_named_def s body typ
278
| None -> print_named_assum s typ
280
let assumptions_for_print lna =
281
List.fold_right (fun na env -> add_name na env) lna empty_names_context
283
(*********************)
286
let print_params env params =
287
if params = [] then mt () else pr_rel_context env params ++ brk(1,2)
289
let print_constructors envpar names types =
291
prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
292
(fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar c)
293
(Array.to_list (array_map2 (fun n t -> (n,t)) names types))
297
let build_inductive sp tyi =
298
let (mib,mip) = Global.lookup_inductive (sp,tyi) in
299
let params = mib.mind_params_ctxt in
300
let args = extended_rel_list 0 params in
301
let env = Global.env() in
302
let fullarity = match mip.mind_arity with
303
| Monomorphic ar -> ar.mind_user_arity
305
it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt in
306
let arity = hnf_prod_applist env fullarity args in
307
let cstrtypes = type_of_constructors env (sp,tyi) in
309
Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
310
let cstrnames = mip.mind_consnames in
311
(IndRef (sp,tyi), params, arity, cstrnames, cstrtypes)
313
let print_one_inductive (sp,tyi) =
314
let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
315
let env = Global.env () in
316
let envpar = push_rel_context params env in
318
pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++ print_params env params ++
319
str ": " ++ pr_lconstr_env envpar arity ++ str " :=") ++
320
brk(0,2) ++ print_constructors envpar cstrnames cstrtypes
322
let pr_mutual_inductive finite indl =
324
str (if finite then "Inductive " else "CoInductive ") ++
325
prlist_with_sep (fun () -> fnl () ++ str" with ")
326
print_one_inductive indl)
329
let rec prodec_rec l subst c =
330
match kind_of_term c with
332
let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
333
prodec_rec ((id,true,substl subst t)::l) (mkVar id::subst) c
334
| LetIn (na,b,_,c) ->
335
let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
336
prodec_rec ((id,false,substl subst b)::l) (mkVar id::subst) c
341
let pr_record (sp,tyi) =
342
let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
343
let env = Global.env () in
344
let envpar = push_rel_context params env in
345
let fields = get_fields cstrtypes.(0) in
348
str "Record " ++ pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++
349
print_params env params ++
350
str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++
351
str ":= " ++ pr_id cstrnames.(0)) ++
354
prlist_with_sep (fun () -> str ";" ++ brk(1,0))
356
str " " ++ pr_id id ++ str (if b then " : " else " := ") ++
357
pr_lconstr_env envpar c) fields) ++ str" }")
359
let gallina_print_inductive sp =
360
let (mib,mip) = Global.lookup_inductive (sp,0) in
361
let mipv = mib.mind_packets in
362
let names = list_tabulate (fun x -> (sp,x)) (Array.length mipv) in
363
(if mib.mind_record & not !Flags.raw_print then
364
pr_record (List.hd names)
366
pr_mutual_inductive mib.mind_finite names) ++ fnl () ++
368
(print_inductive_implicit_args sp mipv ++
369
print_inductive_argument_scopes sp mipv)
371
let print_named_decl id =
372
gallina_print_named_decl (Global.lookup_named id) ++ fnl ()
374
let gallina_print_section_variable id =
375
print_named_decl id ++
376
with_line_skip (print_name_infos (VarRef id))
378
let print_body = function
379
| Some lc -> pr_lconstr (Declarations.force lc)
380
| None -> (str"<no body>")
382
let print_typed_body (val_0,typ) =
383
(print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ)
385
let ungeneralized_type_of_constant_type = function
386
| PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
387
| NonPolymorphicType t -> t
389
let print_constant with_values sep sp =
390
let cb = Global.lookup_constant sp in
391
let val_0 = cb.const_body in
392
let typ = ungeneralized_type_of_constant_type cb.const_type in
397
print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++
400
print_basename sp ++ str sep ++ cut () ++
401
(if with_values then print_typed_body (val_0,typ) else pr_ltype typ))
404
let gallina_print_constant_with_infos sp =
405
print_constant true " = " sp ++
406
with_line_skip (print_name_infos (ConstRef sp))
408
let gallina_print_syntactic_def kn =
410
and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
411
and (vars,a) = Syntax_def.search_syntactic_definition dummy_loc kn in
412
let c = Topconstr.rawconstr_of_aconstr dummy_loc a in
413
str "Notation " ++ pr_qualid qid ++
414
prlist_with_sep spc pr_id (List.map fst vars) ++ str sep ++
415
Constrextern.without_symbols pr_lrawconstr c ++ fnl ()
417
let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
418
let sep = if with_values then " = " else " : "
419
and tag = object_tag lobj in
420
match (oname,tag) with
422
(* Outside sections, VARIABLES still exist but only with universes
424
(try Some(print_named_decl (basename sp)) with Not_found -> None)
426
Some (print_constant with_values sep (constant_of_kn kn))
428
Some (gallina_print_inductive kn)
430
let (mp,_,l) = repr_kn kn in
431
Some (print_module with_values (MPdot (mp,l)))
432
| (_,"MODULE TYPE") ->
433
let (mp,_,l) = repr_kn kn in
434
Some (print_modtype (MPdot (mp,l)))
435
| (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
436
"COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None
437
(* To deal with forgotten cases... *)
440
let gallina_print_library_entry with_values ent =
441
let pr_name (sp,_) = pr_id (basename sp) in
443
| (oname,Lib.Leaf lobj) ->
444
gallina_print_leaf_entry with_values (oname,lobj)
445
| (oname,Lib.OpenedSection (dir,_)) ->
446
Some (str " >>>>>>> Section " ++ pr_name oname)
447
| (oname,Lib.ClosedSection _) ->
448
Some (str " >>>>>>> Closed Section " ++ pr_name oname)
449
| (_,Lib.CompilingLibrary (dir,_)) ->
450
Some (str " >>>>>>> Library " ++ pr_dirpath dir)
451
| (oname,Lib.OpenedModule _) ->
452
Some (str " >>>>>>> Module " ++ pr_name oname)
453
| (oname,Lib.ClosedModule _) ->
454
Some (str " >>>>>>> Closed Module " ++ pr_name oname)
455
| (oname,Lib.OpenedModtype _) ->
456
Some (str " >>>>>>> Module Type " ++ pr_name oname)
457
| (oname,Lib.ClosedModtype _) ->
458
Some (str " >>>>>>> Closed Module Type " ++ pr_name oname)
459
| (_,Lib.FrozenState _) ->
462
let gallina_print_leaf_entry with_values c =
463
match gallina_print_leaf_entry with_values c with
465
| Some pp -> pp ++ fnl()
467
let gallina_print_context with_values =
468
let rec prec n = function
469
| h::rest when n = None or Option.get n > 0 ->
470
(match gallina_print_library_entry with_values h with
471
| None -> prec n rest
472
| Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ())
477
let gallina_print_eval red_fun env evmap _ {uj_val=trm;uj_type=typ} =
478
let ntrm = red_fun env evmap trm in
479
(str " = " ++ gallina_print_typed_value_in_env env (ntrm,typ))
481
(******************************************)
482
(**** Printing abstraction layer *)
484
let default_object_pr = {
485
print_inductive = gallina_print_inductive;
486
print_constant_with_infos = gallina_print_constant_with_infos;
487
print_section_variable = gallina_print_section_variable;
488
print_syntactic_def = gallina_print_syntactic_def;
489
print_module = gallina_print_module;
490
print_modtype = gallina_print_modtype;
491
print_named_decl = gallina_print_named_decl;
492
print_leaf_entry = gallina_print_leaf_entry;
493
print_library_entry = gallina_print_library_entry;
494
print_context = gallina_print_context;
495
print_typed_value_in_env = gallina_print_typed_value_in_env;
496
print_eval = gallina_print_eval;
499
let object_pr = ref default_object_pr
500
let set_object_pr = (:=) object_pr
502
let print_inductive x = !object_pr.print_inductive x
503
let print_constant_with_infos c = !object_pr.print_constant_with_infos c
504
let print_section_variable c = !object_pr.print_section_variable c
505
let print_syntactic_def x = !object_pr.print_syntactic_def x
506
let print_module x = !object_pr.print_module x
507
let print_modtype x = !object_pr.print_modtype x
508
let print_named_decl x = !object_pr.print_named_decl x
509
let print_leaf_entry x = !object_pr.print_leaf_entry x
510
let print_library_entry x = !object_pr.print_library_entry x
511
let print_context x = !object_pr.print_context x
512
let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x
513
let print_eval x = !object_pr.print_eval x
515
(******************************************)
516
(**** Printing declarations and judgments *)
517
(**** Abstract layer *****)
519
let print_typed_value x = print_typed_value_in_env (Global.env ()) x
521
let print_judgment env {uj_val=trm;uj_type=typ} =
522
print_typed_value_in_env env (trm, typ)
524
let print_safe_judgment env j =
525
let trm = Safe_typing.j_val j in
526
let typ = Safe_typing.j_type j in
527
print_typed_value_in_env env (trm, typ)
529
(*********************)
532
let print_full_context () =
533
print_context true None (Lib.contents_after None)
535
let print_full_context_typ () =
536
print_context false None (Lib.contents_after None)
538
let print_full_pure_context () =
539
let rec prec = function
540
| ((_,kn),Lib.Leaf lobj)::rest ->
541
let pp = match object_tag lobj with
543
let con = constant_of_kn kn in
544
let cb = Global.lookup_constant con in
545
let val_0 = cb.const_body in
546
let typ = ungeneralized_type_of_constant_type cb.const_type in
550
str (if cb.const_opaque then "Axiom " else "Parameter ") ++
551
print_basename con ++ str " : " ++ cut () ++ pr_ltype typ
553
if cb.const_opaque then
554
str "Theorem " ++ print_basename con ++ cut () ++
555
str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++
556
str "Proof " ++ print_body val_0
558
str "Definition " ++ print_basename con ++ cut () ++
559
str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++
560
print_body val_0) ++ str "." ++ fnl () ++ fnl ()
562
let (mib,mip) = Global.lookup_inductive (kn,0) in
563
let mipv = mib.mind_packets in
564
let names = list_tabulate (fun x -> (kn,x)) (Array.length mipv) in
565
pr_mutual_inductive mib.mind_finite names ++ str "." ++
568
(* TODO: make it reparsable *)
569
let (mp,_,l) = repr_kn kn in
570
print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
572
(* TODO: make it reparsable *)
573
(* TODO: make it reparsable *)
574
let (mp,_,l) = repr_kn kn in
575
print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()
578
| _::rest -> prec rest
580
prec (Lib.contents_after None)
582
(* For printing an inductive definition with
583
its constructors and elimination,
584
assume that the declaration of constructors and eliminations
585
follows the definition of the inductive type *)
587
let list_filter_vec f vec =
590
else if f vec.(n) then
591
frec (n-1) (vec.(n)::lf)
595
frec (Array.length vec -1) []
597
(* This is designed to print the contents of an opened section *)
598
let read_sec_context r =
599
let loc,qid = qualid_of_reference r in
601
try Nametab.locate_section qid
603
user_err_loc (loc,"read_sec_context", str "Unknown section.") in
604
let rec get_cxt in_cxt = function
605
| (_,Lib.OpenedSection ((dir',_),_) as hd)::rest ->
606
if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
607
| (_,Lib.ClosedSection _)::rest ->
608
error "Cannot print the contents of a closed section."
609
(* LEM: Actually, we could if we wanted to. *)
611
| hd::rest -> get_cxt (hd::in_cxt) rest
613
let cxt = (Lib.contents_after None) in
614
List.rev (get_cxt [] cxt)
616
let print_sec_context sec =
617
print_context true None (read_sec_context sec)
619
let print_sec_context_typ sec =
620
print_context false None (read_sec_context sec)
623
match locate_any_name ref with
624
| Term (ConstRef sp) -> print_constant_with_infos sp
625
| Term (IndRef (sp,_)) -> print_inductive sp
626
| Term (ConstructRef ((sp,_),_)) -> print_inductive sp
627
| Term (VarRef sp) -> print_section_variable sp
628
| Syntactic kn -> print_syntactic_def kn
629
| Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
631
| ModuleType (_,kn) -> print_modtype kn
633
try (* Var locale de but, pas var de section... donc pas d'implicits *)
634
let dir,str = repr_qualid qid in
635
if (repr_dirpath dir) <> [] then raise Not_found;
636
let (_,c,typ) = Global.lookup_named str in
637
(print_named_decl (str,c,typ))
640
let sp = Nametab.locate_obj qid in
643
List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None)
646
| Lib.Leaf obj -> (oname,obj)
647
| _ -> raise Not_found
649
print_leaf_entry true (oname,lobj)
652
"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
654
let print_opaque_name qid =
655
let env = Global.env () in
656
match global qid with
658
let cb = Global.lookup_constant cst in
659
if cb.const_body <> None then
660
print_constant_with_infos cst
662
error "Not a defined constant."
665
| ConstructRef cstr ->
666
let ty = Inductiveops.type_of_constructor env cstr in
667
print_typed_value (mkConstruct cstr, ty)
669
let (_,c,ty) = lookup_named id env in
670
print_named_decl (id,c,ty)
672
let print_about ref =
673
let k = locate_any_name ref in
676
print_ref false ref ++ fnl () ++ print_name_infos ref ++
679
print_syntactic_def kn
680
| Dir _ | ModuleType _ | Undefined _ ->
683
hov 0 (str "Expands to: " ++ pr_located_qualid k)
685
let print_impargs ref =
686
let ref = Nametab.global ref in
687
let impl = implicits_of_global ref in
688
let has_impl = List.filter is_status_implicit impl <> [] in
689
(* Need to reduce since implicits are computed with products flattened *)
690
print_ref (need_expansion impl ref) ref ++ fnl() ++
691
(if has_impl then print_impl_args impl
692
else (str "No implicit arguments" ++ fnl ()))
694
let unfold_head_fconst =
695
let rec unfrec k = match kind_of_term k with
696
| Const cst -> constant_value (Global.env ()) cst
697
| Lambda (na,t,b) -> mkLambda (na,t,unfrec b)
698
| App (f,v) -> appvect (unfrec f,v)
705
print_context false (Some depth) (Lib.contents_after None)
708
(*************************************************************************)
709
(* Pretty-printing functions coming from classops.ml *)
713
let print_coercion_value v = pr_lconstr (get_coercion_value v)
716
let cl,_ = class_info_from_index i in
719
let print_path ((i,j),p) =
721
str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++
723
print_class i ++ str" >-> " ++ print_class j
725
let _ = Classops.install_path_printer print_path
728
prlist_with_sep pr_fnl print_path (inheritance_graph())
730
let print_classes () =
731
prlist_with_sep pr_spc pr_class (classes())
733
let print_coercions () =
734
prlist_with_sep pr_spc print_coercion_value (coercions())
736
let index_of_class cl =
740
errorlabstrm "index_of_class"
741
(pr_class cl ++ spc() ++ str "not a defined class.")
743
let print_path_between cls clt =
744
let i = index_of_class cls in
745
let j = index_of_class clt in
748
lookup_path_between_class (i,j)
750
errorlabstrm "index_cl_of_id"
751
(str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
756
let pr_cs_pattern = function
757
Const_cs c -> pr_global c
758
| Prod_cs -> str "_ -> _"
759
| Default_cs -> str "_"
760
| Sort_cs s -> pr_sort_family s
762
let print_canonical_projections () =
763
prlist_with_sep pr_fnl
764
(fun ((r1,r2),o) -> pr_cs_pattern r2 ++
766
pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )")
767
(canonical_projections ())
769
(*************************************************************************)
771
(*************************************************************************)
772
(* Pretty-printing functions for type classes *)
776
let pr_typeclass env t =
777
print_ref false t.cl_impl
779
let print_typeclasses () =
780
let env = Global.env () in
781
prlist_with_sep fnl (pr_typeclass env) (typeclasses ())
783
let pr_instance env i =
784
(* gallina_print_constant_with_infos i.is_impl *)
786
print_ref false (ConstRef (instance_impl i))
788
let print_all_instances () =
789
let env = Global.env () in
790
let inst = all_instances () in
791
prlist_with_sep fnl (pr_instance env) inst
793
let print_instances r =
794
let env = Global.env () in
795
let inst = instances r in
796
prlist_with_sep fnl (pr_instance env) inst
added
removed
parsing/prettyp.ml
