tptpParser

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

• help -> install new software
• in the in the workwith field enter our update site "http://marklemay.github.io/tptpParser/site.p2"
• check parser
• click next
• follow the prompts until the plugin is installed

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

• go to /org.xtext.example.mydsl.tests/src/org/xtext/example/mydsl/tests/CheckThemALL.java
• change the files paths ("C:\tptp\TPTP-v6.0.0\TPTP-v6.0.0\Axioms", "C:\tptp\Problems\Problems", "C:\tptp\TPTP-v6.0.0\TPTP-v6.0.0\Problems") to point to your local directories of Problems and Axioms, and compitition problem files
• run the main function

(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

• houscleaning
• currently unsupported files section
• unsupported problems list from https://github.com/marklemay/tptpParser/blob/master/com.theoremsandstuff.tptp.parser.tests/src/com/theoremsandstuff/tptp/parser/tests/CheckThemALL.java
• untested problems list from https://github.com/marklemay/tptpParser/blob/master/com.theoremsandstuff.tptp.parser.tests/src/com/theoremsandstuff/tptp/parser/tests/CheckThemALL.java
• link the links in readme
• clarify design principles
• delete tmp
• check spelling
• reactivate theoremsandstuff.com
• ...capitalization?
• see what other ignored things don't need to be checked in
• tests
• make tests more parameterized
• make tests parameterized junit tests
• set up continous integration
• other stuff
• what is the best way to aviod type colisions?
• merge the separate implementations, make things handled more consistently
• review the models for name clarity (and spelling)
• review prolog number, variable, and constant syntax
• separate antlr parser directory (may just be a copy and past procedure)
• write download instructions in the readme
• create a simple demo project that imports it?
• eclipse download site (marklemay.github.io/tptpParser/site.p2)
• write download instructions in the readme
• add a picture!
• deploy to maven
• Continuous integration setup
• separate sublanguages into separate files
• autoformatter
• tooltip hints
• file linking with the include directive (include from only the same language)
• eclipse icon?
• compiletime validation of linking and type checking
• comment meta info tagging
• separate eclipse plugins that could just target the sublanguages? most users don't need all
• synchronize and embed version number in the build properties, maven and documentation
• why doesn't this work https://github.com/blog/1375-task-lists-in-gfm-issues-pulls-comments
• write shameless self promotion about the project leaders.
• rename "parser" is an awful name

currently unsupported TODO