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

@@ -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.

notebooks/tests/language.ipynb

+{
+ "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
+}

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);

src/main/java/de/prob2/jupyter/FormulaLanguage.java

+package de.prob2.jupyter;
+
+public enum FormulaLanguage {
+	DEFAULT,
+	CLASSICAL_B,
+	EVENT_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);

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);

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;

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

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);

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,

src/main/java/de/prob2/jupyter/commands/LanguageCommand.java

+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());
+			}
+		));
+	}
+}

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);
 	}

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);

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);

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);

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());