More monomorphic List.mem + List.assoc + ...

 To reduce the amount of syntactic noise, we now provide
 a few inner modules Int.List, Id.List, String.List, Sorts.List
 which contain some monomorphic (or semi-monomorphic) functions
 such as mem, assoc, ...

 NB: for Int.List.mem and co we reuse List.memq and so on.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 51 insertions, 45 deletions

diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 26fab4ac2..bf46065d0 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -13,6 +13,8 @@
 (************************************************************************)
 
 open Pp
+open Util
+open Names
 
 (* Utility Functions *)
 
@@ -37,7 +39,7 @@ let get_module_path_of_full_path path =
 (*CSC: not exist two modules whose dir_paths are one a prefix of the other *)
 let remove_module_dirpath_from_dirpath ~basedir dir =
   if Libnames.is_dirpath_prefix_of basedir dir then
-   let ids = Names.DirPath.repr dir in
+   let ids = DirPath.repr dir in
    let rec remove_firsts n l =
     match n,l with
        (0,l) -> l
@@ -47,11 +49,11 @@ let remove_module_dirpath_from_dirpath ~basedir dir =
     let ids' =
      List.rev
       (remove_firsts
-        (List.length (Names.DirPath.repr basedir))
+        (List.length (DirPath.repr basedir))
         (List.rev ids))
     in
      ids'
-  else Names.DirPath.repr dir
+  else DirPath.repr dir
 ;;
 
 
@@ -60,21 +62,22 @@ let get_uri_of_var v pvars =
    function
       [] -> Errors.error ("Variable "^v^" not found")
     | he::tl as modules ->
-       let dirpath = Names.DirPath.make modules in
-        if List.mem (Names.Id.of_string v) (Decls.last_section_hyps dirpath) then
+       let dirpath = DirPath.make modules in
+       if Id.List.mem (Id.of_string v) (Decls.last_section_hyps dirpath)
+       then
          modules
-        else
+       else
          search_in_open_sections tl
   in
    let path =
-    if List.mem v pvars then
+    if String.List.mem v pvars then
       []
     else
-      search_in_open_sections (Names.DirPath.repr (Lib.cwd ()))
+      search_in_open_sections (DirPath.repr (Lib.cwd ()))
    in
     "cic:" ^
      List.fold_left
-      (fun i x -> "/" ^ Names.Id.to_string x ^ i) "" path
+      (fun i x -> "/" ^ Id.to_string x ^ i) "" path
 ;;
 
 type tag =
@@ -105,31 +108,31 @@ let ext_of_tag =
 exception FunctorsXMLExportationNotImplementedYet;;
 
 let subtract l1 l2 =
- let l1' = List.rev (Names.DirPath.repr l1) in
- let l2' = List.rev (Names.DirPath.repr l2) in
+ let l1' = List.rev (DirPath.repr l1) in
+ let l2' = List.rev (DirPath.repr l2) in
   let rec aux =
    function
       he::tl when tl = l2' -> [he]
     | he::tl -> he::(aux tl)
     | [] -> assert (l2' = []) ; []
   in
-   Names.DirPath.make (List.rev (aux l1'))
+   DirPath.make (List.rev (aux l1'))
 ;;
 
 let token_list_of_path dir id tag =
   let token_list_of_dirpath dirpath =
-   List.rev_map Names.Id.to_string (Names.DirPath.repr dirpath) in
-  token_list_of_dirpath dir @ [Names.Id.to_string id ^ "." ^ (ext_of_tag tag)]
+   List.rev_map Id.to_string (DirPath.repr dirpath) in
+  token_list_of_dirpath dir @ [Id.to_string id ^ "." ^ (ext_of_tag tag)]
 
 let token_list_of_kernel_name tag =
  let id,dir = match tag with
    | Variable kn ->
-       Names.Label.to_id (Names.label kn), Lib.cwd ()
+       Label.to_id (Names.label kn), Lib.cwd ()
    | Constant con ->
-       Names.Label.to_id (Names.con_label con),
+       Label.to_id (Names.con_label con),
        Lib.remove_section_part (Globnames.ConstRef con)
    | Inductive kn ->
-       Names.Label.to_id (Names.mind_label kn),
+       Label.to_id (Names.mind_label kn),
        Lib.remove_section_part (Globnames.IndRef (kn,0))
  in
  token_list_of_path dir id (etag_of_tag tag)
@@ -188,7 +191,7 @@ let typeur sigma metamap =
   let rec type_of env cstr=
     match Term.kind_of_term cstr with
     | T.Meta n ->
-          (try T.strip_outer_cast (Util.List.assoc_f Int.equal n metamap)
+          (try T.strip_outer_cast (Int.List.assoc n metamap)
            with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term"))
     | T.Rel n ->
         let (_,_,ty) = Environ.lookup_rel n env in
@@ -198,7 +201,7 @@ let typeur sigma metamap =
           let (_,_,ty) = Environ.lookup_named id env in
           ty
         with Not_found ->
-          Errors.anomaly ~label:"type_of" (str "variable " ++ Names.Id.print id ++ str " unbound"))
+          Errors.anomaly ~label:"type_of" (str "variable " ++ Id.print id ++ str " unbound"))
     | T.Const c ->
         let cb = Environ.lookup_constant c env in
         Typeops.type_of_constant_type env (cb.Declarations.const_type)
@@ -447,8 +450,8 @@ print_endline "PASSATO" ; flush stdout ;
                 let he1' = remove_module_dirpath_from_dirpath ~basedir he1_sp in
                 let he1'' =
                  String.concat "/"
-                  (List.rev_map Names.Id.to_string he1') ^ "/"
-                 ^ (Names.Id.to_string he1_id) ^ ".var"
+                  (List.rev_map Id.to_string he1') ^ "/"
+                 ^ (Id.to_string he1_id) ^ ".var"
                 in
                  (he1'',he2)::subst, extra_args, uninst
            in
@@ -493,13 +496,13 @@ print_endline "PASSATO" ; flush stdout ;
                Acic.ARel (fresh_id'', n, List.nth idrefs (n-1), id)
            | Term.Var id ->
 	      let pvars = Termops.ids_of_named_context (Environ.named_context env) in
-	      let pvars = List.map Names.Id.to_string pvars in
-              let path = get_uri_of_var (Names.Id.to_string id) pvars in
+	      let pvars = List.map Id.to_string pvars in
+              let path = get_uri_of_var (Id.to_string id) pvars in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                if is_a_Prop innersort  && expected_available then
                 add_inner_type fresh_id'' ;
                Acic.AVar
-                (fresh_id'', path ^ "/" ^ (Names.Id.to_string id) ^ ".var")
+                (fresh_id'', path ^ "/" ^ (Id.to_string id) ^ ".var")
            | Term.Evar (n,l) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort  && expected_available then
@@ -602,7 +605,7 @@ print_endline "PASSATO" ; flush stdout ;
            | Term.LetIn (n,s,t,d) ->
               let id =
                match n with
-                   Names.Anonymous -> Names.Id.of_string "_X"
+                   Names.Anonymous -> Id.of_string "_X"
                  | Names.Name id -> id
               in
               let n' =
@@ -877,7 +880,7 @@ let acic_object_of_cic_object sigma obj =
                          in
                          let dummy_never_used =
                           let s = "dummy_never_used" in
-                           Acic.ARel (s,99,s,Names.Id.of_string s)
+                           Acic.ARel (s,99,s,Id.of_string s)
                          in
                           final_env,final_idrefs,
                            (hid,(n,Acic.Def (at,dummy_never_used)))::atl
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index abd6b3b73..83a4d425b 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -21,6 +21,8 @@ let verbose = ref false;;
 let print_if_verbose s = if !verbose then print_string s;;
 
 open Decl_kinds
+open Names
+open Util
 
 (* filter_params pvars hyps *)
 (* filters out from pvars (which is a list of lists) all the variables *)
@@ -35,18 +37,19 @@ let filter_params pvars hyps =
       let ids' = id::ids in
       let ids'' =
        "cic:/" ^
-        String.concat "/" (List.rev_map Names.Id.to_string ids') in
+        String.concat "/" (List.rev_map Id.to_string ids') in
       let he' =
-       ids'', List.rev (List.filter (function x -> List.mem x hyps) he) in
+       ids'', List.rev (List.filter (function x -> String.List.mem x hyps) he)
+      in
       let tl' = aux ids' tl in
        match he' with
           _,[] -> tl'
         | _,_  -> he'::tl'
  in
   let cwd = Lib.cwd () in
-  let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in
+  let cwdsp = Libnames.make_path cwd (Id.of_string "dummy") in
   let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
-   aux (Names.DirPath.repr modulepath) (List.rev pvars)
+   aux (DirPath.repr modulepath) (List.rev pvars)
 ;;
 
 (* The computation is very inefficient, but we can't do anything *)
@@ -54,15 +57,15 @@ let filter_params pvars hyps =
 (* module.                                                       *)
 let search_variables () =
   let cwd = Lib.cwd () in
-  let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in
+  let cwdsp = Libnames.make_path cwd (Id.of_string "dummy") in
   let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
    let rec aux =
     function
        [] -> []
      | he::tl as modules ->
         let one_section_variables =
-         let dirpath = Names.DirPath.make (modules @ Names.DirPath.repr modulepath) in
-          let t = List.map Names.Id.to_string (Decls.last_section_hyps dirpath) in
+         let dirpath = DirPath.make (modules @ DirPath.repr modulepath) in
+          let t = List.map Id.to_string (Decls.last_section_hyps dirpath) in
            [he,t]
         in
          one_section_variables @ aux tl
@@ -110,7 +113,7 @@ let theory_filename xml_library_root =
   match xml_library_root with
     None -> None  (* stdout *)
   | Some xml_library_root' ->
-     let toks = List.map Names.Id.to_string (Names.DirPath.repr (Lib.library_dp ())) in
+     let toks = List.map Id.to_string (DirPath.repr (Lib.library_dp ())) in
      (* theory from A/B/C/F.v goes into A/B/C/F.theory *)
      let alltoks = List.rev toks in
        Some (join_dirs xml_library_root' alltoks ^ ".theory")
@@ -150,7 +153,7 @@ let print_object uri obj sigma filename =
 
 let string_list_of_named_context_list =
  List.map
-  (function (n,_,_) -> Names.Id.to_string n)
+  (function (n,_,_) -> Id.to_string n)
 ;;
 
 (* Function to collect the variables that occur in a term. *)
@@ -159,7 +162,7 @@ let string_list_of_named_context_list =
 let find_hyps t =
   let rec aux l t =
    match Term.kind_of_term t with
-      Term.Var id when not (List.mem id l) ->
+      Term.Var id when not (Id.List.mem id l) ->
        let (_,bo,ty) = Global.lookup_named id in
         let boids =
          match bo with
@@ -193,7 +196,7 @@ let find_hyps t =
   and map_and_filter l =
    function
       [] -> []
-    | (n,_,_)::tl when not (List.mem n l) -> n::(map_and_filter l tl)
+    | (n,_,_)::tl when not (Id.List.mem n l) -> n::(map_and_filter l tl)
     | _::tl -> map_and_filter l tl
   in
    aux [] t
@@ -208,11 +211,11 @@ let mk_variable_obj id body typ =
    | Some bo -> find_hyps bo, Some (Unshare.unshare bo)
  in
   let hyps' = find_hyps typ @ hyps in
-  let hyps'' = List.map Names.Id.to_string hyps' in
+  let hyps'' = List.map Id.to_string hyps' in
   let variables = search_variables () in
   let params = filter_params variables hyps'' in
    Acic.Variable
-    (Names.Id.to_string id, unsharedbody, Unshare.unshare typ, params)
+    (Id.to_string id, unsharedbody, Unshare.unshare typ, params)
 ;;
 
 
@@ -222,10 +225,10 @@ let mk_constant_obj id bo ty variables hyps =
  let params = filter_params variables hyps in
   match bo with
      None ->
-      Acic.Constant (Names.Id.to_string id,None,ty,params)
+      Acic.Constant (Id.to_string id,None,ty,params)
    | Some c ->
       Acic.Constant
-       (Names.Id.to_string id, Some (Unshare.unshare c), ty,params)
+       (Id.to_string id, Some (Unshare.unshare c), ty,params)
 ;;
 
 let mk_inductive_obj sp mib packs variables nparams hyps finite =
@@ -371,7 +374,7 @@ let print internal glob_ref kind xml_library_root =
        let (_,body,typ) = Global.lookup_named id in
         Cic2acic.Variable kn,mk_variable_obj id body typ
     | Globnames.ConstRef kn ->
-       let id = Names.Label.to_id (Names.con_label kn) in
+       let id = Label.to_id (Names.con_label kn) in
        let cb = Global.lookup_constant kn in
        let val0 = Declareops.body_of_constant cb in
        let typ = cb.Declarations.const_type in
@@ -444,7 +447,7 @@ let _ =
          (* I saved in the Pfedit.set_xml_cook_proof callback.          *)
         let fn = filename_of_path xml_library_root (Cic2acic.Constant kn) in
          show_pftreestate internal fn pftreestate
-	  (Names.Label.to_id (Names.con_label kn)) ;
+	  (Label.to_id (Names.con_label kn)) ;
          proof_to_export := None)
 ;;
 
@@ -508,7 +511,7 @@ let _ = Hook.set Lexer.xml_output_comment (theory_output_string ~do_not_quote:tr
 
 let uri_of_dirpath dir =
   "/" ^ String.concat "/"
-    (List.rev_map Names.Id.to_string (Names.DirPath.repr dir))
+    (List.rev_map Id.to_string (DirPath.repr dir))
 ;;
 
 let _ =
@@ -527,5 +530,5 @@ let _ =
   Hook.set Library.xml_require
     (fun d -> theory_output_string
       (Printf.sprintf "<b>Require</b> <a helm:helm_link=\"href\" href=\"theory:%s.theory\">%s</a>.<br/>"
-       (uri_of_dirpath d) (Names.DirPath.to_string d)))
+       (uri_of_dirpath d) (DirPath.to_string d)))
 ;;