From 2c370dac8bf92892a269c19c3964fb8b99d7c072 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Fri, 4 Aug 2023 19:57:13 +0200
Subject: [PATCH] Begin supporting use of native let variables on the Prolog
side
---
src/main/java/de/prob2/jupyter/ProBKernel.java | 9 +++++++++
.../java/de/prob2/jupyter/commands/AssertCommand.java | 2 +-
src/main/java/de/prob2/jupyter/commands/EvalCommand.java | 2 +-
src/main/java/de/prob2/jupyter/commands/LetCommand.java | 2 +-
4 files changed, 12 insertions(+), 3 deletions(-)
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index daa5953..95d6eb1 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -40,6 +40,8 @@ import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.ClassicalB;
import de.prob.animator.domainobjects.ErrorItem;
import de.prob.animator.domainobjects.EvalElementType;
+import de.prob.animator.domainobjects.EvalExpandMode;
+import de.prob.animator.domainobjects.EvalOptions;
import de.prob.animator.domainobjects.EvalResult;
import de.prob.animator.domainobjects.EventB;
import de.prob.animator.domainobjects.FormulaExpand;
@@ -149,6 +151,13 @@ public final class ProBKernel extends BaseKernel {
private static final @NotNull Pattern BSYMB_COMMAND_PATTERN = Pattern.compile("\\\\([a-z]+)");
private static final @NotNull Pattern LATEX_FORMULA_PATTERN = Pattern.compile("(\\$\\$?)([^\\$]+)\\1");
+ public static final @NotNull EvalOptions EVAL_OPTIONS = EvalOptions.DEFAULT
+ .withProvideStoredLetValues(true)
+ .withEvalExpand(EvalExpandMode.EFFICIENT);
+ public static final @NotNull EvalOptions TRUNCATE_EVAL_OPTIONS = EVAL_OPTIONS
+ .withEvalExpand(EvalExpandMode.NEVER)
+ .withExpand(FormulaExpand.TRUNCATE);
+
private static final @NotNull Collection<@NotNull Class<? extends Command>> COMMAND_CLASSES = Collections.unmodifiableList(Arrays.asList(
AssertCommand.class,
BrowseCommand.class,
diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index 9c974c0..781d113 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
@@ -72,7 +72,7 @@ public final class AssertCommand implements Command {
final ProBKernel kernel = this.kernelProvider.get();
final IEvalElement formula = kernel.parseFormula(args.get(FORMULA_PARAM), FormulaExpand.TRUNCATE);
final AbstractEvalResult result = CommandUtils.withSourceCode(formula, () ->
- kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula))
+ kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula, ProBKernel.TRUNCATE_EVAL_OPTIONS))
);
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/EvalCommand.java b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
index ae399d3..0b2da0e 100644
--- a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java
@@ -67,7 +67,7 @@ public final class EvalCommand implements Command {
final ProBKernel kernel = this.injector.getInstance(ProBKernel.class);
final IEvalElement formula = kernel.parseFormula(args.get(FORMULA_PARAM), FormulaExpand.EXPAND);
return CommandUtils.withSourceCode(formula, () -> {
- final AbstractEvalResult aer = this.animationSelector.getCurrentTrace().evalCurrent(formula);
+ final AbstractEvalResult aer = this.animationSelector.getCurrentTrace().evalCurrent(formula, ProBKernel.EVAL_OPTIONS);
return CommandUtils.displayDataForEvalResult(kernel.postprocessEvalResult(aer));
});
}
diff --git a/src/main/java/de/prob2/jupyter/commands/LetCommand.java b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
index 84b288c..dc6c272 100644
--- a/src/main/java/de/prob2/jupyter/commands/LetCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LetCommand.java
@@ -80,7 +80,7 @@ public final class LetCommand implements Command {
final ProBKernel kernel = this.kernelProvider.get();
final IEvalElement formula = kernel.parseFormula(expression, FormulaExpand.EXPAND);
final AbstractEvalResult evaluated = CommandUtils.withSourceCode(formula, () ->
- kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula))
+ kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula, ProBKernel.EVAL_OPTIONS))
);
if (evaluated instanceof EvalResult) {
kernel.getVariables().put(name, ((EvalResult)evaluated).getValue());
--
GitLab