Frama-C:
Plug-ins:
Libraries:

Frama-C API - List

Extension of OCaml's Stdlib.List module. @see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

  • since 31.0-Gallium

Monad

include Monad.S_with_product with type 'a t = 'a list
val return : 'a -> 'a list
val bind : ('a -> 'b list) -> 'a list -> 'b list
val product : 'a list -> 'b list -> ('a * 'b) list
module Bool : sig ... end
module Option : sig ... end
module List : sig ... end
module Operators : sig ... end
include module type of Stdlib.List
type !'a t = 'a list =
  1. | []
  2. | :: of 'a * 'a list
val length : 'a list -> int
val compare_lengths : 'a list -> 'b list -> int
val compare_length_with : 'a list -> int -> int
val cons : 'a -> 'a list -> 'a list
val hd : 'a list -> 'a
val tl : 'a list -> 'a list
val nth : 'a list -> int -> 'a
val nth_opt : 'a list -> int -> 'a option
val rev : 'a list -> 'a list
val init : int -> (int -> 'a) -> 'a list
val append : 'a list -> 'a list -> 'a list
val rev_append : 'a list -> 'a list -> 'a list
val concat : 'a list list -> 'a list
val flatten : 'a list list -> 'a list
val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
val iter : ('a -> unit) -> 'a list -> unit
val iteri : (int -> 'a -> unit) -> 'a list -> unit
val map : ('a -> 'b) -> 'a list -> 'b list
val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
val rev_map : ('a -> 'b) -> 'a list -> 'b list
val filter_map : ('a -> 'b option) -> 'a list -> 'b list
val concat_map : ('a -> 'b list) -> 'a list -> 'b list
val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val iter2 : ('a -> 'b -> unit) -> 'a list -> 'b list -> unit
val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val rev_map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
val fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
val for_all : ('a -> bool) -> 'a list -> bool
val exists : ('a -> bool) -> 'a list -> bool
val for_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val exists2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val mem : 'a -> 'a list -> bool
val memq : 'a -> 'a list -> bool
val find : ('a -> bool) -> 'a list -> 'a
val find_opt : ('a -> bool) -> 'a list -> 'a option
val find_map : ('a -> 'b option) -> 'a list -> 'b option
val filter : ('a -> bool) -> 'a list -> 'a list
val find_all : ('a -> bool) -> 'a list -> 'a list
val filteri : (int -> 'a -> bool) -> 'a list -> 'a list
val partition : ('a -> bool) -> 'a list -> 'a list * 'a list
val partition_map : ('a -> ('b, 'c) Stdlib.Either.t) -> 'a list -> 'b list * 'c list
val assoc : 'a -> ('a * 'b) list -> 'b
val assoc_opt : 'a -> ('a * 'b) list -> 'b option
val assq : 'a -> ('a * 'b) list -> 'b
val assq_opt : 'a -> ('a * 'b) list -> 'b option
val mem_assoc : 'a -> ('a * 'b) list -> bool
val mem_assq : 'a -> ('a * 'b) list -> bool
val remove_assoc : 'a -> ('a * 'b) list -> ('a * 'b) list
val remove_assq : 'a -> ('a * 'b) list -> ('a * 'b) list
val split : ('a * 'b) list -> 'a list * 'b list
val combine : 'a list -> 'b list -> ('a * 'b) list
val sort : ('a -> 'a -> int) -> 'a list -> 'a list
val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list
val fast_sort : ('a -> 'a -> int) -> 'a list -> 'a list
val sort_uniq : ('a -> 'a -> int) -> 'a list -> 'a list
val merge : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
val to_seq : 'a list -> 'a Stdlib.Seq.t
val of_seq : 'a Stdlib.Seq.t -> 'a list

Datatype functions

val hash : ('a -> int) -> 'a t -> int

Compute a hash for the list given a hash for the elements.

  • since Frama-C+dev
val pretty : ?format:(Pretty.tformatter -> unit) Pretty.format -> ?item:('a Pretty.aformatter -> 'a -> unit) Pretty.format -> ?sep:unit Pretty.format -> ?last:unit Pretty.format -> ?empty:unit Pretty.format -> (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a t -> unit

Pretty prints a list given a printer for the elements.

  • parameter format

    defaults to " %t "

  • parameter item

    defaults to "%a"

  • parameter sep

    defaults to ";@ "

  • parameter last

    defaults to sep

  • parameter empty

    defaults to ""

  • since Frama-C+dev
val pretty_text : ?format:(Pretty.tformatter -> unit) Pretty.format -> ?item:('a Pretty.aformatter -> 'a -> unit) Pretty.format -> ?sep:unit Pretty.format -> ?last:unit Pretty.format -> ?empty:unit Pretty.format -> (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a t -> unit

Pretty prints the list as a user readable text.

  • parameter format

    defaults to "%t"

  • parameter item

    defaults to "%a"

  • parameter sep

    defaults to ",@ "

  • parameter last

    defaults to "@ and@ "

  • parameter empty

    defaults to "<empty>"

  • since Frama-C+dev

Iterators

val find_index : ('a -> bool) -> 'a list -> int option

Returns the index (starting at 0) of the first element verifying the condition. Appears in Ocaml 5.1.

  • since Frama-C+dev
val mapi2 : (int -> 'a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list

Same as Stdlib.List.map2 but gives the index of the current element to f

  • since Frama-C+dev
val map_no_copy : ('a -> 'a) -> 'a list -> 'a list

Same as Stdlib.List.map but avoid creating a copy of the list's tail if the mapped function returns its argument (tested through physical equality).

  • since Frama-C+dev
val concat_map_no_copy : ('a -> 'a list) -> 'a list -> 'a list

Same as Stdlib.List.concat_map but avoid creating a copy of the list's tail if the mapped function returns a singleton list with its argument (tested through physical equality).

  • since Frama-C+dev

Accessors

val as_singleton : 'a list -> 'a

returns the unique element of a singleton list.

  • raises Invalid_argument

    on a non singleton list.

  • since Frama-C+dev
val last : 'a list -> 'a

returns the last element of a list.

  • raises Invalid_argument

    on an empty list

  • since Frama-C+dev
val take : int -> 'a list -> 'a list

take n l returns the first n elements of the list. Tail recursive. It returns an empty list if n is nonpositive and the whole list if n is greater than List.length l. This function is introduced in OCaml 5.3 and is made available here until OCaml 5.4 is the minimal supported version. (The 5.3 version is raising exceptions on negative n values) It is equivalent to slice ~last:n l.

  • since Frama-C+dev
val drop : int -> 'a list -> 'a list

drop n l returns the list without the first n elements. It returns the whole list if n is nonpositive and an empty list if n is greater than List.length l. This function is introduced in OCaml 5.3 and is made available here until OCaml 5.4 is the minimal supported version. (The 5.3 version is raising exceptions on negative n values) It is equivalent to slice ~first:n l.

  • since Frama-C+dev
val break : int -> 'a list -> 'a list * 'a list

break n l returns a couple of the list of the first n elements and the list of the remaining elements. If n is smaller than 0 (resp. greater than the list length) then ([], l) is returned (resp. (l, [])). It is equivalent to (take n l, drop n l).

  • since Frama-C+dev
val slice : ?first:int -> ?last:int -> 'a list -> 'a list

slice ?first ?last l is equivalent to Python's slice operator (lfirst:last): returns the range of the list between first (inclusive) and last (exclusive), starting from 0. If omitted, first defaults to 0 and last to List.length l. Negative indices are allowed, and count from the end of the list. slice never raises exceptions: out-of-bounds arguments are clipped, and inverted ranges result in empty lists.

  • since Frama-C+dev

Mutators

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

replace cmp x l replaces the first element y of l such that cmp x y is true by x. If no such element exists, x is added at the tail of l.

  • since Frama-C+dev

Product of lists

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

product_map f l1 l2 applies f to all the pairs of an elt of l1 and an element of l2.

  • since Frama-C+dev
val product_fold : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a

product_fold f acc l1 l2 is similar to fold_left f acc l12 with l12 the list of all pairs of an elt of l1 and an elt of l2

  • since Frama-C+dev

Conversion

val to_option : 'a list -> 'a option

converts a list with 0 or 1 element into an option.

  • raises Invalid_argument

    on lists with more than one argument

  • since Frama-C+dev

Combinations

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

combinations k l computes the combinations of k elements from list l. E.g. combinations 2 [1;2;3;4] = [[1;2];[1;3];[1;4];[2;3];[2;4];[3;4]]. This function preserves the order of the elements in l when computing the sublists. l should not contain duplicates.

  • since Frama-C+dev