Module `Lib`

General-purpose library functions

author: Christoph Sticksel

Helper functions

val identity : 'a -> 'a: Identity function.

val print_pass : string -> 'a -> 'a: Prints the first argument and returns the second.

val true_of_unit : unit -> bool: Returns true when given unit.

val false_of_unit : unit -> bool: Returns false when given unit.

val none_of_unit : unit -> 'a option: Returns None when given unit.

val true_of_any : 'a -> bool: Return true

val false_of_any : 'a -> bool: Return false

val mk_dir : string -> unit

Option types

val get : 'a option -> 'a: Return the value of an option type, raise Invalid_argument "get" if the option value is None

val min_option : float option -> float option -> float option: Return the min between two optional floats. Return None if both floats are None.

Integer functions

val string_starts_with : string -> string -> bool: string_starts_with s1 s2 returns true if the first characters of s1 up to the length of s2 are ientical to s2. Return false if s2 is longer than s1.

Integer functions

val safe_hash_interleave : int -> int -> int -> int: safe_hash_interleave h m i compute m * h + i and makes sure that the result does not overflow to a negtive number

List functions

val (@::) : 'a option -> 'a list -> 'a list

Add element to the head of the list if the option value is not None.

The function symbol is right-associative and infix:

Some 1 @:: None @:: Some 2 @:: [3;4]

returns

\[1;2;3;4\]

val list_init : (int -> 'a) -> int -> 'a list: Creates a size-n list equal to f 0; f 1; ... ; f (n-1)

val list_max : 'a list -> 'a: Returns the maximum element of a non-empty list

val list_index : ('a -> bool) -> 'a list -> int: Return the index of the first element that satisfies the predicate p, raise excpetion Not_found if no element satisfies the predicate.

val list_indexes : 'a list -> 'a list -> int list: list_indexes l1 l2 returns the indexes in list l2 of elements in list l1

val list_filter_nth : 'a list -> int list -> 'a list: list_filter_nth l [p1; p2; ...] returns the elements l at positions p1, p2 etc.

val list_extract_nth : 'a list -> int -> 'a * 'a list: Remove and returns the nth element form a list

val chain_list : 'a list -> 'a list list: chain_list [e1; e2; ...] is [[e1; e2]; [e2; e3]; ... ]

val chain_list_p : 'a list -> ('a * 'a) list: chain_list_p [e1; e2; ...] is [(e1, e2); (e2, e3); ... ]

val list_subtract : 'a list -> 'a list -> 'a list: Return a list containing all values in the first list that are not in the second list

val list_uniq : 'a list -> 'a list: From a sorted list return a list with physical duplicates removed

val list_merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list: Merge two sorted lists without physical duplicates to a sorted list without physical duplicates

val list_inter_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list: From two sorted lists without physical duplicates return a sorted list without physical duplicates containing elements in both lists

val list_diff_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list: From two sorted lists without physical duplicates return a sorted list without physical duplicates containing elements in the first but not in the second list

val list_subset_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> bool: For two sorted lists without physical duplicates return true if the first list contains a physically equal element for each element in the second list

val list_join : ('a -> 'a -> bool) -> ('a * 'b) list -> ('a * 'b list) list -> ('a * 'b list) list

Given two ordered association lists with identical keys, push the values of each element of the first association list to the list of elements of the second association list.

The returned association list is in the order of the input lists, the function equal is used to compare keys. Raise Failure "list_join" if the lists are not of identical length and the keys at each element are equal.

val compare_pairs : ('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a * 'b) -> ('a * 'b) -> int: Lexicographic comparison of pairs

val compare_lists : ('a -> 'a -> int) -> 'a list -> 'a list -> int: Lexicographic comparison of lists

Array functions

val array_max : 'a array -> 'a: Returns the maximum element of a non-empty array

Set functions

module IntegerSet : Stdlib.Set.S with type IntegerSet.elt = int: Sets of integers

module IntegerHashtbl : Stdlib.Hashtbl.S with type IntegerHashtbl.key = int: Hashtable of integers

Pretty-printing helpers

val pp_print_arrayi : (Stdlib.Format.formatter -> int -> 'a -> unit) -> (unit, Stdlib.Format.formatter, unit) Stdlib.format -> Stdlib.Format.formatter -> 'a array -> unit

Pretty-print an array with given separator

pp_print_array elem_printer separator formatter array calls, for each index i of the array whose corresponding element is element, elem_printer formatter i element. Between each of these calls it prints the string separator.

In order to get line breaks between the elements, do not use a line feed character \n as separator, this might mess up indentation. Instead wrap the list into a vertical box with the format string @[<v>%a@] and the empty string as separator.

val pp_print_list : (Stdlib.Format.formatter -> 'a -> unit) -> ('b, Stdlib.Format.formatter, unit) Stdlib.format -> Stdlib.Format.formatter -> 'a list -> unit

Pretty-print a list with given separator

pp_print_list p s f l pretty-prints the elements in the list l by calling the pretty-printer p on each, separating the elements by printing the string s.

val pp_print_listi : (Stdlib.Format.formatter -> int -> 'a -> unit) -> ('b, Stdlib.Format.formatter, unit) Stdlib.format -> Stdlib.Format.formatter -> 'a list -> unit

Pretty-print a list with given separator and maintain a counter of elements

See pp_print_list, except that the pretty-printer is passes an zero-based counter for the list's elements as the argument preceding the list element.

val pp_print_list2i : (Stdlib.Format.formatter -> int -> 'a -> 'b -> unit) -> ('c, Stdlib.Format.formatter, unit) Stdlib.format -> Stdlib.Format.formatter -> 'a list -> 'b list -> unit: Pretty-print two lists of the same length with given separator and maintain a counter of their elements.

val pp_print_option : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a option -> unit: Pretty-print an option type

val pp_print_if_not_empty : (unit, Stdlib.Format.formatter, unit) Stdlib.format -> Stdlib.Format.formatter -> 'a list -> unit: Pretty-print if list is not empty

val string_of_t : (Stdlib.Format.formatter -> 'a -> unit) -> 'a -> string: Pretty-print into a string

val width_of_string : string -> int: Return the width of the string, meaning the wisth of it's longest line

val paren_string_of_string_list : string list -> string: Return the strings as a parenthesized and space separated list

val escape_json_string : string -> string
val escape_xml_string : string -> string

Logging

Levels of log messages

L_fatal A severe error that will lead to an immediate abort

L_error An error event that might still allow to continue

L_warn A potentially harmful situation

L_note An important note (soft warning)

L_info An informational message that highlight progress at a coarse-grained level

L_debug A fine-grained informational event that is useful for debugging but not for an end user

L_trace A finer-grained informational event than L_debug

val default_log_level : log_level: Default log level.

val int_of_log_level : log_level -> int: Associate an integer with each level to induce a total ordering

val log_level_of_int : int -> log_level
val string_of_log_level : log_level -> string
val log_ppf : Stdlib.Format.formatter Stdlib.ref: Current formatter for output

val log_to_file : string -> unit: Ouputs all log messages to the given file

val log_to_stdout : unit -> unit: Write all log messages to the standard output

val set_log_level : log_level -> unit

Set log level

Only output messages of levels with equal or higher priority

val get_log_level : unit -> log_level: Gets the log level.

val output_on_level : log_level -> bool: Return true if given log level is of higher or equal priority than current log level?

val ignore_or_fprintf : log_level -> Stdlib.Format.formatter -> ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a: Return Format.fprintf if level is is of higher or equal priority than current log level, otherwise return Format.ifprintf

System functions

val pp_print_banner : Stdlib.Format.formatter -> unit -> unit: Output the banner on the formatter

val pp_print_version : Stdlib.Format.formatter -> unit: Output the version number on the formatter

type kind_module = [ | `IC3 | `BMC | `IND | `IND2 | `INVGEN | `INVGENOS | `INVGENINT | `INVGENINTOS | `INVGENREAL | `INVGENREALOS | `C2I | `Interpreter | `Supervisor | `Parser | `Certif | `MCS ]: Kind modules

exception TimeoutWall: Wallclock timeout

exception TimeoutVirtual: CPU timeout

exception Signal of int: System signal caught

val string_of_signal : int -> string: String representation of signal

val pp_print_process_status : Stdlib.Format.formatter -> Unix.process_status -> unit: Pretty-print the termination status of a process

val exception_on_signal : int -> 'a: Raise exception on signal

val pp_print_kind_module : Stdlib.Format.formatter -> kind_module -> unit: Pretty-print the name of a kind module

val string_of_kind_module : kind_module -> string: String representation of a process type

val int_of_kind_module : kind_module -> int: String representation of a process type

val short_name_of_kind_module : kind_module -> string: Return a short representation of kind module

val kind_module_of_string : string -> kind_module: Kind module of a string

val minisleep : float -> unit: Sleep for seconds, resolution is in ms

val find_on_path : string -> string: Return full path to executable, search PATH environment variable and current working directory

val find_file : string -> string list -> string option: Return full path to file if the file is found in the list of directories, or None otherwise *

Positions in the input

type position: A position in the input

val dummy_pos : position: Dummy position different from any valid position

val compare_pos : position -> position -> int: Comparision on positions

val is_dummy_pos : position -> bool: Return true if the position is not a valid position in the input

val pp_print_position : Stdlib.Format.formatter -> position -> unit: Pretty-print a position

val pp_print_pos : Stdlib.Format.formatter -> position -> unit: Pretty-print a position in a concise way

val file_row_col_of_pos : position -> string * int * int: Return the file, line and column of a position; fail with Invalid_argument "file_row_col_of_pos" if the position is a dummy position

val pos_of_file_row_col : (string * int * int) -> position: Inverse of file_row_col_of_pos

val position_of_lexing : Stdlib.Lexing.position -> position: Convert a position of the lexer to a position

val print_backtrace : Stdlib.Format.formatter -> Stdlib.Printexc.raw_backtrace -> unit: Pretty print a backtrace

val extract_scope_name : string -> string * string list: Extract scope from a concatenated name

val create_dir : string -> unit: Create a directory if it does not already exists.

val file_copy : string -> string -> unit: Copying file: file_copy from to copies file from to file to

val files_cat_open : ?⁠add_prefix:(Stdlib.Format.formatter -> unit) -> string list -> string -> Unix.file_descr
val syscall : string -> string: Get standard output of command

val set_liberal_gc : unit -> unit: Changes garbage collector parameters limit its effect

val reset_gc_params : unit -> unit: Reset the parameters of the GC to its default values. Call after set_liberal_gc.

module Paths : sig ... end: Paths Kind 2 can write some files. Factored to avoid clashes.

module ReservedIds : sig ... end: Reserved identifiers.

module ExitCodes : sig ... end: Exit codes.

module Names : sig ... end: File names.