KJ-11 Eliminate the rule [runtime-elabExpressions]

Implemented, awaits confirmation by jenkins tests.

Author: denis-bogdanas

semantics/api-core.k

@@ -187,7 +187,7 @@ when
 
 rule [methodInvokeRuntime-String-equals]:
     methodInvokeRuntime(rtString, sig(MethodName:Id, _), ThisStr:String::_, ParamStr:String::_ ,_ )::_
-    => 'Eq(ThisStr,, ParamStr)
+    => elab('Eq(ThisStr,, ParamStr))
 when Id2String(MethodName) ==String "equals"
 
 //@String.toString()
@@ -213,7 +213,7 @@ when
 
 rule [methodInvokeRuntime-String-compareTo]:
     methodInvokeRuntime(rtString, sig(MethodName:Id, _), ThisStr:String::_, ParamStr:String::_ ,_ )::_
-    => 'If(ThisStr <String ParamStr,, -1,, 'If(ThisStr ==String ParamStr,, 0,, 1))
+    => elab('If(ThisStr <String ParamStr,, -1,, 'If(ThisStr ==String ParamStr,, 0,, 1)))
 when Id2String(MethodName) ==String "compareTo"
 
 //@\subsection{Array clone}

semantics/api-threads.k

@@ -27,7 +27,7 @@ rule [thread-start]:
       <thread>
         <k>
           //typedLookup(OL).runnable.run()
-          'ExprStm(
+          elab('ExprStm(
             'Invoke(
               'Method(
                 'MethodName(
@@ -40,7 +40,7 @@ rule [thread-start]:
               ),,
               'ListWrap(.KList)
             )
-          )
+          ))
         </k>
         <tid> TId </tid>
         ...
@@ -78,12 +78,12 @@ rule [Synchronized-nested]:
 
 rule [Synchronized-on-null]:
     'Synchronized(null::_,,_)
-    =>  'Throw('NewInstance(
+    =>  elab('Throw('NewInstance(
           'None(.KList),,
           class String2Id("java.lang.NullPointerException"),,
           'ListWrap( null ),,
           'None(.KList)
-        ))
+        )))
 
 /*@Release one level of lock for the given object.*/
 syntax K ::= "releaseLock" "(" Int ")"
@@ -137,12 +137,12 @@ rule [thread-join-interrupted]:
         methodClosure(Class:ClassType,_,_,_,_,_, 'NoMethodBody(_))::methodType(sig(MethodName:Id, _),_), _,
         'ListWrap(TId:Int :: _)
       )
-      =>  'Throw('NewInstance(
+      =>  elab('Throw('NewInstance(
             'None(.KList),,
             class String2Id("java.lang.InterruptedException"),,
             'ListWrap( null ),,
             'None(.KList)
-          ))
+          )))
       ...
     </k>
     <interrupted> true => false </interrupted>
@@ -178,12 +178,12 @@ rule [object-wait-notify-notifyAll-without-sync]:
         methodClosure(Class:ClassType,_,_,_,_,_, 'NoMethodBody(_))::methodType(sig(MethodName:Id, _),_),
         OL:Int, 'ListWrap(.KList)
       )
-      =>  'Throw('NewInstance(
+      =>  elab('Throw('NewInstance(
             'None(.KList),,
             class String2Id("java.lang.IllegalMonitorStateException"),,
             'ListWrap( null ),,
             'None(.KList)
-          ))
+          )))
       ...
     </k>
     <holds> Holds:Map </holds>
@@ -218,12 +218,12 @@ when
 rule [waitImpl-interrupted]:
     <k>
       waitImpl(OL:Int)
-      =>  'Throw('NewInstance(
+      =>  elab('Throw('NewInstance(
             'None(.KList),,
             class String2Id("java.lang.InterruptedException"),,
             'ListWrap( null ),,
             'None(.KList)
-          ))
+          )))
       ...
     </k>
     <tid> TId:Int </tid>

semantics/arrays.k

@@ -34,7 +34,7 @@ rule [ArrayVarDecIdDiscard]:
 rule [VarDecWithArrayInitDesugar]:
     'LocalVarDec(_:K,, T:Type,, 'ListWrap('VarDec(
       X:Id,,
-      ( 'ArrayInit(InitK:K) => 'NewArray(T,, 'ListWrap(.KList),, 'ArrayInit(InitK)) )
+      ( 'ArrayInit(InitK:K) => elab('NewArray(T,, 'ListWrap(.KList),, 'ArrayInit(InitK))) )
     )))                                                 [structural, anywhere]
 
 //same three rules for fields
@@ -58,7 +58,7 @@ rule [ArrayFieldDecIdDiscard]:
 rule [FieldDecWithArrayInitDesugar]:
     'FieldDec(_:K,, T:Type,, 'ListWrap('VarDec(
       X:Id,,
-      ( 'ArrayInit(InitK:K) => 'NewArray(T,, 'ListWrap(.KList),, 'ArrayInit(InitK)) )
+      ( 'ArrayInit(InitK:K) => elab('NewArray(T,, 'ListWrap(.KList),, 'ArrayInit(InitK))) )
     )))                                                 [structural]
 
 //first two rules - desugaring C-like array declarations, for params
@@ -104,28 +104,28 @@ rule [lookupArrayLocation]:
 
 rule [ArrayIndexOutOfBoundsException]:
     'ArrayAccess(arrayRef(_,_,M:Int) :: _,, N:Int::_)::_
-    => 'Throw('NewInstance(
+    => elab('Throw('NewInstance(
       'None(.KList),,
       (class String2Id("java.lang.ArrayIndexOutOfBoundsException")),,
       'ListWrap( Int2String(N) ),,
       'None(.KList)
-    ))
+    )))
 when notBool ((N >=Int 0) andBool (N <Int M))
         [structural, anywhere]
 
-//Required to desugar effects of the previous rule, when exception happens
-//inside lvalue.
+/*@ Required when a JVM-related exception (e.g. produced by the semantics at runtime) is thrown inside a lvalue.
+*/
 rule [LvalueIndexOutOfBoundsDesugar]:
-    lvalue('Throw(K:K)) => 'Throw(K)
+    lvalue(elab('Throw(K:K))) => elab('Throw(K))
 
 rule [arrayAccessNull]:
     'ArrayAccess(null::_ ,, _)::_
-    => 'Throw('NewInstance(
+    => elab('Throw('NewInstance(
       'None(.KList),,
       class String2Id("java.lang.NullPointerException"),,
       'ListWrap( null ),,
       'None(.KList)
-    ))
+    )))
         [structural, anywhere]
 
 //Array length, as defined in JDK
@@ -174,12 +174,12 @@ when NI >=Int 0
 
 rule [NegativeArraySizeException]:
     checkNonNegative((NI:Int::_),, _)
-    => 'Throw('NewInstance(
+    => elab('Throw('NewInstance(
       'None(.KList),,
       class String2Id("java.lang.NegativeArraySizeException"),,
       'ListWrap( null ),,
       'None(.KList)
-    ))
+    )))
 when
     NI <Int 0
 
@@ -279,7 +279,7 @@ rule [assignImpl]:
 
 rule [ArrayStoreException]:
     assignImpl( false::bool, _, TV:TypedVal)
-    =>  'Throw('NewInstance(
+    =>  elab('Throw('NewInstance(
           'None(.KList),,
           (class String2Id("java.lang.ArrayStoreException")),,
           'ListWrap(
@@ -295,7 +295,7 @@ rule [ArrayStoreException]:
             )
           ),,
           'None(.KList)
-        ))
+        )))
 
 //@ \subsection{Array initializer}
 

semantics/classes.k

@@ -28,10 +28,10 @@ module CLASSES
 //@ \texttt{toString for objectClosure}
 
 rule toString(objectClosure(I:Int, Obj:List, ObjLocalClassesEnv:Map) :: T:Type)
-    =>  'Invoke(
+    =>  elab('Invoke(
           'MethodName(objectClosure(I, Obj, ObjLocalClassesEnv) :: T,, String2Id("toString")),,
           'ListWrap(.KList)
-        )
+        ))
         [anywhere]
 
 //@ \texttt{typeOf for reference types}
@@ -142,10 +142,10 @@ syntax K ::= "invokeConstr" "(" Int       //OL - object location
 rule [invokeConstr]:
     invokeConstr(OL:Int, Class:ClassType, Vals:KList, EnclosingObj:KResult)
     => setEncloser(lookup(OL)::Class, Class, EnclosingObj)
-    ~> 'ExprStm('Invoke(
+    ~> elab('ExprStm('Invoke(
           'Method('MethodName( lookup(OL)::Class,, getConsName(Class) )),,
           'ListWrap( Vals )
-        ))
+        )))
 
 rule [setEncloser-value]:
     <k>
@@ -249,13 +249,13 @@ rule [CastRef]:
       =>  'If(
             subtype(typeOf(V), RT1),,
             (V::RT1),,
-            'Throw('NewInstance(
+            elab('Throw('NewInstance(
                     'None(.KList),,
                     (class String2Id("java.lang.ClassCastException")),,
                     'ListWrap( 'Plus('Plus(toString(typeOf(V)),, " cannot be cast to ")::rtString,,
                         toString(RT1))::rtString ),,
                     'None(.KList)
-                  ))
+            )))
           )
       ...
     </k>

semantics/elaborate-blocks.k

@@ -547,17 +547,9 @@ rule [unwrapElabNaked]:
 when
     isElabNaked(K)
 
-rule [elabCoolStatement]:
+rule [elabCool-elabRes]:
     (elabRes(K:K) => .) ~> elab(_:KLabel(_,, (CHOLE => elabRes(K)),, _))
-/*when
-    notBool isElabIndependent(K)*/
 
-/*rule [elabCoolExpressionOrKResult]:
-    (elabRes(ElabIndep:K) => .) ~> elab(_:KLabel(_,, (CHOLE => ElabIndep),, _))
-when
-    isElabIndependent(ElabIndep)*/
-
-/*Was KR:ElabIndependent before, but in fact only KResult may stay free in this position.*/
 rule [elabCoolKResult]:
     (KR:KResult => .) ~> elab(_:KLabel(_,, (CHOLE => KR),, _))
 
@@ -599,18 +591,6 @@ rule isElab(K:K,, Ks:KList)
 
 rule isElab(.KList) => true
 
-/*@ Either of:
-  - KResult
-  - TypedExp
-Used in defaut cooling rules of elaboration phase, to distinguish between elborated statements and elaborated
-  expressions. When expressions are cooled they are unwrapped fron thei elabRes() wrapper.
-*/
-/*
-syntax K ::= "isElabIndependent" "(" K ")"            [function]
-rule isElabIndependent(K:K)
-     => (isKResult(K) ==K true) orBool (isTypedExp(K) ==K true)
-*/
-
 //@ True if given KList have no terms of the form elabRes(...), false otherwise.
 syntax K ::= "haveNoElabRes" "(" KList ")"          [function]
 rule haveNoElabRes(K:K,, Ks:KList)
@@ -1287,24 +1267,17 @@ rule count(Ks:KList) => count(0, Ks)
 rule count(I:Int, K:K,, Ks:KList) => count(I +Int 1, Ks)
 rule count(I:Int, .KList) => I::int
 
-//todo latex workaround: manual character escape: \%
-
-//@ Elaborate all expressions once they reach the top of computation,
-//@ both in elaboration and in execution phase.
-//@ Performance: Using this rule instead of the rule above leads to execution performance decrease by 5\%
-//@ in helloWorld, with medium execution time rising from 9.6s to 10.1s
-rule [runtime-elabExpressions]:
-    KL:KLabel(Ks:KList) => elab(KL(Ks))
-when
-    isExpressionLabel(KL)
-
 //@ Unwrap elaborated terms in execution phase, so that they could be executed.
-rule [elabResInExecutionPhase]:
+rule [elabRes-ExecutionPhase-discard1]:
     <k> (elabRes(K:K) => K) ~> KL:KLabel(_) ...</k>
-     <globalPhase> ExecutionPhase  </globalPhase>
+    <globalPhase> ExecutionPhase </globalPhase>
 when
     KL =/=KLabel 'elab`(_`)
 
+rule [elabRes-ExecutionPhase-discard2]:
+    <k> elabRes(K:K) => K </k>
+    <globalPhase> ExecutionPhase </globalPhase>
+
 //@\subsection{Elaboration of SuperConstrInv, AltConstrInv}
 
 //@ Desugaring unqualified superclass constructor invocation into a qualified one

semantics/expressions.k

@@ -118,25 +118,25 @@ rule                  'Div(F1:Float :: _,, F2:Float :: _) :: ResT:FloatType => (
 
 //todo test that the first argument is fully evaluated, right now it may be not evaluated
 rule                  'Div(_::_     ,, 0::_)::_
-   => 'Throw('NewInstance(
+   => elab('Throw('NewInstance(
         'None(.KList),,
         (class String2Id("java.lang.ArithmeticException")),,
         'ListWrap( "/ by zero" ),,
         'None(.KList)
-      ))
+      )))
 
 rule /* I1 % I2    */ 'Remain(I1:Int :: _,, I2:Int :: _) :: ResT:IntType => normalize( (I1 %Int I2) :: ResT )
     when I2 =/=Int 0
 rule                  'Remain(F1:Float :: _,, F2:Float :: _) :: ResT:FloatType => (F1 %Float F2) :: ResT
 
 //todo test that the first argument is fully evaluated, right now it may be not evaluated
 rule                  'Remain(_::_     ,, 0::_)::_
-   => 'Throw('NewInstance(
+   => elab('Throw('NewInstance(
         'None(.KList),,
         (class String2Id("java.lang.ArithmeticException")),,
         'ListWrap( "/ by zero" ),,
         'None(.KList)
-      ))
+      )))
 
 rule [NormalizeLeftOperandToFloat]:
     KL:KLabel((I:Int::_:IntType => Int2Float(I)::float),, _:Float :: _:FloatType)::_

semantics/literals.k

@@ -8,6 +8,7 @@ module LITERALS
     imports CORE
     imports AUX-STRINGS
     imports PRIMITIVE-TYPES
+    imports ELABORATE-BLOCKS //for elab(), should disappear after semantics separation
 
 //@ \subsection{Auxiliary constructs}
 
@@ -152,9 +153,9 @@ rule 'Lit('Char('UnicodeEscape(_:K,, I1:Int,, I2:Int,, I3:Int,, I4:Int)))
 //@ \subsection{String literals}
 
 rule  'Lit('String('ListWrap(K1:K,, K2:K,, Ks:KList)))
-      => 'Plus('Lit('String('ListWrap(K1))),,
+      => elab('Plus('Lit('String('ListWrap(K1))),,
                'Lit('String('ListWrap(K2,, Ks)))
-          )
+          ))
 
 rule 'Lit('String('ListWrap('Chars(Str:String)))) => Str
 

semantics/method-invoke.k

@@ -418,12 +418,12 @@ when
 
 rule [methodInvokeRuntimeOnNull]:
     methodInvokeRuntime(_,_, null::_, ParamVals:KList, instanceCT)::_
-    =>  'Throw('NewInstance(
+    =>  elab('Throw('NewInstance(
           'None(.KList),,
           class String2Id("java.lang.NullPointerException"),,
           'ListWrap( null ),,
           'None(.KList)
-        ))
+        )))
 when
     isKResult(ParamVals)
 
@@ -649,7 +649,7 @@ syntax K ::= "bindto" KList
 rule [bindto]:
     <k>
       bindto paramImpl(T:Type, X:Id),, RestP:KList, TV:TypedVal,, RestV:KList
-      => 'ExprStm('Assign(localVar(X)::T,,TV:TypedVal)) ~> bindto RestP, RestV
+      => elab('ExprStm('Assign(localVar(X)::T,,TV:TypedVal))) ~> bindto RestP, RestV
       ...
     </k>
     <env> Env:Map => Env[L/X] </env>

semantics/process-local-classes.k

@@ -225,7 +225,7 @@ rule buildConstructorFirstLineArgs(.KList, Ks:KList, _) => resultListWrap(Ks)
 
 rule [elabAnonymous-QNewInstance-extends-class]:
     <k>
-      elab('QNewInstance(Qual:TypedExp,, Arg2:K,, Class:ClassType,, Arg4:K,,
+      elab('QNewInstance(elabRes(Qual:TypedExp),, Arg2:K,, Class:ClassType,, Arg4:K,,
           elabRes('ListWrap(ActualArgs:KList)),,
           'Some('ClassBody('ListWrap(AnonClassDecs:KList)))
       ))