Integrate diproche via swipl-wasm

.gitignore

@@ -4,7 +4,7 @@
 /node_modules
 /.pnp
 .pnp.js
-/src/util/diproche/diprocheProgram
+/diproche.pl
 
 # testing
 /coverage

package.json

@@ -1,48 +1,50 @@
 {
-	"name": "diproche-webinterface",
-	"version": "0.1.0",
-	"private": true,
-	"dependencies": {
-		"@types/lodash": "^4.14.136",
-		"@types/react-router-dom": "^4.3.4",
-		"@types/shortid": "0.0.29",
-		"bootstrap": "^4.3.1",
-		"jquery": "^3.4.1",
-		"lodash": "^4.17.15",
-		"node-sass": "^4.12.0",
-		"react": "^16.8.6",
-		"react-bootstrap": "^1.0.0-beta.10",
-		"react-dom": "^16.8.6",
-		"react-router-dom": "^5.0.1",
-		"react-scripts": "^3.0.1",
-		"shortid": "^2.2.14",
-		"tau-prolog": "^0.2.66",
-		"typescript": "3.4.2"
-	},
-	"scripts": {
-		"start": "react-scripts start",
-		"lint": "tslint --project .",
-		"build": "react-scripts build",
-		"test": "react-scripts test",
-		"eject": "react-scripts eject"
-	},
-	"eslintConfig": {
-		"extends": "react-app"
-	},
-	"browserslist": [
-		">0.2%",
-		"not dead",
-		"not ie <= 11",
-		"not op_mini all"
-	],
-	"devDependencies": {
-		"@types/jest": "24.0.11",
-		"@types/node": "11.13.2",
-		"@types/node-sass": "^4.11.0",
-		"@types/react": "16.8.13",
-		"@types/react-dom": "16.8.3",
-		"shx": "^0.3.2",
-		"tslint": "^5.18.0"
-	},
-	"proxy": "http://localhost:5000"
+  "name": "diproche-webinterface",
+  "version": "0.1.0",
+  "private": true,
+  "dependencies": {
+    "@types/lodash": "^4.14.136",
+    "@types/react-router-dom": "^4.3.4",
+    "@types/shortid": "0.0.29",
+    "bootstrap": "^4.3.1",
+    "jquery": "^3.4.1",
+    "lodash": "^4.17.15",
+    "node-sass": "^4.12.0",
+    "one_file_diproche": "git+ssh://git@github.com/TimothyGillespie/one_file_diproche.git",
+    "react": "^16.8.6",
+    "react-bootstrap": "^1.0.0-beta.10",
+    "react-dom": "^16.8.6",
+    "react-router-dom": "^5.0.1",
+    "react-scripts": "^3.0.1",
+    "shortid": "^2.2.14",
+    "tau-prolog": "^0.2.66",
+    "typescript": "3.4.2"
+  },
+  "scripts": {
+    "start": "npm run mv-diproche && react-scripts start",
+    "lint": "tslint --project .",
+    "build": "npm run mv-diproche && react-scripts build",
+    "test": "npm run mv-diproche && react-scripts test",
+    "eject": "react-scripts eject",
+    "mv-diproche": "shx cp ./node_modules/one_file_diproche/diproche_onefile.pl ./diproche.pl"
+  },
+  "eslintConfig": {
+    "extends": "react-app"
+  },
+  "browserslist": [
+    ">0.2%",
+    "not dead",
+    "not ie <= 11",
+    "not op_mini all"
+  ],
+  "devDependencies": {
+    "@types/jest": "24.0.11",
+    "@types/node": "11.13.2",
+    "@types/node-sass": "^4.11.0",
+    "@types/react": "16.8.13",
+    "@types/react-dom": "16.8.3",
+    "shx": "^0.3.2",
+    "tslint": "^5.18.0"
+  },
+  "proxy": "http://localhost:5000"
 }

src/util/diproche/addDiprocheIssues.ts

@@ -0,0 +1,10 @@
+import { addIssue } from "../issueHandling/issueMapping";
+
+function addDiprocheIssues(unverifiedLines: number[]): void {
+	unverifiedLines.forEach((singleLine: number) => {
+		addIssue("UNVERIFIED_LINE", {	fromIndex: singleLine, toIndex: singleLine});
+	});
+
+}
+
+export default addDiprocheIssues;

src/util/diproche/diprocheHandler.test.ts

@@ -0,0 +1,17 @@
+import DiprocheHandler from "./diprocheHandler";
+import tests from "./diprocheTestAssets.json";
+
+describe("Diproche Handler", () => {
+
+	const diproche = new DiprocheHandler();
+
+	beforeAll(async () => {
+		await diproche.loadDiproche();
+	}, 15000);
+
+	test("Will return 16 for test1", async () => {
+		const result = await diproche.query(tests.test1);
+		expect(result).toEqual([16]);
+	}, 50000);
+
+});

src/util/diproche/diprocheHandler.ts

@@ -0,0 +1,33 @@
+import fs from "fs";
+import path from "path";
+
+// The order of these two imports makes a functional difference
+// tslint:disable: ordered-imports
+import "../swipl-wasm/swipl-web";
+import { consult, loadingComplete as swiLoadingComplete, query } from "../prolog/swiplwasmHandler";
+// tslint:enable: ordered-imports
+
+const diprocheProgramCode: string = fs.readFileSync(
+	path.resolve(__dirname, "../../../diproche.pl"),
+	{encoding: "utf-8"},
+);
+
+class DiprocheHandler {
+	public async loadDiproche(): Promise<void> {
+		await swiLoadingComplete;
+		await consult(diprocheProgramCode);
+		console.log("Diproche was loaded");
+	}
+
+	public async query(queryString: string): Promise<string> {
+		let copyQueryString: string = queryString;
+		copyQueryString = copyQueryString.substr(0, copyQueryString.length - 1);
+
+		const result: string = await query("diproche_fo(" + copyQueryString + ", X).");
+		return result;
+
+	}
+
+}
+
+export default DiprocheHandler;

src/util/diproche/diprocheInterface.ts

@@ -1,14 +1,15 @@
 import { textFormatter } from "../inputFormatter/textFormatter";
 import { getDiprocheResponse } from "../proofChecker";
 import { collectInvalidWordsInIssues } from "../vocabularyChecker/detectWrongSyntax";
-import { addDiprocheIssues } from "./diprocheResponseProcessing";
+import addDiprocheIssues from "./addDiprocheIssues";
 
 export enum Mode {
 	propositionalLogic = "diproche",
 	firstOrderPredicateLogic = "diproche_fo",
 	test = "teste",
 }
 
+// The following function is added for testing reasons
 /**
  * returns a string containing the userInput as an argument of a predicate
  * @param userInput - the user input
@@ -44,7 +45,7 @@ export function getErrorsBeforeDiproche(userInput: string) {
  * Collects all errors that diproche returns
  */
 export async function getErrorsAfterDiproche(diprocheInput: string): Promise<void> {
-	const response: string = await getDiprocheResponse(diprocheInput);
+	const response: number[] = await getDiprocheResponse(diprocheInput);
 	addDiprocheIssues(response);
 }
 
@@ -55,6 +56,6 @@ export async function createErrors(userinput: string): Promise<void> {
 	getErrorsBeforeDiproche(userinput);
 
 	// Also adds Issues which are caused when progressing this function
-	const diprocheInput = textFormatter(userinput) + ".";
+	const diprocheInput = addPredicate(textFormatter(userinput), Mode.firstOrderPredicateLogic);
 	await getErrorsAfterDiproche(diprocheInput);
 }

src/util/diproche/diprocheTestAssets.json

@@ -0,0 +1,3 @@
+{
+  "test1": "[[wir,zeigen,[a,and,b],<->,[b,and,a]],[=>],[angenommen,a,and,b],[dann,a],[ferner,gilt,b],[damit,folgt,b,and,a],[qed],[abs],[<=],[nehmen,wir,jetzt,an,dass,b,and,a],[dann,folgt,a],[ausserdem,folgt,b],[also,gilt,nun,a,and,b],[qed],[damit,gilt,[a,and,b],<->,[c,and,a]]]."
+}

src/util/parseStringToIntegerArray.ts

@@ -0,0 +1,26 @@
+/**
+	* Converts a string to an array of numbers
+	* @param integerArrayAsString - A string representing a array of integers (i.e. [16, 87, 27])
+	* @return An array of integers represented by the string
+	*/
+export default function parseStringToIntegerArray(integerArrayAsString: string) {
+
+	if (integerArrayAsString === "[]") {
+		return [];
+	}
+
+	if (
+		integerArrayAsString.substr(0, 1) !== "[" ||
+		integerArrayAsString.substr(integerArrayAsString.length - 1, 1) !== "]"
+	) {
+		throw new Error("The given string is not contained in brackets '[]'");
+	}
+
+	// Removing the outter brackets
+	integerArrayAsString = integerArrayAsString.substr(1, integerArrayAsString.length - 2);
+
+	const arrayOfInteger = integerArrayAsString.split(",").map(s => Number.parseInt(s, 10));
+
+	return arrayOfInteger;
+
+}

src/util/prolog/swiplwasmHandler.test.ts

@@ -0,0 +1,66 @@
+// The order of these two imports makes a functional difference
+// tslint:disable: ordered-imports
+import "../swipl-wasm/swipl-web";
+import { consult, loadingComplete as swiLoadingComplete, query } from "./swiplwasmHandler";
+// tslint:enable: ordered-imports
+
+describe("swiplWasmHandler", () => {
+	beforeAll(async () => {
+		await swiLoadingComplete;
+	}, 15000);
+
+	test("Test whether bob and frank are men", async () => {
+		await consult("man(bob).");
+		expect(await query("man(bob).")).toEqual("true.");
+		expect(await query("man(frank).")).toEqual("false.");
+	});
+
+	test("Waiting on previous results and maintaining order is not necessary", async () => {
+		consult("man(bob).");
+		const bobResult = query("man(bob).");
+		const frankResult = query("man(frank).");
+
+		expect(await frankResult).toEqual("false.");
+		expect(await bobResult).toEqual("true.");
+	});
+
+	test("Can reconsult", async () => {
+		consult("man(bob).");
+		const bobResult = query("man(bob).");
+
+		consult("man(frank).");
+		const frankResult = query("man(frank).");
+
+		expect(await bobResult).toEqual("true.");
+		expect(await frankResult).toEqual("true.");
+	});
+
+	test("Can return concrete answer", async () => {
+		await consult("man(bob).");
+		expect(await query("man(N).")).toEqual("N = bob.");
+	});
+
+	/* doesn't work yet.
+
+	test("Can return multiple answers", async () => {
+		await consult("man(bob). man(frank).");
+		expect(await query("man(N).")).toEqual("N = bob;", "N = frank.");
+	});
+
+	test("Handles consulting errors", async () => {
+		try {
+			await consult("man(bob.");
+			fail("Should have thrown.");
+		} catch (e) {
+			expect(e.message).toBe(
+				"ERROR: /file.pl:1:7: Syntax error: Operator expected",
+			);
+		}
+	});
+
+	test("Handles querying errors", async () => {
+		await consult("man(bob).");
+		await query("man(bob).");
+	});
+	*/
+});