closes expression in parser

lang/src/main/antlr4/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4

@@ -114,17 +114,13 @@ casesStmt
     ;
 
 casesList
-  //  : simpleCase
-   // | closableCase
-    :   CASE  (ISCLOSED | expression) COLON? INDENT stmtList DEDENT
+    :   CASE  (TRY | expression | closesExpression) COLON? INDENT stmtList DEDENT
     ;
-/*simpleCase
-    : CASE expression COLON? INDENT stmtList DEDENT
-    ;
-closableCase
-    : CASE MATCH ISCLOSED COLON? INDENT stmtList DEDENT
+
+closesExpression
+    : CLOSES closesScript= scriptCommand
     ;
-*/
+
 forEachStmt
     :   FOREACH INDENT stmtList DEDENT
     ;
@@ -133,6 +129,7 @@ theOnlyStmt
     :   THEONLY INDENT stmtList DEDENT
     ;
 
+
 scriptCommand
     :   cmd=ID parameters? SEMICOLON
     ;
@@ -155,7 +152,8 @@ MULTI_LINE_COMMENT  : '/*' (MULTI_LINE_COMMENT|.)*? '*/' -> channel(HIDDEN);
 
 CASES: 'cases';
 CASE: 'case';
-ISCLOSED: 'isCloseable';
+TRY: 'try';
+CLOSES: 'closes';
 DERIVABLE : 'derivable';
 DEFAULT: 'default';
 ASSIGN : ':=';

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTChanger.java

@@ -23,8 +23,9 @@ package edu.kit.iti.formal.psdbg.parser;
  */
 
 
-import edu.kit.iti.formal.psdbg.parser.types.Type;
 import edu.kit.iti.formal.psdbg.parser.ast.*;
+import edu.kit.iti.formal.psdbg.parser.types.Type;
+
 import java.util.ArrayList;
 import java.util.Map;
 import java.util.Set;
@@ -111,9 +112,9 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> {
     }
 
     @Override
-    public IsClosableCase visit(IsClosableCase isClosableCase) {
-        isClosableCase.getBody().accept(this);
-        return isClosableCase;
+    public tryCase visit(tryCase tryCase) {
+        tryCase.getBody().accept(this);
+        return tryCase;
     }
 
     @Override
@@ -123,6 +124,13 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> {
         return simpleCaseStatement;
     }
 
+    @Override
+    public ASTNode visit(ClosesCase closesCase) {
+        closesCase.getClosesScript().accept(this);
+        closesCase.getBody().accept(this);
+        return closesCase;
+    }
+
     @Override
     public CaseStatement visit(CaseStatement caseStatement) {
         //caseStatement.getGuard().accept(this);

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTTraversal.java

@@ -161,8 +161,8 @@ public interface ASTTraversal<T> extends Visitor<T> {
     }
 
     @Override
-    default T visit(IsClosableCase isClosableCase) {
-        isClosableCase.getBody().accept(this);
+    default T visit(tryCase tryCase) {
+        tryCase.getBody().accept(this);
         return null;
     }
 
@@ -181,4 +181,11 @@ public interface ASTTraversal<T> extends Visitor<T> {
         }
         return null;
     }
+
+    @Override
+    default T visit(ClosesCase closesCase) {
+        closesCase.getClosesScript().accept(this);
+        closesCase.getBody().accept(this);
+        return null;
+    }
 }

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/DefaultASTVisitor.java

@@ -133,8 +133,8 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
     }
 
     @Override
-    public T visit(IsClosableCase isClosableCase) {
-        return defaultVisit(isClosableCase);
+    public T visit(tryCase tryCase) {
+        return defaultVisit(tryCase);
     }
 
     @Override
@@ -142,5 +142,9 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
         return defaultVisit(simpleCaseStatement);
     }
 
+    @Override
+    public T visit(ClosesCase closesCase) {
+        return defaultVisit(closesCase);
+    }
 }
 

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java

@@ -23,6 +23,7 @@ package edu.kit.iti.formal.psdbg.parser;
  */
 
 
+import edu.kit.iti.formal.psdbg.parser.ast.*;
 import edu.kit.iti.formal.psdbg.parser.types.TypeFacade;
 import org.antlr.v4.runtime.ParserRuleContext;
 import org.antlr.v4.runtime.tree.ErrorNode;
@@ -34,7 +35,6 @@ import java.util.ArrayList;
 import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map;
-import edu.kit.iti.formal.psdbg.parser.ast.*;
 
 /**
  * @author Alexander Weigl
@@ -318,11 +318,20 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
     @Override
     public Object visitCasesList(ScriptLanguageParser.CasesListContext ctx) {
 
-        if (ctx.ISCLOSED() != null) {
-            IsClosableCase isClosableCase = new IsClosableCase();
-            isClosableCase.setRuleContext(ctx);
-            isClosableCase.setBody((Statements) ctx.stmtList().accept(this));
-            return isClosableCase;
+        if (ctx.TRY() != null) {
+            tryCase tryCase = new tryCase();
+            tryCase.setRuleContext(ctx);
+            tryCase.setBody((Statements) ctx.stmtList().accept(this));
+            return tryCase;
+        }
+        if (ctx.closesExpression() != null) {
+            ClosesCase closesCase = new ClosesCase();
+            closesCase.setClosedStmt(true);
+            closesCase.setRuleContext(ctx);
+            closesCase.setClosesScript((CallStatement) ctx.closesExpression().closesScript.accept(this));
+            closesCase.setBody((Statements) ctx.stmtList().accept(this));
+            return closesCase;
+
         } else {
             SimpleCaseStatement caseStatement = new SimpleCaseStatement();
             caseStatement.setRuleContext(ctx);
@@ -338,6 +347,11 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
 
     }
 
+    @Override
+    public Object visitClosesExpression(ScriptLanguageParser.ClosesExpressionContext ctx) {
+        return null;
+    }
+
 /*
     @Override
     public Object visitSimpleCase(ScriptLanguageParser.SimpleCaseContext ctx) {

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/Visitor.java

@@ -68,11 +68,13 @@ public interface Visitor<T> {
     T visit(UnaryExpression e);
 
 
-    T visit(IsClosableCase isClosableCase);
+    T visit(tryCase tryCase);
 
     T visit(SimpleCaseStatement simpleCaseStatement);
 
     T visit(CaseStatement caseStatement);
 
     T visit(SubstituteExpression subst);
+
+    T visit(ClosesCase colsesCase);
 }

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ClosesCase.java

+package edu.kit.iti.formal.psdbg.parser.ast;
+
+import edu.kit.iti.formal.psdbg.parser.Visitor;
+import lombok.Data;
+import lombok.NoArgsConstructor;
+
+/**
+ * Object representing  a "closes closeScriptCall(): { Commands}" block in a cases
+ */
+@Data
+@NoArgsConstructor
+public class ClosesCase extends CaseStatement {
+
+    private boolean isClosedStmt = true;
+
+    /**
+     * Script that should be executed and shown whether case can be closed
+     */
+    private CallStatement closesScript;
+
+    /**
+     * A close subscript() {bodyscript} expression
+     *
+     * @param closesScript the script that is exectued in order to determine whether goal would clos. This proof is pruned afterwards
+     * @param body         the actual script that is then executed when closesscript was successful and pruned
+     */
+    public ClosesCase(CallStatement closesScript, Statements body) {
+        this.body = body;
+        this.closesScript = closesScript;
+    }
+
+    /**
+     * {@inheritDoc}
+     */
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
+        return visitor.visit(this);
+    }
+
+    /**
+     * {@inheritDoc}
+     */
+    @Override
+    public tryCase copy() {
+        return new tryCase(body.copy());
+    }
+
+}

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/IsClosableCase.java → lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/tryCase.java

@@ -5,14 +5,14 @@ import lombok.Data;
 import lombok.NoArgsConstructor;
 
 /**
- * Object representing  a "match isClosable{ Commands}" block
+ * Object representing  a "try { Commands}" block in a cases
  */
 @Data
 @NoArgsConstructor
-public class IsClosableCase extends CaseStatement {
+public class tryCase extends CaseStatement {
     private boolean isClosedStmt = true;
 
-    public IsClosableCase(Statements body) {
+    public tryCase(Statements body) {
         this.body = body;
     }
 
@@ -28,7 +28,7 @@ public class IsClosableCase extends CaseStatement {
      * {@inheritDoc}
      */
     @Override
-    public IsClosableCase copy() {
-        return new IsClosableCase(body.copy());
+    public tryCase copy() {
+        return new tryCase(body.copy());
     }
 }

lang/src/test/resources/edu/kit/iti/formal/psdbg/parser/scripts/closesAndTrycases.txt

+script ruRg ()
+{   cases
+    {   case abc :
+        {   aM:TERM:=not ka&bi;
+            dsL f5=90;
+        }
+        case try :
+        {   last;
+        }
+
+        case closes body;{
+            last;
+            last;
+        }
+    }
+
+}
+
+script body()
+{
+    foo;
+}
\ No newline at end of file

pom.xml

@@ -57,7 +57,7 @@
         <module>rt</module>
         <module>rt-key</module>
         <module>ui</module>
-        <module>DockFX</module>
+        <module>lib/DockFX</module>
         <module>lint</module>
         <module>keydeps</module>
         <module>matcher</module>

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java

@@ -11,7 +11,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandLookup;
-import edu.kit.iti.formal.psdbg.parser.ast.IsClosableCase;
+import edu.kit.iti.formal.psdbg.parser.ast.tryCase;
 import edu.kit.iti.formal.psdbg.parser.types.SimpleType;
 import lombok.Getter;
 import org.key_project.util.collection.ImmutableList;
@@ -43,14 +43,14 @@ public class KeyInterpreter extends Interpreter<KeyData> {
 
 
     @Override
-    public Object visit(IsClosableCase isClosableCase) {
+    public Object visit(tryCase tryCase) {
         State<KeyData> currentStateToMatch = peekState();
         State<KeyData> currentStateToMatchCopy = peekState().copy(); //deepcopy
         GoalNode<KeyData> selectedGoalNode = currentStateToMatch.getSelectedGoalNode();
         GoalNode<KeyData> selectedGoalCopy = currentStateToMatch.getSelectedGoalNode().deepCopy(); //deepcopy
 
-        enterScope(isClosableCase);
-        executeBody(isClosableCase.getBody(), selectedGoalNode, new VariableAssignment(selectedGoalNode.getAssignments()));
+        enterScope(tryCase);
+        executeBody(tryCase.getBody(), selectedGoalNode, new VariableAssignment(selectedGoalNode.getAssignments()));
         State<KeyData> stateafterIsClosable = peekState();
         List<GoalNode<KeyData>> goals = stateafterIsClosable.getGoals();
         boolean allClosed = true;
@@ -70,7 +70,7 @@ public class KeyInterpreter extends Interpreter<KeyData> {
             pushState(currentStateToMatchCopy);
         }
         //check if state is closed
-        exitScope(isClosableCase);
+        exitScope(tryCase);
         return false;
     }
 }

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java

@@ -165,10 +165,10 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
     }
 
     @Override
-    public Object visit(IsClosableCase isClosableCase) {
-        enterScope(isClosableCase);
+    public Object visit(tryCase tryCase) {
+        enterScope(tryCase);
 
-        exitScope(isClosableCase);
+        exitScope(tryCase);
         return false;
     }