Notice: this Wiki will be going read only early in 2024 and edits will no longer be possible. Please see: https://gitlab.eclipse.org/eclipsefdn/helpdesk/-/wikis/Wiki-shutdown-plan for the plan.
VIATRA2/Examples/VTCL/TypeChecking
Contents
Overview: Type checking
Type checking is introduced to the VTCL language in a backward compatible way. This means that any existing VTCL transformation should compile without modification. Moreover, it also implies that detailed type checking is only initiated if a type is defined explicitly for a variable (or an ASM function).
As the main extension of the language, one can add type information to
- all variables defined locally with the let rule
- a parameter of an ASM rule, graph pattern or graph transformation rule
- for the parameters and return values of ASM functions
Then the VIATRA2 parser checks if these variables are used in a type conformant way.
Typed variables within ASM rules
In ASM rules, types can be assigned to variables within the let rule with the following syntax VarName : TypeConst = InitValue. Here the type constant TypeConst should be a valid element of the model space, which can be resolved at compile time.
The following example demonstrates two typical type errors identified by the typechecker.
machine typechecking_errors { rule main() = let X : datatypes.Integer = 0, // Type error: Type incompatible initialization: expecting a term of type 'Integer' instead of 'String' Y : datatypes.Integer = "oops0" in seq { // Type error: operation '*' undefined for types ('Integer', 'String') update X = X * "oops1"; // Type error: type incompatible assignment: left value is of type 'Integer', right value is of type 'String' update X = X + "oops2"; // This is correct update X = X + 3; } }
In case of user defined ASM rules, types may be attached to symbolic parameters of the rule with the following syntax: Dir VarName : TypeConst where Dir denotes the direction of the parameter (i.e. it is either in, out or inout).
TODO: Maybe, the following example should not be a type error
rule calledAsmRule(in X: datatypes.Integer, out Y: datatypes.Double) = seq { update Y = 2 * X; } rule typecheck_asmrule() = let X : datatypes.Integer = 2, Y : datatypes.Integer = 0 in seq { // Type error: The type 'Integer' of actual parameter is not compatible with the type 'Double' of symbolic parameter 'Y'. // See the definition of 'calledAsmRule'. call calledAsmRule(X, Y); }
Typed variables in ASM functions
In case of ASM functions, types can be defined (separately) for each parameter (location) as well as for the return value with the following syntax:
asmfunction myFun (TypeConst1, TypeConst2) : ReturnTypeConst
machine typecheck_asmfun { asmfunction goals(datatypes.String) : datatypes.Integer { // Correct initialization ("Messi") = 3; // Type error (left value): type incompatible initialization: expecting a term of type 'String' instead of type 'Integer' // Type error (right value): type incompatible initialization: expecting a term of type 'Integer' instead of type 'String' (3) = "Giggs"; } rule main () = let X : datatypes.Integer = 0, Y : datatypes.String = "Giggs" in seq { // Correct assignment update X = goals("Messi"); // Type error: Type incompatible assignment: left value is of type 'String', right value is of type 'Integer' update Y = goals("Messi"); // Correct assignment update goals(Y) = 2; // Type error: Type incompatible initialization: expecting a term of type 'String' instead of type 'Integer' update goals(X) = 2; } }
Typed variables in graph patterns
In case of graph patterns, there are two kinds of type definitions for pattern variables:
- Types of symbolic parameters: This is defined similarly to the type definition in case of ASM rules, i.e. X: Class.
- Pattern body elements: the type of pattern variables defined within a pattern body is defined by the prefixing type constant. For instance, the type X in Class(X) is, obviously, Class.
The following situations are typechecked:
- a pattern is called with incompatible types (see find childPattern(P) below)
- the type of a pattern body element is incompatible with the type of the symbolic parameter (see X: Class and Classifier(X) below)
pattern myPattern(X: Class, Y: Classifier) = { // Type error for X: The type 'Classifier' of variable reference is not compatible with the type 'Class' of its definition. Classifier(X); // Type error for X: The type 'Classifier' of variable reference is not compatible with the type 'Class' of its definition. Element.ownedElement(OE1, P, X); Package(P); // The type 'Package' of actual parameter is not compatible with the type 'Classifier' of symbolic parameter 'A'. // See the definition of 'childPattern1'. find childPattern1(P); // The type 'Package' of actual parameter is not compatible with the type 'Class' of symbolic parameter 'A'. // See the definition of 'childPattern2'. find childPattern2(P); Element.ownedElement(OE2, P, Y); Class(Y); } pattern childPattern1(A: Classifier) = { Class(A); } pattern childPattern2(A) = { Class(A); }
Note that the type of a pattern variable is infered (if possible) from the local pattern body elements. Therefore, an error message is reported when calling childPattern2 with an incorrectly typed parameter P as the symbolic parameter A of childPattern2 is typed implicitly by the pattern body Class(A).
Error messages
The following error messages are issued by the type checker. Note that currently, these messages are classified as warnings!
- Operator '-' is undefined for the argument type ('datatypes.String'): issued when checking an ASM term
- Operator '*' is undefined for the argument types ('datatypes.String', 'datatypes.String'): issued when checking an ASM term
- The type 'uml2.metamodel.Classifier' of actual parameter is not compatible with the type 'uml2.metamodel.Class' of symbolic parameter 'C'. See the definition of 'myPattern' : issued when calling a graph pattern using the find construct
- The type 'uml2.metamodel.Classifier' of variable reference is not compatible with the type 'uml2.metamodel.Class' of its definition.: issued in ASM rules or in the body of graph patterns
- Type incompatible assignment: left value is of type 'datatypes.String', right value is of type 'datatypes.Integer' : issued in case of an update rule
- Type incompatible initialization: expecting a term of type 'datatypes.String' instead of 'datatypes.Integer' : issued when initializing an ASM function
--Varro.mit.bme.hu 11:02, 25 May 2009 (UTC)