From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- dev/top_printers.ml | 147 ++++++++++++++++++++++++++++------------------------ 1 file changed, 79 insertions(+), 68 deletions(-) (limited to 'dev/top_printers.ml') 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 "") ++ + (if id = id0 then mt () + else spc () ++ 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(,"^(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 -- cgit v1.2.3