introduce lining

src/main/java/edu/kit/formal/dbg/Blocker.java

 package edu.kit.formal.dbg;
 
 import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
-import edu.kit.formal.proofscriptparser.ast.ASTNode;
+import edu.kit.formal.proofscriptparser.ast.*;
 
 import java.util.Set;
 import java.util.TreeSet;
-import java.util.concurrent.Semaphore;
 import java.util.concurrent.atomic.AtomicInteger;
 import java.util.concurrent.locks.Condition;
 import java.util.concurrent.locks.Lock;
-import java.util.concurrent.locks.LockSupport;
 import java.util.concurrent.locks.ReentrantLock;
 
 /**
  * Created by weigl on 21.05.2017.
  */
 public class Blocker extends DefaultASTVisitor<Void> {
-    public AtomicInteger stepUntilBlock = new AtomicInteger(-1);
+    AtomicInteger stepUntilBlock = new AtomicInteger(-1);
     //needs to threadable
-    public Set<Integer> brkpnts = new TreeSet<>();
-    public final Lock lock = new ReentrantLock();
-    public final Condition block = lock.newCondition();
+    Set<Integer> brkpnts = new TreeSet<>();
+    final Lock lock = new ReentrantLock();
+    final Condition block = lock.newCondition();
 
-    @Override
-    public Void defaultVisit(ASTNode node) {
+    //better a semaphore?
+    //Semaphore semaphore = new Semaphore();
+
+    public Void checkForHalt(ASTNode node) {
         if (stepUntilBlock.get() > 0)
             stepUntilBlock.decrementAndGet();
 
@@ -61,4 +61,45 @@ public class Blocker extends DefaultASTVisitor<Void> {
             lock.unlock();
         }
     }
+
+
+    @Override
+    public Void visit(ProofScript proofScript) {
+        return checkForHalt(proofScript);
+    }
+
+    @Override
+    public Void visit(AssignmentStatement assignment) {
+        return checkForHalt(assignment);
+    }
+
+    @Override
+    public Void visit(CasesStatement casesStatement) {
+        return checkForHalt(casesStatement);
+    }
+
+    @Override
+    public Void visit(CaseStatement caseStatement) {
+        return checkForHalt(caseStatement);
+    }
+
+    @Override
+    public Void visit(CallStatement call) {
+        return checkForHalt(call);
+    }
+
+    @Override
+    public Void visit(TheOnlyStatement theOnly) {
+        return checkForHalt(theOnly);
+    }
+
+    @Override
+    public Void visit(ForeachStatement foreach) {
+        return checkForHalt(foreach);
+    }
+
+    @Override
+    public Void visit(RepeatStatement repeatStatement) {
+        return checkForHalt(repeatStatement);
+    }
 }

src/main/java/edu/kit/formal/dbg/Debugger.java

@@ -4,14 +4,23 @@ import edu.kit.formal.interpreter.*;
 import edu.kit.formal.interpreter.funchdl.BuiltinCommands;
 import edu.kit.formal.interpreter.funchdl.CommandHandler;
 import edu.kit.formal.interpreter.funchdl.DefaultLookup;
-import edu.kit.formal.proofscriptparser.*;
+import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
+import edu.kit.formal.proofscriptparser.Facade;
+import edu.kit.formal.proofscriptparser.ScriptLanguageParser;
+import edu.kit.formal.proofscriptparser.TransformAst;
 import edu.kit.formal.proofscriptparser.ast.*;
 import org.antlr.v4.runtime.CharStreams;
 
-import java.io.*;
+import java.io.BufferedReader;
+import java.io.File;
+import java.io.IOException;
+import java.io.InputStreamReader;
 import java.math.BigInteger;
+import java.util.Collections;
 import java.util.List;
 import java.util.function.BiConsumer;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
 
 /**
  * @author Alexander Weigl
@@ -30,7 +39,7 @@ public class Debugger {
         DefaultLookup lookup = new DefaultLookup();
         lookup.getBuilders().add(new BuiltinCommands.SplitCommand());
         interpreter = new Interpreter(lookup);
-
+        interpreter.setMatcherApi(new PseudoMatcher());
         history = new HistoryListener(interpreter);
         scripts = Facade.getAST(new File(file));
         interpreter.getEntryListeners().add(history);
@@ -111,7 +120,7 @@ public class Debugger {
         int steps = 1;
         if (il != null)
             steps = il.getValue().intValue();
-        blocker.stepUntilBlock.set(steps * 2); //FIXME times two is strange, something wrong on sync
+        blocker.stepUntilBlock.set(steps); //FIXME times two is strange, something wrong on sync
         //LockSupport.unpark(interpreterThread);
         blocker.unlock();
     }
@@ -247,4 +256,21 @@ public class Debugger {
             return super.visit(repeatStatement);
         }
     }
+
+
+    public static class PseudoMatcher implements MatcherApi {
+        @Override
+        public List<VariableAssignment> matchLabel(GoalNode currentState, String label) {
+            Pattern p = Pattern.compile(label, Pattern.CASE_INSENSITIVE);
+            Matcher m = p.matcher(currentState.getSequent());
+            return m.matches()
+                    ? Collections.singletonList(new VariableAssignment())
+                    : Collections.emptyList();
+        }
+
+        @Override
+        public List<VariableAssignment> matchSeq(GoalNode currentState, String data) {
+            return Collections.emptyList();
+        }
+    }
 }

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

@@ -7,7 +7,6 @@ import lombok.Getter;
 import lombok.Setter;
 
 import java.util.ArrayList;
-import java.util.Collections;
 import java.util.List;
 
 /**
@@ -17,7 +16,8 @@ import java.util.List;
  * @author A. Weigl
  */
 public class Evaluator extends DefaultASTVisitor<Value> implements ScopeObservable {
-    private List<VariableAssignment> matchedVariables = new ArrayList<>();
+    @Getter
+    private final List<VariableAssignment> matchedVariables = new ArrayList<>();
     @Getter
     @Setter
     private MatcherApi matcher;

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

@@ -119,4 +119,9 @@ public class GoalNode {
         //TODO method does nothing helpful atm
         return new GoalNode(this.getParent(), sequent);
     }
+
+    public VariableAssignment enterNewVarScope(VariableAssignment va) {
+        assignments = assignments.push(va);
+        return assignments;
+    }
 }

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

@@ -2,16 +2,13 @@ package edu.kit.formal.interpreter;
 
 import de.uka.ilkd.key.api.ScriptApi;
 import de.uka.ilkd.key.macros.scripts.EngineState;
-import edu.kit.formal.interpreter.funchdl.CommandCall;
 import edu.kit.formal.interpreter.funchdl.CommandLookup;
 import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
 import edu.kit.formal.proofscriptparser.Visitor;
 import edu.kit.formal.proofscriptparser.ast.*;
 import lombok.Getter;
 import lombok.Setter;
-import org.antlr.v4.runtime.ParserRuleContext;
 
-import javax.xml.bind.annotation.XmlSeeAlso;
 import java.util.*;
 import java.util.logging.Logger;
 
@@ -107,13 +104,31 @@ public class Interpreter extends DefaultASTVisitor<Void>
         return null;
     }
 
-    private Value evaluate(Expression expr) {
+
+    public VariableAssignment evaluateWithAssignments(GoalNode g, Expression expr) {
+        enterScope(expr);
+        Evaluator evaluator = new Evaluator(g.getAssignments(), g);
+        evaluator.setMatcher(matcherApi);
+        evaluator.getEntryListeners().addAll(entryListeners);
+        evaluator.getExitListeners().addAll(exitListeners);
+        exitScope(expr);
+        Value value = evaluator.eval(expr);
+        if (value.equals(Value.TRUE)) {
+            if (evaluator.getMatchedVariables().size() == 0)
+                return new VariableAssignment();
+            else
+                return evaluator.getMatchedVariables().get(0);
+        }
+        return null;
+    }
+
+    public Value evaluate(Expression expr) {
         return evaluate(getSelectedNode(), expr);
     }
 
-    private Value evaluate(GoalNode g, Expression expr) {
+    public Value evaluate(GoalNode g, Expression expr) {
         enterScope(expr);
-        Evaluator evaluator = new Evaluator(g.getAssignments(),g);
+        Evaluator evaluator = new Evaluator(g.getAssignments(), g);
         evaluator.setMatcher(matcherApi);
         evaluator.getEntryListeners().addAll(entryListeners);
         evaluator.getExitListeners().addAll(exitListeners);
@@ -145,78 +160,32 @@ public class Interpreter extends DefaultASTVisitor<Void>
     @Override
     public Void visit(CasesStatement casesStatement) {
         enterScope(casesStatement);
-        State beforeCases = (State) stateStack.pop();
-        List<GoalNode> allGoalsBeforeCases = beforeCases.getGoals();
-        for (GoalNode node : allGoalsBeforeCases) {
-            node.enterNewVarScope();
-        }
         List<GoalNode> goalsAfterCases = new ArrayList<>();
         //copy the list of goal nodes for keeping track of goals
-        Set<GoalNode> copiedList = new HashSet<>();
-        for (GoalNode goalNode : allGoalsBeforeCases) {
-            copiedList.add(goalNode);
-        }
+        Set<GoalNode> currentGoals = new HashSet<>(getCurrentGoals());
+        //List<Map<GoalNode, VariableAssignment>> matchedGoals = new ArrayList<>();
 
-        //handle cases
-        List<CaseStatement> cases = casesStatement.getCases();
-        Iterator<CaseStatement> casesIter = cases.iterator();
-        while (casesIter.hasNext()) {
-            //get information for case
-            CaseStatement currentCase = casesIter.next();
-            Expression guard = currentCase.getGuard();
-            Statements body = currentCase.getBody();
-
-
-            Iterator<GoalNode> goalIter = copiedList.iterator();
-            Set<GoalNode> forCase = new HashSet<>();
-            //iterate over all available goals and select those that evaluate to true with the guard
-            //assumption, matchpattern handles varAssignments
-            while (goalIter.hasNext()) {
-                GoalNode g = goalIter.next();
-                Value eval = evaluate(g, guard);
-                System.out.println();
-                if (eval.getData().equals(true)) {
-                    forCase.add(g);
-                }
-            }
-            copiedList.removeAll(forCase);
-
-            //for each selected goal put a state onto tze stack and visit the body of the case
-            Iterator<GoalNode> caseGoals = forCase.iterator();
-            while (caseGoals.hasNext()) {
-                GoalNode current = caseGoals.next();
-                List<GoalNode> goalList = new ArrayList<>();
-                goalList.add(current);
-                State s = new State(goalList, current);
-                stateStack.push(s);
-                visit(body);
-                //after executing the body collect the newly created goals form the stack and remove the state
-                State aftercase = (State) stateStack.pop();
-                goalsAfterCases.addAll(aftercase.getGoals());
-            }
 
-        }
-        //for all remaining goals execute default
-        if (!copiedList.isEmpty()) {
-            Statements defaultCase = casesStatement.getDefaultCase();
-            Iterator<GoalNode> remainingGoalsIter = copiedList.iterator();
-            while (remainingGoalsIter.hasNext()) {
-                GoalNode next = remainingGoalsIter.next();
-                List<GoalNode> goalList = new ArrayList<>();
-                goalList.add(next);
-                State s = new State(goalList, next);
-                stateStack.push(s);
-                visit(defaultCase);
-                State aftercase = (State) stateStack.pop();
-                goalsAfterCases.addAll(aftercase.getGoals());
+        for (CaseStatement currentCase : casesStatement.getCases()) {
+            //calculate the goal nodes activations
+            Map<GoalNode, VariableAssignment> mg = getMatchedGoal(currentGoals, currentCase);
+            //matchedGoals.add(mg);
+            currentGoals.removeAll(mg.keySet());
 
+            // execute
+            for (Map.Entry<GoalNode, VariableAssignment> s : mg.entrySet()) {
+                enterScope(currentCase);
+                executeStatements(currentCase.getBody(), s.getKey(), s.getValue());
+                exitScope(currentCase);
             }
-
-
         }
 
-        //exit scope and create a new state using the union of all newly created goals
+        // execute
+        for (GoalNode s : currentGoals) {
+            executeStatements(casesStatement.getDefaultCase(), s, new VariableAssignment());
+        }
 
+        /*/exit scope and create a new state using the union of all newly created goals
         State newStateAfterCases;
         if (!goalsAfterCases.isEmpty()) {
             for (GoalNode goalAfterCases : goalsAfterCases) {
@@ -228,12 +197,40 @@ public class Interpreter extends DefaultASTVisitor<Void>
                 newStateAfterCases = new State(goalsAfterCases, null);
             }
             stateStack.push(newStateAfterCases);
-        }
+        }*/
 
         exitScope(casesStatement);
         return null;
     }
 
+    public void executeStatements(Statements currentCase, GoalNode gn, VariableAssignment va) {
+        enterScope(currentCase);
+        AbstractState ns = newState(gn);
+        ns.getSelectedGoalNode().enterNewVarScope(va);
+        currentCase.accept(this);
+        mergeGoalsAndPop(ns, gn);
+        exitScope(currentCase);
+    }
+
+    private void mergeGoalsAndPop(AbstractState ns, GoalNode toRemoved) {
+        AbstractState popped = popState();
+        assert popped == ns;
+        getCurrentState().getGoals().remove(toRemoved);
+        getCurrentState().getGoals().addAll(popped.getGoals());
+    }
+
+
+    private Map<GoalNode, VariableAssignment> getMatchedGoal(Collection<GoalNode> currentGoals,
+                                                             CaseStatement currentCase) {
+        Map<GoalNode, VariableAssignment> map = new HashMap<>();
+        for (GoalNode gn : currentGoals) {
+            VariableAssignment va = evaluateWithAssignments(gn, currentCase.getGuard());
+            if (va != null)
+                map.put(gn, va);
+        }
+        return map;
+    }
+
 
     /**
      * @param caseStatement

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

@@ -142,4 +142,11 @@ public class VariableAssignment {
     public Map<String, Value> asMap() {
         return asMap(new HashMap<>());
     }
+
+    public VariableAssignment push(VariableAssignment va) {
+        VariableAssignment p = push();
+        p.values.putAll(va.values);
+        p.types.putAll(va.types);
+        return p;
+    }
 }

src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java

@@ -7,123 +7,155 @@ package edu.kit.formal.proofscriptparser;
  * Copyright (C) 2017 Application-oriented Formal Verification
  * %%
  * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as
+ * it under the terms of the GNU General default License as
  * published by the Free Software Foundation, either version 3 of the
  * License, or (at your option) any later version.
  * 
  * This program is distributed in the hope that it will be useful,
  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
+ * GNU General default License for more details.
  * 
- * You should have received a copy of the GNU General Public
+ * You should have received a copy of the GNU General default
  * License along with this program.  If not, see
  * <http://www.gnu.org/licenses/gpl-3.0.html>.
  * #L%
  */
 
 
-
 import edu.kit.formal.proofscriptparser.ast.*;
 
+import java.util.Map;
+
 /**
  * {@link ASTTraversal} provides a visitor with a a default traversal of the given AST.
  *
  * @author Alexander Weigl
  * @version 1 (29.04.17)
  */
-public class ASTTraversal<T> implements Visitor<T> {
-    @Override public T visit(ProofScript proofScript) {
+public interface ASTTraversal<T> extends Visitor<T> {
+    @Override
+    default T visit(ProofScript proofScript) {
         proofScript.getBody().accept(this);
         return null;
     }
 
-    @Override public T visit(AssignmentStatement assign) {
+    @Override
+    default T visit(AssignmentStatement assign) {
         assign.getLhs().accept(this);
         return null;
     }
 
-    @Override public T visit(BinaryExpression e) {
+    @Override
+    default T visit(BinaryExpression e) {
         e.getLeft().accept(this);
         e.getRight().accept(this);
         return null;
     }
 
-    @Override public T visit(MatchExpression match) {
+    @Override
+    default T visit(MatchExpression match) {
         match.getPattern().accept(this);
         match.getSignature().accept(this);
         return null;
     }
 
-    @Override public T visit(TermLiteral term) {
+    @Override
+    default T visit(TermLiteral term) {
         term.accept(this);
         return null;
     }
 
-    @Override public T visit(StringLiteral string) {
+    @Override
+    default T visit(StringLiteral string) {
         return null;
     }
 
-    @Override public T visit(Variable variable) {
+    @Override
+    default T visit(Variable variable) {
         return null;
     }
 
-    @Override public T visit(BooleanLiteral bool) {
+    @Override
+    default T visit(BooleanLiteral bool) {
         return null;
     }
 
-    @Override public T visit(Statements statements) {
+    @Override
+    default T visit(Statements statements) {
         for (Statement statement : statements) {
             statement.accept(this);
         }
         return null;
     }
 
-    @Override public T visit(IntegerLiteral integer) {
+    @Override
+    default T visit(IntegerLiteral integer) {
         return null;
     }
 
-    @Override public T visit(CasesStatement casesStatement) {
+    @Override
+    default T visit(CasesStatement casesStatement) {
         for (CaseStatement c : casesStatement.getCases()) {
             c.accept(this);
         }
         return null;
     }
 
-    @Override public T visit(CaseStatement caseStatement) {
+    @Override
+    default T visit(CaseStatement caseStatement) {
         caseStatement.getGuard().accept(this);
         caseStatement.getBody().accept(this);
         return null;
     }
 
-    @Override public T visit(CallStatement call) {
+    @Override
+    default T visit(CallStatement call) {
         for (Expression e : call.getParameters().values()) {
             e.accept(this);
         }
         return null;
     }
 
-    @Override public T visit(TheOnlyStatement theOnly) {
+    @Override
+    default T visit(TheOnlyStatement theOnly) {
+        theOnly.getBody().accept(this);
         return null;
     }
 
-    @Override public T visit(ForeachStatement foreach) {
+    @Override
+    default T visit(ForeachStatement foreach) {
+        foreach.getBody().accept(this);
         return null;
     }
 
-    @Override public T visit(RepeatStatement repeatStatement) {
+    @Override
+    default T visit(RepeatStatement repeatStatement) {
+        repeatStatement.getBody().accept(this);
         return null;
     }
 
-    @Override public T visit(Signature signature) {
+    @Override
+    default T visit(Signature signature) {
+        for (Map.Entry<Variable, Type> e : signature.entrySet()) {
+            e.getKey().accept(this);
+        }
         return null;
     }
 
-    @Override public T visit(Parameters parameters) {
+    @Override
+    default T visit(Parameters parameters) {
+        for (Map.Entry<Variable, Expression> e :
+             parameters.entrySet()) {
+            e.getKey().accept(this);
+            e.getValue().accept(this);
+        }
         return null;
     }
 
-    @Override public T visit(UnaryExpression e) {
+    @Override
+    default T visit(UnaryExpression e) {
+        e.getExpression().accept(this);
         return null;
     }
 }

src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java

@@ -277,7 +277,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
                     ctx.defList.accept(this)
             );
         }
-
+        cases.setRuleContext(ctx);
         return cases;
     }
 

src/main/java/edu/kit/formal/proofscriptparser/ast/CasesStatement.java

@@ -37,7 +37,7 @@ import java.util.List;
  * @version 1 (28.04.17)
  */
 @Data
-public class CasesStatement extends Statement<ScriptLanguageParser.CasesListContext> {
+public class CasesStatement extends Statement<ScriptLanguageParser.CasesStmtContext> {
     @NonNull private final List<CaseStatement> cases = new ArrayList<>();
     @NonNull private Statements defaultCase = new Statements();
 

src/main/java/edu/kit/formal/proofscriptparser/ast/MatchExpression.java

@@ -36,7 +36,7 @@ import lombok.Data;
  */
 @Data
 public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatternContext> {
-    private Signature signature;
+    private Signature signature = new Signature();
     private Expression pattern;
 
     /**

src/main/java/edu/kit/formal/proofscriptparser/lint/LintProblem.java

+package edu.kit.formal.proofscriptparser.lint;
+
+import edu.kit.formal.proofscriptparser.ast.ASTNode;
+import edu.kit.formal.proofscriptparser.ast.GoalSelector;
+import edu.kit.formal.proofscriptparser.ast.Statement;
+import lombok.*;
+
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.List;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (23.05.17)
+ */
+@Data
+@NoArgsConstructor
+@AllArgsConstructor
+public class LintProblem {
+    @Getter
+    @Setter(AccessLevel.MODULE)
+    private String message;
+
+    @Getter
+    @Setter(AccessLevel.MODULE)
+    private char level;
+
+    @Getter
+    @Setter(AccessLevel.MODULE)
+    private int number;
+
+    @Getter
+    @Setter(AccessLevel.MODULE)
+    private String lintRule;
+
+    @Getter
+    private List<ASTNode> affectedNodes = new ArrayList<>();
+
+    public static LintProblem create(String ruleName) {
+        LintProblem lp = new LintProblem();
+        lp.setLintRule(ruleName);
+        return lp;
+    }
+
+    public LintProblem level(char w) {
+        setLevel(w);
+        return this;
+    }
+
+    public LintProblem message(String s) {
+        setMessage(s);
+        return this;
+    }
+
+    public LintProblem nodes(ASTNode... nodes) {
+        getAffectedNodes().addAll(Arrays.asList(nodes));
+        return this;
+    }
+}