From 8cc623262c625bda20e97c75f9ba083ae8e7760d Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Sep 2012 19:13:19 +0000 Subject: 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 --- checker/check.mllib | 1 + checker/closure.ml | 2 +- checker/declarations.ml | 20 ++++++++++---------- checker/environ.ml | 2 +- checker/indtypes.ml | 12 ++++++------ checker/inductive.ml | 4 ++-- checker/reduction.ml | 6 +++--- checker/subtyping.ml | 10 +++++----- checker/term.ml | 10 +++++----- checker/typeops.ml | 8 ++++---- 10 files changed, 38 insertions(+), 37 deletions(-) (limited to 'checker') 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 -- cgit v1.2.3