diff --git a/notebooks/tests/language.ipynb b/notebooks/tests/language.ipynb
index 8dcf650bb2e242a592c82fb46a95d4e8de28dc74..db068921ecd05a7afc9be0fc08bf67bc8dd7eca5 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 6f85e01ab8f8a310da0de1ca21e4f81221add975..0000000000000000000000000000000000000000
--- 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 768148d0cefad5f361f299950cc32a505229e2b3..e364beb35800c2a8807948e12e3602460bcb3208 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 43dbcf51983fcb1fa28df6e331266abde5551b56..110c3fa6f701fe455e6ac789cd519da88c2d4fa1 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()));
}
}