diff options
71 files changed, 334 insertions, 233 deletions
diff --git a/checker/check.ml b/checker/check.ml index f1fe3b8c5..366eb3695 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -339,7 +339,7 @@ let rec intern_library seen (dir, f) needed = try let _ = find_library dir in needed with Not_found -> (* Look if already listed and consequently its dependencies too *) - if List.mem_assoc dir needed then needed + if List.mem_assoc_f DirPath.equal dir needed then needed else (* [dir] is an absolute name which matches [f] which must be in loadpath *) let m = intern_from_file (dir,f) in diff --git a/checker/closure.ml b/checker/closure.ml index 4500d371c..6744269ec 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -180,7 +180,7 @@ let ref_value_cache info ref = let body = match ref with | RelKey n -> - let (s,l) = info.i_rels in lift n (List.assoc_f Int.equal (s-n) l) + let (s,l) = info.i_rels in lift n (Int.List.assoc (s-n) l) | VarKey id -> raise Not_found | ConstKey cst -> constant_value info.i_env cst in diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 539a36331..9f0f5844b 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -254,7 +254,8 @@ let typecheck_one_inductive env params mib mip = (* mind_kelim: checked by positivity criterion ? *) let sorts = compute_elim_sorts env params mib mip.mind_arity mip.mind_nf_lc in - if List.exists (fun s -> not (List.mem s sorts)) mip.mind_kelim then + let reject_sort s = not (List.mem_f family_equal s sorts) in + if List.exists reject_sort mip.mind_kelim then failwith "elimination not allowed"; (* mind_recargs: checked by positivity criterion *) () diff --git a/checker/term.ml b/checker/term.ml index 371889436..ea81f5dab 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -23,6 +23,8 @@ let family_of_sort = function | Prop Pos -> InSet | Type _ -> InType +let family_equal = (==) + (********************************************************************) (* Constructions as implemented *) (********************************************************************) diff --git a/checker/term.mli b/checker/term.mli index 68b408617..f75341b9d 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -2,6 +2,7 @@ open Names open Cic val family_of_sort : sorts -> sorts_family +val family_equal : sorts_family -> sorts_family -> bool val strip_outer_cast : constr -> constr val collapse_appl : constr -> constr diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 2c44d6da3..8337e96f0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -364,7 +364,7 @@ let reset_hidden_inductive_implicit_test env = let check_hidden_implicit_parameters id impls = if Id.Map.exists (fun _ -> function - | (Inductive indparams,_,_,_) -> List.mem id indparams + | (Inductive indparams,_,_,_) -> Id.List.mem id indparams | _ -> false) impls then errorlabstrm "" (strbrk "A parameter of an inductive type " ++ @@ -456,7 +456,8 @@ let intern_generalization intern env lvar loc bk ak c = | None -> false | Some sc -> String.equal sc Notation.type_scope in - is_type_scope || List.mem Notation.type_scope env.scopes + is_type_scope || + String.List.mem Notation.type_scope env.scopes in if pi then (fun (id, loc') acc -> @@ -812,10 +813,10 @@ let product_of_cases_patterns ids idspl = (* @return the first variable that occurs twice in a pattern -naive n2 algo *) +naive n^2 algo *) let rec has_duplicate = function | [] -> None - | x::l -> if List.mem x l then (Some x) else has_duplicate l + | x::l -> if Id.List.mem x l then (Some x) else has_duplicate l let loc_of_lhs lhs = Loc.merge (fst (List.hd lhs)) (fst (List.last lhs)) diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 734b330e7..4d4fe9117 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -83,7 +83,7 @@ let ungeneralizable loc id = let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let found loc id bdvars l = - if List.mem id l then l + if Id.List.mem id l then l else if is_freevar bdvars (Global.env ()) id then if find_generalizable_ident id then id :: l @@ -124,7 +124,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp let rec vars bound vs = function | GVar (loc,id) -> if is_freevar bound (Global.env ()) id then - if List.mem_assoc id vs then vs + if Id.List.mem_assoc id vs then vs else (id, loc) :: vs else vs | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) @@ -219,9 +219,8 @@ let combine_params avoid fn applied needed = match app, need with [], [] -> List.rev ids, avoid - | app, (_, (Name id, _, _)) :: need - when List.mem_assoc_f Id.equal id named -> - aux (List.assoc_f Id.equal id named :: ids) avoid app need + | app, (_, (Name id, _, _)) :: need when Id.List.mem_assoc id named -> + aux (Id.List.assoc id named :: ids) avoid app need | (x, None) :: app, (None, (Name id, _, _)) :: need -> aux (x :: ids) avoid app need diff --git a/interp/notation.ml b/interp/notation.ml index b661c33c6..5fa6346f0 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -121,7 +121,7 @@ let scope_stack = ref [] let current_scopes () = !scope_stack let scope_is_open_in_scopes sc l = - List.mem (Scope sc) l + List.exists (function Scope sc' -> String.equal sc sc' | _ -> false) l let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack) @@ -841,19 +841,18 @@ let browse_notation strict ntn map = if String.contains ntn ' ' then String.equal ntn ntn' else let toks = decompose_notation_key ntn' in - let trms = List.filter (function Terminal _ -> true | _ -> false) toks in - if strict then match trms with - | [Terminal ntn'] -> String.equal ntn ntn' - | _ -> false - else - List.mem (Terminal ntn) trms in + let get_terminals = function Terminal ntn -> Some ntn | _ -> None in + let trms = List.map_filter get_terminals toks in + if strict then String.List.equal [ntn] trms + else String.List.mem ntn trms + in let l = String.Map.fold (fun scope_name sc -> String.Map.fold (fun ntn ((_,r),df) l -> if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations) map [] in - List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l + List.sort (fun x y -> String.compare (fst x) (fst y)) l let global_reference_of_notation test (ntn,(sc,c,_)) = match c with @@ -917,20 +916,20 @@ let collect_notation_in_scope scope sc known = assert (not (String.equal scope default_scope)); String.Map.fold (fun ntn ((_,r),(_,df)) (l,known as acc) -> - if List.mem ntn known then acc else ((df,r)::l,ntn::known)) + if String.List.mem ntn known then acc else ((df,r)::l,ntn::known)) sc.notations ([],known) let collect_notations stack = fst (List.fold_left (fun (all,knownntn as acc) -> function | Scope scope -> - if List.mem_assoc scope all then acc + if String.List.mem_assoc scope all then acc else let (l,knownntn) = collect_notation_in_scope scope (find_scope scope) knownntn in ((scope,l)::all,knownntn) | SingleNotation ntn -> - if List.mem ntn knownntn then (all,knownntn) + if String.List.mem ntn knownntn then (all,knownntn) else let ((_,r),(_,df)) = String.Map.find ntn (find_scope default_scope).notations in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 50cbcd605..d469f36fa 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -22,14 +22,6 @@ open Decl_kinds (**********************************************************************) (* Re-interpret a notation as a glob_constr, taking care of binders *) -module IdList = struct - let assoc id l = List.assoc_f Id.equal id l - let remove_assoc id l = List.remove_assoc_f Id.equal id l - let mem id l = List.exists (Id.equal id) l - let mem_assoc id l = List.exists (fun (a,_) -> Id.equal id a) l - let rev_mem_assoc id l = List.exists (fun (_,b) -> Id.equal id b) l -end - let name_to_ident = function | Anonymous -> Errors.error "This expression should be a simple identifier." | Name id -> id @@ -45,15 +37,15 @@ let rec cases_pattern_fold_map loc g e = function e', PatCstr (loc,cstr,patl',na') let rec subst_glob_vars l = function - | GVar (_,id) as r -> (try IdList.assoc id l with Not_found -> r) + | GVar (_,id) as r -> (try Id.List.assoc id l with Not_found -> r) | GProd (loc,Name id,bk,t,c) -> let id = - try match IdList.assoc id l with GVar(_,id') -> id' | _ -> id + try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in GProd (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) | GLambda (loc,Name id,bk,t,c) -> let id = - try match IdList.assoc id l with GVar(_,id') -> id' | _ -> id + try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *) @@ -313,18 +305,18 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) = let useless_vars = Id.Map.fold fold recvars Id.Set.empty in let vars = Id.Map.filter (fun y _ -> not (Id.Set.mem y useless_vars)) vars in let check_recvar x = - if IdList.mem x found then + if Id.List.mem x found then errorlabstrm "" (pr_id x ++ strbrk " should only be used in the recursive part of a pattern.") in let check (x, y) = check_recvar x; check_recvar y in let () = List.iter check foundrec in let () = List.iter check foundrecbinding in let check_bound x = - if not (IdList.mem x found) then - if IdList.mem_assoc x foundrec || - IdList.mem_assoc x foundrecbinding || - IdList.rev_mem_assoc x foundrec || - IdList.rev_mem_assoc x foundrecbinding + if not (Id.List.mem x found) then + if Id.List.mem_assoc x foundrec || + Id.List.mem_assoc x foundrecbinding || + Id.List.mem_assoc_sym x foundrec || + Id.List.mem_assoc_sym x foundrecbinding then error (Id.to_string x ^ @@ -526,11 +518,11 @@ let add_env alp (sigma,sigmalist,sigmabinders) var v = let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v = try - let v' = IdList.assoc var sigma in + let v' = Id.List.assoc var sigma in match v, v' with | GHole _, _ -> fullsigma | _, GHole _ -> - add_env alp (IdList.remove_assoc var sigma,sigmalist,sigmabinders) var v + add_env alp (Id.List.remove_assoc var sigma,sigmalist,sigmabinders) var v | _, _ -> if Pervasives.(=) v v' then fullsigma (** FIXME *) else raise No_match @@ -558,7 +550,7 @@ let match_opt f sigma t1 t2 = match (t1,t2) with | _ -> raise No_match let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with - | (_,Name id2) when IdList.mem id2 (fst metas) -> + | (_,Name id2) when Id.List.mem id2 (fst metas) -> let rhs = match na1 with | Name id1 -> GVar (Loc.ghost,id1) | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole) in @@ -589,15 +581,15 @@ let rec match_iterated_binders islambda decls = function | b -> (decls,b) let remove_sigma x (sigmavar,sigmalist,sigmabinders) = - (IdList.remove_assoc x sigmavar,sigmalist,sigmabinders) + (Id.List.remove_assoc x sigmavar,sigmalist,sigmabinders) let match_abinderlist_with_app match_fun metas sigma rest x iter termin = let rec aux sigma acc rest = try let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in - let rest = IdList.assoc ldots_var (pi1 sigma) in + let rest = Id.List.assoc ldots_var (pi1 sigma) in let b = - match IdList.assoc x (pi3 sigma) with [b] -> b | _ ->assert false + match Id.List.assoc x (pi3 sigma) with [b] -> b | _ ->assert false in let sigma = remove_sigma x (remove_sigma ldots_var sigma) in aux sigma (b::acc) rest @@ -610,8 +602,8 @@ let match_alist match_fun metas sigma rest x iter termin lassoc = let rec aux sigma acc rest = try let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in - let rest = IdList.assoc ldots_var (pi1 sigma) in - let t = IdList.assoc x (pi1 sigma) in + let rest = Id.List.assoc ldots_var (pi1 sigma) in + let t = Id.List.assoc x (pi1 sigma) in let sigma = remove_sigma x (remove_sigma ldots_var sigma) in aux sigma (t::acc) rest with No_match when not (List.is_empty acc) -> @@ -635,7 +627,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = match (a1,a2) with (* Matching notation variable *) - | r1, NVar id2 when IdList.mem id2 tmetas -> bind_env alp sigma id2 r1 + | r1, NVar id2 when Id.List.mem id2 tmetas -> bind_env alp sigma id2 r1 (* Matching recursive notations for terms *) | r1, NList (x,_,iter,termin,lassoc) -> @@ -656,10 +648,10 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin (* Matching individual binders as part of a recursive pattern *) - | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when IdList.mem id blmetas -> + | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when Id.List.mem id blmetas -> match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 | GProd (_,na,bk,t,b1), NProd (Name id,_,b2) - when IdList.mem id blmetas && na != Anonymous -> + when Id.List.mem id blmetas && na != Anonymous -> match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 (* Matching compositionally *) @@ -773,7 +765,7 @@ let match_notation_constr u c (metas,pat) = let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in (* Reorder canonically the substitution *) let find x = - try IdList.assoc x terms + try Id.List.assoc x terms with Not_found -> (* Happens for binders bound to Anonymous *) (* Find a better way to propagate Anonymous... *) @@ -783,9 +775,9 @@ let match_notation_constr u c (metas,pat) = | NtnTypeConstr -> ((find x, scl)::terms',termlists',binders') | NtnTypeConstrList -> - (terms',(IdList.assoc x termlists,scl)::termlists',binders') + (terms',(Id.List.assoc x termlists,scl)::termlists',binders') | NtnTypeBinderList -> - (terms',termlists',(IdList.assoc x binders,scl)::binders')) + (terms',termlists',(Id.List.assoc x binders,scl)::binders')) metas ([],[],[]) (* Matching cases pattern *) @@ -796,7 +788,7 @@ let add_patterns_for_params ind l = let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v = try - let vvar = IdList.assoc var sigma in + let vvar = Id.List.assoc var sigma in if Pervasives.(=) v vvar then fullsigma else raise No_match (** FIXME *) with Not_found -> (* TODO: handle the case of multiple occs in different scopes *) @@ -804,7 +796,7 @@ let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v = let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with - | r1, NVar id2 when IdList.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) + | r1, NVar id2 when Id.List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) | PatVar (_,Anonymous), NHole _ -> sigma,(0,[]) | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> sigma,(0,add_patterns_for_params (fst r1) largs) @@ -846,8 +838,8 @@ let match_ind_pattern metas sigma ind pats a2 = let reorder_canonically_substitution terms termlists metas = List.fold_right (fun (x,(scl,typ)) (terms',termlists') -> match typ with - | NtnTypeConstr -> ((IdList.assoc x terms, scl)::terms',termlists') - | NtnTypeConstrList -> (terms',(IdList.assoc x termlists,scl)::termlists') + | NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists') + | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists') | NtnTypeBinderList -> assert false) metas ([],[]) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 832af5331..7c9db3ef7 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -141,7 +141,7 @@ let fold_constr_expr_with_binders g f n acc = function let free_vars_of_constr_expr c = let rec aux bdvars l = function - | CRef (Ident (_,id)) -> if List.mem id bdvars then l else Id.Set.add id l + | CRef (Ident (_,id)) -> if Id.List.mem id bdvars then l else Id.Set.add id l | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c in aux [] Id.Set.empty c diff --git a/kernel/closure.ml b/kernel/closure.ml index 98fb467c8..41338c1cc 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -250,7 +250,7 @@ let ref_value_cache info ref = | None -> raise Not_found | Some t -> lift n t end - | VarKey id -> List.assoc_f Id.equal id info.i_vars + | VarKey id -> Id.List.assoc id info.i_vars | ConstKey cst -> constant_value info.i_env cst in let v = info.i_repr info body in diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 9d2580ce4..50c052abb 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -239,6 +239,14 @@ let typecheck_inductive env mie = let inds = Array.of_list inds in let arities = Array.of_list arity_list in + let has_some_univ u = function + | Some v when Universe.equal u v -> true + | _ -> false + in + let remove_some_univ u = function + | Some v when Universe.equal u v -> None + | x -> x + in let fold l (_, b, p) = match b with | None -> (* Parameter contributes to polymorphism only if explicit Type *) @@ -247,8 +255,8 @@ let typecheck_inductive env mie = (* polymorphism unless there is aliasing (i.e. non distinct levels) *) begin match kind_of_term c with | Sort (Type u) -> - if List.mem (Some u) l then - None :: List.map (function Some v when Universe.equal u v -> None | x -> x) l + if List.exists (has_some_univ u) l then + None :: List.map (remove_some_univ u) l else Some u :: l | _ -> diff --git a/kernel/names.ml b/kernel/names.ml index c505017f6..d02e0ce07 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -64,6 +64,8 @@ struct module Pred = Predicate.Make(Self) + module List = String.List + let hcons = String.hcons end diff --git a/kernel/names.mli b/kernel/names.mli index 417e35aaa..16d0ae5d0 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -46,6 +46,9 @@ sig module Pred : Predicate.S with type elt = t (** Predicates over identifiers. *) + module List : List.MonoS with type elt = t + (** Operations over lists of identifiers. *) + val hcons : t -> t (** Hashconsing of identifiers. *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index d656eceb6..fd8844e00 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -615,14 +615,14 @@ let get_rel env id i = List.nth env.env_rel (i-1) else let i = i - env.env_bound in - try List.assoc_f Int.equal i !(env.env_urel) + try Int.List.assoc i !(env.env_urel) with Not_found -> let local = MLlocal (fresh_lname id) in env.env_urel := (i,local) :: !(env.env_urel); local let get_var env id = - try List.assoc_f Id.equal id !(env.env_named) + try Id.List.assoc id !(env.env_named) with Not_found -> let local = MLlocal (fresh_lname (Name id)) in env.env_named := (id, local)::!(env.env_named); @@ -1501,18 +1501,20 @@ let compile_constant env prefix ~interactive con body = let loaded_native_files = ref ([] : string list) +let is_loaded_native_file s = String.List.mem s !loaded_native_files + let register_native_file s = - if not (List.mem s !loaded_native_files) then + if not (is_loaded_native_file s) then loaded_native_files := s :: !loaded_native_files let is_code_loaded ~interactive name = match !name with | NotLinked -> false | LinkedInteractive (s,_) -> - if (interactive && List.mem s !loaded_native_files) then true + if (interactive && is_loaded_native_file s) then true else (name := NotLinked; false) | Linked (s,_) -> - if List.mem s !loaded_native_files then true + if is_loaded_native_file s then true else (name := NotLinked; false) let param_name = Name (id_of_string "params") diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 04deade92..03f1cd265 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -59,6 +59,11 @@ let hash = function let h = Universe.hash u in combinesmall 2 h +module List = struct + let mem = List.memq + let intersect l l' = CList.intersect family_equal l l' +end + module Hsorts = Hashcons.Make( struct diff --git a/kernel/sorts.mli b/kernel/sorts.mli index b64e92fba..2750145f1 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -30,3 +30,8 @@ val family : t -> family val hcons : t -> t val family_equal : family -> family -> bool + +module List : sig + val mem : family -> family list -> bool + val intersect : family list -> family list -> family list +end diff --git a/kernel/univ.ml b/kernel/univ.ml index 9b5c42f56..7f5c71c70 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -950,10 +950,12 @@ let no_upper_constraints u cst = (* Is u mentionned in v (or equals to v) ? *) +let level_list_mem u l = List.mem_f UniverseLevel.equal u l + let univ_depends u v = match u, v with | Atom u, Atom v -> UniverseLevel.equal u v - | Atom u, Max (gel,gtl) -> List.mem u gel || List.mem u gtl + | Atom u, Max (gel,gtl) -> level_list_mem u gel || level_list_mem u gtl | _ -> anomaly (Pp.str "univ_depends given a non-atomic 1st arg") (* Pretty-printing *) diff --git a/lib/cList.ml b/lib/cList.ml index 140728242..02e46092c 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -140,6 +140,16 @@ sig ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list + module type MonoS = sig + type elt + val equal : elt list -> elt list -> bool + val mem : elt -> elt list -> bool + val assoc : elt -> (elt * 'a) list -> 'a + val mem_assoc : elt -> (elt * 'a) list -> bool + val remove_assoc : elt -> (elt * 'a) list -> (elt * 'a) list + val mem_assoc_sym : elt -> ('a * elt) list -> bool + end + end include List @@ -788,3 +798,13 @@ let rec factorize_left cmp = function let al,l' = partition (fun (a',_) -> cmp a a') l in (a,(b::List.map snd al)) :: factorize_left cmp l' | [] -> [] + +module type MonoS = sig + type elt + val equal : elt list -> elt list -> bool + val mem : elt -> elt list -> bool + val assoc : elt -> (elt * 'a) list -> 'a + val mem_assoc : elt -> (elt * 'a) list -> bool + val remove_assoc : elt -> (elt * 'a) list -> (elt * 'a) list + val mem_assoc_sym : elt -> ('a * elt) list -> bool +end diff --git a/lib/cList.mli b/lib/cList.mli index 6b9f2a8c2..6af32fdd0 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -241,6 +241,16 @@ sig (** Keep only those products that do not return None *) val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list + + module type MonoS = sig + type elt + val equal : elt list -> elt list -> bool + val mem : elt -> elt list -> bool + val assoc : elt -> (elt * 'a) list -> 'a + val mem_assoc : elt -> (elt * 'a) list -> bool + val remove_assoc : elt -> (elt * 'a) list -> (elt * 'a) list + val mem_assoc_sym : elt -> ('a * elt) list -> bool + end end include ExtS diff --git a/lib/cString.ml b/lib/cString.ml index 551b62834..842625aa4 100644 --- a/lib/cString.ml +++ b/lib/cString.ml @@ -61,6 +61,7 @@ sig val is_sub : string -> string -> int -> bool module Set : Set.S with type elt = t module Map : CMap.ExtS with type key = t and module Set := Set + module List : CList.MonoS with type elt = t val hcons : string -> string end @@ -191,4 +192,14 @@ end module Set = Set.Make(Self) module Map = CMap.Make(Self) +module List = struct + type elt = string + let mem id l = List.exists (equal id) l + let assoc id l = CList.assoc_f equal id l + let remove_assoc id l = CList.remove_assoc_f equal id l + let mem_assoc id l = List.exists (fun (a,_) -> equal id a) l + let mem_assoc_sym id l = List.exists (fun (_,b) -> equal id b) l + let equal l l' = CList.equal equal l l' +end + let hcons = Hashcons.simple_hcons Hashcons.Hstring.generate () diff --git a/lib/cString.mli b/lib/cString.mli index d8a19c8e4..5f3616231 100644 --- a/lib/cString.mli +++ b/lib/cString.mli @@ -99,6 +99,9 @@ sig module Map : CMap.ExtS with type key = t and module Set := Set (** Finite maps on [string] *) + module List : CList.MonoS with type elt = t + (** Association lists with [string] as keys *) + val hcons : string -> string (** Hashconsing on [string] *) diff --git a/lib/int.ml b/lib/int.ml index 6eb426065..b5519a571 100644 --- a/lib/int.ml +++ b/lib/int.ml @@ -22,3 +22,10 @@ end module Set = Set.Make(Self) module Map = CMap.Make(Self) + +module List = struct + let mem = List.memq + let assoc = List.assq + let mem_assoc = List.mem_assq + let remove_assoc = List.remove_assq +end diff --git a/lib/int.mli b/lib/int.mli index 956432a52..a84798950 100644 --- a/lib/int.mli +++ b/lib/int.mli @@ -18,3 +18,10 @@ val hash : t -> int module Set : Set.S with type elt = t module Map : CMap.ExtS with type key = t and module Set := Set + +module List : sig + val mem : int -> int list -> bool + val assoc : int -> (int * 'a) list -> 'a + val mem_assoc : int -> (int * 'a) list -> bool + val remove_assoc : int -> (int * 'a) list -> (int * 'a) list +end diff --git a/library/goptions.ml b/library/goptions.ml index 87c387080..7ceac2f6a 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -60,7 +60,7 @@ module MakeTable = let nick = nickname A.key let _ = - if List.mem_assoc nick !A.table then + if String.List.mem_assoc nick !A.table then error "Sorry, this table name is already used." module MySet = Set.Make (struct type t = A.t let compare = compare end) @@ -121,7 +121,7 @@ module MakeTable = let string_table = ref [] -let get_string_table k = List.assoc_f String.equal (nickname k) !string_table +let get_string_table k = String.List.assoc (nickname k) !string_table module type StringConvertArg = sig @@ -150,7 +150,7 @@ module MakeStringTable = let ref_table = ref [] -let get_ref_table k = List.assoc_f String.equal (nickname k) !ref_table +let get_ref_table k = String.List.assoc (nickname k) !ref_table module type RefConvertArg = sig @@ -210,8 +210,8 @@ let check_key key = try let _ = get_option key in error "Sorry, this option name is already used." with Not_found -> - if List.mem_assoc (nickname key) !string_table - || List.mem_assoc (nickname key) !ref_table + if String.List.mem_assoc (nickname key) !string_table + || String.List.mem_assoc (nickname key) !ref_table then error "Sorry, this option name is already used." open Libobject diff --git a/library/library.ml b/library/library.ml index 09968c5ae..d2d67f484 100644 --- a/library/library.ml +++ b/library/library.ml @@ -234,9 +234,7 @@ let locate_qualified_library warn qid = let name = Id.to_string base ^ ".vo" in let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in - let dir = - add_dirpath_suffix (List.assoc_f String.equal lpath loadpath) base - in + let dir = add_dirpath_suffix (String.List.assoc lpath loadpath) base in (* Look if loaded *) if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir) (* Otherwise, look for it in the file system *) diff --git a/library/nametab.ml b/library/nametab.ml index fd27ef264..7eb48a714 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -240,7 +240,7 @@ let shortest_qualid ctx uname tab = let push_node node l = match node with - | Absolute (_,o) | Relative (_,o) when not (List.mem o l) -> o::l + | Absolute (_,o) | Relative (_,o) when not (List.mem_f E.equal o l) -> o::l | _ -> l let rec flatten_idmap tab l = diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 959dba132..9561b8130 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -74,7 +74,7 @@ let nmtoken (loc,a) = with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.") let get_xml_attr s al = - try List.assoc_f String.equal s al + try String.List.assoc s al with Not_found -> error ("No attribute "^s) (* Interpreting specific attributes *) @@ -124,7 +124,7 @@ let get_xml_constructor al = (get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al)) let get_xml_binder al = - try Name (ident_of_cdata (List.assoc_f String.equal "binder" al)) + try Name (ident_of_cdata (String.List.assoc "binder" al)) with Not_found -> Anonymous let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al) diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 01f90f6c6..bbac10f0f 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -278,8 +278,7 @@ let rec bind_primary_aliases map pat = List.fold_left bind_primary_aliases map1 lpat let bind_secondary_aliases map subst = - Id.Map.fold - (fun ids idp map -> (ids,List.assoc_f Id.equal idp map)::map) subst map + Id.Map.fold (fun ids idp map -> (ids,Id.List.assoc idp map)::map) subst map let bind_aliases patvars subst patt = let map = bind_primary_aliases [] patt in @@ -349,7 +348,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let inject = function Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp) | Thesis (For rec_occ) -> - if not (List.mem rec_occ pat_vars) then + if not (Id.List.mem rec_occ pat_vars) then errorlabstrm "suppose it is" (str "Variable " ++ Nameops.pr_id rec_occ ++ str " does not occur in pattern."); diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 673b749e1..30ed01c49 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1189,7 +1189,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls | End_patt (id,(nparams,nhyps)),[] -> begin - match List.assoc_f Id.equal id args with + match Id.List.assoc id args with [None,br_args] -> let all_metas = List.init (nparams + nhyps) (fun n -> mkMeta (succ n)) in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 947a1a482..c6bb9faa0 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -141,7 +141,8 @@ let sign_with_implicits r s nb_params = | [] -> [] | sign::s -> let sign' = - if sign == Keep && List.mem i implicits then Kill Kother else sign + if sign == Keep && Int.List.mem i implicits + then Kill Kother else sign in sign' :: add_impl (succ i) s in add_impl (1+nb_params) s @@ -657,7 +658,8 @@ and extract_cst_app env mle mlt kn args = (* Can we instantiate types variables for this constant ? *) (* In Ocaml, inside the definition of this constant, the answer is no. *) let instantiated = - if lang () == Ocaml && List.mem kn !current_fixpoints then var2var' (snd schema) + if lang () == Ocaml && List.mem_f Constant.equal kn !current_fixpoints + then var2var' (snd schema) else instantiation schema in (* Then the expected type of this constant. *) @@ -1048,7 +1050,7 @@ let extract_inductive env kn = | [] -> [] | t::l -> let l' = filter (succ i) l in - if isDummy (expand env t) || List.mem i implicits then l' + if isDummy (expand env t) || Int.List.mem i implicits then l' else t::l' in filter (1+ind.ind_nparams) l in diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 1e6a1fffc..22e7080e1 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1005,7 +1005,7 @@ let kill_some_lams bl (ids,c) = let kill_dummy_lams c = let ids,c = collect_lams c in let bl = List.map sign_of_id ids in - if not (List.mem Keep bl) then raise Impossible; + if not (List.memq Keep bl) then raise Impossible; let rec fst_kill n = function | [] -> raise Impossible | Kill _ :: bl -> n diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 083108bef..2556460f5 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -32,7 +32,7 @@ let unif t1 t2= match kind_of_term t with Meta i-> (try - head_reduce (List.assoc_f Int.equal i !sigma) + head_reduce (Int.List.assoc i !sigma) with Not_found->t) | _->t in Queue.add (t1,t2) bige; @@ -105,7 +105,7 @@ let mk_rel_inst t= match kind_of_term t with Meta n-> (try - mkRel (d+(List.assoc_f Int.equal n !rel_env)) + mkRel (d+(Int.List.assoc n !rel_env)) with Not_found-> let m= !new_rel in incr new_rel; @@ -117,7 +117,7 @@ let mk_rel_inst t= let unif_atoms i dom t1 t2= try - let t=List.assoc_f Int.equal i (unif t1 t2) in + let t=Int.List.assoc i (unif t1 t2) in if isMeta t then Some (Phantom dom) else Some (Real(mk_rel_inst t,value i t1)) with diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 95aaf4518..8edb16850 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -766,7 +766,7 @@ let build_proof } in build_proof_args do_finalize new_infos g - | Const c when not (List.mem c fnames) -> + | Const c when not (List.mem_f Constant.equal c fnames) -> let new_infos = { dyn_infos with info = (f,args) @@ -915,7 +915,7 @@ let generalize_non_dep hyp g = let hyp_typ = pf_type_of g (mkVar hyp) in let to_revert,_ = Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) -> - if List.mem hyp hyps + if Id.List.mem hyp hyps || List.exists (Termops.occur_var_in_decl env hyp) keep || Termops.occur_var env hyp hyp_typ || Termops.is_section_variable hyp (* should be dangerous *) diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index cb9d12c5e..e65ca94f0 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -367,7 +367,7 @@ let poseq_list_ids lcstr gl = let find_fapp (test:constr -> bool) g : fapp_info list = let pre_res = hdMatchSub (Tacmach.pf_concl g) test in let res = - List.fold_right (fun x acc -> if List.mem x acc then acc else x::acc) pre_res [] in + List.fold_right (List.add_set Pervasives.(=)) pre_res [] in (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res); res) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 91ea714c1..dd02dfe8d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -126,7 +126,7 @@ let rec replace_var_by_term_in_binder x_id term = function | [] -> [] | (bt,t)::l -> (bt,replace_var_by_term x_id term t):: - if List.mem x_id (ids_of_binder bt) + if Id.List.mem x_id (ids_of_binder bt) then l else replace_var_by_term_in_binder x_id term l @@ -134,14 +134,14 @@ let add_bt_names bt = List.append (ids_of_binder bt) let apply_args ctxt body args = let need_convert_id avoid id = - List.exists (is_free_in id) args || List.mem id avoid + List.exists (is_free_in id) args || Id.List.mem id avoid in let need_convert avoid bt = List.exists (need_convert_id avoid) (ids_of_binder bt) in let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) = match na with - | Name id when List.mem id avoid -> + | Name id when Id.List.mem id avoid -> let new_id = Namegen.next_ident_away id avoid in Name new_id,Id.Map.add id new_id mapping,new_id::avoid | _ -> na,mapping,avoid diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index a16b5f0fe..79cba2c7c 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -199,7 +199,7 @@ let rec alpha_pat excluded pat = let new_id = Indfun_common.fresh_id excluded "_x" in PatVar(loc,Name new_id),(new_id::excluded),Id.Map.empty | PatVar(loc,Name id) -> - if List.mem id excluded + if Id.List.mem id excluded then let new_id = Namegen.next_ident_away id excluded in PatVar(loc,Name new_id),(new_id::excluded), @@ -208,7 +208,7 @@ let rec alpha_pat excluded pat = | PatCstr(loc,constr,patl,na) -> let new_na,new_excluded,map = match na with - | Name id when List.mem id excluded -> + | Name id when Id.List.mem id excluded -> let new_id = Namegen.next_ident_away id excluded in Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty | _ -> na,excluded,Id.Map.empty @@ -412,7 +412,7 @@ let is_free_in id = | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t | GCast (_,b,CastCoerce) -> is_free_in b and is_free_in_br (_,ids,_,rt) = - (not (List.mem id ids)) && is_free_in rt + (not (Id.List.mem id ids)) && is_free_in rt in is_free_in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 57019b3fa..a77968092 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -294,7 +294,9 @@ let check_not_nested forbidden e = let rec check_not_nested e = match kind_of_term e with | Rel _ -> () - | Var x -> if List.mem x (forbidden) then error ("check_not_nested : failure "^Id.to_string x) + | Var x -> + if Id.List.mem x forbidden + then error ("check_not_nested : failure "^Id.to_string x) | Meta _ | Evar _ | Sort _ -> () | Cast(e,_,t) -> check_not_nested e;check_not_nested t | Prod(_,t,b) -> check_not_nested t;check_not_nested b @@ -652,7 +654,7 @@ let mkDestructEq : let to_revert = Util.List.map_filter (fun (id, _, t) -> - if List.mem id not_on_hyp || not (Termops.occur_term expr t) + if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t) then None else Some id) hyps in let to_revert_constr = List.rev_map mkVar to_revert in let type_of_expr = pf_type_of g expr in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 5c057231a..4f96d7209 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -140,8 +140,7 @@ let rev_assoc k = let tag_hypothesis,tag_of_hyp, hyp_of_tag = let l = ref ([]:(Id.t * int) list) in (fun h id -> l := (h,id):: !l), - (fun h -> - try List.assoc_f Id.equal h !l with Not_found -> failwith "tag_hypothesis"), + (fun h -> try Id.List.assoc h !l with Not_found -> failwith "tag_hypothesis"), (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis") let hide_constr,find_constr,clear_tables,dump_tables = @@ -1022,7 +1021,7 @@ let replay_history tactic_normalisation = begin try tclTHEN - (List.assoc_f Id.equal (hyp_of_tag e.id) tactic_normalisation) + (Id.List.assoc (hyp_of_tag e.id) tactic_normalisation) (loop l) with Not_found -> loop l end | NEGATE_CONTRADICT (e2,e1,b) :: l -> diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index b74faf30b..4e9ca6ffc 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -546,30 +546,30 @@ let rec depend relie_on accu = function | act :: l -> begin match act with | DIVIDE_AND_APPROX (e,_,_,_) -> - if List.mem e.id relie_on then depend relie_on (act::accu) l + if Int.List.mem e.id relie_on then depend relie_on (act::accu) l else depend relie_on accu l | EXACT_DIVIDE (e,_) -> - if List.mem e.id relie_on then depend relie_on (act::accu) l + if Int.List.mem e.id relie_on then depend relie_on (act::accu) l else depend relie_on accu l | WEAKEN (e,_) -> - if List.mem e relie_on then depend relie_on (act::accu) l + if Int.List.mem e relie_on then depend relie_on (act::accu) l else depend relie_on accu l | SUM (e,(_,e1),(_,e2)) -> - if List.mem e relie_on then + if Int.List.mem e relie_on then depend (e1.id::e2.id::relie_on) (act::accu) l else depend relie_on accu l | STATE {st_new_eq=e;st_orig=o} -> - if List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l + if Int.List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l else depend relie_on accu l | HYP e -> - if List.mem e.id relie_on then depend relie_on (act::accu) l + if Int.List.mem e.id relie_on then depend relie_on (act::accu) l else depend relie_on accu l | FORGET_C _ -> depend relie_on accu l | FORGET _ -> depend relie_on accu l | FORGET_I _ -> depend relie_on accu l | MERGE_EQ (e,e1,e2) -> - if List.mem e relie_on then + if Int.List.mem e relie_on then depend (e1.id::e2::relie_on) (act::accu) l else depend relie_on accu l @@ -673,7 +673,7 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = try let _ = loop2 sys in raise NO_CONTRADICTION with UNSOLVABLE -> let relie_on,path = depend [] [] (history ()) in - let dc,_ = List.partition (fun (_,id,_) -> List.mem id relie_on) decomp in + let dc,_ = List.partition (fun (_,id,_) -> Int.List.mem id relie_on) decomp in let red = List.map (fun (x,_,_) -> x) dc in (red,relie_on,decomp,path)) sys_exploded @@ -705,7 +705,7 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = let s2' = List.map remove_int s2 in let (r1,relie1) = solve s1' and (r2,relie2) = solve s2' in - let (eq,id1,id2) = Util.List.assoc_f Int.equal id explode_map in + let (eq,id1,id2) = Int.List.assoc id explode_map in [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.List.union Int.equal relie1 relie2 with FULL_SOLUTION (x0,x1) -> (x0,x1) diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index af833dacb..5416e936c 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -23,7 +23,7 @@ let string_of_global r = | [] -> "" | m::_ -> let s = Names.Id.to_string m in - if List.mem s meaningful_submodule then s^"." else "" + if Util.String.List.mem s meaningful_submodule then s^"." else "" in prefix^(Names.Id.to_string (Nametab.basename_of_global r)) 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))) ;; diff --git a/pretyping/cases.ml b/pretyping/cases.ml index be62e65b3..d10a52fce 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -496,7 +496,7 @@ let extract_rhs pb = let occur_in_rhs na rhs = match na with | Anonymous -> false - | Name id -> List.mem id rhs.rhs_vars + | Name id -> Id.List.mem id rhs.rhs_vars let is_dep_patt_in eqn = function | PatVar (_,name) -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs @@ -1521,7 +1521,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t = let depvl = free_rels ty in let inst = List.map_i - (fun i _ -> if List.mem i vl then u else mkRel i) 1 + (fun i _ -> if Int.List.mem i vl then u else mkRel i) 1 (rel_context extenv) in let rel_filter = List.map (fun a -> not (isRel a) || dependent a u @@ -1760,7 +1760,7 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c = | Rel n when n > lift -> (try (* Make the predicate dependent on the matched variable *) - let idx = List.assoc_f Int.equal (n - lift) subst in + let idx = Int.List.assoc (n - lift) subst in mkRel (idx + lift) with Not_found -> (* A variable that is not matched, lift over the arsign. *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index aa8f2d08e..63d7b6294 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1179,8 +1179,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = let (evd,evar,(evk',argsv' as ev')) = materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in let ts = expansions_of_var aliases t in - (** FIXME : [List.mem] on constr ???*) - let test c = isEvar c || List.mem c ts in + let test c = isEvar c || List.mem_f Constr.equal c ts in let filter = restrict_upon_filter evd evk test argsv' in let filter = closure_of_filter evd evk' filter in let candidates = extract_candidates sols in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 88702b350..94ff780ec 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -139,7 +139,7 @@ let occur_glob_constr id = || (List.exists occur_pattern pl) | GLetTuple (loc,nal,rtntyp,b,c) -> occur_return_type rtntyp id - || (occur b) || (not (List.mem (Name id) nal) && (occur c)) + || (occur b) || (not (List.mem_f Name.equal (Name id) nal) && (occur c)) | GIf (loc,c,rtntyp,b1,b2) -> occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2) | GRec (loc,fk,idl,bl,tyl,bv) -> @@ -158,7 +158,7 @@ let occur_glob_constr id = | CastVM t | CastNative t -> occur t | CastCoerce -> false) | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false - and occur_pattern (loc,idl,p,c) = not (List.mem id idl) && (occur c) + and occur_pattern (loc,idl,p,c) = not (Id.List.mem id idl) && (occur c) and occur_option = function None -> false | Some p -> occur p diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 23996282c..bf9fd8a10 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -55,7 +55,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind = mib.mind_params_ctxt in - if not (List.mem kind (elim_sorts specif)) then + if not (Sorts.List.mem kind (elim_sorts specif)) then raise (RecursionSchemeError (NotAllowedCaseAnalysis (false, Termops.new_sort_in_family kind, ind))); @@ -508,10 +508,10 @@ let check_arities listdepkind = let _ = List.fold_left (fun ln ((_,ni as mind),mibi,mipi,dep,kind) -> let kelim = elim_sorts (mibi,mipi) in - if not (List.exists ((==) kind) kelim) then raise + if not (Sorts.List.mem kind kelim) then raise (RecursionSchemeError (NotAllowedCaseAnalysis (true, Termops.new_sort_in_family kind,mind))) - else if List.mem ni ln then raise + else if Int.List.mem ni ln then raise (RecursionSchemeError (NotMutualInScheme (mind,mind))) else ni::ln) [] listdepkind diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index b0637a972..812900ea8 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -79,7 +79,7 @@ let mis_is_recursive_subset listind rarg = List.exists (fun ra -> match dest_recarg ra with - | Mrec (_,i) -> List.mem i listind + | Mrec (_,i) -> Int.List.mem i listind | _ -> false) rvec in Array.exists one_is_rec (dest_subterms rarg) diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 22f154795..3bbd8af44 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -27,8 +27,8 @@ let convert_occs = function let is_selected occ = function | AllOccurrences -> true - | AllOccurrencesBut l -> not (List.mem occ l) - | OnlyOccurrences l -> List.mem occ l + | AllOccurrencesBut l -> not (Int.List.mem occ l) + | OnlyOccurrences l -> Int.List.mem occ l | NoOccurrences -> false (** Usual clauses *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 13eb91393..b8dbefb88 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -183,7 +183,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = if not (List.distinct_f Int.compare reversible_rels) then raise Elimconst; List.iteri (fun i t_i -> - if not (List.mem_assoc (i+1) li) then + if not (Int.List.mem_assoc (i+1) li) then let fvs = List.map ((+) (i+1)) (Int.Set.elements (free_rels t_i)) in match List.intersect Int.equal fvs reversible_rels with | [] -> () @@ -888,8 +888,8 @@ let contextually byhead (occs,c) f env sigma t = try let subst = if byhead then matches_head c t else matches c t in let ok = - if nowhere_except_in then List.mem !pos locs - else not (List.mem !pos locs) in + if nowhere_except_in then Int.List.mem !pos locs + else not (Int.List.mem !pos locs) in incr pos; if ok then let subst' = Id.Map.map (traverse envc) subst in @@ -923,8 +923,8 @@ let substlin env evalref n (nowhere_except_in,locs) c = if nowhere_except_in && !pos > maxocc then c else if eq_constr c term then let ok = - if nowhere_except_in then List.mem !pos locs - else not (List.mem !pos locs) in + if nowhere_except_in then Int.List.mem !pos locs + else not (Int.List.mem !pos locs) in incr pos; if ok then value else c else diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 9ecf86698..5fb74dcad 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -625,7 +625,7 @@ type meta_value_map = (metavariable * constr) list let rec subst_meta bl c = match kind_of_term c with - | Meta i -> (try List.assoc_f Int.equal i bl with Not_found -> c) + | Meta i -> (try Int.List.assoc i bl with Not_found -> c) | _ -> map_constr (subst_meta bl) c (* First utilities for avoiding telescope computation for subst_term *) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 9fe95a119..bbcc5727b 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -79,8 +79,8 @@ let e_check_branch_types env evdref ind cj (lfj,explft) = done let max_sort l = - if List.mem InType l then InType else - if List.mem InSet l then InSet else InProp + if Sorts.List.mem InType l then InType else + if Sorts.List.mem InSet l then InSet else InProp let e_is_correct_arity env evdref c pj ind specif params = let arsign = make_arity_signature env true (make_ind_family (ind,params)) in @@ -93,7 +93,8 @@ let e_is_correct_arity env evdref c pj ind specif params = if not (Evarconv.e_cumul env evdref a1 a1') then error (); srec (push_rel (na1,None,a1) env) t ar' | Sort s, [] -> - if not (List.mem (family_of_sort s) allowed_sorts) then error () + if not (Sorts.List.mem (Sorts.family s) allowed_sorts) + then error () | Evar (ev,_), [] -> let s = Termops.new_sort_in_family (max_sort allowed_sorts) in evdref := Evd.define ev (mkSort s) !evdref diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e19be4e12..6cfa6d47f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -960,7 +960,7 @@ and pr_extend s cl = try pr_gen a with Failure _ -> str ("<error in "^s^">") in try - let rls = List.assoc_f String.equal s (Egramml.get_extend_vernac_grammars()) in + let rls = String.List.assoc s (Egramml.get_extend_vernac_grammars()) in let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in let start,rl,cl = match rl with diff --git a/proofs/goal.ml b/proofs/goal.ml index 48cce3fa7..7901ec0a5 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -429,8 +429,10 @@ let rename_hyp_sign id1 id2 sign = let rename_hyp id1 id2 env rdefs gl info = let hyps = hyps env rdefs gl info in if not (Names.Id.equal id1 id2) && - List.mem id2 (Termops.ids_of_named_context (Environ.named_context_of_val hyps)) then - Errors.error ((Names.Id.to_string id2)^" is already used."); + Names.Id.List.mem id2 + (Termops.ids_of_named_context (Environ.named_context_of_val hyps)) + then + Errors.error ((Names.Id.to_string id2)^" is already used."); let new_hyps = rename_hyp_sign id1 id2 hyps in let new_env = Environ.reset_with_named_context new_hyps env in let old_concl = concl env rdefs gl info in diff --git a/proofs/logic.ml b/proofs/logic.ml index 5a29c3b0e..c848a45ab 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -210,7 +210,7 @@ let reorder_val_context env sign ord = let check_decl_position env sign (x,_,_ as d) = let needed = global_vars_set_of_decl env d in let deps = dependency_closure env (named_context_of_val sign) needed in - if List.mem x deps then + if Id.List.mem x deps then error ("Cannot create self-referring hypothesis "^Id.to_string x); x::deps @@ -690,7 +690,9 @@ let prim_refiner r sigma goal = | Rename (id1,id2) -> if !check && not (Id.equal id1 id2) && - List.mem id2 (ids_of_named_context (named_context_of_val sign)) then + Id.List.mem id2 + (ids_of_named_context (named_context_of_val sign)) + then error ((Id.to_string id2)^" is already used."); let sign' = rename_hyp id1 id2 sign in let cl' = replace_vars [id1,mkVar id2] cl in diff --git a/tactics/auto.ml b/tactics/auto.ml index 6050fdc9a..cf8707a46 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -404,7 +404,8 @@ module Hint_db = struct else rebuild_dn st (sl1', sl2', dn) let remove_list grs db = - let filter (_, h) = match h.name with PathHints [gr] -> not (List.mem gr grs) | _ -> true in + let filter (_, h) = + match h.name with PathHints [gr] -> not (List.mem gr grs) | _ -> true in let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in { db with hintdb_map = hintmap; hintdb_nopat = hintnopat } @@ -880,7 +881,7 @@ let interp_hints = HintsExternEntry (pri, pat, tacexp) let add_hints local dbnames0 h = - if List.mem "nocore" dbnames0 then + if String.List.mem "nocore" dbnames0 then error "The hint database \"nocore\" is meant to stay empty."; let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in let env = Global.env() and sigma = Evd.empty in diff --git a/tactics/equality.ml b/tactics/equality.ml index 9bc86a0b9..0864048f9 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -566,7 +566,7 @@ let find_positions env sigma t1 t2 = when Int.equal (List.length args1) (mis_constructor_nargs_env env sp1) -> let sorts = - List.intersect Sorts.family_equal sorts (allowed_sorts env (fst sp1)) + Sorts.List.intersect sorts (allowed_sorts env (fst sp1)) in (* both sides are fully applied constructors, so either we descend, or we can discriminate here. *) @@ -577,7 +577,8 @@ let find_positions env sigma t1 t2 = List.flatten (List.map2_i (fun i -> findrec sorts ((sp1,i)::posn)) 0 rargs1 rargs2) - else if List.mem InType sorts then (* see build_discriminator *) + else if Sorts.List.mem InType sorts + then (* see build_discriminator *) raise (DiscrFound (List.rev posn,sp1,sp2)) else [] @@ -589,7 +590,9 @@ let find_positions env sigma t1 t2 = else let ty1_0 = get_type_of env sigma t1_0 in let s = get_sort_family_of env sigma ty1_0 in - if List.mem s sorts then [(List.rev posn,t1_0,t2_0)] else [] in + if Sorts.List.mem s sorts + then [(List.rev posn,t1_0,t2_0)] else [] + in try (* Rem: to allow injection on proofs objects, just add InProp *) Inr (findrec [InSet;InType] [] t1 t2) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 2a2a1e356..19e7153b5 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -156,7 +156,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let revargs,ownsign = fold_named_context (fun env (id,_,_ as d) (revargs,hyps) -> - if List.mem id ivars then + if Id.List.mem id ivars then ((mkVar id)::revargs,add_named_decl d hyps) else (revargs,hyps)) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 327739378..eb7b28690 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -634,7 +634,9 @@ let eq_env x y = x == y let apply_rule by loccs : (hypinfo * int) pure_strategy = let (nowhere_except_in,occs) = convert_occs loccs in let is_occ occ = - if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in + if nowhere_except_in + then Int.List.mem occ occs + else not (Int.List.mem occ occs) in fun (hypinfo, occ) env avoid t ty cstr evars -> let hypinfo = if not (eq_env hypinfo.cl.env env) then diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index 06a9ab811..aa254c2f8 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -64,7 +64,7 @@ let to_list v = end let is_variable env id = - List.mem id (Termops.ids_of_named_context (Environ.named_context env)) + Id.List.mem id (Termops.ids_of_named_context (Environ.named_context env)) (* Transforms an id into a constr if possible, or fails with Not_found *) let constr_of_id env id = @@ -155,7 +155,7 @@ let coerce_to_evaluable_ref env v = | _ -> fail () else if has_type v (topwit wit_var) then let id = out_gen (topwit wit_var) v in - if List.mem id (Termops.ids_of_context env) then EvalVarRef id + if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id else fail () else let ev = match Value.to_constr v with diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 9e4060752..6b06a0534 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -124,7 +124,7 @@ let lookup_ltacref r = KNmap.find r !mactab let find_ident id ist = Id.Set.mem id ist.ltacvars || - List.mem id (ids_of_named_context (Environ.named_context ist.genv)) + Id.List.mem id (ids_of_named_context (Environ.named_context ist.genv)) let find_recvar qid ist = Id.Map.find qid ist.ltacrecvars @@ -138,7 +138,7 @@ let find_ctxvar id ist = Id.Set.mem id ist.ltacvars let find_ltacvar id ist = Id.Set.mem id ist.ltacvars let find_hyp id ist = - List.mem id (ids_of_named_context (Environ.named_context ist.genv)) + Id.List.mem id (ids_of_named_context (Environ.named_context ist.genv)) (* Globalize a name introduced by Intro/LetTac/... ; it is allowed to *) (* be fresh in which case it is binding later on *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 190c1ba58..0e0ccac2e 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -289,7 +289,7 @@ let extend_values_with_bindings (ln,lm) lfun = (* Evaluation/interpretation *) let is_variable env id = - List.mem id (ids_of_named_context (Environ.named_context env)) + Id.List.mem id (ids_of_named_context (Environ.named_context env)) (* Debug reference *) let debug = ref DebugOff @@ -472,7 +472,7 @@ let rec extract_ids ids lfun = let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let (_, ipat) = out_gen (topwit wit_intro_pattern) v in - if List.mem id ids then accu + if Id.List.mem id ids then accu else accu @ intropattern_ids (dloc, ipat) else accu in @@ -910,7 +910,7 @@ let read_pattern lfun ist env sigma = function (* Reads the hypotheses of a Match Context rule *) let cons_and_check_name id l = - if List.mem id l then + if Id.List.mem id l then user_err_loc (dloc,"read_match_goal_hyps", strbrk ("Hypothesis pattern-matching variable "^(Id.to_string id)^ " used twice in the same pattern.")) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2505a43ad..c1bd8e0c9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1213,7 +1213,7 @@ let specialize mopt (c,lbind) g = tclEVARS clause.evd, term in match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with - | Var id when List.mem id (pf_ids_of_hyps g) -> + | Var id when Id.List.mem id (pf_ids_of_hyps g) -> tclTHEN tac (tclTHENFIRST (fun g -> internal_cut_replace id (pf_type_of g term) g) @@ -1230,7 +1230,7 @@ let keep hyps gl = let ccl = pf_concl gl in let cl,_ = fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) -> - if List.mem hyp hyps + if Id.List.mem hyp hyps || List.exists (occur_var_in_decl env hyp) keep || occur_var env hyp ccl then (clear,decl::keep) @@ -1572,7 +1572,7 @@ let simple_apply_in id c = let generalized_name c t ids cl = function | Name id as na -> - if List.mem id ids then + if Id.List.mem id ids then errorlabstrm "" (pr_id id ++ str " is already used"); na | Anonymous -> @@ -1609,10 +1609,10 @@ let generalize_dep ?(with_let=false) c gl = let to_quantify = Context.fold_named_context seek sign ~init:[] in let to_quantify_rev = List.rev to_quantify in let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in - let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in + let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in let tothin' = match kind_of_term c with - | Var id when mem_named_context id sign && not (List.mem id init_ids) + | Var id when mem_named_context id sign && not (Id.List.mem id init_ids) -> id::tothin | _ -> tothin in @@ -2199,13 +2199,14 @@ let cook_sign hyp0_opt indvars env = indvars too, so add it to indhyps. *) (if Option.is_empty hyp0_opt then indhyps := hyp::!indhyps); MoveFirst (* fake value *) - end else if List.mem hyp indvars then begin + end else if Id.List.mem hyp indvars then begin (* warning: hyp can still occur after induction *) (* e.g. if the goal (t hyp hyp0) with other occs of hyp in t *) indhyps := hyp::!indhyps; rhyp end else - if not (List.is_empty inhyps) && List.mem hyp inhyps || List.is_empty inhyps && + if not (List.is_empty inhyps) && Id.List.mem hyp inhyps || + List.is_empty inhyps && (List.exists (fun id -> occur_var_in_decl env id decl) allindhyps || List.exists (fun (id,_,_) -> occur_var_in_decl env id decl) !decldeps) then begin @@ -2222,11 +2223,11 @@ let cook_sign hyp0_opt indvars env = (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *) let compute_lstatus lhyp (hyp,_,_) = if Id.equal hyp hyp0 then raise (Shunt lhyp); - if List.mem hyp !ldeps then begin + if Id.List.mem hyp !ldeps then begin lstatus := (hyp,lhyp)::!lstatus; lhyp end else - if List.mem hyp !indhyps then lhyp else MoveAfter hyp + if Id.List.mem hyp !indhyps then lhyp else MoveAfter hyp in try let _ = @@ -3156,7 +3157,7 @@ let clear_unselected_context id inhyps cls gl = match cls.onhyps with | Some hyps -> let to_erase (id',_,_ as d) = - if List.mem id' inhyps then (* if selected, do not erase *) None + if Id.List.mem id' inhyps then (* if selected, do not erase *) None else (* erase if not selected and dependent on id or selected hyps *) let test id = occur_var_in_decl (pf_env gl) id d in diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index e63c22bf8..ff1dab46a 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -297,10 +297,10 @@ let build_beq_scheme kn = done; Array.init nb_ind (fun i -> let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in - if not (List.mem InSet kelim) then - raise (NonSingletonProp (kn,i)); - let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in - create_input fix), + if not (Sorts.List.mem InSet kelim) then + raise (NonSingletonProp (kn,i)); + let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in + create_input fix), !eff let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 73fbde781..9ad54ac96 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -140,7 +140,7 @@ let rec complete_signature (k:signature -> unit) (cl,gen,evm:signature) = try evm_fold_rev ( fun ev evi _ -> - if not (is_defined evm ev) && not (List.mem ev gen) then + if not (is_defined evm ev) && not (List.mem_f Evar.equal ev gen) then raise (Continue (ev,evi)) ) evm (); k (cl,gen,evm) with Continue (ev,evi) -> complete_evar (cl,gen,evm) (ev,evi) (complete_signature k) @@ -282,7 +282,7 @@ let gen_sort_topo l evm = if Evd.is_defined evm ev then aux (evar_definition (Evd.find evm ev)) in let r = ref [] in let rec dfs ev = iter_evar dfs ev; - if not(List.mem ev !r) then r := ev::!r in + if not(List.mem_f Evar.equal ev !r) then r := ev::!r in List.iter dfs l; List.rev !r (* register real typeclass instance given a totally defined evd *) diff --git a/toplevel/command.ml b/toplevel/command.ml index 56a370155..3017aeacb 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -475,9 +475,9 @@ let rec partial_order cmp = function let non_full_mutual_message x xge y yge isfix rest = let reason = - if List.mem x yge then + if Id.List.mem x yge then Id.to_string y^" depends on "^Id.to_string x^" but not conversely" - else if List.mem y xge then + else if Id.List.mem y xge then Id.to_string x^" depends on "^Id.to_string y^" but not conversely" else Id.to_string y^" and "^Id.to_string x^" are not mutually dependent" in @@ -805,7 +805,7 @@ let interp_recursive isfix fixl notations = let check_recursive isfix env evd (fixnames,fixdefs,_) = check_evars_are_solved env Evd.empty evd; - if not (List.mem None fixdefs) then begin + if List.for_all Option.has_some fixdefs then begin let fixdefs = List.map Option.get fixdefs in check_mutuality env isfix (List.combine fixnames fixdefs) end @@ -821,7 +821,7 @@ let interp_cofixpoint l ntns = fix,info let declare_fixpoint local ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = - if List.mem None fixdefs then + if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in @@ -848,7 +848,7 @@ let declare_fixpoint local ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = List.iter Metasyntax.add_notation_interpretation ntns let declare_cofixpoint local ((fixnames,fixdefs,fixtypes),fiximps) ntns = - if List.mem None fixdefs then + if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 5846c73a8..4607e70eb 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -149,7 +149,7 @@ let define_mutual_scheme_base kind suff f internal names mind = let cl, eff = f mind in let mib = Global.lookup_mind mind in let ids = Array.init (Array.length mib.mind_packets) (fun i -> - try List.assoc_f Int.equal i names + try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in let consts = Array.map2 (define internal) ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 67c5ba92f..9eabd1df6 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -200,7 +200,7 @@ let declare_one_case_analysis_scheme ind = (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the apropriate type *) - if List.mem InType kelim then + if Sorts.List.mem InType kelim then ignore (define_individual_scheme dep KernelVerbose None ind) (* Induction/recursion schemes *) @@ -222,7 +222,7 @@ let declare_one_induction_scheme ind = let kelim = elim_sorts (mib,mip) in let elims = List.map_filter (fun (sort,kind) -> - if List.mem sort kelim then Some kind else None) + if Sorts.List.mem sort kelim then Some kind else None) (if from_prop then kinds_from_prop else kinds_from_type) in List.iter (fun kind -> ignore (define_individual_scheme kind KernelVerbose None ind)) elims diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 97e50aadb..7452f1f45 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -380,7 +380,7 @@ let rec get_notation_vars = function | NonTerminal id :: sl -> let vars = get_notation_vars sl in if Id.equal id ldots_var then vars else - if List.mem id vars then + if Id.List.mem id vars then error ("Variable "^Id.to_string id^" occurs more than once.") else id::vars @@ -809,14 +809,14 @@ let interp_modifiers modl = (assoc,level,etyps,!onlyparsing,format) | SetEntryType (s,typ) :: l -> let id = Id.of_string s in - if List.mem_assoc id etyps then + if Id.List.mem_assoc id etyps then error (s^" is already assigned to an entry or constr level."); interp assoc level ((id,typ)::etyps) format l | SetItemLevel ([],n) :: l -> interp assoc level etyps format l | SetItemLevel (s::idl,n) :: l -> let id = Id.of_string s in - if List.mem_assoc id etyps then + if Id.List.mem_assoc id etyps then error (s^" is already assigned to an entry or constr level."); let typ = ETConstr (n,()) in interp assoc level ((id,typ)::etyps) format (SetItemLevel (idl,n)::l) @@ -911,9 +911,9 @@ let make_interpretation_vars recvars allvars = let () = List.iter check recvars in let useless_recvars = List.map snd recvars in let mainvars = - Id.Map.filter (fun x _ -> not (List.mem x useless_recvars)) allvars in + Id.Map.filter (fun x _ -> not (Id.List.mem x useless_recvars)) allvars in Id.Map.mapi (fun x (sc, typ) -> - (sc, make_interpretation_type (List.mem_assoc x recvars) typ)) mainvars + (sc, make_interpretation_type (Id.List.mem_assoc x recvars) typ)) mainvars let check_rule_productivity l = if List.for_all (function NonTerminal _ -> true | _ -> false) l then diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index b6e86a212..15e197a98 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -94,7 +94,11 @@ let subst_evar_constr evs n idf t = | _, _ -> acc (*failwith "subst_evars: invalid argument"*) in aux hyps args [] in - if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then + if List.exists + (fun x -> match kind_of_term x with + | Rel n -> Int.List.mem n fixrels + | _ -> false) args + then transparent := Id.Set.add idstr !transparent; mkApp (idf idstr, Array.of_list args) | Fix _ -> @@ -425,7 +429,7 @@ let replace_appvars subst = if isVar f then try let c' = List.map (map_constr aux) l in - let (t, b) = List.assoc_f Id.equal (destVar f) subst in + let (t, b) = Id.List.assoc (destVar f) subst in mkApp (delayed_force hide_obligation, [| prod_applist t c'; applistc b c' |]) with Not_found -> map_constr aux c diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 85e9a30ab..2411eed6e 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -1291,9 +1291,9 @@ let init () = let opts = match !Flags.coq_slave_options with | None -> [] | Some s -> Str.split_delim (Str.regexp ",") s in - if List.mem "fallback-to-lazy-if-marshal-error=no" opts then + if String.List.mem "fallback-to-lazy-if-marshal-error=no" opts then fallback_to_lazy_if_marshal_error := false; - if List.mem "fallback-to-lazy-if-slave-dies=no" opts then + if String.List.mem "fallback-to-lazy-if-slave-dies=no" opts then fallback_to_lazy_if_slave_dies := false; begin try let env_opt = Str.regexp "^extra-env=" in |