From c7674844e7be35a4e66208b8de45f8f1ca17248e Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Sun, 5 Jun 2022 23:45:11 +0200
Subject: [PATCH] Use new ProB 2 Language class instead of custom
FormulaLanguage
---
notebooks/tests/language.ipynb | 9 ++-
.../de/prob2/jupyter/FormulaLanguage.java | 8 --
.../java/de/prob2/jupyter/ProBKernel.java | 39 +++++-----
.../jupyter/commands/LanguageCommand.java | 78 +++++++++----------
4 files changed, 63 insertions(+), 71 deletions(-)
delete mode 100644 src/main/java/de/prob2/jupyter/FormulaLanguage.java
diff --git a/notebooks/tests/language.ipynb b/notebooks/tests/language.ipynb
index 8dcf650..db06892 100644
--- a/notebooks/tests/language.ipynb
+++ b/notebooks/tests/language.ipynb
@@ -112,11 +112,14 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: Computation not completed: Type mismatch: Expected POW(_A), but was INTEGER in '2',Type mismatch: Expected POW(_A), but was INTEGER in '3'",
+ "ename": "WithSourceCodeException",
+ "evalue": "de.prob.exception.ProBError: ERROR\nProB returned error messages:\nError: Type mismatch: Expected POW(_A), but was INTEGER in '2'\nError: Type mismatch: Expected POW(_A), but was INTEGER in '3'",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: Computation not completed: Type mismatch: Expected POW(_A), but was INTEGER in '2',Type mismatch: Expected POW(_A), but was INTEGER in '3'\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mERROR\u001b[0m",
+ "\u001b[1m\u001b[30m2 errors:\u001b[0m",
+ "\u001b[1m\u001b[31mError: Type mismatch: Expected POW(_A), but was INTEGER in '2'\u001b[0m",
+ "\u001b[1m\u001b[31mError: Type mismatch: Expected POW(_A), but was INTEGER in '3'\u001b[0m"
]
}
],
diff --git a/src/main/java/de/prob2/jupyter/FormulaLanguage.java b/src/main/java/de/prob2/jupyter/FormulaLanguage.java
deleted file mode 100644
index 6f85e01..0000000
--- a/src/main/java/de/prob2/jupyter/FormulaLanguage.java
+++ /dev/null
@@ -1,8 +0,0 @@
-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 768148d..e364beb 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -43,9 +43,9 @@ 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.model.eventb.EventBModel;
import de.prob.scripting.ClassicalBFactory;
import de.prob.statespace.AnimationSelector;
+import de.prob.statespace.Language;
import de.prob.statespace.StateSpace;
import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
@@ -251,7 +251,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 Language currentFormulaLanguage;
private @Nullable String currentCellSourceCode;
@Inject
@@ -275,7 +275,7 @@ public final class ProBKernel extends BaseKernel {
// 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.currentFormulaLanguage = null;
this.currentCellSourceCode = null;
this.switchMachine(Paths.get(""), null, this::loadDefaultMachine);
}
@@ -308,11 +308,11 @@ public final class ProBKernel extends BaseKernel {
this.currentMachineDirectory = currentMachineDirectory;
}
- public @NotNull FormulaLanguage getCurrentFormulaLanguage() {
+ public @Nullable Language getCurrentFormulaLanguage() {
return this.currentFormulaLanguage;
}
- public void setCurrentFormulaLanguage(final @NotNull FormulaLanguage currentFormulaLanguage) {
+ public void setCurrentFormulaLanguage(final @Nullable Language currentFormulaLanguage) {
this.currentFormulaLanguage = currentFormulaLanguage;
}
@@ -334,7 +334,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.setCurrentFormulaLanguage(null);
this.currentCellSourceCode = cellSourceCode;
final StateSpace newStateSpace = this.animator.createStateSpace();
try {
@@ -356,7 +356,7 @@ public final class ProBKernel extends BaseKernel {
* @return whether formulas are currently parsed as Event-B
*/
public boolean isEventBMode() {
- return this.getCurrentFormulaLanguage() == FormulaLanguage.EVENT_B || this.animationSelector.getCurrentTrace().getModel() instanceof EventBModel;
+ return this.getCurrentFormulaLanguage() == Language.EVENT_B || this.animationSelector.getCurrentTrace().getModel().getLanguage() == Language.EVENT_B;
}
/**
@@ -370,18 +370,19 @@ public final class ProBKernel extends BaseKernel {
* @return the parsed formula
*/
public IEvalElement parseFormulaWithoutLetVariables(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());
+ if (this.getCurrentFormulaLanguage() == null) {
+ return this.animationSelector.getCurrentTrace().getModel().parseFormula(code, expand);
+ } else {
+ switch (this.getCurrentFormulaLanguage()) {
+ 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());
+ }
}
}
diff --git a/src/main/java/de/prob2/jupyter/commands/LanguageCommand.java b/src/main/java/de/prob2/jupyter/commands/LanguageCommand.java
index 43dbcf5..110c3fa 100644
--- a/src/main/java/de/prob2/jupyter/commands/LanguageCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LanguageCommand.java
@@ -10,13 +10,11 @@ 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.Language;
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;
@@ -29,16 +27,17 @@ 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 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;
+ private static final @NotNull Map<@NotNull String, @NotNull Language> 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);
+ final Map<String, Language> languageByIdentifierMap = new HashMap<>();
+ languageByIdentifierMap.put("default", null);
+ languageByIdentifierMap.put("classical_b", Language.CLASSICAL_B);
+ languageByIdentifierMap.put("event_b", Language.EVENT_B);
LANGUAGE_BY_IDENTIFIER_MAP = Collections.unmodifiableMap(languageByIdentifierMap);
}
@@ -78,38 +77,35 @@ public final class LanguageCommand implements Command {
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) {
+ private static @NotNull String getLanguageName(final @NotNull Language language) {
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);
+ case CLASSICAL_B: return "classical B";
+ case B_RULES: return "B rules";
+ case EVENT_B: return "Event-B";
+ case TLA: return "TLA+";
+ case ALLOY: return "Alloy";
+ case Z: return "Z";
+ case CSP: return "CSP-M";
+ case XTL: return "XTL Prolog";
+ default: return language.toString();
+ }
+ }
+
+ private static @NotNull String describeLanguage(final @Nullable Language language, final @NotNull AbstractModel model) {
+ if (language == null) {
+ Language lang = model.getLanguage();
+ if (lang.getTranslatedTo() != null) {
+ // For languages that ProB internally translates to B,
+ // such as TLA and Alloy,
+ // 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,
+ // so we really only care about the translation target language.
+ lang = lang.getTranslatedTo();
+ }
+ return getLanguageName(lang) + " (default for model)";
+ } else {
+ return getLanguageName(language) + " (forced)";
}
}
@@ -122,11 +118,11 @@ public final class LanguageCommand implements Command {
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());
+ final Language 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();
+ final Language language = kernel.getCurrentFormulaLanguage();
return new DisplayData("Current language for user input is " + describeLanguage(language, trace.getModel()));
}
}
--
GitLab