diff --git a/CHANGELOG.md b/CHANGELOG.md
index 72a16990f5777255a46c85c35f65493885997e85..67774efcc29a6c92438461c8bcd220941d5a4d18 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,7 @@
## [(next version)](./README.md#for-developers)
* 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).
* 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.
* Significantly refactored the logic for parsing commands and their arguments.
diff --git a/notebooks/tests/language.ipynb b/notebooks/tests/language.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..d28855ad3ca621a55e27a1135795035be1495eef
--- /dev/null
+++ b/notebooks/tests/language.ipynb
@@ -0,0 +1,359 @@
+{
+ "cells": [
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "```\n",
+ ":language [LANGUAGE]\n",
+ "```\n",
+ "\n",
+ "Change the language used to parse formulas entered by the user.\n",
+ "\n",
+ "By default, formulas entered by the user are parsed using the language of the currently loaded model. Using this command, the language can be changed, so that for example formulas in Event-B syntax can be evaluated in the context of a classical B machine.\n",
+ "\n",
+ "Some features will not work correctly when a non-default language is set, such as `DEFINITIONS` from classical B machines."
+ ],
+ "text/plain": [
+ ":language [LANGUAGE]\n",
+ "Change the language used to parse formulas entered by the user.\n",
+ "\n",
+ "By default, formulas entered by the user are parsed using the language of the currently loaded model. Using this command, the language can be changed, so that for example formulas in Event-B syntax can be evaluated in the context of a classical B machine.\n",
+ "\n",
+ "Some features will not work correctly when a non-default language is set, such as `DEFINITIONS` from classical B machines."
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help :language"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The language can be switched when no machine is loaded."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Current language for user input is classical B (default for model)"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":language"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$8$"
+ ],
+ "text/plain": [
+ "8"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "2**3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Changed language for user input to Event-B (forced)"
+ ]
+ },
+ "execution_count": 4,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":language event_b"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":eval: Computation not completed: Type mismatch: Expected POW(_A), but was INTEGER in '2'",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:eval: Computation not completed: Type mismatch: Expected POW(_A), but was INTEGER in '2'\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ "2**3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(2\\mapsto 3)\\}$"
+ ],
+ "text/plain": [
+ "{(2↦3)}"
+ ]
+ },
+ "execution_count": 6,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{2}**{3}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Changed language for user input to classical B (forced)"
+ ]
+ },
+ "execution_count": 7,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":language classical_b"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$8$"
+ ],
+ "text/plain": [
+ "8"
+ ]
+ },
+ "execution_count": 8,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "2**3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Changed language for user input to classical B (default for model)"
+ ]
+ },
+ "execution_count": 9,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":language default"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$8$"
+ ],
+ "text/plain": [
+ "8"
+ ]
+ },
+ "execution_count": 10,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "2**3"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "The language can be switched when a classical B machine is loaded."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Loaded machine: things"
+ ]
+ },
+ "execution_count": 11,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":load things.mch"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\mathit{ONE},\\mathit{TWO}\\}$"
+ ],
+ "text/plain": [
+ "{ONE,TWO}"
+ ]
+ },
+ "execution_count": 12,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{ONE, TWO}"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "Changed language for user input to Event-B (forced)"
+ ]
+ },
+ "execution_count": 13,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":language event_b"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Identifiers from the machine can still be accessed when using a non-default language."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{(\\mathit{ONE}\\mapsto \\mathit{TWO})\\}$"
+ ],
+ "text/plain": [
+ "{(ONE↦TWO)}"
+ ]
+ },
+ "execution_count": 14,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ "{ONE}**{TWO}"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "TODO: Test switching language when a non-classical-B file is loaded (Event-B, TLA, CSP, Z, etc.)"
+ ]
+ }
+ ],
+ "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": 4
+}
diff --git a/src/main/java/de/prob2/jupyter/CommandUtils.java b/src/main/java/de/prob2/jupyter/CommandUtils.java
index 7cb21e06bacfbcd9da9007d9e67c3b3a17387135..4f199cf7e995d498207b0e3ac5626fdc51a5cd95 100644
--- a/src/main/java/de/prob2/jupyter/CommandUtils.java
+++ b/src/main/java/de/prob2/jupyter/CommandUtils.java
@@ -374,6 +374,7 @@ public final class CommandUtils {
return null;
}
final String identifier = identifierMatcher.group();
+ // TODO Handle non-default languages (i. e. forced classical B or Event-B parsing) - important for the different meaning of INT in classical B vs. Event-B
final IEvalElement formula = trace.getModel().parseFormula(identifier, FormulaExpand.TRUNCATE);
final TypeCheckResult type = trace.getStateSpace().typeCheck(formula);
final AbstractEvalResult currentValue = trace.evalCurrent(formula);
diff --git a/src/main/java/de/prob2/jupyter/FormulaLanguage.java b/src/main/java/de/prob2/jupyter/FormulaLanguage.java
new file mode 100644
index 0000000000000000000000000000000000000000..6f85e01ab8f8a310da0de1ca21e4f81221add975
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/FormulaLanguage.java
@@ -0,0 +1,8 @@
+package de.prob2.jupyter;
+
+public enum FormulaLanguage {
+ DEFAULT,
+ CLASSICAL_B,
+ EVENT_B,
+ ;
+}
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 66ffbd6c6a4b9dec747ec4a6ee331d91544b3ea5..c8ba0adea04a33338d2aa4ec66b83e4039e70272 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -34,8 +34,11 @@ import com.google.inject.Injector;
import com.google.inject.Singleton;
import de.prob.animator.ReusableAnimator;
+import de.prob.animator.domainobjects.ClassicalB;
import de.prob.animator.domainobjects.ErrorItem;
+import de.prob.animator.domainobjects.EventB;
import de.prob.animator.domainobjects.FormulaExpand;
+import de.prob.animator.domainobjects.IEvalElement;
import de.prob.exception.ProBError;
import de.prob.scripting.ClassicalBFactory;
import de.prob.statespace.AnimationSelector;
@@ -55,6 +58,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.LanguageCommand;
import de.prob2.jupyter.commands.LetCommand;
import de.prob2.jupyter.commands.LoadCellCommand;
import de.prob2.jupyter.commands.LoadFileCommand;
@@ -153,6 +157,7 @@ public final class ProBKernel extends BaseKernel {
GroovyCommand.class,
HelpCommand.class,
InitialiseCommand.class,
+ LanguageCommand.class,
LetCommand.class,
LoadCellCommand.class,
LoadFileCommand.class,
@@ -242,6 +247,7 @@ public final class ProBKernel extends BaseKernel {
private final @NotNull Map<@NotNull String, @NotNull String> variables;
private @NotNull Path currentMachineDirectory;
+ private @NotNull FormulaLanguage currentFormulaLanguage;
private @Nullable String currentCellSourceCode;
@Inject
@@ -262,7 +268,10 @@ public final class ProBKernel extends BaseKernel {
this.currentCommandFuture = new AtomicReference<>(Futures.immediateCancelledFuture());
this.variables = new HashMap<>();
+ // These variables need to be initialized here,
+ // but they will be overwritten immediately by the switchMachine call.
this.currentMachineDirectory = Paths.get("");
+ this.currentFormulaLanguage = FormulaLanguage.DEFAULT;
this.currentCellSourceCode = null;
this.switchMachine(Paths.get(""), null, this::loadDefaultMachine);
}
@@ -295,6 +304,14 @@ public final class ProBKernel extends BaseKernel {
this.currentMachineDirectory = currentMachineDirectory;
}
+ public @NotNull FormulaLanguage getCurrentFormulaLanguage() {
+ return this.currentFormulaLanguage;
+ }
+
+ public void setCurrentFormulaLanguage(final @NotNull FormulaLanguage currentFormulaLanguage) {
+ this.currentFormulaLanguage = currentFormulaLanguage;
+ }
+
public void unloadMachine() {
final Trace oldTrace = this.animationSelector.getCurrentTrace();
if (oldTrace != null) {
@@ -312,6 +329,7 @@ public final class ProBKernel extends BaseKernel {
public void switchMachine(final @NotNull Path machineDirectory, final @Nullable String cellSourceCode, final @NotNull Function<@NotNull StateSpace, @NotNull Trace> newTraceCreator) {
this.unloadMachine();
+ this.setCurrentFormulaLanguage(FormulaLanguage.DEFAULT);
this.currentCellSourceCode = cellSourceCode;
final StateSpace newStateSpace = this.animator.createStateSpace();
try {
@@ -325,6 +343,30 @@ public final class ProBKernel extends BaseKernel {
this.setCurrentMachineDirectory(machineDirectory);
}
+ /**
+ * Parse the given formula code into an {@link IEvalElement}.
+ * The language used for parsing depends on the current formula language (see {@link #getCurrentFormulaLanguage()}.
+ *
+ * @param code the formula code
+ * @param expand the expansion mode to use when evaluating the formula
+ * @return the parsed formula
+ */
+ public IEvalElement parseFormula(final String code, final FormulaExpand expand) {
+ switch (this.getCurrentFormulaLanguage()) {
+ case DEFAULT:
+ return this.animationSelector.getCurrentTrace().getModel().parseFormula(code, expand);
+
+ case CLASSICAL_B:
+ return new ClassicalB(code, expand);
+
+ case EVENT_B:
+ return new EventB(code, expand);
+
+ default:
+ throw new AssertionError("Unhandled formula parse mode: " + this.getCurrentFormulaLanguage());
+ }
+ }
+
public @NotNull DisplayData executeOperation(final @NotNull String name, final @Nullable String predicate) {
final Trace trace = this.animationSelector.getCurrentTrace();
final String translatedOpName = Transition.unprettifyName(name);
diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index 9b8a8be7362f7eda50e9fae2e7979fb99370a65d..b87904640f83af41c08295fecfcc1244f5fc97d2 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
@@ -8,6 +8,7 @@ import com.google.inject.Provider;
import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.EvalResult;
import de.prob.animator.domainobjects.FormulaExpand;
+import de.prob.animator.domainobjects.IEvalElement;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
@@ -67,8 +68,10 @@ public final class AssertCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
- final String code = this.kernelProvider.get().insertLetVariables(args.get(FORMULA_PARAM));
- final AbstractEvalResult result = CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().evalCurrent(code, FormulaExpand.TRUNCATE));
+ final ProBKernel kernel = this.kernelProvider.get();
+ final String code = kernel.insertLetVariables(args.get(FORMULA_PARAM));
+ final IEvalElement formula = kernel.parseFormula(code, FormulaExpand.TRUNCATE);
+ final AbstractEvalResult result = CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().evalCurrent(formula));
if (result instanceof EvalResult && "TRUE".equals(((EvalResult)result).getValue())) {
// Use EvalResult.TRUE instead of the real result so that solution variables are not displayed.
return CommandUtils.displayDataForEvalResult(EvalResult.TRUE);
diff --git a/src/main/java/de/prob2/jupyter/commands/DotCommand.java b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
index 321fa101a2356baedc2157f830a15611be60928b..98cbedfda173a0b5a068ef2ac96e9e8521b2d433 100644
--- a/src/main/java/de/prob2/jupyter/commands/DotCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
@@ -95,8 +95,9 @@ public final class DotCommand implements Command {
final List<IEvalElement> dotCommandArgs;
final String code;
if (args.get(FORMULA_PARAM).isPresent()) {
- code = this.kernelProvider.get().insertLetVariables(args.get(FORMULA_PARAM).get());
- final IEvalElement formula = CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().getModel().parseFormula(code, FormulaExpand.EXPAND));
+ final ProBKernel kernel = this.kernelProvider.get();
+ code = kernel.insertLetVariables(args.get(FORMULA_PARAM).get());
+ final IEvalElement formula = CommandUtils.withSourceCode(code, () -> kernel.parseFormula(code, FormulaExpand.EXPAND));
dotCommandArgs = Collections.singletonList(formula);
} else {
code = null;
diff --git a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
index ee8e47021bbc49aa89c0438cb3096b1492725e98..add281adcfa5d8a5961020dd36f81b9ffc4ceed7 100644
--- a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
@@ -6,6 +6,7 @@ import com.google.inject.Inject;
import com.google.inject.Injector;
import de.prob.animator.domainobjects.FormulaExpand;
+import de.prob.animator.domainobjects.IEvalElement;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
@@ -62,8 +63,10 @@ public final class EvalCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
- final String code = this.injector.getInstance(ProBKernel.class).insertLetVariables(args.get(FORMULA_PARAM));
- return CommandUtils.displayDataForEvalResult(CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().evalCurrent(code, FormulaExpand.EXPAND)));
+ final ProBKernel kernel = this.injector.getInstance(ProBKernel.class);
+ final String code = kernel.insertLetVariables(args.get(FORMULA_PARAM));
+ final IEvalElement formula = kernel.parseFormula(code, FormulaExpand.EXPAND);
+ return CommandUtils.displayDataForEvalResult(CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().evalCurrent(formula)));
}
@Override
diff --git a/src/main/java/de/prob2/jupyter/commands/FindCommand.java b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
index 8e2beb04845c11112f15781139cb494dc8c2dd8b..df91c04775b9e28839cadee5e9d9ceda4d793c91 100644
--- a/src/main/java/de/prob2/jupyter/commands/FindCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
@@ -64,10 +64,11 @@ public final class FindCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final ProBKernel kernel = this.kernelProvider.get();
final Trace trace = this.animationSelector.getCurrentTrace();
- final String code = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM));
+ final String code = kernel.insertLetVariables(args.get(PREDICATE_PARAM));
final Trace newTrace = CommandUtils.withSourceCode(code, () -> {
- final IEvalElement pred = trace.getModel().parseFormula(code, FormulaExpand.EXPAND);
+ final IEvalElement pred = kernel.parseFormula(code, FormulaExpand.EXPAND);
return trace.getStateSpace().getTraceToState(pred);
});
this.animationSelector.changeCurrentAnimation(newTrace);
diff --git a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
index 7b78a10859ef38441064cb5ccf710b6254cd0d42..ff190c0dc7ccfbad3c274059756dea24d57bb558 100644
--- a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
@@ -40,7 +40,8 @@ public final class HelpCommand implements Command {
PrettyPrintCommand.class,
LetCommand.class,
UnletCommand.class,
- AssertCommand.class
+ AssertCommand.class,
+ LanguageCommand.class
)));
commandCategories.put("Animation", Collections.unmodifiableList(Arrays.asList(
LoadCellCommand.class,
diff --git a/src/main/java/de/prob2/jupyter/commands/LanguageCommand.java b/src/main/java/de/prob2/jupyter/commands/LanguageCommand.java
new file mode 100644
index 0000000000000000000000000000000000000000..43dbcf51983fcb1fa28df6e331266abde5551b56
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/commands/LanguageCommand.java
@@ -0,0 +1,152 @@
+package de.prob2.jupyter.commands;
+
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.Optional;
+import java.util.stream.Collectors;
+
+import com.google.inject.Inject;
+import com.google.inject.Provider;
+
+import de.prob.model.eventb.EventBModel;
+import de.prob.model.representation.AbstractModel;
+import de.prob.statespace.AnimationSelector;
+import de.prob.statespace.FormalismType;
+import de.prob.statespace.Trace;
+import de.prob2.jupyter.Command;
+import de.prob2.jupyter.FormulaLanguage;
+import de.prob2.jupyter.Parameter;
+import de.prob2.jupyter.ParameterCompleters;
+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.ReplacementOptions;
+import io.github.spencerpark.jupyter.kernel.display.DisplayData;
+
+import org.jetbrains.annotations.NotNull;
+
+public final class LanguageCommand implements Command {
+ private static final @NotNull Parameter.OptionalSingle LANGUAGE_PARAM = Parameter.optional("language");
+
+ private static final @NotNull Map<@NotNull String, @NotNull FormulaLanguage> LANGUAGE_BY_IDENTIFIER_MAP;
+ static {
+ final Map<String, FormulaLanguage> languageByIdentifierMap = new HashMap<>();
+ languageByIdentifierMap.put("default", FormulaLanguage.DEFAULT);
+ languageByIdentifierMap.put("classical_b", FormulaLanguage.CLASSICAL_B);
+ languageByIdentifierMap.put("event_b", FormulaLanguage.EVENT_B);
+ LANGUAGE_BY_IDENTIFIER_MAP = Collections.unmodifiableMap(languageByIdentifierMap);
+ }
+
+ private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
+ private final @NotNull AnimationSelector animationSelector;
+
+ @Inject
+ private LanguageCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final @NotNull AnimationSelector animationSelector) {
+ super();
+
+ this.kernelProvider = kernelProvider;
+ this.animationSelector = animationSelector;
+ }
+
+ @Override
+ public @NotNull String getName() {
+ return ":language";
+ }
+
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(LANGUAGE_PARAM));
+ }
+
+ @Override
+ public @NotNull String getSyntax() {
+ return ":language [LANGUAGE]";
+ }
+
+ @Override
+ public @NotNull String getShortHelp() {
+ return "Change the language used to parse formulas entered by the user.";
+ }
+
+ @Override
+ public @NotNull String getHelpBody() {
+ return "By default, formulas entered by the user are parsed using the language of the currently loaded model. Using this command, the language can be changed, so that for example formulas in Event-B syntax can be evaluated in the context of a classical B machine.\n\nSome features will not work correctly when a non-default language is set, such as `DEFINITIONS` from classical B machines.";
+ }
+
+ private static @NotNull String describeLanguage(final FormulaLanguage language, final AbstractModel model) {
+ switch (language) {
+ case DEFAULT:
+ final FormalismType formalismType = model.getFormalismType();
+ final String languageName;
+ if (model instanceof EventBModel) {
+ languageName = "Event-B";
+ } else if (formalismType == FormalismType.CSP) {
+ languageName = "CSP";
+ } else if (formalismType == FormalismType.B || formalismType == FormalismType.Z) {
+ // Languages that ProB internally translates to B, such as TLA and Alloy,
+ // have their formalism type set to B.
+ // For such models, only the model itself is translated to B.
+ // Formulas passed to model.parseFormula must be in classical B syntax,
+ // not the original language of the model.
+ // Z models are also internally translated to classical B,
+ // but currently have their own formalism type in ProB 2 (FIXME?).
+ languageName = "classical B";
+ } else {
+ // Fallback for future formalism types
+ languageName = "unknown (" + formalismType + ")";
+ }
+ return languageName + " (default for model)";
+
+ case CLASSICAL_B:
+ return "classical B (forced)";
+
+ case EVENT_B:
+ return "Event-B (forced)";
+
+ default:
+ throw new AssertionError("Unhandled formula language: " + language);
+ }
+ }
+
+ @Override
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final Optional<String> languageName = args.get(LANGUAGE_PARAM);
+ final ProBKernel kernel = this.kernelProvider.get();
+ final Trace trace = this.animationSelector.getCurrentTrace();
+ if (languageName.isPresent()) {
+ if (!LANGUAGE_BY_IDENTIFIER_MAP.containsKey(languageName.get())) {
+ throw new UserErrorException("Unknown language: " + languageName.get());
+ }
+ final FormulaLanguage language = LANGUAGE_BY_IDENTIFIER_MAP.get(languageName.get());
+ kernel.setCurrentFormulaLanguage(language);
+ return new DisplayData("Changed language for user input to " + describeLanguage(language, trace.getModel()));
+ } else {
+ final FormulaLanguage language = kernel.getCurrentFormulaLanguage();
+ return new DisplayData("Current language for user input is " + describeLanguage(language, trace.getModel()));
+ }
+ }
+
+ @Override
+ public @NotNull ParameterInspectors getParameterInspectors() {
+ return ParameterInspectors.NONE;
+ }
+
+ @Override
+ public @NotNull ParameterCompleters getParameterCompleters() {
+ return new ParameterCompleters(Collections.singletonMap(
+ LANGUAGE_PARAM, (argString, at) -> {
+ final String prefix = argString.substring(0, at);
+ final List<String> replacements = LANGUAGE_BY_IDENTIFIER_MAP.keySet()
+ .stream()
+ .filter(s -> s.startsWith(prefix))
+ .collect(Collectors.toList());
+ return new ReplacementOptions(replacements, 0, argString.length());
+ }
+ ));
+ }
+}
diff --git a/src/main/java/de/prob2/jupyter/commands/LetCommand.java b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
index dbe689bb3bd2c0e74e588f4692c53ff0197a6d9a..7e4a10e604cb61ecdee2801cae2c189078fcd18b 100644
--- a/src/main/java/de/prob2/jupyter/commands/LetCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
@@ -8,6 +8,7 @@ import com.google.inject.Provider;
import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.EvalResult;
import de.prob.animator.domainobjects.FormulaExpand;
+import de.prob.animator.domainobjects.IEvalElement;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
@@ -67,10 +68,12 @@ public final class LetCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final String name = args.get(NAME_PARAM);
- final String expr = this.kernelProvider.get().insertLetVariables(args.get(EXPRESSION_PARAM));
- final AbstractEvalResult evaluated = CommandUtils.withSourceCode(expr, () -> this.animationSelector.getCurrentTrace().evalCurrent(expr, FormulaExpand.EXPAND));
+ final ProBKernel kernel = this.kernelProvider.get();
+ final String expr = kernel.insertLetVariables(args.get(EXPRESSION_PARAM));
+ final IEvalElement formula = kernel.parseFormula(expr, FormulaExpand.EXPAND);
+ final AbstractEvalResult evaluated = CommandUtils.withSourceCode(expr, () -> this.animationSelector.getCurrentTrace().evalCurrent(formula));
if (evaluated instanceof EvalResult) {
- this.kernelProvider.get().getVariables().put(name, evaluated.toString());
+ kernel.getVariables().put(name, evaluated.toString());
}
return CommandUtils.displayDataForEvalResult(evaluated);
}
diff --git a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
index 45b6493e59e97b4dfd12f89efb46730ea7f033af..e8f0fa78aa32ebcc6215ca94c045324b22870da7 100644
--- a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
@@ -3,6 +3,7 @@ package de.prob2.jupyter.commands;
import java.util.Collections;
import com.google.inject.Inject;
+import com.google.inject.Provider;
import de.prob.animator.command.PrettyPrintFormulaCommand;
import de.prob.animator.domainobjects.FormulaExpand;
@@ -15,6 +16,7 @@ import de.prob2.jupyter.ParameterCompleters;
import de.prob2.jupyter.ParameterInspectors;
import de.prob2.jupyter.Parameters;
import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -23,12 +25,14 @@ import org.jetbrains.annotations.NotNull;
public final class PrettyPrintCommand implements Command {
private static final @NotNull Parameter.RequiredSingle PREDICATE_PARAM = Parameter.requiredRemainder("predicate");
+ private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final AnimationSelector animationSelector;
@Inject
- private PrettyPrintCommand(final AnimationSelector animationSelector) {
+ private PrettyPrintCommand(final @NotNull Provider<@NotNull ProBKernel> kernelProvider, final AnimationSelector animationSelector) {
super();
+ this.kernelProvider = kernelProvider;
this.animationSelector = animationSelector;
}
@@ -61,7 +65,7 @@ public final class PrettyPrintCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final String code = args.get(PREDICATE_PARAM);
- final IEvalElement formula = this.animationSelector.getCurrentTrace().getModel().parseFormula(code, FormulaExpand.EXPAND);
+ final IEvalElement formula = this.kernelProvider.get().parseFormula(code, FormulaExpand.EXPAND);
final PrettyPrintFormulaCommand cmdUnicode = new PrettyPrintFormulaCommand(formula, PrettyPrintFormulaCommand.Mode.UNICODE);
cmdUnicode.setOptimize(false);
diff --git a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
index 8d01043072bc16780849a0f9d587cae5408c2ce7..028758ed5f8c2316b86e3fe9b9102609b772ec37 100644
--- a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
@@ -80,13 +80,14 @@ public final class SolveCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final ProBKernel kernel = this.kernelProvider.get();
final Trace trace = this.animationSelector.getCurrentTrace();
final CbcSolveCommand.Solvers solver = SOLVERS.get(args.get(SOLVER_PARAM));
if (solver == null) {
throw new UserErrorException("Unknown solver: " + args.get(SOLVER_PARAM));
}
- final String code = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM));
- final IEvalElement predicate = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
+ final String code = kernel.insertLetVariables(args.get(PREDICATE_PARAM));
+ final IEvalElement predicate = CommandUtils.withSourceCode(code, () -> kernel.parseFormula(code, FormulaExpand.EXPAND));
final CbcSolveCommand cmd = new CbcSolveCommand(predicate, solver, this.animationSelector.getCurrentTrace().getCurrentState());
trace.getStateSpace().execute(cmd);
diff --git a/src/main/java/de/prob2/jupyter/commands/TableCommand.java b/src/main/java/de/prob2/jupyter/commands/TableCommand.java
index ea1049fffb22216216172a07ed937d11e7f8b19e..d2d75c0c43ed0c1da0a4584db617ddace15dad80 100644
--- a/src/main/java/de/prob2/jupyter/commands/TableCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TableCommand.java
@@ -70,9 +70,10 @@ public final class TableCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final ProBKernel kernel = this.kernelProvider.get();
final Trace trace = this.animationSelector.getCurrentTrace();
- final String code = this.kernelProvider.get().insertLetVariables(args.get(EXPRESSION_PARAM));
- final IEvalElement formula = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
+ final String code = kernel.insertLetVariables(args.get(EXPRESSION_PARAM));
+ final IEvalElement formula = CommandUtils.withSourceCode(code, () -> kernel.parseFormula(code, FormulaExpand.EXPAND));
final GetAllTableCommands cmd1 = new GetAllTableCommands(trace.getCurrentState());
trace.getStateSpace().execute(cmd1);
diff --git a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
index 09e466fb940bc9121cfa13e698634b83ad842678..dc5da6d24b6f280438aa51cd807f779050709b7d 100644
--- a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
@@ -65,9 +65,10 @@ public final class TypeCommand implements Command {
@Override
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final ProBKernel kernel = this.kernelProvider.get();
final Trace trace = this.animationSelector.getCurrentTrace();
- final String code = this.kernelProvider.get().insertLetVariables(args.get(FORMULA_PARAM));
- final IEvalElement formula = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
+ final String code = kernel.insertLetVariables(args.get(FORMULA_PARAM));
+ final IEvalElement formula = CommandUtils.withSourceCode(code, () -> kernel.parseFormula(code, FormulaExpand.EXPAND));
final TypeCheckResult result = trace.getStateSpace().typeCheck(formula);
if (result.isOk()) {
return new DisplayData(result.getType());