Util (u.2ae07f0414095fe13bd771b09bde6561.logtk.1.5.1.doc.logtk.Logtk.Util)

Some helpers

Various helpers for the provers.

It provides counters for statistics, basic profilers, helper functions, debugging functions…

Time facilities

Sourceval total_time_s : unit -> float

time elapsed since start of program, in seconds

Misc

Sourcemodule Section : sig ... end

Debug section

Sourceval set_debug : int -> unit

Set debug level of Section.root

Sourceval get_debug : unit -> int

Current debug level for Section.root

Sourceval break_on_debug : bool ref

Shall we wait for user input after each debug message?

Source

val debugf : 
  ?section:Section.t ->
  int ->
  ('a, Format.formatter, unit, unit) format4 ->
  ('a -> unit) ->
  unit

Print a debug message, with the given section and verbosity level. The message might be dropped if its level is too high.

Sourceval debug : ?section:Section.t -> int -> string -> unit

Cheap non-formatting version of debugf

Source

val ksprintf_noc : 
  f:(string -> 'a) ->
  ('b, Format.formatter, unit, 'a) format4 ->
  'b

Same as CCFormat.ksprintf, but without colors

Sourceval err_spf : ('b, Format.formatter, unit, string) format4 -> 'b

Version of sprintf that adds a colored "error" prefix

Sourceval warn : string -> unit

Emit warning

Sourceval warnf : ('a, Format.formatter, unit, unit) format4 -> 'a

Emit warning, with formatting

Sourceexception Error of string * string

generalist error that do not really belong elsewhere. Error (where,what) means that error what was raised from where.

Sourceval error : where:string -> string -> 'a

error msg raises Error msg

raises Error
duh

Sourceval errorf : where:string -> ('b, Format.formatter, unit, 'a) format4 -> 'b

Formatting version of error

Sourceval pp_pos : Lexing.position -> string

Sourceval set_memory_limit : int -> unit

Limit the amount of memory available to the process (in MB)

Sourceval set_time_limit : int -> unit

Limit the CPU time available to the process (in seconds)

OCaml Stack

requires ocaml >= 4.01

since 0.8

Sourcemodule Exn : sig ... end

profiling facilities

Sourcetype profiler

Sourceval enable_profiling : bool ref

Enable/disable profiling

Sourceval mk_profiler : string -> profiler

Create a named profiler

Sourceval enter_prof : profiler -> unit

Enter the profiler

Sourceval exit_prof : profiler -> unit

Exit the profiler

Sourceval with_prof : profiler -> ('a -> 'b) -> 'a -> 'b

Runtime statistics

Sourcetype stat

Sourceval mk_stat : string -> stat

Sourceval print_global_stats : comment:string -> unit -> unit

comment prefix

Sourceval incr_stat : stat -> unit

Sourceval add_stat : stat -> int -> unit

Flags as integers

Sourcemodule Flag : sig ... end

Others

Sourceval finally : do_:(unit -> unit) -> (unit -> 'a) -> 'a

finally ~do_ f calls f () and returns its result. If it raises, the same exception is raised; in any case, do_ () is called after f () terminates.

Source

val pp_pair : 
  ?sep:string ->
  'a CCFormat.printer ->
  'b CCFormat.printer ->
  ('a * 'b) CCFormat.printer

Sourceval pp_list : ?sep:string -> 'a CCFormat.printer -> 'a list CCFormat.printer

Print a list without begin/end separators

Sourceval pp_seq : ?sep:string -> 'a CCFormat.printer -> 'a Iter.t CCFormat.printer

Sourceval pp_list0 : ?sep:string -> 'a CCFormat.printer -> 'a list CCFormat.printer

Print a list with a whitespace in front if it's non empty, or does nothing if the list is empty Default separator is " "

Sourceval tstp_needs_escaping : string -> bool

Is this name a proper TSTP identifier, or does it need ' ' around it?

Sourceval pp_str_tstp : string CCFormat.printer

possibly escaping

Sourceval pp_var_tstp : string CCFormat.printer

Sourceval ord_option : 'a CCOrd.t -> 'a option CCOrd.t

Sourceval take_drop_while : ('a -> bool) -> 'a list -> 'a list * 'a list

Sourceval map_product : f:('a -> 'b list list) -> 'a list -> 'b list list

Sourceval seq_map_l : f:('a -> 'b list) -> 'a list -> 'b list Iter.t

Sourceval seq_zipi : 'a Iter.t -> (int * 'a) Iter.t

Sourceval invalid_argf : ('a, Format.formatter, unit, 'b) format4 -> 'a

Sourceval failwithf : ('a, Format.formatter, unit, 'b) format4 -> 'a

Sourcemodule Int_map : CCMap.S with type key = int

Sourcemodule Int_set : CCSet.S with type elt = int

Sourceval escape_dot : string -> string

String escaping for graphviz

File utils

Sourcetype 'a or_error = ('a, string) CCResult.t

Sourceval popen : cmd:string -> input:string -> string or_error

Run the given command cmd with the given input, wait for it to terminate, and return its stdout.