From 9db68c3ab1e8a1b688691907c1acde58199b3920 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 13 Jan 2020 11:23:42 +0100
Subject: [PATCH] Allow loading machines without an explicit ::load command
This allows typing machine code directly into a cell (just like an
expression or predicate), which is more convenient in most cases.
---
CHANGELOG.md | 1 +
notebooks/tests/load_cell.ipynb | 96 ++++++++++++++-----
.../java/de/prob2/jupyter/ProBKernel.java | 14 ++-
.../prob2/jupyter/kernelspecfiles/kernel.js | 2 +-
4 files changed, 88 insertions(+), 25 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index cba20fc..ffc7986 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -8,6 +8,7 @@
* Added a `:modelcheck` command to run the ProB model checker.
* Added support for additional languages and file extensions. The `:load` command now recognizes all languages and file extensions supported by ProB 2.
* **Note:** Some languages are not fully working yet (for example XTL).
+* Allowed loading B machines by entering their code directly, without an explicit `::load` command, similar to how this is already allowed with expressions.
* Added a `:bsymb` command to load ProB's custom bsymb.sty LaTeX definitions on demand. After this command is executed, bsymb commands can be used in LaTeX formulas in Markdown cells.
* Added support for Java 11.
* Updated ProB 2 to version 3.2.12.
diff --git a/notebooks/tests/load_cell.ipynb b/notebooks/tests/load_cell.ipynb
index 936659a..f122de4 100644
--- a/notebooks/tests/load_cell.ipynb
+++ b/notebooks/tests/load_cell.ipynb
@@ -49,6 +49,28 @@
"Machines can be loaded from code in the notebook."
]
},
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: dinge"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "MACHINE dinge\n",
+ "SETS DINGE = {EINS, ZWEI, DREI, VIER}\n",
+ "END"
+ ]
+ },
{
"cell_type": "code",
"execution_count": 2,
@@ -56,8 +78,11 @@
"outputs": [
{
"data": {
+ "text/markdown": [
+ "$\\{\\mathit{EINS},\\mathit{ZWEI},\\mathit{DREI},\\mathit{VIER}\\}$"
+ ],
"text/plain": [
- "Loaded machine: things"
+ "{EINS,ZWEI,DREI,VIER}"
]
},
"execution_count": 2,
@@ -65,6 +90,33 @@
"output_type": "execute_result"
}
],
+ "source": [
+ "DINGE"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Machines can be loaded with an explicit `::load` command."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: things"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
"source": [
"::load\n",
"MACHINE things\n",
@@ -74,7 +126,7 @@
},
{
"cell_type": "code",
- "execution_count": 3,
+ "execution_count": 4,
"metadata": {},
"outputs": [
{
@@ -86,7 +138,7 @@
"{ONE,TWO,THREE,FOUR}"
]
},
- "execution_count": 3,
+ "execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
@@ -104,7 +156,7 @@
},
{
"cell_type": "code",
- "execution_count": 4,
+ "execution_count": 5,
"metadata": {},
"outputs": [
{
@@ -113,7 +165,7 @@
"Loaded machine: prefs"
]
},
- "execution_count": 4,
+ "execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
@@ -126,7 +178,7 @@
},
{
"cell_type": "code",
- "execution_count": 5,
+ "execution_count": 6,
"metadata": {},
"outputs": [
{
@@ -138,7 +190,7 @@
"{−5,−4,−3,−2,−1,0,1,2,3,4,5}"
]
},
- "execution_count": 5,
+ "execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
@@ -156,7 +208,7 @@
},
{
"cell_type": "code",
- "execution_count": 6,
+ "execution_count": 7,
"metadata": {},
"outputs": [
{
@@ -177,22 +229,22 @@
},
{
"cell_type": "code",
- "execution_count": 7,
+ "execution_count": 8,
"metadata": {
"scrolled": true
},
"outputs": [
{
"ename": "WithSourceCodeException",
- "evalue": "de.prob.exception.ProBError: Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:19)\nError: Identifier 'x' declared twice at (Line:Col[:File]) (Line:2 Col:17) and (Line:2 Col:14) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:19)",
+ "evalue": "de.prob.exception.ProBError: Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\nError: Identifier 'x' declared twice at (Line:Col[:File]) (Line:2 Col:17) and (Line:2 Col:14) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProlog said no.\u001b[0m",
"\u001b[1m\u001b[30m2 errors:\u001b[0m",
- "\u001b[1m\u001b[31mError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:19)\u001b[0m",
- "\u001b[1m\u001b[31mError end column 19 out of bounds (0..17)\u001b[0m",
- "\u001b[1m\u001b[31mError: Identifier 'x' declared twice at (Line:Col[:File]) (Line:2 Col:17) and (Line:2 Col:14) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:19)\u001b[0m",
- "\u001b[1m\u001b[31mError end column 19 out of bounds (0..17)\u001b[0m"
+ "\u001b[1m\u001b[31mError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\u001b[0m",
+ "\u001b[1m\u001b[30m CONSTANTS x, \u001b[0m\u001b[1m\u001b[30m\u001b[41mx\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
+ "\u001b[1m\u001b[31mError: Identifier 'x' declared twice at (Line:Col[:File]) (Line:2 Col:17) and (Line:2 Col:14) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:18)\u001b[0m",
+ "\u001b[1m\u001b[30m CONSTANTS x, \u001b[0m\u001b[1m\u001b[30m\u001b[41mx\u001b[0m\u001b[1m\u001b[30m\u001b[0m"
]
}
],
@@ -206,24 +258,24 @@
},
{
"cell_type": "code",
- "execution_count": 8,
+ "execution_count": 9,
"metadata": {},
"outputs": [
{
"ename": "WithSourceCodeException",
- "evalue": "de.prob.exception.ProBError: Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:14 to 2:16)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\" ^ \"string\" ^ \"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:35 to 5:17)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:19 to 3:26)",
+ "evalue": "de.prob.exception.ProBError: Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:14 to 2:15)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\" ^ \"string\" ^ \"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:35 to 5:18)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:19 to 3:27)",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProlog said no.\u001b[0m",
"\u001b[1m\u001b[30m3 errors:\u001b[0m",
- "\u001b[1m\u001b[31mError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:14 to 2:16)\u001b[0m",
- "\u001b[1m\u001b[31mError end column 16 out of bounds (0..14)\u001b[0m",
- "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\" ^ \"string\" ^ \"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:35 to 5:17)\u001b[0m",
+ "\u001b[1m\u001b[31mError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:14 to 2:15)\u001b[0m",
+ "\u001b[1m\u001b[30m CONSTANTS \u001b[0m\u001b[1m\u001b[30m\u001b[41mx\u001b[0m\u001b[1m\u001b[30m\u001b[0m",
+ "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\" ^ \"string\" ^ \"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:35 to 5:18)\u001b[0m",
"\u001b[1m\u001b[30m PROPERTIES 1 = \"string\" & 1 = (\u001b[0m\u001b[1m\u001b[30m\u001b[41m\"string\"\u001b[0m",
"\u001b[1m\u001b[30m\u001b[41m ^ \"string\"\u001b[0m",
- "\u001b[1m\u001b[30m\u001b[41m ^ \"string\u001b[0m\u001b[1m\u001b[30m\")\u001b[0m",
- "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:19 to 3:26)\u001b[0m",
- "\u001b[1m\u001b[30m PROPERTIES 1 = \u001b[0m\u001b[1m\u001b[30m\u001b[41m\"string\u001b[0m\u001b[1m\u001b[30m\" & 1 = (\"string\"\u001b[0m"
+ "\u001b[1m\u001b[30m\u001b[41m ^ \"string\"\u001b[0m\u001b[1m\u001b[30m)\u001b[0m",
+ "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:19 to 3:27)\u001b[0m",
+ "\u001b[1m\u001b[30m PROPERTIES 1 = \u001b[0m\u001b[1m\u001b[30m\u001b[41m\"string\"\u001b[0m\u001b[1m\u001b[30m & 1 = (\"string\"\u001b[0m"
]
}
],
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index a599d36..a150536 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -277,19 +277,29 @@ public final class ProBKernel extends BaseKernel {
return result;
}
+ private static boolean isMachineCode(final @NotNull String code) {
+ return code.startsWith("MACHINE");
+ }
+
@Override
public @Nullable DisplayData eval(final String expr) {
assert expr != null;
final Matcher commandMatcher = COMMAND_PATTERN.matcher(expr);
if (commandMatcher.matches()) {
+ // The input is a command, execute it directly.
final String name = commandMatcher.group(1);
assert name != null;
final String argString = commandMatcher.group(2) == null ? "" : commandMatcher.group(2);
return this.executeCommand(name, argString);
+ } else if (isMachineCode(expr)) {
+ // The input appears to be a machine, load it.
+ // The leading newline here is important. ::load expects the first input line to contain preference assignments; the actual machine code has to start on the second line.
+ return this.executeCommand("::load", "\n" + expr);
+ } else {
+ // By default, assume that the input is an expression and evaluate it.
+ return this.executeCommand(":eval", expr);
}
-
- return this.executeCommand(":eval", expr);
}
@Override
diff --git a/src/main/resources/de/prob2/jupyter/kernelspecfiles/kernel.js b/src/main/resources/de/prob2/jupyter/kernelspecfiles/kernel.js
index 0a8e0a5..d771df0 100644
--- a/src/main/resources/de/prob2/jupyter/kernelspecfiles/kernel.js
+++ b/src/main/resources/de/prob2/jupyter/kernelspecfiles/kernel.js
@@ -309,7 +309,7 @@ define([
}
return "meta";
} else {
- // No command found, switch to B mode.
+ // No command found, meaning the input is a B machine or expression, so switch to B mode.
switchToMode(state, "classicalb");
return state.innerMode.token(stream, state.innerState);
}
--
GitLab