Merge branch 'master' of git.scc.kit.edu:xt9634/ProofScriptParser

* 'master' of git.scc.kit.edu:xt9634/ProofScriptParser:
  Small working debugger, with some little quirks.

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 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);
+    //needs to threadable
+    public Set<Integer> brkpnts = new TreeSet<>();
+    public final Lock lock = new ReentrantLock();
+    public final Condition block = lock.newCondition();
+
+    @Override
+    public Void defaultVisit(ASTNode node) {
+        if (stepUntilBlock.get() > 0)
+            stepUntilBlock.decrementAndGet();
+
+        if (stepUntilBlock.get() == 0)
+            block();
+
+        int lineNumber = node.getStartPosition().getLineNumber();
+        if (brkpnts.contains(lineNumber)) {
+            block();
+        }
+
+        return super.defaultVisit(node);
+    }
+
+    private void block() {
+        try {
+            lock.lock();
+            block.await();
+        } catch (InterruptedException e) {
+            e.printStackTrace();
+        } finally {
+            lock.unlock();
+        }
+    }
+
+    public void addBreakpoint(int i) {
+        brkpnts.add(i);
+    }
+
+    public void unlock() {
+        try {
+            lock.lock();
+            block.signal();
+        } finally {
+            lock.unlock();
+        }
+    }
+}

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

+package edu.kit.formal.dbg;
+
+import edu.kit.formal.interpreter.*;
+import edu.kit.formal.interpreter.funchdl.BuiltinCommands;
+import edu.kit.formal.interpreter.funchdl.DefaultLookup;
+import edu.kit.formal.proofscriptparser.*;
+import edu.kit.formal.proofscriptparser.ast.*;
+import org.antlr.v4.runtime.CharStreams;
+
+import java.io.*;
+import java.math.BigInteger;
+import java.util.List;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (21.05.2017)
+ */
+public class Debugger {
+    Interpreter interpreter;
+    private List<ProofScript> scripts;
+    private Blocker blocker = new Blocker();
+    private DefaultLookup debuggerFunctions = new DefaultLookup();
+    private HistoryListener history;
+
+    private Thread interpreterThread;
+
+    public Debugger(String file) throws IOException {
+        DefaultLookup lookup = new DefaultLookup();
+        lookup.getBuilders().add(new BuiltinCommands.SplitCommand());
+        interpreter = new Interpreter(lookup);
+
+        history = new HistoryListener(interpreter);
+        scripts = Facade.getAST(new File(file));
+        interpreter.getEntryListeners().add(history);
+        interpreter.getEntryListeners().add(blocker);
+        interpreter.getEntryListeners().add(new CommandLogger());
+        //TODO install debugger functions
+
+        debuggerFunctions.getBuilders().add(new Step());
+        debuggerFunctions.getBuilders().add(new Printer());
+        debuggerFunctions.getBuilders().add(new ChgSel());
+        debuggerFunctions.getBuilders().add(new Start());
+        debuggerFunctions.getBuilders().add(new Pause());
+        debuggerFunctions.getBuilders().add(new BrkPnt());
+        debuggerFunctions.getBuilders().add(new Status());
+
+    }
+
+    public static void main(String[] args) throws IOException {
+        Debugger d = new Debugger("src/test/resources/edu/kit/formal/interpreter/dbg.kps");
+        d.run();
+    }
+
+    private void run() throws IOException {
+        blocker.stepUntilBlock.set(2);
+        interpreterThread = new Thread(() -> {
+            interpreter.interpret(scripts, "start");
+        });
+        interpreterThread.setName("interpreter");
+
+        BufferedReader br = new BufferedReader(new InputStreamReader(System.in));
+
+        int counter = 0;
+        while (true) {
+            System.out.printf("dbg (%03d)> ", ++counter);
+            String input = br.readLine();
+            execuate(input);
+        }
+    }
+
+    private void execuate(String input) {
+        input = input.trim();
+        if (input.isEmpty()) {
+            return;
+        }
+
+        if (!input.endsWith(";"))
+            input += ';';
+
+        ScriptLanguageParser parser = Facade.getParser(CharStreams.fromString(input));
+        ScriptLanguageParser.ScriptCommandContext ctx = parser.scriptCommand();
+        CallStatement call = (CallStatement) ctx.accept(new TransformAst());
+        try {
+            debuggerFunctions.callCommand(interpreter, call, new VariableAssignment());
+        } catch (IllegalStateException e) {
+            System.out.println("No function for " + input + " defined! ");
+            e.printStackTrace();
+
+        }
+    }
+
+
+    private class Step implements edu.kit.formal.interpreter.funchdl.CommandHandler {
+        @Override
+        public boolean handles(CallStatement call) throws IllegalArgumentException {
+            return call.getCommand().equals("step");
+        }
+
+        @Override
+        public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) {
+            IntegerLiteral il = (IntegerLiteral) call.getParameters().get(new Variable("#1"));
+            int steps = 1;
+            if (il != null)
+                steps = il.getValue().intValue();
+            blocker.stepUntilBlock.set(steps * 2); //FIXME times two is strange, something wrong on sync
+            //LockSupport.unpark(interpreterThread);
+            blocker.unlock();
+        }
+    }
+
+    private class Printer implements edu.kit.formal.interpreter.funchdl.CommandHandler {
+        @Override
+        public boolean handles(CallStatement call) throws IllegalArgumentException {
+            return call.getCommand().equals("psel");
+        }
+
+        @Override
+        public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) {
+            AbstractState state = interpreter.getCurrentState();
+            int i = 0;
+            GoalNode sel;
+            try {
+                sel = state.getSelectedGoalNode();
+            } catch (IllegalStateException e) {
+                sel = null;
+            }
+
+            for (GoalNode g : state.getGoals()) {
+                System.out.printf("%2d %s %s\n     %s\n",
+                        i++,
+                        g == sel ? "*" : " ",
+                        g.getSequent(),
+                        g.getAssignments().asMap());
+            }
+        }
+    }
+
+
+    private class Start implements edu.kit.formal.interpreter.funchdl.CommandHandler {
+        @Override
+        public boolean handles(CallStatement call) throws IllegalArgumentException {
+            return call.getCommand().equals("start");
+        }
+
+        @Override
+        public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) {
+            interpreterThread.start();
+        }
+    }
+
+
+    private class Pause implements edu.kit.formal.interpreter.funchdl.CommandHandler {
+        @Override
+        public boolean handles(CallStatement call) throws IllegalArgumentException {
+            return call.getCommand().equals("pause");
+        }
+
+        @Override
+        public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) {
+            blocker.stepUntilBlock.set(1); // block at next statement
+        }
+    }
+
+    private class BrkPnt implements edu.kit.formal.interpreter.funchdl.CommandHandler {
+        @Override
+        public boolean handles(CallStatement call) throws IllegalArgumentException {
+            return call.getCommand().equals("b");
+        }
+
+        @Override
+        public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) {
+            IntegerLiteral il = (IntegerLiteral) call.getParameters().get(new Variable("#1"));
+            blocker.addBreakpoint(il.getValue().intValue());
+
+            System.out.println("brkpnts: " + blocker.brkpnts);
+
+        }
+    }
+
+
+    private class Status implements edu.kit.formal.interpreter.funchdl.CommandHandler {
+        @Override
+        public boolean handles(CallStatement call) throws IllegalArgumentException {
+            return call.getCommand().equals("status");
+        }
+
+        @Override
+        public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) {
+            System.out.format("name: %s, p: %s, state: %s, alive:%s, daemon:%s, interrupted:%s %n",
+                    interpreterThread.getName(),
+                    interpreterThread.getPriority(),
+                    interpreterThread.getState(),
+                    interpreterThread.isAlive(),
+                    interpreterThread.isDaemon(),
+                    interpreterThread.isInterrupted());
+
+            List<ASTNode> nodes = history.getQueueNode();
+            List<AbstractState> states = history.getQueueState();
+            CommandLogger cmd = new CommandLogger();
+            for (int i = 0; i < nodes.size(); i++) {
+                ASTNode node = nodes.get(i);
+                node.accept(cmd);
+                // System.out.format("\t\t\t>>> %d states: [%s]%n", states.get(i).getGoals().size(),
+                //         states.get(i).getSelectedGoalNode().getAssignments().asMap());
+            }
+        }
+    }
+
+    private class ChgSel implements edu.kit.formal.interpreter.funchdl.CommandHandler {
+        @Override
+        public boolean handles(CallStatement call) throws IllegalArgumentException {
+            return call.getCommand().equals("chgsel");
+        }
+
+        @Override
+        public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) {
+            AbstractState state = interpreter.getCurrentState();
+            params = interpreter.evaluateParameters(call.getParameters());
+            Value<BigInteger> v = params.getValues().get("#1");
+
+            interpreter.newState(state.getGoals(),
+                    state.getGoals().get(v.getData().intValue()));
+
+        }
+    }
+
+    private class CommandLogger extends DefaultASTVisitor<Void> {
+        public void suffix(ASTNode node) {
+            System.out.format("%02d: ", node.getStartPosition().getLineNumber());
+        }
+
+        @Override
+        public Void visit(ProofScript proofScript) {
+            suffix(proofScript);
+            System.out.printf("script %s (%s) {%n",
+                    proofScript.getName(),
+                    Facade.prettyPrint(proofScript.getSignature())
+            );
+            return null;
+        }
+
+        @Override
+        public Void visit(AssignmentStatement assignment) {
+            suffix(assignment);
+            System.out.println(Facade.prettyPrint(assignment));
+            return super.visit(assignment);
+        }
+
+        @Override
+        public Void visit(CasesStatement casesStatement) {
+            suffix(casesStatement);
+            System.out.println("cases {");
+            return super.visit(casesStatement);
+        }
+
+        @Override
+        public Void visit(CaseStatement caseStatement) {
+            suffix(caseStatement);
+            System.out.println("case " + Facade.prettyPrint(caseStatement.getGuard()));
+            return super.visit(caseStatement);
+        }
+
+        @Override
+        public Void visit(CallStatement call) {
+            suffix(call);
+            System.out.println(Facade.prettyPrint(call));
+            return super.visit(call);
+        }
+
+        @Override
+        public Void visit(TheOnlyStatement theOnly) {
+            suffix(theOnly);
+            System.out.println("theonly {");
+            return super.visit(theOnly);
+        }
+
+        @Override
+        public Void visit(ForeachStatement foreach) {
+            suffix(foreach);
+            System.out.println("foreach {");
+            return super.visit(foreach);
+        }
+
+        @Override
+        public Void visit(RepeatStatement repeatStatement) {
+            suffix(repeatStatement);
+            System.out.println("repeat {");
+            return super.visit(repeatStatement);
+        }
+    }
+}

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

@@ -7,6 +7,7 @@ import lombok.Getter;
 import lombok.Setter;
 
 import java.util.ArrayList;
+import java.util.Collections;
 import java.util.List;
 
 /**
@@ -16,7 +17,6 @@ import java.util.List;
  * @author A. Weigl
  */
 public class Evaluator extends DefaultASTVisitor<Value> implements ScopeObservable {
-    private GoalNode currentState;
     private List<VariableAssignment> matchedVariables = new ArrayList<>();
     @Getter
     @Setter
@@ -27,13 +27,12 @@ public class Evaluator extends DefaultASTVisitor<Value> implements ScopeObservab
     private List<Visitor> entryListeners = new ArrayList<>(),
             exitListeners = new ArrayList<>();
 
-    public Evaluator(GoalNode s) {
-        this.currentState = s;
-    }
+    private final GoalNode goal;
+    private final VariableAssignment state;
 
-    public Evaluator(GoalNode g, MatcherApi matcherApi) {
-        this(g);
-        setMatcher(matcherApi);
+    public Evaluator(VariableAssignment assignment, GoalNode node) {
+        state = new VariableAssignment(assignment); // unmodifiable version of assignment
+        goal = node;
     }
 
     /**
@@ -66,9 +65,9 @@ public class Evaluator extends DefaultASTVisitor<Value> implements ScopeObservab
 
         List<VariableAssignment> va = null;
         if (pattern.getType() == Type.STRING) {
-            va = matcher.matchLabel(currentState, (String) pattern.getData());
+            va = matcher.matchLabel(goal, (String) pattern.getData());
         } else if (pattern.getType() == Type.TERM) {
-            va = matcher.matchSeq(currentState, (String) pattern.getData());
+            va = matcher.matchSeq(goal, (String) pattern.getData());
         }
 
         return va != null && va.size() > 0 ? Value.TRUE : Value.FALSE;
@@ -94,7 +93,7 @@ public class Evaluator extends DefaultASTVisitor<Value> implements ScopeObservab
     public Value visit(Variable variable) {
         //get variable value
         String id = variable.getIdentifier();
-        Value v = currentState.lookupVarValue(id);
+        Value v = state.lookupVarValue(id);
         if (v != null) {
             return v;
         } else {

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

@@ -16,6 +16,7 @@ import java.util.List;
 public class HistoryListener extends DefaultASTVisitor<Void> {
     @Getter
     private final List<ASTNode> queueNode = new LinkedList<>();
+    @Getter
     private final List<AbstractState> queueState = new LinkedList<>();
 
     private final Interpreter interpreter;

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

@@ -113,7 +113,8 @@ public class Interpreter extends DefaultASTVisitor<Void>
 
     private Value evaluate(GoalNode g, Expression expr) {
         enterScope(expr);
-        Evaluator evaluator = new Evaluator(g, matcherApi);
+        Evaluator evaluator = new Evaluator(g.getAssignments(),g);
+        evaluator.setMatcher(matcherApi);
         evaluator.getEntryListeners().addAll(entryListeners);
         evaluator.getExitListeners().addAll(exitListeners);
         exitScope(expr);
@@ -272,7 +273,7 @@ public class Interpreter extends DefaultASTVisitor<Void>
     }
 
 
-    private VariableAssignment evaluateParameters(Parameters parameters) {
+    public VariableAssignment evaluateParameters(Parameters parameters) {
         VariableAssignment va = new VariableAssignment();
         parameters.entrySet().forEach(entry -> {
             Value val = evaluate(entry.getValue());
@@ -370,18 +371,18 @@ public class Interpreter extends DefaultASTVisitor<Void>
         return stateStack.peek();
     }
 
-    private AbstractState newState(List<GoalNode> goals, GoalNode selected) {
+    public AbstractState newState(List<GoalNode> goals, GoalNode selected) {
         if (selected != null && !goals.contains(selected)) {
             throw new IllegalStateException("selected goal not in list of goals");
         }
         return pushState(new State(goals, selected));
     }
 
-    private AbstractState newState(List<GoalNode> goals) {
+    public AbstractState newState(List<GoalNode> goals) {
         return newState(goals, null);
     }
 
-    private AbstractState newState(GoalNode selected) {
+    public AbstractState newState(GoalNode selected) {
         return newState(Collections.singletonList(selected), selected);
     }
 
@@ -393,7 +394,7 @@ public class Interpreter extends DefaultASTVisitor<Void>
         return state;
     }
 
-    private void popState(AbstractState expected) {
+    public void popState(AbstractState expected) {
         AbstractState actual = stateStack.pop();
         if (!expected.equals(actual)) {
             throw new IllegalStateException("Error on the stack!");

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

@@ -23,7 +23,6 @@ package edu.kit.formal.proofscriptparser;
  */
 
 
-
 import edu.kit.formal.proofscriptparser.ast.*;
 import lombok.Getter;
 import lombok.Setter;
@@ -83,9 +82,9 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
 
     @Override
     public Void visit(AssignmentStatement assign) {
-        assign.getRhs().accept(this);
-        s.append(" := ");
         assign.getLhs().accept(this);
+        s.append(" := ");
+        assign.getRhs().accept(this);
         s.append(";");
         return null;
     }
@@ -299,8 +298,11 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
         int posnewline = s.length() - 1;
         while (s.charAt(posnewline) != '\n') {
             posnewline--;
+            if (posnewline < 0) {
+                break;
+            }
         }
-        return posnewline;
+        return Math.max(posnewline, 0);
     }
 
     private String getWhitespacePrefix() {

src/test/java/edu/kit/formal/interpreter/EvaluatorTest.java

@@ -43,7 +43,7 @@ public class EvaluatorTest {
         va.setVarValue("a", Value.from(1));
         va.setVarValue("b", Value.from(1));
         GoalNode selected = new GoalNode(parent, "selg");
-        eval = new Evaluator(selected);
+        eval = new Evaluator(selected.getAssignments(), selected);
         eval.setMatcher(new PseudoMatcher());
     }
 
@@ -58,7 +58,7 @@ public class EvaluatorTest {
     static class PseudoMatcher implements MatcherApi {
         @Override
         public List<VariableAssignment> matchLabel(GoalNode currentState, String label) {
-            Pattern p = Pattern.compile(label,Pattern.CASE_INSENSITIVE);
+            Pattern p = Pattern.compile(label, Pattern.CASE_INSENSITIVE);
             Matcher m = p.matcher(currentState.getSequent());
             return m.matches()
                     ? Collections.singletonList(new VariableAssignment())

src/test/resources/edu/kit/formal/interpreter/dbg.kps

+script Simple1(i:int, j:int) {
+    i := 1;
+    j := 2;
+
+    theonly {
+        i := 4;
+        j := i+i;
+    }
+
+    split 5;
+
+    foreach {
+        i := 4;
+        j := i+i;
+    }
+
+    repeat {
+        foreach { i := i + 1; split;}
+    }
+}
\ No newline at end of file