KJ-15 Eliminated the rule unwrapElabNaked - replaced with context rule.

The logic of literals had to be changed slightly. I had to review what should be wrapped into elab and what should not.

Author: denis-bogdanas

semantics/api-core.k

@@ -84,7 +84,7 @@ rule [object-getClass-on-object]:
       invokeImpl(
         methodClosure(_,_,_,_,_,_, 'NoMethodBody(_))::methodType(sig(MethodName:Id, _),_), OL:Int,
         'ListWrap(.KList)
-      ) => 'Lit('Class(T))
+      ) => elab('Lit('Class(T)))
       ...
     </k>
     <store>
@@ -99,15 +99,15 @@ rule [object-getClass-on-String]:
     invokeImpl(
       methodClosure(_,_,_,_,_,_, 'NoMethodBody(_))::methodType(sig(MethodName:Id, _),_), Str:String::rtString,
       'ListWrap(.KList)
-    ) => 'Lit('Class(rtString))
+    ) => elab('Lit('Class(rtString)))
 when
     Id2String(MethodName) ==String "getClass"
 
 rule [object-getClass-on-array]:
     invokeImpl(
       methodClosure(_,_,_,_,_,_, 'NoMethodBody(_))::methodType(sig(MethodName:Id, _),_), arrayRef(_,_,_)::ArrT:Type,
       'ListWrap(.KList)
-    ) => 'Lit('Class(ArrT))
+    ) => elab('Lit('Class(ArrT)))
 when
     Id2String(MethodName) ==String "getClass"
 

semantics/api-threads.k

@@ -108,7 +108,7 @@ rule [synchronized-method-inst-desugar]:
 rule [synchronized-method-static-desugar]:
     <k>
       storeMethod(_, staticCT, _, (true => false)::bool, _,_,
-          Body:K => 'Synchronized('Lit('Class(Class)),, Body),
+          Body:K => 'Synchronized(elab('Lit('Class(Class))),, Body),
           _)
       ...
     </k>

semantics/elaborate-blocks.k

@@ -280,14 +280,15 @@ The attribute [transition-strictness] is used as transition attribute for testin
 This is a rule that may lead to unexpected nondeterminism if it is wrongly implemented.
 In order to expose incorrect nondeterminism we need to model-check a program that exposes the nondeterminism.
 */
-rule [elabHeatDefault]:
+rule [elabHeat-default]:
     (. => elab(K)) ~> elab(KL:KLabel(HeadKs:KList,, (K:K => CHOLE),, TailKs:KList))
 when
             defaultElabChildren(KL)
             //notBool customElabChildren(KL)
     andBool notBool isElab(K)
+    andBool notBool isElabNaked(K)
     andBool isElab(HeadKs)    //Forces elaboration left-to-right. Required when KL == 'ListWrap of statements.
-    [transition-strictness]
+        [transition-strictness]
 
 rule [elabCool-default]:
     (ElabK:K => .) ~> elab(_:KLabel(_,, (CHOLE => ElabK),, _))
@@ -460,11 +461,11 @@ rule defaultElabChildren(KL:KLabel) =>
     orBool (KL ==KLabel 'Throw)
     orBool (KL ==KLabel 'Synchronized)
     orBool (KL ==KLabel 'Try)
-//    orBool (KL ==KLabel 'Catch)
-//    orBool (KL ==KLabel 'LocalVarDecStm)
-//    orBool (KL ==KLabel 'LocalVarDec)
-//    orBool (KL ==KLabel 'Block)
-//    orBool (KL ==KLabel 'ClassDecStm)
+    /*orBool (KL ==KLabel 'Catch)
+    orBool (KL ==KLabel 'LocalVarDecStm)
+    orBool (KL ==KLabel 'LocalVarDec)
+    orBool (KL ==KLabel 'Block)
+    orBool (KL ==KLabel 'ClassDecStm)*/
     /*orBool (KL ==KLabel 'MethodDec)
     orBool (KL ==KLabel 'MethodDecHead)
     orBool (KL ==KLabel 'DeprMethodDecHead)
@@ -494,8 +495,8 @@ rule defaultElabChildren(KL:KLabel) =>
 //    orBool (KL ==KLabel 'TypeName)
     orBool (KL ==KLabel 'ExprName)
 
-    orBool auxLabelInElab(KL)
     orBool (KL ==KLabel 'MethodName)
+    orBool auxLabelInElab(KL)
     /*orBool (KL ==KLabel 'PackageOrTypeName)
     orBool (KL ==KLabel 'TypeArgs)
     orBool (KL ==KLabel 'TypeArgs)
@@ -546,8 +547,18 @@ rule auxLabelInElab(KL:KLabel) =>
     orBool KL ==KLabel 'stmtAndExp`(_`,_`)
     orBool KL ==KLabel 'toString`(_`)
 
-/*@ Represents terms that shoud never be wrapped by elab() or related wrappers. They are processed to their final state
-  in elaboration phase. Those are types names, package names, id's ad literals.
+/*@  elabHeat-naked-children
+  Since a naked term is always computed int oa KResult during elaboration,
+  we can use a simple context rule to heat such terms.
+*/
+context elab(KL:KLabel(_:KList,, HOLE,, _:KList))
+when
+            defaultElabChildren(KL)
+    andBool isElabNaked(HOLE)
+
+/*@ Naked terms are those that should be computed directly into KResult during elaboration.
+  Those are literals, types and packages. They are heated "as is", without being wrapped into elab().
+  An exception is the class literal that is not executed during elaboration.
 */
 syntax K ::= "isElabNaked" "(" K ")"                            [function]
 rule isElabNaked(K:K) =>
@@ -561,15 +572,10 @@ rule isElabNaked(K:K) =>
     orBool (getKLabel(K) ==KLabel 'PackageName)
     orBool (getKLabel(K) ==KLabel 'PackageOrTypeName)
     orBool (getKLabel(K) ==KLabel 'Id)
-    orBool (getKLabel(K) ==KLabel 'Lit)
+    orBool (getKLabel(K) ==KLabel 'Lit andBool getInnerKLabel(K) =/=KLabel 'Class)
 
-/*@ The sole place where isElabNaked is used - naked terms should be automatically unwrapped from elab() wrapper.
-  Will not match .K - is not isElabNaked. (.K) is matched by [elabDotK].
-*/
-rule [unwrapElabNaked]:
-    elab(K:K) => K
-when
-    isElabNaked(K)
+syntax KLabel ::= "getInnerKLabel" "(" K ")"                    [function]
+rule getInnerKLabel(_:KLabel(KL:KLabel(_))) => KL
 
 /*@ The default algorithm of transforming the term from elab to elabRes, when the children were completely elaborated.
   Deletes elabRes wrappers from children. This algorithm is activated when the following conditions apply:
@@ -1238,13 +1244,15 @@ rule [elab-QNewInstance]:
 rule [elabInstanceOf]:
     elabDispose('InstanceOf(TE:TypedExp,, RT2:RefType)) => elabRes('InstanceOf(TE,, RT2) :: bool)
 
-context 'Lit('Class(HOLE))
+//@ Class literal types are heated by this rule.
+context elab('Lit('Class(HOLE)))
 
 rule [elabLitClass]:
-    'Lit('Class(T:Type)) => elabRes('Lit('Class(T:Type)) :: class String2Id("java.lang.Class"))
+    elab('Lit('Class(T:Type))) => elabRes('Lit('Class(T:Type)) :: class String2Id("java.lang.Class"))
 
 rule [elabArrayAccess]:
-    elabDispose('ArrayAccess(TargetExp:K::arrayOf T:Type,, IndexTE:TypedExp)) => elabRes('ArrayAccess(TargetExp::arrayOf T,, IndexTE) :: T)
+    elabDispose('ArrayAccess(TargetExp:K::arrayOf T:Type,, IndexTE:TypedExp))
+    => elabRes('ArrayAccess(TargetExp::arrayOf T,, IndexTE) :: T)
 
 rule [elabArrayLength]:
     elabDispose('Field(Qual:K :: arrayOf T:Type,, X:Id))

semantics/literals.k

@@ -8,7 +8,6 @@ module LITERALS
     imports CORE
     imports AUX-STRINGS
     imports PRIMITIVE-TYPES
-    imports ELABORATE-BLOCKS //for elab(), should disappear after semantics separation
 
 //@ \subsection{Auxiliary constructs}
 
@@ -153,9 +152,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)))
-      => elab('Plus('Lit('String('ListWrap(K1))),,
+      => 'Plus('Lit('String('ListWrap(K1))),,
                'Lit('String('ListWrap(K2,, Ks)))
-          ))
+          ) :: rtString
 
 rule 'Lit('String('ListWrap('Chars(Str:String)))) => Str