Parsing and type-checking generics #671

koflin · 2023-08-24T18:30:39Z

These are my changes to support parsing and type-checking generics.

- generated gobra parser code - added Ast nodes for type parameters and type arguments - modified parse tree translator

- modified parser and parse tree translator accordingly - implemented ambiguity resolution for indexed expression (normal index expression or type arguments)

- add tests - fix some issues in the parse tree translator and the pretty printer

… underlying type of type parameters

This reverts commit 3725a9b.

koflin · 2023-08-24T18:54:24Z

@Felalolf

These are the merged changes.

First of all, the unit tests fail because of an issue I already mentioned. It has to do with this PR (#634) It somehow breaks some of my unit tests. It always complains that
Logic error: Expected that package pkg has access to the type information of package BuiltInImport
I believe that replacing new TypeInfoImpl(tree, context)(config) with new TypeInfoImpl(tree, Map.empty)(config) in the ExprTypingUnitTests.scala causes this issue. I don't know how to fix this.

Second, the GobraTests of the integration suit is stuck. I also don't know what the issue is here. Before merging everything worked fine.

Note that before the merge with the current master everything was working fine which can be seen here: https://github.com/koflin/gobra/tree/generics-before-merge.

Felalolf

Some comments

Felalolf · 2023-08-24T19:12:51Z

src/main/antlr4/.antlr/GoLexer.java

@@ -0,0 +1,606 @@
+// Generated from s:\GitHub\gobra\src\main\antlr4\GoLexer.g4 by ANTLR 4.9.2


Remove this file

Felalolf · 2023-08-24T19:26:06Z

src/main/scala/viper/gobra/frontend/Desugar.scala

@@ -2775,6 +2780,7 @@ object Desugar extends LazyLogging {
              for {
                dArgs <- sequence(args.map { x => option(x.map(exprD(ctx, info)(_))) })
                idT = info.typ(base) match {
+                  // TODO handle this


handle what? please make the comment more concrete.

It was a comment for myself, I'll remove it

Felalolf · 2023-08-24T19:30:34Z

src/main/scala/viper/gobra/frontend/info/implementation/property/UnderlyingType.scala

@@ -22,6 +22,7 @@ trait UnderlyingType { this: TypeInfoImpl =>
  lazy val underlyingType: Type => Type =
    attr[Type, Type] {
      case Single(DeclaredT(t: PTypeDecl, context: ExternalTypeInfo)) => underlyingType(context.symbType(t.right))
+      case Single(TypeParameterT(_, t: PInterfaceType, ctx)) => underlyingType(ctx.symbType(t))


this looks as if the underlying type of a type parameter is the underlying type of its constraint. Is this intended? Why is this correct?

Yes, the underlying type of a type parameter is the underlying type of its type constraint (interface) https://go.dev/ref/spec#Underlying_types

then please add a comment

Felalolf · 2023-08-24T19:31:13Z

src/main/scala/viper/gobra/frontend/info/implementation/property/UnderlyingType.scala

      case _ => false
    }
  }
+
+  def isTypeParameter(t: Type): Boolean = t match {
+    case TypeParameterT(_, _, _) => true


Suggested change

case TypeParameterT(_, _, _) => true

case _: TypeParameterT => true

Felalolf · 2023-08-24T19:32:07Z

src/main/scala/viper/gobra/frontend/info/implementation/resolution/AmbiguityResolution.scala

@@ -35,6 +35,9 @@ trait AmbiguityResolution { this: TypeInfoImpl =>
              case _ => Left(n)
            })

+      case n: PIndexedExp =>
+        if (exprOrType(n.base).isLeft) Left(n) else Right(n)


add a comment

Felalolf · 2023-08-24T20:23:55Z

src/main/scala/viper/gobra/frontend/info/base/Type.scala

+    override def withChildren(children: Seq[Any], pos: Option[(Position, Position)], forceRewrite: Boolean): this.type = {
+      assert(pos.isEmpty, "The pos argument must be set to nil if called on Gobra nodes.")
+
+      if (!forceRewrite && this.children == children) {
+        this
+      } else {
+        create(children)
+      }
+    }
+
+    private def create(children: Seq[Any]): this.type = {
+      import scala.reflect.runtime.{universe => reflection}
+      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)
+
+      // Call constructor
+      val newNode = constructorMirror(children: _*)
+      newNode.asInstanceOf[this.type]
+    }


Why is this necessary?

viper.gobra.ast.internal.Node needs this to work correctly. It is taken from viper.gobra.ast.internal.Rewritable and modified slightly

Felalolf · 2023-08-24T20:26:12Z

src/main/scala/viper/gobra/frontend/info/implementation/resolution/TypeSet.scala

+import scala.annotation.tailrec
+sealed trait TypeSet
+
+object TypeSet {


add more documentation

I mean for the entire file

yes, sorry. I forgot this one

Felalolf · 2023-08-24T20:27:38Z

src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala

@@ -160,6 +166,29 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl =>

        case _ => violation(s"expected type, but got $n")
      }
+
+    case n: PIndexedExp =>
+      resolve(n) match {


also deal with unexpected matches (via violation).

Felalolf · 2023-08-24T20:34:53Z

src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala

+              val typeMap = f.args.filter(isTypeParameter).zip(fc.args.map(exprType)).map {
+                case (TypeParameterT(id, _, _), typ) => (PIdnDef(id.name), typ)
+              }.toMap[PIdnDef, Type]


I am not sure this is correct. If only the second argument is a type parameter, would you then not zip the second parameter with the first argument?

yes you are right, I'll correct this

Felalolf · 2023-08-24T20:38:08Z

src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala

+                    val typeMap = args.filter(isTypeParameter).zip(argTypes).map {
+                      case (TypeParameterT(id, _, _), typ) => (PIdnDef(id.name), typ)
+                    }.toMap[PIdnDef, Type]


please refactor the type inference into a separate method

koflin added 30 commits April 23, 2023 21:08

add support for parsing generic types and functions

72adaf1

add support for parsing generic types and functions

caea3b6

Merge branch 'generics' of https://github.com/koflin/gobra into generics

4f5555b

modified parse tree translator

a90ed72

- generated gobra parser code - added Ast nodes for type parameters and type arguments - modified parse tree translator

changed typeArgument rule to index instead

2917a1a

- modified parser and parse tree translator accordingly - implemented ambiguity resolution for indexed expression (normal index expression or type arguments)

fix a few things such that compilation can succeed

b1f7878

add some tests for generics

864e185

- add tests - fix some issues in the parse tree translator and the pretty printer

started expression typing

f822f7f

expression typing of generic function instantiation working

e8c0846

implement parse tree translator for instantiated generic types

e9c0878

implement typing of generic types

6b10b39

add first prototype of assignability

7971b35

implement assignability with type parameters

1159896

changed type constraint to be an interface

ca0c310

handle expression typing of integer constants properly

c0b00aa

embed non interface type constraints into interfaces

4253b7e

implemented satisfiability, comparability, identity, type merging and…

4139ed6

… underlying type of type parameters

implement generic type instantiation with PIndexedExp

4aa1b02

add fact test

04836b0

implement simple Go type inference

162b257

adjust GhostErasureUnitTest

b00f8fb

Trigger CI/CD

1ed090d

[skip ci] remove lost line

1ed4471

fix bug introduced in ghost assignability

9e21e21

fix printing of types

26e627c

fix type inference

30fe086

Add type parameters to the desugar

ee2cf0a

added some tests from master

d9f6eed

remove change to be consistent with master

3725a9b

Revert "remove change to be consistent with master"

d0fd09a

This reverts commit 3725a9b.

koflin added 5 commits August 24, 2023 19:35

clean up some stuff

91da1d2

Merge branch 'generics-before-merge' into generics-merged

79dd96f

regenerate parser after merge

a13e324

add dependency

ecfd59e

adapted member typing unit test

4bf94a5

Felalolf reviewed Aug 24, 2023

View reviewed changes

koflin added 4 commits August 25, 2023 01:27

fix type parameter inference and refactor

fc874a6

make parameterizable stateless

aa375f8

unapplied type args

f537564

document type set, underlying type and rename syntaxImplements

b11a8d8

This was referenced Apr 29, 2024

Replace monomorphised examples and exercises with generic versions viperproject/program-proofs-gobra#11

Open

Replace "monomorphised" lemmas with generic versions viperproject/gobra-libs#17

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Parsing and type-checking generics #671

Parsing and type-checking generics #671

koflin commented Aug 24, 2023

koflin commented Aug 24, 2023

Felalolf left a comment

Felalolf Aug 24, 2023

Felalolf Aug 24, 2023

koflin Aug 24, 2023

Felalolf Aug 24, 2023

koflin Aug 24, 2023

Felalolf Aug 25, 2023

Felalolf Aug 24, 2023

Felalolf Aug 24, 2023

Felalolf Aug 24, 2023

koflin Aug 24, 2023

Felalolf Aug 24, 2023

Felalolf Aug 25, 2023

koflin Aug 25, 2023

Felalolf Aug 24, 2023

Felalolf Aug 24, 2023

koflin Aug 24, 2023

Felalolf Aug 24, 2023

		@@ -0,0 +1,606 @@
		// Generated from s:\GitHub\gobra\src\main\antlr4\GoLexer.g4 by ANTLR 4.9.2

	case TypeParameterT(_, _, _) => true
	case _: TypeParameterT => true

Parsing and type-checking generics #671

Are you sure you want to change the base?

Parsing and type-checking generics #671

Conversation

koflin commented Aug 24, 2023

koflin commented Aug 24, 2023

Felalolf left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment