Up  

Functor Logic.Make

module Make: 
functor (L : ParseLocation.S) -> 
functor (I : Id_intf.Logic) -> 
functor (T : Term_intf.Logic  with type location := L.t and type id := I.t) -> 
functor (S : Stmt_intf.Logic  with type location := L.t and type id := I.t and type term := T.t) -> sig .. end
Parameters:
L : ParseLocation.S
I : Id_intf.Logic
T : Term_intf.Logic with type location := L.t and type id := I.t
S : Stmt_intf.Logic with type location := L.t and type id := I.t and type term := T.t 
exception Extension_not_found of string
Raised when trying to find a language given a file extension.

Supported languages


type language =
| Dimacs (*
Dimacs CNF format
*)
| ICNF (*
iCNF format
*)
| Smtlib (*
Smtlib format
*)
| Tptp (*
TPTP format (including THF)
*)
| Zf (*
Zipperposition format
*)
The languages supported by the Logic class.
val enum : (string * language) list
Enumeration of languages together with an appropriate name. Can be used for command-line arguments (for instance, with cmdliner).
val string_of_language : language -> string
String representation of the variant

High-level parsing


val find : ?language:language -> ?dir:string -> string -> string option
Tries and find the given file, using the language specification.
val parse_file : ?language:language -> string -> language * S.t list
Given a filename, parse the file, and return the detected language together with the list of statements parsed.
language : specify a language; overrides auto-detection.
val parse_input : ?language:language ->
       [ `File of string | `Stdin of language ] ->
       language * (unit -> S.t option)
Incremental parsing of either a file (see ), or stdin (with given language).
language : specify a language for parsing, overrides auto-detection and stdin specification.

Mid-level parsing


module type S = Language_intf.S  with type statement := S.t
The type of language modules. 
val of_language : language -> language * string * (module Logic.Make.S)
val of_extension : string -> language * string * (module Logic.Make.S)
These function take as argument either a language, or a filename, and return a triple: Extensions should start with a dot (for instance : ".smt2")
Raises Extension_not_found when the extension is not recognized.