debug some previously defined syntax

Author: laurayuwen

src/common/exp-syntax.k

@@ -52,7 +52,7 @@ syntax Exp ::=
  		| Exp "-" Exp [seqstrict, klabel('Minus)]
 
 //todo: change to LHS?
-syntax AssignExp ::= K "=" Exp [seqstrict, klabel('Assign)]
+syntax AssignExp ::= K "=" Exp [klabel('Assign)]
 syntax AssignExp ::= CompoundAssignExp
 syntax CompoundAssignExp ::= "dummyCompoundAssignExp"
                             | Exp "*=" Exp [klabel('AssignMul)]

src/common/stmt-syntax.k

@@ -4,7 +4,7 @@ require "core-classes.k"
 module STMT-SYNTAX
     imports CORE-SORTS
     imports CORE-CLASSES
-//todo:be specific
+
 syntax Stmt ::= StmtWithoutTrailing|LabeledStmt|IfThenElseStmt|IfThenStmt|WhileStmt|ForStmt
 
 syntax IfThenElseStmt ::= "if" "(" Exp ")" "{" K "}" "else" "{" K "}" [strict(1),klabel('If)]
@@ -25,8 +25,7 @@ syntax StmtWithoutTrailing ::= Block
 |SynchronizedStmt
 
 syntax BlockStmt ::= Stmt|LocalVarDecStmt|ClassDecStmt
-syntax LocalVarDecStmt ::= LocalVarDec ";" [klabel('LocalVarDecStm)]
-syntax LocalVarDec ::= KListWrap Type Id [strict(2,3), klabel('LocalVarDec)]
+syntax LocalVarDecStmt ::= Type Id ";" [klabel('LocalVarDec)]
 
 //todo:ClassDecStm
 syntax ClassDecStmt ::= "dummyclassdecstm"
@@ -44,11 +43,9 @@ syntax SwitchBlock::= "{" KListWrap KListWrap "}" [klabel('SwitchBlock)]
 syntax DoStmt ::="do" "{" K "}" "while" "(" K ")"[strict(2),klabel('DoWhile)]
 syntax TryStmt ::= "try" Block KListWrap "finally" Block [klabel('Try)]
 		           |"try" Block KListWrap [klabel('Try)]
+		           |"catch" "(" K ")" Block [klabel('Catch)]
 		           //todo:catches
-
-syntax CatchClause ::= "catch" "(" K ")" Block [strict(1),klabel('Catch),result(ExtKResult)]
-
-//syntax Catches ::= List{CatchClause,""}
+	//syntax Catches ::= List{CatchClause,""}
 //syntax KItem ::= toCatches( KListWrap )          [function]
 //           | toCatches( KListWrap , Catches ) [function]
 //rule [L:KList,,C:CatchClause] => toCatches([L,,C])
@@ -63,7 +60,7 @@ syntax BreakStmt ::= "break" K ";" [klabel('Break)]
 syntax ReturnStmt ::= "return" K ";" [klabel('Return)]
 
 syntax SynchronizedStmt ::= "synchronized" "(" Exp ")" Block [strict(1),klabel('Synchronized)]
-//todo: replace Exp with StmtExp
+//todo: replace Exp with StmtExp when all StmtExp are defined
 syntax ExprStmt ::= Exp ";"  [strict, klabel('ExprStm)]
 
 endmodule

src/exec/api-threads.k

@@ -46,7 +46,7 @@ when
 
 rule [Synchronized-first-time]:
     <k>
-          synchronized (objectRef(OId:Int,_)::_) Block:Block
+          synchronized (objectRef(OId:Int,_)::_) Block:K
           => try Block [.KList] finally releaseLock(OId)
           ...
     </k>
@@ -58,7 +58,7 @@ when
 
 rule [Synchronized-nested]:
     <k>
-            synchronized (objectRef(OId:Int,_)::_) Block:Block
+            synchronized (objectRef(OId:Int,_)::_) Block:K
             => try Block [.KList] finally releaseLock(OId)
       ...
     </k>

src/exec/method-invoke.k

@@ -760,7 +760,7 @@ syntax KItem ::= initParams ( Params,   // {T:Type X:Id},... - parameter declara
 
 rule [initParams]:
     initParams(P{T:Type X:Id}, RestP:Params, (TV:TypedVal, RestV:TypedVals))
-      => [.KList] T X;
+      => T X;
       ~> (X = ((T) TV:TypedVal));
       ~> initParams(RestP, RestV)
 

src/exec/statements.k

@@ -49,7 +49,7 @@ rule [env-double-Discard]:
     Not only local but fields also*/
 
 rule [LocalVarDec]:
-    <k> _:KListWrap T:Type X:Id; => . ...</k>
+    <k> T:Type X:Id; => . ...</k>
     <env> Env:Map => Env[L/X] </env>
     <store>... . => L |-> default(T) ...</store>
     <storeMetadata>... . => L |-> LocalLocMetadata ...</storeMetadata>
@@ -423,6 +423,7 @@ rule [Try-Catch-Finally-Desugar]:
 context try _:K [_,, HOLE,, _]
 
 //resolve 'Param term of the catch clause
+
 context catch(HOLE)_                                [result(ExtKResult)]
 
 rule catch(KR:ExtKResult)S:K => catchImpl(KR,S)

src/exec/syntax-conversions.k

@@ -68,10 +68,8 @@ syntax MethodName ::= Id | MethodRef
 
 /*@ \subsection{Local variable declaration}*/
 
-//@ 'LocalVarDec(\_:K,, T:Type,, ['VarDec(X:Id)])
 syntax KLabel ::= "'VarDec"
-
-rule 'LocalVarDec(_:KListWrap,, T:Type,,(['VarDec(X:Id)] => X)) [structural]
+rule 'LocalVarDec(_:K,, T:Type,,['VarDec(X:Id)]) => T X;  [structural]
 
 /*@ \subsection{Cast}*/