This is a parser for the TPTP format (see http://www.cs.miami.edu/~tptp/), written in Java, using Antlr v2.7.

Project maintainer: Alexandre Riazanov, alexandre.riazanov@gmail.com


Authors and contributors
------------------------

This software is created by Andrei Tchaltsev <tchaltsev AT itc.it>
and Alexandre Riazanov <alexandre.riazanov AT gmail.com>.

Geoff Sutcliffe <geoff AT cs.miami.edu> contributed significantly by
updating constantly the code and implementing pretty-printing.

Overview
--------

This package provides Java sources for a parser for the (new) TPTP format.
It contains the parser itself, generated by ANTLR from a grammar file 
also provided with the package.

The parser is intended to be highly reusable. The grammar and the parser
itself can be used without modifications in practically any application.
This universality is achieved by isolating the parser code by a special 
interface layer. This layer consist of a number of interfaces, grouped 
under the interface TptpParserOutput, which specify a protocol of iteraction
between the parser and a client code. 

These interfaces are in essence an abstract syntax for the TPTP format. 
They allow creation of abstract syntax representations of various 
TPTP elements, although they do not specify access to constituents of 
these representations. The user is supposed to provide an implementation 
of these interfaces most suitable for his specific needs. The user is free 
to choose any concrete representation of TPTP elements. A simple but
reasonably efficient default implementation of the interface layer 
is also provided with this package. It is likely to be sufficient 
for most but rather sophisticated uses of the parser.

Our parser is re-enterable in quite a strong sense: several streams can be 
parsed simultaneously by separate parser objects and, moreover, 
these parser objects can use the same instance of the interface layer.
However, the latter mode is not thread safe, i.e. a call to a method on 
one parser object must return before a call to another method on another
object.


Requirements
------------

Use Maven 2 to build and install the parser (see pom.xml). 


Files
-----


./README                                     
                          This file.

./src/main/java/logic/is/power/tptp_parser/tptp_tester.java                   
                          Example command line application. The
                          program parses a specified file and checks
                          it syntactically and semantically. The
                          semantic check verifies that signature symbols
                          in the input file are used consistently.
                          However, the main purpose of tptp_tester.java
                          is to illustrate simple use of the parser
                          and SimpleTptpParserOutput.java.


./src/main/java/logic/is/power/tptp_parser/TptpParserOutput.java              
                          Specification of the interface layer. It
                          contains a bundle of Java interfaces to be
                          implemented by user-provided classes. A default
                          implementation is also given in 
                          SimpleTptpParserOutput.java.

./src/main/java/logic/is/power/tptp_parser/SimpleTptpParserOutput.java        
                          Default implementation of the interface layer. 
                          It is however likely to be sufficient for
                          most uses but rather sophisticated ones. 

./src/main/antlr/tptp.g              
                          ANTLR grammar file for TPTP.

./target/generated-sources/antlr/logic/is/power/tptp_parser/TptpLexer.java  
                          Lexer (tokeniser) class generated by ANTLR
                          from the grammar.



./target/generated-sources/antlr/logic/is/power/tptp_parser/TptpParser.java                    
                          Parser classes generated by ANTLR from the grammar.

./target/generated-sources/antlr/logic/is/power/tptp_parserTptpTokenTypes.java                
                          Auxilliary file generated by ANTLR, to be
                          used with TptpLexer.java and TptpParser.java.


./test.p                             
                          Dummy file in the TPTP format, which provides
                          a good coverage of TPTP features.


Notes on the grammar
--------------------

There are a few discrepancies between the official TPTP grammar specification
and its implementation in our parser. Here is the list of such differences:
*  a number can also be a real in scientific notation, i.e. with exponent.
   For example, -3e10 and 3.6E-123;
*  the TAB character is allowed in one-line comments;
*  not only printable but also TAB, newlines, extended ASCII and a few 
   other characters are  allowed in <distinct_object>
*  in <atomic_formula> propositions and predicates (in <plain_atom>)
   can also be <dollar_word>, i.e. begin with $ character.
*  in <defined_term> new alternatives "<atomic_defined_word>" and 
    "<atomic_defined_word> (<arguments>)" are added, i.e.
   term now may have <dollar_word> as functor or constant.
*  semantic grammar rules for <source> and <useful_info> are encoded hard into
   the parser, i.e. it is a syntactic error if an input violates any of the
   corresponding semantic grammar rule;
*  old style syntax rule for input_formula and input_clause are still
   maintained (although, in the grammar description they are explicitly not
   supported any more)
*  in rule <formula_role> "lemma_conjecture" was removed, but "assumption" and
   "type" added.
*  a new subrule <assumptions_record> is added to <inference_item>.
   <assumptions_record> :== assumptions([<name_list>])
*  rule <intro_type> has an additional alternative <assumption>
*  <general_data> has additional alternatives <variables> and (<fof_formula>)


Quick user guide
----------------



1. Simplest use.
^^^^^^^^^^^^^^^^

In your code write something like this:


...

import.tptp_parser.*;

...

/* Open input stream */
DataInputStream inputStream = 
  new DataInputStream(new FileInputStream(new File(myInputFileName)));

/* Create a lexer object */
TptpLexer lexer = new TptpLexer(inputStream);

/* Create a parser object */

TptpLexer parser = new TptpParser(lexer);

/* Create the parser interface layer object */

SimpleTptpParserOutput parserOutput = new SimpleTptpParserOutput();

try {
      
    for (SimpleTptpParserOutput.TopLevelItem item = 
           (SimpleTptpParserOutput.TopLevelItem)parser.topLevelItem(parserOutput);
         item != null;
         item =
           (SimpleTptpParserOutput.TopLevelItem)parser.topLevelItem(parserOutput))
    {
      
      // Do what you have to do with the item, e.g. check it semantically.
      // Consult the docs for SimpleTptpParserOutput.TopLevelItem
      // on how such objects can be precessed.
      ...

    };
}
// General ANTLR exception, provides diagnostics.
catch (antlr.ANTLRException e) {
    System.err.println("Syntax error in " + myInputFileName + ": " + e);
}
// Other exceptions.
catch (Exception e) {
    System.err.println("Internal error: " + e);
}

...

A complete example of simple use of the parser can be found in
./src/main/java/logic/is/power/tptp_parser/tptp_tester.java . This code also demonstrates how include directives
can be processed on the fly. In particular, when nested includes are parsed,
there may be several active lexer and parser objects simultaneously, 
and they use the same ParserOutput object.


2. Advanced use options
^^^^^^^^^^^^^^^^^^^^^^^

-- In some situations the functionality or performance of 
SimpleTptpParserOutput may not be sufficient for your purposes. For example, 
you may want to use a more sofisticated data structures better suited for 
later processing required by your application. In this case you are free 
to use your own implementation of the TptpParserOutput interface. 
For requirements to such an implementation see the docs for TptpParserOutput. 
Note that no changes will be required in the code provided by this package, 
you will only have to add some code.

-- Online docs can be created by typing "make docs".

-- The parser sources, class files and the TptpParser.jar file can be
recreated from the grammar file by running make without arguments.
To do this, change the relevant paths (variable ANTLR_JAR) in Makefile.

Important notes
---------------

-- Note that this is only an alpha version and some changes 
in the functionality and the interface are very likely. Ocassional errors
are also not unlikely. Bug reports will be appreciated.

-- Note that in the TPTP syntax infix operator "=" is used 
for the equality predicate. This predicate will be distinguished from
"equal" which is currently an uninterpreted predicate.

-- The tptp_tester program can be used as follows:
prompt> java -jar target/tptp-parser-2.0-jar-with-dependencies.jar <input file>
For help, use 
prompt> java -jar target/tptp-parser-2.0-jar-with-dependencies.jar -h
The program reports syntactic errors in the input file (without examining
the includes) as well as inconsitencies in the use of signature symbols,
e.g. when some symbol is used both as a predicate and as a function.



Bug reports
-----------

To report a bug, please use the GitHub repository https://github.com/riazanov/tptp-parser or contact the project maintainer, Alexandre Riazanov (alexandre.riazanov@gmail.com).