From cc20826fe3fd2a49a2628d493be1572e6543cb2b Mon Sep 17 00:00:00 2001 From: Sarah Grebing Date: Fri, 18 Aug 2017 20:28:39 +0200 Subject: [PATCH] Interim state: some minor modifications at DebuggerMain and first part of semiseq matching, next part follows tomorrow --- .../formal/psdb/termmatcher/MatchPattern.g4 | 6 +- .../psdb/gui/controller/ContractChooser.java | 21 ++- .../psdb/gui/controller/DebuggerMain.java | 171 ++++++++++-------- .../formal/psdb/gui/controller/Events.java | 10 + .../formal/psdb/gui/controls/ScriptArea.java | 13 +- .../psdb/gui/controls/ScriptController.java | 103 ++++++----- .../graphs/ProofTreeController.java | 2 +- .../psdb/termmatcher/MatcherFacade.java | 72 +++++++- .../formal/psdb/termmatcher/MatcherImpl.java | 101 ++++++----- .../psdb/gui/controller/DebuggerMain.fxml | 20 +- .../psdb/termmatcher/MatcherFacadeTest.java | 47 +++++ .../edu/kit/formal/psdb/termmatcher/test.key | 2 + 12 files changed, 360 insertions(+), 208 deletions(-) diff --git a/src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4 b/src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4 index 831d2f54..2787bdfc 100644 --- a/src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4 +++ b/src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4 @@ -14,7 +14,8 @@ f(..., ...?X...) f(..., ... g(x) ...) f(_, x, _, y, ... y ...) */ - +semiSeqPattern : termPattern (',' termPattern)*; +sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern?; termPattern : DONTCARE #dontCare //| STARDONTCARE #starDontCare @@ -25,8 +26,7 @@ termPattern : /* f(x), f(x,y,g(y)), X, ?Y, _, ..., f(... ?X ...), f(..., ?X), f(..., ...?X...), f(..., ... g(x) ...), f(_, x, _, y, ... y ...) */ -semiSeqPattern : termPattern (',' termPattern)*; -sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern?; + ARROW : '⇒' | '==>'; DONTCARE: '?' | '_' | '█'; diff --git a/src/main/java/edu/kit/formal/psdb/gui/controller/ContractChooser.java b/src/main/java/edu/kit/formal/psdb/gui/controller/ContractChooser.java index 4fd41432..adc80d44 100644 --- a/src/main/java/edu/kit/formal/psdb/gui/controller/ContractChooser.java +++ b/src/main/java/edu/kit/formal/psdb/gui/controller/ContractChooser.java @@ -30,6 +30,12 @@ public class ContractChooser extends Dialog { private final ListView listOfContractsView = new ListView<>(); private final Services services; + public ContractChooser(Services services, + SimpleListProperty contracts) { + this(services); + listOfContractsView.itemsProperty().bind(contracts); + } + public ContractChooser(Services services) { super(); this.services = services; @@ -59,12 +65,6 @@ public class ContractChooser extends Dialog { listOfContractsView.setOnKeyPressed(event -> okButton.fire()); } - public ContractChooser(Services services, - SimpleListProperty contracts) { - this(services); - listOfContractsView.itemsProperty().bind(contracts); - } - public ContractChooser(Services service, List contracts) { this(service); listOfContractsView.itemsProperty().get().setAll(contracts); @@ -97,7 +97,10 @@ public class ContractChooser extends Dialog { private void render() { if (getItem() != null) { - webView.getEngine().loadContent(getItem().getHTMLText(services)); + String content = beautifyContractHTML(getItem().getHTMLText(services), getItem().getTarget().toString()); + webView.getEngine().loadContent(content); + + //webView.getEngine().loadContent(getItem().getHTMLText(services)); //int val = (int) webView.getEngine().executeScript("document.height"); webView.setPrefHeight(150); webView.setDisable(true); @@ -107,5 +110,9 @@ public class ContractChooser extends Dialog { } } } + + private String beautifyContractHTML(String html, String name) { + return "Contract for " + name + "
" + html; + } } } diff --git a/src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java b/src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java index 9f697872..3019e42b 100644 --- a/src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java +++ b/src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java @@ -155,17 +155,6 @@ public class DebuggerMain implements Initializable { } - private void initializeExamples() { - examplesMenu.getItems().clear(); - Examples.loadExamples().forEach(example -> { - MenuItem item = new MenuItem(example.getName()); - item.setOnAction(event -> { - example.open(this); - }); - examplesMenu.getItems().add(item); - }); - } - /** * If the mouse moves other toolbar button, the help text should display in the status bar */ @@ -203,8 +192,16 @@ public class DebuggerMain implements Initializable { proofTreeController.currentHighlightNodeProperty().addListener((observable, oldValue, newValue) -> { scriptController.getDebugPositionHighlighter().highlight(newValue); + }); + /*proofTreeController.currentExecutionEndProperty().addListener((observable, oldValue, newValue) -> { + scriptController.getMainScript().getScriptArea().removeExecutionMarker(); + LineMapping lm = new LineMapping(scriptController.getMainScript().getScriptArea().getText()); + int i = lm.getLineEnd(newValue.getEndPosition().getLineNumber() - 1); + scriptController.getMainScript().getScriptArea().insertExecutionMarker(i); + + });*/ Utils.addDebugListener(proofTreeController.currentGoalsProperty(), Utils::reprKeyDataList); Utils.addDebugListener(proofTreeController.currentSelectedGoalProperty(), Utils::reprKeyData); Utils.addDebugListener(proofTreeController.currentHighlightNodeProperty()); @@ -264,6 +261,17 @@ public class DebuggerMain implements Initializable { return inspectionViewsController; } + private void initializeExamples() { + examplesMenu.getItems().clear(); + Examples.loadExamples().forEach(example -> { + MenuItem item = new MenuItem(example.getName()); + item.setOnAction(event -> { + example.open(this); + }); + examplesMenu.getItems().add(item); + }); + } + public void showCodeDock(ActionEvent actionEvent) { if (!javaAreaDock.isDocked()) { javaAreaDock.dock(dockStation, DockPos.RIGHT); @@ -285,29 +293,16 @@ public class DebuggerMain implements Initializable { } */ //region Actions: Execution - @FXML - public void executeToBreakpoint() { - - } - - - //region Actions: Menu - /* @FXML - public void closeProgram() { - System.exit(0); - }*/ - - /* @FXML - public void openScript() { - File scriptFile = openFileChooserOpenDialog("Select Script File", - "Proof Script File", "kps"); - if (scriptFile != null) { - openScript(scriptFile); - } - }*/ + /** + * When play button is used + */ @FXML public void executeScript() { + executorHelper(); + } + + private void executorHelper() { if (proofTreeController.isAlreadyExecuted()) { File file; boolean isKeyfile = false; @@ -318,6 +313,7 @@ public class DebuggerMain implements Initializable { file = getKeyFile(); } + Task reloading = reloadEnvironment(file, isKeyfile); reloading.setOnSucceeded(event -> { statusBar.publishMessage("Cleared and Reloaded Environment"); @@ -338,8 +334,29 @@ public class DebuggerMain implements Initializable { executeScript(FACADE.buildInterpreter(), false); } + + } + + public File getJavaFile() { + return javaFile.get(); } + //region Actions: Menu + /* @FXML + public void closeProgram() { + System.exit(0); + }*/ + + /* @FXML + public void openScript() { + File scriptFile = openFileChooserOpenDialog("Select Script File", + "Proof Script File", "kps"); + if (scriptFile != null) { + openScript(scriptFile); + } + }*/ + + /* private void saveScript(File scriptFile) { try { scriptController.saveCurrentScriptAs(scriptFile); @@ -371,10 +388,6 @@ public class DebuggerMain implements Initializable { } }*/ - public File getJavaFile() { - return javaFile.get(); - } - public void setJavaFile(File javaFile) { this.javaFile.set(javaFile); } @@ -419,6 +432,7 @@ public class DebuggerMain implements Initializable { */ private void executeScript(InterpreterBuilder ib, boolean debugMode) { Set breakpoints = scriptController.getBreakpoints(); + if (proofTreeController.isAlreadyExecuted()) { proofTreeController.saveGraphs(); } @@ -442,12 +456,6 @@ public class DebuggerMain implements Initializable { } } - /* @FXML - protected void loadKeYFile() { - File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "kps"); - openKeyFile(keyFile); - } - */ public void openKeyFile(File keyFile) { if (keyFile != null) { setKeyFile(keyFile); @@ -456,7 +464,6 @@ public class DebuggerMain implements Initializable { task.setOnSucceeded(event -> { statusBar.publishMessage("Loaded key sourceName: %s", keyFile); statusBar.stopProgress(); - // getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals()); }); task.setOnFailed(event -> { @@ -473,11 +480,6 @@ public class DebuggerMain implements Initializable { } } - - //endregion - - //region Santa's Little Helper - public void openJavaFile(File javaFile) { if (javaFile != null) { setJavaFile(javaFile); @@ -486,6 +488,32 @@ public class DebuggerMain implements Initializable { } } + /* @FXML + protected void loadKeYFile() { + File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "kps"); + openKeyFile(keyFile); + } + */ + + @FXML + public void executeToBreakpoint() { + Set breakpoints = scriptController.getBreakpoints(); + if (breakpoints.size() == 0) { + //we need to add breakpoint at end if no breakpoint exists + } + executorHelper(); + } + + + //endregion + + //region Santa's Little Helper + + @FXML + public void executeInDebugMode() { + executeScript(FACADE.buildInterpreter(), true); + } + @FXML public void saveScript() { try { @@ -501,17 +529,6 @@ public class DebuggerMain implements Initializable { showCodeDock(null); } - /** - * Save KeY proof as proof file - * - * @param - */ - /* public void saveProof(ActionEvent actionEvent) { - - LOGGER.error("saveProof not implemented!!!"); - }*/ - - //endregion //region Santa's Little Helper @@ -554,29 +571,7 @@ public class DebuggerMain implements Initializable { } - //deprecated - @FXML - public void executeScriptFromCursor() { - InterpreterBuilder ib = FACADE.buildInterpreter(); - //b.inheritState(interpreterService.interpreterProperty().get()); - - // Get State before cursor - // use goalnode to build new interpreter in proof tree controller. - // - - - //LineMapping lm = new LineMapping(scriptArea.getText()); - //int line = lm.getLine(scriptArea.getCaretPosition()); - //int inLine = lm.getCharInLine(scriptArea.getCaretPosition()); - - //ib.ignoreLinesUntil(scriptController.getSelectedScriptArea().getCaretPosition()); - //executeScript(ib, true); - } - @FXML - public void executeInDebugMode() { - executeScript(FACADE.buildInterpreter(), true); - } //endregion //region Actions: Menu @@ -883,3 +878,19 @@ public class DebuggerMain implements Initializable { //endregion } +//deprecated + /* @FXML + public void executeScriptFromCursor() { + InterpreterBuilder ib = FACADE.buildInterpreter(); + //b.inheritState(interpreterService.interpreterProperty().get()); + + // Get State before cursor + // use goalnode to build new interpreter in proof tree controller. + // + //LineMapping lm = new LineMapping(scriptArea.getText()); + //int line = lm.getLine(scriptArea.getCaretPosition()); + //int inLine = lm.getCharInLine(scriptArea.getCaretPosition()); + + //ib.ignoreLinesUntil(scriptController.getSelectedScriptArea().getCaretPosition()); + //executeScript(ib, true); + }*/ diff --git a/src/main/java/edu/kit/formal/psdb/gui/controller/Events.java b/src/main/java/edu/kit/formal/psdb/gui/controller/Events.java index 7899041e..e7b8a08f 100644 --- a/src/main/java/edu/kit/formal/psdb/gui/controller/Events.java +++ b/src/main/java/edu/kit/formal/psdb/gui/controller/Events.java @@ -4,6 +4,7 @@ import com.google.common.eventbus.EventBus; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.rule.TacletApp; import edu.kit.formal.psdb.gui.controls.ScriptArea; +import edu.kit.formal.psdb.parser.ast.ASTNode; import edu.kit.formal.psdb.parser.ast.CallStatement; import lombok.Data; import lombok.RequiredArgsConstructor; @@ -48,4 +49,13 @@ public class Events { private final int line; private final CallStatement cs; } + + @Data + @RequiredArgsConstructor + /** + * A new AST node of existing script was executed + */ + public static class NewNodeExecuted { + private final ASTNode correspondingASTNode; + } } diff --git a/src/main/java/edu/kit/formal/psdb/gui/controls/ScriptArea.java b/src/main/java/edu/kit/formal/psdb/gui/controls/ScriptArea.java index e5ddd9cf..7fca4414 100644 --- a/src/main/java/edu/kit/formal/psdb/gui/controls/ScriptArea.java +++ b/src/main/java/edu/kit/formal/psdb/gui/controls/ScriptArea.java @@ -7,11 +7,11 @@ import de.uka.ilkd.key.logic.SequentFormula; import edu.kit.formal.psdb.gui.controller.Events; import edu.kit.formal.psdb.gui.model.Breakpoint; import edu.kit.formal.psdb.gui.model.MainScriptIdentifier; +import edu.kit.formal.psdb.lint.LintProblem; +import edu.kit.formal.psdb.lint.LinterStrategy; import edu.kit.formal.psdb.parser.Facade; import edu.kit.formal.psdb.parser.ScriptLanguageLexer; import edu.kit.formal.psdb.parser.ast.*; -import edu.kit.formal.psdb.lint.LintProblem; -import edu.kit.formal.psdb.lint.LinterStrategy; import javafx.beans.InvalidationListener; import javafx.beans.Observable; import javafx.beans.binding.BooleanBinding; @@ -389,15 +389,19 @@ public class ScriptArea extends CodeArea { return getText().replace("" + EXECUTION_MARKER, ""); } + /** + * Insert Execution marker at absolute character position + * + * @param pos + */ public void insertExecutionMarker(int pos) { LOGGER.debug("ScriptArea.insertExecutionMarker"); Events.register(this); String text = getText(); setText(text.substring(0, pos) + EXECUTION_MARKER + text.substring(pos)); - - } + @Subscribe public void handle(Events.TacletApplicationEvent tap) { LOGGER.debug("ScriptArea.handleTacletApplication"); @@ -430,6 +434,7 @@ public class ScriptArea extends CodeArea { } + private static class GutterView extends HBox { private final SimpleObjectProperty annotation = new SimpleObjectProperty<>(); diff --git a/src/main/java/edu/kit/formal/psdb/gui/controls/ScriptController.java b/src/main/java/edu/kit/formal/psdb/gui/controls/ScriptController.java index 0a9ea511..084a4156 100644 --- a/src/main/java/edu/kit/formal/psdb/gui/controls/ScriptController.java +++ b/src/main/java/edu/kit/formal/psdb/gui/controls/ScriptController.java @@ -55,6 +55,37 @@ public class ScriptController { fsa.getScriptArea().requestFocus(); } + @Subscribe + public void handle(Events.NewNodeExecuted newNode) { + logger.debug("Handling new node added event!"); + ASTNode scriptNode = newNode.getCorrespondingASTNode(); + ScriptArea editor = findEditor(scriptNode); + editor.removeExecutionMarker(); + LineMapping lm = new LineMapping(editor.getText()); + int pos = lm.getLineEnd(scriptNode.getStartPosition().getLineNumber() - 1); + editor.insertExecutionMarker(pos); + } + + private ScriptArea findEditor(ASTNode node) { + File f = new File(node.getRuleContext().getStart().getInputStream().getSourceName()); + return findEditor(f); + } + + /** + * Find the scriptarea for the requested file + * + * @param filePath + * @return + */ + public ScriptArea findEditor(File filePath) { + return openScripts.keySet().stream() + .filter(scriptArea -> + scriptArea.getFilePath().equals(filePath) + ) + .findAny() + .orElse(null); + } + public ObservableMap getOpenScripts() { return openScripts; } @@ -153,38 +184,6 @@ public class ScriptController { return breakpoints; } - /** - * Find the scriptarea for the requested file - * @param filePath - * @return - */ - public ScriptArea findEditor(File filePath) { - return openScripts.keySet().stream() - .filter(scriptArea -> - scriptArea.getFilePath().equals(filePath) - ) - .findAny() - .orElse(null); - } - - /** - * Save the script currently in focus to the specified file - * @param scriptFile - * @throws IOException - */ - public void saveCurrentScriptAs(File scriptFile) throws IOException { - - for (ScriptArea area : openScripts.keySet()) { - - if (openScripts.size() == 1 || area.isFocused()) { - System.out.println(area.getText()); - FileUtils.write(scriptFile, area.getText(), Charset.defaultCharset()); - area.setFilePath(scriptFile); - area.setDirty(false); - } - } - } - public List getCombinedAST() { ArrayList all = new ArrayList<>(); for (ScriptArea area : openScripts.keySet()) { @@ -223,6 +222,25 @@ public class ScriptController { // throw new NotImplementedException(); } + /** + * Save the script currently in focus to the specified file + * + * @param scriptFile + * @throws IOException + */ + public void saveCurrentScriptAs(File scriptFile) throws IOException { + + for (ScriptArea area : openScripts.keySet()) { + + if (openScripts.size() == 1 || area.isFocused()) { + System.out.println(area.getText()); + FileUtils.write(scriptFile, area.getText(), Charset.defaultCharset()); + area.setFilePath(scriptFile); + area.setDirty(false); + } + } + } + public MainScriptIdentifier getMainScript() { return mainScript.get(); } @@ -235,11 +253,6 @@ public class ScriptController { return mainScript; } - private ScriptArea findEditor(ASTNode node) { - File f = new File(node.getRuleContext().getStart().getInputStream().getSourceName()); - return findEditor(f); - } - public class ASTNodeHighlighter { public final String clazzName; private ScriptArea.RegionStyle lastRegion; @@ -249,14 +262,6 @@ public class ScriptController { this.clazzName = clazzName; } - public void remove() { - logger.debug("remove highlight"); - if (lastScriptArea != null) { - logger.debug("previous highlight on {} for {}", lastScriptArea, lastRegion); - lastScriptArea.getMarkedRegions().remove(lastRegion); - } - } - public void highlight(ASTNode node) { logger.debug("Highlight requested for {}", node); remove(); @@ -274,6 +279,14 @@ public class ScriptController { lastRegion = r; } + public void remove() { + logger.debug("remove highlight"); + if (lastScriptArea != null) { + logger.debug("previous highlight on {} for {}", lastScriptArea, lastRegion); + lastScriptArea.getMarkedRegions().remove(lastRegion); + } + } + private ScriptArea.RegionStyle asRegion(ASTNode node) { assert node != null; return new ScriptArea.RegionStyle(node.getRuleContext().getStart().getStartIndex(), diff --git a/src/main/java/edu/kit/formal/psdb/interpreter/graphs/ProofTreeController.java b/src/main/java/edu/kit/formal/psdb/interpreter/graphs/ProofTreeController.java index e482d5b9..70b617c6 100644 --- a/src/main/java/edu/kit/formal/psdb/interpreter/graphs/ProofTreeController.java +++ b/src/main/java/edu/kit/formal/psdb/interpreter/graphs/ProofTreeController.java @@ -106,7 +106,7 @@ public class ProofTreeController { //set value of newly computed node nextComputedNode.setValue(nodeAddedEvent.getAddedNode()); //setNewState(this.statePointer.getState()); - + //Events.fire(new Events.NewNodeExecuted(nodeAddedEvent.getAddedNode().getScriptstmt())); } }; diff --git a/src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java b/src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java index e8cdcef7..126af962 100644 --- a/src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java +++ b/src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java @@ -2,15 +2,21 @@ package edu.kit.formal.psdb.termmatcher; import de.uka.ilkd.key.logic.Semisequent; import de.uka.ilkd.key.logic.Sequent; +import de.uka.ilkd.key.logic.SequentFormula; import de.uka.ilkd.key.logic.Term; import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.CharStreams; import org.antlr.v4.runtime.CommonTokenStream; +import org.key_project.util.collection.ImmutableList; + +import java.util.ArrayList; +import java.util.List; /** * A facade for capturing everthing we want to do with matchers. * * @author Alexander Weigl + * @author S.Grebing */ public class MatcherFacade { public static Matchings matches(String pattern, Term keyTerm) { @@ -37,12 +43,12 @@ public class MatcherFacade { /** * Match a semisequent against a sequent * - * @param pattern Semiseqeuent pattern e.g. f(x), f(x) + * @param pattern Semisequent pattern e.g. f(x), f(x) * @param semiSeq Concrete KeY Semisequent * @return Matchings */ public static Matchings matches(String pattern, Semisequent semiSeq) { - MatcherImpl matcher = new MatcherImpl(); + MatchPatternParser mpp = getParser(pattern); MatchPatternParser.SemiSeqPatternContext ctx = mpp.semiSeqPattern(); return matches(ctx, semiSeq); @@ -50,13 +56,57 @@ public class MatcherFacade { } public static Matchings matches(MatchPatternParser.SemiSeqPatternContext pattern, Semisequent semiSeq) { - //semiSeq.iterator() - // List termPatternContexts = ctx.termPattern(); - // for (MatchPatternParser.TermPatternContext termpattern: termPatternContexts) { - //for all terms in seq - // Matchings s = accept(termpattern, peek); - // } - return null; + MatcherImpl matcher = new MatcherImpl(); + ImmutableList allSequentFormulas = semiSeq.asList(); + + List termPatternContexts = pattern.termPattern(); + + List allMatches = new ArrayList<>(); + + for (MatchPatternParser.TermPatternContext termPatternContext : termPatternContexts) { + Matchings m = new Matchings(); + for (SequentFormula form : allSequentFormulas) { + Matchings temp = matcher.accept(termPatternContext, form.formula()); + m.addAll(temp); + } + allMatches.add(m); + } + + Matchings res = reduceCompatibleMatches(allMatches); + System.out.println("res = " + res); + return res; + } + + /** + * Reduce all matches to only comaptible matchings + * @param allMatches + * @return + */ + private static Matchings reduceCompatibleMatches(List allMatches) { + if (allMatches.size() == 2) { + return MatcherImpl.reduceConform(allMatches.get(0), allMatches.get(1)); + } else { + Matchings tmp = MatcherImpl.reduceConform(allMatches.get(0), allMatches.get(1)); + List list = new ArrayList<>(); + list.add(tmp); + list.addAll(allMatches.subList(2, allMatches.size())); + return reduceCompatibleMatches(list); + } + } + + /** + * Filter matchings s.t. only those remain, that fit the pattern + * + * @param allCompatibelMatchings + * @param pattern + * @return + */ + private static List filterMatchings(List allCompatibelMatchings, MatchPatternParser.SemiSeqPatternContext pattern) { + List ret = new ArrayList<>(); + List termPatternContexts = pattern.termPattern(); + + + return ret; } /** @@ -70,8 +120,10 @@ public class MatcherFacade { MatcherImpl matcher = new MatcherImpl(); MatchPatternParser mpp = getParser(pattern); MatchPatternParser.SequentPatternContext ctx = mpp.sequentPattern(); + Semisequent antec = sequent.antecedent(); + Semisequent succ = sequent.succedent(); - return null; + return matches(pattern,antec); } } diff --git a/src/main/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java b/src/main/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java index 2de3a9ab..727d842e 100644 --- a/src/main/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java +++ b/src/main/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java @@ -20,29 +20,65 @@ class MatcherImpl extends MatchPatternDualVisitor { private Stack termStack = new Stack<>(); /** - * Visit '_' - * - * @param ctx - * @param peek + * Reduce the matchings by eliminating non-compatible matchings. + * For example: + * m1: , and m2: + * @param m1 + * @param m2 * @return */ - @Override - public Matchings visitDontCare(MatchPatternParser.DontCareContext ctx, Term peek) { + protected static Matchings reduceConform(Matchings m1, Matchings m2) { + if (m1 == NO_MATCH || m2 == NO_MATCH) return NO_MATCH; + + Matchings m3 = new Matchings(); + boolean oneMatch = false; + for (HashMap h1 : m1) { + for (HashMap h2 : m2) { + HashMap h3 = reduceConform(h1, h2); + if (h3 != null) { + m3.add(h3); + oneMatch = true; + } + } + } + return oneMatch ? m3 : NO_MATCH; + } + + /*@Override + protected Matchings visitStartDontCare(MatchPatternParser.StarDontCareContext ctx, Term peek) { if (peek != null) { return EMPTY_MATCH; } else { return NO_MATCH; } + }*/ + + private static HashMap reduceConform(HashMap h1, HashMap h2) { + HashMap h3 = new HashMap<>(h1); + for (String s1 : h3.keySet()) { + if (h2.containsKey(s1) && !h2.get(s1).equals(h1.get(s1))) { + return null; + } + } + h3.putAll(h2); + return h3; } - /*@Override - protected Matchings visitStartDontCare(MatchPatternParser.StarDontCareContext ctx, Term peek) { + /** + * Visit '_' + * + * @param ctx + * @param peek + * @return + */ + @Override + public Matchings visitDontCare(MatchPatternParser.DontCareContext ctx, Term peek) { if (peek != null) { return EMPTY_MATCH; } else { return NO_MATCH; } - }*/ + } /** * Visit a Schema Variable @@ -76,7 +112,6 @@ class MatcherImpl extends MatchPatternDualVisitor { return m; } - /** * Visit a function and predicate symbol without a sequent arrow * @param ctx @@ -91,7 +126,7 @@ class MatcherImpl extends MatchPatternDualVisitor { ) { return IntStream.range(0, peek.arity()) .mapToObj(i -> (Matchings) accept(ctx.termPattern(i), peek.sub(i))) - .reduce(this::reduceConform) + .reduce(MatcherImpl::reduceConform) .orElse(NO_MATCH); } return NO_MATCH; @@ -105,6 +140,13 @@ class MatcherImpl extends MatchPatternDualVisitor { */ @Override protected Matchings visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx, Term peek) { + /*Matchings m = new Matchings(); + List termPatterns = ctx.termPattern(); + for (MatchPatternParser.TermPatternContext termPattern : termPatterns) { + System.out.println("Searching for "+termPattern.getText()+" and "+peek.toString()); + Matchings m1 = accept(termPattern,peek); + + }*/ return null; } @@ -119,7 +161,6 @@ class MatcherImpl extends MatchPatternDualVisitor { return null; } - private Stream subTerms(Term peek) { ArrayList list = new ArrayList<>(); subTerms(list, peek); @@ -132,42 +173,6 @@ class MatcherImpl extends MatchPatternDualVisitor { subTerms(list, s); } } - - /** - * Reduce the matchings by eliminating non-compatible matchings. - * For example: - * m1: , and m2: - * @param m1 - * @param m2 - * @return - */ - private Matchings reduceConform(Matchings m1, Matchings m2) { - if (m1 == NO_MATCH || m2 == NO_MATCH) return NO_MATCH; - - Matchings m3 = new Matchings(); - boolean oneMatch = false; - for (HashMap h1 : m1) { - for (HashMap h2 : m2) { - HashMap h3 = reduceConform(h1, h2); - if (h3 != null) { - m3.add(h3); - oneMatch = true; - } - } - } - return oneMatch ? m3 : NO_MATCH; - } - - private HashMap reduceConform(HashMap h1, HashMap h2) { - HashMap h3 = new HashMap<>(h1); - for (String s1 : h3.keySet()) { - if (h2.containsKey(s1) && !h2.get(s1).equals(h1.get(s1))) { - return null; - } - } - h3.putAll(h2); - return h3; - } } /** diff --git a/src/main/resources/edu/kit/formal/psdb/gui/controller/DebuggerMain.fxml b/src/main/resources/edu/kit/formal/psdb/gui/controller/DebuggerMain.fxml index 3bbcbb39..f9ee8bc0 100644 --- a/src/main/resources/edu/kit/formal/psdb/gui/controller/DebuggerMain.fxml +++ b/src/main/resources/edu/kit/formal/psdb/gui/controller/DebuggerMain.fxml @@ -89,16 +89,16 @@ - - - - - + @@ -157,14 +157,14 @@ -