From 6b8d6bb6d3c627e2f48a636bcc78ed304aa1e582 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Thu, 5 Nov 2020 18:37:39 +0100
Subject: [PATCH] Allow switching the language used to parse formulas input by
the user
This doesn't affect predicates passed to :exec/:constants/:init yet,
because ProB 2's StateSpace.transitionFromPredicate method currently
only accepts a string predicate (which is parsed using the model's
languate) and not an arbitrary IEvalElement.
---
CHANGELOG.md | 1 +
notebooks/tests/language.ipynb | 359 ++++++++++++++++++
.../java/de/prob2/jupyter/CommandUtils.java | 1 +
.../de/prob2/jupyter/FormulaLanguage.java | 8 +
.../java/de/prob2/jupyter/ProBKernel.java | 42 ++
.../prob2/jupyter/commands/AssertCommand.java | 7 +-
.../de/prob2/jupyter/commands/DotCommand.java | 5 +-
.../prob2/jupyter/commands/EvalCommand.java | 7 +-
.../prob2/jupyter/commands/FindCommand.java | 5 +-
.../prob2/jupyter/commands/HelpCommand.java | 3 +-
.../jupyter/commands/LanguageCommand.java | 152 ++++++++
.../de/prob2/jupyter/commands/LetCommand.java | 9 +-
.../jupyter/commands/PrettyPrintCommand.java | 8 +-
.../prob2/jupyter/commands/SolveCommand.java | 5 +-
.../prob2/jupyter/commands/TableCommand.java | 5 +-
.../prob2/jupyter/commands/TypeCommand.java | 5 +-
16 files changed, 602 insertions(+), 20 deletions(-)
create mode 100644 notebooks/tests/language.ipynb
create mode 100644 src/main/java/de/prob2/jupyter/FormulaLanguage.java
create mode 100644 src/main/java/de/prob2/jupyter/commands/LanguageCommand.java
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 72a1699..67774ef 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 0000000..d28855a
--- /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 7cb21e0..4f199cf 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 0000000..6f85e01
--- /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 66ffbd6..c8ba0ad 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 9b8a8be..b879046 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 321fa10..98cbedf 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 ee8e470..add281a 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 8e2beb0..df91c04 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 7b78a10..ff190c0 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 0000000..43dbcf5
--- /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 dbe689b..7e4a10e 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 45b6493..e8f0fa7 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 8d01043..028758e 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 ea1049f..d2d75c0 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 09e466f..dc5da6d 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());
--
GitLab