From 4be934118404871782cfe4af8039d0dd743ee7ab Mon Sep 17 00:00:00 2001 From: "Felix A. Wolf" Date: Fri, 29 Sep 2023 14:12:26 +0200 Subject: [PATCH] fixed some issues --- .../scala/viper/gobra/ast/frontend/AstPattern.scala | 1 + .../viper/gobra/frontend/info/base/SymbolTable.scala | 2 +- .../resolution/AmbiguityResolution.scala | 5 +++-- .../implementation/resolution/NameResolution.scala | 12 +++++++++--- .../info/implementation/typing/TypeTyping.scala | 4 ++-- src/test/resources/regressions/issues/000655.gobra | 2 +- .../resources/regressions/issues/000655/pkg/f.gobra | 8 ++++++++ 7 files changed, 25 insertions(+), 9 deletions(-) diff --git a/src/main/scala/viper/gobra/ast/frontend/AstPattern.scala b/src/main/scala/viper/gobra/ast/frontend/AstPattern.scala index 3a6cfdc9c..96d88e903 100644 --- a/src/main/scala/viper/gobra/ast/frontend/AstPattern.scala +++ b/src/main/scala/viper/gobra/ast/frontend/AstPattern.scala @@ -20,6 +20,7 @@ object AstPattern { sealed trait Type extends Pattern + case class Import(id: PIdnUse, symb: st.Import) extends Type with Symbolic case class NamedType(id: PIdnUse, symb: st.ActualTypeEntity) extends Type with Symbolic case class PointerType(base: PType) extends Type case class AdtClause(id: PIdnUse, symb: st.AdtClause) extends Type with Symbolic diff --git a/src/main/scala/viper/gobra/frontend/info/base/SymbolTable.scala b/src/main/scala/viper/gobra/frontend/info/base/SymbolTable.scala index 9776daa7a..8b96ff873 100644 --- a/src/main/scala/viper/gobra/frontend/info/base/SymbolTable.scala +++ b/src/main/scala/viper/gobra/frontend/info/base/SymbolTable.scala @@ -261,7 +261,7 @@ object SymbolTable extends Environments[Entity] { override def addressable: Boolean = false } - case class AdtClause(decl: PAdtClause, typeDecl: PTypeDef, context: ExternalTypeInfo) extends GhostTypeMember { + case class AdtClause(decl: PAdtClause, typeDecl: PTypeDef, context: ExternalTypeInfo) extends GhostTypeMember with TypeEntity { require(typeDecl.right.isInstanceOf[PAdtType]) override def rep: PNode = decl diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/AmbiguityResolution.scala b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/AmbiguityResolution.scala index dfc9f8cd5..746ccf4b2 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/AmbiguityResolution.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/AmbiguityResolution.scala @@ -9,7 +9,7 @@ package viper.gobra.frontend.info.implementation.resolution import viper.gobra.ast.frontend._ import viper.gobra.ast.frontend.{AstPattern => ap} import viper.gobra.frontend.info.base.{SymbolTable => st} -import viper.gobra.frontend.info.base.Type.{ImportT, PredT, FunctionT} +import viper.gobra.frontend.info.base.Type.{AdtT, FunctionT, ImportT, PredT} import viper.gobra.frontend.info.implementation.TypeInfoImpl import viper.gobra.util.Violation.violation @@ -31,7 +31,7 @@ trait AmbiguityResolution { this: TypeInfoImpl => .fold( _ => Left(n), symbType(_) match { // check if base is a package qualifier and id points to a type - case _: ImportT if pointsToType(n.id) => Right(n) + case _: ImportT | _: AdtT if pointsToType(n.id) => Right(n) case _ => Left(n) }) @@ -50,6 +50,7 @@ trait AmbiguityResolution { this: TypeInfoImpl => case n: PNamedOperand => entity(n.id) match { + case s: st.Import => Some(ap.Import(n.id, s)) case s: st.NamedType => Some(ap.NamedType(n.id, s)) case s: st.Variable => s match { case g: st.GlobalVariable => Some(ap.GlobalVariable(n.id, g)) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala index 9465a2c3d..ee076f137 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/NameResolution.scala @@ -11,7 +11,7 @@ import viper.gobra.frontend.PackageResolver.RegularImport import viper.gobra.frontend.info.base.BuiltInMemberTag import viper.gobra.frontend.info.base.BuiltInMemberTag.{BuiltInFPredicateTag, BuiltInFunctionTag, BuiltInMPredicateTag, BuiltInMethodTag, BuiltInTypeTag} import viper.gobra.frontend.info.base.SymbolTable._ -import viper.gobra.frontend.info.base.Type.{AdtClauseT, InterfaceT, StructT} +import viper.gobra.frontend.info.base.Type.{AdtT, InterfaceT, StructT} import viper.gobra.frontend.info.implementation.TypeInfoImpl import viper.gobra.frontend.info.implementation.property.{AssignMode, StrictAssignMode} import viper.gobra.util.Violation @@ -320,7 +320,13 @@ trait NameResolution { case c => Violation.violation(s"Only the root has no parent, but got $c") } - lazy val topLevelEnvironment: Environment = scopedDefenv(tree.originalRoot) + /** Symboltable imported by a package import. */ + lazy val topLevelEnvironment: Environment = { + val thisPkg = tree.originalRoot + val base = scopedDefenv(thisPkg) + val late = lateEnvironments(thisPkg) + base ++ late + } lazy val entity: PIdnNode => Entity = attr[PIdnNode, Entity] { @@ -350,7 +356,7 @@ trait NameResolution { // if the enclosing literal is a struct then id is a field case t: StructT => tryFieldLookup(t, id).map(_._1).getOrElse(UnknownEntity()) // if the enclosing literal is an adt clause then id is an adt field - case t: AdtClauseT => tryAdtMemberLookup(t, id).map(_._1).getOrElse(UnknownEntity()) + case t: AdtT => tryAdtMemberLookup(t, id).map(_._1).getOrElse(UnknownEntity()) // otherwise it is just a variable case _ => symbTableLookup(n) } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala index cd1957434..993be91a3 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala @@ -72,7 +72,7 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => isRecursiveInterface } - case t: PExpressionAndType => wellDefExprAndType(t).out + case t: PExpressionAndType => wellDefExprAndType(t).out ++ isType(t).out } lazy val typeSymbType: Typing[PType] = { @@ -158,7 +158,7 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => val fields = p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ)) AdtClauseT(p.symb.getName, fields, p.symb.decl, p.symb.typeDecl, p.symb.context) - case _ => violation(s"expected type, but got $n") + case p => violation(s"expected type, but got $n with resolved pattern $p") } } diff --git a/src/test/resources/regressions/issues/000655.gobra b/src/test/resources/regressions/issues/000655.gobra index fcafa8991..071f68f74 100644 --- a/src/test/resources/regressions/issues/000655.gobra +++ b/src/test/resources/regressions/issues/000655.gobra @@ -13,4 +13,4 @@ pure func foo(x pkg.List) bool { case pkg.Cons{?head, pkg.Nil{}}: true case _: false } -} \ No newline at end of file +} diff --git a/src/test/resources/regressions/issues/000655/pkg/f.gobra b/src/test/resources/regressions/issues/000655/pkg/f.gobra index 2252d81b9..6df472b61 100644 --- a/src/test/resources/regressions/issues/000655/pkg/f.gobra +++ b/src/test/resources/regressions/issues/000655/pkg/f.gobra @@ -12,3 +12,11 @@ type List adt { Nil {} } +type Tree adt { + Leaf{} + Branch{ Left, Right Tree } +} + +func Leaf() { +} +