Module `Logtk_parsers.Util_tptp`

module A = Ast_tptp

type 'a or_error = ('a, string) CCResult.t
type untyped = Logtk.STerm.t
type typed = Logtk.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 -> Stdlib.Lexing.lexbuf -> untyped A.t Iter.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 Iter.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 find_file for included files.

parameter parse_cache: used to avoid including the same file twice, if recursive=true

returns: an error-wrapped sequence of declarations.

val print_into : 't CCFormat.printer -> 't A.t Iter.t CCFormat.printer
val print_into_file : 't CCFormat.printer -> string -> 't A.t Iter.t -> unit
val has_includes : _ A.t Iter.t -> bool: Check whether some include declaration can be found in the sequence

Bridge to UntypedAST

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

raises Error: if there are remaining includes

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

raises Error: if the AST contains Data