Skip to content

Commit 2f5eee3

Browse files
denis-bogdanasdenis-bogdanas
committed
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.
1 parent ad0a942 commit 2f5eee3

10 files changed

+1473
-1426
lines changed

‎semantics/elaborate-blocks.k

Lines changed: 0 additions & 1418 deletions
This file was deleted.

‎semantics/elaboration-core.k

Lines changed: 528 additions & 0 deletions
Large diffs are not rendered by default.

‎semantics/elaboration-expressions.k

Lines changed: 573 additions & 0 deletions
Large diffs are not rendered by default.

‎semantics/elaboration-statements.k

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
require "core.k"
2+
require "elaboration-core.k"
3+
4+
module ELABORATION-STATEMENTS
5+
imports CORE
6+
imports ELABORATION-CORE
7+
8+
//@ Elaboration of blocks
9+
10+
rule [elabBlockHeat]:
11+
<k> elab('Block('ListWrap(Ks:KList))) => elab('ListWrap(Ks)) ~> elab('Block(CHOLE)) ...</k>
12+
<elabEnv> (. => ListItem(StEnvK)) ListItem(StEnvK:K) ...</elabEnv>
13+
<localTypes> (. => ListItem(LocTypesK)) ListItem(LocTypesK:K) ...</localTypes>
14+
15+
rule [elabForHeatFirstSubterm]:
16+
<k> (.=> elab(K)) ~> elab('For((K:K => CHOLE),, Ks:KList)) ...</k>
17+
<elabEnv> (. => ListItem(StEnvK)) ListItem(StEnvK:K) ...</elabEnv>
18+
<localTypes> (. => ListItem(LocTypesK)) ListItem(LocTypesK:K) ...</localTypes>
19+
when getKLabel(K) =/=KLabel 'elabRes`(_`)
20+
21+
rule [elabForHeatOtherSubterms]:
22+
(.=> elab(K)) ~> elab('For(_,, elabRes(_),, (K:K => CHOLE),, _))
23+
when getKLabel(K) =/=KLabel 'elabRes`(_`)
24+
25+
//@ HOLE is transformed into paramImpl
26+
context elab('Catch(HOLE,, _))
27+
when getKLabel(HOLE) =/=KLabel 'elabRes`(_`)
28+
29+
//@ Catch creates a new env layer and saves its argument.
30+
rule [elabCatch]:
31+
<k> elab('Catch(Param:KResult,, Body:K)) => elabParams(Param) ~> elab(Body) ~> elab('Catch(elabRes(Param),, CHOLE)) ...</k>
32+
<elabEnv> (. => ListItem(StEnvK)) ListItem(StEnvK:K) ...</elabEnv>
33+
<localTypes> (. => ListItem(LocTypesK)) ListItem(LocTypesK:K) ...</localTypes>
34+
35+
//here we need elabDispose because the block content is a list.
36+
//We could move the elabdospose logic to ListWrap instead of having it here.
37+
rule [elabDisposeBlockForOrCatch]:
38+
<k> elab(KL:KLabel(ElabResL:KList)) => removeLastElabEnv ~> elabDispose(KL(ElabResL)) ...</k>
39+
when
40+
isElab(ElabResL)
41+
andBool ((KL ==KLabel 'Block) orBool (KL ==KLabel 'For) orBool (KL ==KLabel 'Catch))
42+
43+
//@ Local var declarations desugaring
44+
45+
rule [LocalVarDecStmRed]:
46+
elab('LocalVarDecStm('LocalVarDec(Ks:KList))
47+
=> 'LocalVarDec(Ks)
48+
) [structural]
49+
50+
//@ Resolve the local var type, required to register the var in <elabEnv>
51+
context elab('LocalVarDec(_:K,, HOLE,, _:K))
52+
53+
rule [VarDecMultiDesugar]:
54+
elab('LocalVarDec(K:K,, T:Type,, 'ListWrap(Var1:K,, Var2:K,, VarDecs:KList))
55+
=> 'ListWrap('LocalVarDec(K,, T,, 'ListWrap(Var1)),,
56+
'LocalVarDec(K,, T,, 'ListWrap(Var2,, VarDecs)))
57+
) [structural]
58+
59+
rule [VarDecWithInitDesugar]:
60+
elab('LocalVarDec(K:K,, T:Type,, 'ListWrap('VarDec(X:Id,,InitExp:K)))
61+
=> 'ListWrap('LocalVarDec(K,, T,, 'ListWrap('VarDec(X:Id))),,
62+
'ExprStm('Assign('ExprName(X),, InitExp))))
63+
when
64+
getKLabel(InitExp) =/=KLabel 'ArrayInit [structural]
65+
66+
rule [elabLocalVarDec]:
67+
<k>
68+
elab('LocalVarDec(K:K,, T:Type,, 'ListWrap('VarDec(X:Id))))
69+
=> elabRes('LocalVarDec(K,, T,, 'ListWrap('VarDec(X))))
70+
...
71+
</k>
72+
<elabEnv> ListItem(stEnv((. => X |-> T) _)) ...</elabEnv>
73+
74+
//@\subsection{Elaboration of SuperConstrInv, AltConstrInv}
75+
76+
//@ Desugaring unqualified superclass constructor invocation into a qualified one
77+
rule [SuperConstrInv-desugar]:
78+
<k>
79+
(. => getElabResQThisSubclassOf(EnclosingClass, SubEnclosingClass))
80+
~> elab(
81+
'SuperConstrInv(K:K,, 'ListWrap( Args:KList ))
82+
=> 'QSuperConstrInv(
83+
CHOLE,,
84+
K,,
85+
'ListWrap(Args)
86+
)
87+
)
88+
...
89+
</k>
90+
<crntClass> Class:ClassType </crntClass>
91+
<class>
92+
<classType> Class </classType>
93+
<extends> SubClass:ClassType </extends>
94+
<enclosingClass> EnclosingClass:ClassType </enclosingClass>
95+
...
96+
</class>
97+
<class>
98+
<classType> SubClass </classType>
99+
<enclosingClass> SubEnclosingClass:ClassType </enclosingClass>
100+
...
101+
</class>
102+
103+
rule [QSuperConstrInv]:
104+
<k>
105+
elab(
106+
'QSuperConstrInv(Qual:K,, _,, 'ListWrap( Args:KList ))
107+
=> 'ListWrap(
108+
setEncloser('This(.KList), BaseClass, Qual),,
109+
'ExprStm('Invoke(
110+
'SuperMethod('None(.KList),, getConsName(BaseClass) ),,
111+
'ListWrap(Args)
112+
)),,
113+
IInit
114+
)
115+
)
116+
...
117+
</k>
118+
<crntClass> Class:ClassType </crntClass>
119+
<classType> Class </classType>
120+
<extends> BaseClass:ClassType </extends>
121+
<instanceInit> IInit:K </instanceInit>
122+
123+
rule [AltConstrInv]:
124+
<k>
125+
elab(
126+
'AltConstrInv(_,, 'ListWrap( Args:KList ))
127+
=> 'ExprStm('Invoke(
128+
'Method('MethodName( getConsName(Class) )),,
129+
'ListWrap(Args)
130+
))
131+
)
132+
...
133+
</k>
134+
<crntClass> Class:ClassType </crntClass>
135+
136+
endmodule

‎semantics/elaboration-top-blocks.k

Lines changed: 130 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,130 @@
1+
require "core.k"
2+
require "elaboration-core.k"
3+
4+
/*@ This module initialtes the elaboration phase. It is responsible for elaborating all top-level code blocks
5+
in the program: methods, constructors, static and instance initializers.
6+
*/
7+
module ELABORATION-TOP-BLOCKS
8+
imports CORE
9+
imports ELABORATION-CORE
10+
11+
rule [elaborateBlocksStart]:
12+
<k> . => elaborateBlocks(getTopLevelClasses) </k>
13+
<globalPhase> ProcClassMembersPhase => ElaborationPhase </globalPhase>
14+
15+
//@It is important to elaborate the instance initializers before the methods.
16+
//@This way, when 'SuperConstrEnv is encountered, it inserts the already elaborated instance
17+
//@initializer in its place, avoiding name collisions between constructor arguments and fields
18+
//@inside instance init.
19+
rule [elaborateBlocks]:
20+
<k>
21+
(. => elabInstanceInit ~> elabMethods(MethodDecs) ~> elabStaticInit
22+
~> elaborateBlocks(getInnerClasses(Class))
23+
)
24+
~> elaborateBlocks(setWrap((SetItem(Class:ClassType) => .) _:Set))
25+
...
26+
</k>
27+
<crntClass> _ => Class </crntClass>
28+
<classType> Class </classType>
29+
<methodDecs> MethodDecs:Map </methodDecs>
30+
31+
rule [elaborateBlocksDiscard]:
32+
elaborateBlocks(setWrap(.)) => .
33+
34+
rule [elabMethodsHeatMethodFirstLine]:
35+
<k>
36+
(. => addElabEnv ~> elabParams(Params) ~> elab(FirstLine))
37+
~> elabMethods( (Sig |-> _ => .Map) _)
38+
...
39+
</k>
40+
<crntClass> Class:ClassType </crntClass>
41+
<classType> Class </classType>
42+
<methodDecs>
43+
Sig:K |-> methodClosure(MClass:ClassType, 'ListWrap(Params:KList), CT:ContextType,_,_, (FirstLine:K => CHOLE), Body:K) :: MethodType:Type
44+
...
45+
</methodDecs>
46+
<contextType> _ => CT </contextType>
47+
48+
//@Required when processing first constructor line of Object, which is .K
49+
rule [elabDotK]:
50+
elab(.K) => elabRes(.K)
51+
52+
rule [elabMethodsHeatMethodBody]:
53+
<k>
54+
(elabRes(FirstLine:K) => elab(Body)) ~> elabMethods(_:Map)
55+
...
56+
</k>
57+
<crntClass> Class:ClassType </crntClass>
58+
<classType> Class </classType>
59+
<methodDecs>
60+
Sig:K |-> methodClosure(MClass:ClassType, 'ListWrap(Params:KList), _,_,_, CHOLE => FirstLine, Body:K => CHOLE) :: MethodType:Type
61+
...
62+
</methodDecs>
63+
64+
rule [elabMethodsCoolMethod]:
65+
<k>
66+
(elabRes(Body:K) => removeLastElabEnv) ~> elabMethods(_:Map)
67+
...
68+
</k>
69+
<crntClass> Class:ClassType </crntClass>
70+
<classType> Class </classType>
71+
<methodDecs>
72+
Sig:K |-> methodClosure(MClass:ClassType, 'ListWrap(Params:KList), _,_, methodRT, FirstLine:K, CHOLE => Body) :: MethodType:Type
73+
...
74+
</methodDecs>
75+
76+
rule [elabMethodsCoolConstructor]:
77+
<k>
78+
(elabRes(Body:K) => removeLastElabEnv) ~> elabMethods(_:Map)
79+
...
80+
</k>
81+
<crntClass> Class:ClassType </crntClass>
82+
<classType> Class </classType>
83+
<methodDecs>
84+
Sig:K |-> methodClosure(MClass:ClassType, 'ListWrap(Params:KList), _,_,
85+
constructorRT => methodRT,
86+
FirstLine:K => noValue,
87+
CHOLE => FirstLine ~> Body
88+
) :: MethodType:Type
89+
...
90+
</methodDecs>
91+
92+
rule [elabMethodsEnd]:
93+
elabMethods( .Map ) => .
94+
95+
rule [elabInstanceHeat]:
96+
<k> (. => addElabEnv ~> elab(K)) ~> elabInstanceInit ...</k>
97+
<crntClass> Class:ClassType </crntClass>
98+
<classType> Class </classType>
99+
<instanceInit> K:K => CHOLE </instanceInit>
100+
<contextType> _ => instanceCT </contextType>
101+
when K =/=K CHOLE
102+
103+
rule [elabInstanceEnd]:
104+
<k> elabRes(K:K) ~> elabInstanceInit => removeLastElabEnv ...</k>
105+
<crntClass> Class:ClassType </crntClass>
106+
<classType> Class </classType>
107+
<instanceInit> CHOLE => K </instanceInit>
108+
109+
rule [elabStaticHeat]:
110+
<k> (. => addElabEnv ~> elab(K)) ~> elabStaticInit ...</k>
111+
<crntClass> Class:ClassType </crntClass>
112+
<classType> Class </classType>
113+
<staticInit> K:K => CHOLE </staticInit>
114+
<contextType> _ => staticCT </contextType>
115+
when K =/=K CHOLE
116+
117+
rule [elabStaticEnd]:
118+
<k> elabRes(K:K) ~> elabStaticInit => removeLastElabEnv ...</k>
119+
<crntClass> Class:ClassType </crntClass>
120+
<classType> Class </classType>
121+
<staticInit> CHOLE => K </staticInit>
122+
123+
//@Adds a new empty layer to <elabEnv>
124+
syntax K ::= "addElabEnv"
125+
rule [addElabEnv]:
126+
<k> addElabEnv => . ...</k>
127+
<elabEnv> . => ListItem(stEnv(.Map)) ...</elabEnv>
128+
<localTypes> . => ListItem(stEnv(.Map)) ...</localTypes>
129+
130+
endmodule

‎semantics/elaboration-types.k

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
require "core.k"
2+
require "elaboration-core.k"
3+
4+
/*@ Elaboration of types and packages.
5+
*/
6+
module ELABORATION-TYPES
7+
imports CORE
8+
imports ELABORATION-CORE
9+
10+
/*@ \subsection{Elaboration of types} */
11+
12+
rule 'ClassOrInterfaceType(TypeK:K,, _) => TypeK [structural]
13+
rule 'InterfaceType(TypeK:K,, _) => TypeK [structural]
14+
rule 'ClassType(TypeK:K,, _) => TypeK [structural]
15+
16+
//@Resolving fully qualified type names A name pack.p2.A is represented as:
17+
//@ 'TypeName('PackageOrTypeName('PackageOrTypeName(pack),,p2),,A)
18+
19+
context 'PackageOrTypeName(HOLE,, _:K)
20+
21+
rule 'PackageOrTypeName(KRs:KList,, K:K) => 'TypeName(KRs,,K) ?? 'PackageName('ListWrap(KRs,,K))
22+
when isKResult(KRs) [structural]
23+
24+
//@When we search for a class qualified by another class, we simply convert
25+
//@the qualifier into a package.
26+
27+
context 'TypeName(HOLE,,_:Id)
28+
29+
rule [TypeNameQualifiedClass]:
30+
'TypeName(ClassQ:ClassType,, X:Id) => 'TypeName(toPackage(ClassQ),, X) [structural]
31+
32+
rule [TypeNameQualifiedPackage]:
33+
'TypeName(Pack:PackageId,, X:Id) => typeNameQualifiedImpl(getNamesMap(Pack), X) [structural]
34+
35+
//@Retrieves the ClassType for the given names map and simple class name
36+
syntax K ::= "typeNameQualifiedImpl" "(" K "," Id ")" [strict(1)]
37+
38+
rule [typeNameQualifiedImplFound]:
39+
typeNameQualifiedImpl(mapWrap(X |-> Class:ClassType _), X:Id) => Class
40+
41+
rule [typeNameQualifiedImplNotFound]:
42+
typeNameQualifiedImpl(mapWrap(NamesMap:Map), X:Id) => noValue
43+
when notBool X in keys(NamesMap)
44+
45+
//Elaboration the type String
46+
//@limitations:
47+
//@ - All string types should be referred by simple name "String".
48+
//@ Fully qualified name java.lang.String is not allowed.
49+
//@ - No other classes with name "String" are possible.
50+
rule [TypeNameString]:
51+
'TypeName(X:Id) => rtString
52+
when
53+
Id2String(X) ==String "String" [structural]
54+
55+
rule [TypeName-Local-in-any-Phase]:
56+
<k> 'TypeName(X:Id) => Class ...</k>
57+
<localTypes> ListItem(stEnv(X |-> Class:ClassType _)) ...</localTypes>
58+
59+
rule [TypeName-Global]:
60+
<k> 'TypeName(X:Id) => Class ...</k>
61+
<localTypes> ListItem(stEnv(LocalTypes:Map)) ...</localTypes>
62+
<crntClass> CrntClass:ClassType </crntClass>
63+
<classType> CrntClass </classType>
64+
<imports>... X |-> Class:ClassType ...</imports>
65+
when
66+
notBool X in keys(LocalTypes)
67+
68+
rule [TypeName-Global-Fail]:
69+
<k> 'TypeName(X:Id) => noValue ...</k>
70+
<localTypes> ListItem(stEnv(LocalTypes:Map)) ...</localTypes>
71+
<crntClass> CrntClass:ClassType </crntClass>
72+
<classType> CrntClass </classType>
73+
<imports> Imp:Map </imports>
74+
when
75+
notBool X in keys(LocalTypes) andBool notBool (X in keys(Imp))
76+
77+
//@ This two rules may only apply during processing of extends/implements clauses of top-level classes.
78+
//@ When the class whose declaration is processed is an inner class,
79+
//@ usual rules for 'TypeName apply.
80+
rule [TypeNameInProcClassDecsPhaseTop]:
81+
<k> 'TypeName(X:Id) => Class ...</k>
82+
<crntClass> noClass </crntClass>
83+
<compUnitImports>... X |-> Class:ClassType ...</compUnitImports>
84+
85+
rule [TypeNameInProcClassDecsPhaseTopFail]:
86+
<k> 'TypeName(X:Id) => noValue ...</k>
87+
<crntClass> noClass </crntClass>
88+
<compUnitImports> Imp:Map </compUnitImports>
89+
when
90+
notBool X in keys(Imp)
91+
92+
endmodule

‎semantics/expressions.k

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
require "core.k"
22
require "subtyping.k"
33
require "primitive-types.k"
4-
require "elaborate-blocks.k"
4+
require "elaboration-expressions.k"
55

66
//@ \section{Module EXPRESSIONS}
77

88
module EXPRESSIONS
99
imports CORE
1010
imports SUBTYPING
1111
imports PRIMITIVE-TYPES
12-
imports ELABORATE-BLOCKS //for "isCompoundAssignLabel
12+
imports ELABORATION-EXPRESSIONS //for "isCompoundAssignLabel
1313

1414
//Infix operators
1515
context /* || */'LazyOr(HOLE,,_)::_

0 commit comments

Comments
 (0)