marklemay / tptpparser Goto Github PK

View Code? Open in Web Editor NEW

8.0 5.0 2.0 6.56 MB

an xtext based parser for the tptp grammer.

License: MIT License

Java 100.00%

tptpparser's Introduction

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)