From 718319071f5c6bb7cf17c874f074805e65d1f66b Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Wed, 17 Jan 2018 14:19:46 +0100 Subject: [PATCH] interim term --- .../formal/psdbg/termmatcher/MatcherImpl.java | 102 +++++++++++------- .../psdbg/termmatcher/mp/MatchPath.java | 4 +- .../psdbg/termmatcher/MatcherFacadeTest.java | 6 +- .../dbg/StepIntoReverseCommand.java | 1 + .../dbg/StepOverReverseCommand.java | 11 ++ .../psdbg/gui/controller/DebuggerMain.java | 16 ++- .../psdbg/examples/java/quicksort/script.kps | 23 ++++ .../psdbg/gui/controller/DebuggerMain.fxml | 18 +++- website/docs/language.md | 7 +- 9 files changed, 140 insertions(+), 48 deletions(-) diff --git a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherImpl.java b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherImpl.java index 1b7a9ea6..654635b8 100644 --- a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherImpl.java +++ b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherImpl.java @@ -79,17 +79,28 @@ class MatcherImpl extends MatchPatternDualVisitor { private boolean catchAll = false; private static HashMap reduceConform(Map h1, Map h2) { + HashMap listOfElementsofH1 = new HashMap<>(h1); - HashMap h3 = new HashMap<>(h1); + for (String s1 : listOfElementsofH1.keySet()) { - for (String s1 : h3.keySet()) { - if (!s1.equals("EMPTY_MATCH") && (h2.containsKey(s1) && !h2.get(s1).equals(h1.get(s1)))) { - return null; - } + if (!s1.equals("EMPTY_MATCH") && h2.containsKey(s1)) { + if (h2.get(s1) instanceof MatchPath.MPQuantifiableVariable && + !((QuantifiableVariable) h2.get(s1).getUnit()).name().toString().equals(h1.get(s1).toString())) { + return null; + } + if (h1.get(s1) instanceof MatchPath.MPQuantifiableVariable && + !((QuantifiableVariable) h1.get(s1).getUnit()).name().toString().equals(h2.get(s1).toString())) { + return null; + } + if (!h2.get(s1).equals(h1.get(s1))) { + return null; + } + + } } - h3.putAll(h2); - return h3; + listOfElementsofH1.putAll(h2); + return listOfElementsofH1; } /** @@ -122,6 +133,7 @@ class MatcherImpl extends MatchPatternDualVisitor { return oneMatch ? m3 : NO_MATCH; } + /** * Transform a number term into an int value. *

@@ -449,11 +461,12 @@ class MatcherImpl extends MatchPatternDualVisitor { QuantifiableVariable qv = toMatch.boundVars().get(i); if (qfPattern.getType() == MatchPatternLexer.DONTCARE) { - match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVarible(peek, qv, i))); + //match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVarible(peek, qv, i))); + match = reduceConform(match, EMPTY_MATCH); continue; } if (qfPattern.getType() == MatchPatternLexer.SID) { - match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVarible(peek, qv, i))); + match = reduceConform(match, Matchings.singleton(qfPattern.getText(), new MatchPath.MPQuantifiableVariable(peek, qv, i))); } else { if (!qv.name().toString().equals(qfPattern.getText())) { return NO_MATCH; @@ -464,8 +477,17 @@ class MatcherImpl extends MatchPatternDualVisitor { Matchings fromTerm = accept(ctx.skope, create(peek, 0)); - //return handleBindClause(ctx.bindClause(), path, m); - Matchings retM = reduceConformQuant(fromTerm, match); + Matchings retM = reduceConform(fromTerm, match); + retM.forEach(stringMatchPathMap -> { + stringMatchPathMap.forEach((s, matchPath) -> { + if (matchPath instanceof MatchPath.MPQuantifiableVariable) { + + //create term from variablename and put instead into map + } + } + + ); + }); return handleBindClause(ctx.bindClause(), peek, retM); } @@ -532,32 +554,7 @@ class MatcherImpl extends MatchPatternDualVisitor { } - private Matchings reduceConformQuant(Matchings fromTerm, Matchings match) { - Matchings ret = new Matchings(); - Map quantifiedVarMap = match.first(); - - List> list = fromTerm.stream().filter( - map -> map.entrySet().stream().allMatch( - entry -> { - if (entry.getValue() != null) { - MatchPath mp = (MatchPath) entry.getValue(); - Term mterm = (Term) mp.getUnit(); - if (quantifiedVarMap.containsKey(entry.getKey())) { - return ((QuantifiableVariable) quantifiedVarMap.get(entry.getKey()).getUnit()).name().toString(). - equals(mterm.op().name().toString()); - } else { - return true; - } - } else { - return true; - } - } - ) - ).collect(Collectors.toList()); - ret.addAll(list); - return ret; - } @Override @@ -621,3 +618,36 @@ class MatcherImpl extends MatchPatternDualVisitor { return random.nextInt(); } } +/* private Matchings reduceConformQuant(Matchings fromTerm, Matchings match) { + Matchings ret = new Matchings(); + Map quantifiedVarMap = match.first(); + + System.out.println("quantifiedVarMap = " + quantifiedVarMap); + + List> list = fromTerm.stream().filter( + map -> map.entrySet().stream().allMatch( + entry -> { + System.out.println("entry = " + entry); + if (entry.getValue() != null) { + MatchPath mp = (MatchPath) entry.getValue(); + Term mterm = (Term) mp.getUnit(); + if (quantifiedVarMap.containsKey(entry.getKey())) { + QuantifiableVariable unit = (QuantifiableVariable) quantifiedVarMap.get(entry.getKey()).getUnit(); + return unit.name().toString(). + equals(mterm.op().name().toString()); + } else { + + return true; + } + } else { + //in this case we have an empty match, however, we may have bound quantVars, we need to add them + System.out.println("entry.getKey() = " + entry.getKey()); + return true; + } + } + ) +).collect(Collectors.toList()); + + ret.addAll(list); + return ret; + }*/ \ No newline at end of file diff --git a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPath.java b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPath.java index f235c45f..f82343f2 100644 --- a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPath.java +++ b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPath.java @@ -47,9 +47,9 @@ public abstract class MatchPath { return unit.toString(); } - public static final class MPQuantifiableVarible extends MatchPath { + public static final class MPQuantifiableVariable extends MatchPath { - public MPQuantifiableVarible(MatchPath parent, QuantifiableVariable unit, int pos) { + public MPQuantifiableVariable(MatchPath parent, QuantifiableVariable unit, int pos) { super(parent, unit, pos); } diff --git a/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java b/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java index 2c7bae2a..17de17fe 100644 --- a/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java +++ b/matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java @@ -59,7 +59,11 @@ public class MatcherFacadeTest { shouldMatchForm("fint2(1,i)", "fint2(1,i)"); - shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists _ _)"); + shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists _ ?Term)"); + + shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists ?X _)"); + shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists ?X (fint2(1,?X)))"); + shouldMatchForm("\\exists int i; \\exists int j; fint2(j,i)", "(\\exists i (\\exists j _))"); diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoReverseCommand.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoReverseCommand.java index 1210d22c..9d86bab7 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoReverseCommand.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoReverseCommand.java @@ -15,5 +15,6 @@ public class StepIntoReverseCommand extends DebuggerCommand { info("There is no previous state to the current one."); } dbg.setStatePointer(stepBack); + } } diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepOverReverseCommand.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepOverReverseCommand.java index 4c978385..20db6e7b 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepOverReverseCommand.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepOverReverseCommand.java @@ -1,8 +1,19 @@ package edu.kit.iti.formal.psdbg.interpreter.dbg; +import lombok.val; + public class StepOverReverseCommand extends DebuggerCommand { @Override public void execute(DebuggerFramework dbg) throws DebuggerException { + val statePointer = dbg.getCurrentStatePointer(); + PTreeNode stepOverReverse = statePointer.getStepInvInto() != null ? + statePointer.getStepInvInto() : + statePointer.getStepInvOver(); + + if (stepOverReverse == null) { + info("There is no previous state to the current one."); + } + dbg.setStatePointer(stepOverReverse); } } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java index 920b0580..89536b76 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java @@ -926,6 +926,17 @@ public class DebuggerMain implements Initializable { } } + public void stepOverReverse(ActionEvent actionEvent) { + LOGGER.debug("DebuggerMain.stepBack"); + try { + model.getDebuggerFramework().execute(new StepOverReverseCommand<>()); + } catch (DebuggerException e) { + Utils.showExceptionDialog("", "", "", e); + LOGGER.error(e); + } + } + + public void stepIntoReverse(ActionEvent actionEvent) { LOGGER.debug("DebuggerMain.stepOverReverse"); try { @@ -1114,7 +1125,9 @@ public class DebuggerMain implements Initializable { return FACADE.getContractsForJavaFileTask(model.getJavaFile()); } } + //endregion + //region: StepIntoHandlers @RequiredArgsConstructor private class StepIntoHandler implements java.util.function.Consumer> { private final PTreeNode original; @@ -1169,8 +1182,7 @@ public class DebuggerMain implements Initializable { node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea())); } } - -//endregion + //endregion } //deprecated /* @FXML diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps index 6896cf22..eaaef40a 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps @@ -1,3 +1,26 @@ +script split_from_quicksort_nice1() { + autopilot_prep; + foreach{ + tryclose; + } + foreach{ + simp_upd; + seqPermFromSwap; + andRight; + } + + + cases{ + case match `==> seqDef(_,_,_) = seqDef(_, _, _)`: + auto; + case match `==> (\exists ?X (\exists ?Y _))`: //this should match + instantiate var=`?X`[?X \ X] with=`i_0`; + instantiate var=`?Y`[?Y \ Y] with=`j_0`; + auto; + } +} + + script split_from_quicksort_nice() { autopilot_prep; foreach{ diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml index a64aae40..17d4571b 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml @@ -113,10 +113,20 @@ - + + + + + + @@ -125,7 +135,7 @@ @@ -266,7 +276,7 @@ -