diff --git a/CHANGELOG.md b/CHANGELOG.md index d7e0fc5a882844b87f6c2d901c67db930330c2de..2fa39f0ddc98faec5f8b39d077e8964b079331df 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,7 @@ * Added support for Java 17. * Updated ProB 2 to version 4.0.0-SNAPSHOT. * Added a `:language` command to allow changing the language used to parse user input. For example `:language event_b` can be used to switch to Event-B syntax when a non-Event-B machine is loaded (or no machine at all). +* Made `:let` syntax more flexible: both `:let name value` and `:let name=value` are now allowed. * Improved the performance of loading machines by reusing the existing instance of ProB instead of starting a new one for each machine. * Improved error highlighting for machines loaded from files and not from the notebook. * Local variables (created using `:let`) are now discarded when a new machine is loaded. Previously local variables would be remembered even across machine loads, which could lead to confusing behavior and errors. diff --git a/notebooks/tests/let.ipynb b/notebooks/tests/let.ipynb index 1b4533e23df7297ad17be6f0fa602d7c285ee896..42303a03033289e6aad77e38666201985bf9731f 100644 --- a/notebooks/tests/let.ipynb +++ b/notebooks/tests/let.ipynb @@ -10,6 +10,7 @@ "text/markdown": [ "```\n", ":let NAME EXPR\n", + ":let NAME=EXPR\n", "```\n", "\n", "Evaluate an expression and store it in a local variable.\n", @@ -22,6 +23,7 @@ ], "text/plain": [ ":let NAME EXPR\n", + ":let NAME=EXPR\n", "Evaluate an expression and store it in a local variable.\n", "\n", "The expression is evaluated once in the current state, and its value is stored. Once set, variables are available in all states. A variable created by `:let` shadows any identifier with the same name from the machine.\n", @@ -199,10 +201,10 @@ "outputs": [ { "ename": "CommandExecutionException", - "evalue": ":eval: Computation not completed: Unknown identifier \"n\", the possible completion is \"not\"", + "evalue": ":eval: Computation not completed: Unknown identifier \"n\", did you mean \"IN\"?", "output_type": "error", "traceback": [ - "\u001b[1m\u001b[31m:eval: Computation not completed: Unknown identifier \"n\", the possible completion is \"not\"\u001b[0m" + "\u001b[1m\u001b[31m:eval: Computation not completed: Unknown identifier \"n\", did you mean \"IN\"?\u001b[0m" ] } ], @@ -360,7 +362,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Local variables can be used in Event-B mode." + "Local variables can be assigned with or without `=`." ] }, { @@ -370,8 +372,11 @@ "outputs": [ { "data": { + "text/markdown": [ + "$1$" + ], "text/plain": [ - "Changed language for user input to Event-B (forced)" + "1" ] }, "execution_count": 16, @@ -380,13 +385,167 @@ } ], "source": [ - ":language event_b" + ":let x 1" ] }, { "cell_type": "code", "execution_count": 17, "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$2$" + ], + "text/plain": [ + "2" + ] + }, + "execution_count": 17, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":let y=2" + ] + }, + { + "cell_type": "code", + "execution_count": 18, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$" + ], + "text/plain": [ + "TRUE" + ] + }, + "execution_count": 18, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":assert x + 1 = y" + ] + }, + { + "cell_type": "code", + "execution_count": 19, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{0,2,4,6,8,10\\}$" + ], + "text/plain": [ + "{0,2,4,6,8,10}" + ] + }, + "execution_count": 19, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":let X {x | x : 0..10 & x mod 2 = 0}" + ] + }, + { + "cell_type": "code", + "execution_count": 20, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\{0,2,4,6,8,10\\}$" + ], + "text/plain": [ + "{0,2,4,6,8,10}" + ] + }, + "execution_count": 20, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":let Y={x | x : 0..10 & x mod 2 = 0}" + ] + }, + { + "cell_type": "code", + "execution_count": 21, + "metadata": {}, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$\n", + "\n", + "**Solution:**\n", + "* $\\mathit{x} = 1$\n", + "* $\\mathit{X} = \\{0,2,4,6,8,10\\}$\n", + "* $\\mathit{y} = 2$\n", + "* $\\mathit{Y} = \\{0,2,4,6,8,10\\}$" + ], + "text/plain": [ + "TRUE\n", + "\n", + "Solution:\n", + "\tx = 1\n", + "\tX = {0,2,4,6,8,10}\n", + "\ty = 2\n", + "\tY = {0,2,4,6,8,10}" + ] + }, + "execution_count": 21, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "X = Y" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Local variables can be used in Event-B mode." + ] + }, + { + "cell_type": "code", + "execution_count": 22, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "Changed language for user input to Event-B (forced)" + ] + }, + "execution_count": 22, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + ":language event_b" + ] + }, + { + "cell_type": "code", + "execution_count": 23, + "metadata": {}, "outputs": [ { "data": { @@ -397,7 +556,7 @@ "{1,2,3,4,5,10}" ] }, - "execution_count": 17, + "execution_count": 23, "metadata": {}, "output_type": "execute_result" } @@ -408,7 +567,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 24, "metadata": {}, "outputs": [ { @@ -420,7 +579,7 @@ "{1,2,3,4,5,10}" ] }, - "execution_count": 18, + "execution_count": 24, "metadata": {}, "output_type": "execute_result" } @@ -431,7 +590,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 25, "metadata": {}, "outputs": [ { @@ -443,7 +602,7 @@ "{1,2,3,4,5,10}" ] }, - "execution_count": 19, + "execution_count": 25, "metadata": {}, "output_type": "execute_result" } @@ -454,7 +613,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 26, "metadata": {}, "outputs": [ { @@ -466,7 +625,7 @@ "FALSE" ] }, - "execution_count": 20, + "execution_count": 26, "metadata": {}, "output_type": "execute_result" } @@ -477,7 +636,7 @@ }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 27, "metadata": {}, "outputs": [ { @@ -489,7 +648,7 @@ "TRUE" ] }, - "execution_count": 21, + "execution_count": 27, "metadata": {}, "output_type": "execute_result" } @@ -500,7 +659,7 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": 28, "metadata": {}, "outputs": [ { @@ -518,7 +677,7 @@ "\tA = {0,1}" ] }, - "execution_count": 22, + "execution_count": 28, "metadata": {}, "output_type": "execute_result" } diff --git a/src/main/java/de/prob2/jupyter/commands/LetCommand.java b/src/main/java/de/prob2/jupyter/commands/LetCommand.java index 1ee993dcfb85d4701575bf4e25e3b0f750049918..e591444456dbc714b17c929ec9d870b255ea0138 100644 --- a/src/main/java/de/prob2/jupyter/commands/LetCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/LetCommand.java @@ -1,6 +1,7 @@ package de.prob2.jupyter.commands; -import java.util.Arrays; +import java.util.Collections; +import java.util.regex.Pattern; import com.google.inject.Inject; import com.google.inject.Provider; @@ -18,14 +19,16 @@ import de.prob2.jupyter.ParameterInspectors; import de.prob2.jupyter.Parameters; import de.prob2.jupyter.ParsedArguments; import de.prob2.jupyter.ProBKernel; +import de.prob2.jupyter.UserErrorException; import io.github.spencerpark.jupyter.kernel.display.DisplayData; import org.jetbrains.annotations.NotNull; public final class LetCommand implements Command { - private static final @NotNull Parameter.RequiredSingle NAME_PARAM = Parameter.required("name"); - private static final @NotNull Parameter.RequiredSingle EXPRESSION_PARAM = Parameter.requiredRemainder("expression"); + private static final @NotNull Parameter.RequiredSingle NAME_AND_EXPRESSION = Parameter.requiredRemainder("nameAndExpression"); + + private static final @NotNull Pattern NAME_AND_EXPRESSION_SPLIT_PATTERN = Pattern.compile("=|\\s+"); private final @NotNull Provider<@NotNull ProBKernel> kernelProvider; private final @NotNull AnimationSelector animationSelector; @@ -45,12 +48,12 @@ public final class LetCommand implements Command { @Override public @NotNull Parameters getParameters() { - return new Parameters(Arrays.asList(NAME_PARAM, EXPRESSION_PARAM)); + return new Parameters(Collections.singletonList(NAME_AND_EXPRESSION)); } @Override public @NotNull String getSyntax() { - return ":let NAME EXPR"; + return ":let NAME EXPR\n:let NAME=EXPR"; } @Override @@ -67,9 +70,15 @@ public final class LetCommand implements Command { @Override public @NotNull DisplayData run(final @NotNull ParsedArguments args) { - final String name = args.get(NAME_PARAM); + final String[] split = NAME_AND_EXPRESSION_SPLIT_PATTERN.split(args.get(NAME_AND_EXPRESSION), 2); + if (split.length != 2) { + throw new UserErrorException("Missing variable value"); + } + final String name = split[0]; + final String expression = split[1]; + final ProBKernel kernel = this.kernelProvider.get(); - final IEvalElement formula = kernel.parseFormula(args.get(EXPRESSION_PARAM), FormulaExpand.EXPAND); + final IEvalElement formula = kernel.parseFormula(expression, FormulaExpand.EXPAND); final AbstractEvalResult evaluated = CommandUtils.withSourceCode(formula, () -> kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula)) );