diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 19:13:19 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 19:13:19 +0000 |
| commit | 8cc623262c625bda20e97c75f9ba083ae8e7760d (patch) | |
| tree | 3e7ef244636612606a574a21e4f8acaab828d517 | |
| parent | 6eaff635db797d1f9225b22196832c1bb76c0d94 (diff) | |
As r15801: putting everything from Util.array_* to CArray.*.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
79 files changed, 804 insertions, 666 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index b7e196d4b..d286651a1 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -8,6 +8,7 @@ Segmenttree Unicodetable Errors CList +CArray Util Option Hashcons diff --git a/checker/closure.ml b/checker/closure.ml index c3351cea1..f86aa82eb 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -414,7 +414,7 @@ and compact_vect s v k = compact_v [] s v k (Array.length v - 1) and compact_v acc s v k i = if i < 0 then let v' = Array.of_list acc in - if array_for_all2 (==) v v' then v,s else v',s + if Array.for_all2 (==) v v' then v,s else v',s else let (a',s') = compact_constr s v.(i) k in compact_v (a'::acc) s' v k (i-1) diff --git a/checker/declarations.ml b/checker/declarations.ml index ad14a3bbe..8b146d18b 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -268,7 +268,7 @@ let rec map_kn f f' c = in let p' = func p in let ct' = func ct in - let l' = array_smartmap func l in + let l' = Array.smartmap func l in if (ci.ci_ind==ci_ind && p'==p && l'==l && ct'==ct)then c else @@ -297,21 +297,21 @@ let rec map_kn f f' c = else LetIn (na, b', t', ct') | App (ct,l) -> let ct' = func ct in - let l' = array_smartmap func l in + let l' = Array.smartmap func l in if (ct'== ct && l'==l) then c else App (ct',l') | Evar (e,l) -> - let l' = array_smartmap func l in + let l' = Array.smartmap func l in if (l'==l) then c else Evar (e,l') | Fix (ln,(lna,tl,bl)) -> - let tl' = array_smartmap func tl in - let bl' = array_smartmap func bl in + let tl' = Array.smartmap func tl in + let bl' = Array.smartmap func bl in if (bl == bl'&& tl == tl') then c else Fix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = array_smartmap func tl in - let bl' = array_smartmap func bl in + let tl' = Array.smartmap func tl in + let bl' = Array.smartmap func bl in if (bl == bl'&& tl == tl') then c else CoFix (ln,(lna,tl',bl')) | _ -> c @@ -720,10 +720,10 @@ let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; mind_consnrealdecls = mbp.mind_consnrealdecls; mind_typename = mbp.mind_typename; - mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc; + mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; mind_arity = subst_arity sub mbp.mind_arity; - mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc; + mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; mind_kelim = mbp.mind_kelim; @@ -742,7 +742,7 @@ let subst_mind sub mib = mind_nparams_rec = mib.mind_nparams_rec; mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt; - mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ; + mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_constraints = mib.mind_constraints } (* Modules *) diff --git a/checker/environ.ml b/checker/environ.ml index d0b0b4ce9..a0fac3492 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -74,7 +74,7 @@ let push_rel d env = let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = - let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in + let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in Array.fold_left (fun e assum -> push_rel assum e) env ctxt (* Named context *) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 6d936796a..3539289e7 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -127,7 +127,7 @@ let is_unit constrsinfos = | _ -> false let small_unit constrsinfos = - let issmall = array_for_all is_small_constr constrsinfos + let issmall = Array.for_all is_small_constr constrsinfos and isunit = is_unit constrsinfos in issmall, isunit @@ -243,13 +243,13 @@ let typecheck_one_inductive env params mib mip = let _ = Array.map (infer_type env) mip.mind_user_lc in (* mind_nf_lc *) let _ = Array.map (infer_type env) mip.mind_nf_lc in - array_iter2 (conv env) mip.mind_nf_lc mip.mind_user_lc; + Array.iter2 (conv env) mip.mind_nf_lc mip.mind_user_lc; (* mind_consnrealdecls *) let check_cons_args c n = let ctx,_ = decompose_prod_assum c in if n <> rel_context_length ctx - rel_context_length params then failwith "bad number of real constructor arguments" in - array_iter2 check_cons_args mip.mind_nf_lc mip.mind_consnrealdecls; + Array.iter2 check_cons_args mip.mind_nf_lc mip.mind_consnrealdecls; (* mind_kelim: checked by positivity criterion ? *) let sorts = compute_elim_sorts env params mib mip.mind_arity mip.mind_nf_lc in @@ -312,7 +312,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = let largs = Array.of_list largs in if Array.length largs < nparams then raise (IllFormedInd (LocalNotEnoughArgs l)); - let (lpar,largs') = array_chop nparams largs in + let (lpar,largs') = Array.chop nparams largs in let nhyps = List.length hyps in let rec check k index = function | [] -> () @@ -322,7 +322,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = | Rel w when w = index -> check (k-1) (index+1) hyps | _ -> raise (IllFormedInd (LocalNonPar (k+1,l))) in check (nparams-1) (n-nhyps) hyps; - if not (array_for_all (noccur_between n ntypes) largs') then + if not (Array.for_all (noccur_between n ntypes) largs') then failwith_non_pos_vect n ntypes largs' (* Arguments of constructor: check the number of recursive parameters nrecp. @@ -520,7 +520,7 @@ let check_positivity env_ar mind params nrecp inds = in let irecargs = Array.mapi check_one inds in let wfp = Rtree.mk_rec irecargs in - array_iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp + Array.iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp (************************************************************************) (************************************************************************) diff --git a/checker/inductive.ml b/checker/inductive.ml index f35d68ad1..605405e35 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -817,7 +817,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = | _ -> raise_err env i NotEnoughAbstractionInFixBody in check_occur fixenv 1 def in (* Do it on every fixpoint *) - let rv = array_map2_i find_ind nvect bodies in + let rv = Array.map2_i find_ind nvect bodies in (Array.map fst rv, Array.map snd rv) @@ -899,7 +899,7 @@ let check_one_cofix env nbfix def deftype = if (List.for_all (noccur_with_meta n nbfix) args) then let nbfix = Array.length vdefs in - if (array_for_all (noccur_with_meta n nbfix) varit) then + if (Array.for_all (noccur_with_meta n nbfix) varit) then let env' = push_rec_types recdef env in (Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs; List.iter (check_rec_call env alreadygrd n vlra) args) diff --git a/checker/reduction.ml b/checker/reduction.ml index 5243bb201..195f7d423 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -122,14 +122,14 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 = | (z1::s1, z2::s2) -> cmp_rec s1 s2; (match (z1,z2) with - | (Zlapp a1,Zlapp a2) -> array_iter2 f a1 a2 + | (Zlapp a1,Zlapp a2) -> Array.iter2 f a1 a2 | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> f fx1 fx2; cmp_rec a1 a2 | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) -> if not (fmind ci1.ci_ind ci2.ci_ind) then raise NotConvertible; f (l1,p1) (l2,p2); - array_iter2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 + Array.iter2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 | _ -> assert false) | _ -> () in if compare_stack_shape stk1 stk2 then @@ -368,7 +368,7 @@ and convert_stacks univ infos lft1 lft2 stk1 stk2 = lft1 stk1 lft2 stk2 and convert_vect univ infos lft1 lft2 v1 v2 = - array_iter2 (fun t1 t2 -> ccnv univ CONV infos lft1 lft2 t1 t2) v1 v2 + Array.iter2 (fun t1 t2 -> ccnv univ CONV infos lft1 lft2 t1 t2) v1 v2 let clos_fconv cv_pb env t1 t2 = let infos = create_clos_infos betaiotazeta env in diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 55ed06665..7d2ced7fd 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -42,7 +42,7 @@ let add_mib_nameobjects mp l mib map = let add_mip_nameobjects j oib map = let ip = (ind,j) in let map = - array_fold_right_i + Array.fold_right_i (fun i id map -> Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map) oib.mind_consnames @@ -50,7 +50,7 @@ let add_mib_nameobjects mp l mib map = in Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map in - array_fold_right_i add_mip_nameobjects mib.mind_packets map + Array.fold_right_i add_mip_nameobjects mib.mind_packets map (* creates (namedobject/namedmodule) map for the whole signature *) @@ -149,7 +149,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2)) in let check_cons_types i p1 p2 = - array_iter2 (check_conv conv env) + Array.iter2 (check_conv conv env) (arities_of_specif kn (mib1,p1)) (arities_of_specif kn (mib2,p2)) in @@ -194,9 +194,9 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= check (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0)); end; (* we first check simple things *) - array_iter2 check_packet mib1.mind_packets mib2.mind_packets; + Array.iter2 check_packet mib1.mind_packets mib2.mind_packets; (* and constructor types in the end *) - let _ = array_map2_i check_cons_types mib1.mind_packets mib2.mind_packets + let _ = Array.map2_i check_cons_types mib1.mind_packets mib2.mind_packets in () let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = diff --git a/checker/term.ml b/checker/term.ml index a7fc0a8b8..b41bebca2 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -473,23 +473,23 @@ let compare_constr f t1 t2 = | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2 | App (c1,l1), App (c2,l2) -> if Array.length l1 = Array.length l2 then - f c1 c2 & array_for_all2 f l1 l2 + f c1 c2 & Array.for_all2 f l1 l2 else let (h1,l1) = decompose_app t1 in let (h2,l2) = decompose_app t2 in if List.length l1 = List.length l2 then f h1 h2 & List.for_all2 f l1 l2 else false - | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & Array.for_all2 f l1 l2 | Const c1, Const c2 -> eq_con_chk c1 c2 | Ind c1, Ind c2 -> eq_ind_chk c1 c2 | Construct (c1,i1), Construct (c2,i2) -> i1=i2 && eq_ind_chk c1 c2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2 + f p1 p2 & f c1 c2 & Array.for_all2 f bl1 bl2 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> - ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 + ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 + ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2 | _ -> false let rec eq_constr m n = diff --git a/checker/typeops.ml b/checker/typeops.ml index 03d2bedcf..91f58a04a 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -20,7 +20,7 @@ open Environ let inductive_of_constructor = fst let conv_leq_vecti env v1 v2 = - array_fold_left2_i + Array.fold_left2_i (fun i _ t1 t2 -> (try conv_leq env t1 t2 with NotConvertible -> raise (NotConvertibleVect i)); ()) @@ -244,7 +244,7 @@ let type_fixpoint env lna lar lbody vdefj = try conv_leq_vecti env vdefj (Array.map (fun ty -> lift lt ty) lar) with NotConvertibleVect i -> - let vdefj = array_map2 (fun b ty -> b,ty) lbody vdefj in + let vdefj = Array.map2 (fun b ty -> b,ty) lbody vdefj in error_ill_typed_rec_body env i lna vdefj lar (************************************************************************) @@ -293,7 +293,7 @@ let rec execute env cstr = (* No sort-polymorphism *) execute env f in - let jl = array_map2 (fun c ty -> c,ty) args jl in + let jl = Array.map2 (fun c ty -> c,ty) args jl in judge_of_apply env (f,j) jl | Lambda (name,c1,c2) -> @@ -362,7 +362,7 @@ and execute_type env constr = and execute_recdef env (names,lar,vdef) i = let larj = execute_array env lar in - let larj = array_map2 (fun c ty -> c,ty) lar larj in + let larj = Array.map2 (fun c ty -> c,ty) lar larj in let lara = Array.map (assumption_of_judgment env) larj in let env1 = push_rec_types (names,lara,vdef) env in let vdefj = execute_array env1 vdef in diff --git a/dev/printers.mllib b/dev/printers.mllib index 0cf74e627..562c58fed 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -9,6 +9,7 @@ Segmenttree Unicodetable Errors CList +CArray Util Bigint Hashcons diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 6849669db..dc63525d5 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -9,6 +9,7 @@ Segmenttree Unicodetable Errors CList +CArray Util Bigint Hashcons diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0ce8a8aac..d5f96e3fd 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1015,7 +1015,7 @@ let any_any_branch = let rec glob_of_pat env = function | PRef ref -> GRef (loc,ref) | PVar id -> GVar (loc,id) - | PEvar (n,l) -> GEvar (loc,n,Some (array_map_to_list (glob_of_pat env) l)) + | PEvar (n,l) -> GEvar (loc,n,Some (Array.map_to_list (glob_of_pat env) l)) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id @@ -1026,7 +1026,7 @@ let rec glob_of_pat env = function | PMeta None -> GHole (loc,Evar_kinds.InternalHole) | PMeta (Some n) -> GPatVar (loc,(false,n)) | PApp (f,args) -> - GApp (loc,glob_of_pat env f,array_map_to_list (glob_of_pat env) args) + GApp (loc,glob_of_pat env f,Array.map_to_list (glob_of_pat env) args) | PSoApp (n,args) -> GApp (loc,GPatVar (loc,(true,n)), List.map (glob_of_pat env) args) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7ad1327fd..a2be41700 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1307,7 +1307,7 @@ let internalize sigma globalenv env allow_patvar lvar c = intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r)) in ((n, ro), List.rev rbl, intern_type env' ty, env')) dl in - let idl = array_map2 (fun (_,_,_,_,bd) (a,b,c,env') -> + let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') -> let env'' = List.fold_left_i (fun i en name -> let (_,bli,tyi,_) = idl_temp.(i) in let fix_args = (List.map (fun (_,(na, bk, _, _)) -> (build_impls bk na)) bli) in @@ -1334,7 +1334,7 @@ let internalize sigma globalenv env allow_patvar lvar c = List.fold_left intern_local_binder (env,[]) bl in (List.rev rbl, intern_type env' ty,env')) dl in - let idl = array_map2 (fun (_,_,_,bd) (b,c,env') -> + let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') -> let env'' = List.fold_left_i (fun i en name -> let (bli,tyi,_) = idl_tmp.(i) in let cofix_args = List.map (fun (_, (na, bk, _, _)) -> (build_impls bk na)) bli in diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index c4cc38a56..64e890616 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -176,7 +176,7 @@ let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty let vs2 = vars bound1 vs1 tyl.(i) in vars bound1 vs2 bv.(i) in - array_fold_left_i vars_fix vs idl + Array.fold_left_i vars_fix vs idl | GCast (loc,c,k) -> let v = vars bound vs c in (match k with CastConv t | CastVM t -> vars bound v t | _ -> v) | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 13356445f..3429ab7b9 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -97,10 +97,10 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function let e',na = g e na in GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2) | NRec (fk,idl,dll,tl,bl) -> - let e,dll = array_fold_map (List.fold_map (fun e (na,oc,b) -> + let e,dll = Array.fold_map (List.fold_map (fun e (na,oc,b) -> let e,na = g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in - let e',idl = array_fold_map (to_id g) e idl in + let e',idl = Array.fold_map (to_id g) e idl in GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) | NCast (c,k) -> GCast (loc,f e c,Miscops.map_cast_type (f e) k) | NSort x -> GSort (loc,x) @@ -423,12 +423,12 @@ let rec subst_notation_constr subst bound raw = | NRec (fk,idl,dll,tl,bl) -> let dll' = - array_smartmap (List.smartmap (fun (na,oc,b as x) -> + Array.smartmap (List.smartmap (fun (na,oc,b as x) -> let oc' = Option.smartmap (subst_notation_constr subst bound) oc in let b' = subst_notation_constr subst bound b in if oc' == oc && b' == b then x else (na,oc',b'))) dll in - let tl' = array_smartmap (subst_notation_constr subst bound) tl in - let bl' = array_smartmap (subst_notation_constr subst bound) bl in + let tl' = Array.smartmap (subst_notation_constr subst bound) tl in + let bl' = Array.smartmap (subst_notation_constr subst bound) bl in if dll' == dll && tl' == tl && bl' == bl then raw else NRec (fk,idl,dll',tl',bl') @@ -500,7 +500,7 @@ let match_fix_kind fk1 fk2 = | GCoFix n1, GCoFix n2 -> n1 = n2 | GFix (nl1,n1), GFix (nl2,n2) -> n1 = n2 && - array_for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2 + Array.for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2 | _ -> false let match_opt f sigma t1 t2 = match (t1,t2) with @@ -658,18 +658,18 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = List.fold_left2 (match_in u alp metas) sigma [a1;b1;c1] [a2;b2;c2] | GRec (_,fk1,idl1,dll1,tl1,bl1), NRec (fk2,idl2,dll2,tl2,bl2) when match_fix_kind fk1 fk2 & Array.length idl1 = Array.length idl2 & - array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) dll1 dll2 + Array.for_all2 (fun l1 l2 -> List.length l1 = List.length l2) dll1 dll2 -> - let alp,sigma = array_fold_left2 + let alp,sigma = Array.fold_left2 (List.fold_left2 (fun (alp,sigma) (na1,_,oc1,b1) (na2,oc2,b2) -> let sigma = match_in u alp metas (match_opt (match_in u alp metas) sigma oc1 oc2) b1 b2 in match_names metas (alp,sigma) na1 na2)) (alp,sigma) dll1 dll2 in - let sigma = array_fold_left2 (match_in u alp metas) sigma tl1 tl2 in - let alp,sigma = array_fold_right2 (fun id1 id2 alsig -> + let sigma = Array.fold_left2 (match_in u alp metas) sigma tl1 tl2 in + let alp,sigma = Array.fold_right2 (fun id1 id2 alsig -> match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in - array_fold_left2 (match_in u alp metas) sigma bl1 bl2 + Array.fold_left2 (match_in u alp metas) sigma bl1 bl2 | GCast(_,c1,CastConv t1), NCast (c2,CastConv t2) | GCast(_,c1,CastVM t1), NCast (c2,CastVM t2) -> match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2 diff --git a/kernel/closure.ml b/kernel/closure.ml index 210dbb02b..251c32ac5 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -499,7 +499,7 @@ and compact_vect s v k = compact_v [] s v k (Array.length v - 1) and compact_v acc s v k i = if i < 0 then let v' = Array.of_list acc in - if array_for_all2 (==) v v' then v,s else v',s + if Array.for_all2 (==) v v' then v,s else v',s else let (a',s') = compact_constr s v.(i) k in compact_v (a'::acc) s' v k (i-1) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index a2ce4f270..b8edcae72 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -325,10 +325,10 @@ let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; mind_consnrealdecls = mbp.mind_consnrealdecls; mind_typename = mbp.mind_typename; - mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc; + mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; mind_arity = subst_indarity sub mbp.mind_arity; - mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc; + mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; mind_kelim = mbp.mind_kelim; @@ -346,7 +346,7 @@ let subst_mind sub mib = mind_nparams_rec = mib.mind_nparams_rec; mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt; - mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ; + mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_constraints = mib.mind_constraints } let hcons_indarity = function @@ -360,13 +360,13 @@ let hcons_mind_packet oib = mind_typename = hcons_ident oib.mind_typename; mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt; mind_arity = hcons_indarity oib.mind_arity; - mind_consnames = array_smartmap hcons_ident oib.mind_consnames; - mind_user_lc = array_smartmap hcons_types oib.mind_user_lc; - mind_nf_lc = array_smartmap hcons_types oib.mind_nf_lc } + mind_consnames = Array.smartmap hcons_ident oib.mind_consnames; + mind_user_lc = Array.smartmap hcons_types oib.mind_user_lc; + mind_nf_lc = Array.smartmap hcons_types oib.mind_nf_lc } let hcons_mind mib = { mib with - mind_packets = array_smartmap hcons_mind_packet mib.mind_packets; + mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; mind_constraints = hcons_constraints mib.mind_constraints } diff --git a/kernel/environ.ml b/kernel/environ.ml index f1adb5340..37a896c77 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -68,7 +68,7 @@ let push_rel = push_rel let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = - let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in + let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in Array.fold_left (fun e assum -> push_rel assum e) env ctxt let fold_rel_context f env ~init = diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b93b9f19b..3199d0faa 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -253,7 +253,7 @@ let typecheck_inductive env mie = (* Compute/check the sorts of the inductive types *) let ind_min_levels = inductive_levels arities inds in let inds, cst = - array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst -> + Array.fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst -> let sign, s = dest_arity env full_arity in let status,cst = match s with | Type u when ar_level <> None (* Explicitly polymorphic *) @@ -330,7 +330,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = let largs = Array.of_list largs in if Array.length largs < nparams then raise (IllFormedInd (LocalNotEnoughArgs l)); - let (lpar,largs') = array_chop nparams largs in + let (lpar,largs') = Array.chop nparams largs in let nhyps = List.length hyps in let rec check k index = function | [] -> () @@ -340,7 +340,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = | Rel w when w = index -> check (k-1) (index+1) hyps | _ -> raise (IllFormedInd (LocalNonPar (k+1,l))) in check (nparams-1) (n-nhyps) hyps; - if not (array_for_all (noccur_between n ntypes) largs') then + if not (Array.for_all (noccur_between n ntypes) largs') then failwith_non_pos_vect n ntypes largs' (* Computes the maximum number of recursive parameters : @@ -518,7 +518,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname in check_constr_rec ienv nmr [] c in let irecargs_nmr = - array_map2 + Array.map2 (fun id c -> let _,rawc = mind_extract_params lparams c in try @@ -646,7 +646,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = mind_nb_args = !nblock; mind_reloc_tbl = rtbl; } in - let packets = array_map2 build_one_packet inds recargs in + let packets = Array.map2 build_one_packet inds recargs in (* Build the mutual inductive *) { mind_record = isrecord; mind_ntypes = ntypes; diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d86abb435..81e6c8f17 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -779,7 +779,7 @@ let check_one_fix renv recpos def = check_rec_call renv [] def let judgment_of_fixpoint (_, types, bodies) = - array_map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies + Array.map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = let nbfix = Array.length bodies in @@ -815,7 +815,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = | _ -> raise_err env i NotEnoughAbstractionInFixBody in check_occur fixenv 1 def in (* Do it on every fixpoint *) - let rv = array_map2_i find_ind nvect bodies in + let rv = Array.map2_i find_ind nvect bodies in (Array.map fst rv, Array.map snd rv) @@ -898,7 +898,7 @@ let check_one_cofix env nbfix def deftype = if (List.for_all (noccur_with_meta n nbfix) args) then let nbfix = Array.length vdefs in - if (array_for_all (noccur_with_meta n nbfix) varit) then + if (Array.for_all (noccur_with_meta n nbfix) varit) then let env' = push_rec_types recdef env in (Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs; List.iter (check_rec_call env alreadygrd n vlra) args) diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index e7a5227e0..61dc2bf29 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -339,7 +339,7 @@ let rec map_kn f f' c = in let p' = func p in let ct' = func ct in - let l' = array_smartmap func l in + let l' = Array.smartmap func l in if (ci.ci_ind==ci_ind && p'==p && l'==l && ct'==ct)then c else @@ -368,21 +368,21 @@ let rec map_kn f f' c = else mkLetIn (na, b', t', ct') | App (ct,l) -> let ct' = func ct in - let l' = array_smartmap func l in + let l' = Array.smartmap func l in if (ct'== ct && l'==l) then c else mkApp (ct',l') | Evar (e,l) -> - let l' = array_smartmap func l in + let l' = Array.smartmap func l in if (l'==l) then c else mkEvar (e,l') | Fix (ln,(lna,tl,bl)) -> - let tl' = array_smartmap func tl in - let bl' = array_smartmap func bl in + let tl' = Array.smartmap func tl in + let bl' = Array.smartmap func bl in if (bl == bl'&& tl == tl') then c else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = array_smartmap func tl in - let bl' = array_smartmap func bl in + let tl' = Array.smartmap func tl in + let bl' = Array.smartmap func bl in if (bl == bl'&& tl == tl') then c else mkCoFix (ln,(lna,tl',bl')) | _ -> c diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 4ce3e7f22..76dcd1d3a 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -153,7 +153,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = | (z1::s1, z2::s2) -> let cu1 = cmp_rec s1 s2 cuniv in (match (z1,z2) with - | (Zlapp a1,Zlapp a2) -> array_fold_right2 f a1 a2 cu1 + | (Zlapp a1,Zlapp a2) -> Array.fold_right2 f a1 a2 cu1 | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> let cu2 = f fx1 fx2 cu1 in cmp_rec a1 a2 cu2 @@ -161,7 +161,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = if not (fmind ci1.ci_ind ci2.ci_ind) then raise NotConvertible; let cu2 = f (l1,p1) (l2,p2) cu1 in - array_fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2 + Array.fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2 | _ -> assert false) | _ -> cuniv in if compare_stack_shape stk1 stk2 then @@ -443,7 +443,7 @@ let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars let conv_leq ?(l2r=false) ?(evars=fun _->None) = fconv CUMUL l2r evars let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 = - array_fold_left2_i + Array.fold_left2_i (fun i c t1 t2 -> let c' = try conv_leq ~l2r ~evars env t1 t2 diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index c590a5101..b8626e227 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -43,7 +43,7 @@ let add_mib_nameobjects mp l mib map = let add_mip_nameobjects j oib map = let ip = (ind,j) in let map = - array_fold_right_i + Array.fold_right_i (fun i id map -> Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map) oib.mind_consnames @@ -51,7 +51,7 @@ let add_mib_nameobjects mp l mib map = in Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map in - array_fold_right_i add_mip_nameobjects mib.mind_packets map + Array.fold_right_i add_mip_nameobjects mib.mind_packets map (* creates (namedobject/namedmodule) map for the whole signature *) @@ -154,7 +154,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 cst in let check_cons_types i cst p1 p2 = - array_fold_left3 + Array.fold_left3 (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst conv env t1 t2) cst p2.mind_consnames @@ -203,11 +203,11 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 end; (* we first check simple things *) let cst = - array_fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets + Array.fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets in (* and constructor types in the end *) let cst = - array_fold_left2_i check_cons_types cst mib1.mind_packets mib2.mind_packets + Array.fold_left2_i check_cons_types cst mib1.mind_packets mib2.mind_packets in cst diff --git a/kernel/term.ml b/kernel/term.ml index 07152d4b6..e54e56f12 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -463,10 +463,10 @@ let fold_constr f acc c = match kind_of_term c with | Evar (_,l) -> Array.fold_left f acc l | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl | Fix (_,(lna,tl,bl)) -> - let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in + let fd = Array.map3 (fun na t b -> (na,t,b)) lna tl bl in Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd | CoFix (_,(lna,tl,bl)) -> - let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in + let fd = Array.map3 (fun na t b -> (na,t,b)) lna tl bl in Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd (* [iter_constr f c] iters [f] on the immediate subterms of [c]; it is @@ -572,17 +572,17 @@ let compare_constr f t1 t2 = | _, App (c2,l2) when isCast c2 -> f t1 (mkApp (pi1 (destCast c2),l2)) | App (c1,l1), App (c2,l2) -> Array.length l1 = Array.length l2 && - f c1 c2 && array_for_all2 f l1 l2 - | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2 + f c1 c2 && Array.for_all2 f l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & Array.for_all2 f l1 l2 | Const c1, Const c2 -> eq_constant c1 c2 | Ind c1, Ind c2 -> eq_ind c1 c2 | Construct c1, Construct c2 -> eq_constructor c1 c2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2 + f p1 p2 & f c1 c2 & Array.for_all2 f bl1 bl2 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> - ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 + ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 + ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2 | _ -> false (*******************************) @@ -618,9 +618,9 @@ let constr_ord_int f t1 t2 = ((f =? f) ==? f) b1 b2 t1 t2 c1 c2 | App (c1,l1), _ when isCast c1 -> f (mkApp (pi1 (destCast c1),l1)) t2 | _, App (c2,l2) when isCast c2 -> f t1 (mkApp (pi1 (destCast c2),l2)) - | App (c1,l1), App (c2,l2) -> (f =? (array_compare f)) c1 c2 l1 l2 + | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2 | Evar (e1,l1), Evar (e2,l2) -> - ((-) =? (array_compare f)) e1 e2 l1 l2 + ((-) =? (Array.compare f)) e1 e2 l1 l2 | Const c1, Const c2 -> kn_ord (canonical_con c1) (canonical_con c2) | Ind (spx, ix), Ind (spy, iy) -> let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c @@ -629,12 +629,12 @@ let constr_ord_int f t1 t2 = (let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c) else c | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - ((f =? f) ==? (array_compare f)) p1 p2 c1 c2 bl1 bl2 + ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> - ((Pervasives.compare =? (array_compare f)) ==? (array_compare f)) + ((Pervasives.compare =? (Array.compare f)) ==? (Array.compare f)) ln1 ln2 tl1 tl2 bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - ((Pervasives.compare =? (array_compare f)) ==? (array_compare f)) + ((Pervasives.compare =? (Array.compare f)) ==? (Array.compare f)) ln1 ln2 tl1 tl2 bl1 bl2 | t1, t2 -> Pervasives.compare t1 t2 diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 3ec08fef4..294d99eea 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -21,7 +21,7 @@ open Type_errors let conv_leq l2r = default_conv CUMUL ~l2r let conv_leq_vecti env v1 v2 = - array_fold_left2_i + Array.fold_left2_i (fun i c t1 t2 -> let c' = try default_conv CUMUL env t1 t2 @@ -476,7 +476,7 @@ and execute_recdef env (names,lar,vdef) i cu = univ_combinator cu2 ((lara.(i),(names,lara,vdefv)),cst) -and execute_array env = array_fold_map' (execute env) +and execute_array env = Array.fold_map' (execute env) (* Derived functions *) let infer env constr = diff --git a/lib/cArray.ml b/lib/cArray.ml new file mode 100644 index 000000000..7f25bb10c --- /dev/null +++ b/lib/cArray.ml @@ -0,0 +1,420 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +module type S = +sig + external length : 'a array -> int = "%array_length" + external get : 'a array -> int -> 'a = "%array_safe_get" + external set : 'a array -> int -> 'a -> unit = "%array_safe_set" + external make : int -> 'a -> 'a array = "caml_make_vect" + external create : int -> 'a -> 'a array = "caml_make_vect" + val init : int -> (int -> 'a) -> 'a array + val make_matrix : int -> int -> 'a -> 'a array array + val create_matrix : int -> int -> 'a -> 'a array array + val append : 'a array -> 'a array -> 'a array + val concat : 'a array list -> 'a array + val sub : 'a array -> int -> int -> 'a array + val copy : 'a array -> 'a array + val fill : 'a array -> int -> int -> 'a -> unit + val blit : 'a array -> int -> 'a array -> int -> int -> unit + val to_list : 'a array -> 'a list + val of_list : 'a list -> 'a array + val iter : ('a -> unit) -> 'a array -> unit + val map : ('a -> 'b) -> 'a array -> 'b array + val iteri : (int -> 'a -> unit) -> 'a array -> unit + val mapi : (int -> 'a -> 'b) -> 'a array -> 'b array + val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a + val fold_right : ('b -> 'a -> 'a) -> 'b array -> 'a -> 'a + val sort : ('a -> 'a -> int) -> 'a array -> unit + val stable_sort : ('a -> 'a -> int) -> 'a array -> unit + val fast_sort : ('a -> 'a -> int) -> 'a array -> unit + external unsafe_get : 'a array -> int -> 'a = "%array_unsafe_get" + external unsafe_set : 'a array -> int -> 'a -> unit = "%array_unsafe_set" +end + +module type ExtS = +sig + include S + val compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int + val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool + val exists : ('a -> bool) -> 'a array -> bool + val for_all : ('a -> bool) -> 'a array -> bool + val for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool + val for_all3 : ('a -> 'b -> 'c -> bool) -> + 'a array -> 'b array -> 'c array -> bool + val for_all4 : ('a -> 'b -> 'c -> 'd -> bool) -> + 'a array -> 'b array -> 'c array -> 'd array -> bool + val for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool + val find_i : (int -> 'a -> bool) -> 'a array -> int option + val hd : 'a array -> 'a + val tl : 'a array -> 'a array + val last : 'a array -> 'a + val cons : 'a -> 'a array -> 'a array + val rev : 'a array -> unit + val fold_right_i : + (int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a + val fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a + val fold_right2 : + ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c + val fold_left2 : + ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a + val fold_left3 : + ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a + val fold_left2_i : + (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a + val fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a + val fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b + val app_tl : 'a array -> 'a list -> 'a list + val list_of_tl : 'a array -> 'a list + val map_to_list : ('a -> 'b) -> 'a array -> 'b list + val chop : int -> 'a array -> 'a array * 'a array + val smartmap : ('a -> 'a) -> 'a array -> 'a array + val map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array + val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array + val map3 : + ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array + val map_left : ('a -> 'b) -> 'a array -> 'b array + val map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array -> + 'b array * 'd array + val iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit + val fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c + val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array + val fold_map2' : + ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c + val distinct : 'a array -> bool + val union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b + val rev_to_list : 'a array -> 'a list + val filter_along : ('a -> bool) -> 'a list -> 'b array -> 'b array + val filter_with : bool list -> 'a array -> 'a array +end + +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 equal cmp t1 t2 = + Array.length t1 = Array.length t2 && + let rec aux i = + (i = Array.length t1) || (cmp t1.(i) t2.(i) && aux (i + 1)) + in aux 0 + +let exists f v = + let rec exrec = function + | -1 -> false + | n -> (f v.(n)) || (exrec (n-1)) + in + exrec ((Array.length v)-1) + +let for_all f v = + let rec allrec = function + | -1 -> true + | n -> (f v.(n)) && (allrec (n-1)) + in + allrec ((Array.length v)-1) + +let for_all2 f v1 v2 = + let rec allrec = function + | -1 -> true + | n -> (f v1.(n) v2.(n)) && (allrec (n-1)) + in + let lv1 = Array.length v1 in + lv1 = Array.length v2 && allrec (pred lv1) + +let for_all3 f v1 v2 v3 = + let rec allrec = function + | -1 -> true + | n -> (f v1.(n) v2.(n) v3.(n)) && (allrec (n-1)) + in + let lv1 = Array.length v1 in + lv1 = Array.length v2 && lv1 = Array.length v3 && allrec (pred lv1) + +let for_all4 f v1 v2 v3 v4 = + let rec allrec = function + | -1 -> true + | n -> (f v1.(n) v2.(n) v3.(n) v4.(n)) && (allrec (n-1)) + in + let lv1 = Array.length v1 in + lv1 = Array.length v2 && + lv1 = Array.length v3 && + lv1 = Array.length v4 && + allrec (pred lv1) + +let for_all_i f i v = + let rec allrec i n = n = Array.length v || f i v.(n) && allrec (i+1) (n+1) in + allrec i 0 + +exception Found of int + +let find_i (pred: int -> 'a -> bool) (arr: 'a array) : int option = + try + for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done; + None + with Found i -> Some i + +let hd v = + match Array.length v with + | 0 -> failwith "Array.hd" + | _ -> v.(0) + +let tl v = + match Array.length v with + | 0 -> failwith "Array.tl" + | n -> Array.sub v 1 (pred n) + +let last v = + match Array.length v with + | 0 -> failwith "Array.last" + | n -> v.(pred n) + +let cons e v = Array.append [|e|] v + +let rev t = + let n=Array.length t in + if n <=0 then () + else + let tmp=ref t.(0) in + for i=0 to pred (n/2) do + tmp:=t.((pred n)-i); + t.((pred n)-i)<- t.(i); + t.(i)<- !tmp + done + +let fold_right_i f v a = + let rec fold a n = + if n=0 then a + else + let k = n-1 in + fold (f k v.(k) a) k in + fold a (Array.length v) + +let fold_left_i f v a = + let n = Array.length a in + let rec fold i v = if i = n then v else fold (succ i) (f i v a.(i)) in + fold 0 v + +let fold_right2 f v1 v2 a = + let lv1 = Array.length v1 in + let rec fold a n = + if n=0 then a + else + let k = n-1 in + fold (f v1.(k) v2.(k) a) k in + if Array.length v2 <> lv1 then invalid_arg "Array.fold_right2"; + fold a lv1 + +let fold_left2 f a v1 v2 = + let lv1 = Array.length v1 in + let rec fold a n = + if n >= lv1 then a else fold (f a v1.(n) v2.(n)) (succ n) + in + if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2"; + fold a 0 + +let fold_left2_i f a v1 v2 = + let lv1 = Array.length v1 in + let rec fold a n = + if n >= lv1 then a else fold (f n a v1.(n) v2.(n)) (succ n) + in + if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2"; + fold a 0 + +let fold_left3 f a v1 v2 v3 = + let lv1 = Array.length v1 in + let rec fold a n = + if n >= lv1 then a else fold (f a v1.(n) v2.(n) v3.(n)) (succ n) + in + if Array.length v2 <> lv1 || Array.length v3 <> lv1 then + invalid_arg "Array.fold_left2"; + fold a 0 + +let fold_left_from n f a v = + let rec fold a n = + if n >= Array.length v then a else fold (f a v.(n)) (succ n) + in + fold a n + +let fold_right_from n f v a = + let rec fold n = + if n >= Array.length v then a else f v.(n) (fold (succ n)) + in + fold n + +let app_tl v l = + if Array.length v = 0 then invalid_arg "Array.app_tl"; + fold_right_from 1 (fun e l -> e::l) v l + +let list_of_tl v = + if Array.length v = 0 then invalid_arg "Array.list_of_tl"; + fold_right_from 1 (fun e l -> e::l) v [] + +let map_to_list f v = + List.map f (Array.to_list v) + +let chop n v = + let vlen = Array.length v in + if n > vlen then failwith "Array.chop"; + (Array.sub v 0 n, Array.sub v n (vlen-n)) + +exception Local of int + +(* If none of the elements is changed by f we return ar itself. + The for loop looks for the first such an element. + If found it is temporarily stored in a ref and the new array is produced, + but f is not re-applied to elements that are already checked *) +let smartmap f ar = + let ar_size = Array.length ar in + let aux = ref None in + try + for i = 0 to ar_size-1 do + let a = ar.(i) in + let a' = f a in + if a != a' then (* pointer (in)equality *) begin + aux := Some a'; + raise (Local i) + end + done; + ar + with + Local i -> + let copy j = + if j<i then ar.(j) + else if j=i then + match !aux with Some a' -> a' | None -> failwith "Error" + else f (ar.(j)) + in + Array.init ar_size copy + +let map2 f v1 v2 = + if Array.length v1 <> Array.length v2 then invalid_arg "Array.map2"; + if Array.length v1 == 0 then + [| |] + else begin + let res = Array.create (Array.length v1) (f v1.(0) v2.(0)) in + for i = 1 to pred (Array.length v1) do + res.(i) <- f v1.(i) v2.(i) + done; + res + end + +let map2_i f v1 v2 = + if Array.length v1 <> Array.length v2 then invalid_arg "Array.map2"; + if Array.length v1 == 0 then + [| |] + else begin + let res = Array.create (Array.length v1) (f 0 v1.(0) v2.(0)) in + for i = 1 to pred (Array.length v1) do + res.(i) <- f i v1.(i) v2.(i) + done; + res + end + +let map3 f v1 v2 v3 = + if Array.length v1 <> Array.length v2 || + Array.length v1 <> Array.length v3 then invalid_arg "Array.map3"; + if Array.length v1 == 0 then + [| |] + else begin + let res = Array.create (Array.length v1) (f v1.(0) v2.(0) v3.(0)) in + for i = 1 to pred (Array.length v1) do + res.(i) <- f v1.(i) v2.(i) v3.(i) + done; + res + end + +let map_left f a = (* Ocaml does not guarantee Array.map is LR *) + let l = Array.length a in (* (even if so), then we rewrite it *) + if l = 0 then [||] else begin + let r = Array.create l (f a.(0)) in + for i = 1 to l - 1 do + r.(i) <- f a.(i) + done; + r + end + +let map_left_pair f a g b = + let l = Array.length a in + if l = 0 then [||],[||] else begin + let r = Array.create l (f a.(0)) in + let s = Array.create l (g b.(0)) in + for i = 1 to l - 1 do + r.(i) <- f a.(i); + s.(i) <- g b.(i) + done; + r, s + end + +let iter2 f v1 v2 = + let n = Array.length v1 in + if Array.length v2 <> n then invalid_arg "Array.iter2" + else for i = 0 to n - 1 do f v1.(i) v2.(i) done + +let pure_functional = false + +let fold_map' f v e = +if pure_functional then + let (l,e) = + Array.fold_right + (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) + v ([],e) in + (Array.of_list l,e) +else + let e' = ref e in + let v' = Array.map (fun x -> let (y,e) = f x !e' in e' := e; y) v in + (v',!e') + +let fold_map f e v = + let e' = ref e in + let v' = Array.map (fun x -> let (e,y) = f !e' x in e' := e; y) v in + (!e',v') + +let fold_map2' f v1 v2 e = + let e' = ref e in + let v' = + map2 (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2 + in + (v',!e') + +let distinct v = + let visited = Hashtbl.create 23 in + try + Array.iter + (fun x -> + if Hashtbl.mem visited x then raise Exit + else Hashtbl.add visited x x) + v; + true + with Exit -> false + +let union_map f a acc = + Array.fold_left + (fun x y -> f y x) + acc + a + +let rev_to_list a = + let rec tolist i res = + if i >= Array.length a then res else tolist (i+1) (a.(i) :: res) in + tolist 0 [] + +let filter_along f filter v = + Array.of_list (CList.filter_along f filter (Array.to_list v)) + +let filter_with filter v = + Array.of_list (CList.filter_with filter (Array.to_list v)) + diff --git a/lib/cArray.mli b/lib/cArray.mli new file mode 100644 index 000000000..bf5648881 --- /dev/null +++ b/lib/cArray.mli @@ -0,0 +1,98 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *) + +module type S = +sig + external length : 'a array -> int = "%array_length" + external get : 'a array -> int -> 'a = "%array_safe_get" + external set : 'a array -> int -> 'a -> unit = "%array_safe_set" + external make : int -> 'a -> 'a array = "caml_make_vect" + external create : int -> 'a -> 'a array = "caml_make_vect" + val init : int -> (int -> 'a) -> 'a array + val make_matrix : int -> int -> 'a -> 'a array array + val create_matrix : int -> int -> 'a -> 'a array array + val append : 'a array -> 'a array -> 'a array + val concat : 'a array list -> 'a array + val sub : 'a array -> int -> int -> 'a array + val copy : 'a array -> 'a array + val fill : 'a array -> int -> int -> 'a -> unit + val blit : 'a array -> int -> 'a array -> int -> int -> unit + val to_list : 'a array -> 'a list + val of_list : 'a list -> 'a array + val iter : ('a -> unit) -> 'a array -> unit + val map : ('a -> 'b) -> 'a array -> 'b array + val iteri : (int -> 'a -> unit) -> 'a array -> unit + val mapi : (int -> 'a -> 'b) -> 'a array -> 'b array + val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a + val fold_right : ('b -> 'a -> 'a) -> 'b array -> 'a -> 'a + val sort : ('a -> 'a -> int) -> 'a array -> unit + val stable_sort : ('a -> 'a -> int) -> 'a array -> unit + val fast_sort : ('a -> 'a -> int) -> 'a array -> unit + external unsafe_get : 'a array -> int -> 'a = "%array_unsafe_get" + external unsafe_set : 'a array -> int -> 'a -> unit = "%array_unsafe_set" +end + +module type ExtS = +sig + include S + val compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int + val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool + val exists : ('a -> bool) -> 'a array -> bool + val for_all : ('a -> bool) -> 'a array -> bool + val for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool + val for_all3 : ('a -> 'b -> 'c -> bool) -> + 'a array -> 'b array -> 'c array -> bool + val for_all4 : ('a -> 'b -> 'c -> 'd -> bool) -> + 'a array -> 'b array -> 'c array -> 'd array -> bool + val for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool + val find_i : (int -> 'a -> bool) -> 'a array -> int option + val hd : 'a array -> 'a + val tl : 'a array -> 'a array + val last : 'a array -> 'a + val cons : 'a -> 'a array -> 'a array + val rev : 'a array -> unit + val fold_right_i : + (int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a + val fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a + val fold_right2 : + ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c + val fold_left2 : + ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a + val fold_left3 : + ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a + val fold_left2_i : + (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a + val fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a + val fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b + val app_tl : 'a array -> 'a list -> 'a list + val list_of_tl : 'a array -> 'a list + val map_to_list : ('a -> 'b) -> 'a array -> 'b list + val chop : int -> 'a array -> 'a array * 'a array + val smartmap : ('a -> 'a) -> 'a array -> 'a array + val map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array + val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array + val map3 : + ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array + val map_left : ('a -> 'b) -> 'a array -> 'b array + val map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array -> + 'b array * 'd array + val iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit + val fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c + val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array + val fold_map2' : + ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c + val distinct : 'a array -> bool + val union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b + val rev_to_list : 'a array -> 'a list + val filter_along : ('a -> bool) -> 'a list -> 'b array -> 'b array + val filter_with : bool list -> 'a array -> 'a array +end + +include ExtS diff --git a/lib/clib.mllib b/lib/clib.mllib index 5b0e14f1e..3716a1021 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -5,6 +5,7 @@ Segmenttree Unicodetable Deque CList +CArray Util Serialize Xml_utils diff --git a/lib/rtree.ml b/lib/rtree.ml index 18ba9d0ef..130bbcf2f 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -103,13 +103,13 @@ let rec map f t = match t with let smartmap f t = match t with Param _ -> t | Node (a,sons) -> - let a'=f a and sons' = Util.array_smartmap (map f) sons in + let a'=f a and sons' = Util.Array.smartmap (map f) sons in if a'==a && sons'==sons then t else Node (a',sons') | Rec(j,defs) -> - let defs' = Util.array_smartmap (map f) defs in + let defs' = Util.Array.smartmap (map f) defs in if defs'==defs then t else @@ -134,7 +134,7 @@ let is_infinite t = fold (fun seen t is_inf -> seen || (match t with - Node(_,v) -> array_exists is_inf v + Node(_,v) -> Array.exists is_inf v | Param _ -> false | _ -> assert false)) t @@ -154,7 +154,7 @@ let compare_rtree f = fold2 else if b > 0 then true else match expand t1, expand t2 with Node(_,v1), Node(_,v2) when Array.length v1 = Array.length v2 -> - array_for_all2 cmp v1 v2 + Array.for_all2 cmp v1 v2 | _ -> false) let eq_rtree cmp t1 t2 = diff --git a/lib/util.ml b/lib/util.ml index 523579d1f..42ad11ee1 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -363,332 +363,15 @@ let ascii_of_ident s = done with End_of_input -> () end; !out +(* Lists *) + module List : CList.ExtS = CList let (@) = CList.append (* Arrays *) -let array_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 array_equal cmp t1 t2 = - Array.length t1 = Array.length t2 && - let rec aux i = - (i = Array.length t1) || (cmp t1.(i) t2.(i) && aux (i + 1)) - in aux 0 - -let array_exists f v = - let rec exrec = function - | -1 -> false - | n -> (f v.(n)) || (exrec (n-1)) - in - exrec ((Array.length v)-1) - -let array_for_all f v = - let rec allrec = function - | -1 -> true - | n -> (f v.(n)) && (allrec (n-1)) - in - allrec ((Array.length v)-1) - -let array_for_all2 f v1 v2 = - let rec allrec = function - | -1 -> true - | n -> (f v1.(n) v2.(n)) && (allrec (n-1)) - in - let lv1 = Array.length v1 in - lv1 = Array.length v2 && allrec (pred lv1) - -let array_for_all3 f v1 v2 v3 = - let rec allrec = function - | -1 -> true - | n -> (f v1.(n) v2.(n) v3.(n)) && (allrec (n-1)) - in - let lv1 = Array.length v1 in - lv1 = Array.length v2 && lv1 = Array.length v3 && allrec (pred lv1) - -let array_for_all4 f v1 v2 v3 v4 = - let rec allrec = function - | -1 -> true - | n -> (f v1.(n) v2.(n) v3.(n) v4.(n)) && (allrec (n-1)) - in - let lv1 = Array.length v1 in - lv1 = Array.length v2 && - lv1 = Array.length v3 && - lv1 = Array.length v4 && - allrec (pred lv1) - -let array_for_all_i f i v = - let rec allrec i n = n = Array.length v || f i v.(n) && allrec (i+1) (n+1) in - allrec i 0 - -exception Found of int - -let array_find_i (pred: int -> 'a -> bool) (arr: 'a array) : int option = - try - for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done; - None - with Found i -> Some i - -let array_hd v = - match Array.length v with - | 0 -> failwith "array_hd" - | _ -> v.(0) - -let array_tl v = - match Array.length v with - | 0 -> failwith "array_tl" - | n -> Array.sub v 1 (pred n) - -let array_last v = - match Array.length v with - | 0 -> failwith "array_last" - | n -> v.(pred n) - -let array_cons e v = Array.append [|e|] v - -let array_rev t = - let n=Array.length t in - if n <=0 then () - else - let tmp=ref t.(0) in - for i=0 to pred (n/2) do - tmp:=t.((pred n)-i); - t.((pred n)-i)<- t.(i); - t.(i)<- !tmp - done - -let array_fold_right_i f v a = - let rec fold a n = - if n=0 then a - else - let k = n-1 in - fold (f k v.(k) a) k in - fold a (Array.length v) - -let array_fold_left_i f v a = - let n = Array.length a in - let rec fold i v = if i = n then v else fold (succ i) (f i v a.(i)) in - fold 0 v - -let array_fold_right2 f v1 v2 a = - let lv1 = Array.length v1 in - let rec fold a n = - if n=0 then a - else - let k = n-1 in - fold (f v1.(k) v2.(k) a) k in - if Array.length v2 <> lv1 then invalid_arg "array_fold_right2"; - fold a lv1 - -let array_fold_left2 f a v1 v2 = - let lv1 = Array.length v1 in - let rec fold a n = - if n >= lv1 then a else fold (f a v1.(n) v2.(n)) (succ n) - in - if Array.length v2 <> lv1 then invalid_arg "array_fold_left2"; - fold a 0 - -let array_fold_left2_i f a v1 v2 = - let lv1 = Array.length v1 in - let rec fold a n = - if n >= lv1 then a else fold (f n a v1.(n) v2.(n)) (succ n) - in - if Array.length v2 <> lv1 then invalid_arg "array_fold_left2"; - fold a 0 - -let array_fold_left3 f a v1 v2 v3 = - let lv1 = Array.length v1 in - let rec fold a n = - if n >= lv1 then a else fold (f a v1.(n) v2.(n) v3.(n)) (succ n) - in - if Array.length v2 <> lv1 || Array.length v3 <> lv1 then - invalid_arg "array_fold_left2"; - fold a 0 - -let array_fold_left_from n f a v = - let rec fold a n = - if n >= Array.length v then a else fold (f a v.(n)) (succ n) - in - fold a n - -let array_fold_right_from n f v a = - let rec fold n = - if n >= Array.length v then a else f v.(n) (fold (succ n)) - in - fold n - -let array_app_tl v l = - if Array.length v = 0 then invalid_arg "array_app_tl"; - array_fold_right_from 1 (fun e l -> e::l) v l - -let array_list_of_tl v = - if Array.length v = 0 then invalid_arg "array_list_of_tl"; - array_fold_right_from 1 (fun e l -> e::l) v [] - -let array_map_to_list f v = - List.map f (Array.to_list v) - -let array_chop n v = - let vlen = Array.length v in - if n > vlen then failwith "array_chop"; - (Array.sub v 0 n, Array.sub v n (vlen-n)) - -exception Local of int - -(* If none of the elements is changed by f we return ar itself. - The for loop looks for the first such an element. - If found it is temporarily stored in a ref and the new array is produced, - but f is not re-applied to elements that are already checked *) -let array_smartmap f ar = - let ar_size = Array.length ar in - let aux = ref None in - try - for i = 0 to ar_size-1 do - let a = ar.(i) in - let a' = f a in - if a != a' then (* pointer (in)equality *) begin - aux := Some a'; - raise (Local i) - end - done; - ar - with - Local i -> - let copy j = - if j<i then ar.(j) - else if j=i then - match !aux with Some a' -> a' | None -> failwith "Error" - else f (ar.(j)) - in - Array.init ar_size copy - -let array_map2 f v1 v2 = - if Array.length v1 <> Array.length v2 then invalid_arg "array_map2"; - if Array.length v1 == 0 then - [| |] - else begin - let res = Array.create (Array.length v1) (f v1.(0) v2.(0)) in - for i = 1 to pred (Array.length v1) do - res.(i) <- f v1.(i) v2.(i) - done; - res - end - -let array_map2_i f v1 v2 = - if Array.length v1 <> Array.length v2 then invalid_arg "array_map2"; - if Array.length v1 == 0 then - [| |] - else begin - let res = Array.create (Array.length v1) (f 0 v1.(0) v2.(0)) in - for i = 1 to pred (Array.length v1) do - res.(i) <- f i v1.(i) v2.(i) - done; - res - end - -let array_map3 f v1 v2 v3 = - if Array.length v1 <> Array.length v2 || - Array.length v1 <> Array.length v3 then invalid_arg "array_map3"; - if Array.length v1 == 0 then - [| |] - else begin - let res = Array.create (Array.length v1) (f v1.(0) v2.(0) v3.(0)) in - for i = 1 to pred (Array.length v1) do - res.(i) <- f v1.(i) v2.(i) v3.(i) - done; - res - end - -let array_map_left f a = (* Ocaml does not guarantee Array.map is LR *) - let l = Array.length a in (* (even if so), then we rewrite it *) - if l = 0 then [||] else begin - let r = Array.create l (f a.(0)) in - for i = 1 to l - 1 do - r.(i) <- f a.(i) - done; - r - end - -let array_map_left_pair f a g b = - let l = Array.length a in - if l = 0 then [||],[||] else begin - let r = Array.create l (f a.(0)) in - let s = Array.create l (g b.(0)) in - for i = 1 to l - 1 do - r.(i) <- f a.(i); - s.(i) <- g b.(i) - done; - r, s - end - -let array_iter2 f v1 v2 = - let n = Array.length v1 in - if Array.length v2 <> n then invalid_arg "array_iter2" - else for i = 0 to n - 1 do f v1.(i) v2.(i) done - -let pure_functional = false - -let array_fold_map' f v e = -if pure_functional then - let (l,e) = - Array.fold_right - (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) - v ([],e) in - (Array.of_list l,e) -else - let e' = ref e in - let v' = Array.map (fun x -> let (y,e) = f x !e' in e' := e; y) v in - (v',!e') - -let array_fold_map f e v = - let e' = ref e in - let v' = Array.map (fun x -> let (e,y) = f !e' x in e' := e; y) v in - (!e',v') - -let array_fold_map2' f v1 v2 e = - let e' = ref e in - let v' = - array_map2 (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2 - in - (v',!e') - -let array_distinct v = - let visited = Hashtbl.create 23 in - try - Array.iter - (fun x -> - if Hashtbl.mem visited x then raise Exit - else Hashtbl.add visited x x) - v; - true - with Exit -> false - -let array_union_map f a acc = - Array.fold_left - (fun x y -> f y x) - acc - a - -let array_rev_to_list a = - let rec tolist i res = - if i >= Array.length a then res else tolist (i+1) (a.(i) :: res) in - tolist 0 [] - -let array_filter_along f filter v = - Array.of_list (CList.filter_along f filter (Array.to_list v)) - -let array_filter_with filter v = - Array.of_list (CList.filter_with filter (Array.to_list v)) +module Array : CArray.ExtS = CArray (* Matrices *) diff --git a/lib/util.mli b/lib/util.mli index 58de91d37..abfab29d5 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -77,57 +77,7 @@ val (@) : 'a list -> 'a list -> 'a list (** {6 Arrays. } *) -val array_compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int -val array_equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool -val array_exists : ('a -> bool) -> 'a array -> bool -val array_for_all : ('a -> bool) -> 'a array -> bool -val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool -val array_for_all3 : ('a -> 'b -> 'c -> bool) -> - 'a array -> 'b array -> 'c array -> bool -val array_for_all4 : ('a -> 'b -> 'c -> 'd -> bool) -> - 'a array -> 'b array -> 'c array -> 'd array -> bool -val array_for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool -val array_find_i : (int -> 'a -> bool) -> 'a array -> int option -val array_hd : 'a array -> 'a -val array_tl : 'a array -> 'a array -val array_last : 'a array -> 'a -val array_cons : 'a -> 'a array -> 'a array -val array_rev : 'a array -> unit -val array_fold_right_i : - (int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a -val array_fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a -val array_fold_right2 : - ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c -val array_fold_left2 : - ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a -val array_fold_left3 : - ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a -val array_fold_left2_i : - (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a -val array_fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a -val array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b -val array_app_tl : 'a array -> 'a list -> 'a list -val array_list_of_tl : 'a array -> 'a list -val array_map_to_list : ('a -> 'b) -> 'a array -> 'b list -val array_chop : int -> 'a array -> 'a array * 'a array -val array_smartmap : ('a -> 'a) -> 'a array -> 'a array -val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array -val array_map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array -val array_map3 : - ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array -val array_map_left : ('a -> 'b) -> 'a array -> 'b array -val array_map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array -> - 'b array * 'd array -val array_iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit -val array_fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c -val array_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array -val array_fold_map2' : - ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c -val array_distinct : 'a array -> bool -val array_union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b -val array_rev_to_list : 'a array -> 'a list -val array_filter_along : ('a -> bool) -> 'a list -> 'b array -> 'b array -val array_filter_with : bool list -> 'a array -> 'a array +module Array : CArray.ExtS (** {6 Streams. } *) diff --git a/library/impargs.ml b/library/impargs.ml index baf2e30ec..cc4a4e45e 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -168,8 +168,8 @@ let push_lift d (e,n) = (push_rel d e,n+1) let is_reversible_pattern bound depth f l = isRel f & let n = destRel f in (n < bound+depth) & (n >= depth) & - array_for_all (fun c -> isRel c & destRel c < depth) l & - array_distinct l + Array.for_all (fun c -> isRel c & destRel c < depth) l & + Array.distinct l (* Precondition: rels in env are for inductive types only *) let add_free_rels_until strict strongly_strict revpat bound env m pos acc = @@ -413,7 +413,7 @@ let compute_mib_implicits flags manual kn = let compute_all_mib_implicits flags manual kn = let imps = compute_mib_implicits flags manual kn in List.flatten - (array_map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps) + (Array.map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps) (*s Variables. *) @@ -606,7 +606,7 @@ let declare_constant_implicits con = let declare_mib_implicits kn = let flags = !implicit_args in - let imps = array_map_to_list + let imps = Array.map_to_list (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) (compute_mib_implicits flags [] kn) in add_anonymous_leaf diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 8af15a1d5..04038b1a7 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -396,7 +396,7 @@ let rec canonize_name c = | LetIn (na,b,t,ct) -> mkLetIn (na, func b,func t,func ct) | App (ct,l) -> - mkApp (func ct,array_smartmap func l) + mkApp (func ct,Array.smartmap func l) | _ -> c (* rebuild a term from a pattern and a substitution *) @@ -502,7 +502,7 @@ let is_redundant state id args = let prev_args = Identhash.find_all state.q_history id in List.exists (fun old_args -> - Util.array_for_all2 (fun i j -> i = find state.uf j) + Util.Array.for_all2 (fun i j -> i = find state.uf j) norm_args old_args) prev_args with Not_found -> false @@ -518,7 +518,7 @@ let add_inst state (inst,int_subst) = let subst = build_subst (forest state) int_subst in let prfhead= mkVar inst.qe_hyp_id in let args = Array.map constr_of_term subst in - let _ = array_rev args in (* highest deBruijn index first *) + let _ = Array.rev args in (* highest deBruijn index first *) let prf= mkApp(prfhead,args) in let s = inst_pattern subst inst.qe_lhs and t = inst_pattern subst inst.qe_rhs in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 423c95509..3b2e42d4e 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -101,7 +101,7 @@ let rec pattern_of_constr env sigma c = App (f,args)-> let pf = decompose_term env sigma f in let pargs,lrels = List.split - (array_map_to_list (pattern_of_constr env sigma) args) in + (Array.map_to_list (pattern_of_constr env sigma) args) in PApp (pf,List.rev pargs), List.fold_left Intset.union Intset.empty lrels | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) -> diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index b5cdec3ec..aaf6f2bd0 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -141,8 +141,8 @@ let check_fix env cb i = let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) = na1 = na2 && - array_equal eq_constr ca1 ca2 && - array_equal eq_constr ta1 ta2 + Array.equal eq_constr ca1 ca2 && + Array.equal eq_constr ta1 ta2 let factor_fix env l cb msb = let _,recd as check = check_fix env cb 0 in @@ -287,7 +287,7 @@ let rec extract_sfb env mp all = function let vl,recd,msb = factor_fix env l cb msb in let vc = Array.map (make_con mp empty_dirpath) vl in let ms = extract_sfb env mp all msb in - let b = array_exists Visit.needed_con vc in + let b = Array.exists Visit.needed_con vc in if all || b then let d = extract_fixpoint env vc recd in if (not b) && (logical_decl d) then ms diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index e1bbcf9c7..ef0de36f5 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -202,7 +202,7 @@ let oib_equal o1 o2 = o1.mind_consnames = o2.mind_consnames let mib_equal m1 m2 = - array_equal oib_equal m1.mind_packets m1.mind_packets && + Array.equal oib_equal m1.mind_packets m1.mind_packets && m1.mind_record = m2.mind_record && m1.mind_finite = m2.mind_finite && m1.mind_ntypes = m2.mind_ntypes && @@ -833,7 +833,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = let metas = Array.map new_meta fi in metas.(i) <- mlt; let mle = Array.fold_left Mlenv.push_type mle metas in - let ei = array_map2 (extract_maybe_term env mle) metas ci in + let ei = Array.map2 (extract_maybe_term env mle) metas ci in MLfix (i, Array.map id_of_name fi, ei) (*S ML declarations. *) @@ -859,7 +859,7 @@ let rec gentypvar_ok c = match kind_of_term c with | App (c,v) -> (* if all arguments are variables, these variables will disappear after extraction (see [empty_s] below) *) - array_for_all isRel v && gentypvar_ok c + Array.for_all isRel v && gentypvar_ok c | Cast (c,_,_) -> gentypvar_ok c | _ -> false @@ -1053,9 +1053,9 @@ let logical_decl = function | Dterm (_,MLdummy,Tdummy _) -> true | Dtype (_,[],Tdummy _) -> true | Dfix (_,av,tv) -> - (array_for_all ((=) MLdummy) av) && - (array_for_all isDummy tv) - | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets + (Array.for_all ((=) MLdummy) av) && + (Array.for_all isDummy tv) + | Dind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets | _ -> false (*s Is a [ml_spec] logical ? *) @@ -1063,5 +1063,5 @@ let logical_decl = function let logical_spec = function | Stype (_, [], Some (Tdummy _)) -> true | Sval (_,Tdummy _) -> true - | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets + | Sind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets | _ -> false diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 2bc2306f1..4fd9f17ee 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -224,7 +224,7 @@ and pp_fix par env i (ids,bl) args = (v 1 (str "let {" ++ fnl () ++ prvect_with_sep (fun () -> str ";" ++ fnl ()) (fun (fi,ti) -> pp_function env (pr_id fi) ti) - (array_map2 (fun a b -> a,b) ids bl) ++ + (Array.map2 (fun a b -> a,b) ids bl) ++ str "}") ++ fnl () ++ str "in " ++ pp_apply (pr_id ids.(i)) false args)) diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 3716695b8..01b98b131 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -524,7 +524,7 @@ let has_deep_pattern br = | Pcons (_,l) | Ptuple l -> not (List.for_all is_basic_pattern l) | Pusual _ | Prel _ | Pwild -> false in - array_exists (function (_,pat,_) -> deep pat) br + Array.exists (function (_,pat,_) -> deep pat) br let is_regular_match br = if Array.length br = 0 then false (* empty match becomes MLexn *) @@ -543,7 +543,7 @@ let is_regular_match br = | ConstructRef (ind,_) -> ind | _ -> raise Impossible in - array_for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br + Array.for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br with Impossible -> false (*S Operations concerning lambdas. *) @@ -770,7 +770,7 @@ let is_opt_pat (_,p,_) = match p with | _ -> false let factor_branches o typ br = - if array_exists is_opt_pat br then None (* already optimized *) + if Array.exists is_opt_pat br then None (* already optimized *) else begin census_clean (); for i = 0 to Array.length br - 1 do diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 8659de03e..9247baba2 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -270,7 +270,7 @@ let rec optim_se top to_appear s = function else all := false done; if !all && top && not (library ()) - && (array_for_all (fun r -> not (List.mem r to_appear)) rv) + && (Array.for_all (fun r -> not (List.mem r to_appear)) rv) then optim_se top to_appear s lse else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse) | (l,SEmodule m) :: lse -> diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 951049b7b..78126bc16 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -374,7 +374,7 @@ and pp_fix par env i (ids,bl) args = prvect_with_sep (fun () -> fnl () ++ str "and ") (fun (fi,ti) -> pr_id fi ++ pp_function env ti) - (array_map2 (fun id b -> (id,b)) ids bl) ++ + (Array.map2 (fun id b -> (id,b)) ids bl) ++ fnl () ++ hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args))) diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index ec338b1db..a0a59e73c 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -163,7 +163,7 @@ and pp_fix env j (ids,bl) args = (prvect_with_sep fnl (fun (fi,ti) -> paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti))) - (array_map2 (fun id b -> (id,b)) ids bl)) ++ + (Array.map2 (fun id b -> (id,b)) ids bl)) ++ fnl () ++ hov 2 (pp_apply (pr_id (ids.(j))) true args)))) diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index f4cc397bc..d224f87df 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -95,7 +95,7 @@ let kind_of_formula gl term = let is_trivial= let is_constant c = nb_prod c = mib.mind_nparams in - array_exists is_constant mip.mind_nf_lc in + Array.exists is_constant mip.mind_nf_lc in if Inductiveops.mis_is_recursive (ind,mib,mip) || (has_realargs && not is_trivial) then @@ -144,7 +144,7 @@ let build_atoms gl metagen side cciterm = let f l = List.fold_left_i g (1-(List.length l)) () l in if polarity && (* we have a constant constructor *) - array_exists (function []->true|_->false) v + Array.exists (function []->true|_->false) v then trivial:=true; Array.iter f v | Exists(i,l)-> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 0796930fc..3505c4d9b 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -371,7 +371,7 @@ let is_property ptes_info t_x full_type_of_hyp = if isApp t_x then let pte,args = destApp t_x in - if isVar pte && array_for_all closed0 args + if isVar pte && Array.for_all closed0 args then try let info = Idmap.find (destVar pte) ptes_info in @@ -1415,11 +1415,11 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = tclFIRST (List.map Equality.rewriteRL eqs ) in let _,hrec_concl = decompose_prod (pf_type_of gls (mkVar hrec)) in - let f_app = array_last (snd (destApp hrec_concl)) in + let f_app = Array.last (snd (destApp hrec_concl)) in let f = (fst (destApp f_app)) in let rec backtrack : tactic = fun g -> - let f_app = array_last (snd (destApp (pf_concl g))) in + let f_app = Array.last (snd (destApp (pf_concl g))) in match kind_of_term f_app with | App(f',_) when eq_constr f' f -> tclIDTAC g | _ -> tclTHEN rewrite backtrack g @@ -1658,7 +1658,7 @@ let prove_principle_for_gen (* observe_tac "finish" *) (fun gl' -> let body = let _,args = destApp (pf_concl gl') in - array_last args + Array.last args in let body_info rec_hyps = { diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index f2eb4b23c..b97fc48f1 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -154,7 +154,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = compute_new_princ_type_for_binder remove mkLambda env x t b | Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved | App(f,args) when is_dom f -> - let var_to_be_removed = destRel (array_last args) in + let var_to_be_removed = destRel (Array.last args) in let num = get_fun_num f in raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement pre_princ num args)) | App(f,args) -> @@ -479,7 +479,7 @@ let get_funs_constant mp dp = let first_infos = extract_info true (List.hd l_bodies) in let check body = (* Hope this is correct *) let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) = - ia1 = ia2 && na1 = na2 && array_equal eq_constr ta1 ta2 && array_equal eq_constr ca1 ca2 + ia1 = ia2 && na1 = na2 && Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2 in if not (eq_infos first_infos (extract_info false body)) then error "Not a mutal recursive block" diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 1c2193449..490d52555 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1240,7 +1240,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b try List.iter_i (fun i ((n,nt,is_defined) as param) -> - if array_for_all + if Array.for_all (fun l -> let (n',nt',is_defined') = List.nth l i in n = n' && Notation_ops.eq_glob_constr nt nt' && is_defined = is_defined') @@ -1319,7 +1319,7 @@ let do_build_inductive Then save the graphs and reset Printing options to their primitive values *) let rel_arities = Array.mapi rel_arity funsargs in - Util.array_fold_left2 (fun env rel_name rel_ar -> + Util.Array.fold_left2 (fun env rel_name rel_ar -> Environ.push_named (rel_name,None, Constrintern.interp_constr Evd.empty env rel_ar) env) env relnames rel_arities in (* and of the real constructors*) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 1d1089a54..d8255e834 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -358,7 +358,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem | App(eq,args), App(graph',_) when (eq_constr eq eq_ind) && - array_exists (eq_constr graph') graphs_constr -> + Array.exists (eq_constr graph') graphs_constr -> (args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) ::acc) | _ -> mkVar hid :: acc @@ -599,7 +599,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem | App(eq,args), App(graph',_) when (eq_constr eq eq_ind) && - array_exists (eq_constr graph') graphs_constr -> + Array.exists (eq_constr graph') graphs_constr -> ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) ::args.(2)::acc) | _ -> mkVar hid :: acc @@ -1029,7 +1029,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g try let graphs_constr = Array.map mkInd graphs in let lemmas_types_infos = - Util.array_map2_i + Util.Array.map2_i (fun i f_constr graph -> let const_of_f = destConst f_constr in let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = @@ -1056,7 +1056,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g (fun entry -> (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type ) ) - (make_scheme (array_map_to_list (fun const -> const,GType None) funs)) + (make_scheme (Array.map_to_list (fun const -> const,GType None) funs)) ) in let proving_tac = @@ -1083,7 +1083,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g ) funs; let lemmas_types_infos = - Util.array_map2_i + Util.Array.map2_i (fun i f_constr graph -> let const_of_f = destConst f_constr in let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info = @@ -1169,7 +1169,7 @@ let revert_graph kn post_tac hid g = match info.completeness_lemma with | None -> tclIDTAC g | Some f_complete -> - let f_args,res = array_chop (Array.length args - 1) args in + let f_args,res = Array.chop (Array.length args - 1) args in tclTHENSEQ [ h_generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]; diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 21c0d86a4..5915d3c0d 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -153,17 +153,9 @@ exception Found of int (* Array scanning *) let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int = - try - for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done; - Array.length arr (* all elt are positive *) - with Found i -> i - -let array_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b array): 'a = - let i = ref 0 in - Array.fold_left - (fun acc x -> - let res = f !i acc x in i := !i + 1; res) - acc arr +match Array.find_i pred arr with +| None -> Array.length arr (* all elt are positive *) +| Some i -> i (* Like List.chop but except that [i] is the size of the suffix of [l]. *) let list_chop_end i l = @@ -660,7 +652,7 @@ let rec merge_types shift accrec1 returns the list of unlinked vars of [allargs2]. *) let build_link_map_aux (allargs1:identifier array) (allargs2:identifier array) (lnk:int merged_arg array) = - array_fold_lefti + Array.fold_left_i (fun i acc e -> if i = Array.length lnk - 1 then acc (* functional arg, not in allargs *) else @@ -939,7 +931,7 @@ let merge (id1:identifier) (id2:identifier) (args1:identifier array) as above: vars may be linked inside args2?? *) Array.mapi (fun i c -> - match array_find_i (fun i x -> x=c) args1 with + match Array.find_i (fun i x -> x=c) args1 with | Some j -> Linked j | None -> Unlinked) args2 in diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 8dbb75cdc..311ab3081 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -211,7 +211,7 @@ let compute_rhs bodyi index_of_f = let rec aux c = match kind_of_term c with | App (j, args) when isRel j && destRel j = index_of_f (* recursive call *) -> - let i = destRel (array_last args) in + let i = destRel (Array.last args) in PMeta (Some (coerce_meta_in i)) | App (f,args) -> PApp (snd (pattern_of_constr Evd.empty f), Array.map aux args) @@ -301,7 +301,7 @@ let rec closed_under cset t = (ConstrSet.mem t cset) or (match (kind_of_term t) with | Cast(c,_,_) -> closed_under cset c - | App(f,l) -> closed_under cset f && array_for_all (closed_under cset) l + | App(f,l) -> closed_under cset f && Array.for_all (closed_under cset) l | _ -> false) (*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete @@ -362,7 +362,7 @@ let path_of_int n = let rec subterm gl (t : constr) (t' : constr) = (pf_conv_x gl t t') or (match (kind_of_term t) with - | App (f,args) -> array_exists (fun t -> subterm gl t t') args + | App (f,args) -> Array.exists (fun t -> subterm gl t t') args | Cast(t,_,_) -> (subterm gl t t') | _ -> false) diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index f838b56c6..abf142e79 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -65,7 +65,7 @@ let rec mk_clos_but f_map subs t = and mk_clos_app_but f_map subs f args n = if n >= Array.length args then mk_atom(mkApp(f, args)) else - let fargs, args' = array_chop n args in + let fargs, args' = Array.chop n args in let f' = mkApp(f,fargs) in match f_map f' with Some map -> diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 196f5a0e7..0ece3496e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1016,7 +1016,7 @@ let rec ungeneralize n ng body = let sign2,p = decompose_prod_n_assum ng p in let p = prod_applist p [mkRel (n+List.length sign+ng)] in it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in - mkCase (ci,p,c,array_map2 (fun q c -> + mkCase (ci,p,c,Array.map2 (fun q c -> let sign,b = decompose_lam_n_assum q c in it_mkLambda_or_LetIn (ungeneralize (n+q) ng b) sign) ci.ci_cstr_ndecls brs) @@ -1046,7 +1046,7 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs = let pred = lift_predicate (-1) pred tomatch in let tomatch = relocate_index_tomatch 1 (n+1) tomatch in let tomatch = lift_tomatch_stack (-1) tomatch in - let brs = array_map2 (ungeneralize_branch n k) brs cs in + let brs = Array.map2 (ungeneralize_branch n k) brs cs in aux k brs tomatch pred tocheck deps | _ -> assert false in aux 0 brs tomatch pred tocheck deps @@ -1255,7 +1255,7 @@ and match_current pb tomatch = let pb,deps = generalize_problem (names,dep) pb deps in (* We compile branches *) - let brvals = array_map2 (compile_branch current realargs (names,dep) deps pb arsign) eqns cstrs in + let brvals = Array.map2 (compile_branch current realargs (names,dep) deps pb arsign) eqns cstrs in (* We build the (elementary) case analysis *) let depstocheck = current::binding_vars_of_inductive typ in let brvals,tomatch,pred,inst = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index d30c1a11f..da5ccc96b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -350,8 +350,8 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | IfStyle when aliastyp = None -> let bl' = Array.map detype bl in let nondepbrs = - array_map3 (extract_nondep_branches testdep) bl bl' consnargsl in - if array_for_all ((<>) None) nondepbrs then + Array.map3 (extract_nondep_branches testdep) bl bl' consnargsl in + if Array.for_all ((<>) None) nondepbrs then GIf (dl,tomatch,(alias,pred), Option.get nondepbrs.(0),Option.get nondepbrs.(1)) else @@ -405,7 +405,7 @@ let rec detype (isgoal:bool) avoid env t = | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c | App (f,args) -> GApp (dl,detype isgoal avoid env f, - array_map_to_list (detype isgoal avoid env) args) + Array.map_to_list (detype isgoal avoid env) args) | Const sp -> GRef (dl, ConstRef sp) | Evar (ev,cl) -> GEvar (dl, ev, @@ -433,7 +433,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) = (id::avoid, add_name (Name id) env, id::l)) (avoid, env, []) names in let n = Array.length tys in - let v = array_map3 + let v = Array.map3 (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t)) bodies tys vn in GRec(dl,GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), @@ -449,7 +449,7 @@ and detype_cofix isgoal avoid env n (names,tys,bodies) = (id::avoid, add_name (Name id) env, id::l)) (avoid, env, []) names in let ntys = Array.length tys in - let v = array_map2 + let v = Array.map2 (fun c t -> share_names isgoal 0 [] def_avoid def_env c (lift ntys t)) bodies tys in GRec(dl,GCoFix n,Array.of_list (List.rev lfi), @@ -501,7 +501,7 @@ and detype_eqns isgoal avoid env ci computable constructs consnargsl bl = mat with _ -> Array.to_list - (array_map3 (detype_eqn isgoal avoid env) constructs consnargsl bl) + (Array.map3 (detype_eqn isgoal avoid env) constructs consnargsl bl) and detype_eqn isgoal avoid env constr construct_nargs branch = let make_pat x avoid env b ids = @@ -653,9 +653,9 @@ let rec subst_glob_constr subst raw = GIf (loc,c',(na,po'),b1',b2') | GRec (loc,fix,ida,bl,ra1,ra2) -> - let ra1' = array_smartmap (subst_glob_constr subst) ra1 - and ra2' = array_smartmap (subst_glob_constr subst) ra2 in - let bl' = array_smartmap + let ra1' = Array.smartmap (subst_glob_constr subst) ra1 + and ra2' = Array.smartmap (subst_glob_constr subst) ra2 in + let bl' = Array.smartmap (List.smartmap (fun (na,k,obd,ty as dcl) -> let ty' = subst_glob_constr subst ty in let obd' = Option.smartmap (subst_glob_constr subst) obd in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 9284e2c23..f931d723f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -692,7 +692,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let second_order_matching_with_args ts env evd ev l t = (* let evd,ev = evar_absorb_arguments env evd ev l in - let argoccs = array_map_to_list (fun _ -> None) (snd ev) in + let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in second_order_matching ts env evd ev argoccs t *) (evd,false) @@ -704,12 +704,12 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let (term2,l2 as appr2) = decompose_app t2 in match kind_of_term term1, kind_of_term term2 with | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = [] - & array_for_all (fun a -> eq_constr a term2 or isEvar a) args1 -> + & Array.for_all (fun a -> eq_constr a term2 or isEvar a) args1 -> (* The typical kind of constraint coming from pattern-matching return type inference *) choose_less_dependent_instance evk1 evd term2 args1 | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] - & array_for_all (fun a -> eq_constr a term1 or isEvar a) args2 -> + & Array.for_all (fun a -> eq_constr a term1 or isEvar a) args2 -> (* The typical kind of constraint coming from pattern-matching return type inference *) choose_less_dependent_instance evk2 evd term1 args2 diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 0243a5780..700b168ae 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -381,7 +381,7 @@ let restrict_applied_evar evd (evk,argsv) filter candidates = | Some filter -> let evi = Evd.find evd evk in let subfilter = extract_subfilter (evar_filter evi) filter in - array_filter_with subfilter argsv in + Array.filter_with subfilter argsv in evd,(newevk,newargsv) (* Restrict an evar in the current evar_map *) @@ -392,7 +392,7 @@ let restrict_evar evd evk filter candidates = let restrict_instance evd evk filter argsv = match filter with None -> argsv | Some filter -> let evi = Evd.find evd evk in - array_filter_with (extract_subfilter (evar_filter evi) filter) argsv + Array.filter_with (extract_subfilter (evar_filter evi) filter) argsv (* This assumes an evar with identity instance and generalizes it over only the De Bruijn part of the context *) @@ -827,7 +827,7 @@ let make_projectable_subst aliases sigma evi args = | _ -> (rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs)) | _ -> anomaly "Instance does not match its signature") - sign (array_rev_to_list args,Idmap.empty,Constrmap.empty) in + sign (Array.rev_to_list args,Idmap.empty,Constrmap.empty) in (full_subst,cstr_subst) let make_pure_subst evi args = @@ -836,7 +836,7 @@ let make_pure_subst evi args = match args with | a::rest -> (rest, (id,a)::l) | _ -> anomaly "Instance does not match its signature") - (evar_filtered_context evi) (array_rev_to_list args,[])) + (evar_filtered_context evi) (Array.rev_to_list args,[])) (*------------------------------------* * operations on the evar constraints * @@ -927,7 +927,7 @@ let find_projectable_constructor env evd cstr k args cstr_subst = List.filter (fun (args',id) -> (* is_conv is maybe too strong (and source of useless computation) *) (* (at least expansion of aliases is needed) *) - array_for_all2 (is_conv env evd) args args') l in + Array.for_all2 (is_conv env evd) args args') l in List.map snd l with Not_found -> [] @@ -1155,7 +1155,7 @@ let filter_of_projection = function Invertible _ -> true | _ -> false let invert_invertible_arg evd aliases k (evk,argsv) args' = let evi = Evd.find_undefined evd evk in let subst,_ = make_projectable_subst aliases evd evi argsv in - let projs = array_map_to_list (invert_arg evd aliases k evk subst) args' in + let projs = Array.map_to_list (invert_arg evd aliases k evk subst) args' in Array.of_list (extract_unique_projections projs) (* Redefines an evar with a smaller context (i.e. it may depend on less @@ -1343,9 +1343,9 @@ let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t = let f,args = decompose_app_vect t in match kind_of_term f with | Construct (ind,_) -> - let params,_ = array_chop (Inductiveops.inductive_nparams ind) args in - array_for_all (is_constrainable_in k g) params - | Ind _ -> array_for_all (is_constrainable_in k g) args + let params,_ = Array.chop (Inductiveops.inductive_nparams ind) args in + Array.for_all (is_constrainable_in k g) params + | Ind _ -> Array.for_all (is_constrainable_in k g) args | Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2 | Evar (ev',_) -> ev' <> ev (*If ev' needed, one may also try to restrict it*) | Var id -> Idset.mem id fv_ids @@ -1443,7 +1443,7 @@ let check_evar_instance evd evk1 body conv_algo = * depend on these args). *) let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 = - if array_equal eq_constr argsv1 argsv2 then evd else + if Array.equal eq_constr argsv1 argsv2 then evd else (* Filter and restrict if needed *) let untypedfilter = restrict_upon_filter evd evk @@ -1549,7 +1549,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in let ts = expansions_of_var aliases t in let test c = isEvar c or List.mem c ts in - let filter = array_map_to_list test argsv' in + let filter = Array.map_to_list test argsv' in let filter = apply_subfilter (evar_filter (Evd.find_undefined evd evk)) filter in let filter = closure_of_filter evd evk' filter in @@ -1952,7 +1952,7 @@ let define_evar_as_product evd (evk,args) = (* Quick way to compute the instantiation of evk with args *) let na,dom,rng = destProd prod in let evdom = mkEvar (fst (destEvar dom), args) in - let evrngargs = array_cons (mkRel 1) (Array.map (lift 1) args) in + let evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in let evrng = mkEvar (fst (destEvar rng), evrngargs) in evd,mkProd (na, evdom, evrng) @@ -1987,7 +1987,7 @@ let define_evar_as_lambda env evd (evk,args) = let evd,lam = define_pure_evar_as_lambda env evd evk in (* Quick way to compute the instantiation of evk with args *) let na,dom,body = destLambda lam in - let evbodyargs = array_cons (mkRel 1) (Array.map (lift 1) args) in + let evbodyargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in let evbody = mkEvar (fst (destEvar body), evbodyargs) in evd,mkLambda (na, dom, evbody) @@ -1998,7 +1998,7 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function let evd,lam = define_pure_evar_as_lambda env evd evk in let _,_,body = destLambda lam in let evk = fst (destEvar body) in - evar_absorb_arguments env evd (evk, array_cons a args) l + evar_absorb_arguments env evd (evk, Array.cons a args) l (* Refining an evar to a sort *) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index d20afaf40..09225b2f6 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -125,7 +125,7 @@ let occur_glob_constr id = | GIf (loc,c,rtntyp,b1,b2) -> occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2) | GRec (loc,fk,idl,bl,tyl,bv) -> - not (array_for_all4 (fun fid bl ty bd -> + not (Array.for_all4 (fun fid bl ty bd -> let rec occur_fix = function [] -> not (occur ty) && (fid=id or not(occur bd)) | (na,k,bbd,bty)::bl -> @@ -192,7 +192,7 @@ let free_glob_vars = let vs2 = vars bounded1 vs1 tyl.(i) in vars bounded1 vs2 bv.(i) in - array_fold_left_i vars_fix vs idl + Array.fold_left_i vars_fix vs idl | GCast (loc,c,k) -> let v = vars bounded vs c in (match k with CastConv t | CastVM t -> vars bounded v t | _ -> v) | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index f11fb4613..15255ea27 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -321,7 +321,7 @@ let mis_make_indrec env sigma listdepkind mib = (fun f -> appvect (f, Termops.extended_rel_vect ndepar lnonparrec)) fi in - array_map3 + Array.map3 (make_rec_branch_arg env sigma (nparrec,depPvec,larsign)) vecfi constrs (dest_subterms recargsvec.(tyi)) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index a026f53d4..4062117b0 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -79,7 +79,7 @@ let mis_is_recursive_subset listind rarg = | Mrec (_,i) -> List.mem i listind | _ -> false) rvec in - array_exists one_is_rec (dest_subterms rarg) + Array.exists one_is_rec (dest_subterms rarg) let mis_is_recursive (ind,mib,mip) = mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1)) @@ -400,7 +400,7 @@ let set_pattern_names env ind brv = rel_context_length ((prod_assum c)) - mib.mind_nparams) mip.mind_nf_lc in - array_map2 (set_names env) arities brv + Array.map2 (set_names env) arities brv let type_case_branches_with_names env indspec p c = let (ind,args) = indspec in diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 37cbcc062..217398a6d 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -183,14 +183,14 @@ let matches_core convert allow_partial_app allow_bound_rels pat c = | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app -> let p = Array.length args2 - Array.length args1 in if p>=0 then - let args21, args22 = array_chop p args2 in + let args21, args22 = Array.chop p args2 in let c = mkApp(c2,args21) in let subst = merge_binding allow_bound_rels stk n c subst in - array_fold_left2 (sorec stk) subst args1 args22 + Array.fold_left2 (sorec stk) subst args1 args22 else raise PatternMatchingFailure | PApp (c1,arg1), App (c2,arg2) -> - (try array_fold_left2 (sorec stk) (sorec stk subst c1 c2) arg1 arg2 + (try Array.fold_left2 (sorec stk) (sorec stk subst c1 c2) arg1 arg2 with Invalid_argument _ -> raise PatternMatchingFailure) | PProd (na1,c1,d1), Prod(na2,c2,d2) -> @@ -292,7 +292,7 @@ let sub_match ?(partial_app=false) ?(closed=true) pat c = let mk_ctx = function | [app';c] -> mk_ctx (mkApp (app',[|c|])) | _ -> assert false in - try_aux [app;array_last lc] mk_ctx next + try_aux [app;Array.last lc] mk_ctx next else let rec aux2 app args next = match args with diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index e4ae1e4b8..1f16385a6 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -23,7 +23,7 @@ open Evd let rec occur_meta_pattern = function | PApp (f,args) -> - (occur_meta_pattern f) or (array_exists occur_meta_pattern args) + (occur_meta_pattern f) or (Array.exists occur_meta_pattern args) | PLambda (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) | PProd (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) | PLetIn (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) @@ -179,7 +179,7 @@ let rec subst_pattern subst pat = | PRel _ -> pat | PApp (f,args) -> let f' = subst_pattern subst f in - let args' = array_smartmap (subst_pattern subst) args in + let args' = Array.smartmap (subst_pattern subst) args in if f' == f && args' == args then pat else PApp (f',args') | PSoApp (i,args) -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0eff92b61..ed65cc9ea 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -316,12 +316,12 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in let ctxtv = Array.map (type_bl env empty_rel_context) bl in let larj = - array_map2 + Array.map2 (fun e ar -> pretype_type empty_valcon (push_rel_context e env) evdref lvar ar) ctxtv lar in let lara = Array.map (fun a -> a.utj_val) larj in - let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in + let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in let nbfix = Array.length lar in let names = Array.map (fun id -> Name id) names in let _ = @@ -336,7 +336,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function (* Note: bodies are not used by push_rec_types, so [||] is safe *) let newenv = push_rec_types (names,ftys,[||]) env in let vdefj = - array_map2_i + Array.map2_i (fun i ctxt def -> (* we lift nbfix times the type in tycon, because of * the nbfix variables pushed to newenv *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index fd9a312fc..f20c0dd83 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -315,7 +315,7 @@ let rec whd_state_gen flags ts env sigma = | App (f,cl) -> let napp = Array.length cl in if napp > 0 then - let x', l' = whrec' (array_last cl, empty_stack) in + let x', l' = whrec' (Array.last cl, empty_stack) in match kind_of_term x' with | Rel 1 when l' = empty_stack -> let lc = Array.sub cl 0 (napp-1) in @@ -371,7 +371,7 @@ let local_whd_state_gen flags sigma = | App (f,cl) -> let napp = Array.length cl in if napp > 0 then - let x', l' = whrec (array_last cl, empty_stack) in + let x', l' = whrec (Array.last cl, empty_stack) in match kind_of_term x' with | Rel 1 when l' = empty_stack -> let lc = Array.sub cl 0 (napp-1) in diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b897c01af..2a6dc35d1 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -176,8 +176,8 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = (function d -> match kind_of_term d with | Rel k -> if - array_for_all (noccurn k) tys - && array_for_all (noccurn (k+nbfix)) bds + Array.for_all (noccurn k) tys + && Array.for_all (noccurn (k+nbfix)) bds then (k, List.nth labs (k-1)) else @@ -902,7 +902,7 @@ let contextually byhead (occs,c) f env sigma t = else if byhead then (* find other occurrences of c in t; TODO: ensure left-to-right *) let (f,l) = destApp t in - mkApp (f, array_map_left (traverse envc) l) + mkApp (f, Array.map_left (traverse envc) l) else t with PatternMatchingFailure -> diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml index 8e56d59a6..451dde11f 100644 --- a/pretyping/term_dnet.ml +++ b/pretyping/term_dnet.ml @@ -127,11 +127,11 @@ struct | DApp (c1,t1), DApp (c2,t2) | DLambda (c1,t1), DLambda (c2,t2)) -> f (f acc c1 c2) t1 t2 | DCase (ci,p1,c1,bl1),DCase (_,p2,c2,bl2) -> - array_fold_left2 f (f (f acc p1 p2) c1 c2) bl1 bl2 + Array.fold_left2 f (f (f acc p1 p2) c1 c2) bl1 bl2 | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) -> - array_fold_left2 f (array_fold_left2 f acc ta1 ta2) ca1 ca2 + Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2 | DCoFix(i,ta1,ca1), DCoFix(_,ta2,ca2) -> - array_fold_left2 f (array_fold_left2 f acc ta1 ta2) ca1 ca2 + Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2 | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2 | _ -> assert false @@ -147,11 +147,11 @@ struct | DLambda (t1,c1), DLambda (t2,c2) -> DLambda (f t1 t2, f c1 c2) | DApp (t1,u1), DApp (t2,u2) -> DApp (f t1 t2,f u1 u2) | DCase (ci,p1,c1,bl1), DCase (_,p2,c2,bl2) -> - DCase (ci, f p1 p2, f c1 c2, array_map2 f bl1 bl2) + DCase (ci, f p1 p2, f c1 c2, Array.map2 f bl1 bl2) | DFix (ia,i,ta1,ca1), DFix (_,_,ta2,ca2) -> - DFix (ia,i,array_map2 f ta1 ta2,array_map2 f ca1 ca2) + DFix (ia,i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2) | DCoFix (i,ta1,ca1), DCoFix (_,ta2,ca2) -> - DCoFix (i,array_map2 f ta1 ta2,array_map2 f ca1 ca2) + DCoFix (i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2) | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2) | _ -> assert false diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 765f1e4fa..9db16baac 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -207,7 +207,7 @@ let push_rels_assum assums = let push_named_rec_types (lna,typarray,_) env = let ctxt = - array_map2_i + Array.map2_i (fun i na t -> match na with | Name id -> (id, None, lift i t) @@ -266,14 +266,14 @@ let rec strip_head_cast c = match kind_of_term c with let rec drop_extra_implicit_args c = match kind_of_term c with (* Removed trailing extra implicit arguments, what improves compatibility for constants with recently added maximal implicit arguments *) - | App (f,args) when isEvar (array_last args) -> + | App (f,args) when isEvar (Array.last args) -> drop_extra_implicit_args - (mkApp (f,fst (array_chop (Array.length args - 1) args))) + (mkApp (f,fst (Array.chop (Array.length args - 1) args))) | _ -> c (* Get the last arg of an application *) let last_arg c = match kind_of_term c with - | App (f,cl) -> array_last cl + | App (f,cl) -> Array.last cl | _ -> anomaly "last_arg" (* Get the last arg of an application *) @@ -296,10 +296,10 @@ let adjust_app_array_size f1 l1 f2 l2 = let len1 = Array.length l1 and len2 = Array.length l2 in if len1 = len2 then (f1,l1,f2,l2) else if len1 < len2 then - let extras,restl2 = array_chop (len2-len1) l2 in + let extras,restl2 = Array.chop (len2-len1) l2 in (f1, l1, appvect (f2,extras), restl2) else - let extras,restl1 = array_chop (len1-len2) l1 in + let extras,restl1 = Array.chop (len1-len2) l1 in (appvect (f1,extras), restl1, f2, l2) (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate @@ -336,7 +336,7 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with (co-)fixpoint) *) let fold_rec_types g (lna,typarray,_) e = - let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in + let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in Array.fold_left (fun e assum -> g assum e) e ctxt @@ -361,19 +361,19 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with let a = al.(Array.length al - 1) in let hd = f l (mkApp (c, Array.sub al 0 (Array.length al - 1))) in mkApp (hd, [| f l a |]) - | Evar (e,al) -> mkEvar (e, array_map_left (f l) al) + | Evar (e,al) -> mkEvar (e, Array.map_left (f l) al) | Case (ci,p,c,bl) -> (* In v8 concrete syntax, predicate is after the term to match! *) let c' = f l c in let p' = f l p in - mkCase (ci, p', c', array_map_left (f l) bl) + mkCase (ci, p', c', Array.map_left (f l) bl) | Fix (ln,(lna,tl,bl as fx)) -> let l' = fold_rec_types g fx l in - let (tl',bl') = array_map_left_pair (f l) tl (f l') bl in + let (tl',bl') = Array.map_left_pair (f l) tl (f l') bl in mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl as fx)) -> let l' = fold_rec_types g fx l in - let (tl',bl') = array_map_left_pair (f l) tl (f l') bl in + let (tl',bl') = Array.map_left_pair (f l) tl (f l') bl in mkCoFix (ln,(lna,tl',bl')) (* strong *) @@ -400,30 +400,30 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with | App (c,al) -> let c' = f l c in let al' = Array.map (f l) al in - if c==c' && array_for_all2 (==) al al' then cstr else mkApp (c', al') + if c==c' && Array.for_all2 (==) al al' then cstr else mkApp (c', al') | Evar (e,al) -> let al' = Array.map (f l) al in - if array_for_all2 (==) al al' then cstr else mkEvar (e, al') + if Array.for_all2 (==) al al' then cstr else mkEvar (e, al') | Case (ci,p,c,bl) -> let p' = f l p in let c' = f l c in let bl' = Array.map (f l) bl in - if p==p' && c==c' && array_for_all2 (==) bl bl' then cstr else + if p==p' && c==c' && Array.for_all2 (==) bl bl' then cstr else mkCase (ci, p', c', bl') | Fix (ln,(lna,tl,bl)) -> let tl' = Array.map (f l) tl in let l' = - array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in + Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in let bl' = Array.map (f l') bl in - if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl' + if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> let tl' = Array.map (f l) tl in let l' = - array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in + Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in let bl' = Array.map (f l') bl in - if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl' + if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr else mkCoFix (ln,(lna,tl',bl')) @@ -446,11 +446,11 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl | Fix (_,(lna,tl,bl)) -> let n' = iterate g (Array.length tl) n in - let fd = array_map2 (fun t b -> (t,b)) tl bl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd | CoFix (_,(lna,tl,bl)) -> let n' = iterate g (Array.length tl) n in - let fd = array_map2 (fun t b -> (t,b)) tl bl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd (* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate @@ -469,11 +469,11 @@ let iter_constr_with_full_binders g f l c = match kind_of_term c with | Evar (_,args) -> Array.iter (f l) args | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl | Fix (_,(lna,tl,bl)) -> - let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in + let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in Array.iter (f l) tl; Array.iter (f l') bl | CoFix (_,(lna,tl,bl)) -> - let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in + let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in Array.iter (f l) tl; Array.iter (f l') bl diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 7821a5f4f..8955cc64c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -71,7 +71,7 @@ let abstract_list_all env evd typ c l = error_cannot_find_well_typed_abstraction env evd p l let set_occurrences_of_last_arg args = - Some AllOccurrences :: List.tl (array_map_to_list (fun _ -> None) args) + Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args) let abstract_list_all_with_dependencies env evd typ c l = let evd,ev = new_evar evd env typ in @@ -324,7 +324,7 @@ let use_metas_pattern_unification flags nb l = !global_evars_pattern_unification_flag && flags.use_pattern_unification || (Flags.version_less_or_equal Flags.V8_3 || flags.use_meta_bound_pattern_unification) && - array_for_all (fun c -> isRel c && destRel c <= nb) l + Array.for_all (fun c -> isRel c && destRel c <= nb) l let expand_key env = function | Some (ConstKey cst) -> constant_opt_value env cst @@ -461,7 +461,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> (try - array_fold_left2 (unirec_rec curenvnb CONV true wt) + Array.fold_left2 (unirec_rec curenvnb CONV true wt) (unirec_rec curenvnb CONV true false (unirec_rec curenvnb CONV true false substn p1 p2) c1 c2) cl1 cl2 @@ -503,7 +503,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag and unify_app curenvnb pb b substn cM f1 l1 cN f2 l2 = try let (f1,l1,f2,l2) = adjust_app_array_size f1 l1 f2 l2 in - array_fold_left2 (unirec_rec curenvnb CONV true false) + Array.fold_left2 (unirec_rec curenvnb CONV true false) (unirec_rec curenvnb CONV true true substn f1 f2) l1 l2 with ex when precatchable_exception ex -> try reduce curenvnb pb b false substn cM cN diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 00efa981d..321364140 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -182,7 +182,7 @@ and nf_stk env c t stk = let (mind,_ as ind),allargs = find_rectype_a env t in let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in - let params,realargs = Util.array_chop nparams allargs in + let params,realargs = Util.Array.chop nparams allargs in let pT = hnf_prod_applist env (type_of_ind env ind) (Array.to_list params) in let pT = whd_betadeltaiota env pT in @@ -264,7 +264,7 @@ and nf_fix env f = let ft = Array.map (fun v -> nf_val env v crazy_type) vt in let name = Array.init ndef (fun _ -> (Name (id_of_string "Ffix"))) in let env = push_rec_types (name,ft,ft) env in - let fb = Util.array_map2 (fun v t -> nf_fun env v t) vb ft in + let fb = Util.Array.map2 (fun v t -> nf_fun env v t) vb ft in mkFix ((rec_args,init),(name,ft,fb)) and nf_fix_app env f vargs = @@ -282,7 +282,7 @@ and nf_cofix env cf = let cft = Array.map (fun v -> nf_val env v crazy_type) vt in let name = Array.init ndef (fun _ -> (Name (id_of_string "Fcofix"))) in let env = push_rec_types (name,cft,cft) env in - let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in + let cfb = Util.Array.map2 (fun v t -> nf_val env v t) vb cft in mkCoFix (init,(name,cft,cfb)) let cbv_vm env c t = diff --git a/printing/printer.ml b/printing/printer.ml index 1ad9dba49..374b5d597 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -640,7 +640,7 @@ let print_constructors envpar names types = let pc = prlist_with_sep (fun () -> brk(1,0) ++ str "| ") (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar c) - (Array.to_list (array_map2 (fun n t -> (n,t)) names types)) + (Array.to_list (Array.map2 (fun n t -> (n,t)) names types)) in hv 0 (str " " ++ pc) diff --git a/proofs/logic.ml b/proofs/logic.ml index 53f5705a5..5be9df317 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -367,7 +367,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in check_conv_leq_goal env sigma trm conclty' conclty; let (acc'',sigma, rbranches) = - array_fold_left2 + Array.fold_left2 (fun (lacc,sigma,bacc) ty fi -> let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc)) (acc',sigma,[]) lbrty lf @@ -403,7 +403,7 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = if isInd f or isConst f - & not (array_exists occur_meta l) (* we could be finer *) + & not (Array.exists occur_meta l) (* we could be finer *) then (goalacc,type_of_global_reference_knowing_parameters env sigma f l,sigma,f) else mk_hdgoals sigma goal goalacc f @@ -415,7 +415,7 @@ and mk_hdgoals sigma goal goalacc trm = | Case (ci,p,c,lf) -> let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in let (acc'',sigma,rbranches) = - array_fold_left2 + Array.fold_left2 (fun (lacc,sigma,bacc) ty fi -> let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc)) (acc',sigma,[]) lbrty lf diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index fd5fbe25a..02d99d707 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -489,7 +489,7 @@ let unfold_head env (ids, csts) c = | true, f' -> true, Reductionops.whd_betaiota Evd.empty (mkApp (f', args)) | false, _ -> let done_, args' = - array_fold_left_i (fun i (done_, acc) arg -> + Array.fold_left_i (fun i (done_, acc) arg -> if done_ then done_, arg :: acc else match aux arg with | true, arg' -> true, arg' :: acc diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index bf29d393e..7f0e486ab 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -754,9 +754,9 @@ let rec has_evar x = | Fix ((_, tr)) | CoFix ((_, tr)) -> has_evar_prec tr and has_evar_array x = - array_exists has_evar x + Array.exists has_evar x and has_evar_prec (_, ts1, ts2) = - array_exists has_evar ts1 || array_exists has_evar ts2 + Array.exists has_evar ts1 || Array.exists has_evar ts2 TACTIC EXTEND has_evar | [ "has_evar" constr(x) ] -> diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index bb35cedea..237c63a83 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -144,7 +144,7 @@ let is_tuple t = "Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *) let test_strict_disjunction n lc = - array_for_all_i (fun i c -> + Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && destRel c = (n - i) | _ -> false) 0 lc @@ -155,7 +155,7 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) t = | Ind ind -> let car = mis_constr_nargs ind in let (mib,mip) = Global.lookup_inductive ind in - if array_for_all (fun ar -> ar = 1) car + if Array.for_all (fun ar -> ar = 1) car && not (mis_is_recursive (ind,mib,mip)) && (mip.mind_nrealargs = 0) then @@ -316,7 +316,7 @@ let match_with_nodep_ind t = let (mib,mip) = Global.lookup_inductive ind in if Array.length (mib.mind_packets)>1 then None else let nodep_constr = has_nodep_prod_after mib.mind_nparams in - if array_for_all nodep_constr mip.mind_nf_lc then + if Array.for_all nodep_constr mip.mind_nf_lc then let params= if mip.mind_nrealargs=0 then args else fst (List.chop mib.mind_nparams args) in diff --git a/tactics/refine.ml b/tactics/refine.ml index 1cb4f01e2..de073b5c9 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -115,7 +115,7 @@ let replace_by_meta env sigma = function exception NoMeta let replace_in_array keep_length env sigma a = - if array_for_all (function (TH (_,_,[])) -> true | _ -> false) a then + if Array.for_all (function (TH (_,_,[])) -> true | _ -> false) a then raise NoMeta; let a' = Array.map (function | (TH (c,mm,[])) when not keep_length -> c,mm,[] @@ -347,7 +347,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = | Name id -> id | _ -> error "Recursive functions must have names." in - let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in + let fixes = Array.map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in let firsts,lasts = List.chop j (Array.to_list fixes) in tclTHENS (tclTHEN @@ -364,7 +364,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = | Name id -> id | _ -> error "Recursive functions must have names." in - let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in + let cofixes = Array.map2 (fun f c -> (out_name f,c)) fi ai in let firsts,lasts = List.chop j (Array.to_list cofixes) in tclTHENS (mutual_cofix (out_name fi.(j)) (firsts@List.tl lasts) j) diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index c36ab2f83..fe869c340 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -121,7 +121,7 @@ let is_applied_rewrite_relation env sigma rels t = if eq_constr (Lazy.force coq_eq) head then None else (try - let params, args = array_chop (Array.length args - 2) args in + let params, args = Array.chop (Array.length args - 2) args in let env' = Environ.push_rel_context rels env in let evd, evar = Evarutil.new_evar sigma env' (new_Type ()) in let inst = mkApp (Lazy.force rewrite_relation_class, [| evar; mkApp (c, params) |]) in @@ -209,12 +209,6 @@ let get_transitive_proof env = find_class_proof transitive_type transitive_proof exception FoundInt of int -let array_find (arr: 'a array) (pred: int -> 'a -> bool): int = - try - for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (FoundInt i) done; - raise Not_found - with FoundInt i -> i - type hypinfo = { cl : clausenv; prf : constr; @@ -239,7 +233,7 @@ let rec decompose_app_rel env evd t = match kind_of_term t with | App (f, args) -> if Array.length args > 1 then - let fargs, args = array_chop (Array.length args - 2) args in + let fargs, args = Array.chop (Array.length args - 2) args in mkApp (f, fargs), args else let (f', args) = decompose_app_rel env evd args.(0) in @@ -587,10 +581,11 @@ let resolve_subrelation env avoid car rel prf rel' res = let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' cstr evars = let evars, morph_instance, proj, sigargs, m', args, args' = - let first = try (array_find args' (fun i b -> b <> None)) - with Not_found -> raise (Invalid_argument "resolve_morphism") in - let morphargs, morphobjs = array_chop first args in - let morphargs', morphobjs' = array_chop first args' in + let first = match (Array.find_i (fun _ b -> b <> None) args') with + | Some i -> i + | None -> raise (Invalid_argument "resolve_morphism") in + let morphargs, morphobjs = Array.chop first args in + let morphargs', morphobjs' = Array.chop first args' in let appm = mkApp(m, morphargs) in let appmtype = Typing.type_of env (goalevars evars) appm in let cstrs = List.map (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) (Array.to_list morphobjs') in @@ -609,7 +604,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' cstr evars evars, morph, morph, sigargs, appm, morphobjs, morphobjs' in let projargs, subst, evars, respars, typeargs = - array_fold_left2 + Array.fold_left2 (fun (acc, subst, evars, sigargs, typeargs') x y -> let (carrier, relation), sigargs = split_head sigargs in match relation with @@ -767,7 +762,7 @@ let subterm all flags (s : strategy) : strategy = | Some false -> Some None | Some true -> let args' = Array.of_list (List.rev args') in - if array_exists + if Array.exists (function | None -> false | Some r -> not (is_rew_cast r.rew_prf)) args' @@ -778,7 +773,7 @@ let subterm all flags (s : strategy) : strategy = rew_evars = evars' } in Some (Some res) else - let args' = array_map2 + let args' = Array.map2 (fun aorig anew -> match anew with None -> aorig | Some r -> r.rew_to) args args' @@ -887,7 +882,7 @@ let subterm all flags (s : strategy) : strategy = let res = make_leibniz_proof (mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs)) ty r in Some (Some (coerce env avoid cstr res)) | x -> - if array_for_all ((=) 0) ci.ci_cstr_ndecls then + if Array.for_all ((=) 0) ci.ci_cstr_ndecls then let cstr = Some (mkApp (Lazy.force coq_eq, [| ty |])) in let found, brs' = Array.fold_left (fun (found, acc) br -> @@ -1765,7 +1760,7 @@ let declare_projection n instance_id r = let init = match kind_of_term typ with App (f, args) when eq_constr f (Lazy.force respectful) -> - mkApp (f, fst (array_chop (Array.length args - 2) args)) + mkApp (f, fst (Array.chop (Array.length args - 2) args)) | _ -> typ in aux init in diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index f88530eec..637269a66 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -211,7 +211,7 @@ let compute_construtor_signatures isrec (_,k as ity) = let lc = Array.map (fun c -> snd (decompose_prod_n_assum n c)) mip.mind_nf_lc in let lrecargs = dest_subterms mip.mind_recargs in - array_map2 analrec lc lrecargs + Array.map2 analrec lc lrecargs let elimination_sort_of_goal gl = pf_apply Retyping.get_sort_family_of gl (pf_concl gl) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b1a9c6732..8e6fc8597 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -718,7 +718,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id c let last_arg c = match kind_of_term c with | App (f,cl) -> - array_last cl + Array.last cl | _ -> anomaly "last_arg" let nth_arg i c = @@ -1305,7 +1305,7 @@ let intro_or_and_pattern loc b ll l' tac id gl = check_or_and_pattern_size loc ll (Array.length nv); tclTHENLASTn (tclTHEN (simplest_case c) (clear [id])) - (array_map2 (fun n l -> tac ((adjust_names_length n n l)@l')) + (Array.map2 (fun n l -> tac ((adjust_names_length n n l)@l')) nv (Array.of_list ll)) gl @@ -2315,7 +2315,7 @@ let ids_of_constr ?(all=false) vars c = | Construct (ind,_) | Ind ind -> let (mib,mip) = Global.lookup_inductive ind in - array_fold_left_from + Array.fold_left_from (if all then 0 else mib.Declarations.mind_nparams) aux vars args | _ -> fold_constr aux vars c) @@ -2328,7 +2328,7 @@ let decompose_indapp f args = | Ind ind -> let (mib,mip) = Global.lookup_inductive ind in let first = mib.Declarations.mind_nparams_rec in - let pars, args = array_chop first args in + let pars, args = Array.chop first args in mkApp (f, pars), args | _ -> f, args @@ -2459,10 +2459,10 @@ let abstract_args gl generalize_vars dep id defined f args = let parvars = ids_of_constr ~all:true Idset.empty f' in if not (linear parvars args') then true, f, args else - match array_find_i (fun i x -> not (isVar x) || is_defined_variable env (destVar x)) args' with + match Array.find_i (fun i x -> not (isVar x) || is_defined_variable env (destVar x)) args' with | None -> false, f', args' | Some nonvar -> - let before, after = array_chop nonvar args' in + let before, after = Array.chop nonvar args' in true, mkApp (f', before), after in if dogen then @@ -2941,7 +2941,7 @@ let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names t (tclTHEN (induct_tac elim) (tclMAP (fun id -> tclTRY (expand_hyp id)) (List.rev indhyps))) - (array_map2 (induct_discharge destopt avoid tac) indsign names) gl + (Array.map2 (induct_discharge destopt avoid tac) indsign names) gl (* Apply induction "in place" taking into account dependent hypotheses from the context *) diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 92b0d6536..dcac6eb79 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -77,7 +77,7 @@ let refresh_polymorphic_type_of_inductive (_,mip) = let process_inductive sechyps modlist mib = let nparams = mib.mind_nparams in let inds = - array_map_to_list + Array.map_to_list (fun mip -> let arity = expmod_constr modlist (refresh_polymorphic_type_of_inductive (mib,mip)) in let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index f6b8ada42..bfd64778f 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -157,7 +157,7 @@ let define_mutual_scheme_base kind suff f internal names mind = let ids = Array.init (Array.length mib.mind_packets) (fun i -> try 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 consts = Array.map2 (define internal) ids cl in declare_scheme kind (Array.mapi (fun i cst -> ((mind,i),cst)) consts); consts diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index a6677a78b..e3c5142d9 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -985,22 +985,18 @@ let admit_obligations n = exception Found of int -let array_find f arr = - try Array.iteri (fun i x -> if f x then raise (Found i)) arr; - raise Not_found - with Found i -> i - let next_obligation n tac = let prg = match n with | None -> get_any_prog_err () | Some _ -> get_prog_err n in let obls, rem = prg.prg_obligations in - let i = - try array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls - with Not_found -> anomaly "Could not find a solvable obligation." - in solve_obligation prg i tac - + let is_open _ x = x.obl_body = None && deps_remaining obls x.obl_deps = [] in + let i = match Array.find_i is_open obls with + | Some i -> i + | None -> anomaly "Could not find a solvable obligation." + in + solve_obligation prg i tac let init_program () = Coqlib.check_required_library ["Coq";"Init";"Datatypes"]; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index dc451fe05..c0b9b1110 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -171,7 +171,7 @@ let make_cases s = let {Declarations.mind_nparams = np} , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr } = Global.lookup_inductive i in - Util.array_fold_right2 + Util.Array.fold_right2 (fun consname typ l -> let al = List.rev (fst (Term.decompose_prod typ)) in let al = Util.List.skipn np al in |