Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
module type S = module type of Array
include Array
let uget = Array.unsafe_get
(* Arrays *)
let compare cmp v1 v2 = if v1 == v2 then 0 else let len = Array.length v1 in let c = Int.compare len (Array.length v2) in if c <> 0 then c else let rec loop i = if i < 0 then 0 else let x = uget v1 i in let y = uget v2 i in let c = cmp x y in if c <> 0 then c else loop (i - 1) in loop (len - 1)
let equal_norefl cmp t1 t2 = let len = Array.length t1 in if not (Int.equal len (Array.length t2)) then false else let rec aux i = if i < 0 then true else let x = uget t1 i in let y = uget t2 i in cmp x y && aux (pred i) in aux (len - 1)
let equal cmp t1 t2 = if t1 == t2 then true else equal_norefl cmp t1 t2
let is_empty array = Int.equal (Array.length array) 0
let exists2 f v1 v2 = let rec exrec = function | -1 -> false | n -> f (uget v1 n) (uget v2 n) || (exrec (n-1)) in let lv1 = Array.length v1 in lv1 = Array.length v2 && exrec (lv1-1)
let for_all2 f v1 v2 = let rec allrec = function | -1 -> true | n -> let ans = f (uget v1 n) (uget v2 n) in ans && (allrec (n-1)) in let lv1 = Array.length v1 in lv1 = Array.length v2 && allrec (pred lv1)
let for_all3 f v1 v2 v3 = let rec allrec = function | -1 -> true | n -> let ans = f (uget v1 n) (uget v2 n) (uget v3 n) in ans && (allrec (n-1)) in let lv1 = Array.length v1 in lv1 = Array.length v2 && lv1 = Array.length v3 && allrec (pred lv1)
let for_all4 f v1 v2 v3 v4 = let rec allrec = function | -1 -> true | n -> let ans = f (uget v1 n) (uget v2 n) (uget v3 n) (uget v4 n) in ans && (allrec (n-1)) in let lv1 = Array.length v1 in lv1 = Array.length v2 && lv1 = Array.length v3 && lv1 = Array.length v4 && allrec (pred lv1)
let for_all_i f i v = let len = Array.length v in let rec allrec i n = n = len || f i (uget v n) && allrec (i+1) (n+1) in allrec i 0
exception Found of int
let findi (pred: int -> 'a -> bool) (arr: 'a array) : int option = try for i=0 to Array.length arr - 1 do if pred i (uget arr i) then raise (Found i) done; None with Found i -> Some i
let find2_map (type a) pred arr1 arr2 = let exception Found of a in let n = Array.length arr1 in if not (Array.length arr2 = n) then failwith "Array.find2_map"; try for i=0 to n - 1 do match pred (Array.unsafe_get arr1 i) (Array.unsafe_get arr2 i) with | Some r -> raise (Found r) | None -> () done; None with Found i -> Some i
let hd v = match Array.length v with | 0 -> failwith "Array.hd" | _ -> uget v 0
let tl v = match Array.length v with | 0 -> failwith "Array.tl" | n -> Array.sub v 1 (pred n)
let last v = match Array.length v with | 0 -> failwith "Array.last" | n -> uget v (pred n)
let cons e v = let len = Array.length v in let ans = Array.make (Array.length v + 1) e in let () = Array.blit v 0 ans 1 len in ans
let rev t = let n=Array.length t in if n <=0 then () else for i = 0 to pred (n/2) do let tmp = uget t ((pred n)-i) in Array.unsafe_set t ((pred n)-i) (uget t i); Array.unsafe_set t i tmp done
let fold_right_i f v a = let rec fold a n = if n=0 then a else let k = n-1 in fold (f k (uget v k) a) k in fold a (Array.length v)
let fold_left_i f v a = let n = Array.length a in let rec fold i v = if i = n then v else fold (succ i) (f i v (uget a i)) in fold 0 v
let fold_right2 f v1 v2 a = let lv1 = Array.length v1 in let rec fold a n = if n=0 then a else let k = n-1 in fold (f (uget v1 k) (uget v2 k) a) k in if Array.length v2 <> lv1 then invalid_arg "Array.fold_right2"; fold a lv1
let fold_left2 f a v1 v2 = let lv1 = Array.length v1 in let rec fold a n = if n >= lv1 then a else fold (f a (uget v1 n) (uget v2 n)) (succ n) in if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2"; fold a 0
let fold_left2_i f a v1 v2 = let lv1 = Array.length v1 in let rec fold a n = if n >= lv1 then a else fold (f n a (uget v1 n) (uget v2 n)) (succ n) in if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2_i"; fold a 0
let fold_right3 f v1 v2 v3 a = let lv1 = Array.length v1 in let rec fold a n = if n=0 then a else let k = n-1 in fold (f (uget v1 k) (uget v2 k) (uget v3 k) a) k in if Array.length v2 <> lv1 || Array.length v3 <> lv1 then invalid_arg "Array.fold_right3"; fold a lv1
let fold_left3 f a v1 v2 v3 = let lv1 = Array.length v1 in let rec fold a n = if n >= lv1 then a else fold (f a (uget v1 n) (uget v2 n) (uget v3 n)) (succ n) in if Array.length v2 <> lv1 || Array.length v3 <> lv1 then invalid_arg "Array.fold_left3"; fold a 0
let fold_left3_i f a v1 v2 v3 = let lv1 = Array.length v1 in let rec fold a n = if n >= lv1 then a else fold (f n a (uget v1 n) (uget v2 n) (uget v3 n)) (succ n) in if Array.length v2 <> lv1 || Array.length v3 <> lv1 then invalid_arg "Array.fold_left3_i"; fold a 0
let fold_left4 f a v1 v2 v3 v4 = let lv1 = Array.length v1 in let rec fold a n = if n >= lv1 then a else fold (f a (uget v1 n) (uget v2 n) (uget v3 n) (uget v4 n)) (succ n) in if Array.length v2 <> lv1 || Array.length v3 <> lv1 || Array.length v4 <> lv1 then invalid_arg "Array.fold_left4"; fold a 0
let fold_left_from n f a v = let len = Array.length v in let () = if n < 0 then invalid_arg "Array.fold_left_from" in let rec fold a n = if n >= len then a else fold (f a (uget v n)) (succ n) in fold a n
let rev_of_list = function| [] -> [| |]| x :: l -> let len = List.length l in let ans = Array.make (succ len) x in let rec set i = function | [] -> () | x :: l -> Array.unsafe_set ans i x; set (pred i) l in let () = set (len - 1) l in ans
let map_to_list = CList.map_of_array
let map_of_list f l = let len = List.length l in let rec fill i v = function | [] -> () | x :: l -> Array.unsafe_set v i (f x); fill (succ i) v l in match l with | [] -> [||] | x :: l -> let ans = Array.make len (f x) in let () = fill 1 ans l in ans
let chop n v = let vlen = Array.length v in if n > vlen then failwith "Array.chop"; (Array.sub v 0 n, Array.sub v n (vlen-n))
let split v = (Array.map fst v, Array.map snd v)
let split3 v = (Array.map (fun (a, _, _) -> a) v, Array.map (fun (_, b, _) -> b) v, Array.map (fun (_, _, c) -> c) v)
let split4 v = (Array.map (fun (a, _, _, _) -> a) v, Array.map (fun (_, b, _, _) -> b) v, Array.map (fun (_, _, c, _) -> c) v, Array.map (fun (_, _, _, d) -> d) v)
let transpose a = let n = Array.length a in if n = 0 then [||] else let n' = Array.length (Array.unsafe_get a 0) in Array.init n' (fun i -> Array.init n (fun j -> a.(j).(i)))
let map2_i f v1 v2 = let len1 = Array.length v1 in let len2 = Array.length v2 in let () = if not (Int.equal len1 len2) then invalid_arg "Array.map2" in if Int.equal len1 0 then [| |] else begin let res = Array.make len1 (f 0 (uget v1 0) (uget v2 0)) in for i = 1 to pred len1 do Array.unsafe_set res i (f i (uget v1 i) (uget v2 i)) done; res end
let map3 f v1 v2 v3 = let len1 = Array.length v1 in let () = if len1 <> Array.length v2 || len1 <> Array.length v3 then invalid_arg "Array.map3" in if Int.equal len1 0 then [| |] else begin let res = Array.make len1 (f (uget v1 0) (uget v2 0) (uget v3 0)) in for i = 1 to pred len1 do Array.unsafe_set res i (f (uget v1 i) (uget v2 i) (uget v3 i)) done; res end
let map3_i f v1 v2 v3 = let len1 = Array.length v1 in let len2 = Array.length v2 in let len3 = Array.length v3 in let () = if not (Int.equal len1 len2 && Int.equal len1 len3) then invalid_arg "Array.map3_i" in if Int.equal len1 0 then [| |] else begin let res = Array.make len1 (f 0 (uget v1 0) (uget v2 0) (uget v3 0)) in for i = 1 to pred len1 do Array.unsafe_set res i (f i (uget v1 i) (uget v2 i) (uget v3 i)) done; res end
let map_left f a = (* Ocaml does not guarantee Array.map is LR *) let l = Array.length a in (* (even if so), then we rewrite it *) if Int.equal l 0 then [||] else begin let r = Array.make l (f (uget a 0)) in for i = 1 to l - 1 do Array.unsafe_set r i (f (uget a i)) done; r end
let iter2_i f v1 v2 = let len1 = Array.length v1 in let len2 = Array.length v2 in let () = if not (Int.equal len2 len1) then invalid_arg "Array.iter2" in for i = 0 to len1 - 1 do f i (uget v1 i) (uget v2 i) done
let iter3 f v1 v2 v3 = let len1 = Array.length v1 in let len2 = Array.length v2 in let len3 = Array.length v3 in let () = if not (Int.equal len2 len1) || not (Int.equal len1 len3) then invalid_arg "Array.iter3" in for i = 0 to len1 - 1 do f (uget v1 i) (uget v2 i) (uget v3 i) done
let map_right f a = let l = length a in if l = 0 then [||] else begin let r = Array.make l (f (unsafe_get a (l-1))) in for i = l-2 downto 0 do unsafe_set r i (f (unsafe_get a i)) done; r end
let map2_right f a b = let l = length a in if l <> length b then invalid_arg "CArray.map2_right: length mismatch"; if l = 0 then [||] else begin let r = Array.make l (f (unsafe_get a (l-1)) (unsafe_get b (l-1))) in for i = l-2 downto 0 do unsafe_set r i (f (unsafe_get a i) (unsafe_get b i)) done; r end
let fold_right_map f v e = let e' = ref e in let v' = map_right (fun x -> let (y,e) = f x !e' in e' := e; y) v in (v',!e')
let fold_left_map f e v = let e' = ref e in let v' = Array.map (fun x -> let (e,y) = f !e' x in e' := e; y) v in (!e',v')
let fold_right2_map f v1 v2 e = let e' = ref e in let v' = map2_right (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2 in (v',!e')
let fold_left2_map f e v1 v2 = let e' = ref e in let v' = map2 (fun x1 x2 -> let (e,y) = f !e' x1 x2 in e' := e; y) v1 v2 in (!e',v')
let fold_left_map_i f e v = let e' = ref e in let v' = mapi (fun idx x -> let (e,y) = f idx !e' x in e' := e; y) v in (!e',v')
let fold_left2_map_i f e v1 v2 = let e' = ref e in let v' = map2_i (fun idx x1 x2 -> let (e,y) = f idx !e' x1 x2 in e' := e; y) v1 v2 in (!e',v')
let distinct v = let visited = Hashtbl.create 23 in try Array.iter (fun x -> if Hashtbl.mem visited x then raise_notrace Exit else Hashtbl.add visited x x) v; true with Exit -> false
let rev_to_list a = let rec tolist i res = if i >= Array.length a then res else tolist (i+1) (uget a i :: res) in tolist 0 []
let filter_with filter v = Array.of_list (CList.filter_with filter (Array.to_list v))
module Smart =struct
(* If none of the elements is changed by f we return ar itself. The while loop looks for the first such an element. If found, we break here and the new array is produced, but f is not re-applied to elements that are already checked *) let map f (ar : 'a array) = let len = Array.length ar in let i = ref 0 in let break = ref true in let temp = ref None in while !break && (!i < len) do let v = Array.unsafe_get ar !i in let v' = f v in if v == v' then incr i else begin break := false; temp := Some v'; end done; if !i < len then begin (* The array is not the same as the original one *) let ans : 'a array = Array.copy ar in let v = match !temp with None -> assert false | Some x -> x in Array.unsafe_set ans !i v; incr i; while !i < len do let v = Array.unsafe_get ans !i in let v' = f v in if v != v' then Array.unsafe_set ans !i v'; incr i done; ans end else ar
(* Same as map_i but smart *) let map_i f (ar : 'a array) = let len = Array.length ar in let i = ref 0 in let break = ref true in let temp = ref None in while !break && (!i < len) do let v = Array.unsafe_get ar !i in let v' = f !i v in if v == v' then incr i else begin break := false; temp := Some v'; end done; if !i < len then begin (* The array is not the same as the original one *) let ans : 'a array = Array.copy ar in let v = match !temp with None -> assert false | Some x -> x in Array.unsafe_set ans !i v; incr i; while !i < len do let v = Array.unsafe_get ans !i in let v' = f !i v in if v != v' then Array.unsafe_set ans !i v'; incr i done; ans end else ar
let map2 f aux_ar ar = let len = Array.length ar in let aux_len = Array.length aux_ar in let () = if not (Int.equal len aux_len) then invalid_arg "Array.Smart.map2" in let i = ref 0 in let break = ref true in let temp = ref None in while !break && (!i < len) do let v = Array.unsafe_get ar !i in let w = Array.unsafe_get aux_ar !i in let v' = f w v in if v == v' then incr i else begin break := false; temp := Some v'; end done; if !i < len then begin (* The array is not the same as the original one *) let ans : 'a array = Array.copy ar in let v = match !temp with None -> assert false | Some x -> x in Array.unsafe_set ans !i v; incr i; while !i < len do let v = Array.unsafe_get ans !i in let w = Array.unsafe_get aux_ar !i in let v' = f w v in if v != v' then Array.unsafe_set ans !i v'; incr i done; ans end else ar
(** Same as [Smart.map] but threads a state meanwhile *) let fold_left_map f accu (ar : 'a array) = let len = Array.length ar in let i = ref 0 in let break = ref true in let r = ref accu in (* This variable is never accessed unset *) let temp = ref None in while !break && (!i < len) do let v = Array.unsafe_get ar !i in let (accu, v') = f !r v in r := accu; if v == v' then incr i else begin break := false; temp := Some v'; end done; if !i < len then begin let ans : 'a array = Array.copy ar in let v = match !temp with None -> assert false | Some x -> x in Array.unsafe_set ans !i v; incr i; while !i < len do let v = Array.unsafe_get ar !i in let (accu, v') = f !r v in r := accu; if v != v' then Array.unsafe_set ans !i v'; incr i done; !r, ans end else !r, ar
(** Same as [Smart.mapi] but threads a state meanwhile *) let fold_left_map_i f accu (ar : 'a array) = let len = Array.length ar in let i = ref 0 in let break = ref true in let r = ref accu in (* This variable is never accessed unset *) let temp = ref None in while !break && (!i < len) do let v = Array.unsafe_get ar !i in let (accu, v') = f !i !r v in r := accu; if v == v' then incr i else begin break := false; temp := Some v'; end done; if !i < len then begin let ans : 'a array = Array.copy ar in let v = match !temp with None -> assert false | Some x -> x in Array.unsafe_set ans !i v; incr i; while !i < len do let v = Array.unsafe_get ar !i in let (accu, v') = f !i !r v in r := accu; if v != v' then Array.unsafe_set ans !i v'; incr i done; !r, ans end else !r, ar
(** Same as [Smart.map2] but threads a state meanwhile *) let fold_left2_map f accu aux_ar ar = let len = Array.length ar in let aux_len = Array.length aux_ar in let () = if not (Int.equal len aux_len) then invalid_arg "Array.Smart.fold_left2_map" in let i = ref 0 in let break = ref true in let r = ref accu in (* This variable is never accessed unset *) let temp = ref None in while !break && (!i < len) do let v = Array.unsafe_get ar !i in let w = Array.unsafe_get aux_ar !i in let (accu, v') = f !r w v in r := accu; if v == v' then incr i else begin break := false; temp := Some v'; end done; if !i < len then begin let ans : 'a array = Array.copy ar in let v = match !temp with None -> assert false | Some x -> x in Array.unsafe_set ans !i v; incr i; while !i < len do let v = Array.unsafe_get ar !i in let w = Array.unsafe_get aux_ar !i in let (accu, v') = f !r w v in r := accu; if v != v' then Array.unsafe_set ans !i v'; incr i done; !r, ans end else !r, ar
end
module Fun1 =struct
let map f arg v = match v with | [| |] -> [| |] | _ -> let len = Array.length v in let x0 = Array.unsafe_get v 0 in let ans = Array.make len (f arg x0) in for i = 1 to pred len do let x = Array.unsafe_get v i in Array.unsafe_set ans i (f arg x) done; ans
let iter f arg v = let len = Array.length v in for i = 0 to pred len do let x = uget v i in f arg x done
let iter2 f arg v1 v2 = let len1 = Array.length v1 in let len2 = Array.length v2 in let () = if not (Int.equal len2 len1) then invalid_arg "Array.Fun1.iter2" in for i = 0 to pred len1 do let x1 = uget v1 i in let x2 = uget v2 i in f arg x1 x2 done
module Smart = struct
let map f arg (ar : 'a array) = let len = Array.length ar in let i = ref 0 in let break = ref true in let temp = ref None in while !break && (!i < len) do let v = Array.unsafe_get ar !i in let v' = f arg v in if v == v' then incr i else begin break := false; temp := Some v'; end done; if !i < len then begin (* The array is not the same as the original one *) let ans : 'a array = Array.copy ar in let v = match !temp with None -> assert false | Some x -> x in Array.unsafe_set ans !i v; incr i; while !i < len do let v = Array.unsafe_get ans !i in let v' = f arg v in if v != v' then Array.unsafe_set ans !i v'; incr i done; ans end else ar
end
end