Frama-C:
Plug-ins:
Libraries:

Frama-C API - Make

Parameters

module D : DATA

Signature

type t
exception Empty
val create : unit -> t

Create a new empty stack.

val singleton : D.t -> t

Create a new qstack with a single element.

  • since Boron-20100401
val is_empty : t -> bool

Test whether the stack is empty or not.

val clear : t -> unit

Remove all the elements of a stack.

val add : D.t -> t -> unit

Add at the beginning of the stack. Complexity: O(1).

val add_at_end : D.t -> t -> unit

Add at the end of the stack. Complexity: O(1).

val top : t -> D.t

Return the top element of the stack. Raise Empty if the stack is empty. Complexity: amortized O(1).

val mem : D.t -> t -> bool

Return true if the data exists in the stack and false otherwise. Complexity: O(n).

val filter : (D.t -> bool) -> t -> D.t list

Return all data of the stack satisfying the specified predicate. The order of the data in the input stack is preserved. Not tail recursive.

val find : (D.t -> bool) -> t -> D.t

Return the first data of the stack satisfying the specified predicate.

  • raises Not_found

    if there is no such data in the stack

val remove : D.t -> t -> unit

Remove an element from the stack. Complexity: O(n).

val move_at_top : D.t -> t -> unit

Move the element x at the top of the stack s. Complexity: O(n).

  • raises Invalid_argument

    if not (mem x s).

val move_at_end : D.t -> t -> unit

Move the element x at the end of the stack s. Complexity: O(n).

  • raises Invalid_argument

    if not (mem x s).

  • since Beryllium-20090901
val iter : (D.t -> unit) -> t -> unit

Iter on all the elements from the top to the end of the stack. Not tail recursive.

val map : (D.t -> D.t) -> t -> unit

Replace in-place all the elements of the stack by mapping the old one. Not tail recursive.

  • since Beryllium-20090901
val fold : ('a -> D.t -> 'a) -> 'a -> t -> 'a

Fold on all the elements from the top to the end of the stack. Not tail recursive.

val nth : int -> t -> D.t
  • returns

    the n-th element of the stack, if any.

  • raises Invalid_argument

    if there is not enough element in the stack.

  • since Beryllium-20090901
val length : t -> int
  • returns

    the length of the stack

  • since Beryllium-20090901
val idx : D.t -> t -> int
  • returns

    the index of the element in the stack

  • raises Not_found

    if the element is not in the stack This function is not tail recursive

  • since Beryllium-20090901