an xtext based parser for the tptp grammer.
Java
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
com.theoremsandstuff.tptp.parser.sdk
com.theoremsandstuff.tptp.parser.tests
com.theoremsandstuff.tptp.parser.ui
com.theoremsandstuff.tptp.parser
doc
tmp
LICENSE
README.md

README.md

tptpParser

usage screenshot

An xtext based parser for the TPTP grammar. (can be used as a java parser, or an awesome eclipse plugin)

This is built with xtext v2.4.3, and we welcome all patches and pull requests!

If you use this libray, we'd love to hear about it!

Installing the Eclipse Plugin

We have tested against Eclipse Kepler

In Eclipse

Using the Parser

If you are using Maven, the easiest way to use this project is to add

<dependency>
    <groupId>tptp</groupId>
    <artifactId>parser</artifactId>
    <version>0.0.6-SNAPSHOT</version>
</dependency>

and

<repositories>
    <repository>
        <id>tptpParser-mvn-repo</id>
        <url>https://raw.github.com/marklemay/tptpParser/mvn-repo/</url>
        <snapshots>
            <enabled>true</enabled>
            <updatePolicy>always</updatePolicy>
        </snapshots>
    </repository>
</repositories>

to your pom.xml (we use the poor man's repo method)

You can also make your project directly dependent on the binary jar or the source jar. This is not recommended because you will need to download transitive dependencies.

See the test file CheckThemALL.java for usage

Committing

Browsing the source

There is only 1 source file, Parser.xtext

Checkout and build the project

  • Open eclipse with xtext
  • window -> open perspective -> other -> Git Repository Exploring
  • paste https://github.com/marklemay/tptpParser.git into the left panel
  • the Clone Git Reposity window will open
  • click finish
  • open tptpParser
  • right click on Working Directory
  • select Import Exiting Project
  • click next
  • you should see the 4 projects selected
  • click finish
  • go back to the java perspective (ignore any errors)
  • open com.theoremsandstuff.tptp.parser -> src -> com.theoremsandstuff.tptp
  • right click on Parser.xtext -> run as -> Generate Xtext Artifact

For further reading about the xtext framework, look at the offical Xtext documentation or Implementing Domain-Specific Languages with Xtext and Xtend by Lorenzo Bettini

See TODOs below about what you can improve

Running the tests

(TODO: see TODOs below about how this test could be improved)

Before committing, run the tests against all axioms, all problems, and all of the prevous competition pormlams.

The design principles

  • the primary goal is the generated java parser, the eclipse plugin (while really cool) is secondary
  • minimal/restrictive AST, we will ignore issues that happen in the extended biased problems, keeping the AST simple and restrictive will make it easier to use in competition programs
  • grammar should be restrictive, no need for multiple languages in the same file
  • validate against all sample problems, this should be competition-ready software
  • keep the eventual java parser and the eventual eclipse plugin (and the target tptp problem set in sync with version numbers)

global TODOs

currently unsupported TODO