package logtk

You can search for identifiers within the package.

in-package search v0.2.0

Core types and algorithms for logic

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

S

Simon Cruanes

Maintainers

S

simon.cruanes.2007@m4x.org

Sources

1.5.1.tar.gz

md5=cc320f66f10555c54822da624419e003

sha512=f8d5f7a5ae790bf0388d74261673803cf375f91f92f7b413b70db1ce5841ef55343a208f98727c8551d66f1840ab892f1c0c943a34861d14d79ce469b235a2f2

doc/logtk.parsers/Logtk_parsers/Util_tptp/index.html

Module `Logtk_parsers.Util_tptp`Source

Sourcemodule A = Ast_tptp

Sourcetype 'a or_error = ('a, string) CCResult.t

Sourcetype untyped = Logtk.STerm.t

Sourcetype typed = Logtk.TypedSTerm.t

Sourceexception Error of string

Printing/Parsing

Sourcetype parse_cache

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

Sourceval create_parse_cache : unit -> parse_cache

Sourceval 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.

Source

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

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

Source

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.

Printing is simpler, because it does not involve includes.

Sourceval print_into : 't CCFormat.printer -> 't A.t Iter.t CCFormat.printer

Sourceval print_into_file : 't CCFormat.printer -> string -> 't A.t Iter.t -> unit

Sourceval has_includes : _ A.t Iter.t -> bool

Check whether some include declaration can be found in the sequence

Bridge to UntypedAST

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

raises Error
if there are remaining includes

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

raises Error
if the AST contains Data

On This Page

Utils related to TPTP
1. Printing/Parsing
2. Bridge to UntypedAST