aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.mllib1
-rw-r--r--checker/closure.ml2
-rw-r--r--checker/declarations.ml20
-rw-r--r--checker/environ.ml2
-rw-r--r--checker/indtypes.ml12
-rw-r--r--checker/inductive.ml4
-rw-r--r--checker/reduction.ml6
-rw-r--r--checker/subtyping.ml10
-rw-r--r--checker/term.ml10
-rw-r--r--checker/typeops.ml8
10 files changed, 38 insertions, 37 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 06:28:11 +0000