KJ-9 create predicate defaultElabChildren, opposite to customElabChildren

Author: denis-bogdanas

semantics/elaborate-blocks.k

@@ -281,12 +281,14 @@ rule [elabParamsEnd]:
 rule [elabHeatDefault]:
     (. => elab(K)) ~> elab(KL:KLabel(HeadKs:KList,, (K:K => CHOLE),, TailKs:KList))
 when
-            notBool customElabChildren(KL)
+            defaultElabChildren(KL)
+            //notBool customElabChildren(KL)
     andBool notBool isElab(K)
-    andBool notBool isElabNaked(KL(HeadKs,,K,,TailKs))
+    //andBool notBool isElabNaked(KL(HeadKs,,K,,TailKs))
     andBool isElab(HeadKs)    //Forces elaboration left-to-right. Required when KL == 'ListWrap of statements.
     [transition-strictness]
 
+
 /*@ Terms that should use custom elaboration rules. For those terms:
     - They will not be automatically heated from their parents into the elab() state.
     - They will not be automatically passed to elabDispose() state. Instead, those terms should have custom rules
@@ -324,6 +326,218 @@ rule isElabNaked(K:K) =>
     orBool (getKLabel(K) ==KLabel 'Id)
     orBool (getKLabel(K) ==KLabel 'Lit)
 
+/*@ Java KLabels that are processed by default heating/cooling rules of elaboration.
+All KLabels that can be part of a code block during elaboration phase,
+except those members of customElabChildren or isElabNaked groups.
+*/
+syntax K ::= "defaultElabChildren" "(" KLabel ")"                [function]
+rule defaultElabChildren(KL:KLabel) =>
+           (KL ==KLabel 'ListWrap)
+    orBool (KL ==KLabel 'Some)
+    orBool (KL ==KLabel 'None)
+    /*orBool (KL ==KLabel 'Single)
+    orBool (KL ==KLabel 'NamedEscape)
+    orBool (KL ==KLabel 'OctaEscape1)
+    orBool (KL ==KLabel 'OctaEscape2)
+    orBool (KL ==KLabel 'OctaEscape3)
+    orBool (KL ==KLabel 'UnicodeEscape)
+    orBool (KL ==KLabel 'String)
+    orBool (KL ==KLabel 'Chars)*/
+
+    orBool (KL ==KLabel 'Assign)
+    orBool (KL ==KLabel 'AssignMul)
+    orBool (KL ==KLabel 'AssignDiv)
+    orBool (KL ==KLabel 'AssignRemain)
+    orBool (KL ==KLabel 'AssignPlus)
+    orBool (KL ==KLabel 'AssignMinus)
+    orBool (KL ==KLabel 'AssignLeftShift)
+    orBool (KL ==KLabel 'AssignRightShift)
+    orBool (KL ==KLabel 'AssignURightShift)
+    orBool (KL ==KLabel 'AssignAnd)
+    orBool (KL ==KLabel 'AssignExcOr)
+    orBool (KL ==KLabel 'AssignOr)
+    orBool (KL ==KLabel 'InstanceOf)
+    orBool (KL ==KLabel 'Mul)
+    orBool (KL ==KLabel 'Div)
+    orBool (KL ==KLabel 'Remain)
+    orBool (KL ==KLabel 'Plus)
+    orBool (KL ==KLabel 'Minus)
+    orBool (KL ==KLabel 'LeftShift)
+    orBool (KL ==KLabel 'RightShift)
+    orBool (KL ==KLabel 'URightShift)
+    orBool (KL ==KLabel 'Lt)
+    orBool (KL ==KLabel 'Gt)
+    orBool (KL ==KLabel 'LtEq)
+    orBool (KL ==KLabel 'GtEq)
+    orBool (KL ==KLabel 'Eq)
+    orBool (KL ==KLabel 'NotEq)
+    orBool (KL ==KLabel 'LazyAnd)
+    orBool (KL ==KLabel 'LazyOr)
+    orBool (KL ==KLabel 'And)
+    orBool (KL ==KLabel 'ExcOr)
+    orBool (KL ==KLabel 'Or)
+    orBool (KL ==KLabel 'Cond)
+    orBool (KL ==KLabel 'PreIncr)
+    orBool (KL ==KLabel 'PreDecr)
+    orBool (KL ==KLabel 'Complement)
+    orBool (KL ==KLabel 'Not)
+    orBool (KL ==KLabel 'CastPrim)
+    orBool (KL ==KLabel 'CastRef)
+    orBool (KL ==KLabel 'PostIncr)
+    orBool (KL ==KLabel 'PostDecr)
+    orBool (KL ==KLabel 'Invoke)
+    orBool (KL ==KLabel 'Method)
+    orBool (KL ==KLabel 'SuperMethod)
+    orBool (KL ==KLabel 'QSuperMethod)
+    orBool (KL ==KLabel 'GenericMethod)
+    orBool (KL ==KLabel 'ArrayAccess)
+    orBool (KL ==KLabel 'Field)
+    orBool (KL ==KLabel 'SuperField)
+    orBool (KL ==KLabel 'QSuperField)
+    orBool (KL ==KLabel 'NewArray)
+//    orBool (KL ==KLabel 'UnboundWld)
+    orBool (KL ==KLabel 'Dim)
+//    orBool (KL ==KLabel 'NewInstance)
+//    orBool (KL ==KLabel 'QNewInstance)
+//    orBool (KL ==KLabel 'Lit)
+//    orBool (KL ==KLabel 'Class)
+   /* orBool (KL ==KLabel 'VoidClass)*/
+    orBool (KL ==KLabel 'This)
+    orBool (KL ==KLabel 'QThis)
+    /*orBool (KL ==KLabel 'PackageDec)
+    orBool (KL ==KLabel 'TypeImportDec)
+    orBool (KL ==KLabel 'TypeImportOnDemandDec) //ok
+    orBool (KL ==KLabel 'StaticImportDec)
+    orBool (KL ==KLabel 'StaticImportOnDemandDec)
+    orBool (KL ==KLabel 'AnnoDec)
+    orBool (KL ==KLabel 'AnnoDecHead)
+    orBool (KL ==KLabel 'AnnoMethodDec)
+    orBool (KL ==KLabel 'Semicolon)
+    orBool (KL ==KLabel 'DefaultVal)
+    orBool (KL ==KLabel 'AbstractMethodDec)
+    orBool (KL ==KLabel 'DeprAbstractMethodDec)
+    orBool (KL ==KLabel 'ConstantDec)
+    orBool (KL ==KLabel 'InterfaceDec)
+    orBool (KL ==KLabel 'InterfaceDecHead)
+    orBool (KL ==KLabel 'ExtendsInterfaces)
+    orBool (KL ==KLabel 'EnumDec)
+    orBool (KL ==KLabel 'EnumDecHead)
+    orBool (KL ==KLabel 'EnumBody)
+    orBool (KL ==KLabel 'EnumConst)
+    orBool (KL ==KLabel 'EnumBodyDecs)*/
+    /*orBool (KL ==KLabel 'ConstrDec)
+    orBool (KL ==KLabel 'ConstrDecHead)
+    orBool (KL ==KLabel 'ConstrBody)*/
+//    orBool (KL ==KLabel 'AltConstrInv)
+//    orBool (KL ==KLabel 'SuperConstrInv)
+//    orBool (KL ==KLabel 'QSuperConstrInv)
+    /*orBool (KL ==KLabel 'StaticInit)
+    orBool (KL ==KLabel 'InstanceInit)*/
+    orBool (KL ==KLabel 'Empty)
+    orBool (KL ==KLabel 'Labeled)
+    orBool (KL ==KLabel 'ExprStm)
+    orBool (KL ==KLabel 'If)
+    orBool (KL ==KLabel 'AssertStm)
+    orBool (KL ==KLabel 'Switch)
+    orBool (KL ==KLabel 'SwitchBlock)
+    orBool (KL ==KLabel 'SwitchGroup)
+    orBool (KL ==KLabel 'Case)
+    orBool (KL ==KLabel 'Default) //default keyword from switch
+    orBool (KL ==KLabel 'While)
+    orBool (KL ==KLabel 'DoWhile)
+//    orBool (KL ==KLabel 'For)
+//    orBool (KL ==KLabel 'ForEach)
+    orBool (KL ==KLabel 'Break)
+    orBool (KL ==KLabel 'Continue)
+    orBool (KL ==KLabel 'Return)
+    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 'MethodDec)
+    orBool (KL ==KLabel 'MethodDecHead)
+    orBool (KL ==KLabel 'DeprMethodDecHead)
+    orBool (KL ==KLabel 'Void)
+    orBool (KL ==KLabel 'Param)
+    orBool (KL ==KLabel 'VarArityParam)
+    orBool (KL ==KLabel 'ThrowsDec) */
+    orBool (KL ==KLabel 'NoMethodBody)
+    orBool (KL ==KLabel 'ArrayInit)
+    /*orBool (KL ==KLabel 'Anno)
+    orBool (KL ==KLabel 'SingleElemAnno)
+    orBool (KL ==KLabel 'MarkerAnno)
+    orBool (KL ==KLabel 'ElemValPair)
+    orBool (KL ==KLabel 'ElemValArrayInit)
+    orBool (KL ==KLabel 'FieldDec)*/
+    orBool (KL ==KLabel 'VarDec)
+    orBool (KL ==KLabel 'ArrayVarDecId)
+    /*orBool (KL ==KLabel 'ClassDec)
+    orBool (KL ==KLabel 'ClassBody)
+    orBool (KL ==KLabel 'ClassDecHead)
+    orBool (KL ==KLabel 'SuperDec)
+    orBool (KL ==KLabel 'ImplementsDec)
+    orBool (KL ==KLabel 'CompilationUnit)
+    orBool (KL ==KLabel 'PackageName)*/
+
+    orBool (KL ==KLabel 'AmbName)
+//    orBool (KL ==KLabel 'TypeName)
+    orBool (KL ==KLabel 'ExprName)
+
+    orBool auxLabelInElab(KL)
+    orBool (KL ==KLabel 'MethodName)
+    /*orBool (KL ==KLabel 'PackageOrTypeName)
+    orBool (KL ==KLabel 'TypeArgs)
+    orBool (KL ==KLabel 'TypeArgs)
+    orBool (KL ==KLabel 'Wildcard)
+    orBool (KL ==KLabel 'WildcardUpperBound)
+    orBool (KL ==KLabel 'TypeParam)
+    orBool (KL ==KLabel 'TypeBound)
+    orBool (KL ==KLabel 'TypeParams)
+    orBool (KL ==KLabel 'ClassOrInterfaceType)
+    orBool (KL ==KLabel 'ClassType)
+    orBool (KL ==KLabel 'InterfaceType
+    orBool (KL ==KLabel 'Member)
+    orBool (KL ==KLabel 'TypeVar)
+    orBool (KL ==KLabel 'ArrayType)
+    orBool (KL ==KLabel 'Boolean)
+    orBool (KL ==KLabel 'Byte)
+    orBool (KL ==KLabel 'Short)
+    orBool (KL ==KLabel 'Int)
+    orBool (KL ==KLabel 'Long)
+    orBool (KL ==KLabel 'Char)
+    orBool (KL ==KLabel 'Float)
+    orBool (KL ==KLabel 'Double)
+    orBool (KL ==KLabel 'Null)
+    orBool (KL ==KLabel 'Bool)
+    orBool (KL ==KLabel 'True)
+    orBool (KL ==KLabel 'False)
+    orBool (KL ==KLabel 'Deci)
+    orBool (KL ==KLabel 'Hexa)
+    orBool (KL ==KLabel 'Octa)
+    orBool (KL ==KLabel 'Public)
+    orBool (KL ==KLabel 'Private)
+    orBool (KL ==KLabel 'Protected)
+    orBool (KL ==KLabel 'Abstract)
+    orBool (KL ==KLabel 'Final)
+    orBool (KL ==KLabel 'Static)
+    orBool (KL ==KLabel 'Native)
+    orBool (KL ==KLabel 'Transient)
+    orBool (KL ==KLabel 'Volatile)
+    orBool (KL ==KLabel 'StrictFP)
+    orBool (KL ==KLabel 'Id)*/
+
+syntax K ::= auxLabelInElab( KLabel ) [function]
+rule auxLabelInElab(KL:KLabel) =>
+           KL ==KLabel 'setEncloser`(_`,_`,_`)
+    orBool KL ==KLabel 'noValue
+    orBool KL ==KLabel 'noClass
+    orBool KL ==KLabel 'stmtAndExp`(_`,_`)
+    orBool KL ==KLabel 'toString`(_`)
+
 //@ Will not match .K - is not isElabNaked. (.K) is matched by [elabDotK].
 rule [unwrapElabNaked]:
     elab(K:K) => K
@@ -357,9 +571,10 @@ syntax K ::= "elabDispose" "(" K ")"
 rule [elabDisposeStartDefault]:
     elab(KL:KLabel(ElabResL:KList)) => elabDispose(KL(ElabResL))
 when
-            notBool customElabChildren(KL)
+            defaultElabChildren(KL)
+//            notBool customElabChildren(KL)
     andBool isElab(ElabResL)
-    andBool notBool isElabNaked(KL(ElabResL))
+//    andBool notBool isElabNaked(KL(ElabResL))
 
 rule [elabDisposeProcess]:
     elabDispose(KL:KLabel(_,, (elabRes(K:K) => K),, _))