Parser-Erweiterung closable and derivable

src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4

@@ -76,8 +76,11 @@ literals :
 
      </pre>*/
 matchPattern
-    :   MATCH (pattern=expression
-        (USING LBRACKET argList RBRACKET)?) | DERIVABLE TERM_LITERAL | IFCLOSED
+    :
+       MATCH (
+         derivable=DERIVABLE derivableExpression=expression
+       | (pattern=expression (USING LBRACKET argList RBRACKET)?)
+       )
     ;
 
 scriptVar
@@ -98,9 +101,17 @@ casesStmt
     ;
 
 casesList
-    :   CASE expression COLON? INDENT stmtList DEDENT
+  //  : simpleCase
+   // | closableCase
+    :   CASE (MATCH ISCLOSED | expression) COLON? INDENT stmtList DEDENT
     ;
-
+/*simpleCase
+    : CASE expression COLON? INDENT stmtList DEDENT
+    ;
+closableCase
+    : CASE MATCH ISCLOSED COLON? INDENT stmtList DEDENT
+    ;
+*/
 forEachStmt
     :   FOREACH INDENT stmtList DEDENT
     ;
@@ -131,6 +142,8 @@ MULTI_LINE_COMMENT  : '/*' (MULTI_LINE_COMMENT|.)*? '*/' -> channel(HIDDEN);
 
 CASES: 'cases';
 CASE: 'case';
+ISCLOSED: 'isCloseable';
+DERIVABLE : 'derivable';
 DEFAULT: 'default';
 ASSIGN : ':=';
 LBRACKET: '[';
@@ -147,8 +160,6 @@ BOOL: 'bool' ;
 TERMTYPE : 'term' ;*/
 FOREACH : 'foreach' ;
 THEONLY : 'theonly' ;
-ISCLOSED: 'isClosable';
-DERIVABLE : 'derivable';
 INDENT : '{' ;
 DEDENT : '}' ;
 SEMICOLON : ';' ;

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

@@ -21,7 +21,7 @@ public class WelcomePane extends AnchorPane {
         proofScriptDebugger.getWelcomePaneDock().close();
         proofScriptDebugger.showActiveInspector(null);
         proofScriptDebugger.openScript(
-                new File("src/test/resources/edu/kit/formal/interpreter/contraposition/wo_branching.kps")
+                new File("src/test/resources/edu/kit/formal/interpreter/contraposition/w_branching.kps")
         );
 
         proofScriptDebugger.openKeyFile(

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

@@ -54,7 +54,7 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
     }
 
     /**
-     * TODO Connect with KeY
+     * Visit a match expression and evaluate expression using matcher
      *
      * @param match
      * @return
@@ -64,16 +64,18 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
         if (match.getSignature() != null && !match.getSignature().isEmpty()) {
             throw new IllegalStateException("not supported");
         }
-
-        Value pattern = (Value) match.getPattern().accept(this);
-
         List<VariableAssignment> va = null;
-        if (pattern.getType() == Type.STRING) {
-            va = matcher.matchLabel(goal, (String) pattern.getData());
-        } else if (pattern.getType() == Type.TERM) {
-            va = matcher.matchSeq(goal, (String) pattern.getData(), match.getSignature());
+        Value pattern = (Value) match.getPattern().accept(this);
+        if (match.isDerivable()) {
+        } else {
+            if (pattern.getType() == Type.STRING) {
+                va = matcher.matchLabel(goal, (String) pattern.getData());
+            } else if (pattern.getType() == Type.TERM) {
+                va = matcher.matchSeq(goal, (String) pattern.getData(), match.getSignature());
+            }
         }
 
+
         return va != null && va.size() > 0 ? Value.TRUE : Value.FALSE;
     }
 

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

@@ -168,15 +168,19 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
         List<GoalNode<T>> goalsAfterCases = new ArrayList<>();
         //copy the list of goal nodes for keeping track of goals
         Set<GoalNode<T>> remainingGoalsSet = new HashSet<>(allGoalsBeforeCases);
-
+        //TODO
         //handle cases
         List<CaseStatement> cases = casesStatement.getCases();
         for (CaseStatement aCase : cases) {
-            Map<GoalNode<T>, VariableAssignment> matchedGoals =
-                    matchGoal(remainingGoalsSet, aCase);
-            if (matchedGoals != null) {
-                remainingGoalsSet.removeAll(matchedGoals.keySet());
-                goalsAfterCases.addAll(executeCase(aCase.getBody(), matchedGoals));
+            if (aCase.isClosedStmt) {
+                System.out.println("IsClosableStmt not implemented yet");
+            } else {
+                Map<GoalNode<T>, VariableAssignment> matchedGoals =
+                        matchGoal(remainingGoalsSet, (SimpleCaseStatement) aCase);
+                if (matchedGoals != null) {
+                    remainingGoalsSet.removeAll(matchedGoals.keySet());
+                    goalsAfterCases.addAll(executeCase(aCase.getBody(), matchedGoals));
+                }
             }
 
         }
@@ -219,11 +223,12 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
      * @param aCase
      * @return
      */
-    private Map<GoalNode<T>, VariableAssignment> matchGoal(Set<GoalNode<T>> allGoalsBeforeCases, CaseStatement aCase) {
+    private Map<GoalNode<T>, VariableAssignment> matchGoal(Set<GoalNode<T>> allGoalsBeforeCases, SimpleCaseStatement aCase) {
 
         HashMap<GoalNode<T>, VariableAssignment> matchedGoals = new HashMap<>();
         Expression matchExpression = aCase.getGuard();
 
+
         for (GoalNode<T> goal : allGoalsBeforeCases) {
             VariableAssignment va = evaluateMatchInGoal(matchExpression, goal);
             if (va != null) {

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

@@ -13,4 +13,5 @@ import java.util.List;
 public interface MatcherApi<T> {
     List<VariableAssignment> matchLabel(GoalNode<T> currentState, String label);
     List<VariableAssignment> matchSeq(GoalNode<T> currentState, String data, Signature sig);
+
 }

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

@@ -221,7 +221,7 @@ public class Debugger {
         }
 
         @Override
-        public Void visit(CaseStatement caseStatement) {
+        public Void visit(SimpleCaseStatement caseStatement) {
             suffix(caseStatement);
             System.out.println("case " + Facade.prettyPrint(caseStatement.getGuard()));
             return super.visit(caseStatement);

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

@@ -110,11 +110,26 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> {
         return casesStatement;
     }
 
+    @Override
+    public IsClosableCase visit(IsClosableCase isClosableCase) {
+        isClosableCase.getBody().accept(this);
+        return isClosableCase;
+    }
+
+    @Override
+    public SimpleCaseStatement visit(SimpleCaseStatement simpleCaseStatement) {
+        simpleCaseStatement.getGuard().accept(this);
+        simpleCaseStatement.getBody().accept(this);
+        return simpleCaseStatement;
+    }
+
     @Override
     public CaseStatement visit(CaseStatement caseStatement) {
-        caseStatement.getGuard().accept(this);
-        caseStatement.getBody().accept(this);
+        //caseStatement.getGuard().accept(this);
+        //caseStatement.getBody().accept(this);
+        caseStatement.accept(this);
         return caseStatement;
+
     }
 
     @Override

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

@@ -104,8 +104,8 @@ public interface ASTTraversal<T> extends Visitor<T> {
 
     @Override
     default T visit(CaseStatement caseStatement) {
-        caseStatement.getGuard().accept(this);
-        caseStatement.getBody().accept(this);
+        //caseStatement.getBody().accept(this);
+        caseStatement.accept(this);
         return null;
     }
 
@@ -158,4 +158,17 @@ public interface ASTTraversal<T> extends Visitor<T> {
         e.getExpression().accept(this);
         return null;
     }
+
+    @Override
+    default T visit(IsClosableCase isClosableCase) {
+        isClosableCase.getBody().accept(this);
+        return null;
+    }
+
+    @Override
+    default T visit(SimpleCaseStatement simpleCaseStatement) {
+        simpleCaseStatement.getGuard().accept(this);
+        simpleCaseStatement.getBody().accept(this);
+        return null;
+    }
 }

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

@@ -128,5 +128,15 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
     public T visit(UnaryExpression unaryExpression) {
         return defaultVisit(unaryExpression);
     }
+
+    @Override
+    public T visit(IsClosableCase isClosableCase) {
+        return defaultVisit(isClosableCase);
+    }
+
+    @Override
+    public T visit(SimpleCaseStatement simpleCaseStatement) {
+        return defaultVisit(simpleCaseStatement);
+    }
 }
 

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

@@ -38,15 +38,13 @@ import java.util.Map;
  */
 public class PrettyPrinter extends DefaultASTVisitor<Void> {
 
+    private final StringBuilder s = new StringBuilder();
     @Getter
     @Setter
     private int maxWidth = 80;
-
     @Getter
     @Setter
     private boolean unicode = true;
-
-    private final StringBuilder s = new StringBuilder();
     private int indentation = 0;
 
     @Override
@@ -168,7 +166,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
     }
 
     @Override
-    public Void visit(CaseStatement caseStatement) {
+    public Void visit(SimpleCaseStatement caseStatement) {
         s.append("case ");
         caseStatement.getGuard().accept(this);
         s.append(" {");

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

@@ -249,9 +249,16 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     public Object visitMatchPattern(ScriptLanguageParser.MatchPatternContext ctx) {
         MatchExpression match = new MatchExpression();
         match.setRuleContext(ctx);
-        if (ctx.argList() != null)
-            match.setSignature((Signature) ctx.argList().accept(this));
-        match.setPattern((Expression) ctx.pattern.accept(this));
+
+        if (ctx.derivable != null) {
+            match.setDerivable(true);
+            match.setDerivableTerm((Expression) ctx.derivableExpression.accept(this));
+        } else {
+            if (ctx.argList() != null)
+                match.setSignature((Signature) ctx.argList().accept(this));
+            match.setPattern((Expression) ctx.pattern.accept(this));
+        }
+
         return match;
     }
 
@@ -283,12 +290,46 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
 
     @Override
     public Object visitCasesList(ScriptLanguageParser.CasesListContext ctx) {
-        CaseStatement caseStatement = new CaseStatement();
+
+        if (ctx.ISCLOSED() != null) {
+            IsClosableCase isClosableCase = new IsClosableCase();
+            isClosableCase.setRuleContext(ctx);
+            isClosableCase.setBody((Statements) ctx.stmtList().accept(this));
+            return isClosableCase;
+        } else {
+            SimpleCaseStatement caseStatement = new SimpleCaseStatement();
+            caseStatement.setRuleContext(ctx);
+            caseStatement.setGuard((Expression) ctx.expression().accept(this));
+            caseStatement.setBody((Statements) ctx.stmtList().accept(this));
+            return caseStatement;
+        }
+     /*   CaseStatement caseStatement = new CaseStatement();
+        caseStatement.setRuleContext(ctx);
+        caseStatement.setGuard((Expression) ctx.expression().accept(this));
+        caseStatement.setBody((Statements) ctx.stmtList().accept(this));
+        return caseStatement;*/
+
+    }
+
+/*
+    @Override
+    public Object visitSimpleCase(ScriptLanguageParser.SimpleCaseContext ctx) {
+        SimpleCaseStatement caseStatement = new SimpleCaseStatement();
         caseStatement.setRuleContext(ctx);
         caseStatement.setGuard((Expression) ctx.expression().accept(this));
         caseStatement.setBody((Statements) ctx.stmtList().accept(this));
         return caseStatement;
+
+    }
+
+    @Override
+    public Object visitClosableCase(ScriptLanguageParser.ClosableCaseContext ctx) {
+        IsClosableCase isClosableCase = new IsClosableCase();
+        isClosableCase.setRuleContext(ctx);
+        isClosableCase.setBody((Statements) ctx.stmtList().accept(this));
+        return isClosableCase;
     }
+*/
 
     @Override
     public Object visitForEachStmt(ScriptLanguageParser.ForEachStmtContext ctx) {

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

@@ -53,7 +53,7 @@ public interface Visitor<T> {
 
     T visit(CasesStatement cases);
 
-    T visit(CaseStatement case_);
+    //T visit(CaseStatement case_);
 
     T visit(CallStatement call);
 
@@ -70,4 +70,9 @@ public interface Visitor<T> {
     T visit(UnaryExpression e);
 
 
+    T visit(IsClosableCase isClosableCase);
+
+    T visit(SimpleCaseStatement simpleCaseStatement);
+
+    T visit(CaseStatement caseStatement);
 }

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

@@ -38,8 +38,8 @@ import lombok.NoArgsConstructor;
 @NoArgsConstructor
 @AllArgsConstructor
 public class CaseStatement extends Statement<ScriptLanguageParser.CasesListContext> {
-    private Expression guard;
-    private Statements body;
+    public boolean isClosedStmt;
+    protected Statements body;
 
     /**
      * {@inheritDoc}
@@ -52,6 +52,6 @@ public class CaseStatement extends Statement<ScriptLanguageParser.CasesListConte
      * {@inheritDoc}
      */
     @Override public CaseStatement copy() {
-        return new CaseStatement(guard.copy(), body.copy());
+        return new CaseStatement(body.copy(), isClosedStmt);
     }
 }

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

+package edu.kit.formal.proofscriptparser.ast;
+
+import edu.kit.formal.proofscriptparser.Visitor;
+import lombok.Data;
+import lombok.NoArgsConstructor;
+
+/**
+ * Object representing  a "match isClosable{ Commands}" block
+ */
+@Data
+@NoArgsConstructor
+public class IsClosableCase extends CaseStatement {
+    private boolean isClosedStmt = true;
+
+    public IsClosableCase(Statements body) {
+        this.body = body;
+    }
+
+    /**
+     * {@inheritDoc}
+     */
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
+        return visitor.visit(this);
+    }
+
+    /**
+     * {@inheritDoc}
+     */
+    @Override
+    public IsClosableCase copy() {
+        return new IsClosableCase(body.copy());
+    }
+}

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

@@ -27,6 +27,8 @@ import edu.kit.formal.proofscriptparser.NotWelldefinedException;
 import edu.kit.formal.proofscriptparser.ScriptLanguageParser;
 import edu.kit.formal.proofscriptparser.Visitor;
 import lombok.Data;
+import lombok.Getter;
+import lombok.Setter;
 
 /**
  * A match expression contains an argument and a uses clause.
@@ -38,6 +40,12 @@ import lombok.Data;
 public class MatchExpression extends Expression<ScriptLanguageParser.MatchPatternContext> {
     private Signature signature = new Signature();
     private Expression pattern;
+    @Getter
+    @Setter
+    private boolean isDerivable;
+    @Getter
+    @Setter
+    private Expression derivableTerm;
 
     /**
      * {@inheritDoc}

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

+package edu.kit.formal.proofscriptparser.ast;
+
+import edu.kit.formal.proofscriptparser.Visitor;
+import lombok.AllArgsConstructor;
+import lombok.Data;
+import lombok.NoArgsConstructor;
+
+/**
+ * Created by sarah on 7/17/17.
+ */
+@Data
+@NoArgsConstructor
+@AllArgsConstructor
+public class SimpleCaseStatement extends CaseStatement {
+    private Expression guard;
+    private boolean isClosedStmt = false;
+
+    public SimpleCaseStatement(Expression guard, Statements body) {
+        this.guard = guard;
+        this.body = body;
+    }
+
+    /**
+     * {@inheritDoc}
+     */
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
+        return visitor.visit(this);
+    }
+
+    /**
+     * {@inheritDoc}
+     */
+    @Override
+    public SimpleCaseStatement copy() {
+        return new SimpleCaseStatement(guard.copy(), body.copy());
+    }
+
+
+}

src/test/resources/edu/kit/formal/interpreter/contraposition/isClosable.kps

+
+script test(){
+    impRight;
+    impRight;
+    cases{
+        case match isCloseable:{
+            notLeft;
+            notRight;
+            replace_known_left occ='2';
+            concrete_impl_1;
+            close;
+        }
+
+        default:{
+            auto;
+        }
+    }
+}
\ No newline at end of file