refactor and matcher

pom.xml

@@ -129,7 +129,7 @@
                 </executions>
                 <configuration>
                     <!-- The package of your generated sources -->
-                    <packageName>edu.kit.formal.proofscriptparser.lint</packageName>
+                    <packageName>edu.kit.formal.psdb.lint</packageName>
                 </configuration>
             </plugin>
 
@@ -207,7 +207,7 @@
                                 <transformer
                                         implementation="org.apache.maven.plugins.shade.resource.ManifestResourceTransformer">
                                     <mainClass>
-                                        edu.kit.formal.gui.ProofScriptDebugger
+                                        edu.kit.formal.psdb.gui.ProofScriptDebugger
                                     </mainClass>
                                 </transformer>
                             </transformers>

src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4

+grammar MatchPattern;
+
+/* Examples for testing
+
+f(x)
+f(x,y,g(y))
+X
+?Y
+_
+...
+f(... ?X ...)
+f(..., ?X)
+f(..., ...?X...)
+f(..., ... g(x) ...)
+f(_, x, _, y, ... y ...)
+*/
+
+termPattern :
+	   DONTCARE      #dontCare
+	 //| STARDONTCARE  #starDontCare
+	 | SID           #schemaVar
+	 | STARDONTCARE termPattern STARDONTCARE #anywhere
+	 | func=ID ( '(' termPattern (',' termPattern)* ')')? #function
+	 ;
+/*
+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 : semiSeqPattern? ARROW semiSeqPattern?;
+
+ARROW : '⇒' | '==>';
+DONTCARE: '?' | '_' | '█';
+STARDONTCARE: '...' | '…';
+DIGITS : DIGIT+ ;
+fragment DIGIT : [0-9] ;
+SID: '?' [_a-zA-Z0-9\\]+ ;
+ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])* ;
+COMMENT: '//' ~[\n\r]* -> channel(HIDDEN);
+WS: [\n\f\r\t ] -> channel(HIDDEN);
\ No newline at end of file

src/main/antlr4/edu/kit/formal/termmatcher/MatchPattern.g4

-grammar MatchPattern;
-schemaTerm :
-	   '_'
-	 |'...'
-	 | schemaVar
-	 | logicalVar
-	 | functionSymbol ('('schemaTerm (',' schemaTerm)? ')')?
-	 ;
-
-termHelper :
-      schemaTerm
-	 | functionSymbol '('termHelper (',' termHelper)? ')'
-	 ;
-
-functionSymbol :
-    ID+
-    ;
-
-schemaVar:
-    '?'ID+
-    ;
-
-logicalVar:
-    ID+
-    ;
-
-
-DIGITS : DIGIT+ ;
-fragment DIGIT : [0-9] ;
-ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\' | '[]' | '-')* ;
\ No newline at end of file

src/main/java/edu/kit/formal/proofscriptparser/lint/checkers/IssuesId.java

-package edu.kit.formal.proofscriptparser.lint.checkers;
-
-/**
- * Should correspond to <code>issues-list-en.xml</code>
- *
- * @author Alexander Weigl
- * @version 1 (23.05.17)
- */
-public enum IssuesId {
-    EMPTY_BLOCKS, EQUAL_SCRIPT_NAMES, NEGATED_MATCH_WITH_USING, SUCC_SAME_BLOCK,
-    FOREACH_AFTER_THEONLY,
-    REDECLARE_VARIABLE, REDECLARE_VARIABLE_TYPE_MISMATCH,
-    VARIABLE_NOT_DECLARED,
-    VARIABLE_NOT_USED, THEONLY_AFTER_FOREACH
-}

src/main/java/edu/kit/formal/proofscriptparser/lint/checkers/NegatedMatchWithUsing.java

-package edu.kit.formal.proofscriptparser.lint.checkers;
-
-import edu.kit.formal.proofscriptparser.ast.MatchExpression;
-import edu.kit.formal.proofscriptparser.ast.UnaryExpression;
-import edu.kit.formal.proofscriptparser.lint.Issue;
-import edu.kit.formal.proofscriptparser.lint.IssuesRepository;
-
-/**
- * @author Alexander Weigl
- * @version 1 (23.05.17)
- */
-public class NegatedMatchWithUsing extends AbstractLintRule {
-    private static Issue ISSUE = IssuesRepository.getIssue(IssuesId.NEGATED_MATCH_WITH_USING);
-
-    public NegatedMatchWithUsing() {
-        super(NMWUSearcher::new);
-    }
-
-    static class NMWUSearcher extends Searcher {
-        @Override
-        public Void visit(UnaryExpression ue) {
-            if (ue.getExpression() instanceof MatchExpression) {
-                MatchExpression me = (MatchExpression) ue.getExpression();
-                if (me.getSignature() != null && me.getSignature().size() > 0) {
-                    problem(ISSUE, ue, me);
-                }
-            }
-            return super.visit(ue);
-        }
-    }
-}

src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java → src/main/java/edu/kit/formal/psdb/gui/ProofScriptDebugger.java

-package edu.kit.formal.gui;
+package edu.kit.formal.psdb.gui;
 
 /**
  * Main Entry for Debugger GUI
@@ -17,7 +17,6 @@ import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 import org.dockfx.DockNode;
 
-import java.io.IOException;
 import java.util.Locale;
 
 public class ProofScriptDebugger extends Application {
@@ -36,9 +35,9 @@ public class ProofScriptDebugger extends Application {
         Locale.setDefault(Locale.ENGLISH);
 
         try {
-            FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource("/DebuggerMain.fxml"));
+            FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource("/edu/kit/formal/psdb/gui/controller/DebuggerMain.fxml"));
             Parent root = fxmlLoader.load();
-            //DebuggerMainWindowController controller = fxmlLoader.<DebuggerMainWindowController>getController();
+            //DebuggerMain controller = fxmlLoader.<DebuggerMain>getController();
             Scene scene = new Scene(root);
             primaryStage.setOnCloseRequest(event -> Platform.exit());
             scene.getStylesheets().addAll(

src/main/java/edu/kit/formal/gui/controller/ContractChooser.java → src/main/java/edu/kit/formal/psdb/gui/controller/ContractChooser.java

-package edu.kit.formal.gui.controller;
+package edu.kit.formal.psdb.gui.controller;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.speclang.Contract;
 import javafx.beans.property.ObjectProperty;
 import javafx.beans.property.SimpleListProperty;
 import javafx.collections.ObservableList;
-import javafx.event.EventHandler;
 import javafx.scene.control.*;
 import javafx.scene.layout.VBox;
 import javafx.stage.Modality;
 import lombok.Getter;
 
-import java.awt.event.KeyEvent;
 import java.util.List;
 
 /**

src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java → src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java

-package edu.kit.formal.gui.controller;
+package edu.kit.formal.psdb.gui.controller;
 
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
 import de.uka.ilkd.key.api.ProofApi;
 import de.uka.ilkd.key.proof.init.ProofInputException;
 import de.uka.ilkd.key.speclang.Contract;
-import edu.kit.formal.gui.ProofScriptDebugger;
-import edu.kit.formal.gui.controls.*;
-import edu.kit.formal.gui.model.InspectionModel;
-import edu.kit.formal.interpreter.Interpreter;
-import edu.kit.formal.interpreter.InterpreterBuilder;
-import edu.kit.formal.interpreter.KeYProofFacade;
-import edu.kit.formal.interpreter.data.KeyData;
-import edu.kit.formal.interpreter.graphs.PTreeNode;
-import edu.kit.formal.interpreter.graphs.ProofTreeController;
-import edu.kit.formal.proofscriptparser.ast.ProofScript;
+import edu.kit.formal.psdb.gui.ProofScriptDebugger;
+import edu.kit.formal.psdb.gui.controls.*;
+import edu.kit.formal.psdb.gui.model.InspectionModel;
+import edu.kit.formal.psdb.interpreter.Interpreter;
+import edu.kit.formal.psdb.interpreter.InterpreterBuilder;
+import edu.kit.formal.psdb.interpreter.KeYProofFacade;
+import edu.kit.formal.psdb.interpreter.data.KeyData;
+import edu.kit.formal.psdb.interpreter.graphs.PTreeNode;
+import edu.kit.formal.psdb.interpreter.graphs.ProofTreeController;
+import edu.kit.formal.psdb.parser.ast.ProofScript;
 import javafx.beans.property.*;
 import javafx.beans.value.ChangeListener;
 import javafx.beans.value.ObservableBooleanValue;
@@ -52,9 +52,9 @@ import java.util.concurrent.Executors;
  * @author S.Grebing
  * @author Alexander Weigl
  */
-public class DebuggerMainWindowController implements Initializable {
+public class DebuggerMain implements Initializable {
     public static final KeYProofFacade FACADE = new KeYProofFacade();
-    protected static final Logger LOGGER = LogManager.getLogger(DebuggerMainWindowController.class);
+    protected static final Logger LOGGER = LogManager.getLogger(DebuggerMain.class);
     public final ContractLoaderService contractLoaderService = new ContractLoaderService();
     private final ProofTreeController proofTreeController = new ProofTreeController();
     private final InspectionViewsController inspectionViewsController = new InspectionViewsController();
@@ -494,12 +494,12 @@ public class DebuggerMainWindowController implements Initializable {
     }
 
     public void stepOver(ActionEvent actionEvent) {
-        LOGGER.debug("DebuggerMainWindowController.stepOver");
+        LOGGER.debug("DebuggerMain.stepOver");
         PTreeNode newState = proofTreeController.stepOver();
     }
 
     public void stepBack(ActionEvent actionEvent) {
-        LOGGER.debug("DebuggerMainWindowController.stepBack");
+        LOGGER.debug("DebuggerMain.stepBack");
         PTreeNode newState = proofTreeController.stepBack();
     }
 

src/main/java/edu/kit/formal/gui/controller/Events.java → src/main/java/edu/kit/formal/psdb/gui/controller/Events.java

-package edu.kit.formal.gui.controller;
+package edu.kit.formal.psdb.gui.controller;
 
 import com.google.common.eventbus.EventBus;
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.rule.TacletApp;
-import edu.kit.formal.gui.controls.ScriptArea;
-import edu.kit.formal.proofscriptparser.ast.CallStatement;
+import edu.kit.formal.psdb.gui.controls.ScriptArea;
+import edu.kit.formal.psdb.parser.ast.CallStatement;
 import lombok.Data;
 import lombok.RequiredArgsConstructor;
 

src/main/java/edu/kit/formal/gui/controller/PuppetMaster.java → src/main/java/edu/kit/formal/psdb/gui/controller/PuppetMaster.java

-package edu.kit.formal.gui.controller;
-
-import edu.kit.formal.interpreter.HistoryListener;
-import edu.kit.formal.interpreter.Interpreter;
-import edu.kit.formal.interpreter.data.GoalNode;
-import edu.kit.formal.interpreter.data.KeyData;
-import edu.kit.formal.interpreter.data.State;
-import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
-import edu.kit.formal.proofscriptparser.Visitor;
-import edu.kit.formal.proofscriptparser.ast.*;
+package edu.kit.formal.psdb.gui.controller;
+
+import edu.kit.formal.psdb.interpreter.HistoryListener;
+import edu.kit.formal.psdb.interpreter.Interpreter;
+import edu.kit.formal.psdb.interpreter.data.GoalNode;
+import edu.kit.formal.psdb.interpreter.data.KeyData;
+import edu.kit.formal.psdb.interpreter.data.State;
+import edu.kit.formal.psdb.parser.DefaultASTVisitor;
+import edu.kit.formal.psdb.parser.Visitor;
+import edu.kit.formal.psdb.parser.ast.*;
 import javafx.application.Platform;
 import javafx.beans.property.SimpleObjectProperty;
 

src/main/java/edu/kit/formal/gui/controls/ANTLR4LexerHighlighter.java → src/main/java/edu/kit/formal/psdb/gui/controls/ANTLR4LexerHighlighter.java

-package edu.kit.formal.gui.controls;
+package edu.kit.formal.psdb.gui.controls;
 
 import org.antlr.v4.runtime.Lexer;
 import org.antlr.v4.runtime.Token;

src/main/java/edu/kit/formal/gui/controls/BaseCodeArea.java → src/main/java/edu/kit/formal/psdb/gui/controls/BaseCodeArea.java

-package edu.kit.formal.gui.controls;
+package edu.kit.formal.psdb.gui.controls;
 
 import javafx.beans.property.BooleanProperty;
 import javafx.beans.property.MapProperty;

src/main/java/edu/kit/formal/gui/controls/CustomTabPaneSkin.java → src/main/java/edu/kit/formal/psdb/gui/controls/CustomTabPaneSkin.java

-package edu.kit.formal.gui.controls;
+package edu.kit.formal.psdb.gui.controls;
 
 import com.sun.javafx.scene.control.skin.TabPaneSkin;
 import javafx.scene.Node;

src/main/java/edu/kit/formal/gui/controls/DebuggerStatusBar.java → src/main/java/edu/kit/formal/psdb/gui/controls/DebuggerStatusBar.java

-package edu.kit.formal.gui.controls;
-
-import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
-import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
-import edu.kit.formal.gui.controller.Events;
-import edu.kit.formal.gui.model.MainScriptIdentifier;
-import javafx.beans.property.*;
-import javafx.beans.value.ObservableStringValue;
-import javafx.collections.FXCollections;
-import javafx.collections.ObservableList;
-import javafx.event.ActionEvent;
+package edu.kit.formal.psdb.gui.controls;
+
+import edu.kit.formal.psdb.gui.controller.Events;
+import edu.kit.formal.psdb.gui.model.MainScriptIdentifier;
+import javafx.beans.property.ObjectProperty;
+import javafx.beans.property.SimpleObjectProperty;
 import javafx.event.EventHandler;
-import javafx.scene.control.*;
-import javafx.scene.input.MouseButton;
+import javafx.scene.control.Control;
+import javafx.scene.control.Label;
+import javafx.scene.control.ProgressIndicator;
 import javafx.scene.input.MouseEvent;
-import javafx.scene.layout.BorderPane;
-import javafx.stage.Modality;
-import org.apache.logging.log4j.Level;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
-import org.apache.logging.log4j.core.Appender;
-import org.apache.logging.log4j.core.LogEvent;
-import org.apache.logging.log4j.core.appender.AbstractAppender;
-import org.apache.logging.log4j.core.layout.PatternLayout;
 import org.controlsfx.control.StatusBar;
 
-import java.util.Date;
-import java.util.LinkedList;
-
 /**
- * Created by weigl on 09.06.2017.
+ * Created on 09.06.2017
+ *
+ * @author Alexander Weigl
  */
 public class DebuggerStatusBar extends StatusBar {
     private static final Logger LOGGER = LogManager.getLogger(DebuggerStatusBar.class);
-    private final Appender loggerHandler = createAppender();
-    private final ContextMenu contextMenu = createContextMenu();
+    //private final Dialog<Void> loggerDialog = createDialog();
+    //private final ContextMenu contextMenu = createContextMenu();
+    //private final Appender loggerHandler = createAppender();
+    //private LogCatchHandlerFX logCatchHandler = new LogCatchHandlerFX();
+
     private ObjectProperty<MainScriptIdentifier> mainScriptIdentifier = new SimpleObjectProperty<>();
     private Label lblCurrentNodes = new Label("#nodes: %s");
     private Label lblMainscript = new Label();
     private ProgressIndicator progressIndicator = new ProgressIndicator();
-    private LogCatchHandlerFX logCatchHandler = new LogCatchHandlerFX();
-    private final Dialog<Void> loggerDialog = createDialog();
     private EventHandler<MouseEvent> toolTipHandler = event -> {
         publishMessage(((Control) event.getTarget()).getTooltip().getText());
     };
 
     public DebuggerStatusBar() {
-        listenOnField("psdbg");
+        //listenOnField("psdbg");
 
         getRightItems().addAll(
                 lblMainscript,
@@ -53,11 +42,11 @@ public class DebuggerStatusBar extends StatusBar {
                 progressIndicator
         );
 
-        setOnMouseClicked(event -> {
+        /*setOnMouseClicked(event -> {
             if (event.getButton() == MouseButton.SECONDARY) {
                 contextMenu.show(this, event.getScreenX(), event.getScreenY());
             }
-        });
+        });*/
 
 
         mainScriptIdentifier.addListener((ov, o, n) -> {
@@ -84,9 +73,9 @@ public class DebuggerStatusBar extends StatusBar {
                 Events.fire(new Events.FocusScriptArea(area));
             }
         });
-
     }
 
+    /*
     private Appender createAppender() {
         PatternLayout layout = PatternLayout.createDefaultLayout();
         return new AbstractAppender("", null, layout) {
@@ -95,7 +84,7 @@ public class DebuggerStatusBar extends StatusBar {
                 publishMessage(event.getMessage().getFormattedMessage());
             }
         };
-    }
+    }*/
 
     public void publishMessage(String format, Object... args) {
         String msg = String.format(format, args);
@@ -106,22 +95,24 @@ public class DebuggerStatusBar extends StatusBar {
         return toolTipHandler;
     }
 
+    /*
     public void listenOnField(ObservableStringValue value) {
         value.addListener((observable, oldValue, newValue) -> {
             publishMessage(newValue);
         });
-    }
+    }*/
 
+    /*
     public void listenOnField(Logger logger) {
         org.apache.logging.log4j.core.Logger plogger = ((org.apache.logging.log4j.core.Logger) logger); // Bypassing the public API
         plogger.addAppender(loggerHandler);
         plogger.addAppender(logCatchHandler);
         logger.info("Listener added");
-    }
+    }*/
 
-    public void listenOnField(String loggerCategory) {
+    /*public void listenOnField(String loggerCategory) {
         listenOnField(LogManager.getLogger(loggerCategory));
-    }
+    }*/
 
     public void indicateProgress() {
         progressIndicator.setProgress(-1);
@@ -131,14 +122,14 @@ public class DebuggerStatusBar extends StatusBar {
         progressIndicator.setProgress(100);
     }
 
-    public ContextMenu createContextMenu() {
+    /*public ContextMenu createContextMenu() {
         ContextMenu cm = new ContextMenu();
         Menu viewOptions = new Menu("View Options");
         MenuItem showLog = new MenuItem("Show Log", new MaterialDesignIconView(MaterialDesignIcon.FORMAT_LIST_BULLETED));
         showLog.setOnAction(this::showLog);
         cm.getItems().addAll(viewOptions, showLog);
         return cm;
-    }
+    }*/
 
     public MainScriptIdentifier getMainScriptIdentifier() {
         return mainScriptIdentifier.get();
@@ -151,12 +142,14 @@ public class DebuggerStatusBar extends StatusBar {
     public ObjectProperty<MainScriptIdentifier> mainScriptIdentifierProperty() {
         return mainScriptIdentifier;
     }
+}
 
+    /*
     private void showLog(ActionEvent actionEvent) {
         loggerDialog.show();
-    }
+    }*/
 
-    public Dialog<Void> createDialog() {
+    /*public Dialog<Void> createDialog() {
         final TableView<LogEvent> recordView = new TableView<>(logCatchHandler.recordsProperty());
         recordView.setEditable(false);
         recordView.setSortPolicy(param -> false);
@@ -180,30 +173,21 @@ public class DebuggerStatusBar extends StatusBar {
         messageColumn.setCellValueFactory(
                 param -> {
                     return new SimpleStringProperty(param.getValue().getMessage().getFormattedMessage());
-                    /*String s = formatter.formatMessage(param.getValue());
-                    if (param.getValue().getThrown() != null) {
-                        StringWriter sw = new StringWriter();
-                        PrintWriter pw = new PrintWriter(sw);
-                        pw.println();
-                        param.getValue().getThrown().printStackTrace(pw);
-                        pw.close();
-                        s += "\n" + sw.toString();
-                    }
-                    return new SimpleStringProperty(s);*/
-                }
+}
         );
 
 
-        Dialog<Void> dialog = new Dialog<>();
+                Dialog<Void> dialog=new Dialog<>();
         dialog.setResizable(true);
         dialog.initModality(Modality.NONE);
         dialog.setHeaderText("Logger Records");
-        DialogPane dpane = dialog.getDialogPane();
+        DialogPane dpane=dialog.getDialogPane();
         dpane.setContent(new BorderPane(recordView));
         dpane.getButtonTypes().setAll(ButtonType.CLOSE);
         return dialog;
-    }
+        }*/
 
+/*
     public static class LogCatchHandlerFX extends AbstractAppender {
         private ListProperty<LogEvent> records = new SimpleListProperty<>(FXCollections.observableList(
                 new LinkedList<>() //remove of head
@@ -243,6 +227,6 @@ public class DebuggerStatusBar extends StatusBar {
             this.maxRecords = maxRecords;
         }
     }
-}
+    }*/
 
 

src/main/java/edu/kit/formal/gui/controls/GoalOptionsMenu.java → src/main/java/edu/kit/formal/psdb/gui/controls/GoalOptionsMenu.java

-package edu.kit.formal.gui.controls;
+package edu.kit.formal.psdb.gui.controls;
 
 import com.google.common.collect.BiMap;
 import com.google.common.collect.HashBiMap;
-import edu.kit.formal.interpreter.data.KeyData;
+import edu.kit.formal.psdb.interpreter.data.KeyData;
 import javafx.beans.property.ObjectProperty;
 import javafx.beans.property.SimpleObjectProperty;
 import javafx.fxml.FXML;

src/main/java/edu/kit/formal/gui/controls/InspectionView.java → src/main/java/edu/kit/formal/psdb/gui/controls/InspectionView.java

-package edu.kit.formal.gui.controls;
+package edu.kit.formal.psdb.gui.controls;
 
-import edu.kit.formal.gui.model.InspectionModel;
-import edu.kit.formal.interpreter.data.GoalNode;
-import edu.kit.formal.interpreter.data.KeyData;
+import edu.kit.formal.psdb.gui.model.InspectionModel;