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.
Exceptions raised when trying to lookup an input method that has not been registered.
module type S = sig ... endThis 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) -> unitRegister a new input method.
val find : string -> (module S)Find an input method by name.
Method_not_registered if the name is not registered.