package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install

Dune Dependency

Authors

Maintainers

Sources

lambdapi-2.5.0.tbz
sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704

doc/lambdapi.common/Common/Error/index.html

Module Common.ErrorSource

Warnings and errors.

err_fmt warning/error output formatter.

Sourceval no_wrn : bool ref

no_wrn disables warnings when set to true.

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

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

Sourceexception 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).

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

Sourceval 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).

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

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

OCaml

Innovation. Community. Security.