Removing some lone List.assoc & List.mem in lib.

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

11 files changed, 35 insertions, 70 deletions

diff --git a/lib/cList.ml b/lib/cList.ml
index e3d5f080b..cf2a54c4b 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -88,7 +88,6 @@ sig
   val smartfilter : ('a -> bool) -> 'a list -> 'a list
   val index : 'a -> 'a list -> int
   val index_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
-  val unique_index : 'a -> 'a list -> int
   val index0 : 'a -> 'a list -> int
   val index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
   val iteri :  (int -> 'a -> unit) -> 'a list -> unit
@@ -425,16 +424,6 @@ let index x =
 
 let index0 x l = index x l - 1
 
-let unique_index x =
-  let rec index_x n = function
-    | y::l ->
-        if x = y then
-          if List.mem x l then raise Not_found
-          else n
-        else index_x (succ n) l
-    | [] -> raise Not_found
-  in index_x 1
-
 let fold_right_i f i l =
   let rec it_f i l a = match l with
     | [] -> a
diff --git a/lib/cList.mli b/lib/cList.mli
index af378a37f..a82759daa 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -135,9 +135,6 @@ sig
 
   val index_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int
 
-  val unique_index : 'a -> 'a list -> int
-  (** [unique_index x l] returns [Not_found] if [x] doesn't occur exactly once. *)
-
   val index0 : 'a -> 'a list -> int
   (** [index0] behaves as [index] except that it starts counting at 0. *)
 
diff --git a/lib/dyn.ml b/lib/dyn.ml
index aec707123..93f19fce9 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -15,7 +15,7 @@ type t = string * Obj.t
 let dyntab = ref ([] : string list)
 
 let create s =
-  if List.mem s !dyntab then
+  if List.exists (fun s' -> CString.equal s s') !dyntab then
     anomaly ~label:"Dyn.create" (Pp.str ("already declared dynamic " ^ s));
   dyntab := s :: !dyntab;
   ((fun v -> (s,Obj.repr v)),
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index b33a20058..9a5f20f0c 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -92,15 +92,6 @@ let recursive_hcons h u =
   let rec hrec x = hc (hrec,u) x in
   hrec
 
-(* If the structure may contain loops, use this one. *)
-let recursive_loop_hcons h u =
-  let hc = h () in
-  let rec hrec visited x =
-    if List.memq x visited then x
-    else hc (hrec (x::visited),u) x
-  in
-  hrec []
-
 (* For 2 mutually recursive types *)
 let recursive2_hcons h1 h2 u1 u2 =
   let hc1 = h1 () in
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index ae7d6b9d9..255cb0430 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -75,11 +75,6 @@ val simple_hcons : (unit -> 'u -> 't -> 't) -> ('u -> 't -> 't)
 val recursive_hcons : (unit -> ('t -> 't) * 'u -> 't -> 't) -> ('u -> 't -> 't)
 (** As [simple_hcons] but intended to be used with well-founded data structures. *)
 
-val recursive_loop_hcons :
-    (unit -> ('t -> 't) * 'u -> 't -> 't) -> ('u -> 't -> 't)
-(** As [simple_hcons] but intended to be used with any recursive data structure,
-    in particular if they contain loops. *)
-
 val recursive2_hcons :
   (unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u1 -> 't1 -> 't1) ->
     (unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u2 -> 't2 -> 't2) ->
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 556881332..16789cd3d 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -8,7 +8,6 @@
 
 open Util
 
-
 (* Type of regular trees:
    - Param denotes tree variables (like de Bruijn indices)
      the first int is the depth of the occurrence, and the second int
@@ -65,12 +64,13 @@ let rec expand = function
    directly one of the parameters of depth 0. Some care is taken to
    accept definitions like  rec X=Y and Y=f(X,Y) *)
 let mk_rec defs =
-  let rec check histo d =
-    match expand d with
-        Param(0,j) when List.mem j histo -> failwith "invalid rec call"
-      | Param(0,j) -> check (j::histo) defs.(j)
-      | _ -> () in
-  Array.mapi (fun i d -> check [i] d; Rec(i,defs)) defs
+  let rec check histo d = match expand d with
+  | Param (0, j) ->
+    if Int.Set.mem j histo then failwith "invalid rec call"
+    else check (Int.Set.add j histo) defs.(j)
+  | _ -> ()
+  in
+  Array.mapi (fun i d -> check (Int.Set.singleton i) d; Rec(i,defs)) defs
 (*
 let v(i,j) = lift i (mk_rec_calls(j+1)).(j);;
 let r = (mk_rec[|(mk_rec[|v(1,0)|]).(0)|]).(0);;
diff --git a/lib/serialize.ml b/lib/serialize.ml
index c6eaa4eda..5c818ad61 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -183,8 +183,17 @@ exception Marshal_error
 
 (** Utility functions *)
 
+let rec has_flag (f : string) = function
+| [] -> false
+| (k, _) :: l -> CString.equal k f || has_flag f l
+
+let rec get_attr attr = function
+| [] -> raise Not_found
+| (k, v) :: l ->
+  if CString.equal k attr then v else get_attr attr l
+
 let massoc x l =
-  try List.assoc x l
+  try get_attr x l
   with Not_found -> raise Marshal_error
 
 let constructor t c args = Element (t, ["val", c], args)
@@ -364,7 +373,7 @@ let of_edit_or_state_id = function
   | Interface.State id -> ["object","state"], of_state_id id
 let to_edit_or_state_id attrs xml =
   try
-    let obj = List.assoc "object" attrs in
+    let obj = get_attr "object" attrs in
     if obj = "edit"then Interface.Edit (to_edit_id xml)
     else if obj = "state" then Interface.State (to_state_id xml)
     else raise Marshal_error
@@ -385,8 +394,8 @@ let to_value f = function
   else if ans = "fail" then
     let loc =
       try
-        let loc_s = int_of_string (List.assoc "loc_s" attrs) in
-        let loc_e = int_of_string (List.assoc "loc_e" attrs) in
+        let loc_s = int_of_string (get_attr "loc_s" attrs) in
+        let loc_e = int_of_string (get_attr "loc_e" attrs) in
         Some (loc_s, loc_e)
       with Not_found | Failure _ -> None
     in
@@ -435,9 +444,9 @@ let to_call = function
   let ans = massoc "val" attrs in
   begin match ans with
   | "interp" ->
-    let id = List.assoc "id" attrs in
-    let raw = List.mem_assoc "raw" attrs in
-    let vrb = List.mem_assoc "verbose" attrs in
+    let id = get_attr "id" attrs in
+    let raw = has_flag "raw" attrs in
+    let vrb = has_flag "verbose" attrs in
     Interp (int_of_string id, raw, vrb, raw_string l)
   | "backto" ->
       (match l with
@@ -446,7 +455,7 @@ let to_call = function
   | "goal" -> Goal ()
   | "evars" -> Evars ()
   | "status" ->
-      let force = List.assoc "force" attrs in
+      let force = get_attr "force" attrs in
       Status (bool_of_string force)
   | "search" ->
     let args = List.map (to_pair to_search_constraint to_bool) l in
@@ -576,8 +585,8 @@ let of_loc loc =
 let to_loc xml = match xml with
 | Element ("loc", l,[]) ->
     (try
-      let start = List.assoc "start" l in
-      let stop = List.assoc "stop" l in
+      let start = get_attr "start" l in
+      let stop = get_attr "stop" l in
       Loc.make_loc (int_of_string start, int_of_string stop)
     with Not_found | Invalid_argument _ -> raise Marshal_error)
 | _ -> raise Marshal_error
diff --git a/lib/system.ml b/lib/system.ml
index 37b8dee4c..fea061b04 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -23,8 +23,8 @@ let skipped_dirnames = ref ["CVS"; "_darcs"]
 let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames
 
 let ok_dirname f =
-  not (String.equal f "") && f.[0] != '.' &&
-  not (List.mem f !skipped_dirnames) &&
+  not (String.is_empty f) && f.[0] != '.' &&
+  not (List.exists (String.equal f) !skipped_dirnames) &&
   (match Unicode.ident_refutation f with None -> true | _ -> false)
 
 let all_subdirs ~unix_path:root =
diff --git a/lib/util.ml b/lib/util.ml
index 35220261c..b7364cbc5 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -44,12 +44,6 @@ end
 
 module String : CString.ExtS = CString
 
-let parse_loadpath s =
-  let l = String.split '/' s in
-  if List.mem "" l then
-    invalid_arg "parse_loadpath: find an empty dir in loadpath";
-  l
-
 let subst_command_placeholder s t =
   let buff = Buffer.create (String.length s + String.length t) in
   let i = ref 0 in
diff --git a/lib/util.mli b/lib/util.mli
index 34aa0e1ab..72217fd0e 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -48,7 +48,6 @@ module String : CString.ExtS
 
 (** Substitute %s in the first chain by the second chain *)
 val subst_command_placeholder : string -> string -> string
-val parse_loadpath : string -> string list
 
 (** {6 Lists. } *)
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 29eb9e9ec..033f46062 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -775,21 +775,12 @@ let add_transparency l b local dbnames =
     dbnames
 
 let add_extern pri pat tacast local dbname =
-  (* We check that all metas that appear in tacast have at least
-     one occurence in the left pattern pat *)
-  let tacmetas = [] in
-    match pat with
-    | Some (patmetas,pat) ->
-	(match (List.subtract tacmetas patmetas) with
-	| i::_ ->
-	    errorlabstrm "add_extern"
-	      (str "The meta-variable ?" ++ Ppconstr.pr_patvar i ++ str" is not bound.")
-	| []  ->
-	    Lib.add_anonymous_leaf
-	      (inAutoHint(local,dbname, AddHints [make_extern pri (Some pat) tacast])))
-    | None ->
-	Lib.add_anonymous_leaf
-	  (inAutoHint(local,dbname, AddHints [make_extern pri None tacast]))
+  let pat = match pat with
+  | None -> None
+  | Some (_, pat) -> Some pat
+  in
+  let hint = local, dbname, AddHints [make_extern pri pat tacast] in
+  Lib.add_anonymous_leaf (inAutoHint hint)
 
 let add_externs pri pat tacast local dbnames =
   List.iter (add_extern pri pat tacast local) dbnames