gillian » Gillian » Utils » List_utils

Module Utils.List_utils

val cross_product : 'a list -> 'b list -> ('a -> 'b -> 'c) -> 'c list

Cross product of two lists, l1 and l2, combining its elements with function f

If l1 is of size n and l2 of size m, the cross product is of size n * m

val remove_duplicates : 'a list -> 'a list

Uses Stdlib.compare to produce a list with duplicate elements removed

The resulting list will also be sorted.

val intersect : 'a list -> 'a list -> 'a list

Gives the intersection of two lists

This uses the polymorphic =

val list_product : 'a list list -> 'a list list

Gives the cross-product of a 2D list

A 2D list of size x * y will give a product of size x ^ y

val right_combine : 'a list -> 'b list -> ('a * 'b) list

The same as List.combine, but allows the first list to be longer than the second

val get_list_somes : 'a option list -> 'a list

Filters Nones from a list while unwrapping the Somes

val split_at : 'a list -> int -> 'a list * 'a list

Splits a list at a specified index

val flaky_map : ('a -> 'b option) -> 'a list -> 'b list option

Similar to List.filter_map, but returns None if, for any element x, f x = None

val list_sub : 'a list -> int -> int -> 'a list option

Returns a sublist using an offset and length

Returns None if the list is too short

val make : int -> 'a -> 'a list

Makes a list of a repeated element

val index_of : 'a -> 'a list -> int option

Gives the index of an element in a list

Uses polymorphic =, and returns None if not found

val nth_or_size : 'a list -> int -> ('a, int) Stdlib.Either.t

Returns Left v if v is the nth element of lst or Right sz if the list is too short and is of size sz. Fails if provided a negative n.

val starts_with : 'a list -> 'a list -> bool

Tests if a list starts with another

Uses polymorphic =

val ends_with : 'a list -> 'a list -> bool

Tests if a list ends with another

Uses polymorphic =

val pop_where : ('a -> bool) -> 'a list -> 'a option * 'a list

Returns the list without the first element that matches the predicate, and the removed element if it exists

val pop_map : ('a -> 'b option) -> 'a list -> ('b * 'a list) option

val hd_tl : 'a list -> 'a option * 'a list

Splits a list into head and tail

Returns (None, []) if the list is empty

val hd_opt : 'a list -> 'a option

Option-returning version of List.hd

val tl_opt : 'a list -> 'a option

Option-returning version of List.tl

val cons_opt : 'a option -> 'a list -> 'a list

Prepends an element if it is Some

val map_results :
  ('a -> ('b, 'c) Stdlib.result) ->
  'a list ->
  ('b list, 'c) Stdlib.result

Similar to flaky_map, but with Results, giving the first error if one exists

val iter_results :
  ('a -> (unit, 'b) Stdlib.result) ->
  'a list ->
  (unit, 'b) Stdlib.result

val for_alli : (int -> 'a -> bool) -> 'a list -> bool

val at_least_two : ('a -> bool) -> 'a list -> bool

val last : 'a list -> 'a option

val filter_mapi : (int -> 'a -> 'b option) -> 'a list -> 'b list

val get_and_remove_nth : int -> 'a list -> 'a option * 'a list

val map_head : ('a -> 'a) -> 'a list -> 'a list

val map_last : ('a -> 'a) -> 'a list -> 'a list

val assoc_replace : 'a -> 'b -> ('a * 'b) list -> ('a * 'b) list

val drop : int -> 'a list -> 'a list