summaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /dev/top_printers.ml
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'dev/top_printers.ml')
-rw-r--r--dev/top_printers.ml73
1 files changed, 68 insertions, 5 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e1ee29e4..afae141b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -32,6 +32,10 @@ open Genarg
let _ = Constrextern.print_evar_arguments := true
let _ = set_bool_option_value (SecondaryTable ("Printing","Matching")) false
+let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
+
+(* std_ppcmds *)
+let pppp x = pp x
(* name printers *)
let ppid id = pp (pr_id id)
@@ -44,20 +48,26 @@ let ppcon con = pp(pr_con con)
let ppkn kn = pp(pr_kn kn)
let ppsp sp = pp(pr_sp sp)
let ppqualid qid = pp(pr_qualid qid)
+let ppclindex cl = pp(Classops.pr_cl_index cl)
(* term printers *)
-let ppconstr x = pp(Termops.print_constr x)
+let rawdebug = ref false
+let ppconstr x = pp (Termops.print_constr x)
+let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x)
let ppterm = ppconstr
let ppsconstr x = ppconstr (Declarations.force x)
let ppconstr_univ x = Constrextern.with_universes ppconstr x
let pprawconstr = (fun x -> pp(pr_lrawconstr x))
let pppattern = (fun x -> pp(pr_constr_pattern x))
let pptype = (fun x -> pp(pr_ltype x))
+
let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
let ppbigint n = pp (Bigint.pr_bigint n);;
-let ppidset l = pp (prlist_with_sep spc pr_id (Idset.elements l))
+let prset pr l = str "[" ++ 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 pP s = pp (hov 0 s)
@@ -81,7 +91,14 @@ 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 pp_idpred s = pp (pr_idpred s)
+let pp_cpred s = pp (pr_cpred s)
+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)
@@ -103,6 +120,8 @@ let ppuni u = pp(pr_uni u)
let ppuniverses u = pp (str"[" ++ pr_universes u ++ str"]")
+let ppconstraints c = pp (pr_constraints c)
+
let ppenv e = pp
(str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++
str "[" ++ pr_rel_context e (rel_context e) ++ str "]")
@@ -240,8 +259,7 @@ let print_pure_constr csr =
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 () =
@@ -253,7 +271,7 @@ let print_pure_constr csr =
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_cut();
@@ -404,3 +422,48 @@ let _ =
(Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr),
ConstrArgType),
Some "c")]]
+
+(* Setting printer of unbound global reference *)
+open Names
+open Nameops
+open Libnames
+
+let encode_path loc prefix mpdir suffix id =
+ let dir = match mpdir with
+ | None -> []
+ | Some (mp,dir) ->
+ (repr_dirpath (dirpath_of_string (string_of_mp mp))@
+ repr_dirpath dir) in
+ Qualid (loc, make_qualid
+ (make_dirpath (List.rev (id_of_string prefix::dir@suffix))) id)
+
+let raw_string_of_ref loc = function
+ | 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]
+ (id_of_string ("_"^string_of_int i))
+ | ConstructRef ((kn,i),j) ->
+ let (mp,dir,id) = repr_kn kn in
+ encode_path loc "CSTR" (Some (mp,dir))
+ [id_of_label id;id_of_string ("_"^string_of_int i)]
+ (id_of_string ("_"^string_of_int j))
+ | 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,i) ->
+ encode_path loc "IND" 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_kn kn));id_of_string ("_"^string_of_int i)]
+ (id_of_string ("_"^string_of_int j))
+
+let _ = Constrextern.set_debug_global_reference_printer
+ (if !rawdebug then raw_string_of_ref else short_string_of_ref)