package lambdapi

  1. Overview
  2. Docs

Warnings and errors.

val err_fmt : Format.formatter ref

err_fmt warning/error output formatter.

val no_wrn : bool ref

no_wrn disables warnings when set to true.

val wrn : Pos.popt -> 'a Lplib.Base.outfmt -> 'a

wrn popt fmt prints a yellow warning message with Format format fmt. Note that the output buffer is flushed by the function, and that output is prefixed with the position popt if given. A newline is automatically put at the end of the message as well.

val with_no_wrn : ('a -> 'b) -> 'a -> 'b

with_no_wrn f x disables warnings before executing f x and then restores the initial state of warnings. The result of f x is returned.

exception Fatal of Pos.popt option * string

Exception raised in case of failure. Note that we use an optional optional source position. None is used on errors that are independant from source code position (e.g., errors related to command-line arguments parsing). In cases where positions are expected Some None may be used to indicate the abscence of a position. This may happen when terms are generated (e.g., by a form of desugaring).

val fatal_msg : 'a Lplib.Base.outfmt -> 'a

fatal_str fmt may be called an arbitrary number of times to build up the error message of the fatal or fatal_no_pos functions prior to calling them. Note that the messages are stored in a buffer that is flushed by the fatal or fatal_no_pos function. Hence, they must be called.

val fatal : Pos.popt -> ('a, 'b) Lplib.Base.koutfmt -> 'a

fatal popt fmt raises the Fatal(popt,msg) exception, in which msg is built from the format fmt (provided the necessary arguments).

val fatal_no_pos : ('a, 'b) Lplib.Base.koutfmt -> 'a

fatal_no_pos fmt is similar to fatal _ fmt, but it is used to raise an error that has no precise attached source code position.

val handle_exceptions : (unit -> unit) -> unit

handle_exceptions f runs f () in an exception handler and handles both expected and unexpected exceptions by displaying a graceful error message. In case of an error, the program is (irrecoverably) stopped with exit code 1 (indicating failure). Hence, handle_exceptions should only be called by the main program logic, not by the internals.