diff options
| -rw-r--r-- | dev/set_raw_db | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 3 | ||||
| -rw-r--r-- | interp/constrextern.ml | 15 | ||||
| -rw-r--r-- | interp/constrextern.mli | 3 |
4 files changed, 20 insertions, 2 deletions
diff --git a/dev/set_raw_db b/dev/set_raw_db new file mode 100644 index 0000000000..5caff7e5d4 --- /dev/null +++ b/dev/set_raw_db @@ -0,0 +1 @@ +install_printer Top_printers.ppconstrdb diff --git a/dev/top_printers.ml b/dev/top_printers.ml index df089f0b1b..df3835d2fe 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -46,7 +46,8 @@ let ppsp sp = pp(pr_sp sp) let ppqualid qid = pp(pr_qualid qid) (* term printers *) -let ppconstr x = pp(Termops.print_constr x) +let ppconstr x = pp (Termops.print_constr x) +let ppconstrdb x = pp(Options.with_option Constrextern.rawdebug Termops.print_constr x) let ppterm = ppconstr let ppsconstr x = ppconstr (Declarations.force x) let ppconstr_univ x = Constrextern.with_universes ppconstr x diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d386622946..96548df711 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -109,6 +109,8 @@ let extern_evar loc n = *) CEvar (loc,n) +let rawdebug = ref false + let raw_string_of_ref = function | ConstRef kn -> "CONST("^(string_of_con kn)^")" @@ -120,11 +122,22 @@ let raw_string_of_ref = function | VarRef id -> "SECVAR("^(string_of_id id)^")" +let short_string_of_ref = function + | VarRef id -> string_of_id id + | ConstRef cst -> string_of_label (pi3 (repr_con cst)) + | IndRef (kn,0) -> string_of_label (pi3 (repr_kn kn)) + | IndRef (kn,i) -> + "IND("^string_of_label (pi3 (repr_kn kn))^(string_of_int i)^")" + | ConstructRef ((kn,i),j) -> + "CONSTRUCT("^ + string_of_label (pi3 (repr_kn kn))^","^(string_of_int i)^","^(string_of_int j)^")" + let extern_reference loc vars r = try Qualid (loc,shortest_qualid_of_global vars r) with Not_found -> (* happens in debugger *) - Ident (loc,id_of_string (raw_string_of_ref r)) + let f = if !rawdebug then raw_string_of_ref else short_string_of_ref in + Ident (loc,id_of_string (f r)) (************************************************************************) (* Equality up to location (useful for translator v8) *) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 0ffb8c333a..9a9c55ec1d 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -52,6 +52,9 @@ val print_universes : bool ref val print_no_symbol : bool ref val print_projections : bool ref +(* Debug printing options *) +val rawdebug : bool ref + (* This governs printing of implicit arguments. If [with_implicits] is on and not [with_arguments] then implicit args are printed prefixed by "!"; if [with_implicits] and [with_arguments] are both on the |