Module AltErgoLib.Input

Typed input

This module defines an abstraction layer over the parsing and typechecking of input formulas. The goal is to be able to use different parsing and/or typechecking engines (e.g. the legacy typechecker, psmt2, or dolmen). To do so, an input method actually generates the typed representation of the input.

Input method

exception Method_not_registered of string

Exceptions raised when trying to lookup an input method that has not been registered.

module type S = sig ... end

This modules defines an input method. Input methods are responsible for two things: parsing and typechceking either an input file (possibly with some preludes files), or arbitrary terms. This last functionality is currently only used in the GUI.

val register : string -> (module S) -> unit

Register a new input method.

val find : string -> (module S)

Find an input method by name.