From 5a378b0f5e47435352e941b868b007e96a7d2033 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 6 Apr 2020 16:17:58 +0200
Subject: [PATCH] Add initial implementation of new command argument parsing
The command arguments are now parsed before Command.run is called,
based on a description of the parameter structure that must be provided
by each command.
For now, only "single" and "remainder" parameters are supported (both
required and optional). There is no native support for repeated
parameters yet.
The parsed argument values can be read by the command implementations
in a type-safe way. For example, a required parameter is returned as a
String and an optional parameter as an Optional<String>, and there are
no generic Object return values that need to be manually casted first.
---
src/main/java/de/prob2/jupyter/Command.java | 4 +-
.../java/de/prob2/jupyter/CommandUtils.java | 36 +++++++
src/main/java/de/prob2/jupyter/Parameter.java | 52 ++++++++++
.../java/de/prob2/jupyter/Parameters.java | 37 +++++++
.../de/prob2/jupyter/ParsedArguments.java | 42 ++++++++
.../de/prob2/jupyter/PositionalParameter.java | 98 +++++++++++++++++++
.../java/de/prob2/jupyter/ProBKernel.java | 2 +-
.../prob2/jupyter/commands/AssertCommand.java | 16 ++-
.../prob2/jupyter/commands/BrowseCommand.java | 15 +--
.../prob2/jupyter/commands/BsymbCommand.java | 9 +-
.../prob2/jupyter/commands/CheckCommand.java | 19 +++-
.../jupyter/commands/ConstantsCommand.java | 16 ++-
.../de/prob2/jupyter/commands/DotCommand.java | 32 +++---
.../prob2/jupyter/commands/EvalCommand.java | 16 ++-
.../prob2/jupyter/commands/ExecCommand.java | 23 +++--
.../prob2/jupyter/commands/FindCommand.java | 16 ++-
.../prob2/jupyter/commands/GotoCommand.java | 16 ++-
.../prob2/jupyter/commands/GroovyCommand.java | 15 ++-
.../prob2/jupyter/commands/HelpCommand.java | 22 +++--
.../jupyter/commands/InitialiseCommand.java | 16 ++-
.../de/prob2/jupyter/commands/LetCommand.java | 24 +++--
.../jupyter/commands/LoadCellCommand.java | 19 +++-
.../jupyter/commands/LoadFileCommand.java | 29 ++++--
.../jupyter/commands/ModelCheckCommand.java | 13 ++-
.../prob2/jupyter/commands/PrefCommand.java | 65 +++++++-----
.../jupyter/commands/PrettyPrintCommand.java | 19 +++-
.../prob2/jupyter/commands/RenderCommand.java | 16 ++-
.../prob2/jupyter/commands/ShowCommand.java | 13 ++-
.../prob2/jupyter/commands/SolveCommand.java | 24 +++--
.../prob2/jupyter/commands/StatsCommand.java | 14 +--
.../prob2/jupyter/commands/TableCommand.java | 14 ++-
.../prob2/jupyter/commands/TimeCommand.java | 15 ++-
.../prob2/jupyter/commands/TraceCommand.java | 15 +--
.../prob2/jupyter/commands/TypeCommand.java | 16 ++-
.../prob2/jupyter/commands/UnletCommand.java | 20 +++-
.../jupyter/commands/VersionCommand.java | 9 +-
36 files changed, 676 insertions(+), 151 deletions(-)
create mode 100644 src/main/java/de/prob2/jupyter/Parameter.java
create mode 100644 src/main/java/de/prob2/jupyter/Parameters.java
create mode 100644 src/main/java/de/prob2/jupyter/ParsedArguments.java
create mode 100644 src/main/java/de/prob2/jupyter/PositionalParameter.java
diff --git a/src/main/java/de/prob2/jupyter/Command.java b/src/main/java/de/prob2/jupyter/Command.java
index ebeca7c..ee1361a 100644
--- a/src/main/java/de/prob2/jupyter/Command.java
+++ b/src/main/java/de/prob2/jupyter/Command.java
@@ -9,6 +9,8 @@ import org.jetbrains.annotations.Nullable;
public interface Command {
public abstract @NotNull String getName();
+ public abstract @NotNull Parameters getParameters();
+
public abstract @NotNull String getSyntax();
public abstract @NotNull String getShortHelp();
@@ -39,7 +41,7 @@ public interface Command {
return result;
}
- public abstract @Nullable DisplayData run(final @NotNull String argString);
+ public abstract @Nullable DisplayData run(final @NotNull ParsedArguments args);
public abstract @Nullable DisplayData inspect(final @NotNull String argString, final int at);
diff --git a/src/main/java/de/prob2/jupyter/CommandUtils.java b/src/main/java/de/prob2/jupyter/CommandUtils.java
index e2b855a..3c83d96 100644
--- a/src/main/java/de/prob2/jupyter/CommandUtils.java
+++ b/src/main/java/de/prob2/jupyter/CommandUtils.java
@@ -2,6 +2,7 @@ package de.prob2.jupyter;
import java.util.ArrayList;
import java.util.Arrays;
+import java.util.Collections;
import java.util.HashMap;
import java.util.LinkedHashSet;
import java.util.List;
@@ -101,6 +102,41 @@ public final class CommandUtils {
return splitArgs(args, 0);
}
+ private static <T> @NotNull String parseSingleArg(final @NotNull ParsedArguments parsed, final @NotNull String remainingArgs, final @NotNull PositionalParameter<T> param) {
+ final Parameter.ParseResult<T> parsedSingleArg = param.parse(remainingArgs);
+ parsed.put(param, parsedSingleArg.getParsedArg());
+ return parsedSingleArg.getRemainingArgString();
+ }
+
+ private static <T> void checkParsedParameter(final @NotNull ParsedArguments parsed, final @NotNull PositionalParameter<T> param) {
+ if (!parsed.containsKey(param)) {
+ if (param.isOptional()) {
+ parsed.put(param, param.getDefaultValue());
+ } else {
+ throw new UserErrorException("Missing required parameter " + param.getIdentifier());
+ }
+ }
+ }
+
+ public static @NotNull ParsedArguments parseArgs(final @NotNull Parameters parameters, final @NotNull String argString) {
+ final ParsedArguments parsed = new ParsedArguments(Collections.emptyMap());
+ String remainingArgs = argString;
+ for (final PositionalParameter<?> param : parameters.getPositionalParameters()) {
+ if (remainingArgs.isEmpty()) {
+ break;
+ }
+
+ remainingArgs = parseSingleArg(parsed, remainingArgs, param);
+ }
+ if (!remainingArgs.isEmpty()) {
+ throw new UserErrorException("Expected at most " + parameters.getPositionalParameters().size() + " arguments, got extra argument: " + remainingArgs);
+ }
+ for (final PositionalParameter<?> param : parameters.getPositionalParameters()) {
+ checkParsedParameter(parsed, param);
+ }
+ return parsed;
+ }
+
public static @NotNull Map<@NotNull String, @NotNull String> parsePreferences(final @NotNull List<@NotNull String> args) {
final Map<String, String> preferences = new HashMap<>();
for (final String arg : args) {
diff --git a/src/main/java/de/prob2/jupyter/Parameter.java b/src/main/java/de/prob2/jupyter/Parameter.java
new file mode 100644
index 0000000..bb1fcb9
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/Parameter.java
@@ -0,0 +1,52 @@
+package de.prob2.jupyter;
+
+import com.google.common.base.MoreObjects;
+
+import org.jetbrains.annotations.NotNull;
+
+public abstract class Parameter<T> {
+ public static final class ParseResult<T> {
+ private final T parsedArg;
+ private final @NotNull String remainingArgString;
+
+ public ParseResult(final T parsedArg, final @NotNull String remainingArgString) {
+ super();
+
+ this.parsedArg = parsedArg;
+ this.remainingArgString = remainingArgString;
+ }
+
+ public T getParsedArg() {
+ return this.parsedArg;
+ }
+
+ public @NotNull String getRemainingArgString() {
+ return this.remainingArgString;
+ }
+ }
+
+ private final @NotNull String identifier;
+
+ protected Parameter(final @NotNull String identifier) {
+ super();
+
+ this.identifier = identifier;
+ }
+
+ public @NotNull String getIdentifier() {
+ return this.identifier;
+ }
+
+ public abstract boolean isOptional();
+
+ public abstract T getDefaultValue();
+
+ public abstract Parameter.ParseResult<T> parse(final @NotNull String argString);
+
+ @Override
+ public String toString() {
+ return MoreObjects.toStringHelper(this)
+ .add("identifier", this.getIdentifier())
+ .toString();
+ }
+}
diff --git a/src/main/java/de/prob2/jupyter/Parameters.java b/src/main/java/de/prob2/jupyter/Parameters.java
new file mode 100644
index 0000000..0ef5427
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/Parameters.java
@@ -0,0 +1,37 @@
+package de.prob2.jupyter;
+
+import java.util.Collections;
+import java.util.List;
+
+import org.jetbrains.annotations.NotNull;
+
+public final class Parameters {
+ public static final @NotNull Parameters NONE = new Parameters(Collections.emptyList());
+
+ private final @NotNull List<PositionalParameter<?>> positionalParameters;
+
+ public Parameters(final @NotNull List<PositionalParameter<?>> positionalParameters) {
+ super();
+
+ this.positionalParameters = positionalParameters;
+
+ boolean seenOptional = false;
+ boolean seenOnlyLast = false;
+ for (final PositionalParameter<?> param : positionalParameters) {
+ final boolean isOptional = param instanceof PositionalParameter.OptionalSingle || param instanceof PositionalParameter.OptionalRemainder;
+ final boolean isOnlyLast = param instanceof PositionalParameter.RequiredRemainder || param instanceof PositionalParameter.OptionalRemainder;
+ if (seenOnlyLast) {
+ throw new IllegalArgumentException("A remainder positional parameter cannot be followed by any more positional parameters");
+ }
+ if (seenOptional && isOptional) {
+ throw new IllegalArgumentException("Required positional parameter " + param + " cannot follow an optional positional parameter");
+ }
+ seenOptional |= isOptional;
+ seenOnlyLast |= isOnlyLast;
+ }
+ }
+
+ public @NotNull List<PositionalParameter<?>> getPositionalParameters() {
+ return this.positionalParameters;
+ }
+}
diff --git a/src/main/java/de/prob2/jupyter/ParsedArguments.java b/src/main/java/de/prob2/jupyter/ParsedArguments.java
new file mode 100644
index 0000000..3d8a81e
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/ParsedArguments.java
@@ -0,0 +1,42 @@
+package de.prob2.jupyter;
+
+import java.util.HashMap;
+import java.util.Map;
+
+import com.google.common.base.MoreObjects;
+
+import org.jetbrains.annotations.NotNull;
+
+public final class ParsedArguments {
+ private final @NotNull Map<@NotNull Parameter<?>, Object> values;
+
+ public ParsedArguments(final @NotNull Map<@NotNull Parameter<?>, Object> values) {
+ super();
+
+ this.values = new HashMap<>(values);
+ }
+
+ public boolean containsKey(final @NotNull Parameter<?> parameter) {
+ return this.values.containsKey(parameter);
+ }
+
+ public <T> T get(final @NotNull Parameter<T> parameter) {
+ if (!this.containsKey(parameter)) {
+ throw new IllegalArgumentException("No value present for parameter " + parameter);
+ }
+ @SuppressWarnings("unchecked")
+ final T value = (T)this.values.get(parameter);
+ return value;
+ }
+
+ public <T> void put(final @NotNull Parameter<T> parameter, final T value) {
+ this.values.put(parameter, value);
+ }
+
+ @Override
+ public String toString() {
+ return MoreObjects.toStringHelper(this)
+ .add("values", this.values)
+ .toString();
+ }
+}
diff --git a/src/main/java/de/prob2/jupyter/PositionalParameter.java b/src/main/java/de/prob2/jupyter/PositionalParameter.java
new file mode 100644
index 0000000..f127f49
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/PositionalParameter.java
@@ -0,0 +1,98 @@
+package de.prob2.jupyter;
+
+import java.util.Optional;
+
+import org.jetbrains.annotations.NotNull;
+
+public abstract class PositionalParameter<T> extends Parameter<T> {
+ public static final class RequiredSingle extends PositionalParameter<@NotNull String> {
+ public RequiredSingle(final @NotNull String identifier) {
+ super(identifier);
+ }
+
+ @Override
+ public boolean isOptional() {
+ return false;
+ }
+
+ @Override
+ public @NotNull String getDefaultValue() {
+ throw new UnsupportedOperationException("Not an optional parameter");
+ }
+
+ @Override
+ public @NotNull Parameter.ParseResult<@NotNull String> parse(final @NotNull String argString) {
+ final String[] split = CommandUtils.ARG_SPLIT_PATTERN.split(argString, 2);
+ return new Parameter.ParseResult<>(split[0], split.length > 1 ? split[1] : "");
+ }
+ }
+
+ public static final class OptionalSingle extends PositionalParameter<@NotNull Optional<String>> {
+ public OptionalSingle(final @NotNull String identifier) {
+ super(identifier);
+ }
+
+ @Override
+ public boolean isOptional() {
+ return true;
+ }
+
+ @Override
+ public @NotNull Optional<String> getDefaultValue() {
+ return Optional.empty();
+ }
+
+ @Override
+ public @NotNull Parameter.ParseResult<@NotNull Optional<String>> parse(final @NotNull String argString) {
+ final String[] split = CommandUtils.ARG_SPLIT_PATTERN.split(argString, 2);
+ return new Parameter.ParseResult<>(Optional.of(split[0]), split.length > 1 ? split[1] : "");
+ }
+ }
+
+ public static final class RequiredRemainder extends PositionalParameter<@NotNull String> {
+ public RequiredRemainder(final @NotNull String identifier) {
+ super(identifier);
+ }
+
+ @Override
+ public boolean isOptional() {
+ return false;
+ }
+
+ @Override
+ public @NotNull String getDefaultValue() {
+ throw new UnsupportedOperationException("Not an optional parameter");
+ }
+
+ @Override
+ public Parameter.ParseResult<@NotNull String> parse(final @NotNull String argString) {
+ return new Parameter.ParseResult<>(argString, "");
+ }
+ }
+
+ public static final class OptionalRemainder extends PositionalParameter<@NotNull Optional<String>> {
+ public OptionalRemainder(final @NotNull String identifier) {
+ super(identifier);
+ }
+
+ @Override
+ public boolean isOptional() {
+ return true;
+ }
+
+ @Override
+ public @NotNull Optional<String> getDefaultValue() {
+ return Optional.empty();
+ }
+
+ @Override
+ public Parameter.ParseResult<@NotNull Optional<String>> parse(final @NotNull String argString) {
+ return new Parameter.ParseResult<>(Optional.of(argString), "");
+ }
+ }
+
+ protected PositionalParameter(final @NotNull String identifier) {
+ super(identifier);
+ }
+
+}
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index d32646d..f126d02 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -297,7 +297,7 @@ public final class ProBKernel extends BaseKernel {
}
final DisplayData result;
try {
- result = command.run(argString);
+ result = command.run(CommandUtils.parseArgs(command.getParameters(), argString));
} catch (final UserErrorException e) {
throw new CommandExecutionException(name, e);
}
diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index 0d79d7a..55574b0 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
@@ -1,5 +1,7 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
+
import com.google.inject.Inject;
import com.google.inject.Provider;
@@ -9,6 +11,9 @@ import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -20,6 +25,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class AssertCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder FORMULA_PARAM = new PositionalParameter.RequiredRemainder("formula");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -36,6 +43,11 @@ public final class AssertCommand implements Command {
return ":assert";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(FORMULA_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":assert PREDICATE";
@@ -54,8 +66,8 @@ public final class AssertCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final String code = this.kernelProvider.get().insertLetVariables(argString);
+ 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));
if (result instanceof EvalResult && "TRUE".equals(((EvalResult)result).getValue())) {
// Use EvalResult.TRUE instead of the real result so that solution variables are not displayed.
diff --git a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
index 6ec6593..28ca4af 100644
--- a/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/BrowseCommand.java
@@ -11,9 +11,9 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.LoadedMachine;
import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
-
import de.prob2.jupyter.Command;
-import de.prob2.jupyter.UserErrorException;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -38,6 +38,11 @@ public final class BrowseCommand implements Command {
return ":browse";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return Parameters.NONE;
+ }
+
@Override
public @NotNull String getSyntax() {
return ":browse";
@@ -58,11 +63,7 @@ public final class BrowseCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- if (!argString.isEmpty()) {
- throw new UserErrorException("Unexpected argument: " + argString);
- }
-
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
final StringBuilder sb = new StringBuilder("Machine: ");
sb.append(trace.getStateSpace().getMainComponent());
diff --git a/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java b/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java
index 07bcee8..e799a47 100644
--- a/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/BsymbCommand.java
@@ -3,6 +3,8 @@ package de.prob2.jupyter.commands;
import com.google.inject.Inject;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -21,6 +23,11 @@ public final class BsymbCommand implements Command {
return ":bsymb";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return Parameters.NONE;
+ }
+
@Override
public @NotNull String getSyntax() {
return ":bsymb";
@@ -37,7 +44,7 @@ public final class BsymbCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final DisplayData data = new DisplayData("Your current environment uses plain text output; the bsymb.sty LaTeX commands will not be loaded.");
// The actual bsymb definitions are added by the ProBKernel class when it processes the command result, and the error message below will be replaced.
// If this error message is visible to the user, it means that the definitions were not added correctly.
diff --git a/src/main/java/de/prob2/jupyter/commands/CheckCommand.java b/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
index 7f06044..088dcce 100644
--- a/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
@@ -22,6 +22,9 @@ import de.prob.statespace.Trace;
import de.prob.unicode.UnicodeTranslator;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -31,6 +34,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class CheckCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredSingle WHAT_PARAM = new PositionalParameter.RequiredSingle("what");
+
private static final @NotNull Map<@NotNull String, @NotNull Class<? extends AbstractTheoremElement>> CHILDREN_BASE_CLASS_MAP;
static {
final Map<String, Class<? extends AbstractTheoremElement>> childrenBaseClassMap = new HashMap<>();
@@ -54,6 +59,11 @@ public final class CheckCommand implements Command {
return ":check";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(WHAT_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":check WHAT";
@@ -70,11 +80,12 @@ public final class CheckCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- if (!CHILDREN_BASE_CLASS_MAP.containsKey(argString)) {
- throw new UserErrorException("Don't know how to check " + argString);
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final String what = args.get(WHAT_PARAM);
+ if (!CHILDREN_BASE_CLASS_MAP.containsKey(what)) {
+ throw new UserErrorException("Don't know how to check " + what);
}
- final Class<? extends AbstractTheoremElement> childrenBaseClass = CHILDREN_BASE_CLASS_MAP.get(argString);
+ final Class<? extends AbstractTheoremElement> childrenBaseClass = CHILDREN_BASE_CLASS_MAP.get(what);
final Trace trace = this.animationSelector.getCurrentTrace();
// Find all children of a subclass of childrenBaseClass.
// This needs to be done manually, because getChildrenOfType only returns children whose class *exactly* matches the given class.
diff --git a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
index 264a3fe..1dc90cc 100644
--- a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
@@ -12,6 +12,9 @@ import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -21,6 +24,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class ConstantsCommand implements Command {
+ private static final @NotNull PositionalParameter.OptionalRemainder PREDICATE_PARAM = new PositionalParameter.OptionalRemainder("predicate");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -37,6 +42,11 @@ public final class ConstantsCommand implements Command {
return ":constants";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(PREDICATE_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":constants [PREDICATE]";
@@ -53,13 +63,13 @@ public final class ConstantsCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
final String predicate;
- if (argString.isEmpty()) {
+ if (!args.get(PREDICATE_PARAM).isPresent()) {
predicate = "1=1";
} else {
- predicate = this.kernelProvider.get().insertLetVariables(argString);
+ predicate = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM).get());
}
final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), "$setup_constants", predicate, 1);
assert !ops.isEmpty();
diff --git a/src/main/java/de/prob2/jupyter/commands/DotCommand.java b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
index 1e10001..75e48d9 100644
--- a/src/main/java/de/prob2/jupyter/commands/DotCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/DotCommand.java
@@ -4,6 +4,7 @@ import java.io.IOException;
import java.io.UncheckedIOException;
import java.nio.file.Files;
import java.nio.file.Path;
+import java.util.Arrays;
import java.util.Collections;
import java.util.List;
import java.util.stream.Collectors;
@@ -21,6 +22,9 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -31,6 +35,9 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class DotCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredSingle COMMAND_PARAM = new PositionalParameter.RequiredSingle("command");
+ private static final @NotNull PositionalParameter.OptionalRemainder FORMULA_PARAM = new PositionalParameter.OptionalRemainder("formula");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -47,6 +54,11 @@ public final class DotCommand implements Command {
return ":dot";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Arrays.asList(COMMAND_PARAM, FORMULA_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":dot COMMAND [FORMULA]";
@@ -76,19 +88,17 @@ public final class DotCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final List<String> split = CommandUtils.splitArgs(argString, 2);
- assert !split.isEmpty();
- final String command = split.get(0);
- final List<IEvalElement> args;
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final String command = args.get(COMMAND_PARAM);
+ final List<IEvalElement> dotCommandArgs;
final String code;
- if (split.size() > 1) {
- code = this.kernelProvider.get().insertLetVariables(split.get(1));
+ 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));
- args = Collections.singletonList(formula);
+ dotCommandArgs = Collections.singletonList(formula);
} else {
code = null;
- args = Collections.emptyList();
+ dotCommandArgs = Collections.emptyList();
}
final Trace trace = this.animationSelector.getCurrentTrace();
@@ -105,7 +115,7 @@ public final class DotCommand implements Command {
} catch (final IOException e) {
throw new UncheckedIOException("Failed to create temp file", e);
}
- final GetSvgForVisualizationCommand cmd2 = new GetSvgForVisualizationCommand(trace.getCurrentState(), item, outPath.toFile(), args);
+ final GetSvgForVisualizationCommand cmd2 = new GetSvgForVisualizationCommand(trace.getCurrentState(), item, outPath.toFile(), dotCommandArgs);
// Provide source code (if any) to error highlighter
final Runnable execute = () -> trace.getStateSpace().execute(cmd2);
if (code != null) {
@@ -119,7 +129,7 @@ public final class DotCommand implements Command {
} catch (final IOException e) {
throw new UncheckedIOException("Failed to read dot output", e);
}
- final DisplayData result = new DisplayData(String.format("<Dot visualization: %s %s>", command, args));
+ final DisplayData result = new DisplayData(String.format("<Dot visualization: %s %s>", command, dotCommandArgs));
result.putSVG(svg);
return result;
}
diff --git a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
index 74c47cf..30de5cd 100644
--- a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
@@ -1,5 +1,7 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
+
import com.google.inject.Inject;
import com.google.inject.Injector;
@@ -7,6 +9,9 @@ import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -16,6 +21,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class EvalCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder FORMULA_PARAM = new PositionalParameter.RequiredRemainder("formula");
+
private final @NotNull Injector injector;
private final @NotNull AnimationSelector animationSelector;
@@ -32,6 +39,11 @@ public final class EvalCommand implements Command {
return ":eval";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(FORMULA_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return "FORMULA\n// or\n:eval FORMULA";
@@ -49,8 +61,8 @@ public final class EvalCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final String code = this.injector.getInstance(ProBKernel.class).insertLetVariables(argString);
+ 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)));
}
diff --git a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
index 3135e01..931a5ca 100644
--- a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
@@ -1,5 +1,6 @@
package de.prob2.jupyter.commands;
+import java.util.Arrays;
import java.util.Collections;
import java.util.List;
import java.util.stream.Collectors;
@@ -13,6 +14,9 @@ import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -22,6 +26,9 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class ExecCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredSingle OPERATION_PARAM = new PositionalParameter.RequiredSingle("operation");
+ private static final @NotNull PositionalParameter.OptionalRemainder PREDICATE_PARAM = new PositionalParameter.OptionalRemainder("predicate");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -38,6 +45,11 @@ public final class ExecCommand implements Command {
return ":exec";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Arrays.asList(OPERATION_PARAM, PREDICATE_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":exec OPERATION [PREDICATE]";
@@ -55,17 +67,14 @@ public final class ExecCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final List<String> split = CommandUtils.splitArgs(argString, 2);
- assert !split.isEmpty();
-
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
- final String translatedOpName = CommandUtils.unprettyOperationName(split.get(0));
+ final String translatedOpName = CommandUtils.unprettyOperationName(args.get(OPERATION_PARAM));
final String predicate;
- if (split.size() < 2) {
+ if (!args.get(PREDICATE_PARAM).isPresent()) {
predicate = "1=1";
} else {
- predicate = this.kernelProvider.get().insertLetVariables(split.get(1));
+ predicate = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM).get());
}
final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), translatedOpName, predicate, 1);
assert !ops.isEmpty();
diff --git a/src/main/java/de/prob2/jupyter/commands/FindCommand.java b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
index 0664e95..e1aae32 100644
--- a/src/main/java/de/prob2/jupyter/commands/FindCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
@@ -1,5 +1,7 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
+
import com.google.inject.Inject;
import com.google.inject.Provider;
@@ -9,6 +11,9 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -18,6 +23,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class FindCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder PREDICATE_PARAM = new PositionalParameter.RequiredRemainder("predicate");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -34,6 +41,11 @@ public final class FindCommand implements Command {
return ":find";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(PREDICATE_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":find PREDICATE";
@@ -51,9 +63,9 @@ public final class FindCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
- final String code = this.kernelProvider.get().insertLetVariables(argString);
+ final String code = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM));
final Trace newTrace = CommandUtils.withSourceCode(code, () -> {
final IEvalElement pred = trace.getModel().parseFormula(code, FormulaExpand.EXPAND);
return trace.getStateSpace().getTraceToState(pred);
diff --git a/src/main/java/de/prob2/jupyter/commands/GotoCommand.java b/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
index 14c07f3..78770f2 100644
--- a/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/GotoCommand.java
@@ -1,11 +1,16 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
+
import com.google.inject.Inject;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -15,6 +20,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class GotoCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredSingle INDEX_PARAM = new PositionalParameter.RequiredSingle("index");
+
private final @NotNull AnimationSelector animationSelector;
@Inject
@@ -29,6 +36,11 @@ public final class GotoCommand implements Command {
return ":goto";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(INDEX_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":goto INDEX";
@@ -46,8 +58,8 @@ public final class GotoCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final int index = Integer.parseInt(argString);
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final int index = Integer.parseInt(args.get(INDEX_PARAM));
final Trace trace = this.animationSelector.getCurrentTrace();
if (index < -1 || index >= trace.size()) {
throw new UserErrorException(String.format("Invalid trace index %d, must be in -1..%d", index, trace.size()-1));
diff --git a/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java b/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java
index ad1e99d..43bfe4f 100644
--- a/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/GroovyCommand.java
@@ -1,5 +1,6 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
import java.util.Objects;
import javax.script.ScriptEngine;
@@ -11,6 +12,9 @@ import com.google.inject.Injector;
import de.prob.scripting.ScriptEngineProvider;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -20,6 +24,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class GroovyCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder EXPRESSION_PARAM = new PositionalParameter.RequiredRemainder("expression");
+
private final @NotNull Injector injector;
private final @NotNull ScriptEngine groovyScriptEngine;
@@ -36,6 +42,11 @@ public final class GroovyCommand implements Command {
return ":groovy";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(EXPRESSION_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":groovy EXPRESSION";
@@ -52,11 +63,11 @@ public final class GroovyCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
this.groovyScriptEngine.put("__console", this.injector.getInstance(ProBKernel.class).getIO().out);
final Object result;
try {
- result = this.groovyScriptEngine.eval(argString);
+ result = this.groovyScriptEngine.eval(args.get(EXPRESSION_PARAM));
} catch (ScriptException e) {
throw new RuntimeException(e);
} finally {
diff --git a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
index 5203da1..487e63a 100644
--- a/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/HelpCommand.java
@@ -13,7 +13,9 @@ import com.google.inject.Inject;
import com.google.inject.Injector;
import de.prob2.jupyter.Command;
-import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -24,6 +26,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class HelpCommand implements Command {
+ private static final @NotNull PositionalParameter.OptionalSingle COMMAND_NAME_PARAM = new PositionalParameter.OptionalSingle("commandName");
+
private static final @NotNull Map<@NotNull String, @NotNull List<@NotNull Class<? extends Command>>> COMMAND_CLASS_CATEGORIES;
static {
final Map<String, List<Class<? extends Command>>> commandCategories = new LinkedHashMap<>();
@@ -73,6 +77,11 @@ public final class HelpCommand implements Command {
return ":help";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(COMMAND_NAME_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":help [COMMAND]";
@@ -89,10 +98,9 @@ public final class HelpCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final ProBKernel kernel = this.injector.getInstance(ProBKernel.class);
- final List<String> args = CommandUtils.splitArgs(argString);
- if (args.isEmpty()) {
+ if (!args.get(COMMAND_NAME_PARAM).isPresent()) {
final StringBuilder sb = new StringBuilder("Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use :load to load an external machine file.\nYou can also use any of the following commands. For more help on a particular command, run :help commandname.\n");
final StringBuilder sbMarkdown = new StringBuilder("Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use `:load` to load an external machine file.\n\nYou can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n");
@@ -141,8 +149,8 @@ public final class HelpCommand implements Command {
final DisplayData result = new DisplayData(sb.toString());
result.putMarkdown(sbMarkdown.toString());
return result;
- } else if (args.size() == 1) {
- String commandName = args.get(0);
+ } else {
+ String commandName = args.get(COMMAND_NAME_PARAM).get();
// If the user entered a command name without colons, add one or two colons as appropriate.
// (If the command cannot be found, no colons are added, because we'll error out later anyway.)
if (!commandName.startsWith(":")) {
@@ -158,8 +166,6 @@ public final class HelpCommand implements Command {
throw new UserErrorException(String.format("Cannot display help for unknown command \"%s\"", commandName));
}
return command.renderHelp();
- } else {
- throw new UserErrorException("Expected at most 1 argument, got " + args.size());
}
}
diff --git a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
index 1599a1d..b7bf155 100644
--- a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
@@ -12,6 +12,9 @@ import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -21,6 +24,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class InitialiseCommand implements Command {
+ private static final @NotNull PositionalParameter.OptionalRemainder PREDICATE_PARAM = new PositionalParameter.OptionalRemainder("predicate");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -37,6 +42,11 @@ public final class InitialiseCommand implements Command {
return ":init";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(PREDICATE_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":init [PREDICATE]";
@@ -53,13 +63,13 @@ public final class InitialiseCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
final String predicate;
- if (argString.isEmpty()) {
+ if (!args.get(PREDICATE_PARAM).isPresent()) {
predicate = "1=1";
} else {
- predicate = this.kernelProvider.get().insertLetVariables(argString);
+ predicate = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM).get());
}
final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), "$initialise_machine", predicate, 1);
assert !ops.isEmpty();
diff --git a/src/main/java/de/prob2/jupyter/commands/LetCommand.java b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
index 9233277..4d7d682 100644
--- a/src/main/java/de/prob2/jupyter/commands/LetCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
@@ -1,6 +1,6 @@
package de.prob2.jupyter.commands;
-import java.util.List;
+import java.util.Arrays;
import com.google.inject.Inject;
import com.google.inject.Provider;
@@ -11,8 +11,10 @@ import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
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;
@@ -21,6 +23,9 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class LetCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredSingle NAME_PARAM = new PositionalParameter.RequiredSingle("name");
+ private static final @NotNull PositionalParameter.RequiredRemainder EXPRESSION_PARAM = new PositionalParameter.RequiredRemainder("expression");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -37,6 +42,11 @@ public final class LetCommand implements Command {
return ":let";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Arrays.asList(NAME_PARAM, EXPRESSION_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":let NAME EXPR";
@@ -55,13 +65,9 @@ public final class LetCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final List<String> split = CommandUtils.splitArgs(argString, 2);
- if (split.size() != 2) {
- throw new UserErrorException("Expected 2 arguments, not " + split.size());
- }
- final String name = split.get(0);
- final String expr = this.kernelProvider.get().insertLetVariables(split.get(1));
+ 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));
if (evaluated instanceof EvalResult) {
this.kernelProvider.get().getVariables().put(name, evaluated.toString());
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
index e08a3c0..3f115cb 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
@@ -1,6 +1,7 @@
package de.prob2.jupyter.commands;
import java.nio.file.Paths;
+import java.util.Collections;
import java.util.List;
import java.util.Map;
@@ -12,6 +13,9 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -22,6 +26,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class LoadCellCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder PREFS_AND_CODE_PARAM = new PositionalParameter.RequiredRemainder("prefsAndCode");
+
private final @NotNull ClassicalBFactory classicalBFactory;
private final @NotNull AnimationSelector animationSelector;
private final @NotNull Provider<ProBKernel> proBKernelProvider;
@@ -44,6 +50,11 @@ public final class LoadCellCommand implements Command {
return "::load";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(PREFS_AND_CODE_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return "MACHINE\n...\nEND\n\n// or\n\n::load [PREF=VALUE ...]\nMACHINE\n...\nEND";
@@ -62,15 +73,15 @@ public final class LoadCellCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final String[] split = argString.split("\n", 2);
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final String[] split = args.get(PREFS_AND_CODE_PARAM).split("\n", 2);
if (split.length != 2) {
throw new UserErrorException("Missing command body");
}
final String prefsString = split[0];
final String body = split[1];
- final List<String> args = CommandUtils.splitArgs(prefsString);
- final Map<String, String> preferences = CommandUtils.parsePreferences(args);
+ final List<String> prefsSplit = CommandUtils.splitArgs(prefsString);
+ final Map<String, String> preferences = CommandUtils.parsePreferences(prefsSplit);
this.animationSelector.changeCurrentAnimation(new Trace(CommandUtils.withSourceCode(body, () ->
this.classicalBFactory.create("(machine from Jupyter cell)", body).load(preferences)
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
index 5d14a5d..4d2155e 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
@@ -4,6 +4,8 @@ import java.io.IOException;
import java.nio.file.Files;
import java.nio.file.Path;
import java.nio.file.Paths;
+import java.util.Arrays;
+import java.util.Collections;
import java.util.List;
import java.util.Map;
import java.util.stream.Collectors;
@@ -20,6 +22,9 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -34,6 +39,9 @@ import org.slf4j.LoggerFactory;
public final class LoadFileCommand implements Command {
private static final @NotNull Logger LOGGER = LoggerFactory.getLogger(LoadFileCommand.class);
+ private static final @NotNull PositionalParameter.RequiredSingle FILE_NAME_PARAM = new PositionalParameter.RequiredSingle("fileName");
+ private static final @NotNull PositionalParameter.OptionalRemainder PREFS_PARAM = new PositionalParameter.OptionalRemainder("prefs");
+
private final @NotNull Injector injector;
private final @NotNull AnimationSelector animationSelector;
private final @NotNull Provider<ProBKernel> proBKernelProvider;
@@ -56,6 +64,11 @@ public final class LoadFileCommand implements Command {
return ":load";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Arrays.asList(FILE_NAME_PARAM, PREFS_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":load FILENAME [PREF=VALUE ...]";
@@ -73,13 +86,8 @@ public final class LoadFileCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final List<String> args = CommandUtils.splitArgs(argString);
- if (args.isEmpty()) {
- throw new UserErrorException("Missing machine file name");
- }
-
- final Path machineFilePath = Paths.get(args.get(0));
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final Path machineFilePath = Paths.get(args.get(FILE_NAME_PARAM));
final String machineFileName = machineFilePath.getFileName().toString();
final Path machineFileDirectory = machineFilePath.getParent() == null ? Paths.get("") : machineFilePath.getParent();
final int dotIndex = machineFileName.lastIndexOf('.');
@@ -90,7 +98,12 @@ public final class LoadFileCommand implements Command {
if (!FactoryProvider.isExtensionKnown(extension)) {
throw new UserErrorException("Unsupported file type: ." + extension);
}
- final Map<String, String> preferences = CommandUtils.parsePreferences(args.subList(1, args.size()));
+ final Map<String, String> preferences;
+ if (args.get(PREFS_PARAM).isPresent()) {
+ preferences = CommandUtils.parsePreferences(CommandUtils.splitArgs(args.get(PREFS_PARAM).get()));
+ } else {
+ preferences = Collections.emptyMap();
+ }
try {
final ModelFactory<?> factory = this.injector.getInstance(FactoryProvider.factoryClassFromExtension(extension));
diff --git a/src/main/java/de/prob2/jupyter/commands/ModelCheckCommand.java b/src/main/java/de/prob2/jupyter/commands/ModelCheckCommand.java
index 7356c6e..8c45b16 100644
--- a/src/main/java/de/prob2/jupyter/commands/ModelCheckCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ModelCheckCommand.java
@@ -16,6 +16,8 @@ import de.prob.check.StateSpaceStats;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.StateSpace;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -45,6 +47,11 @@ public final class ModelCheckCommand implements Command {
return ":modelcheck";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return Parameters.NONE;
+ }
+
@Override
public @NotNull String getSyntax() {
return ":modelcheck";
@@ -80,11 +87,7 @@ public final class ModelCheckCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- if (!argString.isEmpty()) {
- throw new UserErrorException("Unexpected argument: " + argString);
- }
-
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final StateSpace stateSpace = this.animationSelector.getCurrentTrace().getStateSpace();
final JupyterIO io = this.kernelProvider.get().getIO();
diff --git a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
index 2be8537..89df593 100644
--- a/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/PrefCommand.java
@@ -1,6 +1,7 @@
package de.prob2.jupyter.commands;
import java.util.ArrayList;
+import java.util.Collections;
import java.util.List;
import java.util.TreeMap;
@@ -14,6 +15,9 @@ import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -23,6 +27,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class PrefCommand implements Command {
+ private static final @NotNull PositionalParameter.OptionalRemainder PREFS_PARAM = new PositionalParameter.OptionalRemainder("prefs");
+
private final @NotNull AnimationSelector animationSelector;
@Inject
@@ -37,6 +43,11 @@ public final class PrefCommand implements Command {
return ":pref";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(PREFS_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":pref [NAME ...]\n// or\n:pref NAME=VALUE [NAME=VALUE ...]";
@@ -54,10 +65,9 @@ public final class PrefCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final List<String> args = CommandUtils.splitArgs(argString);
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final StringBuilder sb = new StringBuilder();
- if (args.isEmpty()) {
+ if (!args.get(PREFS_PARAM).isPresent()) {
final GetCurrentPreferencesCommand cmd = new GetCurrentPreferencesCommand();
this.animationSelector.getCurrentTrace().getStateSpace().execute(cmd);
// TreeMap is used to sort the preferences by name.
@@ -67,31 +77,34 @@ public final class PrefCommand implements Command {
sb.append(v);
sb.append('\n');
});
- } else if (args.get(0).contains("=")) {
- final List<SetPreferenceCommand> cmds = new ArrayList<>();
- CommandUtils.parsePreferences(args).forEach((pref, value) -> {
- cmds.add(new SetPreferenceCommand(pref, value));
- sb.append("Preference changed: ");
- sb.append(pref);
- sb.append(" = ");
- sb.append(value);
- sb.append('\n');
- });
- this.animationSelector.getCurrentTrace().getStateSpace().execute(new ComposedCommand(cmds));
} else {
- final List<GetPreferenceCommand> cmds = new ArrayList<>();
- for (final String arg : args) {
- if (arg.contains("=")) {
- throw new UserErrorException(String.format("Cannot view and change preferences in the same command (attempted to assign preference %s)", arg));
+ final List<String> prefsSplit = CommandUtils.splitArgs(args.get(PREFS_PARAM).get());
+ if (prefsSplit.get(0).contains("=")) {
+ final List<SetPreferenceCommand> cmds = new ArrayList<>();
+ CommandUtils.parsePreferences(prefsSplit).forEach((pref, value) -> {
+ cmds.add(new SetPreferenceCommand(pref, value));
+ sb.append("Preference changed: ");
+ sb.append(pref);
+ sb.append(" = ");
+ sb.append(value);
+ sb.append('\n');
+ });
+ this.animationSelector.getCurrentTrace().getStateSpace().execute(new ComposedCommand(cmds));
+ } else {
+ final List<GetPreferenceCommand> cmds = new ArrayList<>();
+ for (final String arg : prefsSplit) {
+ if (arg.contains("=")) {
+ throw new UserErrorException(String.format("Cannot view and change preferences in the same command (attempted to assign preference %s)", arg));
+ }
+ cmds.add(new GetPreferenceCommand(arg));
+ }
+ this.animationSelector.getCurrentTrace().getStateSpace().execute(new ComposedCommand(cmds));
+ for (final GetPreferenceCommand cmd : cmds) {
+ sb.append(cmd.getKey());
+ sb.append(" = ");
+ sb.append(cmd.getValue());
+ sb.append('\n');
}
- cmds.add(new GetPreferenceCommand(arg));
- }
- this.animationSelector.getCurrentTrace().getStateSpace().execute(new ComposedCommand(cmds));
- for (final GetPreferenceCommand cmd : cmds) {
- sb.append(cmd.getKey());
- sb.append(" = ");
- sb.append(cmd.getValue());
- sb.append('\n');
}
}
return new DisplayData(sb.toString());
diff --git a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
index fc0a2a2..a6fe79a 100644
--- a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java
@@ -1,5 +1,7 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
+
import com.google.inject.Inject;
import de.prob.animator.command.PrettyPrintFormulaCommand;
@@ -8,6 +10,9 @@ import de.prob.animator.domainobjects.IEvalElement;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -16,6 +21,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class PrettyPrintCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder PREDICATE_PARAM = new PositionalParameter.RequiredRemainder("predicate");
+
private final AnimationSelector animationSelector;
@Inject
@@ -30,6 +37,11 @@ public final class PrettyPrintCommand implements Command {
return ":prettyprint";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(PREDICATE_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":prettyprint PREDICATE";
@@ -47,14 +59,15 @@ public final class PrettyPrintCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final IEvalElement formula = this.animationSelector.getCurrentTrace().getModel().parseFormula(argString, FormulaExpand.EXPAND);
+ 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 PrettyPrintFormulaCommand cmdUnicode = new PrettyPrintFormulaCommand(formula, PrettyPrintFormulaCommand.Mode.UNICODE);
cmdUnicode.setOptimize(false);
final PrettyPrintFormulaCommand cmdLatex = new PrettyPrintFormulaCommand(formula, PrettyPrintFormulaCommand.Mode.LATEX);
cmdLatex.setOptimize(false);
- CommandUtils.withSourceCode(argString, () -> this.animationSelector.getCurrentTrace().getStateSpace().execute(cmdUnicode, cmdLatex));
+ CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().getStateSpace().execute(cmdUnicode, cmdLatex));
final DisplayData ret = new DisplayData(cmdUnicode.getPrettyPrint());
ret.putLatex('$' + cmdLatex.getPrettyPrint() + '$');
diff --git a/src/main/java/de/prob2/jupyter/commands/RenderCommand.java b/src/main/java/de/prob2/jupyter/commands/RenderCommand.java
index 51d77d6..4e37855 100644
--- a/src/main/java/de/prob2/jupyter/commands/RenderCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/RenderCommand.java
@@ -1,8 +1,13 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
+
import com.google.inject.Inject;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.UserErrorException;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -12,6 +17,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class RenderCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder MIME_TYPE_AND_CONTENT_PARAM = new PositionalParameter.RequiredRemainder("mimeTypeAndContent");
+
@Inject
private RenderCommand() {
super();
@@ -22,6 +29,11 @@ public final class RenderCommand implements Command {
return "::render";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(MIME_TYPE_AND_CONTENT_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return "::render MIMETYPE\nCONTENT";
@@ -39,8 +51,8 @@ public final class RenderCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final String[] split = argString.split("\n", 2);
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
+ final String[] split = args.get(MIME_TYPE_AND_CONTENT_PARAM).split("\n", 2);
if (split.length != 2) {
throw new UserErrorException("Missing content (the content cannot be placed on the same line as the command)");
}
diff --git a/src/main/java/de/prob2/jupyter/commands/ShowCommand.java b/src/main/java/de/prob2/jupyter/commands/ShowCommand.java
index 592ba37..84441d3 100644
--- a/src/main/java/de/prob2/jupyter/commands/ShowCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ShowCommand.java
@@ -16,6 +16,8 @@ import de.prob.animator.domainobjects.AnimationMatrixEntry;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -42,6 +44,11 @@ public final class ShowCommand implements Command {
return ":show";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return Parameters.NONE;
+ }
+
@Override
public @NotNull String getSyntax() {
return ":show";
@@ -58,11 +65,7 @@ public final class ShowCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- if (!argString.isEmpty()) {
- throw new UserErrorException("Expected no arguments");
- }
-
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
if (!trace.getCurrentState().isInitialised()) {
diff --git a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
index f89ee34..d172344 100644
--- a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
@@ -16,6 +16,9 @@ import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -26,6 +29,9 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class SolveCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredSingle SOLVER_PARAM = new PositionalParameter.RequiredSingle("solver");
+ private static final @NotNull PositionalParameter.RequiredRemainder PREDICATE_PARAM = new PositionalParameter.RequiredRemainder("predicate");
+
private static final @NotNull Map<@NotNull String, CbcSolveCommand.@NotNull Solvers> SOLVERS = Arrays.stream(CbcSolveCommand.Solvers.values())
.collect(Collectors.toMap(s -> s.name().toLowerCase(), s -> s));
@@ -45,6 +51,11 @@ public final class SolveCommand implements Command {
return ":solve";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Arrays.asList(SOLVER_PARAM, PREDICATE_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":solve SOLVER PREDICATE";
@@ -67,18 +78,13 @@ public final class SolveCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- final List<String> split = CommandUtils.splitArgs(argString, 2);
- if (split.size() != 2) {
- throw new UserErrorException("Expected 2 arguments, got 1");
- }
-
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
- final CbcSolveCommand.Solvers solver = SOLVERS.get(split.get(0));
+ final CbcSolveCommand.Solvers solver = SOLVERS.get(args.get(SOLVER_PARAM));
if (solver == null) {
- throw new UserErrorException("Unknown solver: " + split.get(0));
+ throw new UserErrorException("Unknown solver: " + args.get(SOLVER_PARAM));
}
- final String code = this.kernelProvider.get().insertLetVariables(split.get(1));
+ final String code = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM));
final IEvalElement predicate = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
final CbcSolveCommand cmd = new CbcSolveCommand(predicate, solver, this.animationSelector.getCurrentTrace().getCurrentState());
diff --git a/src/main/java/de/prob2/jupyter/commands/StatsCommand.java b/src/main/java/de/prob2/jupyter/commands/StatsCommand.java
index 212fd82..8c180dc 100644
--- a/src/main/java/de/prob2/jupyter/commands/StatsCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/StatsCommand.java
@@ -5,9 +5,9 @@ import com.google.inject.Inject;
import de.prob.animator.command.ComputeStateSpaceStatsCommand;
import de.prob.check.StateSpaceStats;
import de.prob.statespace.AnimationSelector;
-
import de.prob2.jupyter.Command;
-import de.prob2.jupyter.UserErrorException;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -30,6 +30,11 @@ public final class StatsCommand implements Command {
return ":stats";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return Parameters.NONE;
+ }
+
@Override
public @NotNull String getSyntax() {
return ":stats";
@@ -46,10 +51,7 @@ public final class StatsCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- if (!argString.isEmpty()) {
- throw new UserErrorException("Expected no arguments");
- }
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final ComputeStateSpaceStatsCommand cmd = new ComputeStateSpaceStatsCommand();
this.animationSelector.getCurrentTrace().getStateSpace().execute(cmd);
final StateSpaceStats stats = cmd.getResult();
diff --git a/src/main/java/de/prob2/jupyter/commands/TableCommand.java b/src/main/java/de/prob2/jupyter/commands/TableCommand.java
index 9a4e3a8..c43bb8c 100644
--- a/src/main/java/de/prob2/jupyter/commands/TableCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TableCommand.java
@@ -18,6 +18,9 @@ import de.prob.statespace.Trace;
import de.prob.unicode.UnicodeTranslator;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -27,6 +30,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class TableCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder EXPRESSION_PARAM = new PositionalParameter.RequiredRemainder("expression");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -43,6 +48,11 @@ public final class TableCommand implements Command {
return ":table";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(EXPRESSION_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":table EXPRESSION";
@@ -59,9 +69,9 @@ public final class TableCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
- final String code = this.kernelProvider.get().insertLetVariables(argString);
+ final String code = this.kernelProvider.get().insertLetVariables(args.get(EXPRESSION_PARAM));
final IEvalElement formula = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
final GetAllTableCommands cmd1 = new GetAllTableCommands(trace.getCurrentState());
diff --git a/src/main/java/de/prob2/jupyter/commands/TimeCommand.java b/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
index ac42663..aacd756 100644
--- a/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TimeCommand.java
@@ -2,12 +2,16 @@ package de.prob2.jupyter.commands;
import java.time.Duration;
import java.time.temporal.ChronoUnit;
+import java.util.Collections;
import com.google.common.base.Stopwatch;
import com.google.inject.Inject;
import com.google.inject.Injector;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -17,6 +21,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class TimeCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder COMMAND_AND_ARGS_PARAM = new PositionalParameter.RequiredRemainder("commandAndArgs");
+
private final @NotNull Injector injector;
@Inject
@@ -31,6 +37,11 @@ public final class TimeCommand implements Command {
return ":time";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(COMMAND_AND_ARGS_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":time COMMAND [ARGS ...]";
@@ -48,10 +59,10 @@ public final class TimeCommand implements Command {
}
@Override
- public @Nullable DisplayData run(final @NotNull String argString) {
+ public @Nullable DisplayData run(final @NotNull ParsedArguments args) {
final ProBKernel kernel = this.injector.getInstance(ProBKernel.class);
final Stopwatch stopwatch = Stopwatch.createStarted();
- final DisplayData result = kernel.eval(argString);
+ final DisplayData result = kernel.eval(args.get(COMMAND_AND_ARGS_PARAM));
stopwatch.stop();
final Duration elapsed = stopwatch.elapsed();
final String text = String.format("Execution time: %d.%09d seconds", elapsed.get(ChronoUnit.SECONDS), elapsed.get(ChronoUnit.NANOS));
diff --git a/src/main/java/de/prob2/jupyter/commands/TraceCommand.java b/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
index 2cb417c..b37af72 100644
--- a/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TraceCommand.java
@@ -7,9 +7,9 @@ import com.google.inject.Inject;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
-
import de.prob2.jupyter.Command;
-import de.prob2.jupyter.UserErrorException;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
@@ -32,6 +32,11 @@ public final class TraceCommand implements Command {
return ":trace";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return Parameters.NONE;
+ }
+
@Override
public @NotNull String getSyntax() {
return ":trace";
@@ -49,11 +54,7 @@ public final class TraceCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
- if (!argString.isEmpty()) {
- throw new UserErrorException("Expected no arguments");
- }
-
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
final StringBuilder sbPlain = new StringBuilder("-1: Root state");
final StringBuilder sbMarkdown = new StringBuilder("* -1: Root state");
diff --git a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
index 8c900cf..d8a9236 100644
--- a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java
@@ -1,5 +1,7 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
+
import com.google.inject.Inject;
import com.google.inject.Provider;
@@ -11,6 +13,9 @@ import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -20,6 +25,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class TypeCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredRemainder FORMULA_PARAM = new PositionalParameter.RequiredRemainder("formula");
+
private final @NotNull Provider<@NotNull ProBKernel> kernelProvider;
private final @NotNull AnimationSelector animationSelector;
@@ -36,6 +43,11 @@ public final class TypeCommand implements Command {
return ":type";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(FORMULA_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":type FORMULA";
@@ -52,9 +64,9 @@ public final class TypeCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final Trace trace = this.animationSelector.getCurrentTrace();
- final String code = this.kernelProvider.get().insertLetVariables(argString);
+ final String code = this.kernelProvider.get().insertLetVariables(args.get(FORMULA_PARAM));
final IEvalElement formula = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND));
final TypeCheckResult result = trace.getStateSpace().typeCheck(formula);
if (result.isOk()) {
diff --git a/src/main/java/de/prob2/jupyter/commands/UnletCommand.java b/src/main/java/de/prob2/jupyter/commands/UnletCommand.java
index b2f7f1e..f3da397 100644
--- a/src/main/java/de/prob2/jupyter/commands/UnletCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/UnletCommand.java
@@ -1,11 +1,15 @@
package de.prob2.jupyter.commands;
+import java.util.Collections;
import java.util.Map;
import com.google.inject.Inject;
import com.google.inject.Injector;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
+import de.prob2.jupyter.PositionalParameter;
import de.prob2.jupyter.ProBKernel;
import de.prob2.jupyter.UserErrorException;
@@ -16,6 +20,8 @@ import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
public final class UnletCommand implements Command {
+ private static final @NotNull PositionalParameter.RequiredSingle NAME_PARAM = new PositionalParameter.RequiredSingle("name");
+
private final @NotNull Injector injector;
@Inject
@@ -30,6 +36,11 @@ public final class UnletCommand implements Command {
return ":unlet";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return new Parameters(Collections.singletonList(NAME_PARAM));
+ }
+
@Override
public @NotNull String getSyntax() {
return ":unlet NAME";
@@ -46,12 +57,13 @@ public final class UnletCommand implements Command {
}
@Override
- public @Nullable DisplayData run(final @NotNull String argString) {
+ public @Nullable DisplayData run(final @NotNull ParsedArguments args) {
final Map<String, String> variables = this.injector.getInstance(ProBKernel.class).getVariables();
- if (!variables.containsKey(argString)) {
- throw new UserErrorException("There is no local variable " + argString);
+ final String name = args.get(NAME_PARAM);
+ if (!variables.containsKey(name)) {
+ throw new UserErrorException("There is no local variable " + name);
}
- variables.remove(argString);
+ variables.remove(name);
return null;
}
diff --git a/src/main/java/de/prob2/jupyter/commands/VersionCommand.java b/src/main/java/de/prob2/jupyter/commands/VersionCommand.java
index c22c7f0..d900dba 100644
--- a/src/main/java/de/prob2/jupyter/commands/VersionCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/VersionCommand.java
@@ -6,6 +6,8 @@ import de.prob.Main;
import de.prob.animator.command.GetVersionCommand;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
+import de.prob2.jupyter.Parameters;
+import de.prob2.jupyter.ParsedArguments;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
@@ -29,6 +31,11 @@ public final class VersionCommand implements Command {
return ":version";
}
+ @Override
+ public @NotNull Parameters getParameters() {
+ return Parameters.NONE;
+ }
+
@Override
public @NotNull String getSyntax() {
return ":version";
@@ -45,7 +52,7 @@ public final class VersionCommand implements Command {
}
@Override
- public @NotNull DisplayData run(final @NotNull String argString) {
+ public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final StringBuilder sb = new StringBuilder("ProB 2 Jupyter kernel: ");
sb.append(ProBKernel.getVersion());
sb.append(" (");
--
GitLab