Merge remote-tracking branch 'origin/master'
This commit is contained in:
@@ -1,2 +1,54 @@
|
|||||||
# Pandamonium Theorem Prover
|
# Pandamonium Theorem Prover
|
||||||
This is the main repository for the Technical Software Project
|
This project contains several different modules for different parts of the system.
|
||||||
|
|
||||||
|
* [persistence](persistence/README.md)
|
||||||
|
* [web-server](src/README.md)
|
||||||
|
|
||||||
|
## Getting Started
|
||||||
|
|
||||||
|
1. Clone the project. `git clone git@github.com:atusa17/tsp.git`
|
||||||
|
2. Open the `pandamonium-theorem-prover` folder with IntelliJ. Use auto-import for a Gradle project.
|
||||||
|
3. Individual Components have their own README. Continue there.
|
||||||
|
|
||||||
|
## Running the Tests
|
||||||
|
|
||||||
|
This project is unit tested with JUnit and Mockito. You can run the unit tests with IntelliJ or Gradle. To run them with IntelliJ, browse to any `*Test.java` file and use IntelliJ's built-in test runner to run or debug the test. To run all the unit tests with Gradle:
|
||||||
|
|
||||||
|
* On a Linux or Macintosh machine:
|
||||||
|
|
||||||
|
```$ ./gradlew test```
|
||||||
|
|
||||||
|
* On a Windows machine:
|
||||||
|
|
||||||
|
```$ gradlew.bat test```
|
||||||
|
|
||||||
|
You can also test modules individually:
|
||||||
|
|
||||||
|
* On a Linux or Macintosh machine:
|
||||||
|
|
||||||
|
```$ ./gradlew persistence:test```
|
||||||
|
|
||||||
|
* On a Windows machine:
|
||||||
|
|
||||||
|
```$ gradlew.bat persistence:test```
|
||||||
|
|
||||||
|
## Integration Tests
|
||||||
|
|
||||||
|
To run the integration tests with IntelliJ, browse to any `*Test.java` file residing in any module name `integrationTest` and use IntelliJ's built-in test runner to run or debug the test. To run all the integration tests with Gradle:
|
||||||
|
|
||||||
|
* On a Linux or Macintosh machine:
|
||||||
|
|
||||||
|
```$ ./gradlew integrationTest```
|
||||||
|
|
||||||
|
* On a Windows machine
|
||||||
|
|
||||||
|
```$ gradlew.bat integrationTest```
|
||||||
|
|
||||||
|
## Built with
|
||||||
|
|
||||||
|
* [Spring Boot](https://projects.spring.io/spring-boot/) - Web framework
|
||||||
|
* [Spring Web Flow](https://projects.spring.io/spring-webflow/) - MVC framework
|
||||||
|
* [Gradle](https://gradle.org/) - Dependency management
|
||||||
|
* [JUnit](http://junit.org/junit4/) - Unit tests
|
||||||
|
* [Mockito](http://site.mockito.org/) - Mock objects library
|
||||||
|
* [Lombok](https://projectlombok.org/) - Boilerplate Code Generator
|
||||||
|
|||||||
@@ -0,0 +1,61 @@
|
|||||||
|
## PTP Persistence API
|
||||||
|
|
||||||
|
The PTP Persistence API is the web API for accessing the theorems database.
|
||||||
|
|
||||||
|
<http://localhost:8090/>
|
||||||
|
|
||||||
|
## Running from IntelliJ
|
||||||
|
|
||||||
|
* Create a new run configuration in IntelliJ.
|
||||||
|
|
||||||
|
```
|
||||||
|
Name: "PTP Persistence API Tomcat"
|
||||||
|
Application Server: Tomcat (8.5.12)
|
||||||
|
HTTP Port: 8090
|
||||||
|
JMX Port: 1090
|
||||||
|
Deployment tabe: Deploy persistence-api.war (exploded)
|
||||||
|
```
|
||||||
|
## Running the Tests
|
||||||
|
|
||||||
|
This project is unit tested with JUnit and Mockito. You can run the unit tests with IntelliJ or Gradle. To run them with IntelliJ, browse to any `*Test.java` file and use IntelliJ's built-in test runner to run or debug the test. To run all the unit tests with Gradle:
|
||||||
|
|
||||||
|
* On a Linux or Macintosh machine:
|
||||||
|
|
||||||
|
```$ ./gradlew test```
|
||||||
|
|
||||||
|
* On a Windows machine:
|
||||||
|
|
||||||
|
```$ gradlew.bat test```
|
||||||
|
|
||||||
|
You can also test modules individually:
|
||||||
|
|
||||||
|
* On a Linux or Macintosh machine:
|
||||||
|
|
||||||
|
```$ ./gradlew persistence:test```
|
||||||
|
|
||||||
|
* On a Windows machine:
|
||||||
|
|
||||||
|
```$ gradlew.bat persistence:test```
|
||||||
|
|
||||||
|
## Integration Tests
|
||||||
|
|
||||||
|
To run the integration tests with IntelliJ, browse to any `*Test.java` file residing in any module name `integrationTest` and use IntelliJ's built-in test runner to run or debug the test. To run all the integration tests with Gradle:
|
||||||
|
|
||||||
|
* On a Linux or Macintosh machine:
|
||||||
|
|
||||||
|
```$ ./gradlew integrationTest```
|
||||||
|
|
||||||
|
* On a Windows machine
|
||||||
|
|
||||||
|
```$ gradlew.bat integrationTest```
|
||||||
|
|
||||||
|
## Built with
|
||||||
|
|
||||||
|
* [Spring Boot](https://projects.spring.io/spring-boot/) - Web framework
|
||||||
|
* [Spring Web Flow](https://projects.spring.io/spring-webflow/) - MVC framework
|
||||||
|
* [Spring Data](https://spring.io/projects/spring-data/) - Persistence framework
|
||||||
|
* [Gradle](https://gradle.org/) - Dependency management
|
||||||
|
* [JUnit](http://junit.org/junit4/) - Unit tests
|
||||||
|
* [Mockito](http://site.mockito.org/) - Mock objects library
|
||||||
|
* [Lombok](https://projectlombok.org/) - Boilerplate Code Generator
|
||||||
|
* [Hibernate ORM](http://hibernate.org/orm/) - Object/Relational Mapping
|
||||||
@@ -0,0 +1,43 @@
|
|||||||
|
package edu.msudenver.tsp.services.parser;
|
||||||
|
|
||||||
|
import lombok.Getter;
|
||||||
|
import lombok.Setter;
|
||||||
|
|
||||||
|
public class Node
|
||||||
|
{
|
||||||
|
@Getter private final String statement;
|
||||||
|
@Getter @Setter private Node left;
|
||||||
|
@Getter @Setter private Node right;
|
||||||
|
@Getter @Setter private Node center;
|
||||||
|
@Getter private final Node parent;
|
||||||
|
@Getter private final int depth;
|
||||||
|
|
||||||
|
public Node(final String statement, final Node parent)
|
||||||
|
{
|
||||||
|
this.statement = statement + "\n";
|
||||||
|
left = null;
|
||||||
|
right = null;
|
||||||
|
center = null;
|
||||||
|
this.parent = parent;
|
||||||
|
if(parent != null)
|
||||||
|
{
|
||||||
|
depth = parent.depth + 1;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
depth = 0;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public String toString()
|
||||||
|
{
|
||||||
|
String returnVal = this.depth + ": " + this.statement;
|
||||||
|
|
||||||
|
if(this.left != null) returnVal += "... " + this.left.toString();
|
||||||
|
if(this.center != null) returnVal += "... " + this.center.toString();
|
||||||
|
if(this.right != null) returnVal += "... " + this.right.toString();
|
||||||
|
|
||||||
|
return returnVal;
|
||||||
|
}
|
||||||
|
}
|
||||||
@@ -1,11 +0,0 @@
|
|||||||
package edu.msudenver.tsp.services.parser;
|
|
||||||
|
|
||||||
import org.springframework.context.annotation.ComponentScan;
|
|
||||||
import org.springframework.context.annotation.Configuration;
|
|
||||||
|
|
||||||
@Configuration
|
|
||||||
@ComponentScan
|
|
||||||
//@PropertySource("classpath:development.properties")
|
|
||||||
public class ParserConfig {
|
|
||||||
|
|
||||||
}
|
|
||||||
@@ -7,12 +7,16 @@ import edu.msudenver.tsp.persistence.controller.TheoremController;
|
|||||||
import org.springframework.beans.factory.annotation.Autowired;
|
import org.springframework.beans.factory.annotation.Autowired;
|
||||||
import org.springframework.stereotype.Service;
|
import org.springframework.stereotype.Service;
|
||||||
|
|
||||||
|
import java.util.ArrayList;
|
||||||
|
import java.util.List;
|
||||||
|
|
||||||
@Service
|
@Service
|
||||||
class ParserService {
|
class ParserService {
|
||||||
private final DefinitionController definitionController;
|
private final DefinitionController definitionController;
|
||||||
private final TheoremController theoremController;
|
private final TheoremController theoremController;
|
||||||
private final NotationController notationController;
|
private final NotationController notationController;
|
||||||
private final ProofController proofController;
|
private final ProofController proofController;
|
||||||
|
private Node root;
|
||||||
|
|
||||||
@Autowired
|
@Autowired
|
||||||
public ParserService(final DefinitionController definitionController, final TheoremController theoremController,
|
public ParserService(final DefinitionController definitionController, final TheoremController theoremController,
|
||||||
@@ -23,4 +27,117 @@ class ParserService {
|
|||||||
this.proofController = proofController;
|
this.proofController = proofController;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
public boolean parseUserInput(final String userInput)
|
||||||
|
{
|
||||||
|
try {
|
||||||
|
final Node tree = parseRawInput(userInput);
|
||||||
|
final List<String> statements = retrieveStatements(tree);
|
||||||
|
|
||||||
|
return true;
|
||||||
|
} catch(final Exception e) {
|
||||||
|
e.printStackTrace();
|
||||||
|
}
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
|
||||||
|
public Node parseRawInput(String input)
|
||||||
|
{
|
||||||
|
input = input.toLowerCase();
|
||||||
|
|
||||||
|
root = new Node(input, null);
|
||||||
|
|
||||||
|
if(input.equals(""))
|
||||||
|
{
|
||||||
|
return root;
|
||||||
|
}
|
||||||
|
|
||||||
|
recurse(root);
|
||||||
|
|
||||||
|
return root;
|
||||||
|
}
|
||||||
|
|
||||||
|
private void recurse(final Node current)
|
||||||
|
{
|
||||||
|
int startIndex;
|
||||||
|
int endIndex;
|
||||||
|
final String statement;
|
||||||
|
|
||||||
|
if (current != null) {
|
||||||
|
statement = current.getStatement();
|
||||||
|
} else {
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
|
||||||
|
String nextStatement;
|
||||||
|
|
||||||
|
if(statement.contains("let"))
|
||||||
|
{
|
||||||
|
current.setLeft(new Node("let", current));
|
||||||
|
|
||||||
|
startIndex = statement.indexOf("let")+"let".length();
|
||||||
|
|
||||||
|
if(statement.contains("if")){
|
||||||
|
endIndex = statement.indexOf("if");
|
||||||
|
} else if(statement.contains("then")){
|
||||||
|
endIndex = statement.indexOf("then");
|
||||||
|
} else {
|
||||||
|
endIndex = statement.length();
|
||||||
|
}
|
||||||
|
|
||||||
|
nextStatement = statement.substring(startIndex, endIndex);
|
||||||
|
|
||||||
|
current.getLeft().setCenter(new Node(nextStatement, current.getLeft()));
|
||||||
|
recurse(current.getLeft().getCenter());
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
if(statement.contains("if"))
|
||||||
|
{
|
||||||
|
current.setCenter(new Node("if", current));
|
||||||
|
|
||||||
|
startIndex = statement.indexOf("if")+"if".length();
|
||||||
|
endIndex = (statement.contains("then") ? statement.indexOf("then") : statement.length());
|
||||||
|
nextStatement = statement.substring(startIndex, endIndex);
|
||||||
|
|
||||||
|
current.getCenter().setCenter(new Node(nextStatement, current.getCenter()));
|
||||||
|
recurse(current.getCenter().getCenter());
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
if(current.getStatement().contains("then"))
|
||||||
|
{
|
||||||
|
current.setRight(new Node("then", current));
|
||||||
|
|
||||||
|
startIndex = statement.indexOf("then")+"then".length();
|
||||||
|
nextStatement = statement.substring(startIndex);
|
||||||
|
|
||||||
|
current.getRight().setCenter(new Node(nextStatement, current.getRight()));
|
||||||
|
recurse(current.getRight().getCenter());
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
public List<String> retrieveStatements(final Node parsedTree)
|
||||||
|
{
|
||||||
|
return populateStatementList(parsedTree, new ArrayList<>());
|
||||||
|
}
|
||||||
|
|
||||||
|
private ArrayList<String> populateStatementList(final Node node, final ArrayList<String> statementList)
|
||||||
|
{
|
||||||
|
if(node == null)
|
||||||
|
{
|
||||||
|
return statementList;
|
||||||
|
}
|
||||||
|
|
||||||
|
final String statement = node.getStatement().trim();
|
||||||
|
if(!(statement.contains("let") || statement.contains("if") || statement.contains("then")))
|
||||||
|
{
|
||||||
|
statementList.add(statement);
|
||||||
|
}
|
||||||
|
|
||||||
|
populateStatementList(node.getLeft(), statementList);
|
||||||
|
populateStatementList(node.getCenter(), statementList);
|
||||||
|
populateStatementList(node.getRight(), statementList);
|
||||||
|
|
||||||
|
return statementList;
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -1,17 +1,143 @@
|
|||||||
package edu.msudenver.tsp.services.parser;
|
package edu.msudenver.tsp.services.parser;
|
||||||
|
|
||||||
|
import edu.msudenver.tsp.persistence.controller.DefinitionController;
|
||||||
import org.junit.Test;
|
import org.junit.Test;
|
||||||
import org.junit.runner.RunWith;
|
import org.junit.runner.RunWith;
|
||||||
|
import org.mockito.InjectMocks;
|
||||||
import org.mockito.runners.MockitoJUnitRunner;
|
import org.mockito.runners.MockitoJUnitRunner;
|
||||||
|
|
||||||
|
import java.util.ArrayList;
|
||||||
|
import java.util.List;
|
||||||
|
|
||||||
import static org.junit.Assert.assertEquals;
|
import static org.junit.Assert.assertEquals;
|
||||||
|
import static org.junit.Assert.assertTrue;
|
||||||
|
import static org.mockito.Matchers.anyString;
|
||||||
|
import static org.mockito.Mockito.mock;
|
||||||
|
import static org.mockito.Mockito.when;
|
||||||
|
|
||||||
@RunWith(MockitoJUnitRunner.class)
|
@RunWith(MockitoJUnitRunner.class)
|
||||||
public class ParserServiceTest {
|
public class ParserServiceTest {
|
||||||
|
|
||||||
|
private final DefinitionController definitionControllerMock = mock(DefinitionController.class);
|
||||||
|
private final ParserService mockParserService = mock(ParserService.class);
|
||||||
|
|
||||||
|
@InjectMocks
|
||||||
|
private final ParserService parserService = new ParserService(definitionControllerMock, null,
|
||||||
|
null, null);
|
||||||
|
|
||||||
@Test
|
@Test
|
||||||
public void test() {
|
public void testEmptyStringEqualsEmptyString() {
|
||||||
assertEquals(3,3);
|
final String expected = "0: \n";
|
||||||
|
final String actual = parserService.parseRawInput("").toString();
|
||||||
|
|
||||||
|
assertEquals(expected, actual);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@Test
|
||||||
|
public void testUselessStringEqualsUselessString() {
|
||||||
|
final String expected = "0: cat\n";
|
||||||
|
final String actual = parserService.parseRawInput("cat").toString();
|
||||||
|
|
||||||
|
assertEquals(expected, actual);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Test
|
||||||
|
public void testSingleIfReturnsIfPlusEmptyString() {
|
||||||
|
final String expected = "0: if\n... 1: if\n... 2: \n\n";
|
||||||
|
final String actual = parserService.parseRawInput("if").toString();
|
||||||
|
|
||||||
|
assertEquals(expected, actual);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Test
|
||||||
|
public void testBaseCaseIfXIsEvenThenXSquaredIsEven() {
|
||||||
|
final String expected = "0: if x is even then x^2 is even\n" +
|
||||||
|
"... 1: if\n" +
|
||||||
|
"... 2: x is even \n" +
|
||||||
|
"... 1: then\n" +
|
||||||
|
"... 2: x^2 is even\n\n";
|
||||||
|
|
||||||
|
final String actual = parserService.parseRawInput("if x is even then x^2 is even").toString();
|
||||||
|
|
||||||
|
assertEquals(expected, actual);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Test
|
||||||
|
public void testLetXBeEvenThenXSquaredIsEven() {
|
||||||
|
final String expected = "0: let x be even. then x^2 is even.\n" +
|
||||||
|
"... 1: let\n" +
|
||||||
|
"... 2: x be even. \n" +
|
||||||
|
"... 1: then\n" +
|
||||||
|
"... 2: x^2 is even.\n\n";
|
||||||
|
|
||||||
|
final String actual = parserService.parseRawInput("Let x be even. Then x^2 is even.").toString();
|
||||||
|
|
||||||
|
assertEquals(expected, actual);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Test
|
||||||
|
public void testLetIfThen() {
|
||||||
|
final String expected = "0: let a. if b, then c.\n" +
|
||||||
|
"... 1: let\n" +
|
||||||
|
"... 2: a. \n" +
|
||||||
|
"... 1: if\n" +
|
||||||
|
"... 2: b, \n" +
|
||||||
|
"... 1: then\n" +
|
||||||
|
"... 2: c.\n\n";
|
||||||
|
|
||||||
|
final String actual = parserService.parseRawInput("Let a. If b, then c.").toString();
|
||||||
|
|
||||||
|
assertEquals(expected, actual);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Test
|
||||||
|
public void testLetStatementWithoutAnyIfOrThenStatements() {
|
||||||
|
final String expected = "0: let a be equal to b.\n" +
|
||||||
|
"... 1: let\n" +
|
||||||
|
"... 2: a be equal to b.\n\n";
|
||||||
|
|
||||||
|
final String actual = parserService.parseRawInput("Let a be equal to b.").toString();
|
||||||
|
|
||||||
|
assertEquals(expected, actual);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Test
|
||||||
|
public void testEmptyStringReturnsEmptyList() {
|
||||||
|
final List<String> expectedList = new ArrayList<>();
|
||||||
|
expectedList.add("");
|
||||||
|
|
||||||
|
when(mockParserService.parseRawInput(anyString())).thenReturn(new Node("", null));
|
||||||
|
final List<String> actualList = parserService.retrieveStatements(mockParserService.parseRawInput(""));
|
||||||
|
|
||||||
|
assertEquals(expectedList, actualList);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Test
|
||||||
|
public void testBaseCaseReturnsXIsEven() {
|
||||||
|
final List<String> expectedList = new ArrayList<>();
|
||||||
|
expectedList.add("x is even");
|
||||||
|
expectedList.add("x^2 is even");
|
||||||
|
|
||||||
|
final Node testNode = new Node("if x is even then x^2 is even", null);
|
||||||
|
testNode.setCenter(new Node("if", testNode));
|
||||||
|
testNode.getCenter().setCenter(new Node(" x is even ", testNode.getCenter()));
|
||||||
|
testNode.setRight(new Node("then", testNode));
|
||||||
|
testNode.getRight().setCenter(new Node(" x^2 is even", testNode.getRight()));
|
||||||
|
|
||||||
|
when(mockParserService.parseRawInput(anyString())).thenReturn(testNode);
|
||||||
|
final List<String> actualList = parserService.retrieveStatements(mockParserService.parseRawInput("baseCase"));
|
||||||
|
|
||||||
|
assertEquals(expectedList, actualList);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Test
|
||||||
|
public void testDriveParseUserInput() {
|
||||||
|
final Node testNode = new Node("", null);
|
||||||
|
when(mockParserService.parseRawInput(anyString())).thenReturn(testNode);
|
||||||
|
when(mockParserService.retrieveStatements(testNode)).thenReturn(new ArrayList<>());
|
||||||
|
|
||||||
|
final boolean successfulTestDrive = parserService.parseUserInput("");
|
||||||
|
|
||||||
|
assertTrue(successfulTestDrive);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
@@ -0,0 +1,58 @@
|
|||||||
|
## PTP Persistence API
|
||||||
|
|
||||||
|
The PTP Persistence API is the web API for accessing the theorems database.
|
||||||
|
|
||||||
|
<http://localhost:8080/>
|
||||||
|
|
||||||
|
## Running from IntelliJ
|
||||||
|
|
||||||
|
* Create a new run configuration in IntelliJ.
|
||||||
|
|
||||||
|
```
|
||||||
|
Name: "Pandamonium Theorem Prover Tomcat"
|
||||||
|
Application Server: Tomcat (8.5.12)
|
||||||
|
HTTP Port: 8080
|
||||||
|
JMX Port: 1080
|
||||||
|
Deployment tabe: Deploy pandamonium-theorem-prover.war (exploded)
|
||||||
|
```
|
||||||
|
## Running the Tests
|
||||||
|
|
||||||
|
This project is unit tested with JUnit and Mockito. You can run the unit tests with IntelliJ or Gradle. To run them with IntelliJ, browse to any `*Test.java` file and use IntelliJ's built-in test runner to run or debug the test. To run all the unit tests with Gradle:
|
||||||
|
|
||||||
|
* On a Linux or Macintosh machine:
|
||||||
|
|
||||||
|
```$ ./gradlew test```
|
||||||
|
|
||||||
|
* On a Windows machine:
|
||||||
|
|
||||||
|
```$ gradlew.bat test```
|
||||||
|
|
||||||
|
You can also test modules individually:
|
||||||
|
|
||||||
|
* On a Linux or Macintosh machine:
|
||||||
|
|
||||||
|
```$ ./gradlew persistence:test```
|
||||||
|
|
||||||
|
* On a Windows machine:
|
||||||
|
|
||||||
|
```$ gradlew.bat persistence:test```
|
||||||
|
|
||||||
|
## Integration Tests
|
||||||
|
|
||||||
|
To run the integration tests with IntelliJ, browse to any `*Test.java` file residing in any module name `integrationTest` and use IntelliJ's built-in test runner to run or debug the test. To run all the integration tests with Gradle:
|
||||||
|
|
||||||
|
* On a Linux or Macintosh machine:
|
||||||
|
|
||||||
|
```$ ./gradlew integrationTest```
|
||||||
|
|
||||||
|
* On a Windows machine
|
||||||
|
|
||||||
|
```$ gradlew.bat integrationTest```
|
||||||
|
|
||||||
|
## Built with
|
||||||
|
|
||||||
|
* [Spring Boot](https://projects.spring.io/spring-boot/) - Web framework
|
||||||
|
* [Gradle](https://gradle.org/) - Dependency management
|
||||||
|
* [JUnit](http://junit.org/junit4/) - Unit tests
|
||||||
|
* [Mockito](http://site.mockito.org/) - Mock objects library
|
||||||
|
* [Lombok](https://projectlombok.org/) - Boilerplate Code Generator
|
||||||
Reference in New Issue
Block a user