aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/ccalgo.ml6
-rw-r--r--plugins/cc/cctac.ml2
-rw-r--r--plugins/extraction/extract_env.ml6
-rw-r--r--plugins/extraction/extraction.ml14
-rw-r--r--plugins/extraction/haskell.ml2
-rw-r--r--plugins/extraction/mlutil.ml6
-rw-r--r--plugins/extraction/modutil.ml2
-rw-r--r--plugins/extraction/ocaml.ml2
-rw-r--r--plugins/extraction/scheme.ml2
-rw-r--r--plugins/firstorder/formula.ml4
-rw-r--r--plugins/funind/functional_principles_proofs.ml8
-rw-r--r--plugins/funind/functional_principles_types.ml4
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/funind/invfun.ml12
-rw-r--r--plugins/funind/merge.ml18
-rw-r--r--plugins/quote/quote.ml6
-rw-r--r--plugins/setoid_ring/newring.ml42
17 files changed, 46 insertions, 54 deletions
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 ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 15:45:56 +0000