module A = Ast_tptptype 'a or_error = ('a, string) CCResult.ttype untyped = Logtk.STerm.ttype typed = Logtk.TypedSTerm.tval enable_def_as_rewrite : bool refval create_parse_cache : unit -> parse_cachefind_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.
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_errorParsing 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.
used to avoid including the same file twice, if recursive=true
an error-wrapped sequence of declarations.
Printing is simpler, because it does not involve includes.
val print_into : 't CCFormat.printer -> 't A.t Iter.t CCFormat.printerval print_into_file : 't CCFormat.printer -> string -> 't A.t Iter.t -> unitCheck whether some include declaration can be found in the sequence
val to_ast : untyped A.t -> Logtk.UntypedAST.statementError if there are remaining includes
val of_ast : Logtk.UntypedAST.statement -> untyped A.tError if the AST contains Data