Module Util_tptp

module Util_tptp: sig .. end

Utils related to TPTP

module A: Ast_tptp

type 'a or_error = [ `Error of string | `Ok of 'a ]

type untyped = Libzipperposition.STerm.t

type typed = Libzipperposition.TypedSTerm.t

exception Error of string

Printing/Parsing

type parse_cache

Cache that remembers the set of files that have been parsed so far

val create_parse_cache : unit -> parse_cache

val find_file : string -> string -> string option

find_file name dir looks for a file with the given name, recursively, in dir, or in its parent dir recursively. It also looks in the "TPTP" environment variable.

val parse_lexbuf : ?names:A.name list ->
       Lexing.lexbuf -> untyped A.t Sequence.t or_error

Given a lexbuf, try to parse its content into a sequence of untyped declarations

val parse_file : ?cache:parse_cache ->
       recursive:bool ->
       string -> untyped A.t Sequence.t or_error

Parsing a TPTP file is here presented with a recursive option that, if true, will make "include" directives to be recursively parsed. It uses Util_tptp.find_file for included files.
Returns an error-wrapped sequence of declarations.

Printing is simpler, because it does not involve includes.

val print_into : 't CCFormat.printer -> 't A.t Sequence.t CCFormat.printer

val print_into_file : 't CCFormat.printer -> string -> 't A.t Sequence.t -> unit

val has_includes : 'a A.t Sequence.t -> bool

Check whether some include declaration can be found in the sequence

Bridge to UntypedAST

val to_ast : untyped A.t -> Libzipperposition.UntypedAST.statement

Raises Error if there are remaining includes

val of_ast : Libzipperposition.UntypedAST.statement -> untyped A.t

Raises Error if the AST contains Data