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 -> floattime elapsed since start of program, in seconds
Misc
val set_debug : int -> unitSet debug level of Section.root
val get_debug : unit -> intCurrent debug level for Section.root
val break_on_debug : bool Stdlib.refShall we wait for user input after each debug message?
val debugf :
?section:Section.t ->
int ->
('a, Stdlib.Format.formatter, unit, unit) Stdlib.format4 ->
('a -> unit) ->
unitPrint 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 -> unitCheap non-formatting version of debugf
val ksprintf_noc :
f:(string -> 'a) ->
('b, Stdlib.Format.formatter, unit, 'a) Stdlib.format4 ->
'bSame as CCFormat.ksprintf, but without colors
val err_spf : ('b, Stdlib.Format.formatter, unit, string) Stdlib.format4 -> 'bVersion of sprintf that adds a colored "error" prefix
val warn : string -> unitval warnf : ('a, Stdlib.Format.formatter, unit, unit) Stdlib.format4 -> 'aEmit warning, with formatting
exception Error of string * stringgeneralist error that do not really belong elsewhere. Error (where,what) means that error what was raised from where.
val error : where:string -> string -> 'aerror msg raises Error msg
val errorf :
where:string ->
('b, Stdlib.Format.formatter, unit, 'a) Stdlib.format4 ->
'bFormatting version of error
val pp_pos : Stdlib.Lexing.position -> stringval set_memory_limit : int -> unitLimit the amount of memory available to the process (in MB)
val set_time_limit : int -> unitLimit the CPU time available to the process (in seconds)
OCaml Stack
requires ocaml >= 4.01
profiling facilities
val enable_profiling : bool Stdlib.refval with_prof : profiler -> ('a -> 'b) -> 'a -> 'bRuntime statistics
val mk_stat : string -> statval print_global_stats : comment:string -> unit -> unitval incr_stat : stat -> unitval add_stat : stat -> int -> unitFlags as integers
module Flag : sig ... endOthers
val finally : do_:(unit -> unit) -> (unit -> 'a) -> 'afinally ~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.printerval pp_list : ?sep:string -> 'a CCFormat.printer -> 'a list CCFormat.printerPrint a list without begin/end separators
val pp_seq : ?sep:string -> 'a CCFormat.printer -> 'a Iter.t CCFormat.printerval pp_list0 : ?sep:string -> 'a CCFormat.printer -> 'a list CCFormat.printerPrint 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 -> boolIs this name a proper TSTP identifier, or does it need ' ' around it?
val pp_str_tstp : string CCFormat.printerval pp_var_tstp : string CCFormat.printerval ord_option : 'a CCOrd.t -> 'a option CCOrd.tval take_drop_while : ('a -> bool) -> 'a list -> 'a list * 'a listval map_product : f:('a -> 'b list list) -> 'a list -> 'b list listval seq_map_l : f:('a -> 'b list) -> 'a list -> 'b list Iter.tval seq_zipi : 'a Iter.t -> (int * 'a) Iter.tval invalid_argf : ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'aval failwithf : ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'amodule Int_map : CCMap.S with type key = intmodule Int_set : CCSet.S with type elt = intval escape_dot : string -> stringString escaping for graphviz
File utils
type 'a or_error = ('a, string) CCResult.tval popen : cmd:string -> input:string -> string or_errorRun the given command cmd with the given input, wait for it to terminate, and return its stdout.