package logtk

  1. Overview
  2. Docs
Core types and algorithms for logic

Install 

dune-project
 Dependency

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

Authors

  1. S
    Simon Cruanes
  2. P
    Petar Vukmirovic
  3. A
    Alexander Bentkamp
  4. S
    Sophie Tourret
  5. V
    Visa Nummelin

Maintainers

  1. S
    simon.cruanes.2.17@m4x.org

Sources

2.1.tar.gz
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287

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

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
val enable_def_as_rewrite : bool ref
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 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.

Printing is simpler, because it does not involve includes.

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

  • raises Error

    if there are remaining includes

  • raises Error

    if the AST contains Data