Permalink
Browse files

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
  • Loading branch information...
1 parent 6eaff63 commit 8cc623262c625bda20e97c75f9ba083ae8e7760d ppedrot committed Sep 14, 2012
Showing with 804 additions and 666 deletions.
  1. +1 −0 checker/check.mllib
  2. +1 −1 checker/closure.ml
  3. +10 −10 checker/declarations.ml
  4. +1 −1 checker/environ.ml
  5. +6 −6 checker/indtypes.ml
  6. +2 −2 checker/inductive.ml
  7. +3 −3 checker/reduction.ml
  8. +5 −5 checker/subtyping.ml
  9. +5 −5 checker/term.ml
  10. +4 −4 checker/typeops.ml
  11. +1 −0 dev/printers.mllib
  12. +1 −0 grammar/grammar.mllib
  13. +2 −2 interp/constrextern.ml
  14. +2 −2 interp/constrintern.ml
  15. +1 −1 interp/implicit_quantifiers.ml
  16. +11 −11 interp/notation_ops.ml
  17. +1 −1 kernel/closure.ml
  18. +7 −7 kernel/declarations.ml
  19. +1 −1 kernel/environ.ml
  20. +5 −5 kernel/indtypes.ml
  21. +3 −3 kernel/inductive.ml
  22. +7 −7 kernel/mod_subst.ml
  23. +3 −3 kernel/reduction.ml
  24. +5 −5 kernel/subtyping.ml
  25. +12 −12 kernel/term.ml
  26. +2 −2 kernel/typeops.ml
  27. +420 −0 lib/cArray.ml
  28. +98 −0 lib/cArray.mli
  29. +1 −0 lib/clib.mllib
  30. +4 −4 lib/rtree.ml
  31. +3 −320 lib/util.ml
  32. +1 −51 lib/util.mli
  33. +4 −4 library/impargs.ml
  34. +3 −3 plugins/cc/ccalgo.ml
  35. +1 −1 plugins/cc/cctac.ml
  36. +3 −3 plugins/extraction/extract_env.ml
  37. +7 −7 plugins/extraction/extraction.ml
  38. +1 −1 plugins/extraction/haskell.ml
  39. +3 −3 plugins/extraction/mlutil.ml
  40. +1 −1 plugins/extraction/modutil.ml
  41. +1 −1 plugins/extraction/ocaml.ml
  42. +1 −1 plugins/extraction/scheme.ml
  43. +2 −2 plugins/firstorder/formula.ml
  44. +4 −4 plugins/funind/functional_principles_proofs.ml
  45. +2 −2 plugins/funind/functional_principles_types.ml
  46. +2 −2 plugins/funind/glob_term_to_relation.ml
  47. +6 −6 plugins/funind/invfun.ml
  48. +5 −13 plugins/funind/merge.ml
  49. +3 −3 plugins/quote/quote.ml
  50. +1 −1 plugins/setoid_ring/newring.ml4
  51. +3 −3 pretyping/cases.ml
  52. +9 −9 pretyping/detyping.ml
  53. +3 −3 pretyping/evarconv.ml
  54. +14 −14 pretyping/evarutil.ml
  55. +2 −2 pretyping/glob_ops.ml
  56. +1 −1 pretyping/indrec.ml
  57. +2 −2 pretyping/inductiveops.ml
  58. +4 −4 pretyping/matching.ml
  59. +2 −2 pretyping/patternops.ml
  60. +3 −3 pretyping/pretyping.ml
  61. +2 −2 pretyping/reductionops.ml
  62. +3 −3 pretyping/tacred.ml
  63. +6 −6 pretyping/term_dnet.ml
  64. +22 −22 pretyping/termops.ml
  65. +4 −4 pretyping/unification.ml
  66. +3 −3 pretyping/vnorm.ml
  67. +1 −1 printing/printer.ml
  68. +3 −3 proofs/logic.ml
  69. +1 −1 tactics/eauto.ml4
  70. +2 −2 tactics/extratactics.ml4
  71. +3 −3 tactics/hipattern.ml4
  72. +3 −3 tactics/refine.ml
  73. +12 −17 tactics/rewrite.ml4
  74. +1 −1 tactics/tacticals.ml
  75. +7 −7 tactics/tactics.ml
  76. +1 −1 toplevel/discharge.ml
  77. +1 −1 toplevel/ind_tables.ml
  78. +6 −10 toplevel/obligations.ml
  79. +1 −1 toplevel/vernacentries.ml
View
@@ -8,6 +8,7 @@ Segmenttree
Unicodetable
Errors
CList
+CArray
Util
Option
Hashcons
View
@@ -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)
View
@@ -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 *)
View
@@ -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 *)
View
@@ -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
(************************************************************************)
(************************************************************************)
View
@@ -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)
View
@@ -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
View
@@ -42,15 +42,15 @@ 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
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 =
View
@@ -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 =
View
@@ -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
View
@@ -9,6 +9,7 @@ Segmenttree
Unicodetable
Errors
CList
+CArray
Util
Bigint
Hashcons
View
@@ -9,6 +9,7 @@ Segmenttree
Unicodetable
Errors
CList
+CArray
Util
Bigint
Hashcons
View
@@ -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)
View
@@ -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
@@ -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
Oops, something went wrong.

0 comments on commit 8cc6232

Please sign in to comment.