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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Format
open Cic
open Names
let chk_pp fmt = Pp.pp_with fmt
let pp_arrayi pp fmt a = Array.iteri (fun i x -> pp fmt (i,x)) a
let pp_instance fmt i = chk_pp fmt (Univ.Instance.pr i)
let pp_id fmt id = fprintf fmt "%s" (Id.to_string id)
let print_pure_constr fmt csr =
let rec pp_term fmt c = match c with
| Rel n -> fprintf fmt "#%d" n
| Meta n -> fprintf fmt "Meta(%d)" n
| Var id -> pp_id fmt id
| Sort s -> pp_sort fmt s
| Cast (c,_, t) ->
fprintf fmt "@[<hov 1>(%a@;::%a)@]" pp_term c pp_term t
| Prod (Name(id),t,c) ->
fprintf fmt "@[<hov 1>(%a:%a)@;@[%a@]@]" pp_id id pp_term t pp_term c
| Prod (Anonymous,t,c) ->
fprintf fmt "(%a@,->@[%a@])" pp_term t pp_term c
| Lambda (na,t,c) ->
fprintf fmt "[%a:@[%a@]]@,@[%a@]" pp_name na pp_term t pp_term c
| LetIn (na,b,t,c) ->
fprintf fmt "[%a=@[%a@]@,:@[%a@]]@,@[%a@]" pp_name na pp_term b pp_term t pp_term c
| App (c,l) ->
fprintf fmt "(@[%a@]@, @[<hov 1>%a@])" pp_term c (pp_arrayi (fun _ (_,s) -> fprintf fmt "@[%a@]@," pp_term s)) l;
| Evar _ -> pp_print_string fmt "Evar#"
| Const (c,u) ->
fprintf fmt "Cons(@[%a,%a@])" sp_con_display c pp_instance u
| Ind ((sp,i),u) ->
fprintf fmt "Ind(@[%a,%d,%a@])" sp_display sp i pp_instance u
| Construct (((sp,i),j),u) ->
fprintf fmt "Constr(%a,%d,%d,%a)" sp_display sp i j pp_instance u
| Case (ci,p,c,bl) ->
let pp_match fmt (_,mc) = fprintf fmt " @[%a@]" pp_term mc in
fprintf fmt "@[<v><@[%a@]>@,Case@ @[%a@]@ of@[<v>%a@]@,end@]" pp_term p pp_term c (pp_arrayi pp_match) bl
| Fix ((t,i),(lna,tl,bl)) ->
let pp_fixc fmt (k,_) =
fprintf fmt "@[<v 0> %a/%d@,:@[%a@]@,:=@[%a@]@]@," pp_name lna.(k) t.(k) pp_term tl.(k) pp_term bl.(k) in
fprintf fmt "Fix(%d)@,@[<v>{%a}@]" i (pp_arrayi pp_fixc) tl
| CoFix(i,(lna,tl,bl)) ->
let pp_fixc fmt (k,_) =
fprintf fmt "@[<v 0> %a@,:@[%a@]@,:=@[%a@]@]@," pp_name lna.(k) pp_term tl.(k) pp_term bl.(k) in
fprintf fmt "CoFix(%d)@,@[<v>{%a}@]" i (pp_arrayi pp_fixc) tl
| Proj (p, c) ->
fprintf fmt "Proj(%a,@,@[%a@])" sp_con_display (Projection.constant p) pp_term c
and pp_sort fmt = function
| Set -> pp_print_string fmt "Set"
| Prop -> pp_print_string fmt "Prop"
| Type u -> fprintf fmt "Type(%a)" chk_pp (Univ.pr_uni u)
and pp_name fmt = function
| Name id -> pp_id fmt id
| Anonymous -> pp_print_string fmt "_"
(* Remove the top names for library and Scratch to avoid long names *)
and sp_display fmt sp =
(* let dir,l = decode_kn sp in
let ls =
match List.rev_map Id.to_string (DirPath.repr dir) with
("Top"::l)-> l
| ("Coq"::_::l) -> l
| l -> l
in List.iter (fun x -> print_string x; print_string ".") ls;*)
pp_print_string fmt (MutInd.debug_to_string sp)
and sp_con_display fmt sp =
(*
let dir,l = decode_kn sp in
let ls =
match List.rev_map Id.to_string (DirPath.repr dir) with
("Top"::l)-> l
| ("Coq"::_::l) -> l
| l -> l
in List.iter (fun x -> print_string x; print_string ".") ls;*)
pp_print_string fmt (Constant.debug_to_string sp)
in
try
fprintf fmt "@[%a@]%!" pp_term csr
with e ->
pp_print_string fmt (Printexc.to_string e);
print_flush ();
raise e
|
