new try catch syntax

Author: laurayuwen

src/common/stmt-syntax.k

@@ -43,15 +43,20 @@ 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 Catches ::= List{CatchClause,""}
-//syntax KItem ::= toCatches( KListWrap )          [function]
-//           | toCatches( KListWrap , Catches ) [function]
-//rule [L:KList,,C:CatchClause] => toCatches([L,,C])
-//rule toCatches([KLCatches:KList]) => toCatches([KLCatches],.Catches)
-//rule toCatches([KLCatches:KList,, C:CatchClause], Catches:Catches) => toCatches([KLCatches], (C Catches))
-//rule toCatches([.KList], Catches:Catches) => Catches
+
+syntax Param ::= Type Id
+syntax CatchClause ::= "catch" "(" Param ")" Block [klabel('Catch)]
+syntax CatchClauses ::= List{CatchClause,""}
+syntax CatchClauses ::= toCatchClauses( KListWrap )          [function]
+           | toCatchClauses( KListWrap , CatchClauses ) [function]
+rule [L:KList,,C:CatchClause] => toCatchClauses([L,,C])
+rule toCatchClauses([KLCatchClauses:KList]) => toCatchClauses([KLCatchClauses],.CatchClauses)
+rule toCatchClauses([KLCatchClauses:KList,, C:CatchClause], CatchClauses:CatchClauses) => toCatchClauses([KLCatchClauses], (C CatchClauses))
+rule toCatchClauses([.KList], CatchClauses:CatchClauses) => CatchClauses
+
+//syntax TryStmt ::= "try" Block CatcheClauses "finally" Block [klabel('Try)]
+//		           |"try" Block CatcheClauses [klabel('Try)]
+//rule 'Try(B1)
 
 syntax StackConsumerStmt ::= "dummyStackConsumerStmt"|ThrowStmt|ContinueStmt|BreakStmt|ReturnStmt
 syntax ThrowStmt ::= "throw" K ";" [strict, klabel('Throw)]

src/exec/method-invoke.k

@@ -767,7 +767,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))
+    initParams((T:Type X:Id, RestP:Params), (TV:TypedVal, RestV:TypedVals))
       => T X;
       ~> (X = ((T) TV:TypedVal));
       ~> initParams(RestP, RestV)

src/exec/statements.k

@@ -358,7 +358,7 @@ rule [Throw]:
     (. => checkCatch(subtype(typeOf(TV), T)))
 //    ~> 'Throw(TV:TypedVal)
     ~> throw TV:TypedVal;
-    ~> catchBlocks([catchImpl('ParamImpl(T:Type,, X:Id),_),, _])
+    ~> catchBlocks([catchImpl(T:Type X:Id,_),, _])
 
 syntax KItem ::= checkCatch ( K )
 context checkCatch(HOLE)
@@ -426,7 +426,7 @@ context try _:K [_,, HOLE,, _]
 
 context catch(HOLE)_                                [result(ExtKResult)]
 
-rule catch(KR:ExtKResult)S:K => catchImpl(KR,S)
+rule catch(KR:Param)S:K => catchImpl(KR,S)
 
 /*@ Extended K Result.
   Represents KLabels that should be treated as KResult during execution phase, but not during elaboration phase.
@@ -435,7 +435,7 @@ syntax ExtKResult ::= "dummy"
 
 rule isExtKResult(KR:KResult) => true
 
-rule isExtKResult('ParamImpl(T:Type,, _:Id)) => true
+rule isExtKResult(T:Type _:Id) => true
 
 //@ Internal representation of a preprocessed catch clause
 syntax KResult ::=  catchImpl (

src/exec/syntax-conversions.k

@@ -13,23 +13,20 @@ module SYNTAX-CONVERSIONS
 // 'Param(\_:K,, T:Type,, X:Id). Consumed by initParams().
 syntax KLabel ::= "'Param"
 
-//Required for catch
-rule 'Param(_,, K:K,, X:Id) => P{K X} [structural]
-
-//add P to {} in case of ambiguity
-syntax Param ::= "P{" K Id "}"        [klabel('ParamImpl)]
+//Required for catch, 'Param cannot be added as klabel attribute for Param ::= Type Id
+rule 'Param(_,, K:Type,, X:Id) => K X [structural]
 
 syntax Params ::= List{Param, ","}
 
 syntax KItem ::= toParams( KListWrap )          [function]
            | toParams( KListWrap , Params ) [function]
 
 rule toParams([KLParams:KList]) => toParams([KLParams], .Params)
-rule toParams([KLParams:KList,, 'Param(_,, K:K,, X:Id)], Params:Params) => toParams([KLParams], (P{K X},Params))
+rule toParams([KLParams:KList,, 'Param(_,, K:Type,, X:Id)], Params:Params) => toParams([KLParams], (K X,Params))
 rule toParams([.KList], Params:Params) => Params
 
 // Required for getTypes()
-rule typeOf('ParamImpl(T:Type,, _:Id)) => T
+rule typeOf(T:Type _:Id) => T
 
 /*@ \subsection{Method invocation}*/