diff --git a/notebooks/tests/let.ipynb b/notebooks/tests/let.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..60f8b19dfc50c8298cec7546dc90e613323a29cd
--- /dev/null
+++ b/notebooks/tests/let.ipynb
@@ -0,0 +1,199 @@
+{
+ "cells": [
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "```\n",
+ ":let NAME VALUE\n",
+ "```\n",
+ "\n",
+ "Set the value of a local variable.\n",
+ "\n",
+ "Variables are available in all states and are not affected by machine loads. A variable created by `:let` shadows any identifier from the machine with the same name."
+ ],
+ "text/plain": [
+ "```\n",
+ ":let NAME VALUE\n",
+ "```\n",
+ "\n",
+ "Set the value of a local variable.\n",
+ "\n",
+ "Variables are available in all states and are not affected by machine loads. A variable created by `:let` shadows any identifier from the machine with the same name."
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help :let"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "```\n",
+ ":unlet NAME\n",
+ "```\n",
+ "\n",
+ "Remove a local variable."
+ ],
+ "text/plain": [
+ "```\n",
+ ":unlet NAME\n",
+ "```\n",
+ "\n",
+ "Remove a local variable."
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help :unlet"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ ":let hello 1..5 \\/ {10}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{1,2,3,4,5,10\\}$"
+ ],
+ "text/plain": [
+ "{1,2,3,4,5,10}"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "hello"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ ":let n 2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$2$"
+ ],
+ "text/plain": [
+ "2"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{2,4,10\\}$"
+ ],
+ "text/plain": [
+ "{2,4,10}"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{x | x : hello & x mod n = 0}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ ":unlet n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":eval: Computation not completed: Unknown identifier \"n\", the possible completion is \"not\"",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:eval: Computation not completed: Unknown identifier \"n\", the possible completion is \"not\"\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ "n"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "codemirror_mode": "prob2_jupyter_repl",
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob2-jupyter-repl",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 46846d62be6d06eabc93b27381cf26bd0b0cb9aa..f53df53a1e8bd0a8f14d48c2c8c40c46a02ca4f0 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -35,6 +35,7 @@ import de.prob2.jupyter.commands.GotoCommand;
import de.prob2.jupyter.commands.GroovyCommand;
import de.prob2.jupyter.commands.HelpCommand;
import de.prob2.jupyter.commands.InitialiseCommand;
+import de.prob2.jupyter.commands.LetCommand;
import de.prob2.jupyter.commands.LoadCellCommand;
import de.prob2.jupyter.commands.LoadFileCommand;
import de.prob2.jupyter.commands.NoSuchCommandException;
@@ -48,6 +49,7 @@ import de.prob2.jupyter.commands.TableCommand;
import de.prob2.jupyter.commands.TimeCommand;
import de.prob2.jupyter.commands.TraceCommand;
import de.prob2.jupyter.commands.TypeCommand;
+import de.prob2.jupyter.commands.UnletCommand;
import de.prob2.jupyter.commands.VersionCommand;
import de.prob2.jupyter.commands.WithSourceCodeException;
@@ -136,6 +138,7 @@ public final class ProBKernel extends BaseKernel {
private final @NotNull AnimationSelector animationSelector;
private final @NotNull Map<@NotNull String, @NotNull Command> commands;
+ private final @NotNull Map<@NotNull String, @NotNull String> variables;
@Inject
private ProBKernel(final @NotNull Injector injector, final @NotNull ClassicalBFactory classicalBFactory, final @NotNull AnimationSelector animationSelector) {
@@ -152,6 +155,8 @@ public final class ProBKernel extends BaseKernel {
this.commands.put(":type", injector.getInstance(TypeCommand.class));
this.commands.put(":table", injector.getInstance(TableCommand.class));
this.commands.put(":solve", injector.getInstance(SolveCommand.class));
+ this.commands.put(":let", injector.getInstance(LetCommand.class));
+ this.commands.put(":unlet", injector.getInstance(UnletCommand.class));
this.commands.put(":load", injector.getInstance(LoadFileCommand.class));
this.commands.put("::load", injector.getInstance(LoadCellCommand.class));
this.commands.put(":pref", injector.getInstance(PrefCommand.class));
@@ -172,6 +177,8 @@ public final class ProBKernel extends BaseKernel {
this.commands.put("::render", injector.getInstance(RenderCommand.class));
this.commands.put(":prettyprint", injector.getInstance(PrettyPrintCommand.class));
+ this.variables = new HashMap<>();
+
this.animationSelector.changeCurrentAnimation(new Trace(classicalBFactory.create("(initial Jupyter machine)", "MACHINE repl END").load()));
}
@@ -179,6 +186,10 @@ public final class ProBKernel extends BaseKernel {
return Collections.unmodifiableMap(this.commands);
}
+ public @NotNull Map<@NotNull String, @NotNull String> getVariables() {
+ return this.variables;
+ }
+
@Override
public @NotNull String getBanner() {
return "ProB Interactive Expression and Predicate Evaluator (on Jupyter)\nType \":help\" for more information.";
diff --git a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
index 8d2e75cbf664f7dfc3a006762c493b71aabe987e..46d85b5f1dc0e40549d12cff0157b7ddc5bc9871 100644
--- a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
@@ -1,22 +1,30 @@
package de.prob2.jupyter.commands;
+import java.util.Map;
+import java.util.StringJoiner;
+
import com.google.inject.Inject;
+import com.google.inject.Injector;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.statespace.AnimationSelector;
+import de.prob2.jupyter.ProBKernel;
+
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
import org.jetbrains.annotations.NotNull;
public final class EvalCommand implements Command {
+ private final @NotNull Injector injector;
private final @NotNull AnimationSelector animationSelector;
@Inject
- private EvalCommand(final @NotNull AnimationSelector animationSelector) {
+ private EvalCommand(final @NotNull Injector injector, final @NotNull AnimationSelector animationSelector) {
super();
+ this.injector = injector;
this.animationSelector = animationSelector;
}
@@ -38,7 +46,20 @@ public final class EvalCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull String argString) {
- return CommandUtils.displayDataForEvalResult(CommandUtils.withSourceCode(argString, () -> this.animationSelector.getCurrentTrace().evalCurrent(argString, FormulaExpand.EXPAND)));
+ final Map<String, String> variables = this.injector.getInstance(ProBKernel.class).getVariables();
+ final String code;
+ if (variables.isEmpty()) {
+ code = argString;
+ } else {
+ final StringJoiner varNames = new StringJoiner(",");
+ final StringJoiner varAssignments = new StringJoiner("&");
+ variables.forEach((name, value) -> {
+ varNames.add(name);
+ varAssignments.add(name + "=(" + value + ')');
+ });
+ code = String.format("LET %s BE %s IN(%s)END", varNames, varAssignments, argString);
+ }
+ return CommandUtils.displayDataForEvalResult(CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().evalCurrent(code, FormulaExpand.EXPAND)));
}
@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/LetCommand.java b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
new file mode 100644
index 0000000000000000000000000000000000000000..df605eba7ddc920af96c10efeedf0dd5df37dbb8
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
@@ -0,0 +1,57 @@
+package de.prob2.jupyter.commands;
+
+import java.util.List;
+
+import com.google.inject.Inject;
+import com.google.inject.Injector;
+
+import de.prob2.jupyter.ProBKernel;
+import de.prob2.jupyter.UserErrorException;
+
+import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
+import io.github.spencerpark.jupyter.kernel.display.DisplayData;
+
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+public final class LetCommand implements Command {
+ private final @NotNull Injector injector;
+
+ @Inject
+ public LetCommand(final @NotNull Injector injector) {
+ super();
+
+ this.injector = injector;
+ }
+
+ @Override
+ public @NotNull String getSyntax() {
+ return ":let NAME VALUE";
+ }
+
+ @Override
+ public @NotNull String getShortHelp() {
+ return "Set the value of a local variable.";
+ }
+
+ @Override
+ public @NotNull String getHelpBody() {
+ return "Variables are available in all states and are not affected by machine loads. A variable created by `:let` shadows any identifier from the machine with the same name.";
+ }
+
+ @Override
+ public @Nullable DisplayData run(final @NotNull String argString) {
+ final List<String> split = CommandUtils.splitArgs(argString, 2);
+ if (split.size() != 2) {
+ throw new UserErrorException("Expected 2 arguments, not " + split.size());
+ }
+ this.injector.getInstance(ProBKernel.class).getVariables().put(split.get(0), split.get(1));
+ return null;
+ }
+
+ @Override
+ public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
+ // TODO
+ return null;
+ }
+}
diff --git a/src/main/java/de/prob2/jupyter/commands/UnletCommand.java b/src/main/java/de/prob2/jupyter/commands/UnletCommand.java
new file mode 100644
index 0000000000000000000000000000000000000000..30af27d964680acd0c52d6652fc3de14ef1960dc
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/commands/UnletCommand.java
@@ -0,0 +1,57 @@
+package de.prob2.jupyter.commands;
+
+import java.util.Map;
+
+import com.google.inject.Inject;
+import com.google.inject.Injector;
+
+import de.prob2.jupyter.ProBKernel;
+import de.prob2.jupyter.UserErrorException;
+
+import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
+import io.github.spencerpark.jupyter.kernel.display.DisplayData;
+
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+public final class UnletCommand implements Command {
+ private final @NotNull Injector injector;
+
+ @Inject
+ public UnletCommand(final @NotNull Injector injector) {
+ super();
+
+ this.injector = injector;
+ }
+
+ @Override
+ public @NotNull String getSyntax() {
+ return ":unlet NAME";
+ }
+
+ @Override
+ public @NotNull String getShortHelp() {
+ return "Remove a local variable.";
+ }
+
+ @Override
+ public @NotNull String getHelpBody() {
+ return "";
+ }
+
+ @Override
+ public @Nullable DisplayData run(final @NotNull String argString) {
+ final Map<String, String> variables = this.injector.getInstance(ProBKernel.class).getVariables();
+ if (!variables.containsKey(argString)) {
+ throw new UserErrorException("There is no local variable " + argString);
+ }
+ variables.remove(argString);
+ return null;
+ }
+
+ @Override
+ public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
+ // TODO
+ return null;
+ }
+}