From 90a73b08da2fe80b0298997f1f9adb65afdfbf54 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Wed, 28 Aug 2013 07:44:10 +0000 Subject: 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 --- lib/cList.ml | 11 ----------- lib/cList.mli | 3 --- lib/dyn.ml | 2 +- lib/hashcons.ml | 9 --------- lib/hashcons.mli | 5 ----- lib/rtree.ml | 14 +++++++------- lib/serialize.ml | 29 +++++++++++++++++++---------- lib/system.ml | 4 ++-- lib/util.ml | 6 ------ lib/util.mli | 1 - tactics/auto.ml | 21 ++++++--------------- 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 -- cgit v1.2.3