From 602badcad9deec9224b78cd1e1033af30358ef2e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Dec 2015 22:35:09 +0100 Subject: Do not compose "str" and "to_string" whenever possible. For instance, calling only Id.print is faster than calling both str and Id.to_string, since the latter performs a copy. It also makes the code a bit simpler to read. --- checker/safe_typing.ml | 6 ++++-- interp/coqlib.ml | 2 +- library/libnames.ml | 4 ++-- library/library.ml | 10 +++++----- library/nameops.ml | 4 ++-- library/nametab.ml | 2 +- plugins/extraction/table.ml | 2 +- printing/ppconstr.ml | 6 +++--- printing/ppvernac.ml | 2 +- printing/printer.ml | 4 ++-- printing/printmod.ml | 2 +- toplevel/himsg.ml | 16 ++++++++-------- toplevel/obligations.ml | 8 ++++---- toplevel/record.ml | 2 +- toplevel/vernacentries.ml | 6 +++--- 15 files changed, 39 insertions(+), 37 deletions(-) diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 81a3cc035..ee3305167 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -13,6 +13,8 @@ open Cic open Names open Environ +let pr_dirpath dp = str (DirPath.to_string dp) + (************************************************************************) (* * Global environment @@ -52,9 +54,9 @@ let check_engagement env (expected_impredicative_set,expected_type_in_type) = let report_clash f caller dir = let msg = - str "compiled library " ++ str(DirPath.to_string caller) ++ + str "compiled library " ++ pr_dirpath caller ++ spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++ - str(DirPath.to_string dir) ++ fnl() in + pr_dirpath dir ++ fnl() in f msg diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 5ac718e3b..b309f26cd 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -87,7 +87,7 @@ let check_required_library d = *) (* or failing ...*) errorlabstrm "Coqlib.check_required_library" - (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.") + (str "Library " ++ pr_dirpath dir ++ str " has to be required first.") (************************************************************************) (* Specific Coq objects *) diff --git a/library/libnames.ml b/library/libnames.ml index cdaec6a3d..36b46ca49 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -13,7 +13,7 @@ open Names (**********************************************) -let pr_dirpath sl = (str (DirPath.to_string sl)) +let pr_dirpath sl = str (DirPath.to_string sl) (*s Operations on dirpaths *) @@ -197,7 +197,7 @@ let string_of_reference = function let pr_reference = function | Qualid (_,qid) -> pr_qualid qid - | Ident (_,id) -> str (Id.to_string id) + | Ident (_,id) -> Id.print id let loc_of_reference = function | Qualid (loc,qid) -> loc diff --git a/library/library.ml b/library/library.ml index 4f964a051..ef621e16b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -132,7 +132,7 @@ let try_find_library dir = try find_library dir with Not_found -> errorlabstrm "Library.find_library" - (str "Unknown library " ++ str (DirPath.to_string dir)) + (str "Unknown library " ++ pr_dirpath dir) let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) @@ -474,7 +474,7 @@ and intern_library_deps libs dir m from = and intern_mandatory_library caller from libs (dir,d) = let digest, libs = intern_library libs (dir, None) from in if not (Safe_typing.digest_match ~actual:digest ~required:d) then - errorlabstrm "" (str "Compiled library " ++ str (DirPath.to_string caller) ++ str ".vo makes inconsistent assumptions over library " ++ str (DirPath.to_string dir)); + errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir); libs let rec_intern_library libs (dir, f) = @@ -567,7 +567,7 @@ let safe_locate_module (loc,qid) = try Nametab.locate_module qid with Not_found -> user_err_loc - (loc,"import_library", str (string_of_qualid qid) ++ str " is not a module") + (loc,"import_library", pr_qualid qid ++ str " is not a module") let import_module export modl = (* Optimization: libraries in a raw in the list are imported @@ -592,7 +592,7 @@ let import_module export modl = try Declaremods.import_module export mp; aux [] l with Not_found -> user_err_loc (loc,"import_library", - str (string_of_qualid dir) ++ str " is not a module")) + pr_qualid dir ++ str " is not a module")) | [] -> flush acc in aux [] modl @@ -604,7 +604,7 @@ let check_coq_overwriting p id = let is_empty = match l with [] -> true | _ -> false in if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then errorlabstrm "" - (str "Cannot build module " ++ str (DirPath.to_string p) ++ str "." ++ pr_id id ++ str "." ++ spc () ++ + (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++ str "it starts with prefix \"Coq\" which is reserved for the Coq library.") (* Verifies that a string starts by a letter and do not contain diff --git a/library/nameops.ml b/library/nameops.ml index 3a23ab97d..418d620c2 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -12,7 +12,7 @@ open Names (* Identifiers *) -let pr_id id = str (Id.to_string id) +let pr_id id = Id.print id let pr_name = function | Anonymous -> str "_" @@ -141,7 +141,7 @@ let name_max na1 na2 = | Name _ -> na1 | Anonymous -> na2 -let pr_lab l = str (Label.to_string l) +let pr_lab l = Label.print l let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/nametab.ml b/library/nametab.ml index 5b6d7cd98..621640ef9 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -523,7 +523,7 @@ let shortest_qualid_of_tactic kn = KnTab.shortest_qualid Id.Set.empty sp !the_tactictab let pr_global_env env ref = - try str (string_of_qualid (shortest_qualid_of_global env ref)) + try pr_qualid (shortest_qualid_of_global env ref) with Not_found as e -> if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 9feaea8cd..30486879e 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -453,7 +453,7 @@ let check_loaded_modfile mp = match base_mp mp with if not (Library.library_is_loaded dp) then begin match base_mp (Lib.current_mp ()) with | MPfile dp' when not (DirPath.equal dp dp') -> - err (str ("Please load library "^(DirPath.to_string dp^" first."))) + err (str "Please load library " ++ pr_dirpath dp ++ str " first.") | _ -> () end | _ -> () diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 56429410c..d15c3ee2f 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -153,11 +153,11 @@ end) = struct let pr_qualid sp = let (sl, id) = repr_qualid sp in - let id = tag_ref (str (Id.to_string id)) in + let id = tag_ref (pr_id id) in let sl = match List.rev (DirPath.repr sl) with | [] -> mt () | sl -> - let pr dir = tag_path (str (Id.to_string dir)) ++ str "." in + let pr dir = tag_path (pr_id dir) ++ str "." in prlist pr sl in sl ++ id @@ -182,7 +182,7 @@ end) = struct let pr_reference = function | Qualid (_, qid) -> pr_qualid qid - | Ident (_, id) -> tag_var (str (Id.to_string id)) + | Ident (_, id) -> tag_var (pr_id id) let pr_cref ref us = pr_reference ref ++ pr_universe_instance us diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index f216c599d..495719990 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1034,7 +1034,7 @@ module Make let pr_tac_body tacdef_body = let id, redef, body = match tacdef_body with - | TacticDefinition ((_,id), body) -> str (Id.to_string id), false, body + | TacticDefinition ((_,id), body) -> pr_id id, false, body | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body in let idl, body = diff --git a/printing/printer.ml b/printing/printer.ml index 2e112f9ac..7c031ea53 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -777,7 +777,7 @@ let pr_assumptionset env s = let (v, a, o, tr) = accu in match t with | Variable id -> - let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in + let var = pr_id id ++ str " : " ++ pr_ltype typ in (var :: v, a, o, tr) | Axiom (kn,[]) -> let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in @@ -786,7 +786,7 @@ let pr_assumptionset env s = let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++ cut() ++ prlist_with_sep cut (fun (lbl, ctx, ty) -> - str " used in " ++ str (Names.Label.to_string lbl) ++ + str " used in " ++ pr_label lbl ++ str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty)) l in (v, ax :: a, o, tr) diff --git a/printing/printmod.ml b/printing/printmod.ml index d6f847cc7..e0b1d55be 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -264,7 +264,7 @@ let nametab_register_modparam mbid mtb = List.iter (nametab_register_body mp dir) struc let print_body is_impl env mp (l,body) = - let name = str (Label.to_string l) in + let name = pr_label l in hov 2 (match body with | SFBmodule _ -> keyword "Module" ++ spc () ++ name | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 8f380830d..e21b6b41c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -822,7 +822,7 @@ let explain_not_match_error = function | ModuleTypeFieldExpected -> strbrk "a module type is expected" | NotConvertibleInductiveField id | NotConvertibleConstructorField id -> - str "types given to " ++ str (Id.to_string id) ++ str " differ" + str "types given to " ++ pr_id id ++ str " differ" | NotConvertibleBodyField -> str "the body of definitions differs" | NotConvertibleTypeField (env, typ1, typ2) -> @@ -847,7 +847,7 @@ let explain_not_match_error = function | RecordProjectionsExpected nal -> (if List.length nal >= 2 then str "expected projection names are " else str "expected projection name is ") ++ - pr_enum (function Name id -> str (Id.to_string id) | _ -> str "_") nal + pr_enum (function Name id -> pr_id id | _ -> str "_") nal | NotEqualInductiveAliases -> str "Aliases to inductive types do not match" | NoTypeConstraintExpected -> @@ -896,11 +896,11 @@ let explain_not_equal_module_paths mp1 mp2 = str "Non equal modules." let explain_no_such_label l = - str "No such label " ++ str (Label.to_string l) ++ str "." + str "No such label " ++ pr_label l ++ str "." let explain_incompatible_labels l l' = str "Opening and closing labels are not the same: " ++ - str (Label.to_string l) ++ str " <> " ++ str (Label.to_string l') ++ str "!" + pr_label l ++ str " <> " ++ pr_label l' ++ str "!" let explain_not_a_module s = quote (str s) ++ str " is not a module." @@ -909,19 +909,19 @@ let explain_not_a_module_type s = quote (str s) ++ str " is not a module type." let explain_not_a_constant l = - quote (Label.print l) ++ str " is not a constant." + quote (pr_label l) ++ str " is not a constant." let explain_incorrect_label_constraint l = str "Incorrect constraint for label " ++ - quote (Label.print l) ++ str "." + quote (pr_label l) ++ str "." let explain_generative_module_expected l = - str "The module " ++ str (Label.to_string l) ++ str " is not generative." ++ + str "The module " ++ pr_label l ++ str " is not generative." ++ strbrk " Only components of generative modules can be changed" ++ strbrk " using the \"with\" construct." let explain_label_missing l s = - str "The field " ++ str (Label.to_string l) ++ str " is missing in " + str "The field " ++ pr_label l ++ str " is missing in " ++ str s ++ str "." let explain_module_error = function diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index cac81a939..a3b973e4d 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -266,7 +266,7 @@ let reduce c = exception NoObligations of Id.t option let explain_no_obligations = function - Some ident -> str "No obligations for program " ++ str (Id.to_string ident) + Some ident -> str "No obligations for program " ++ Id.print ident | None -> str "No obligations remaining" type obligation_info = @@ -996,7 +996,7 @@ let show_obligations_of_prg ?(msg=true) prg = if !showed > 0 then ( decr showed; msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ - str "of" ++ spc() ++ str (Id.to_string n) ++ str ":" ++ spc () ++ + str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++ hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++ str "." ++ fnl ()))) | Some _ -> ()) @@ -1013,14 +1013,14 @@ let show_obligations ?(msg=true) n = let show_term n = let prg = get_prog_err n in let n = prg.prg_name in - (str (Id.to_string n) ++ spc () ++ str":" ++ spc () ++ + (Id.print n ++ spc () ++ str":" ++ spc () ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body) let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls = let sign = Decls.initialize_named_context_for_proof () in - let info = str (Id.to_string n) ++ str " has type-checked" in + let info = Id.print n ++ str " has type-checked" in let prg = init_prog_info sign ~opaque n term t ctx [] None [] obls implicits kind reduce hook in let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( diff --git a/toplevel/record.ml b/toplevel/record.ml index 3a75004b0..c432274a0 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -171,7 +171,7 @@ let warning_or_error coe indsp err = let st = match err with | MissingProj (fi,projs) -> let s,have = if List.length projs > 1 then "s","were" else "","was" in - (str(Id.to_string fi) ++ + (pr_id fi ++ strbrk" cannot be defined because the projection" ++ str s ++ spc () ++ prlist_with_sep pr_comma pr_id projs ++ spc () ++ str have ++ strbrk " not defined.") diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 28b5bace1..7144db494 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -156,7 +156,7 @@ let show_match id = (* "Print" commands *) let print_path_entry p = - let dir = str (DirPath.to_string (Loadpath.logical p)) in + let dir = pr_dirpath (Loadpath.logical p) in let path = str (Loadpath.physical p) in (dir ++ str " " ++ tbrk (0, 0) ++ path) @@ -947,7 +947,7 @@ let register_ltac local tacl = match tactic_body with | TacticDefinition ((loc,id), body) -> let kn = Lib.make_kn id in - let id_pp = str (Id.to_string id) in + let id_pp = pr_id id in let () = if is_defined_tac kn then Errors.user_err_loc (loc, "", str "There is already an Ltac named " ++ id_pp ++ str".") @@ -1584,7 +1584,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt = let natureofid = match bdyopt with | None -> "Hypothesis" | Some bdy ->"Constant (let in)" in - v 0 (str (Id.to_string id) ++ str":" ++ pr_constr typ ++ fnl() ++ fnl() + v 0 (pr_id id ++ str":" ++ pr_constr typ ++ fnl() ++ fnl() ++ str natureofid ++ str " of the goal context.") with (* fallback to globals *) | NoHyp | Not_found -> print_about ref_or_by_not -- cgit v1.2.3