document type set, underlying type and rename syntaxImplements

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

@@ -17,7 +17,7 @@ trait Implements { this: TypeInfoImpl =>
 
   def implements(l: Type, r: Type): PropertyResult = underlyingType(r) match {
     case itf: Type.InterfaceT =>
-      val valid = syntaxImplements(l, r)
+      val valid = implementsMemberSet(l, r)
       if (valid.holds && l != NilType && !itf.isEmpty) {
         _requiredImplements ++= Set((l, itf))
       }
@@ -55,10 +55,10 @@ trait Implements { this: TypeInfoImpl =>
     (localRequiredImplements ++ localGuaranteedImplements).groupMap(_._2)(_._1)
   }
 
-  def syntaxImplements(l: Type, r: Type): PropertyResult = (l, underlyingType(r)) match {
+  def implementsMemberSet(l: Type, r: Type): PropertyResult = (l, underlyingType(r)) match {
     case (NilType, _: Type.InterfaceT) => successProp
     // a type parameter syntactically implements an interface iff its type constraint syntactically implements the interface
-    case (Type.TypeParameterT(_, constraint, _), _: Type.InterfaceT) => syntaxImplements(symbType(constraint), r)
+    case (Type.TypeParameterT(_, constraint, _), _: Type.InterfaceT) => implementsMemberSet(symbType(constraint), r)
     case (_, _: Type.InterfaceT) =>
       supportedSortForInterfaces(l) and {
         val itfMemberSet = memberSet(r)

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

@@ -23,6 +23,6 @@ trait Satisfiability extends BaseProperty { this: TypeInfoImpl =>
           failedProp("is not a subset of the allowed type set", !TypeSet.isSubset(TypeSet.from(i.decl, this), interfaceTypeSet))
         case _ =>
           failedProp("is not an element of the allowed type set", !TypeSet.contains(interfaceTypeSet, typ))
-      }) and syntaxImplements(typ, InterfaceT(interfacePType, this))
+      }) and implementsMemberSet(typ, InterfaceT(interfacePType, this))
   }
 }

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))
+      // the underlying type of a type parameter is the underlying type of its type constraint (interface)
       case Single(TypeParameterT(_, t: PInterfaceType, ctx)) => underlyingType(ctx.symbType(t))
       case t => t
     }

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

@@ -6,10 +6,21 @@ import viper.gobra.frontend.info.implementation.TypeInfoImpl
 
 sealed trait TypeSet
 
+/**
+  * The type set of a type parameter constraint is the set of all types that satisfy this constraint
+  * In this implementation, type sets that are unbounded are represented by the [[UnboundedTypeSet]]
+  * Bounded type sets are represented by [[BoundedTypeSet]] and explicitly list the set of types they contains
+  *
+  * Additionally, an unbounded type set needs to keep track whether all types in the type set are comparable
+  * The comparability of a bounded type set can just be calculated with the set of types it contains
+  */
 object TypeSet {
   case class UnboundedTypeSet(isComparable: Boolean = false) extends TypeSet
   case class BoundedTypeSet(ts: Set[Type]) extends TypeSet
 
+  /**
+    * Constructs the type set from a type parameter constraint
+    */
   def from(constraint: PInterfaceType, ctx: TypeInfoImpl): TypeSet = typeSetFromInterfaceType(constraint, ctx)
 
   private def typeSetFromInterfaceType(inter: PInterfaceType, ctx: TypeInfoImpl): TypeSet = inter match {

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala

@@ -30,7 +30,7 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl =>
       val subType = symbType(ip.subT)
       val superType = symbType(ip.superT)
 
-      val syntaxImplementsMsgs = syntaxImplements(subType, superType).asReason(ip, s"${ip.subT} does not implement the interface ${ip.superT}")
+      val syntaxImplementsMsgs = implementsMemberSet(subType, superType).asReason(ip, s"${ip.subT} does not implement the interface ${ip.superT}")
       if (syntaxImplementsMsgs.nonEmpty) syntaxImplementsMsgs
       else {
         addDemandedImplements(subType, superType)