Module Read_tme (.ml)

module Read_tme: sig .. end

reads tme files

See Backus Naur tme Syntax for the complete tme specification.

all functions
Raises Const.PARSE_ERROR on incorrect input.

Only the subset necessary to read formula is supported in darwin, fancy things like costs, flags, ... are not.

E.g. MSC006-1 from TPTPv2.6:

  q(X, Z) :- 

    q(X, Y), 

    q(Y, Z).

  p(X, Y); 

  q(X, Y).

  false :- p(a, b).

The supported tme subset in EBNF:

clause    ::= head [ ( ':-' | '<-' ) body ]

head      ::= literal { ( ',' | ';' ) literal }

body      ::= literal { ',' literal }

literal   ::= [ ('-' | '~') ] atom

            | 'true'

            | 'false'

atom      ::= symbol

            | symbol '(' term { ',' term } ')'

            | '(' term '=' term ')'

term      ::= variable

            | symbol [ '(' term { ',' term } ')' ]?

variable  ::= ( 'A'-'Z' | '_' ) { 'a'-'z' | 'A'-'Z' | '0'-'9' | '_' }

symbol    ::= ( 'a'-'z' | '0'-'9' ) { 'a'-'z' | 'A'-'Z' | '0'-'9' | '_' }

% is used for line comments, /* ... */ to comment regions.

Parameteric variables can not be represented in a tme file.

type clause = Term.clause

val to_clauses_from_string : string -> clause list

to_clauses_from_file file_name reads the tme file file_name into a Term.clause list.

On a parsing error a Failure exception is raised.

val to_clauses_from_file : string -> clause list

to_clauses_from_file file_name reads the tme file file_name into a Term.clause list.

On a parsing error a Failure exception is raised.

val to_clause : string -> clause

converts a string to a Term.clause.