From a3a5711d8c2f9f0e12ed707c8b69c828e30bbcf4 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 24 Oct 2013 09:41:19 +0000 Subject: Turn many List.assoc into List.assoc_f git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/decl_mode/decl_interp.ml | 3 ++- plugins/decl_mode/decl_proof_instr.ml | 2 +- plugins/extraction/modutil.ml | 2 +- plugins/firstorder/unify.ml | 6 +++--- plugins/funind/functional_principles_types.ml | 4 ++-- plugins/funind/recdef.ml | 4 ++-- plugins/micromega/sos.ml | 2 +- plugins/omega/coq_omega.ml | 12 ++++++++---- plugins/omega/omega.ml | 2 +- plugins/romega/refl_omega.ml | 2 +- plugins/xml/cic2acic.ml | 2 +- 11 files changed, 23 insertions(+), 18 deletions(-) (limited to 'plugins') diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 8060dcabf..01f90f6c6 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -278,7 +278,8 @@ 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 : Id.t) map -> (ids,List.assoc idp map)::map) subst map + Id.Map.fold + (fun ids idp map -> (ids,List.assoc_f Id.equal idp map)::map) subst map let bind_aliases patvars subst patt = let map = bind_primary_aliases [] patt in diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index e18df6e46..673b749e1 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 id args with + match List.assoc_f Id.equal id args with [None,br_args] -> let all_metas = List.init (nparams + nhyps) (fun n -> mkMeta (succ n)) in diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 45977b657..e6bcefe22 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -213,7 +213,7 @@ let get_decl_in_structure r struc = try let base_mp,ll = labels_of_ref r in if not (at_toplevel base_mp) then error_not_visible r; - let sel = List.assoc base_mp struc in + let sel = List.assoc_f ModPath.equal base_mp struc in let rec go ll sel = match ll with | [] -> assert false | l :: ll -> diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index eeaf270c3..083108bef 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 i !sigma) + head_reduce (List.assoc_f Int.equal 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 n !rel_env)) + mkRel (d+(List.assoc_f Int.equal 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 i (unif t1 t2) in + let t=List.assoc_f Int.equal 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_types.ml b/plugins/funind/functional_principles_types.ml index 58f43ed49..e5d8fe4c1 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -482,7 +482,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in List.map - (function const -> List.assoc const this_block_funs_indexes) + (function cst -> List.assoc_f Constant.equal cst this_block_funs_indexes) funs in let ind_list = @@ -665,7 +665,7 @@ let build_case_scheme fa = let prop_sort = InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in - List.assoc (destConst funs) this_block_funs_indexes + List.assoc_f Constant.equal (destConst funs) this_block_funs_indexes in let ind_fun = let ind = first_fun_kn,funs_indexes in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 96a60424c..57019b3fa 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -701,7 +701,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ = args; begin try - let v = List.assoc args expr_info.args_assoc in + let v = List.assoc_f (List.equal Constr.equal) args expr_info.args_assoc in let new_infos = {expr_info with info = v} in tclTHENLIST[ continuation_tac new_infos; @@ -951,7 +951,7 @@ let equation_app f_and_args expr_info continuation_tac infos = let equation_app_rec (f,args) expr_info continuation_tac info = begin try - let v = List.assoc args expr_info.args_assoc in + let v = List.assoc_f (List.equal Constr.equal) args expr_info.args_assoc in let new_infos = {expr_info with info = v} in observe_tac (str "app_rec found") (continuation_tac new_infos) with Not_found -> diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml index eb3d81901..c8957f4cd 100644 --- a/plugins/micromega/sos.ml +++ b/plugins/micromega/sos.ml @@ -1377,7 +1377,7 @@ let allvarorders l = List.map (fun vlis x -> index x vlis) (allpermutations l);; let changevariables_monomial zoln (m:monomial) = - foldl (fun a x k -> (List.assoc x zoln |-> k) a) monomial_1 m;; + foldl (fun a x k -> (List.assoc_f (=) x zoln |-> k) a) monomial_1 m;; let changevariables zoln pol = foldl (fun a m c -> (changevariables_monomial zoln m |-> c) a) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index c39b2ff0a..5c057231a 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -131,20 +131,24 @@ let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] let rev_assoc k = let rec loop = function - | [] -> raise Not_found | (v,k')::_ when Int.equal k k' -> v | _ :: l -> loop l + | [] -> raise Not_found + | (v,k')::_ when Int.equal k k' -> v + | _ :: l -> loop l in loop 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 h !l with Not_found -> failwith "tag_hypothesis"), + (fun h -> + try List.assoc_f Id.equal 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 = let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in (fun h id eg b -> l := (h,(id,eg,b)):: !l), - (fun h -> try List.assoc_f eq_constr h !l with Not_found -> failwith "find_contr"), + (fun h -> + try List.assoc_f Constr.equal h !l with Not_found -> failwith "find_contr"), (fun () -> l := []), (fun () -> !l) @@ -1018,7 +1022,7 @@ let replay_history tactic_normalisation = begin try tclTHEN - (List.assoc (hyp_of_tag e.id) tactic_normalisation) + (List.assoc_f Id.equal (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 cf1a7e6db..b74faf30b 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -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) = List.assoc id explode_map in + let (eq,id1,id2) = Util.List.assoc_f Int.equal 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/refl_omega.ml b/plugins/romega/refl_omega.ml index 860a2524c..c5a0f798c 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -198,7 +198,7 @@ let display_omega_var i = Printf.sprintf "OV%d" i le terme d'un monome (le plus souvent un atome) *) let intern_omega env t = - begin try List.assoc t env.om_vars + begin try List.assoc_f Pervasives.(=) t env.om_vars (* FIXME *) with Not_found -> let v = new_omega_var () in env.om_vars <- (t,v) :: env.om_vars; v diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index f98625b64..26fab4ac2 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -188,7 +188,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 (List.assoc n metamap) + (try T.strip_outer_cast (Util.List.assoc_f Int.equal 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 -- cgit v1.2.3