Merge pull request #758 from viperproject/meilers_type_var_defaults

No longer substituting Int as default for unconstrained type variables inside domains

Author: marcoeilers

src/main/scala/viper/silver/parser/ParseAst.scala

@@ -321,6 +321,7 @@ object PTypeVar {
   }
 
   val sep = "#"
+  val domainNameSep = "%"
 
   //TODO: do this properly
   def isFreePTVName(s: String) = s.contains(sep)
@@ -342,9 +343,18 @@ object PTypeVar {
     freshTypeSubstitution(tvs map (tv => tv.domain.name))
   }
 
-  def freshTypeSubstitution(tvns: Seq[String]): PTypeRenaming = {
+  def freshTypeSubstitution(tvns: Seq[String], domainName: Option[String] = None): PTypeRenaming = {
     val ind = lastIndex.getAndIncrement()
-    new PTypeRenaming((tvns map (tv => tv -> getFreshName(tv, ind))).toMap)
+    new PTypeRenaming((tvns map (tv => {
+      val tvName = domainName match {
+        case Some(dn) =>
+          // Choose a name for the type variable that contains the domain name.
+          // This enables us to choose a useful default in case the type variable is unconstrained.
+          dn + domainNameSep + tv
+        case None => tv
+      }
+      tv -> getFreshName(tvName, ind)
+    })).toMap)
   }
 }
 

src/main/scala/viper/silver/parser/Resolver.scala

@@ -492,9 +492,31 @@ case class TypeChecker(names: NameAnalyser) {
 
   def ground(exp: PExp, pts: PTypeSubstitution): PTypeSubstitution = {
     pts.m.flatMap(kv => kv._2.freeTypeVariables &~ pts.m.keySet).foldLeft(pts)((ts, fv) => {
-      messages ++= FastMessaging.message(exp,
-        s"Unconstrained type parameter, substituting default type ${PTypeSubstitution.defaultType}.", error = false)
-      ts.add(PTypeVar(fv), PTypeSubstitution.defaultType).toOption.get
+      var chosenType: PType = PTypeSubstitution.defaultType
+      curMember match {
+        case ax: PAxiom if ax.parent.exists(p => p.isInstanceOf[PDomain]) =>
+          // If we are inside the domain that defines the type variable, then we choose the type variable itself
+          // as the default.
+          val domain = ax.parent.get.asInstanceOf[PDomain]
+          // The name pf domain function application type variables has the form
+          // domainName + PTypeVar.domainNameSep + typeVarName + PTypeVar.sep + index
+          if (fv.startsWith(domain.idndef.name + PTypeVar.domainNameSep)) {
+            var tvName = fv.substring(domain.idndef.name.length + 1)
+            if (tvName.contains(PTypeVar.sep)) {
+              tvName = tvName.substring(0, tvName.indexOf(PTypeVar.sep))
+              if (domain.typVars.exists(tv => tv.idndef.name == tvName)) {
+                // The type variable refers to an actual type variable of the current domain.
+                chosenType = PTypeVar(tvName)
+              }
+            }
+          }
+        case _ =>
+      }
+      if (chosenType == PTypeSubstitution.defaultType) {
+        messages ++= FastMessaging.message(exp,
+          s"Unconstrained type parameter, substituting default type ${PTypeSubstitution.defaultType}.", error = false)
+      }
+      ts.add(PTypeVar(fv), chosenType).toOption.get
     })
   }
 
@@ -642,7 +664,7 @@ case class TypeChecker(names: NameAnalyser) {
 
                         case pdf@PDomainFunction(_, _, _, _, _) =>
                           val domain = names.definition(curMember)(pdf.domainName).get.asInstanceOf[PDomain]
-                          val fdtv = PTypeVar.freshTypeSubstitution((domain.typVars map (tv => tv.idndef.name)).distinct) //fresh domain type variables
+                          val fdtv = PTypeVar.freshTypeSubstitution((domain.typVars map (tv => tv.idndef.name)).distinct, Some(domain.idndef.name)) //fresh domain type variables
                           pfa.domainTypeRenaming = Some(fdtv)
                           pfa._extraLocalTypeVariables = (domain.typVars map (tv => PTypeVar(tv.idndef.name))).toSet
                           extraReturnTypeConstraint = explicitType

src/test/resources/all/issues/silver/0236.vpr

@@ -0,0 +1,19 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+domain Option[T] {
+  axiom ax_Option_None_discr {
+    Option_discr(Option_None()) == 0
+  }
+  function Option_discr(Option[T]): Int
+  function Option_None(): Option[T]
+  function Option_Some(T): Option[T]
+}
+
+method m() {
+    assert Option_discr((Option_None(): Option[Bool])) == 0;
+    assert Option_discr((Option_None(): Option[Ref])) == 0;
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert Option_discr((Option_None(): Option[Perm])) == 1;
+}