KJ-16 Split elaboration module into a few smaller modules.

Split into 5 modules, although module ELABORATION-CORE contains approximately 40% of all that was elaboration before. We need to investigate whether parts of that module could be moved/ eliminated.

semantics/elaboration-statements.k

@@ -0,0 +1,136 @@
+require "core.k"
+require "elaboration-core.k"
+
+module ELABORATION-STATEMENTS
+    imports CORE
+    imports ELABORATION-CORE
+
+//@ Elaboration of blocks
+
+rule [elabBlockHeat]:
+    <k> elab('Block('ListWrap(Ks:KList))) => elab('ListWrap(Ks)) ~> elab('Block(CHOLE)) ...</k>
+    <elabEnv> (. => ListItem(StEnvK)) ListItem(StEnvK:K) ...</elabEnv>
+    <localTypes> (. => ListItem(LocTypesK)) ListItem(LocTypesK:K) ...</localTypes>
+
+rule [elabForHeatFirstSubterm]:
+    <k> (.=> elab(K)) ~> elab('For((K:K => CHOLE),, Ks:KList)) ...</k>
+    <elabEnv> (. => ListItem(StEnvK)) ListItem(StEnvK:K) ...</elabEnv>
+    <localTypes> (. => ListItem(LocTypesK)) ListItem(LocTypesK:K) ...</localTypes>
+when getKLabel(K) =/=KLabel 'elabRes`(_`)
+
+rule [elabForHeatOtherSubterms]:
+    (.=> elab(K)) ~> elab('For(_,, elabRes(_),, (K:K => CHOLE),, _))
+when getKLabel(K) =/=KLabel 'elabRes`(_`)
+
+//@ HOLE is transformed into paramImpl
+context elab('Catch(HOLE,, _))
+when getKLabel(HOLE) =/=KLabel 'elabRes`(_`)
+
+//@ Catch creates a new env layer and saves its argument.
+rule [elabCatch]:
+    <k> elab('Catch(Param:KResult,, Body:K)) => elabParams(Param) ~> elab(Body) ~> elab('Catch(elabRes(Param),, CHOLE)) ...</k>
+    <elabEnv> (. => ListItem(StEnvK)) ListItem(StEnvK:K) ...</elabEnv>
+    <localTypes> (. => ListItem(LocTypesK)) ListItem(LocTypesK:K) ...</localTypes>
+
+//here we need elabDispose because the block content is a list.
+//We could move the elabdospose logic to ListWrap instead of having it here.
+rule [elabDisposeBlockForOrCatch]:
+    <k> elab(KL:KLabel(ElabResL:KList)) => removeLastElabEnv ~> elabDispose(KL(ElabResL)) ...</k>
+when
+    isElab(ElabResL)
+    andBool ((KL ==KLabel 'Block) orBool (KL ==KLabel 'For) orBool (KL ==KLabel 'Catch))
+
+//@ Local var declarations desugaring
+
+rule [LocalVarDecStmRed]:
+    elab('LocalVarDecStm('LocalVarDec(Ks:KList))
+      => 'LocalVarDec(Ks)
+    )                                                   [structural]
+
+//@ Resolve the local var type, required to register the var in <elabEnv>
+context elab('LocalVarDec(_:K,, HOLE,, _:K))
+
+rule [VarDecMultiDesugar]:
+    elab('LocalVarDec(K:K,, T:Type,, 'ListWrap(Var1:K,, Var2:K,, VarDecs:KList))
+      => 'ListWrap('LocalVarDec(K,, T,, 'ListWrap(Var1)),,
+            'LocalVarDec(K,, T,, 'ListWrap(Var2,, VarDecs)))
+    )                                                   [structural]
+
+rule [VarDecWithInitDesugar]:
+    elab('LocalVarDec(K:K,, T:Type,, 'ListWrap('VarDec(X:Id,,InitExp:K)))
+    => 'ListWrap('LocalVarDec(K,, T,, 'ListWrap('VarDec(X:Id))),,
+        'ExprStm('Assign('ExprName(X),, InitExp))))
+when
+    getKLabel(InitExp) =/=KLabel 'ArrayInit             [structural]
+
+rule [elabLocalVarDec]:
+    <k>
+      elab('LocalVarDec(K:K,, T:Type,, 'ListWrap('VarDec(X:Id))))
+      => elabRes('LocalVarDec(K,, T,, 'ListWrap('VarDec(X))))
+      ...
+    </k>
+    <elabEnv> ListItem(stEnv((. => X |-> T) _)) ...</elabEnv>
+
+//@\subsection{Elaboration of SuperConstrInv, AltConstrInv}
+
+//@ Desugaring unqualified superclass constructor invocation into a qualified one
+rule [SuperConstrInv-desugar]:
+    <k>
+      (. => getElabResQThisSubclassOf(EnclosingClass, SubEnclosingClass))
+      ~> elab(
+        'SuperConstrInv(K:K,, 'ListWrap( Args:KList ))
+        =>  'QSuperConstrInv(
+              CHOLE,,
+              K,,
+              'ListWrap(Args)
+            )
+      )
+      ...
+    </k>
+    <crntClass> Class:ClassType </crntClass>
+    <class>
+      <classType> Class </classType>
+      <extends> SubClass:ClassType </extends>
+      <enclosingClass> EnclosingClass:ClassType </enclosingClass>
+      ...
+    </class>
+    <class>
+      <classType> SubClass </classType>
+      <enclosingClass> SubEnclosingClass:ClassType </enclosingClass>
+      ...
+    </class>
+
+rule [QSuperConstrInv]:
+    <k>
+      elab(
+        'QSuperConstrInv(Qual:K,, _,, 'ListWrap( Args:KList ))
+        => 'ListWrap(
+              setEncloser('This(.KList), BaseClass, Qual),,
+              'ExprStm('Invoke(
+                'SuperMethod('None(.KList),, getConsName(BaseClass) ),,
+                'ListWrap(Args)
+              )),,
+              IInit
+            )
+      )
+      ...
+    </k>
+    <crntClass> Class:ClassType </crntClass>
+    <classType> Class </classType>
+    <extends> BaseClass:ClassType </extends>
+    <instanceInit> IInit:K </instanceInit>
+
+rule [AltConstrInv]:
+    <k>
+      elab(
+        'AltConstrInv(_,, 'ListWrap( Args:KList ))
+        => 'ExprStm('Invoke(
+                  'Method('MethodName( getConsName(Class) )),,
+                  'ListWrap(Args)
+            ))
+      )
+      ...
+    </k>
+    <crntClass> Class:ClassType </crntClass>
+
+endmodule

semantics/elaboration-top-blocks.k

@@ -0,0 +1,130 @@
+require "core.k"
+require "elaboration-core.k"
+
+/*@ This module initialtes the elaboration phase. It is responsible for elaborating all top-level code blocks
+  in the program: methods, constructors, static and instance initializers.
+*/
+module ELABORATION-TOP-BLOCKS
+    imports CORE
+    imports ELABORATION-CORE
+
+rule [elaborateBlocksStart]:
+    <k> . => elaborateBlocks(getTopLevelClasses) </k>
+    <globalPhase> ProcClassMembersPhase => ElaborationPhase  </globalPhase>
+
+//@It is important to elaborate the instance initializers before the methods.
+//@This way, when 'SuperConstrEnv is encountered, it inserts the already elaborated instance
+//@initializer in its place, avoiding name collisions between constructor arguments and fields
+//@inside instance init.
+rule [elaborateBlocks]:
+    <k>
+      (. => elabInstanceInit ~> elabMethods(MethodDecs) ~> elabStaticInit
+        ~> elaborateBlocks(getInnerClasses(Class))
+      )
+      ~> elaborateBlocks(setWrap((SetItem(Class:ClassType) => .) _:Set))
+      ...
+    </k>
+    <crntClass> _ => Class </crntClass>
+    <classType> Class </classType>
+    <methodDecs> MethodDecs:Map </methodDecs>
+
+rule [elaborateBlocksDiscard]:
+    elaborateBlocks(setWrap(.)) => .
+
+rule [elabMethodsHeatMethodFirstLine]:
+    <k>
+      (. => addElabEnv ~> elabParams(Params) ~> elab(FirstLine))
+      ~> elabMethods( (Sig |-> _ => .Map) _)
+      ...
+    </k>
+    <crntClass> Class:ClassType </crntClass>
+    <classType> Class </classType>
+    <methodDecs>
+      Sig:K |-> methodClosure(MClass:ClassType, 'ListWrap(Params:KList), CT:ContextType,_,_, (FirstLine:K => CHOLE), Body:K) :: MethodType:Type
+      ...
+    </methodDecs>
+    <contextType> _ => CT </contextType>
+
+//@Required when processing first constructor line of Object, which is .K
+rule [elabDotK]:
+    elab(.K) => elabRes(.K)
+
+rule [elabMethodsHeatMethodBody]:
+    <k>
+      (elabRes(FirstLine:K) => elab(Body)) ~> elabMethods(_:Map)
+      ...
+    </k>
+    <crntClass> Class:ClassType </crntClass>
+    <classType> Class </classType>
+    <methodDecs>
+      Sig:K |-> methodClosure(MClass:ClassType, 'ListWrap(Params:KList), _,_,_, CHOLE => FirstLine, Body:K => CHOLE) :: MethodType:Type
+      ...
+    </methodDecs>
+
+rule [elabMethodsCoolMethod]:
+    <k>
+      (elabRes(Body:K) => removeLastElabEnv) ~> elabMethods(_:Map)
+      ...
+    </k>
+    <crntClass> Class:ClassType </crntClass>
+    <classType> Class </classType>
+    <methodDecs>
+      Sig:K |-> methodClosure(MClass:ClassType, 'ListWrap(Params:KList), _,_, methodRT, FirstLine:K, CHOLE => Body) :: MethodType:Type
+      ...
+    </methodDecs>
+
+rule [elabMethodsCoolConstructor]:
+    <k>
+      (elabRes(Body:K) => removeLastElabEnv) ~> elabMethods(_:Map)
+      ...
+    </k>
+    <crntClass> Class:ClassType </crntClass>
+    <classType> Class </classType>
+    <methodDecs>
+      Sig:K |-> methodClosure(MClass:ClassType, 'ListWrap(Params:KList), _,_,
+        constructorRT => methodRT,
+        FirstLine:K => noValue,
+        CHOLE => FirstLine ~> Body
+      ) :: MethodType:Type
+      ...
+    </methodDecs>
+
+rule [elabMethodsEnd]:
+    elabMethods( .Map ) => .
+
+rule [elabInstanceHeat]:
+    <k> (. => addElabEnv ~> elab(K)) ~> elabInstanceInit ...</k>
+    <crntClass> Class:ClassType </crntClass>
+    <classType> Class </classType>
+    <instanceInit> K:K => CHOLE </instanceInit>
+    <contextType> _ => instanceCT </contextType>
+when K =/=K CHOLE
+
+rule [elabInstanceEnd]:
+    <k> elabRes(K:K) ~> elabInstanceInit => removeLastElabEnv ...</k>
+    <crntClass> Class:ClassType </crntClass>
+    <classType> Class </classType>
+    <instanceInit> CHOLE => K </instanceInit>
+
+rule [elabStaticHeat]:
+    <k> (. => addElabEnv ~> elab(K)) ~> elabStaticInit ...</k>
+    <crntClass> Class:ClassType </crntClass>
+    <classType> Class </classType>
+    <staticInit> K:K => CHOLE </staticInit>
+    <contextType> _ => staticCT </contextType>
+when K =/=K CHOLE
+
+rule [elabStaticEnd]:
+    <k> elabRes(K:K) ~> elabStaticInit => removeLastElabEnv ...</k>
+    <crntClass> Class:ClassType </crntClass>
+    <classType> Class </classType>
+    <staticInit> CHOLE => K </staticInit>
+
+//@Adds a new empty layer to <elabEnv>
+syntax K ::= "addElabEnv"
+rule [addElabEnv]:
+    <k> addElabEnv => . ...</k>
+    <elabEnv> . => ListItem(stEnv(.Map)) ...</elabEnv>
+    <localTypes> . => ListItem(stEnv(.Map)) ...</localTypes>
+
+endmodule

semantics/elaboration-types.k

@@ -0,0 +1,92 @@
+require "core.k"
+require "elaboration-core.k"
+
+/*@ Elaboration of types and packages.
+*/
+module ELABORATION-TYPES
+    imports CORE
+    imports ELABORATION-CORE
+
+/*@ \subsection{Elaboration of types} */
+
+rule 'ClassOrInterfaceType(TypeK:K,, _) => TypeK [structural]
+rule 'InterfaceType(TypeK:K,, _) => TypeK        [structural]
+rule 'ClassType(TypeK:K,, _) => TypeK            [structural]
+
+//@Resolving fully qualified type names A name pack.p2.A is represented as:
+//@ 'TypeName('PackageOrTypeName('PackageOrTypeName(pack),,p2),,A)
+
+context 'PackageOrTypeName(HOLE,, _:K)
+
+rule 'PackageOrTypeName(KRs:KList,, K:K) => 'TypeName(KRs,,K) ?? 'PackageName('ListWrap(KRs,,K))
+when isKResult(KRs)                              [structural]
+
+//@When we search for a class qualified by another class, we simply convert
+//@the qualifier into a package.
+
+context 'TypeName(HOLE,,_:Id)
+
+rule [TypeNameQualifiedClass]:
+    'TypeName(ClassQ:ClassType,, X:Id) => 'TypeName(toPackage(ClassQ),, X)            [structural]
+
+rule [TypeNameQualifiedPackage]:
+    'TypeName(Pack:PackageId,, X:Id) => typeNameQualifiedImpl(getNamesMap(Pack), X)   [structural]
+
+//@Retrieves the ClassType for the given names map and simple class name
+syntax K ::= "typeNameQualifiedImpl" "(" K "," Id ")" [strict(1)]
+
+rule [typeNameQualifiedImplFound]:
+    typeNameQualifiedImpl(mapWrap(X |-> Class:ClassType _), X:Id) => Class
+
+rule [typeNameQualifiedImplNotFound]:
+    typeNameQualifiedImpl(mapWrap(NamesMap:Map), X:Id) => noValue
+when notBool X in keys(NamesMap)
+
+//Elaboration the type String
+//@limitations:
+//@ - All string types should be referred by simple name "String".
+//@    Fully qualified name java.lang.String is not allowed.
+//@ - No other classes with name "String" are possible.
+rule [TypeNameString]:
+    'TypeName(X:Id) => rtString
+when
+    Id2String(X) ==String "String"                      [structural]
+
+rule [TypeName-Local-in-any-Phase]:
+    <k> 'TypeName(X:Id) => Class ...</k>
+    <localTypes> ListItem(stEnv(X |-> Class:ClassType _)) ...</localTypes>
+
+rule [TypeName-Global]:
+    <k> 'TypeName(X:Id) => Class ...</k>
+    <localTypes> ListItem(stEnv(LocalTypes:Map)) ...</localTypes>
+    <crntClass> CrntClass:ClassType </crntClass>
+    <classType> CrntClass </classType>
+    <imports>... X |-> Class:ClassType ...</imports>
+when
+    notBool X in keys(LocalTypes)
+
+rule [TypeName-Global-Fail]:
+    <k> 'TypeName(X:Id) => noValue ...</k>
+    <localTypes> ListItem(stEnv(LocalTypes:Map)) ...</localTypes>
+    <crntClass> CrntClass:ClassType </crntClass>
+    <classType> CrntClass </classType>
+    <imports> Imp:Map </imports>
+when
+    notBool X in keys(LocalTypes) andBool notBool (X in keys(Imp))
+
+//@ This two rules may only apply during processing of extends/implements clauses of top-level classes.
+//@ When the class whose declaration is processed is an inner class,
+//@ usual rules for 'TypeName apply.
+rule [TypeNameInProcClassDecsPhaseTop]:
+    <k> 'TypeName(X:Id) => Class ...</k>
+    <crntClass> noClass </crntClass>
+    <compUnitImports>... X |-> Class:ClassType ...</compUnitImports>
+
+rule [TypeNameInProcClassDecsPhaseTopFail]:
+    <k> 'TypeName(X:Id) => noValue ...</k>
+    <crntClass> noClass </crntClass>
+    <compUnitImports> Imp:Map </compUnitImports>
+when
+    notBool X in keys(Imp)
+
+endmodule

semantics/expressions.k

@@ -1,15 +1,15 @@
 require "core.k"
 require "subtyping.k"
 require "primitive-types.k"
-require "elaborate-blocks.k"
+require "elaboration-expressions.k"
 
 //@ \section{Module EXPRESSIONS}
 
 module EXPRESSIONS
     imports CORE
     imports SUBTYPING
     imports PRIMITIVE-TYPES
-    imports ELABORATE-BLOCKS //for "isCompoundAssignLabel
+    imports ELABORATION-EXPRESSIONS //for "isCompoundAssignLabel
 
 //Infix operators
 context /* ||  */'LazyOr(HOLE,,_)::_