Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for ADTs in Viper #574

Merged
merged 56 commits into from
May 18, 2022
Merged
Changes from 1 commit
Commits
Show all changes
56 commits
Select commit Hold shift + click to select a range
8cf2805
Implement PAST nodes for ADT Declaration
amaissen Feb 25, 2022
a726400
Add AST nodes for ADT Declaration
amaissen Feb 25, 2022
8084def
Implement translation of ADT declaration and ADT constructors to AST …
amaissen Feb 25, 2022
a3d5c7a
Extend PAST with a new type for ADT's
amaissen Feb 25, 2022
e0d78f6
Properly implement the method withChildren for PAdtConstructor
amaissen Feb 25, 2022
c358505
Translate PDomainType to PAdtType if necessary
amaissen Feb 25, 2022
48326cd
Implement type-checking for ADT declaration, ADT constructors and ADT…
amaissen Feb 25, 2022
9fc8bee
Add an AST node for the ADT type
amaissen Feb 25, 2022
20b0ab9
Enhance PrettyPrinter
amaissen Feb 24, 2022
cbcd1d0
Change order of member signature translation
amaissen Feb 24, 2022
01e67e2
Add prettyPrinting for extension AST nodes
amaissen Feb 25, 2022
e9737c4
Finalize translation of PAST nodes to AST nodes for ADT declarations
amaissen Feb 25, 2022
9e193c2
Resolve TODO
amaissen Feb 25, 2022
7e4bb7a
Implement method withChildren for AdtConstructor and AdtType
amaissen Mar 2, 2022
1952c7f
Fix issue in rewriting strategy
amaissen Mar 2, 2022
ecaf1c6
Resolve TODO
amaissen Mar 2, 2022
72cb46a
Created a new class for the AdtEncoder
amaissen Mar 2, 2022
22a56b9
Use the AdtEncoder
amaissen Mar 2, 2022
c960afc
Add a PAST node for an ADT constructor call
amaissen Mar 3, 2022
ff73fe5
Add return type to AdtConstructor
amaissen Mar 4, 2022
5faa7c0
Add an AST node for an ADT constructor application
amaissen Mar 4, 2022
9476942
Fix type checking for constructor call and add implement transaltion
amaissen Mar 4, 2022
2245302
Add an AdtNameManager
amaissen Mar 11, 2022
a5b0856
Finalize main encoding of ADTs as domain functions
amaissen Mar 11, 2022
2432860
The type variable mapping should be set if there are type variables
amaissen Mar 11, 2022
ac8429c
Extend ADT type checker
amaissen Mar 11, 2022
d3146c3
Enable ADT constructor calls
amaissen Mar 16, 2022
e118d57
Merge branch 'amaissen/adjust-plugin-infrastructure' into add-adt-pas…
amaissen Mar 16, 2022
051999e
Merge branch 'amaissen/fix-plugin-infrastructure-in-resolver' into ad…
amaissen Mar 16, 2022
a0b4f57
Merge branch 'amaissen/fix-strategy-builder' into add-adt-past-extension
amaissen Mar 16, 2022
7c1f171
Adjust to updated plugin infrastructure
amaissen Mar 16, 2022
9b85472
Prepare for adding destructors
amaissen Mar 16, 2022
035c321
Add an AST node for a destructor application
amaissen Mar 16, 2022
5ea759c
Add encoding for ADT destructor calls
amaissen Mar 16, 2022
09b3cdd
Add a Parser AST node for destructor calls and implement typechecking
amaissen Mar 16, 2022
eb28ae3
Enable destructor calls
amaissen Mar 16, 2022
ee6ca75
Add an AST node for an adt discriminator application
amaissen Mar 17, 2022
6e42ce7
Add encoding for adt discriminator applications
amaissen Mar 17, 2022
be46785
Add parser AST node for adt discriminator call
amaissen Mar 17, 2022
df6af71
Merge branch 'master' into add-adt-extension
amaissen Mar 21, 2022
3cf21ed
Fix issue in resolving constructor calls with wrong number of arguments
amaissen Mar 21, 2022
8a2530e
Fix issue in tag axiom
amaissen Mar 22, 2022
9ba76b8
Fix issue in AdtNameManager
amaissen Mar 22, 2022
71b1c4d
Fix issue in resolving discriminator calls
amaissen Mar 22, 2022
a761dcb
Fix the discriminator syntax and its parsing
amaissen Mar 29, 2022
4fd759e
Add test resources for adt plugin
amaissen Mar 29, 2022
cacd64b
Add contains function for ADTs
amaissen Mar 31, 2022
558cbb0
Implement Syntax for Deriving System
amaissen Apr 11, 2022
e83d75b
Merge branch 'viperproject:master' into add-adt-extension
amaissen Apr 11, 2022
993e2a3
Fix small issue in syntax for deriving functions
amaissen Apr 12, 2022
5120fa9
Add test for deriving system and derivable contains function
amaissen Apr 12, 2022
8de12f3
Minor changes in ADT constructor argument handling
amaissen Apr 12, 2022
f55e455
Make the ADT plugin a default plugin
amaissen Apr 25, 2022
1ce41ce
Merge pull request #1 from amaissen/add-adt-extension
amaissen Apr 25, 2022
4e4d861
Fix the plugin tests
amaissen Apr 26, 2022
81b2a02
Fix some whitespace and formatting issues
amaissen Apr 26, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Properly implement the method withChildren for PAdtConstructor
-As for PDomainFunction we have to make some adaptions to the method withChildren such that it can properly be used. (e.g needed if we use some StrategyBuilder)
-Basically we have to make sure that 'adtName' is handled correctly
-Currently, the only way it works, is with the Reflection approach. A simplified implementation is desired and provided in a later step
  • Loading branch information
amaissen committed Mar 11, 2022
commit e0d78f65ea7c174f26600c451d7b448f45675724
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,11 @@
package viper.silver.plugin.standard.adt

import viper.silver.ast.{Member, NoInfo, NoPosition, Position, TypeVar}
import viper.silver.parser.Transformer.ParseTreeDuplicationError
import viper.silver.parser.{NameAnalyser, PAnyFormalArgDecl, PExtender, PGenericType, PGlobalDeclaration, PIdentifier, PIdnDef, PIdnUse, PMember, PNode, PType, PTypeSubstitution, PTypeVarDecl, Translator, TypeChecker}
import viper.silver.plugin.standard.adt.PAdtConstructor.findAdtConstructor

import scala.reflect.runtime.{universe => reflection}

case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[PAdtConstructor])(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration {

Expand Down Expand Up @@ -61,6 +63,50 @@ case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])(
override def translateMember(t: Translator): Member = {
findAdtConstructor(idndef, t)
}

override def withChildren(children: Seq[Any], pos: Option[(Position, Position)] = None, forceRewrite: Boolean = false): this.type = {
if (!forceRewrite && this.children == children && pos.isEmpty)
this
else {

// TODO: Why can we not simplify with following code? => results in an Exception, is reflection really the only way?
/*
val first = children.head.asInstanceOf[PIdnDef]
val others = children.tail.asInstanceOf[Seq[PAnyFormalArgDecl]]


PAdtConstructor(first, others)(this.adtName)(pos.getOrElse(this.pos)).asInstanceOf[this.type]
*/

// Infer constructor from type
val mirror = reflection.runtimeMirror(reflection.getClass.getClassLoader)
val instanceMirror = mirror.reflect(this)
val classSymbol = instanceMirror.symbol
val classMirror = mirror.reflectClass(classSymbol)
val constructorSymbol = instanceMirror.symbol.primaryConstructor.asMethod
val constructorMirror = classMirror.reflectConstructor(constructorSymbol)

// Add additional arguments to constructor call, besides children
val firstArgList = children
var secondArgList = Seq.empty[Any]

this match {
case pd: PAdtConstructor => secondArgList = Seq(pd.adtName) ++ Seq(pos.getOrElse(pd.pos))
case _ =>
}

// Call constructor
val newNode = try {
constructorMirror(firstArgList ++ secondArgList: _*)
}
catch {
case _: Exception if this.isInstanceOf[PNode] =>
throw ParseTreeDuplicationError(this.asInstanceOf[PNode], children)
}

newNode.asInstanceOf[this.type]
}
}
}

object PAdtConstructor {
Expand Down