sequent view and clean

.checkstyle_rules.xml

@@ -43,7 +43,7 @@
 
     <!-- Checks that a package-info.java file exists for each package.     -->
     <!-- See http://checkstyle.sf.net/config_javadoc.html#JavadocPackage -->
-    <module name="JavadocPackage"/>
+    <!-- <module name="JavadocPackage"/> -->
 
     <!-- Checks whether files end with a new line.                        -->
     <!-- See http://checkstyle.sf.net/config_misc.html#NewlineAtEndOfFile -->
@@ -153,7 +153,7 @@
         <module name="AvoidInlineConditionals"/>
         <module name="EmptyStatement"/>
         <module name="EqualsHashCode"/>
-        <module name="HiddenField"/>
+        <!--  <module name="HiddenField"/> -->
         <module name="IllegalInstantiation"/>
         <module name="InnerAssignment"/>
         <module name="MagicNumber"/>
@@ -172,7 +172,7 @@
         <!-- Miscellaneous other checks.                   -->
         <!-- See http://checkstyle.sf.net/config_misc.html -->
         <module name="ArrayTypeStyle"/>
-       <!-- <module name="FinalParameters"/> -->
+        <!-- <module name="FinalParameters"/> -->
         <module name="TodoComment"/>
         <module name="UpperEll"/>
 

pom.xml

@@ -185,7 +185,7 @@
         <dependency>
             <groupId>org.fxmisc.richtext</groupId>
             <artifactId>richtextfx</artifactId>
-            <version>0.6.10</version>
+            <version>0.7-M5</version>
         </dependency>
         <dependency>
             <groupId>junit</groupId>

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

@@ -61,7 +61,7 @@ public class ContractChooser extends Dialog<Contract> {
     }
 
     private class ContractListCell extends ListCell<Contract> {
-        public ContractListCell(ListView<Contract> contractListView) {
+        ContractListCell(ListView<Contract> contractListView) {
             itemProperty().addListener((observable, oldValue, newValue) -> render());
             selectedProperty().addListener((observable, oldValue, newValue) -> render());
         }

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

@@ -141,6 +141,10 @@ public class PuppetMaster {
         return stepUntilBlock;
     }
 
+    public void deinstall() {
+        deinstall(puppet);
+    }
+
     private class EntryListener extends DefaultASTVisitor<Void> {
 
         @Override

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

@@ -2,8 +2,8 @@ package edu.kit.formal.gui.controls;
 
 import org.antlr.v4.runtime.Lexer;
 import org.antlr.v4.runtime.Token;
-import org.fxmisc.richtext.StyleSpans;
-import org.fxmisc.richtext.StyleSpansBuilder;
+import org.fxmisc.richtext.model.StyleSpans;
+import org.fxmisc.richtext.model.StyleSpansBuilder;
 
 import java.util.Collection;
 import java.util.Collections;
@@ -23,7 +23,7 @@ public class ANTLR4LexerHighlighter {
     }
 
 
-    public StyleSpans<Collection<String>> highlight(String sourcecode) {
+    public StyleSpans<? extends Collection<String>> highlight(String sourcecode) {
         Lexer lexer = factory.apply(sourcecode);
         StyleSpansBuilder<Collection<String>> spansBuilder = new StyleSpansBuilder<>();
         try {

src/main/java/edu/kit/formal/gui/controls/LineMapping.java

@@ -7,7 +7,7 @@ import java.util.List;
  * @author Alexander Weigl
  * @version 1 (04.06.17)
  */
-class LineMapping {
+public class LineMapping {
     private List<Integer> marks = new ArrayList<>();
 
     public LineMapping(String value) {
@@ -37,4 +37,16 @@ class LineMapping {
         return getLineStart(line + 1) - 1;
     }
 
+    public int getCharInLine(int caretPosition) {
+        return caretPosition - getLineStart(getLine(caretPosition));
+    }
+
+    public int getLine(int caretPosition) {
+        for (int i = 0; i < marks.size(); i++) {
+            if (caretPosition >= marks.get(i)) {
+                return i;
+            }
+        }
+        return -1;
+    }
 }

src/main/java/edu/kit/formal/gui/controls/ScriptArea.java

@@ -14,7 +14,6 @@ import javafx.collections.ObservableList;
 import javafx.collections.ObservableSet;
 import javafx.geometry.Insets;
 import javafx.geometry.Point2D;
-import javafx.geometry.Pos;
 import javafx.scene.Node;
 import javafx.scene.control.Label;
 import javafx.scene.layout.Background;

src/main/java/edu/kit/formal/gui/controls/SequentView.java

@@ -3,15 +3,13 @@ package edu.kit.formal.gui.controls;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.NamespaceSet;
 import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.pp.IdentitySequentPrintFilter;
-import de.uka.ilkd.key.pp.LogicPrinter;
-import de.uka.ilkd.key.pp.NotationInfo;
-import de.uka.ilkd.key.pp.ProgramPrinter;
+import de.uka.ilkd.key.pp.*;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import javafx.beans.Observable;
 import javafx.beans.property.SimpleObjectProperty;
 import javafx.scene.input.MouseEvent;
+import org.fxmisc.richtext.CharacterHit;
 import org.fxmisc.richtext.CodeArea;
 
 import java.io.StringWriter;
@@ -21,6 +19,7 @@ import java.io.StringWriter;
  * @version 1 (03.06.17)
  */
 public class SequentView extends CodeArea {
+    private Services services;
 
     private LogicPrinter lp;
     private IdentitySequentPrintFilter filter;
@@ -35,24 +34,50 @@ public class SequentView extends CodeArea {
     }
 
     private void hightlight(MouseEvent mouseEvent) {
-        double x = mouseEvent.getX();
-        double y = mouseEvent.getY();
-
-        /*
-        TextAreaSkin skin = (TextAreaSkin) getSkin();
-        int insertionPoint = skin.getInsertionPoint(x, y);
+        if (backend == null) return;
 
+        CharacterHit hit = hit(mouseEvent.getX(), mouseEvent.getY());
+        int insertionPoint = hit.getInsertionIndex();
         PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter);
         if (pis != null) {
-            System.out.println(pis);
             Range r = backend.getPositionTable().rangeForIndex(insertionPoint, getLength());
-
-            selectRange(r.start(), r.end());
+            hightlightRange(r.start(), r.end());
         } else {
-            selectRange(0, 0);
+            hightlightRange(0, 0);
         }
         mouseEvent.consume();
-        */
+    }
+
+    public void mouseClick(MouseEvent e) {
+        if (backend == null) {
+            return;
+        }
+        CharacterHit hit = hit(e.getX(), e.getY());
+        int insertionPoint = hit.getInsertionIndex();
+        PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter);
+
+/*
+        Goal g = new Goal(node, null);
+        ImmutableList<NoPosTacletApp> rules = g.ruleAppIndex().getFindTaclet(new TacletFilter() {
+            @Override
+            protected boolean filter(Taclet taclet) {
+                return true;
+            }
+        }, pis.getPosInOccurrence(), services);
+
+
+        RuleAppIndex index = g.ruleAppIndex();
+*/
+
+    }
+
+    private void hightlightRange(int start, int end) {
+        clearHighlight();
+        setStyleClass(start, end, "sequent-highlight");
+    }
+
+    private void clearHighlight() {
+        clearStyle(0, getLength());
     }
 
     public void update(Observable o) {

src/main/java/edu/kit/formal/gui/model/RootModel.java

@@ -8,11 +8,8 @@ import edu.kit.formal.interpreter.data.State;
 import javafx.beans.property.ListProperty;
 import javafx.beans.property.SimpleListProperty;
 import javafx.beans.property.SimpleObjectProperty;
-import javafx.beans.value.ObservableValue;
 import javafx.collections.FXCollections;
 import javafx.collections.ObservableList;
-import lombok.Getter;
-import lombok.Setter;
 
 import java.io.File;
 
@@ -25,50 +22,38 @@ public class RootModel {
     /**
      * Property: current loaded ScriptFile
      */
-    private final SimpleObjectProperty<File> scriptFile;
+    private final SimpleObjectProperty<File> scriptFile = new SimpleObjectProperty<>();
 
     /**
      * Property: current loaded javaFile
      */
-    private final SimpleObjectProperty<File> javaFile;
+    private final SimpleObjectProperty<File> javaFile = new SimpleObjectProperty<>();
 
     /**
      * Property: current loaded KeY File
      */
-    private final SimpleObjectProperty<File> keYFile;
+    private final SimpleObjectProperty<File> keYFile = new SimpleObjectProperty<>();
 
     /**
      * Property: current loaded script string
      */
-    private ObservableValue<String> currentScript;
+    //private ObservableValue<String> currentScript;
 
     /**
      * ListProperty: list of goal nodes in the current state (depending on interpreter state)
      */
-    private ListProperty<GoalNode<KeyData>> currentGoalNodes;
+    private final ListProperty<GoalNode<KeyData>> currentGoalNodes = new SimpleListProperty<>(FXCollections.observableArrayList());
 
     /**
      * Current SelectedGoalNode
      */
-    private SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoalNode;
+    private final SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoalNode = new SimpleObjectProperty<>();
 
-    private SimpleListProperty<Contract> loadedContracts;
-
-    private SimpleObjectProperty<Contract> chosenContract = new SimpleObjectProperty<>();
-
-
-    @Getter
-    @Setter
-    private State<KeyData> currentState;
+    private final SimpleListProperty<Contract> loadedContracts = new SimpleListProperty<>(FXCollections.observableArrayList());
 
+    private final SimpleObjectProperty<Contract> chosenContract = new SimpleObjectProperty<>();
 
     public RootModel() {
-        javaFile = new SimpleObjectProperty<>();
-        scriptFile = new SimpleObjectProperty<>();
-        keYFile = new SimpleObjectProperty<>();
-        currentSelectedGoalNode = new SimpleObjectProperty<>();
-        currentGoalNodes = new SimpleListProperty<>(FXCollections.observableArrayList());
-        loadedContracts = new SimpleListProperty<>(FXCollections.observableArrayList());
     }
 
 
@@ -159,12 +144,4 @@ public class RootModel {
         this.chosenContract.set(chosenContract);
     }
 
-    public State<KeyData> getCurrentState() {
-        return currentState;
-    }
-
-    public RootModel setCurrentState(State<KeyData> currentState) {
-        this.currentState = currentState;
-        return this;
-    }
 }

src/main/java/edu/kit/formal/interpreter/Execute.java

@@ -8,6 +8,7 @@ import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import edu.kit.formal.interpreter.data.GoalNode;
 import edu.kit.formal.interpreter.data.KeyData;
 import edu.kit.formal.proofscriptparser.Facade;
+import edu.kit.formal.proofscriptparser.ast.ProofScript;
 import org.apache.commons.cli.CommandLine;
 import org.apache.commons.cli.DefaultParser;
 import org.apache.commons.cli.Options;
@@ -37,15 +38,21 @@ public class Execute {
             ProofManagementApi pma = KeYApi.loadFromKeyFile(new File(keyFiles.get(0)));
             ProofApi pa = pma.getLoadedProof();
             ProjectedNode root = pa.getFirstOpenGoal();
-            interpreterBuilder.proof(pa).macros().scriptCommands();
+
+            List<ProofScript> ast = Facade.getAST(scriptFile);
+            interpreterBuilder.proof(pa).macros()
+                    .scriptCommands()
+                    .addProofScripts(ast)
+                    .scriptSearchPath(new File("."));
+
             pa.getProof().getProofIndependentSettings().getGeneralSettings().setOneStepSimplification(false);
+
             Interpreter<KeyData> inter = interpreterBuilder.build();
             KeyData keyData = new KeyData(root.getProofNode(), pa.getEnv(), pa.getProof());
-            inter.interpret(Facade.getAST(scriptFile), new GoalNode<>(null, keyData));
+            inter.newState(new GoalNode<>(null, keyData));
+            inter.interpret(ast.get(0));
             return inter;
-        } catch (ProblemLoaderException e) {
-            e.printStackTrace();
-        } catch (IOException e) {
+        } catch (ProblemLoaderException | IOException e) {
             e.printStackTrace();
         }
         return null;

src/main/java/edu/kit/formal/interpreter/Interpreter.java

@@ -9,6 +9,7 @@ import edu.kit.formal.interpreter.data.GoalNode;
 import edu.kit.formal.interpreter.data.State;
 import edu.kit.formal.interpreter.data.Value;
 import edu.kit.formal.interpreter.data.VariableAssignment;
+import edu.kit.formal.interpreter.exceptions.InterpreterRuntimeException;
 import edu.kit.formal.interpreter.funchdl.CommandLookup;
 import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
 import edu.kit.formal.proofscriptparser.Visitor;
@@ -60,12 +61,11 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
     /**
      * starting point is a statement list
      */
-    public void interpret(List<ProofScript> scripts, GoalNode<T> startGoal) {
-        newState(startGoal);
-        //execute first script (RULE: The first script in the file is main script)
-        ProofScript m = scripts.get(0);
-        //later through interface with getMainScript();
-        m.accept(this);
+    public void interpret(ProofScript script) {
+        if (stateStack.empty()) {
+            throw new InterpreterRuntimeException("no state on stack. call newState before interpret");
+        }
+        script.accept(this);
     }
 
 
@@ -158,7 +158,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
     @Override
     public Void visit(CasesStatement casesStatement) {
         enterScope(casesStatement);
-        State<T> beforeCases = stateStack.peek();
+        State<T> beforeCases = peekState();
 
 
         List<GoalNode<T>> allGoalsBeforeCases = beforeCases.getGoals();
@@ -279,7 +279,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
      * @param goalsToApply @return
      */
     private List<GoalNode<T>> executeCase(Statements caseStmts,
-                                       Map<GoalNode<T>, VariableAssignment> goalsToApply) {
+                                          Map<GoalNode<T>, VariableAssignment> goalsToApply) {
         enterScope(caseStmts);
         List<GoalNode<T>> goalsAfterCases = new ArrayList<>();
 
@@ -439,7 +439,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
     public State<T> getCurrentState() {
         try {
             return stateStack.peek();
-        }catch (EmptyStackException e) {
+        } catch (EmptyStackException e) {
             return new State<T>(null);
             //FIXME
         }
@@ -480,6 +480,11 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
         return stateStack.pop();
     }
 
+
+    public State<T> peekState() {
+        return stateStack.peek();
+    }
+
     public List<GoalNode<T>> getCurrentGoals() {
         return getCurrentState().getGoals();
     }

src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java

@@ -8,9 +8,11 @@ import de.uka.ilkd.key.macros.ProofMacro;
 import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
 import de.uka.ilkd.key.proof.Proof;
 import edu.kit.formal.interpreter.data.KeyData;
+import edu.kit.formal.interpreter.data.VariableAssignment;
 import edu.kit.formal.interpreter.funchdl.*;
 import edu.kit.formal.proofscriptparser.Facade;
 import edu.kit.formal.proofscriptparser.Visitor;
+import edu.kit.formal.proofscriptparser.ast.CallStatement;
 import edu.kit.formal.proofscriptparser.ast.ProofScript;
 import lombok.Getter;
 
@@ -19,6 +21,7 @@ import java.io.IOException;
 import java.util.Arrays;
 import java.util.Collection;
 import java.util.List;
+import java.util.Set;
 
 /**
  * @author Alexander Weigl
@@ -136,4 +139,46 @@ public class InterpreterBuilder {
         pa.getRules().forEach(s -> pmr.getRules().put(s, null));
         return this;
     }
+
+    public InterpreterBuilder setScripts(List<ProofScript> scripts) {
+        psh.getScripts().clear();
+        return addProofScripts(scripts);
+    }
+
+    public InterpreterBuilder inheritState(Interpreter<KeyData> interpreter) {
+        this.interpreter.pushState(interpreter.peekState());
+        return this;
+    }
+
+    public InterpreterBuilder ignoreLines(Set<Integer> lines) {
+        CommandHandler<KeyData> ignoreHandler = new CommandHandler<KeyData>() {
+            @Override
+            public boolean handles(CallStatement call) throws IllegalArgumentException {
+                return lines.contains(call.getStartPosition().getLineNumber());
+            }
+
+            @Override
+            public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params) {
+                System.out.println("InterpreterBuilder.evaluate");
+            }
+        };
+        lookup.getBuilders().add(0, ignoreHandler);
+        return this;
+    }
+
+    public InterpreterBuilder ignoreLinesUntil(final int caretPosition) {
+        CommandHandler<KeyData> ignoreHandler = new CommandHandler<KeyData>() {
+            @Override
+            public boolean handles(CallStatement call) throws IllegalArgumentException {
+                return call.getRuleCtx().getStart().getStartIndex() < caretPosition;
+            }
+
+            @Override
+            public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params) {
+                System.out.println("InterpreterBuilder.evaluate");
+            }
+        };
+        lookup.getBuilders().add(0, ignoreHandler);
+        return this;
+    }
 }

src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java

@@ -4,124 +4,160 @@ import de.uka.ilkd.key.api.KeYApi;
 import de.uka.ilkd.key.api.ProjectedNode;
 import de.uka.ilkd.key.api.ProofApi;
 import de.uka.ilkd.key.api.ProofManagementApi;
+import de.uka.ilkd.key.control.KeYEnvironment;
 import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.init.ProofInputException;
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import de.uka.ilkd.key.speclang.Contract;
-import edu.kit.formal.gui.model.RootModel;
 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.interpreter.exceptions.InterpreterRuntimeException;
-import edu.kit.formal.proofscriptparser.Facade;
-import edu.kit.formal.proofscriptparser.ast.ProofScript;
-import lombok.Getter;
+import javafx.beans.binding.BooleanBinding;
+import javafx.beans.property.SimpleObjectProperty;
+import javafx.concurrent.Task;
 
 import java.io.File;
-import java.io.IOException;
+import java.util.Collection;
+import java.util.Collections;
 import java.util.List;
 
 /**
  * Created by sarah on 5/29/17.
  */
 public class KeYProofFacade {
+    private SimpleObjectProperty<Proof> proof = new SimpleObjectProperty<>();
+    private SimpleObjectProperty<KeYEnvironment> environment = new SimpleObjectProperty<>();
+
+    private SimpleObjectProperty<Contract> contract = new SimpleObjectProperty<>();
+
+    private BooleanBinding readyToExecute = proof.isNotNull();
+
+    //region loading
+    public Task<Void> loadKeyFileTask(File keYFile) {
+        Task<Void> task = new Task<Void>() {
+            @Override
+            protected Void call() throws Exception {
+                loadKeyFile(keYFile);
+                return null;
+            }
+        };
+        return task;
+    }
+
+    public void loadKeyFile(File keYFile) throws ProblemLoaderException {
+        ProofManagementApi pma = KeYApi.loadFromKeyFile(keYFile);
+        ProofApi pa = pma.getLoadedProof();
+        environment.set(pa.getEnv());
+        proof.set(pa.getProof());
+        contract.set(null);
+    }
+
+    public Task<List<Contract>> getContractsForJavaFileTask(File javaFile) {
+        return new Task<List<Contract>>() {
+            @Override
+            protected List<Contract> call() throws Exception {
+                return getContractsForJavaFile(javaFile);
+            }
+        };
+    }
 
-    @Getter
+    //Workaround until api is relaxed
     private ProofManagementApi pma;
-    @Getter
-    private ProofApi pa;
-    @Getter
-    private ProjectedNode currentRoot;
 
-    private RootModel model;
+    public List<Contract> getContractsForJavaFile(File javaFile)
+            throws ProblemLoaderException {
+        pma = KeYApi.loadFromKeyFile(javaFile);
+        //TODO relax key api setEnvironment(pma.getEnvironment());
+        return pma.getProofContracts();
+    }
 
-    @Getter
-    private Interpreter<KeyData> interpreter;
+    public void activateContract(Contract c) throws ProofInputException {
+        ProofApi pa = pma.startProof(c);
+        environment.set(pa.getEnv());
+        proof.set(pa.getProof());
+        contract.set(null);
+    }
+    //endregion
 
+    /**
+     * Build the KeYInterpreter that handles the execution of the loaded key problem file
+     *
+     * @param keYFile
+     * @param scriptText
+     */
+    public InterpreterBuilder buildInterpreter() {
+        assert readyToExecute.getValue();
 
-    public KeYProofFacade(RootModel model) {
-        this.model = model;
+        InterpreterBuilder interpreterBuilder = new InterpreterBuilder();
+        interpreterBuilder.proof(environment.get(), proof.get())
+                .macros()
+                .scriptCommands()
+                .scriptSearchPath(new File("."));
+        getProof().getProofIndependentSettings().getGeneralSettings().setOneStepSimplification(false);
+
+        // Set first state
+        final ProofApi pa = new ProofApi(getProof(), getEnvironment());
+        final ProjectedNode root = pa.getFirstOpenGoal();
+        final KeyData keyData = new KeyData(root.getProofNode(), pa.getEnv(), pa.getProof());
+        final GoalNode<KeyData> startGoal = new GoalNode<>(null, keyData);
+        return interpreterBuilder;
     }
 
-    public State<KeyData> executeScriptWithKeYProblemFile(String currentScriptText, File keyProblemFile) {
-        buildKeYInterpreter(keyProblemFile, false);
-        currentRoot = pa.getFirstOpenGoal();
 
-        KeyData keyData = new KeyData(currentRoot.getProofNode(), pa.getEnv(), pa.getProof());
-        interpreter.interpret(Facade.getAST(currentScriptText), new GoalNode<>(null, keyData));
-        return interpreter.getCurrentState();
+    //region Getter and Setters
+    public Services getService() {
+        //FIXME if key api relaxed
+        return pma != null ? pma.getServices() : getEnvironment().getServices();
     }
 
-    public void prepareEnvWithKeYFile(File keYFile) {
-        try {
-            pma = KeYApi.loadFromKeyFile(keYFile);
-            pa = pma.getLoadedProof();
-            buildKeYInterpreter(keYFile, false);
-        } catch (ProblemLoaderException e) {
-            e.printStackTrace();
-        }
+    public Proof getProof() {
+        return proof.get();
     }
 
-    public List<Contract> getContractsForJavaFile(File javaFile) {
-        try {
-            pma = KeYApi.loadFromKeyFile(javaFile);
+    public SimpleObjectProperty<Proof> proofProperty() {
+        return proof;
+    }
 
-            return pma.getProofContracts();
-        } catch (ProblemLoaderException e) {
-            e.printStackTrace();
-        }
-        return null;
+    public void setProof(Proof proof) {
+        this.proof.set(proof);
     }
 
-    public void prepareEnvForContract(Contract c, File javaFile) {
-        try {
-            pa = pma.startProof(c);
-            buildKeYInterpreter(javaFile, true);