package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.Util

Some helpers

Various helpers for the provers.

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

Time facilities

val total_time_s : unit -> float

time elapsed since start of program, in seconds

val get_time_mon_us : unit -> float

A monotonic clock, in microseconds

Misc

module Section : sig ... end

Debug section

val set_debug : int -> unit

Set debug level of Section.root

val get_debug : unit -> int

Current debug level for Section.root

val break_on_debug : bool ref

Shall we wait for user input after each debug message?

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.

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

Cheap non-formatting version of debugf

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

Same as CCFormat.ksprintf, but without colors

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

Version of sprintf that adds a colored "error" prefix

val warn : string -> unit

Emit warning

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

Emit warning, with formatting

exception Error of string * string

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

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

error msg raises Error msg

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

Formatting version of error

val pp_pos : Lexing.position -> string
val set_memory_limit : int -> unit

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

val set_time_limit : int -> unit

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

OCaml Stack

requires ocaml >= 4.01

  • since 0.8
module Exn : sig ... end

Runtime statistics

type stat
val mk_stat : string -> stat
val print_global_stats : comment:string -> unit -> unit

comment prefix

val incr_stat : stat -> unit
val add_stat : stat -> int -> unit
val pp_stat : Format.formatter -> stat -> unit

Flags as integers

module Flag : sig ... end

Others

val 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.

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

Print a list without begin/end separators

val pp_seq : ?sep:string -> 'a CCFormat.printer -> 'a Seq.t CCFormat.printer
val pp_iter : ?sep:string -> 'a CCFormat.printer -> 'a Iter.t CCFormat.printer
val 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 " "

val tstp_needs_escaping : string -> bool

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

val pp_str_tstp : string CCFormat.printer

possibly escaping

val pp_var_tstp : string CCFormat.printer
val ord_option : 'a CCOrd.t -> 'a option CCOrd.t
val take_drop_while : ('a -> bool) -> 'a list -> 'a list * 'a list
val map_product : f:('a -> 'b list list) -> 'a list -> 'b list list
val seq_map_l : f:('a -> 'b list) -> 'a list -> 'b list Iter.t
val seq_zipi : 'a Iter.t -> (int * 'a) Iter.t
val invalid_argf : ('a, Format.formatter, unit, 'b) format4 -> 'a
val failwithf : ('a, Format.formatter, unit, 'b) format4 -> 'a
module Int_map : CCMap.S with type key = int
module Int_set : CCSet.S with type elt = int
val escape_dot : string -> string

String escaping for graphviz

File utils

type 'a or_error = ('a, string) CCResult.t
val 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.