aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
diff options
context:
space:
mode:
Diffstat (limited to 'dev/top_printers.ml')
-rw-r--r--dev/top_printers.ml62
1 files changed, 32 insertions, 30 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index dea70360a5..b552d99949 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -22,7 +22,6 @@ open Evd
open Goptions
open Genarg
open Clenv
-open Universes
let _ = Detyping.print_evar_arguments := true
let _ = Detyping.print_universes := true
@@ -30,7 +29,7 @@ let _ = set_bool_option_value ["Printing";"Matching"] false
let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
(* std_ppcmds *)
-let pppp x = pp x
+let pp x = Pp.pp_with !Pp_control.std_ft x
(** Future printer *)
@@ -41,10 +40,10 @@ let ppid id = pp (pr_id id)
let pplab l = pp (pr_lab l)
let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
let ppdir dir = pp (pr_dirpath dir)
-let ppmp mp = pp(str (string_of_mp mp))
+let ppmp mp = pp(str (ModPath.debug_to_string mp))
let ppcon con = pp(debug_pr_con con)
let ppproj con = pp(debug_pr_con (Projection.constant con))
-let ppkn kn = pp(pr_kn kn)
+let ppkn kn = pp(str (KerName.to_string kn))
let ppmind kn = pp(debug_pr_mind kn)
let ppind (kn,i) = pp(debug_pr_mind kn ++ str"," ++int i)
let ppsp sp = pp(pr_path sp)
@@ -80,7 +79,7 @@ let ppconstr_univ x = Constrextern.with_universes ppconstr x
let ppglob_constr = (fun x -> pp(pr_lglob_constr x))
let pppattern = (fun x -> pp(pr_constr_pattern x))
let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e)))
-let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
+let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
let ppbigint n = pp (str (Bigint.to_string n));;
@@ -216,13 +215,12 @@ let ppuniverse_subst l = pp (Univ.pr_universe_subst l)
let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l)
let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l)
let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l)
-let ppconstraints_map c = pp (Universes.pr_constraints_map c)
let ppconstraints c = pp (pr_constraints Level.pr c)
let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
let ppuniverse_context_future c =
let ctx = Future.force c in
ppuniverse_context ctx
-let ppuniverses u = pp (Univ.pr_universes Level.pr u)
+let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
let ppnamedcontextval e =
pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
@@ -230,6 +228,11 @@ let ppenv e = pp
(str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]")
+let ppenvwithcst e = pp
+ (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
+ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++
+ str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
+
let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x))
let ppobj obj = Format.print_string (Libobject.object_tag obj)
@@ -311,7 +314,7 @@ let constr_display csr =
| Anonymous -> "Anonymous"
in
- Pp.pp (str (term_display csr) ++fnl ()); Pp.pp_flush ()
+ pp (str (term_display csr) ++fnl ())
open Format;;
@@ -452,7 +455,7 @@ let print_pure_constr csr =
print_string (Printexc.to_string e);print_flush ();
raise e
-let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
+let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
let pploc x = let (l,r) = Loc.unloc x in
print_string"(";print_int l;print_string",";print_int r;print_string")"
@@ -463,16 +466,19 @@ let pp_generic_argument arg =
pp(str"<genarg:"++pr_argument_type(genarg_tag arg)++str">")
let prgenarginfo arg =
- let tpe = pr_argument_type (genarg_tag arg) in
- let pr_gtac _ x = Pptactic.pr_glob_tactic (Global.env()) x in
- try
- let data = Pptactic.pr_top_generic pr_constr pr_lconstr pr_gtac pr_constr_pattern arg in
- str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >"
- with _any ->
+ let Geninterp.Val.Dyn (tag, _) = arg in
+ let tpe = Geninterp.Val.pr tag in
+ (** FIXME *)
+(* try *)
+(* let data = Pptactic.pr_top_generic (Global.env ()) arg in *)
+(* str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >" *)
+(* with _any -> *)
str "<genarg:" ++ tpe ++ str ">"
let ppgenarginfo arg = pp (prgenarginfo arg)
+let ppgenargargt arg = pp (str (Genarg.ArgT.repr arg))
+
let ppist ist =
let pr id arg = prgenarginfo arg in
pp (pridmap pr ist.Geninterp.lfun)
@@ -481,9 +487,7 @@ let ppist ist =
(* Vernac-level debugging commands *)
let in_current_context f c =
- let (evmap,sign) =
- try Pfedit.get_current_goal_context ()
- with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) in
+ let (evmap,sign) = Pfedit.get_current_context () in
f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*)
(* We expand the result of preprocessing to be independent of camlp4
@@ -498,42 +502,40 @@ END
open Pcoq
open Genarg
-open Constrarg
+open Stdarg
open Egramml
let _ =
try
- Vernacinterp.vinterp_add ("PrintConstr", 0)
+ Vernacinterp.vinterp_add false ("PrintConstr", 0)
(function
- [c] when genarg_tag c = ConstrArgType && true ->
+ [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
let c = out_gen (rawwit wit_constr) c in
(fun () -> in_current_context constr_display c)
| _ -> failwith "Vernac extension: cannot occur")
with
- e -> Pp.pp (Errors.print e)
+ e -> pp (CErrors.print e)
let _ =
extend_vernac_command_grammar ("PrintConstr", 0) None
[GramTerminal "PrintConstr";
GramNonTerminal
- (Loc.ghost,ConstrArgType,Aentry ("constr","constr"),
- Some (Names.Id.of_string "c"))]
+ (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)]
let _ =
try
- Vernacinterp.vinterp_add ("PrintPureConstr", 0)
+ Vernacinterp.vinterp_add false ("PrintPureConstr", 0)
(function
- [c] when genarg_tag c = ConstrArgType && true ->
+ [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
let c = out_gen (rawwit wit_constr) c in
(fun () -> in_current_context print_pure_constr c)
| _ -> failwith "Vernac extension: cannot occur")
with
- e -> Pp.pp (Errors.print e)
+ e -> pp (CErrors.print e)
let _ =
extend_vernac_command_grammar ("PrintPureConstr", 0) None
[GramTerminal "PrintPureConstr";
GramNonTerminal
- (Loc.ghost,ConstrArgType,Aentry ("constr","constr"),
- Some (Names.Id.of_string "c"))]
+ (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)]
(* Setting printer of unbound global reference *)
open Names
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 16:11:05 +0000