package lambdapi
Proof assistant for the λΠ-calculus modulo rewriting
Install
Dune Dependency
Authors
Maintainers
Sources
lambdapi-2.6.0.tbz
sha256=d01e5f13db2eaba6e4fe330667149e0059d4886c651ff9d6b672db2dfc9765ed
sha512=33b68c972aca37985ed73c527076198e7d4961c7e27c89cdabfe4d1cff97cd41ccfb85ae9499eb98ad9a0aefd920bc55555df6393fc441ac2429e4d99cddafa8
doc/src/lambdapi.lplib/array.ml.html
Source file array.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
module A = Stdlib.Array include A open Base (** [for_all2 p a1 a2] checks if the corresponding elements of arrays [a1] and [a2] satisfy the predicate [p]. The [Invalid_argument] exception is raised if the arrays do not have the same size. *) let for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool = fun f a1 a2 -> let exception Done in let f x y = if not (f x y) then raise Done in try iter2 f a1 a2; true with Done -> false (** [pp elt sep ppf a] prints the array [a] on the formatter [ppf] using [sep] as separator and [elt] for printing the elements. *) let pp : 'a pp -> string -> 'a array pp = fun elt sep oc a -> let n = A.length a in if n > 0 then elt oc (A.get a 0); for i = 1 to n - 1 do out oc "%s%a" sep elt (A.get a i) done (** Comparison function on arrays. *) let cmp : 'a cmp -> 'a array cmp = fun cmp_elt -> let cmp a1 a2 (* of the same length *) = let exception Distinct of int in let rec cmp i = if i >= 0 then match cmp_elt (A.get a1 i) (A.get a2 i) with | 0 -> cmp (i - 1) | n -> raise (Distinct n) in try cmp (A.length a1 - 1); 0 with Distinct n -> n in fun a1 a2 -> if a1 == a2 then 0 else lex (cmp_map Stdlib.compare A.length) cmp (a1,a1) (a2,a2) (** [eq eq_elt a1 a2] tests the equality of [a1] and [a2], comparing their elements with [eq_elt]. *) let eq : 'a eq -> 'a array eq = fun eq_elt a1 a2 -> a1 == a2 || (A.length a1 = A.length a2 && for_all2 eq_elt a1 a2) (** [max_index ?cmp a] returns the index of the first maximum of array [a] according to comparison [?cmp]. If [cmp] is not given, defaults to [Stdlib.compare]. *) let max_index : ?cmp:('a -> 'a -> int) -> 'a array -> int = fun ?(cmp = Stdlib.compare) arr -> let len = A.length arr in if len = 0 then invalid_arg "Extra.Array.max_index" else let max = ref 0 in for i = 1 to len - 1 do if cmp (A.get arr !max) (A.get arr i) < 0 then max := i done; !max (** [max ?cmp a] returns the higher element according to comparison function [?cmp], using [Stdlib.compare] if not given, in array [a]. *) let max : ?cmp:('a -> 'a -> int) -> 'a array -> 'a = fun ?(cmp = Stdlib.compare) arr -> A.get arr (max_index ~cmp arr) (** [unzip a] is [List.unzip (Array.to_list a)]. *) let unzip : ('a * 'b) array -> 'a list * 'b list = fun a -> let aux (el, er) (accl, accr) = (el :: accl, er :: accr) in A.fold_right aux a ([], []) (** [drop n a] discards the first [n] elements of [a]. The empty array is returned if [n > length a]. *) let drop : int -> 'a array -> 'a array = fun n a -> let l = length a in if n >= l then [||] else A.sub a n (l - n)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>