summaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
diff options
context:
space:
mode:
Diffstat (limited to 'dev/top_printers.ml')
-rw-r--r--dev/top_printers.ml147
1 files changed, 79 insertions, 68 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index d7d2f6d8..23701c23 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -28,10 +28,11 @@ open Cerrors
open Evd
open Goptions
open Genarg
+open Mod_subst
let _ = Constrextern.print_evar_arguments := true
-let _ = set_bool_option_value (SecondaryTable ("Printing","Matching")) false
+let _ = set_bool_option_value ["Printing";"Matching"] false
let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
(* std_ppcmds *)
@@ -40,13 +41,13 @@ let pppp x = pp x
(* name printers *)
let ppid id = pp (pr_id id)
let pplab l = pp (pr_lab l)
-let ppmsid msid = pp (str (debug_string_of_msid msid))
let ppmbid mbid = pp (str (debug_string_of_mbid mbid))
let ppdir dir = pp (pr_dirpath dir)
let ppmp mp = pp(str (string_of_mp mp))
-let ppcon con = pp(pr_con con)
+let ppcon con = pp(debug_pr_con con)
let ppkn kn = pp(pr_kn kn)
-let ppsp sp = pp(pr_sp sp)
+let ppmind kn = pp(debug_pr_mind kn)
+let ppsp sp = pp(pr_path sp)
let ppqualid qid = pp(pr_qualid qid)
let ppclindex cl = pp(Classops.pr_cl_index cl)
@@ -65,17 +66,30 @@ let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
let ppbigint n = pp (Bigint.pr_bigint n);;
-let prset pr l = str "[" ++ prlist_with_sep spc pr l ++ str "]"
+let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
let ppintset l = pp (prset int (Intset.elements l))
let ppidset l = pp (prset pr_id (Idset.elements l))
+let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
+let ppidmap pr l =
+ let pr (id,b) = pr_id id ++ str "=>" ++ pr id b in
+ pp (prset' pr (Idmap.fold (fun a b l -> (a,b)::l) l []))
+
+let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) ->
+ hov 0
+ (Termops.print_constr c ++
+ (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++
+ Termops.print_constr c ++ str">") ++
+ (if id = id0 then mt ()
+ else spc () ++ str "<canonical: " ++ pr_id id ++ str ">"))))
+
let pP s = pp (hov 0 s)
-let safe_pr_global = function
- | ConstRef kn -> pp (str "CONSTREF(" ++ pr_con kn ++ str ")")
- | IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++
+let safe_pr_global = function
+ | ConstRef kn -> pp (str "CONSTREF(" ++ debug_pr_con kn ++ str ")")
+ | IndRef (kn,i) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++
int i ++ str ")")
- | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++
+ | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++
int i ++ str "," ++ int j ++ str ")")
| VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")")
@@ -92,6 +106,7 @@ let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t)
let ppj j = pp (genppj pr_ljudge j)
let prsubst s = pp (Mod_subst.debug_pr_subst s)
+let prdelta s = pp (Mod_subst.debug_pr_delta s)
let pp_idpred s = pp (pr_idpred s)
let pp_cpred s = pp (pr_cpred s)
@@ -100,9 +115,9 @@ let pp_transparent_state s = pp (pr_transparent_state s)
(* proof printers *)
let ppmetas metas = pp(pr_metaset metas)
let ppevm evd = pp(pr_evar_map evd)
-let ppevd evd = pp(pr_evar_defs evd)
let ppclenv clenv = pp(pr_clenv clenv)
let ppgoal g = pp(db_pr_goal g)
+let pppftreestate p = pp(print_pftreestate p)
let pr_gls gls =
hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls))
@@ -134,7 +149,7 @@ let ppobj obj = Format.print_string (Libobject.object_tag obj)
let cnt = ref 0
-let cast_kind_display k =
+let cast_kind_display k =
match k with
| VMcast -> "VMcast"
| DEFAULTcast -> "DEFAULTcast"
@@ -145,7 +160,7 @@ let constr_display csr =
| Meta n -> "Meta("^(string_of_int n)^")"
| Var id -> "Var("^(string_of_id id)^")"
| Sort s -> "Sort("^(sort_display s)^")"
- | Cast (c,k, t) ->
+ | Cast (c,k, t) ->
"Cast("^(term_display c)^","^(cast_kind_display k)^","^(term_display t)^")"
| Prod (na,t,c) ->
"Prod("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n"
@@ -158,9 +173,9 @@ let constr_display csr =
| Evar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")"
| Const c -> "Const("^(string_of_con c)^")"
| Ind (sp,i) ->
- "MutInd("^(string_of_kn sp)^","^(string_of_int i)^")"
+ "MutInd("^(string_of_mind sp)^","^(string_of_int i)^")"
| Construct ((sp,i),j) ->
- "MutConstruct(("^(string_of_kn sp)^","^(string_of_int i)^"),"
+ "MutConstruct(("^(string_of_mind sp)^","^(string_of_int i)^"),"
^(string_of_int j)^")"
| Case (ci,p,c,bl) ->
"MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
@@ -212,25 +227,25 @@ let print_pure_constr csr =
print_string "::"; (term_display t); print_string ")"; close_box()
| Prod (Name(id),t,c) ->
open_hovbox 1;
- print_string"("; print_string (string_of_id id);
- print_string ":"; box_display t;
- print_string ")"; print_cut();
+ print_string"("; print_string (string_of_id id);
+ print_string ":"; box_display t;
+ print_string ")"; print_cut();
box_display c; close_box()
| Prod (Anonymous,t,c) ->
print_string"("; box_display t; print_cut(); print_string "->";
- box_display c; print_string ")";
+ box_display c; print_string ")";
| Lambda (na,t,c) ->
print_string "["; name_display na;
print_string ":"; box_display t; print_string "]";
- print_cut(); box_display c;
+ print_cut(); box_display c;
| LetIn (na,b,t,c) ->
- print_string "["; name_display na; print_string "=";
+ print_string "["; name_display na; print_string "=";
box_display b; print_cut();
print_string ":"; box_display t; print_string "]";
- print_cut(); box_display c;
- | App (c,l) ->
- print_string "(";
- box_display c;
+ print_cut(); box_display c;
+ | App (c,l) ->
+ print_string "(";
+ box_display c;
Array.iter (fun x -> print_space (); box_display x) l;
print_string ")"
| Evar (e,l) -> print_string "Evar#"; print_int e; print_string "{";
@@ -257,25 +272,25 @@ let print_pure_constr csr =
open_vbox 0;
Array.iter (fun x -> print_cut(); box_display x) bl;
close_box();
- print_cut();
- print_string "end";
+ print_cut();
+ print_string "end";
close_box()
| Fix ((t,i),(lna,tl,bl)) ->
- print_string "Fix("; print_int i; print_string ")";
+ print_string "Fix("; print_int i; print_string ")";
print_cut();
open_vbox 0;
let rec print_fix () =
for k = 0 to (Array.length tl) - 1 do
open_vbox 0;
- name_display lna.(k); print_string "/";
+ name_display lna.(k); print_string "/";
print_int t.(k); print_cut(); print_string ":";
box_display tl.(k) ; print_cut(); print_string ":=";
box_display bl.(k); close_box ();
print_cut()
done
- in print_string"{"; print_fix(); print_string"}"
+ in print_string"{"; print_fix(); print_string"}"
| CoFix(i,(lna,tl,bl)) ->
- print_string "CoFix("; print_int i; print_string ")";
+ print_string "CoFix("; print_int i; print_string ")";
print_cut();
open_vbox 0;
let rec print_fix () =
@@ -300,27 +315,27 @@ let print_pure_constr csr =
| Name id -> print_string (string_of_id id)
| Anonymous -> print_string "_"
(* Remove the top names for library and Scratch to avoid long names *)
- and sp_display sp =
+ and sp_display sp =
(* let dir,l = decode_kn sp in
- let ls =
- match List.rev (List.map string_of_id (repr_dirpath dir)) with
+ let ls =
+ match List.rev (List.map string_of_id (repr_dirpath dir)) with
("Top"::l)-> l
- | ("Coq"::_::l) -> l
+ | ("Coq"::_::l) -> l
| l -> l
in List.iter (fun x -> print_string x; print_string ".") ls;*)
- print_string (string_of_kn sp)
- and sp_con_display sp =
+ print_string (debug_string_of_mind sp)
+ and sp_con_display sp =
(* let dir,l = decode_kn sp in
- let ls =
- match List.rev (List.map string_of_id (repr_dirpath dir)) with
+ let ls =
+ match List.rev (List.map string_of_id (repr_dirpath dir)) with
("Top"::l)-> l
- | ("Coq"::_::l) -> l
+ | ("Coq"::_::l) -> l
| l -> l
in List.iter (fun x -> print_string x; print_string ".") ls;*)
- print_string (string_of_con sp)
+ print_string (debug_string_of_con sp)
in
- try
+ try
box_display csr; print_flush()
with e ->
print_string (Printexc.to_string e);print_flush ();
@@ -369,7 +384,7 @@ let pp_generic_argument arg =
(* Vernac-level debugging commands *)
let in_current_context f c =
- let (evmap,sign) =
+ let (evmap,sign) =
try Pfedit.get_current_goal_context ()
with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) in
f (Constrintern.interp_constr evmap sign c)
@@ -400,12 +415,10 @@ let _ =
e -> Pp.pp (Cerrors.explain_exn e)
let _ =
extend_vernac_command_grammar "PrintConstr"
- [[TacTerm "PrintConstr";
- TacNonTerm
- (dummy_loc,
- (Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr),
- ConstrArgType),
- Some "c")]]
+ [[GramTerminal "PrintConstr";
+ GramNonTerminal
+ (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"),
+ Some (Names.id_of_string "c"))]]
let _ =
try
@@ -419,12 +432,10 @@ let _ =
e -> Pp.pp (Cerrors.explain_exn e)
let _ =
extend_vernac_command_grammar "PrintPureConstr"
- [[TacTerm "PrintPureConstr";
- TacNonTerm
- (dummy_loc,
- (Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr),
- ConstrArgType),
- Some "c")]]
+ [[GramTerminal "PrintPureConstr";
+ GramNonTerminal
+ (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"),
+ Some (Names.id_of_string "c"))]]
(* Setting printer of unbound global reference *)
open Names
@@ -434,38 +445,38 @@ open Libnames
let encode_path loc prefix mpdir suffix id =
let dir = match mpdir with
| None -> []
- | Some (mp,dir) ->
+ | Some (mp,dir) ->
(repr_dirpath (dirpath_of_string (string_of_mp mp))@
repr_dirpath dir) in
- Qualid (loc, make_qualid
+ Qualid (loc, make_qualid
(make_dirpath (List.rev (id_of_string prefix::dir@suffix))) id)
let raw_string_of_ref loc = function
- | ConstRef cst ->
+ | ConstRef cst ->
let (mp,dir,id) = repr_con cst in
encode_path loc "CST" (Some (mp,dir)) [] (id_of_label id)
| IndRef (kn,i) ->
- let (mp,dir,id) = repr_kn kn in
- encode_path loc "IND" (Some (mp,dir)) [id_of_label id]
+ let (mp,dir,id) = repr_mind kn in
+ encode_path loc "IND" (Some (mp,dir)) [id_of_label id]
(id_of_string ("_"^string_of_int i))
- | ConstructRef ((kn,i),j) ->
- let (mp,dir,id) = repr_kn kn in
+ | ConstructRef ((kn,i),j) ->
+ let (mp,dir,id) = repr_mind kn in
encode_path loc "CSTR" (Some (mp,dir))
- [id_of_label id;id_of_string ("_"^string_of_int i)]
+ [id_of_label id;id_of_string ("_"^string_of_int i)]
(id_of_string ("_"^string_of_int j))
- | VarRef id ->
+ | VarRef id ->
encode_path loc "SECVAR" None [] id
let short_string_of_ref loc = function
| VarRef id -> Ident (loc,id)
| ConstRef cst -> Ident (loc,id_of_label (pi3 (repr_con cst)))
- | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_kn kn)))
+ | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_mind kn)))
| IndRef (kn,i) ->
- encode_path loc "IND" None [id_of_label (pi3 (repr_kn kn))]
+ encode_path loc "IND" None [id_of_label (pi3 (repr_mind kn))]
(id_of_string ("_"^string_of_int i))
- | ConstructRef ((kn,i),j) ->
- encode_path loc "CSTR" None
- [id_of_label (pi3 (repr_kn kn));id_of_string ("_"^string_of_int i)]
+ | ConstructRef ((kn,i),j) ->
+ encode_path loc "CSTR" None
+ [id_of_label (pi3 (repr_mind kn));id_of_string ("_"^string_of_int i)]
(id_of_string ("_"^string_of_int j))
let _ = Constrextern.set_debug_global_reference_printer
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 07:14:54 +0000