Library Ltac2.List
Require Import Ltac2.Init.
Require Ltac2.Int.
Require Ltac2.Control.
Require Ltac2.Bool.
Require Ltac2.Message.
Compute the length of a list.
Ltac2 rec length (ls : 'a list) : int :=
match ls with
| [] => 0
| _ :: xs => Int.add 1 (length xs)
end.
match ls with
| [] => 0
| _ :: xs => Int.add 1 (length xs)
end.
compare_lengths ls1 ls2 is equal to Int.compare (length ls1) (length ls2),
but is more efficient in most cases: it runs in O(min (length ls1) (length ls2))
instead of O(max (length ls1) (length ls2)).
Ltac2 rec compare_lengths (ls1 : 'a list) (ls2 : 'b list) : int :=
match ls1 with
| []
=> match ls2 with
| [] => 0
| _ :: _ => -1
end
| _ :: ls1
=> match ls2 with
| [] => 1
| _ :: ls2 => compare_lengths ls1 ls2
end
end.
match ls1 with
| []
=> match ls2 with
| [] => 0
| _ :: _ => -1
end
| _ :: ls1
=> match ls2 with
| [] => 1
| _ :: ls2 => compare_lengths ls1 ls2
end
end.
compare_length_with ls n is equal to Int.compare (length ls) n,
but is more efficient in most cases: it runs in O(min (length ls) n)
instead of O(length ls).
Ltac2 rec compare_length_with (ls : 'a list) (n : int) : int :=
match Int.lt n 0 with
| true => 1
| false
=> match ls with
| [] => Int.compare 0 n
| _ :: ls => compare_length_with ls (Int.sub n 1)
end
end.
Ltac2 cons (x : 'a) (xs : 'a list) : 'a list :=
x :: xs.
match Int.lt n 0 with
| true => 1
| false
=> match ls with
| [] => Int.compare 0 n
| _ :: ls => compare_length_with ls (Int.sub n 1)
end
end.
Ltac2 cons (x : 'a) (xs : 'a list) : 'a list :=
x :: xs.
Since Ltac2 distinguishes between backtracking and fatal exceptions,
we provide option and default variants of functions which throw in the
OCaml stdlib.
Return the first element of a list.
Returns None if the list is empty.
Ltac2 hd_opt (ls : 'a list) : 'a option :=
match ls with
| [] => None
| x :: _ => Some x
end.
match ls with
| [] => None
| x :: _ => Some x
end.
Return the first element of a list.
Throw an exception if the list is empty.
Ltac2 hd (ls : 'a list) : 'a :=
match ls with
| [] => Control.throw_invalid_argument "List.hd"
| x :: _ => x
end.
match ls with
| [] => Control.throw_invalid_argument "List.hd"
| x :: _ => x
end.
Remove the first element from a list.
The empty list is returned as is.
Ltac2 tl (ls : 'a list) : 'a list :=
match ls with
| [] => []
| _ :: xs => xs
end.
match ls with
| [] => []
| _ :: xs => xs
end.
Destruct a list into its head and tail.
Throws an exception if the list is empty.
Ltac2 dest (xs : 'a list) : 'a * 'a list :=
match xs with
| x :: xs => (x, xs)
| [] => Control.throw_invalid_argument "List.dest: list empty"
end.
match xs with
| x :: xs => (x, xs)
| [] => Control.throw_invalid_argument "List.dest: list empty"
end.
Return true if the list is empty.
Ltac2 is_empty (xs : 'a list) : bool :=
match xs with
| _ :: _ => false
| _ => true
end.
match xs with
| _ :: _ => false
| _ => true
end.
Return the last element of a list.
Returns None if the list is empty.
Ltac2 rec last_opt (ls : 'a list) : 'a option :=
match ls with
| [] => None
| x :: xs
=> match xs with
| [] => Some x
| _ :: _ => last_opt xs
end
end.
match ls with
| [] => None
| x :: xs
=> match xs with
| [] => Some x
| _ :: _ => last_opt xs
end
end.
Return the last element of a list.
Throws an exception if the list is empty.
Ltac2 last (ls : 'a list) : 'a :=
match last_opt ls with
| None => Control.throw_invalid_argument "List.last"
| Some v => v
end.
match last_opt ls with
| None => Control.throw_invalid_argument "List.last"
| Some v => v
end.
Remove the last element of a list.
The empty list is returned as is.
Ltac2 rec removelast (ls : 'a list) : 'a list :=
match ls with
| [] => []
| x :: xs
=> match xs with
| [] => []
| _ :: _ => x :: removelast xs
end
end.
match ls with
| [] => []
| x :: xs
=> match xs with
| [] => []
| _ :: _ => x :: removelast xs
end
end.
Helper function for nth_opt.
Ltac2 rec nth_opt_aux (ls : 'a list) (n : int) :=
match ls with
| [] => None
| x :: xs
=> match Int.equal n 0 with
| true => Some x
| false => nth_opt_aux xs (Int.sub n 1)
end
end.
match ls with
| [] => None
| x :: xs
=> match Int.equal n 0 with
| true => Some x
| false => nth_opt_aux xs (Int.sub n 1)
end
end.
nth_opt ls n returns the n-th element ls, starting at 0.
Throws an exception if n < 0. Returns None if n >= length ls.
Ltac2 nth_opt (ls : 'a list) (n : int) : 'a option :=
Control.assert_valid_argument "List.nth" (Int.ge n 0);
nth_opt_aux ls n.
Control.assert_valid_argument "List.nth" (Int.ge n 0);
nth_opt_aux ls n.
nth ls n returns the n-th element of ls, starting at 0.
Throws an exception if n < 0 or n >= length ls.
Ltac2 nth (ls : 'a list) (n : int) : 'a :=
match nth_opt ls n with
| Some v => v
| None => Control.throw_out_of_bounds "List.nth"
end.
match nth_opt ls n with
| Some v => v
| None => Control.throw_out_of_bounds "List.nth"
end.
Reverse l1, and append it with l2:
rev_append l1 l2 = append (rev l1) l2.
Ltac2 rec rev_append (l1 : 'a list) (l2 : 'a list) : 'a list :=
match l1 with
| [] => l2
| a :: l => rev_append l (a :: l2)
end.
match l1 with
| [] => l2
| a :: l => rev_append l (a :: l2)
end.
Reverse a list.
Ltac2 rev (l : 'a list) : 'a list :=
rev_append l [].
rev_append l [].
Append two lists ls1 and ls2. Complexity: O(length ls1).
Ltac2 rec append (ls1 : 'a list) (ls2 : 'a list) : 'a list :=
match ls1 with
| [] => ls2
| x :: xs => x :: append xs ls2
end.
match ls1 with
| [] => ls2
| x :: xs => x :: append xs ls2
end.
Concatenate a list of lists.
Ltac2 rec concat (ls : 'a list list) : 'a list :=
match ls with
| [] => []
| x :: xs => append x (concat xs)
end.
match ls with
| [] => []
| x :: xs => append x (concat xs)
end.
Synonym for concat.
Ltac2 flatten (ls : 'a list list) : 'a list :=
concat ls.
concat ls.
Iterate a function on each element of a list.
Elements are processed from first to last.
Ltac2 rec iter (f : 'a -> unit) (ls : 'a list) : unit :=
match ls with
| [] => ()
| l :: ls => f l; iter f ls
end.
match ls with
| [] => ()
| l :: ls => f l; iter f ls
end.
Helper function for iteri.
Ltac2 rec iteri_aux (i : int) (f : int -> 'a -> unit) (ls : 'a list) : unit :=
match ls with
| [] => ()
| l :: ls => f i l; iteri_aux (Int.add i 1) f ls
end.
match ls with
| [] => ()
| l :: ls => f i l; iteri_aux (Int.add i 1) f ls
end.
Iterate a function f on each element of a list.
f is additionally supplied the index of each element, starting at 0.
Elements are processed from first to last.
Ltac2 iteri (f : int -> 'a -> unit) (ls : 'a list) : unit :=
iteri_aux 0 f ls.
iteri_aux 0 f ls.
map f [x0 ; x1 ; ... ; xN] is f x0 ; f x1 ; ... ; f xN.
Elements are processed from first to last.
Ltac2 rec map (f : 'a -> 'b) (ls : 'a list) : 'b list :=
match ls with
| [] => []
| l :: ls => f l :: map f ls
end.
match ls with
| [] => []
| l :: ls => f l :: map f ls
end.
Helper function for mapi.
Ltac2 rec mapi_aux (i : int) (f : int -> 'a -> 'b) (ls : 'a list) : 'b list :=
match ls with
| [] => []
| l :: ls => f i l :: mapi_aux (Int.add i 1) f ls
end.
match ls with
| [] => []
| l :: ls => f i l :: mapi_aux (Int.add i 1) f ls
end.
mapi f [x0 ; x1 ; ... ; xN] is f 0 x0 ; f 1 x1 ; ... ; f N xN.
Elements are processed from first to last.
Ltac2 mapi (f : int -> 'a -> 'b) (ls : 'a list) : 'b list :=
mapi_aux 0 f ls.
mapi_aux 0 f ls.
Map a function over a list, and then concatenate the results.
Ltac2 rec flat_map (f : 'a -> 'b list) (xs : 'a list) : 'b list :=
match xs with
| [] => []
| x :: xs => append (f x) (flat_map f xs)
end.
match xs with
| [] => []
| x :: xs => append (f x) (flat_map f xs)
end.
rev_map f l is equal to rev (map f l),
but is more efficient in most cases.
Ltac2 rev_map (f : 'a -> 'b) (ls : 'a list) : 'b list :=
let rec rmap_f accu ls :=
match ls with
| [] => accu
| a::l => rmap_f (f a :: accu) l
end in
rmap_f [] ls.
let rec rmap_f accu ls :=
match ls with
| [] => accu
| a::l => rmap_f (f a :: accu) l
end in
rmap_f [] ls.
fold_right f [a1; ...; an] init is f a1 (f a2 (... (f an init) ...)).
Ltac2 rec fold_right (f : 'a -> 'b -> 'b) (ls : 'a list) (a : 'b) : 'b :=
match ls with
| [] => a
| l :: ls => f l (fold_right f ls a)
end.
match ls with
| [] => a
| l :: ls => f l (fold_right f ls a)
end.
fold_left f init [b1; ...; bn] is f (... (f (f init b1) b2) ...) bn.
Ltac2 rec fold_left (f : 'a -> 'b -> 'a) (a : 'a) (xs : 'b list) : 'a :=
match xs with
| [] => a
| x :: xs => fold_left f (f a x) xs
end.
Ltac2 fold_lefti (f : int -> 'a -> 'b -> 'a) (a : 'a) (xs : 'b list) : 'a :=
let rec go i a xs :=
match xs with
| [] => a
| x :: xs => go (Int.add i 1) (f i a x) xs
end
in go 0 a xs.
match xs with
| [] => a
| x :: xs => fold_left f (f a x) xs
end.
Ltac2 fold_lefti (f : int -> 'a -> 'b -> 'a) (a : 'a) (xs : 'b list) : 'a :=
let rec go i a xs :=
match xs with
| [] => a
| x :: xs => go (Int.add i 1) (f i a x) xs
end
in go 0 a xs.
Iterate a function over two lists.
Elements are processed from first to last.
Throws an exception if the lengths of the lists differ.
Ltac2 rec iter2 (f : 'a -> 'b -> unit) (ls1 : 'a list) (ls2 : 'b list) : unit :=
match ls1 with
| []
=> match ls2 with
| [] => ()
| _ :: _ => Control.throw_invalid_argument "List.iter2"
end
| l1 :: ls1
=> match ls2 with
| [] => Control.throw_invalid_argument "List.iter2"
| l2 :: ls2
=> f l1 l2; iter2 f ls1 ls2
end
end.
match ls1 with
| []
=> match ls2 with
| [] => ()
| _ :: _ => Control.throw_invalid_argument "List.iter2"
end
| l1 :: ls1
=> match ls2 with
| [] => Control.throw_invalid_argument "List.iter2"
| l2 :: ls2
=> f l1 l2; iter2 f ls1 ls2
end
end.
Map a function over two lists.
Elements are processed from first to last.
Throws an exception if the lengths of the lists differ.
Ltac2 rec map2 (f : 'a -> 'b -> 'c) (ls1 : 'a list) (ls2 : 'b list) : 'c list :=
match ls1 with
| []
=> match ls2 with
| [] => []
| _ :: _ => Control.throw_invalid_argument "List.map2"
end
| l1 :: ls1
=> match ls2 with
| [] => Control.throw_invalid_argument "List.map2"
| l2 :: ls2
=> f l1 l2 :: map2 f ls1 ls2
end
end.
match ls1 with
| []
=> match ls2 with
| [] => []
| _ :: _ => Control.throw_invalid_argument "List.map2"
end
| l1 :: ls1
=> match ls2 with
| [] => Control.throw_invalid_argument "List.map2"
| l2 :: ls2
=> f l1 l2 :: map2 f ls1 ls2
end
end.
rev_map2 f l1 l2 is equal to rev (map2 f l1 l2),
but is more efficient in most cases.
Ltac2 rev_map2 (f : 'a -> 'b -> 'c) (ls1 : 'a list) (ls2 : 'b list) : 'c list :=
let rec rmap2_f accu ls1 ls2 :=
match ls1 with
| []
=> match ls2 with
| [] => accu
| _ :: _ => Control.throw_invalid_argument "List.rev_map2"
end
| l1 :: ls1
=> match ls2 with
| [] => Control.throw_invalid_argument "List.rev_map2"
| l2 :: ls2
=> rmap2_f (f l1 l2 :: accu) ls1 ls2
end
end in
rmap2_f [] ls1 ls2.
let rec rmap2_f accu ls1 ls2 :=
match ls1 with
| []
=> match ls2 with
| [] => accu
| _ :: _ => Control.throw_invalid_argument "List.rev_map2"
end
| l1 :: ls1
=> match ls2 with
| [] => Control.throw_invalid_argument "List.rev_map2"
| l2 :: ls2
=> rmap2_f (f l1 l2 :: accu) ls1 ls2
end
end in
rmap2_f [] ls1 ls2.
Right fold over two lists.
Throws an exception if the lengths of the lists differ.
Ltac2 rec fold_right2 (f : 'a -> 'b -> 'c -> 'c) (ls1 : 'a list) (ls2 : 'b list) (a : 'c) : 'c :=
match ls1 with
| []
=> match ls2 with
| [] => a
| _ :: _ => Control.throw_invalid_argument "List.fold_right2"
end
| l1 :: ls1
=> match ls2 with
| [] => Control.throw_invalid_argument "List.fold_right2"
| l2 :: ls2
=> f l1 l2 (fold_right2 f ls1 ls2 a)
end
end.
match ls1 with
| []
=> match ls2 with
| [] => a
| _ :: _ => Control.throw_invalid_argument "List.fold_right2"
end
| l1 :: ls1
=> match ls2 with
| [] => Control.throw_invalid_argument "List.fold_right2"
| l2 :: ls2
=> f l1 l2 (fold_right2 f ls1 ls2 a)
end
end.
Left fold over two lists.
Throws an exception if the lengths of the lists differ.
Ltac2 rec fold_left2 (f : 'a -> 'b -> 'c -> 'a) (a : 'a) (ls1 : 'b list) (ls2 : 'c list) : 'a :=
match ls1 with
| []
=> match ls2 with
| [] => a
| _ :: _ => Control.throw_invalid_argument "List.fold_left2"
end
| l1 :: ls1
=> match ls2 with
| [] => Control.throw_invalid_argument "List.fold_left2"
| l2 :: ls2
=> fold_left2 f (f a l1 l2) ls1 ls2
end
end.
match ls1 with
| []
=> match ls2 with
| [] => a
| _ :: _ => Control.throw_invalid_argument "List.fold_left2"
end
| l1 :: ls1
=> match ls2 with
| [] => Control.throw_invalid_argument "List.fold_left2"
| l2 :: ls2
=> fold_left2 f (f a l1 l2) ls1 ls2
end
end.
for_all f l checks that f returns true on all elements of the list l.
In particular for_all f [] is true.
Ltac2 rec for_all (f : 'a -> bool) (ls : 'a list) : bool :=
match ls with
| [] => true
| x :: xs => match f x with
| true => for_all f xs
| false => false
end
end.
match ls with
| [] => true
| x :: xs => match f x with
| true => for_all f xs
| false => false
end
end.
exist f l checks that f returns true on at least one element of the list l.
In particular exist f [] is false.
We would call this exists a la OCaml's List.exists,
but that would be a syntax error (because it conflicts with the notation for tactic `exists`), so instead we name it exist.
Ltac2 rec exist (f : 'a -> bool) (ls : 'a list) : bool :=
match ls with
| [] => false
| x :: xs => match f x with
| true => true
| false => exist f xs
end
end.
match ls with
| [] => false
| x :: xs => match f x with
| true => true
| false => exist f xs
end
end.
Helper function for for_all2.
Ltac2 rec for_all2_aux (on_length_mismatch : 'a list -> 'b list -> bool) f xs ys : bool :=
match xs with
| [] => match ys with
| [] => true
| _ :: _ => on_length_mismatch xs ys
end
| x :: xs'
=> match ys with
| [] => on_length_mismatch xs ys
| y :: ys'
=> match f x y with
| true => for_all2_aux on_length_mismatch f xs' ys'
| false => false
end
end
end.
match xs with
| [] => match ys with
| [] => true
| _ :: _ => on_length_mismatch xs ys
end
| x :: xs'
=> match ys with
| [] => on_length_mismatch xs ys
| y :: ys'
=> match f x y with
| true => for_all2_aux on_length_mismatch f xs' ys'
| false => false
end
end
end.
Same as for_all but for two lists.
Throws an exception in case the lengths of the lists differ.
Ltac2 for_all2 (f : 'a -> 'b -> bool) (xs : 'a list) (ys : 'b list) : bool :=
for_all2_aux (fun _ _ => Control.throw_invalid_argument "List.for_all2") f xs ys.
for_all2_aux (fun _ _ => Control.throw_invalid_argument "List.for_all2") f xs ys.
Same as for_all but for two lists.
Returns false in case the lengths of the lists differ.
Ltac2 equal (f : 'a -> 'b -> bool) (xs : 'a list) (ys : 'b list) : bool :=
for_all2_aux (fun _ _ => false) f xs ys.
for_all2_aux (fun _ _ => false) f xs ys.
Same as exist but for two lists.
Throws an exception if the lengths of the lists differ.
Ltac2 rec exist2 (f : 'a -> 'b -> bool) (xs : 'a list) (ys : 'b list) : bool :=
match xs with
| [] => match ys with
| [] => false
| _ :: _ => Control.throw_invalid_argument "List.exist2"
end
| x :: xs'
=> match ys with
| [] => Control.throw_invalid_argument "List.exist2"
| y :: ys'
=> match f x y with
| true => true
| false => exist2 f xs' ys'
end
end
end.
match xs with
| [] => match ys with
| [] => false
| _ :: _ => Control.throw_invalid_argument "List.exist2"
end
| x :: xs'
=> match ys with
| [] => Control.throw_invalid_argument "List.exist2"
| y :: ys'
=> match f x y with
| true => true
| false => exist2 f xs' ys'
end
end
end.
find_opt f xs returns the first element of the list xs satisfying f.
Returns None if no element is found.
Ltac2 rec find_opt (f : 'a -> bool) (xs : 'a list) : 'a option :=
match xs with
| [] => None
| x :: xs => match f x with
| true => Some x
| false => find_opt f xs
end
end.
match xs with
| [] => None
| x :: xs => match f x with
| true => Some x
| false => find_opt f xs
end
end.
find f xs returns the first element of the list xs satisfying f.
Throws an exception if no element is found.
Ltac2 find (f : 'a -> bool) (xs : 'a list) : 'a :=
match find_opt f xs with
| Some v => v
| None => Control.throw Not_found
end.
match find_opt f xs with
| Some v => v
| None => Control.throw Not_found
end.
find_rev_opt f xs returns the last element of the list xs satisfying f.
Returns None if no element is found.
Ltac2 rec find_rev_opt (f : 'a -> bool) (xs : 'a list) : 'a option :=
match xs with
| [] => None
| x :: xs => match find_rev_opt f xs with
| Some v => Some v
| None => match f x with
| true => Some x
| false => None
end
end
end.
match xs with
| [] => None
| x :: xs => match find_rev_opt f xs with
| Some v => Some v
| None => match f x with
| true => Some x
| false => None
end
end
end.
find_rev f xs returns the last element of the list xs satisfying f.
Throws an exception if no element is found.
Ltac2 find_rev (f : 'a -> bool) (xs : 'a list) : 'a :=
match find_rev_opt f xs with
| Some v => v
| None => Control.throw Not_found
end.
match find_rev_opt f xs with
| Some v => v
| None => Control.throw Not_found
end.
mem eq a ls checks if an element of ls is equal to a according
to the user-supplied equality function eq.
Ltac2 mem (eq : 'a -> 'a -> bool) (a : 'a) (ls : 'a list) : bool :=
exist (eq a) ls.
exist (eq a) ls.
filter f xs removes all the elements of xs which do not satisfy f.
Ltac2 rec filter (f : 'a -> bool) (xs : 'a list) : 'a list :=
match xs with
| [] => []
| x :: xs
=> match f x with
| true => x :: filter f xs
| false => filter f xs
end
end.
match xs with
| [] => []
| x :: xs
=> match f x with
| true => x :: filter f xs
| false => filter f xs
end
end.
filter_out f xs removes all the elements of xs which satisfy f.
Ltac2 rec filter_out (f : 'a -> bool) (xs : 'a list) : 'a list :=
filter (fun x => Bool.neg (f x)) xs.
filter (fun x => Bool.neg (f x)) xs.
Synonym for filter.
Ltac2 find_all (f : 'a -> bool) (ls : 'a list) : 'a list := filter f ls.
remove eqb x ls removes all elements of ls which are equal to x,
according to the user-supplied equality function eqb.
Ltac2 remove (eqb : 'a -> 'a -> bool) (x : 'a) (ls : 'a list) : 'a list :=
filter_out (eqb x) ls.
filter_out (eqb x) ls.
count_occ eqb x ls counts how many elements of ls are equal to x, according
to the user-supplied equality function eqb.
Ltac2 count_occ (eqb : 'a -> 'a -> bool) (x : 'a) (ls : 'a list) : int :=
length (filter (eqb x) ls).
length (filter (eqb x) ls).
list_power ls1 ls2) is [ls2]^[ls1], or the set of sequences of elements
of [ls2] indexed by elements of [ls1], sorted in lexicographic order.
Ltac2 rec list_power (ls1 : 'a list) (ls2 : 'b list) : ('a * 'b) list list :=
match ls1 with
| [] => [] :: []
| x :: t
=> flat_map (fun f => map (fun y => (x, y) :: f) ls2)
(list_power t ls2)
end.
match ls1 with
| [] => [] :: []
| x :: t
=> flat_map (fun f => map (fun y => (x, y) :: f) ls2)
(list_power t ls2)
end.
partition f l returns two lists (l_true, l_false) such that:
- l_true is the sublist of elements of l which satisfy f.
- l_false is the sublist of elements of l which do not satisfy f.
Ltac2 rec partition (f : 'a -> bool) (l : 'a list) : 'a list * 'a list :=
match l with
| [] => ([], [])
| x :: tl
=> let (g, d) := partition f tl in
match f x with
| true => ((x::g), d)
| false => (g, (x::d))
end
end.
match l with
| [] => ([], [])
| x :: tl
=> let (g, d) := partition f tl in
match f x with
| true => ((x::g), d)
| false => (g, (x::d))
end
end.
list_prod ls1 ls2 returns the cartesian product of ls1 and ls2,
i.e. the list of all pairs (x, y) where x is in ls1 and y is in ls2.
Ltac2 rec list_prod (ls1 : 'a list) (ls2 : 'b list) : ('a * 'b) list :=
match ls1 with
| [] => []
| x :: t
=> append (map (fun y => (x, y)) ls2) (list_prod t ls2)
end.
match ls1 with
| [] => []
| x :: t
=> append (map (fun y => (x, y)) ls2) (list_prod t ls2)
end.
fistn n ls returns the first n elements of ls.
Throws an exception if n < 0 or n > length ls.
Ltac2 rec firstn (n : int) (ls : 'a list) : 'a list :=
Control.assert_valid_argument "List.firstn" (Int.ge n 0);
match Int.equal n 0 with
| true => []
| false
=> match ls with
| [] => Control.throw_out_of_bounds "List.firstn"
| x :: xs
=> x :: firstn (Int.sub n 1) xs
end
end.
Control.assert_valid_argument "List.firstn" (Int.ge n 0);
match Int.equal n 0 with
| true => []
| false
=> match ls with
| [] => Control.throw_out_of_bounds "List.firstn"
| x :: xs
=> x :: firstn (Int.sub n 1) xs
end
end.
skipn n ls removes the first n elements of ls.
Throws an exception if n < 0 or n > length ls.
Ltac2 rec skipn (n : int) (ls : 'a list) : 'a list :=
Control.assert_valid_argument "List.skipn" (Int.ge n 0);
match Int.equal n 0 with
| true => ls
| false
=> match ls with
| [] => Control.throw_out_of_bounds "List.skipn"
| _ :: xs
=> skipn (Int.sub n 1) xs
end
end.
Control.assert_valid_argument "List.skipn" (Int.ge n 0);
match Int.equal n 0 with
| true => ls
| false
=> match ls with
| [] => Control.throw_out_of_bounds "List.skipn"
| _ :: xs
=> skipn (Int.sub n 1) xs
end
end.
lastn n ls returns the last n elements of ls.
Throws an exception if n < 0 or n > length ls.
Ltac2 lastn (n : int) (ls : 'a list) : 'a list :=
let l := length ls in
Control.assert_valid_argument "List.lastn" (Int.ge n 0);
Control.assert_bounds "List.lastn" (Int.le n l);
skipn (Int.sub l n) ls.
let l := length ls in
Control.assert_valid_argument "List.lastn" (Int.ge n 0);
Control.assert_bounds "List.lastn" (Int.le n l);
skipn (Int.sub l n) ls.
nodup eqb ls removes duplicates from ls, according
to the user-suppplied equality function eq.
Ltac2 rec nodup (eqb : 'a -> 'a -> bool) (ls : 'a list) : 'a list :=
match ls with
| [] => []
| x :: xs
=> match mem eqb x xs with
| true => nodup eqb xs
| false => x :: nodup eqb xs
end
end.
match ls with
| [] => []
| x :: xs
=> match mem eqb x xs with
| true => nodup eqb xs
| false => x :: nodup eqb xs
end
end.
seq start step last returns the list start ; (start + step) ; (start + 2*step) ; ...,
stopping when start + n*step >= last. In particular the lower bound start is included,
whereas the upper bound last is excluded.
Ltac2 rec seq (start : int) (step : int) (last : int) : int list :=
match Int.lt (Int.sub last start) step with
| true
=> []
| false
=> start :: seq (Int.add start step) step last
end.
match Int.lt (Int.sub last start) step with
| true
=> []
| false
=> start :: seq (Int.add start step) step last
end.
init n f returns the list f 0 ; f 1 ; ... ; f (n-1).
Throws an exception if n < 0.
Ltac2 init (n : int) (f : int -> 'a) : 'a list :=
Control.assert_valid_argument "List.init" (Int.ge n 0);
map f (seq 0 1 n).
Control.assert_valid_argument "List.init" (Int.ge n 0);
map f (seq 0 1 n).
repeat x n returns the list of length n with all elements equal to x.
Ltac2 repeat (x : 'a) (n : int) : 'a list :=
init n (fun _ => x).
init n (fun _ => x).
assoc eqk k l returns the first value associated to key k in an association list l,
using eqk to compare keys for equality.
Throws an exception if no value is found.
Ltac2 assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) : 'v :=
let eq_key kv := let (k', _) := kv in eqk k k' in
let (_, v) := find eq_key l in
v.
let eq_key kv := let (k', _) := kv in eqk k k' in
let (_, v) := find eq_key l in
v.
assoc eqk k l returns the first value associated to key k in an association list l,
using eqk to compare keys for equality.
Returns None if no value is found.
Ltac2 assoc_opt (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) : 'v option :=
let eq_key kv := let (k', _) := kv in eqk k k' in
match find_opt eq_key l with
| Some kv => let (_, v) := kv in Some v
| None => None
end.
let eq_key kv := let (k', _) := kv in eqk k k' in
match find_opt eq_key l with
| Some kv => let (_, v) := kv in Some v
| None => None
end.
mem_assoc eqk k l checks if the key k is present in an association list l,
using eqk to compare keys for equality.
Ltac2 mem_assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) : bool :=
let eq_key kv := let (k', _) := kv in eqk k k' in
exist eq_key l.
let eq_key kv := let (k', _) := kv in eqk k k' in
exist eq_key l.
remove_assoc eqk k l removes all key/value pairs associated with key k
from an association list l, using eqk to compare keys for equality.
Ltac2 remove_assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) : ('k * 'v) list :=
let eq_key kv := let (k', _) := kv in eqk k k' in
filter_out eq_key l.
let eq_key kv := let (k', _) := kv in eqk k k' in
filter_out eq_key l.
Split a list of pairs into a pair of lists.
Ltac2 rec split (ls : ('a * 'b) list) : 'a list * 'b list :=
match ls with
| [] => ([], [])
| xy :: tl
=> let (x, y) := xy in
let (left, right) := split tl in
((x::left), (y::right))
end.
match ls with
| [] => ([], [])
| xy :: tl
=> let (x, y) := xy in
let (left, right) := split tl in
((x::left), (y::right))
end.
Combine two lists into a list of pairs. Only pairs of elements
at the same position are considered.
Throws an exception if the lengths of the lists differ.
Ltac2 rec combine (ls1 : 'a list) (ls2 : 'b list) : ('a * 'b) list :=
match ls1 with
| []
=> match ls2 with
| [] => []
| _ :: _ => Control.throw_invalid_argument "List.combine"
end
| x :: xs
=> match ls2 with
| y :: ys
=> (x, y) :: combine xs ys
| [] => Control.throw_invalid_argument "List.combine"
end
end.
match ls1 with
| []
=> match ls2 with
| [] => []
| _ :: _ => Control.throw_invalid_argument "List.combine"
end
| x :: xs
=> match ls2 with
| y :: ys
=> (x, y) :: combine xs ys
| [] => Control.throw_invalid_argument "List.combine"
end
end.
enumerate [x0 ; x1 ; x2 ; ...] returns the list (0, x0) ; (1, x1) ; (2, x2) ; ....
Ltac2 enumerate (ls : 'a list) :=
mapi (fun i v => (i,v)) ls.
mapi (fun i v => (i,v)) ls.
Merge two list sorted in increasing order into a sorted list,
using a user-provided comparison function.
Ltac2 rec merge (cmp : 'a -> 'a -> int) (l1 : 'a list) (l2 : 'a list) : 'a list :=
let rec merge_aux l2 :=
match l1 with
| [] => l2
| a1 :: l1'
=> match l2 with
| [] => l1
| a2 :: l2'
=> match Int.le (cmp a1 a2) 0 with
| true => a1 :: merge cmp l1' l2
| false => a2 :: merge_aux l2'
end
end
end in
merge_aux l2.
Ltac2 rec merge_list_to_stack cmp stack l :=
match stack with
| [] => [Some l]
| l' :: stack'
=> match l' with
| None => Some l :: stack'
| Some l'
=> None :: merge_list_to_stack cmp stack' (merge cmp l' l)
end
end.
Ltac2 rec merge_stack cmp stack :=
match stack with
| [] => []
| l :: stack'
=> match l with
| None => merge_stack cmp stack'
| Some l => merge cmp l (merge_stack cmp stack')
end
end.
Ltac2 rec iter_merge cmp stack l :=
match l with
| [] => merge_stack cmp stack
| a::l' => iter_merge cmp (merge_list_to_stack cmp stack [a]) l'
end.
let rec merge_aux l2 :=
match l1 with
| [] => l2
| a1 :: l1'
=> match l2 with
| [] => l1
| a2 :: l2'
=> match Int.le (cmp a1 a2) 0 with
| true => a1 :: merge cmp l1' l2
| false => a2 :: merge_aux l2'
end
end
end in
merge_aux l2.
Ltac2 rec merge_list_to_stack cmp stack l :=
match stack with
| [] => [Some l]
| l' :: stack'
=> match l' with
| None => Some l :: stack'
| Some l'
=> None :: merge_list_to_stack cmp stack' (merge cmp l' l)
end
end.
Ltac2 rec merge_stack cmp stack :=
match stack with
| [] => []
| l :: stack'
=> match l with
| None => merge_stack cmp stack'
| Some l => merge cmp l (merge_stack cmp stack')
end
end.
Ltac2 rec iter_merge cmp stack l :=
match l with
| [] => merge_stack cmp stack
| a::l' => iter_merge cmp (merge_list_to_stack cmp stack [a]) l'
end.
sort cmp l sorts the list l in increasing order,
according to the user-supplied comparison function cmp.
It is currently implemented using a variant of merge sort.
Ltac2 sort (cmp : 'a -> 'a -> int) (l : 'a list) : 'a list :=
iter_merge cmp [] l.
iter_merge cmp [] l.
sort cmp l sorts the list l in increasing order and removes duplicates,
according to the user-supplied comparison function cmp.
This takes advantage of the fact that removing duplicates from a sorted list
is much faster than for an arbitrary list.
Ltac2 sort_uniq (cmp : 'a -> 'a -> int) (l : 'a list) : 'a list :=
let rec uniq l :=
match l with
| [] => []
| x1 :: xs
=> match xs with
| [] => x1 :: xs
| x2 :: _
=> match Int.equal (cmp x1 x2) 0 with
| true => uniq xs
| false => x1 :: uniq xs
end
end
end in
uniq (sort cmp l).
let rec uniq l :=
match l with
| [] => []
| x1 :: xs
=> match xs with
| [] => x1 :: xs
| x2 :: _
=> match Int.equal (cmp x1 x2) 0 with
| true => uniq xs
| false => x1 :: uniq xs
end
end
end in
uniq (sort cmp l).
inclusive_range lb ub returns the list lb ; lb+1 ; lb+2 ; ... ; up.
In particular both the lower bound lb and upper bound ub are included.
Ltac2 inclusive_range (lb : int) (ub : int) : int list :=
seq lb 1 (Int.add ub 1).
seq lb 1 (Int.add ub 1).
range lb ub returns the list lb ; lb+1 ; lb+2 ; ... ; up-1.
In particular the lower bound lb is included, whereas the upper bound ub is excluded.
Ltac2 range (lb : int) (ub : int) : int list :=
seq lb 1 ub.
seq lb 1 ub.
concat_rev [x1; ..; xN-1; xN] computes rev xN ++ rev xN-1 ++ .. ++ x1.
Note that x1 is not reversed and appears in its original order.
concat_rev is faster than concat and should be preferred over concat
when the order of items does not matter.
Ltac2 concat_rev (ls : 'a list list) : 'a list :=
let rec go ls acc :=
match ls with
| [] => acc
| l :: ls => go ls (rev_append l acc)
end
in
match ls with
| [] => []
| l :: ls => go ls l
end.
let rec go ls acc :=
match ls with
| [] => acc
| l :: ls => go ls (rev_append l acc)
end
in
match ls with
| [] => []
| l :: ls => go ls l
end.
map_filter f l maps f over l, then removes all elements that are None.
Ltac2 rec map_filter (f : 'a -> 'b option) (l : 'a list) : 'b list :=
match l with
| [] => []
| x :: l =>
match f x with
| Some y => y :: map_filter f l
| None => map_filter f l
end
end.
match l with
| [] => []
| x :: l =>
match f x with
| Some y => y :: map_filter f l
| None => map_filter f l
end
end.