Skip to content
Snippets Groups Projects
Commit bbddc42a authored by dgelessus's avatar dgelessus
Browse files

Add :type command to display the type of a formula (closes #11)

parent b9176907
No related branches found
No related tags found
No related merge requests found
%% Cell type:code id: tags:
``` prob
:help :type
```
%% Output
```
:type FORMULA
```
Display the type of a formula.
:type FORMULA
Display the type of a formula.
%% Cell type:markdown id: tags:
`:type` works on expressions.
%% Cell type:code id: tags:
``` prob
:type 1
```
%% Output
integer
%% Cell type:code id: tags:
``` prob
:type {}
```
%% Output
set(any)
%% Cell type:code id: tags:
``` prob
:type {1, 2, 3}
```
%% Output
set(integer)
%% Cell type:code id: tags:
``` prob
:type 1..5
```
%% Output
set(integer)
%% Cell type:code id: tags:
``` prob
:type [1, 2, 3]
```
%% Output
seq(integer)
%% Cell type:code id: tags:
``` prob
:type {{(1, 2, 3), (4, 5, 6)}, {(7, 8, 9)}}
```
%% Output
set(set(couple(couple(integer,integer),integer)))
%% Cell type:markdown id: tags:
`:type` works on predicates.
%% Cell type:code id: tags:
``` prob
:type 1 = 1
```
%% Output
pred
%% Cell type:code id: tags:
``` prob
:type #x.(x : INT & x > 1)
```
%% Output
pred
%% Cell type:markdown id: tags:
`:type` displays type errors.
%% Cell type:code id: tags:
``` prob
:type {1, TRUE, "string", {}}
```
%% Output
Error from ProB: Type errors in formula
3 errors:
Error: Type mismatch: Expected INTEGER, but was BOOL in 'TRUE' (:1:4 to 1:8)
Error: Type mismatch: Expected INTEGER, but was STRING in '"string"' (:1:10 to 1:16)
Error: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:20 to 1:22)
%% Cell type:code id: tags:
``` prob
:type 1 + {}
```
%% Output
Error from ProB: Type errors in formula
Error: Type mismatch: Expected INTEGER, but was POW(_A) in '{}' (:1:4 to 1:6)
......@@ -36,6 +36,7 @@ import de.prob2.jupyter.commands.RenderCommand;
import de.prob2.jupyter.commands.SolveCommand;
import de.prob2.jupyter.commands.TableCommand;
import de.prob2.jupyter.commands.TimeCommand;
import de.prob2.jupyter.commands.TypeCommand;
import de.prob2.jupyter.commands.VersionCommand;
import io.github.spencerpark.jupyter.kernel.BaseKernel;
......@@ -70,6 +71,7 @@ public final class ProBKernel extends BaseKernel {
this.commands.put(":help", help);
this.commands.put(":version", injector.getInstance(VersionCommand.class));
this.commands.put(":eval", injector.getInstance(EvalCommand.class));
this.commands.put(":type", injector.getInstance(TypeCommand.class));
this.commands.put(":table", injector.getInstance(TableCommand.class));
this.commands.put(":solve", injector.getInstance(SolveCommand.class));
this.commands.put(":load", injector.getInstance(LoadFileCommand.class));
......
package de.prob2.jupyter.commands;
import com.google.inject.Inject;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.animator.domainobjects.IEvalElement;
import de.prob.animator.domainobjects.TypeCheckResult;
import de.prob.exception.ProBError;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob2.jupyter.ProBKernel;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
import org.jetbrains.annotations.NotNull;
public final class TypeCommand implements Command {
private final @NotNull AnimationSelector animationSelector;
@Inject
private TypeCommand(final @NotNull AnimationSelector animationSelector) {
super();
this.animationSelector = animationSelector;
}
@Override
public @NotNull String getSyntax() {
return ":type FORMULA";
}
@Override
public @NotNull String getShortHelp() {
return "Display the type of a formula.";
}
@Override
public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
final Trace trace = this.animationSelector.getCurrentTrace();
final IEvalElement formula = trace.getModel().parseFormula(argString, FormulaExpand.EXPAND);
final TypeCheckResult result = trace.getStateSpace().typeCheck(formula);
if (result.isOk()) {
return new DisplayData(result.getType());
} else {
throw new ProBError("Type errors in formula", result.getErrors());
}
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment