From 80690b54468a30b300dd4e5587ca115894c65670 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 16 Jul 2018 13:55:04 +0200
Subject: [PATCH] Add :let and :unlet commands to create and remove local
 variables

---
 notebooks/tests/let.ipynb                     | 199 ++++++++++++++++++
 .../java/de/prob2/jupyter/ProBKernel.java     |  11 +
 .../prob2/jupyter/commands/EvalCommand.java   |  25 ++-
 .../de/prob2/jupyter/commands/LetCommand.java |  57 +++++
 .../prob2/jupyter/commands/UnletCommand.java  |  57 +++++
 5 files changed, 347 insertions(+), 2 deletions(-)
 create mode 100644 notebooks/tests/let.ipynb
 create mode 100644 src/main/java/de/prob2/jupyter/commands/LetCommand.java
 create mode 100644 src/main/java/de/prob2/jupyter/commands/UnletCommand.java

diff --git a/notebooks/tests/let.ipynb b/notebooks/tests/let.ipynb
new file mode 100644
index 0000000..60f8b19
--- /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 46846d6..f53df53 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 8d2e75c..46d85b5 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 0000000..df605eb
--- /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 0000000..30af27d
--- /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;
+	}
+}
-- 
GitLab