Module Tools

module Tools: sig  end

Collection of useful functions used throughout ICS.
Author(s): Jean-Christophe Filliatre, Harald Ruess

Global variables

val linenumber : int Pervasives.ref

linenumber used by lexer and parser.

val profiling : bool Pervasives.ref

Exit functions

val add_at_exit : (unit -> unit) -> unit

Procedures f without parameters can be registered as exit procedures by add_to_exit f. Exit procedures can, for example be used for displaying statistics after running ICS.

Parameters:

f : unit -> unit

val do_at_exit : unit -> unit

Procedures f registered by Tools.add_at_exit are called by do_at_exit(). The order in which these functions are called is unspecified.

Parameters:

() : unit

Reset functions

val add_at_reset : (unit -> unit) -> unit

add_to_reset f registers f as a reset procedure

Parameters:

f : unit -> unit

val do_at_reset : unit -> unit

do_at_reset(). which are then called, one-by-one, by do_at_reset().

Parameters:

() : unit

Timings

val utime : ('a -> 'b) -> 'a -> 'b * float

utime f a returns not only the result of applying f to a but also the time required to compute the function.

Parameters:

f	:	`'a -> 'b`
x	:	`'a`

Profiling

val profile : string -> ('a -> 'b) -> 'a -> 'b

profile str f profiles function f, and registers an exit function which outputs the number of calls of this function, and the total time spent in this function; the argument str is usually just the name of the function.

Parameters:

str	:	`string`
f	:	`'a -> 'b`
a	:	`'a`

Accumulation of side effects

val acc1 : 'a list Pervasives.ref -> ('b -> 'c * 'a) -> 'b -> 'c

acc1 acc f b calls f b to obtain (c, a). Now, a is consed to acc as a side effect and the result c is returned.

Parameters:

acc	:	`'a list Pervasives.ref`
f	:	`'b -> 'c * 'a`
a	:	`'b`

val acc2 : 'a list Pervasives.ref -> ('b -> 'c -> 'd * 'a) -> 'b -> 'c -> 'd

acc2 acc f b1 b2 calls f b1 b2 to obtain (c, a). Now, a is consed to acc as a side effect and the result c is returned.

Parameters:

acc	:	`'a list Pervasives.ref`
f	:	`'b -> 'c -> 'd * 'a`
a1	:	`'b`
a2	:	`'c`

val accb : 'a list Pervasives.ref -> ('b -> 'a option) -> 'b -> bool

accb acc p b calls p b. If the result of evaluating p b is of the form Some(a), then a is consed to acc as a side effect and the result true is returned. Otherwise, if p b is None, there is no side effect, and false is returned.

Parameters:

acc	:	`'a list Pervasives.ref`
p	:	`'b -> 'a option`
a	:	`'b`