Various helpers for the provers.
It provides counters for statistics, basic profilers, helper functions, debugging functions…
module Section : sig ... endDebug section
val break_on_debug : bool refShall we wait for user input after each debug message?
val debugf :
?section:Section.t ->
int ->
('a, Format.formatter, unit, unit) 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 ksprintf_noc :
f:(string -> 'a) ->
('b, Format.formatter, unit, 'a) format4 ->
'bSame as CCFormat.ksprintf, but without colors
val err_spf : ('b, Format.formatter, unit, string) format4 -> 'bVersion of sprintf that adds a colored "error" prefix
val warnf : ('a, Format.formatter, unit, unit) format4 -> 'aEmit warning, with formatting
generalist error that do not really belong elsewhere. Error (where,what) means that error what was raised from where.
val errorf : where:string -> ('b, Format.formatter, unit, 'a) format4 -> 'bFormatting version of error
val pp_pos : Lexing.position -> stringrequires ocaml >= 4.01
module Exn : sig ... endval enable_profiling : bool refEnable/disable profiling
val mk_profiler : string -> profilerCreate a named profiler
val enter_prof : profiler -> unitEnter the profiler
val exit_prof : profiler -> unitExit the profiler
val with_prof : profiler -> ('a -> 'b) -> 'a -> 'bval mk_stat : string -> statval incr_stat : stat -> unitval add_stat : stat -> int -> unitmodule Flag : sig ... endfinally ~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 " "
Is this name a proper TSTP identifier, or does it need ' ' around it?
val pp_str_tstp : string CCFormat.printerpossibly escaping
val pp_var_tstp : string CCFormat.printerval seq_map_l : f:('a -> 'b list) -> 'a list -> 'b list Iter.tval invalid_argf : ('a, Format.formatter, unit, 'b) format4 -> 'aval failwithf : ('a, Format.formatter, unit, 'b) format4 -> 'atype '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.