From 914d19f19cd73d1794c0160bd6e7358c13eba630 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Sat, 23 Mar 2013 15:05:26 +0000 Subject: Minor code cleaning in CArray / CList. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/indtypes.ml | 6 ++-- checker/inductive.ml | 4 +-- kernel/indtypes.ml | 6 ++-- kernel/inductive.ml | 4 +-- lib/cArray.ml | 46 +++++++++++++++--------- lib/cList.ml | 67 +++++++++-------------------------- lib/cList.mli | 6 ++-- library/heads.ml | 2 +- plugins/cc/cctac.ml | 2 +- plugins/decl_mode/decl_interp.ml | 5 ++- plugins/decl_mode/decl_proof_instr.ml | 2 +- plugins/firstorder/instances.ml | 2 +- plugins/firstorder/rules.ml | 2 +- plugins/firstorder/sequent.ml | 4 +-- plugins/firstorder/unify.ml | 2 +- plugins/setoid_ring/newring.ml4 | 2 +- pretyping/coercion.ml | 2 +- pretyping/detyping.ml | 4 +-- pretyping/indrec.ml | 2 +- pretyping/inductiveops.ml | 2 +- pretyping/reductionops.ml | 4 +-- pretyping/tacred.ml | 4 +-- printing/printer.ml | 2 +- tactics/auto.ml | 7 ++-- tactics/inv.ml | 2 +- tactics/tactics.ml | 4 +-- toplevel/discharge.ml | 2 +- toplevel/indschemes.ml | 2 +- toplevel/obligations.ml | 2 +- 29 files changed, 89 insertions(+), 112 deletions(-) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 9a669e403..8f93ff0be 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -355,8 +355,8 @@ let abstract_mind_lc env ntyps npars lc = lc else let make_abs = - List.tabulate - (function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps + List.init ntyps + (function i -> lambda_implicit_lift npars (Rel (i+1))) in Array.map (substl make_abs) lc @@ -514,7 +514,7 @@ let check_positivity env_ar mind params nrecp inds = let lparams = rel_context_length params in let check_one i mip = let ra_env = - List.tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in + List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in let ienv = (env_ar, 1+lparams, ntypes, ra_env) in check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc in diff --git a/checker/inductive.ml b/checker/inductive.ml index abc162af7..5fdca0fab 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -58,7 +58,7 @@ let inductive_params (mib,_) = mib.mind_nparams let ind_subst mind mib = let ntypes = mib.mind_ntypes in let make_Ik k = Ind (mind,ntypes-k-1) in - List.tabulate make_Ik ntypes + List.init ntypes make_Ik (* Instantiate inductives in constructor type *) let constructor_instantiate mind mib c = @@ -527,7 +527,7 @@ let branches_specif renv c_spec ci = vra | Dead_code -> Array.make nca Dead_code | _ -> Array.make nca Not_subterm) in - List.tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca) + List.init nca (fun j -> lazy (Lazy.force lvra).(j))) car (* [subterm_specif renv t] computes the recursive structure of [t] and diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e6faaaa85..57e638982 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -386,8 +386,8 @@ let abstract_mind_lc env ntyps npars lc = lc else let make_abs = - List.tabulate - (function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps + List.init ntyps + (function i -> lambda_implicit_lift npars (mkRel (i+1))) in Array.map (substl make_abs) lc @@ -552,7 +552,7 @@ let check_positivity kn env_ar params inds = let nmr = rel_context_nhyps params in let check_one i (_,lcnames,lc,(sign,_)) = let ra_env = - List.tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in + List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in let ienv = (env_ar, 1+lparams, ntypes, ra_env) in let nargs = rel_context_nhyps sign - nmr in check_positivity_one ienv params (kn,i) nargs lcnames lc diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 3132b7e79..b93237679 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -55,7 +55,7 @@ let inductive_params (mib,_) = mib.mind_nparams let ind_subst mind mib = let ntypes = mib.mind_ntypes in let make_Ik k = mkInd (mind,ntypes-k-1) in - List.tabulate make_Ik ntypes + List.init ntypes make_Ik (* Instantiate inductives in constructor type *) let constructor_instantiate mind mib c = @@ -527,7 +527,7 @@ let branches_specif renv c_spec ci = vra | Dead_code -> Array.make nca Dead_code | _ -> Array.make nca Not_subterm) in - List.tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca) + List.init nca (fun j -> lazy (Lazy.force lvra).(j))) car (* [subterm_specif renv t] computes the recursive structure of [t] and diff --git a/lib/cArray.ml b/lib/cArray.ml index 05c8cc87c..eff317aac 100644 --- a/lib/cArray.ml +++ b/lib/cArray.ml @@ -90,31 +90,43 @@ include Array (* Arrays *) -let compare item_cmp v1 v2 = - let c = compare (Array.length v1) (Array.length v2) in - if c<>0 then c else - let rec cmp = function - -1 -> 0 - | i -> - let c' = item_cmp v1.(i) v2.(i) in - if c'<>0 then c' - else cmp (i-1) in - cmp (Array.length v1 - 1) +let compare cmp v1 v2 = + if v1 == v2 then 0 + else + let len = Array.length v1 in + let c = Int.compare len (Array.length v2) in + if c <> 0 then c else + let rec loop i = + if i < 0 then 0 + else + let x = Array.unsafe_get v1 i in + let y = Array.unsafe_get v2 i in + let c = cmp x y in + if c <> 0 then c + else loop (i - 1) + in + loop (len - 1) let equal cmp t1 t2 = if t1 == t2 then true else - if not (Array.length t1 = Array.length t2) then false - else - let rec aux i = - (i = Array.length t1) || (cmp t1.(i) t2.(i) && aux (i + 1)) - in aux 0 + let len = Array.length t1 in + if not (Int.equal len (Array.length t2)) then false + else + let rec aux i = + if i < 0 then true + else + let x = Array.unsafe_get t1 i in + let y = Array.unsafe_get t2 i in + cmp x y && aux (pred i) + in + aux (len - 1) -let is_empty array = (Array.length array) = 0 +let is_empty array = Int.equal (Array.length array) 0 let exists f v = let rec exrec = function | -1 -> false - | n -> (f v.(n)) || (exrec (n-1)) + | n -> f (Array.unsafe_get v n) || (exrec (n-1)) in exrec ((Array.length v)-1) diff --git a/lib/cList.ml b/lib/cList.ml index 8e031a0c9..e3d5f080b 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -57,6 +57,7 @@ sig val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool val is_empty : 'a list -> bool + val init : int -> (int -> 'a) -> 'a list val add_set : 'a -> 'a list -> 'a list val eq_set : 'a list -> 'a list -> bool val intersect : 'a list -> 'a list -> 'a list @@ -64,9 +65,6 @@ sig val unionq : 'a list -> 'a list -> 'a list val subtract : 'a list -> 'a list -> 'a list val subtractq : 'a list -> 'a list -> 'a list - - (** [tabulate f n] builds [[f 0; ...; f (n-1)]] *) - val tabulate : (int -> 'a) -> int -> 'a list val interval : int -> int -> int list val make : int -> 'a -> 'a list val assign : 'a list -> int -> 'a -> 'a list @@ -76,9 +74,6 @@ sig val map_filter : ('a -> 'b option) -> 'a list -> 'b list val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list val filter_with : bool list -> 'a list -> 'a list - - (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i - [ f ai == ai], then [smartmap f l==l] *) val smartmap : ('a -> 'a) -> 'a list -> 'a list val map_left : ('a -> 'b) -> 'a list -> 'b list val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list @@ -90,19 +85,10 @@ sig ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list val filteri : (int -> 'a -> bool) -> 'a list -> 'a list - - (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i - [f ai = true], then [smartfilter f l==l] *) val smartfilter : ('a -> bool) -> 'a list -> 'a list - - (** [index] returns the 1st index of an element in a list (counting from 1) *) val index : 'a -> 'a list -> int val index_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int - - (** [unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *) val unique_index : 'a -> 'a list -> int - - (** [index0] behaves as [index] except that it starts counting at 0 *) val index0 : 'a -> 'a list -> int val index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int val iteri : (int -> 'a -> unit) -> 'a list -> unit @@ -121,12 +107,9 @@ sig val sep_last : 'a list -> 'a * 'a list val find_map : ('a -> 'b option) -> 'a list -> 'b val uniquize : 'a list -> 'a list - - (** merges two sorted lists and preserves the uniqueness property: *) val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list val subset : 'a list -> 'a list -> bool val chop : int -> 'a list -> 'a list * 'a list - (* former [split_at] was a duplicate of [chop] *) val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list val firstn : int -> 'a list -> 'a list @@ -136,42 +119,21 @@ sig val skipn_at_least : int -> 'a list -> 'a list val addn : int -> 'a -> 'a list -> 'a list val prefix_of : 'a list -> 'a list -> bool - - (** [drop_prefix p l] returns [t] if [l=p++t] else return [l] *) val drop_prefix : 'a list -> 'a list -> 'a list val drop_last : 'a list -> 'a list - - (** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *) val map_append : ('a -> 'b list) -> 'a list -> 'b list - - (** raises [Invalid_argument] if the two lists don't have the same length *) val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list - - (** [fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]] - where [(e_i,k_i)=f e_{i-1} l_i] *) val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list val assoc_f : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b - - (** A generic cartesian product: for any operator (**), - [cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], - and so on if there are more elements in the lists. *) val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list - - (** [cartesians] is an n-ary cartesian product: it iterates - [cartesian] over a list of lists. *) val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list - - (** combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *) val combinations : 'a list list -> 'a list list val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list - val cartesians_filter : ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list - (** Keep only those products that do not return None *) - val factorize_left : ('a * 'b) list -> ('a * 'b list) list end @@ -239,6 +201,21 @@ let rec copy p = function p.tail <- cast c; copy c l +let rec init_loop len f p i = + if Int.equal i len then () + else + let c = { head = f i; tail = [] } in + p.tail <- cast c; + init_loop len f c (succ i) + +let init len f = + if len < 0 then invalid_arg "List.init" + else if Int.equal len 0 then [] + else + let c = { head = f 0; tail = [] } in + init_loop len f c 1; + cast c + let rec concat_loop p = function | [] -> () | x :: l -> concat_loop (copy p x) l @@ -362,17 +339,7 @@ let subtract l1 l2 = let subtractq l1 l2 = if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1 -let rec tabulate_loop f len p i = - if len <= i then () - else - let c = { head = f i; tail = [] } in - let () = p.tail <- cast c in - tabulate_loop f len c (succ i) - -let tabulate f len = - let dummy = { head = Obj.magic 0; tail = [] } in - tabulate_loop f len dummy 0; - dummy.tail +let tabulate = init let interval n m = let rec interval_n (l,m) = diff --git a/lib/cList.mli b/lib/cList.mli index 9b3a988ab..af378a37f 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -66,6 +66,9 @@ sig val is_empty : 'a list -> bool (** Checks whether a list is empty *) + val init : int -> (int -> 'a) -> 'a list + (** [init n f] constructs the list [f 0; ... ; f (n - 1)]. *) + val add_set : 'a -> 'a list -> 'a list (** [add_set x l] adds [x] in [l] if it is not already there, or returns [l] otherwise. *) @@ -79,9 +82,6 @@ sig val subtract : 'a list -> 'a list -> 'a list val subtractq : 'a list -> 'a list -> 'a list - val tabulate : (int -> 'a) -> int -> 'a list - (** [tabulate f n] builds [[f 0; ...; f (n-1)]] *) - val interval : int -> int -> int list (** [interval i j] creates the list [[i; i + 1; ...; j]], or [[]] when [j <= i]. *) diff --git a/library/heads.ml b/library/heads.ml index 62e27dd00..e6c9bc9a8 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -119,7 +119,7 @@ let kind_of_head env t = else (* enough arguments to [cst] *) k,List.skipn n l,List.nth l (i-1) in - let l' = List.tabulate (fun _ -> mkMeta 0) q @ rest in + let l' = List.make q (mkMeta 0) @ rest in aux k' l' a (with_subcase or with_case) | ConstructorHead when with_case -> NotImmediatelyComputableHead | x -> x diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 20cf9edb8..a5baa00f9 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -365,7 +365,7 @@ let discriminate_tac cstr p gls = let build_term_to_complete uf meta pac = let cinfo = get_constructor_info uf pac.cnode in let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in - let dummy_args = List.rev (List.tabulate meta pac.arity) in + let dummy_args = List.rev (List.init pac.arity meta) in let all_args = List.rev_append real_args dummy_args in applistc (mkConstruct cinfo.ci_constr) all_args diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 3cc0686ad..9d34dc99a 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -341,9 +341,8 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = (fun (loc,(id,_)) -> GVar (loc,id)) params in let dum_args= - List.tabulate - (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false))) - oib.Declarations.mind_nrealargs in + List.init oib.Declarations.mind_nrealargs + (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false))) in glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in let pat_vars,aliases,patt = interp_pattern env pat in let inject = function diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 1ae8419c8..2ef2c9756 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1190,7 +1190,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = match List.assoc id args with [None,br_args] -> let all_metas = - List.tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps) in + List.init (nparams + nhyps) (fun n -> mkMeta (succ n)) in let param_metas,hyp_metas = List.chop nparams all_metas in tclTHEN (tclDO nhrec introf) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index baf1972e6..12b2304ac 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -112,7 +112,7 @@ let mk_open_instance id gl m t= match nam with Name id -> id | Anonymous -> dummy_bvid in - let revt=substl (List.tabulate (fun i->mkRel (m-i)) m) t in + let revt=substl (List.init m (fun i->mkRel (m-i))) t in let rec aux n avoid= if n=0 then [] else let nid=(fresh_id avoid var_id gl) in diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index c812deaf5..8abf9d7e2 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -129,7 +129,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl= let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in it_mkLambda_or_LetIn head rc in let lp=Array.length rcs in - let newhyps=List.tabulate myterm lp in + let newhyps=List.init lp myterm in tclIFTHENELSE (tclTHENLIST [generalize newhyps; diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 238813e39..4e4a6f19f 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -189,8 +189,8 @@ let empty_seq depth= let expand_constructor_hints = List.map_append (function | IndRef ind -> - List.tabulate (fun i -> ConstructRef (ind,i+1)) - (Inductiveops.nconstructors ind) + List.init (Inductiveops.nconstructors ind) + (fun i -> ConstructRef (ind,i+1)) | gr -> [gr]) diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 93f84687e..75fd0261a 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -124,7 +124,7 @@ let unif_atoms i dom t1 t2= | Not_found ->Some (Phantom dom) let renum_metas_from k n t= (* requires n = max (free_rels t) *) - let l=List.tabulate (fun i->mkMeta (k+i)) n in + let l=List.init n (fun i->mkMeta (k+i)) in substl l t let more_general (m1,t1) (m2,t2)= diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index a0f565ce3..1b2ba0e87 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -179,7 +179,7 @@ let dummy_goal env = Evd.sigma = sigma} let exec_tactic env n f args = - let lid = List.tabulate(fun i -> Id.of_string("x"^string_of_int i)) n in + let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in let res = ref [||] in let get_res ist = let l = List.map (fun id -> List.assoc id ist.lfun) lid in diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 9c61d3f06..7d2ad487c 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -52,7 +52,7 @@ let apply_pattern_coercion loc pat p = List.fold_left (fun pat (co,n) -> let f i = if i contract_branch isgoal e (cnl.(i),mkpat i,cl.(i))) - (Array.length cl)) + (List.init (Array.length cl) + (fun i -> contract_branch isgoal e (cnl.(i),mkpat i,cl.(i)))) and align_tree nal isgoal (e,c as rhs) = match nal with | [] -> [[],rhs] diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index a5c4ecd3b..8904e2b7b 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -432,7 +432,7 @@ let mis_make_indrec env sigma listdepkind mib = mis_make_case_com dep env sigma indi (mibi,mipi) kind in (* Body of mis_make_indrec *) - List.tabulate make_one_rec nrec + List.init nrec make_one_rec (**********************************************************************) (* This builds elimination predicate for Case tactic *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ef95fbb5c..610bde687 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -92,7 +92,7 @@ let mis_nf_constructor_type (ind,mib,mip) j = and nconstr = Array.length mip.mind_consnames in let make_Ik k = mkInd ((fst ind),ntypes-k-1) in if j > nconstr then error "Not enough constructors in the type."; - substl (List.tabulate make_Ik ntypes) specif.(j-1) + substl (List.init ntypes make_Ik) specif.(j-1) (* Arity of constructors excluding parameters and local defs *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 732001fde..24ae6c1d0 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -293,7 +293,7 @@ let contract_cofix ?env (bodynum,(names,types,bodies as typedbodies)) cst = match env with | None -> bd | Some e -> magicaly_constant_of_fixbody e bd names.(ind) in - let closure = List.tabulate make_Fi nbodies in + let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) let reduce_mind_case mia = @@ -322,7 +322,7 @@ let contract_fix ?env ((recindices,bodynum),(names,types,bodies as typedbodies)) match env with | None -> bd | Some e -> magicaly_constant_of_fixbody e bd names.(ind) in - let closure = List.tabulate make_Fi nbodies in + let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) let fix_recarg ((recindices,bodynum),_) stack = diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 508569f0d..b46b69c62 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -457,7 +457,7 @@ let contract_fix_use_function env sigma f ((recindices,bodynum),(_names,_types,bodies as typedbodies)) = let nbodies = Array.length recindices in let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in - let lbodies = List.tabulate make_Fi nbodies in + let lbodies = List.init nbodies make_Fi in substl_checking_arity env (List.rev lbodies) (nf_beta sigma bodies.(bodynum)) let reduce_fix_use_function env sigma f whfun fix stack = @@ -480,7 +480,7 @@ let contract_cofix_use_function env sigma f (bodynum,(_names,_,bodies as typedbodies)) = let nbodies = Array.length bodies in let make_Fi j = (mkCoFix(j,typedbodies), f j) in - let subbodies = List.tabulate make_Fi nbodies in + let subbodies = List.init nbodies make_Fi in substl_checking_arity env (List.rev subbodies) (nf_beta sigma bodies.(bodynum)) diff --git a/printing/printer.ml b/printing/printer.ml index 8fc38bc6c..ac7761994 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -735,7 +735,7 @@ let print_one_inductive env mib ((_,i) as ind) = brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes let print_mutual_inductive env mind mib = - let inds = List.tabulate (fun x -> (mind,x)) (Array.length mib.mind_packets) + let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) in hov 0 ( str (if mib.mind_finite then "Inductive " else "CoInductive ") ++ diff --git a/tactics/auto.ml b/tactics/auto.ml index f9b45bdfb..e05c5384a 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -873,10 +873,9 @@ let interp_hints = let constr_hints_of_ind qid = let ind = global_inductive_with_alias qid in Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind"; - List.tabulate (fun i -> let c = (ind,i+1) in + List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in - None, true, PathHints [gr], IsGlobal gr) - (nconstructors ind) in + None, true, PathHints [gr], IsGlobal gr) in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) | HintsExtern (pri, patcom, tacexp) -> let pat = Option.map fp patcom in @@ -1069,7 +1068,7 @@ let expand_constructor_hints env lems = List.map_append (fun (sigma,lem) -> match kind_of_term lem with | Ind ind -> - List.tabulate (fun i -> mkConstruct (ind,i+1)) (nconstructors ind) + List.init (nconstructors ind) (fun i -> mkConstruct (ind,i+1)) | _ -> [prepare_hint env (sigma,lem)]) lems diff --git a/tactics/inv.ml b/tactics/inv.ml index c99c15a45..7308b7091 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -472,7 +472,7 @@ let raw_inversion inv_kind id status names gl = (fun id -> (tclTHEN (apply_term (mkVar id) - (List.tabulate (fun _ -> Evarutil.mk_new_meta()) neqns)) + (List.init neqns (fun _ -> Evarutil.mk_new_meta()))) reflexivity))]) gl diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ac783adf3..210800955 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -938,14 +938,14 @@ let descend_in_conjunctions tac exit c gl = let elim = pf_apply build_case_analysis_scheme gl ind false sort in NotADefinedRecordUseScheme elim in tclFIRST - (List.tabulate (fun i gl -> + (List.init n (fun i gl -> match make_projection (project gl) params cstr sign elim i n c with | None -> tclFAIL 0 (mt()) gl | Some (p,pt) -> tclTHENS (internal_cut id pt) [refine p; (* Might be ill-typed due to forbidden elimination. *) - tclTHEN (tac (not isrec) (mkVar id)) (thin [id])] gl) n) + tclTHEN (tac (not isrec) (mkVar id)) (thin [id])] gl)) gl | None -> raise Exit diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index b12378c56..4dd00301f 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -38,7 +38,7 @@ let abstract_inductive hyps nparams inds = let ntyp = List.length inds in let nhyp = named_context_length hyps in let args = instance_from_named_context (List.rev hyps) in - let subs = List.tabulate (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) ntyp in + let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in let inds' = List.map (function (tname,arity,cnames,lc) -> diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 616430007..bed262bbb 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -178,7 +178,7 @@ let beq_scheme_msg mind = (* TODO: mutual inductive case *) str "Boolean equality on " ++ pr_enum (fun ind -> quote (Printer.pr_inductive (Global.env()) ind)) - (List.tabulate (fun i -> (mind,i)) (Array.length mib.mind_packets)) + (List.init (Array.length mib.mind_packets) (fun i -> (mind,i))) let declare_beq_scheme_with l kn = try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 6b8780cda..092c329f3 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -31,7 +31,7 @@ let trace s = let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) -let mkMetas n = List.tabulate (fun _ -> Evarutil.mk_new_meta ()) n +let mkMetas n = List.init n (fun _ -> Evarutil.mk_new_meta ()) let check_evars env evm = List.iter -- cgit v1.2.3