package alt-ergo-lib

  1. Overview
  2. Docs
On This Page
  1. Input method
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.