Skip to content

Commit

Permalink
fixed some issues
Browse files Browse the repository at this point in the history
  • Loading branch information
Felalolf committed Sep 29, 2023
1 parent a1372c5 commit 4be9341
Show file tree
Hide file tree
Showing 7 changed files with 25 additions and 9 deletions.
1 change: 1 addition & 0 deletions src/main/scala/viper/gobra/ast/frontend/AstPattern.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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)
})

Expand All @@ -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))
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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] {
Expand Down Expand Up @@ -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)
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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] = {
Expand Down Expand Up @@ -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")
}
}

Expand Down
2 changes: 1 addition & 1 deletion src/test/resources/regressions/issues/000655.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -13,4 +13,4 @@ pure func foo(x pkg.List) bool {
case pkg.Cons{?head, pkg.Nil{}}: true
case _: false
}
}
}
8 changes: 8 additions & 0 deletions src/test/resources/regressions/issues/000655/pkg/f.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -12,3 +12,11 @@ type List adt {
Nil {}
}

type Tree adt {
Leaf{}
Branch{ Left, Right Tree }
}

func Leaf() {
}

0 comments on commit 4be9341

Please sign in to comment.