From 602badcad9deec9224b78cd1e1033af30358ef2e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
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.
---
 library/libnames.ml |  4 ++--
 library/library.ml  | 10 +++++-----
 library/nameops.ml  |  4 ++--
 library/nametab.ml  |  2 +-
 4 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'library')

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
 
-- 
cgit v1.2.3