-
Notifications
You must be signed in to change notification settings - Fork 25
Language Extensions
In addition to contributing new plugins to Overture, you can also extend the VDM language itself. For language-based extensions there are multiple steps that are common to all extensions. These consist of actually getting your extended language to show up in the tool so you can then use it. This guide will help you do that.
Essentially, you have to:
- Add the definitions of your extension to the VDM grammar
- Add the new nodes to the AST
- Extend the parser to construct your new definitions
- Extend the type checker to validate the definitions
Let's go through each of the above steps in detail. As an example, we'll add a new element to the language: a rely condition (keyword rely). This condition applies only to operations and has the same syntax as a post condition. Its use is related to concurrency (it describes the assumptions an operation can make
about the environment in concurrent executions) but that's not terribly important right now.
The VDM grammar is defined in the language manual (can be found in the documentation folder and also ships with the Overture). If you are extending the language, it's nice to define how exactly the extension looks like. It's enough to do this as a note. Simply copy the affected grammar and add your changes in bold. If you add entire new definitions to the grammar, add them in regular font.
Here are the operation definitions, extended with the new rely condition:
explicit operation definition = identifier, ':', operation type, identifier, parameters, '==', operation body, [ 'pre', expression ], ['rely', expression], [ 'post', expression ] ; implicit operation body = [ externals ], [ 'pre', expression ], ['rely', expression], 'post', expression, [ exceptions ] ;
Now that we know how our new extension affects the grammar, we can begin to implement it in the tool. The first step is to add it to the AST specification file. The details of how the specification file is defined are beyond this guide. We will simply locate the appropriate nodes (in this case, operation definitions) and add the new fields.
First, we add them to the explicit operation definition:
#Operation {-> package='org.overture.ast.definitions'
| [body]:stm
| [precondition]:exp
| [postcondition]:exp
| [relycondition]:exp
| (predef):definition.#Function.explicit
| (relydef):definition.#Function.explicit
| (guardef):definition.#Function.explicit
| (state):definition.state
| (actualResult):type
| [isConstructor]:java_Boolean
= {explicit}
[parameterPatterns]:pattern*
(paramDefinitions):definition*
(...)
| {implicit}
Implicit operations are constructed using the specification statement so we will also have to add the rely condition to it:
stm {-> package='org.overture.ast.statements'
| [location]:location
| (type):type}
=
(...)
| {specification}
[externals]:clause.external*
[precondition]:exp
[postcondition]:exp
[relycondition]:exp
(...)
;
After this is done, we need to run mvn clean install in root/core/ so
that a new AST is generated with the rely condition present in explicit and
implicit operations.
The final step is to update the AST factory in
core/ast/src/main/java/org/overture/ast/factory/AstFactory.java so that it
can construct the new versions of the nodes.
Below, you can see the new version of the method for creating explicit operation definitions. Note that it already receives the rely condition as an expression. The parser will be extended to construct that.
public static AExplicitOperationDefinition newAExplicitOperationDefinition(
ILexNameToken name, AOperationType type, List<PPattern> parameters,
PExp precondition, PExp postcondition, PExp relyCondition, PStm body)
{
AExplicitOperationDefinition result = new AExplicitOperationDefinition();
initDefinition(result, Pass.DEFS, name.getLocation(), name, NameScope.GLOBAL);
result.setType(type);
result.setParameterPatterns(parameters);
result.setPrecondition(precondition);
result.setPostcondition(postcondition);
// new rely condition
result.setRelycondition(relyCondition);
result.setBody(body);
result.setIsConstructor(false);
return result;
}We must do a similar change to the newASpecificationStm(...) method since
that is the other AST node we changed.
Now that we have our AST nodes and the factory methods to create them, we need to change the parser so it recognizes the new rely condition and calls the new version of the factory method.
Since we added a new keyword, the first thing we should do is add it to the
list of recognized tokens. This is done by editing the
core/ast/src/main/java/org/overture/ast/lex/VDMToken.java file. It's just a
big enum so we add the new entry like so:
RELY("rely","rely",VDM_SL)
RELY is the name of our enum entry. The first "rely" indicates that it's a
keyword and what that keyword is. The second "rely" is the token that is read and the third entry
is the VDM dialect where the keyword can be used. For comparison, the plus token is PLUS(null, "+", VDM_SL, VDM_PP, VDM_RT).
Now the lexer will recognize rely as a keyword. All that's left to do is
change the parser. Since we made changes to definitions, we need to edit
the definition reader:
core/parser/src/main/java/org/overture/parser/syntax/DefinitionReader.java.
In this case, we edit the readExplicitOperationDefinition(...) method. It's
quite large so we won't reprint it all here. However, the order is important.
We have defined above that the rely condition comes after the post condition
and before the pre condition.
So, in the definition reader, after the code chunk that parses pre conditions and before the code chunk that parses post conditions, we add the new code for rely condition:
//...
if (lastToken().is(VDMToken.PRE))
{
nextToken();
precondition = getExpressionReader().readExpression();
}
PExp relyCondition = null;
if (lastToken().is(VDMToken.RELY))
{
nextToken();
relyCondition = getExpressionReader().readExpression();
}
if (lastToken().is(VDMToken.POST))
{
nextToken();
postcondition = getExpressionReader().readExpression();
}
//...
return AstFactory.newAExplicitOperationDefinition(idToName(funcName), type, parameters, precondition, postcondition, relyCondition, body);Once again, a similar process needs to be done for specification statements by
editing the readSpecification(...) method.
And that's it! Now, we did make it very easy on ourselves by making the rely condition the same as a post condition so the parse code is virtually the same.
But many extensions will be along these lines. A new keyword and then some existing construct, whether it's an expression, a statement or something else. If your language extension is something much more complex then you will have to handwrite the new parser code for it.
Now that the parser produces our new definitions, we need the type checker to type check them. This step will mostly likely vary a bit between extensions. But the general principle will always be the same. We need to add code to the type checker so that it visits and checks the nodes for the language extension. If the extension is just a new field in an existing node, it be easier. If it's an entirely new node, then you will have to add some more code, including possibly one or more visitor cases.
Our specific extension consists of a new field in operation definitions so
we will only need to change existing methods. We begin by looking at the
definition visitor in the type checker:
core/typechecker/src/.../typechecker/visitor/TypeCheckerDefinitionVisitor.java.
The case we are interested in is caseAExplicitOperationDefinition(...). It
is very large but we only need to make some small changes. Unlike the parser,
the order does not have to be so precise since we are working on a structured
data type (it makes no difference whether you type check the rely condition
before or after the post condition, for example).
It is only important that we type check our condition after the operation parameters have been type checked and added to the environment since the parameters can show up in the rely condition. Thus, we will type check the rely condition after the post condition. We add the following code to the method mentioned above:
// ...
// (end of) Post condition type check
if (!question.assistantFactory.createPTypeAssistant().isType(b, ABooleanBasicType.class))
{
TypeCheckerErrors.report(3018, "Postcondition returns unexpected type", node.getLocation(), node);
TypeCheckerErrors.detail2("Actual", b, "Expected", expected);
}
}
// Rely condition type check
if (node.getRelydef() != null)
{
FlatEnvironment rely = new FlatEnvironment(question.assistantFactory, new Vector<PDefinition>(), local);
rely.setEnclosingDefinition(node.getRelydef());
PType b = node.getRelydef().getBody().apply(THIS, new TypeCheckInfo(question.assistantFactory, rely, NameScope.NAMESANDANYSTATE));
ABooleanBasicType expected = AstFactory.newABooleanBasicType(node.getLocation());
if (!question.assistantFactory.createPTypeAssistant().isType(b, ABooleanBasicType.class))
{
TypeCheckerErrors.report(3018, "Rely-condition returns unexpected type", node.getLocation(), node);
TypeCheckerErrors.detail2("Actual", b, "Expected", expected);
}
}
// ...The code we just added is essentially the same as the one that type checks post conditions. Basically, it sets up a new environement for the rely condition and type checks it. The condition must be a predicate and so we also check that the type produced by type checking the condition is a boolean.
However, if you make these changes and try to type check a specification with a
rely condition, it will not work. This is because the initial check of
node.getRelydef() !=null will always be false. The rely definition is not there.
Even though we already changed the parser.
The reason for this is something called implicitly defined functions. Whenever a model
defines a pre/post or a rely condition for an operation, it also implicitly defines
a function called pre_op/post_op/rely_op. This function is used for quoting these conditions elsewhere in the model.
The parser does not create these special implicit definitions. This is done during the type check process in an initial phase called implicit definitions. We need to extend that part of the type checker so that it also creates a definition for the rely condition..
The type checker constructs the implicit definitions in the implicit definition
finder class:
core/typechecker/src/.../typechecker/utilities/ImplicitDefinitionFinder.java.
This is a visitor so we look at caseAExplicitOperationDefinition(...).
Once again, we can draw inspiration from what's done for post conditions:
// ...
// Post condition implicit definition construction
if (node.getPostcondition() != null)
{
node.setPostdef(af.createAExplicitOperationDefinitionAssistant().getPostDefinition(node, question));
af.createPDefinitionAssistant().markUsed(node.getPostdef());
}
// Rely condition implicit definition construction
if (node.getRelycondition() != null)
{
node.setRelydef(af.createSOPerationDefinitionAssistant().getRelyDefinition(node, question));
af.createPDefinitionAssistant().markUsed(node.getRelydef());
}
//...This code just checks if the rely condition is present (remember, this one is
set by the parser) and it is, calls an assistant that constructs the definition
for the rely_op function. It then sets the function and marks it as used.
We won't go into detail of how the assistant creates these implicit
definitions. There is a common method that constructs all implicit definitions
and we just the name of each of them depending on what we want (also, pre_op
does not have the after state or the result as parameters).
At this point, we are finally done. If we try to parse and TC a model with our
new extension it should go smoothly. Now that we have the extension in the AST,
it's time to use it for something. If the extension requires evaluation, that's done in the interpreter module and that is also implemented as a visitor so
it should be possible to take from here.
After we've added the new nodes to the AST specification file, we can
make toString() methods for them (very useful for debugging).
This is done by editing the
core/ast/src/main/java/ast/util/ToStringUtil.java and
core/ast/src/main/resources/overtureII.astv2.tostring files. For reference, he
is the entry for the rely condition:
Throughout this work, the changes we make are bound to introduce Java type errors in the code base. For example, when we change the factory methods, we will have a few errors in the places where the methods are called. In general, it's best to fix any errors right away, before proceeding to the next step.
Fully testing a new extension may be complex and depends on what exactly the extension is meant to do. However, we can easily test if these changes are being done correctly by writing a small test that takes a very simple model with the new language extension and calls the parser and type checker on it. If nothing breaks, we're on the right track.
Most of this guide was written off work done to extend Overture with rely
and guarantee conditions. If you check out the branch ldc/argog you can see
most of this done on the actual code base. It starts at commit #9842056. Keep in mind
that it is neither as simple nor as well-ordered as what this guide presents.
On an absolutely final note, since this has run very long, if you want your language extension to become an official part of VDM, there is a formal process to submit language modification requests. This is handled by our friends at the VDM language board.