aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/cArray.ml47
-rw-r--r--lib/cArray.mli50
-rw-r--r--lib/cList.ml1
-rw-r--r--lib/cList.mli4
-rw-r--r--plugins/funind/merge.ml4
-rw-r--r--pretyping/termops.ml15
-rw-r--r--tactics/rewrite.ml42
-rw-r--r--tactics/tactics.ml2
-rw-r--r--toplevel/obligations.ml2
9 files changed, 66 insertions, 61 deletions
diff --git a/lib/cArray.ml b/lib/cArray.ml
index 7f25bb10c7..bdc084f44b 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -50,7 +50,7 @@ sig
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 findi : (int -> 'a -> bool) -> 'a array -> int option
val hd : 'a array -> 'a
val tl : 'a array -> 'a array
val last : 'a array -> 'a
@@ -68,9 +68,6 @@ sig
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
@@ -79,17 +76,13 @@ sig
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
@@ -161,7 +154,7 @@ let for_all_i f i v =
exception Found of int
-let find_i (pred: int -> 'a -> bool) (arr: 'a array) : int option =
+let findi (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
@@ -249,20 +242,6 @@ let fold_left_from n f a v =
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)
@@ -347,18 +326,6 @@ let map_left f a = (* Ocaml does not guarantee Array.map is LR *)
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"
@@ -390,6 +357,7 @@ let fold_map2' f v1 v2 e =
in
(v',!e')
+
let distinct v =
let visited = Hashtbl.create 23 in
try
@@ -401,20 +369,11 @@ let distinct 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
index bf5648881c..1738bb6184 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -43,8 +43,14 @@ module type ExtS =
sig
include S
val compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int
+ (** First size comparison, then lexicographic order. *)
+
val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
+ (** Lift equality to array type. *)
+
val exists : ('a -> bool) -> 'a array -> bool
+ (** As [List.exists] but on arrays. *)
+
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) ->
@@ -52,12 +58,24 @@ sig
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 findi : (int -> 'a -> bool) -> 'a array -> int option
+
val hd : 'a array -> 'a
+ (** First element of an array, or [Failure "Array.hd"] if empty. *)
+
val tl : 'a array -> 'a array
+ (** Remaining part of [hd], or [Failure "Array.tl"] if empty. *)
+
val last : 'a array -> 'a
+ (** Last element of an array, or [Failure "Array.last"] if empty. *)
+
val cons : 'a -> 'a array -> 'a array
+ (** Append an element on the left. *)
+
val rev : 'a array -> unit
+ (** In place reversal. *)
+
val fold_right_i :
(int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a
val fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a
@@ -70,29 +88,45 @@ sig
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
+ (** Composition of [map] and [to_list]. *)
+
val chop : int -> 'a array -> 'a array * 'a array
+ (** [chop i a] returns [(a1, a2)] s.t. [a = a1 + a2] and [length a1 = n].
+ Raise [Failure "Array.chop"] if [i] is not a valid index. *)
+
val smartmap : ('a -> 'a) -> 'a array -> 'a array
+ (** [smartmap f a] behaves as [map f a] but returns [a] instead of a copy when
+ [f x == x] for all [x] in [a]. *)
+
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
+ (** As [map] but guaranteed to be left-to-right. *)
+
val iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit
+ (** Iter on two arrays. Raise [Invalid_argument "Array.iter2" if sizes differ. *)
+
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
+ (** Return [true] if every element of the array is unique (for default
+ equality). *)
+
val rev_to_list : 'a array -> 'a list
- val filter_along : ('a -> bool) -> 'a list -> 'b array -> 'b array
+ (** [rev_to_list a] is equivalent to [List.rev (List.of_array a)]. *)
+
val filter_with : bool list -> 'a array -> 'a array
+ (** [filter_with b a] selects elements of [a] whose corresponding element in
+ [b] is [true]. Raise [Invalid_argument _] when sizes differ. *)
+
end
include ExtS
diff --git a/lib/cList.ml b/lib/cList.ml
index 3a4a2f5669..2bf8d3597b 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -75,7 +75,6 @@ sig
val map_filter : ('a -> 'b option) -> 'a list -> 'b list
val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
val filter_with : bool list -> 'a list -> 'a list
- val filter_along : ('a -> bool) -> 'a list -> 'b list -> 'b list
(** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i
[ f ai == ai], then [smartmap f l==l] *)
diff --git a/lib/cList.mli b/lib/cList.mli
index 20b63dcd61..fbc87f301e 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -100,8 +100,10 @@ sig
val filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
val map_filter : ('a -> 'b option) -> 'a list -> 'b list
val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
+
val filter_with : bool list -> 'a list -> 'a list
- val filter_along : ('a -> bool) -> 'a list -> 'b list -> 'b list
+ (** [filter_with b a] selects elements of [a] whose corresponding element in
+ [b] is [true]. Raise [Invalid_argument _] when sizes differ. *)
val smartmap : ('a -> 'a) -> 'a list -> 'a list
(** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 5915d3c0d4..5410e724a2 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -153,7 +153,7 @@ exception Found of int
(* Array scanning *)
let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int =
-match Array.find_i pred arr with
+match Array.findi pred arr with
| None -> Array.length arr (* all elt are positive *)
| Some i -> i
@@ -931,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.findi (fun i x -> x=c) args1 with
| Some j -> Linked j
| None -> Unlinked)
args2 in
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f8cd3609ad..2585d44898 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -340,6 +340,17 @@ 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
Array.fold_left (fun e assum -> g assum e) e ctxt
+let map_left2 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 map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
@@ -370,11 +381,11 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
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') = map_left2 (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') = map_left2 (f l) tl (f l') bl in
mkCoFix (ln,(lna,tl',bl'))
(* strong *)
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index fe869c340f..db2abea350 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -581,7 +581,7 @@ 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 = match (Array.find_i (fun _ b -> b <> None) args') with
+ let first = match (Array.findi (fun _ b -> b <> None) args') with
| Some i -> i
| None -> raise (Invalid_argument "resolve_morphism") in
let morphargs, morphobjs = Array.chop first args in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bdf2ea96d3..a29ab24bac 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2461,7 +2461,7 @@ 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.findi (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
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index e3c5142d9e..b4e6eb543d 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -992,7 +992,7 @@ let next_obligation n tac =
in
let obls, rem = prg.prg_obligations in
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
+ let i = match Array.findi is_open obls with
| Some i -> i
| None -> anomaly "Could not find a solvable obligation."
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 16:31:48 +0000