Added support for Seq[type]() syntax, so that empty sequences of spec…

…ified type can be created. This is needed e.g. for examples in which assertions t==Seq() are wanted; the type-checker complains without more type information. Also fixed a typo in a name (PUnkown -> PUnknown)
viperproject · Sep 3, 2013 · 09b9abe · 09b9abe
1 parent 0de4299
commit 09b9abe
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 18 deletions.
diff --git a/src/main/scala/semper/sil/parser/ParseAst.scala b/src/main/scala/semper/sil/parser/ParseAst.scala
@@ -81,7 +81,7 @@ case class PFormalArgDecl(idndef: PIdnDef, typ: PType) extends PNode with RealEn
 
 // Types
 sealed trait PType extends PNode {
-  def isUnknown: Boolean = this.isInstanceOf[PUnkown]
+  def isUnknown: Boolean = this.isInstanceOf[PUnknown]
   def isConcrete: Boolean = true
   def substitute(newTypVarsMap: Map[String, PType]): PType = this
 }
@@ -134,7 +134,7 @@ case class PMultisetType(elementType: PType) extends PType {
   override def substitute(map: Map[String, PType]) = PMultisetType(elementType.substitute(map))
 }
 // for resolving if something cannot be typed
-case class PUnkown() extends PType {
+case class PUnknown() extends PType {
   override def toString = "<error type>"
 }
 // used during resolving for predicate accesses
@@ -145,7 +145,7 @@ case class PPredicateType() extends PType {
 
 // Expressions
 sealed trait PExp extends PNode {
-  var typ: PType = PUnkown()
+  var typ: PType = PUnknown()
 }
 case class PBinExp(left: PExp, op: String, right: PExp) extends PExp
 case class PUnExp(op: String, exp: PExp) extends PExp
@@ -175,8 +175,10 @@ case class PWildcard() extends PExp
 case class PEpsilon() extends PExp
 case class PAccPred(loc: PLocationAccess, perm: PExp) extends PExp
 case class POld(e: PExp) extends PExp
-
-case class PEmptySeq() extends PExp
+case class PEmptySeq(t : PType) extends PExp 
+{
+  typ = (if (t.isUnknown) PUnknown() else PSeqType(t)) // type can be specified as PUnknown() if unknown
+}
 case class PExplicitSeq(elems: Seq[PExp]) extends PExp
 case class PRangeSeq(low: PExp, high: PExp) extends PExp
 case class PSeqIndex(seq: PExp, idx: PExp) extends PExp
@@ -274,7 +276,7 @@ object Nodes {
       case PSeqType(elemType) => Seq(elemType)
       case PSetType(elemType) => Seq(elemType)
       case PMultisetType(elemType) => Seq(elemType)
-      case PUnkown() => Nil
+      case PUnknown() => Nil
       case PBinExp(left, op, right) => Seq(left, right)
       case PUnExp(op, exp) => Seq(exp)
       case PIntLit(i) => Nil
@@ -297,7 +299,7 @@ object Nodes {
       case PWildcard() => Nil
       case PEpsilon() => Nil
       case PAccPred(loc, perm) => Seq(loc, perm)
-      case PEmptySeq() => Nil
+      case PEmptySeq(_) => Nil
       case PExplicitSeq(elems) => elems
       case PRangeSeq(low, high) => Seq(low, high)
       case PSeqIndex(seq, idx) => Seq(seq, idx)

diff --git a/src/main/scala/semper/sil/parser/Parser.scala b/src/main/scala/semper/sil/parser/Parser.scala
@@ -348,9 +348,11 @@ trait BaseParser extends WhitespacePositionedParserUtilities {
   // --- Sequences
 
   lazy val seq =
-    seqLength | explicitSeq | seqIndex | seqRange |
+    seqTypedEmpty | seqLength | explicitSeq | seqIndex | seqRange |
       seqTake | seqDrop | seqTakeDrop |
       seqContains | seqUpdate
+  lazy val seqTypedEmpty: PackratParser[PExp] =
+    "Seq[" ~> typ <~ "]()" ^^ PEmptySeq
   lazy val seqLength: PackratParser[PExp] =
     "|" ~> exp <~ "|" ^^ PSize
   lazy val seqTake: PackratParser[PExp] =
@@ -369,7 +371,7 @@ trait BaseParser extends WhitespacePositionedParserUtilities {
     exp ~ ("[" ~> exp <~ ":=") ~ (exp <~ "]") ^^ PSeqUpdate
   lazy val explicitSeq: PackratParser[PExp] =
     "Seq(" ~> repsep(exp, ",") <~ ")" ^^ {
-      case Nil => PEmptySeq()
+      case Nil => PEmptySeq(PUnknown())
       case elems => PExplicitSeq(elems)
     }
   lazy val seqRange: PackratParser[PExp] =

diff --git a/src/main/scala/semper/sil/parser/Resolver.scala b/src/main/scala/semper/sil/parser/Resolver.scala
@@ -237,7 +237,7 @@ case class TypeChecker(names: NameAnalyser) {
         check(elemType)
       case PMultisetType(elemType) =>
         check(elemType)
-      case PUnkown() =>
+      case PUnknown() =>
         message(typ, "expected concrete type, but found unknown typ")
     }
   }
@@ -265,13 +265,13 @@ case class TypeChecker(names: NameAnalyser) {
 
   /**
    * Are types 'a' and 'b' compatible?  Type variables are assumed to be unbound so far,
-   * and if they occur they are compatible with any type.  PUnkown is also compatible with
+   * and if they occur they are compatible with any type.  PUnknown is also compatible with
    * everything.
    */
   def isCompatible(a: PType, b: PType): Boolean = {
     (a, b) match {
-      case (PUnkown(), t) => true
-      case (t, PUnkown()) => true
+      case (PUnknown(), t) => true
+      case (t, PUnknown()) => true
       case (PTypeVar(name), t) => true
       case (t, PTypeVar(name)) => true
       case (PSeqType(e1), PSeqType(e2)) => isCompatible(e1, e2)
@@ -348,7 +348,7 @@ case class TypeChecker(names: NameAnalyser) {
      * Sets an error type for 'exp' to suppress further warnings.
      */
     def setErrorType() {
-      setType(PUnkown())
+      setType(PUnknown())
     }
     def genericSeqType: PSeqType = PSeqType(PTypeVar("."))
     def genericSetType: PSetType = PSetType(PTypeVar("."))
@@ -627,8 +627,8 @@ case class TypeChecker(names: NameAnalyser) {
         check(loc, Seq())
         check(perm, Perm)
         setType(Bool)
-      case PEmptySeq() =>
-        val typ = genericSeqType
+      case PEmptySeq(_) =>
+        val typ = (if (exp.typ.isUnknown) genericSeqType else exp.typ)
         if (expected.size == 1) {
           setRefinedType(typ, learn(typ, expected.head))
         } else {

diff --git a/src/main/scala/semper/sil/parser/Translator.scala b/src/main/scala/semper/sil/parser/Translator.scala
@@ -321,7 +321,7 @@ case class Translator(program: PProgram) {
           case _ =>
             sys.error("unexpected location")
         }
-      case PEmptySeq() =>
+      case PEmptySeq(_) =>
         EmptySeq(ttyp(pexp.typ.asInstanceOf[PSeqType].elementType))(pos)
       case PExplicitSeq(elems) =>
         ExplicitSeq(elems map exp)(pos)
@@ -383,7 +383,7 @@ case class Translator(program: PProgram) {
           assert(args.length == 0)
           TypeVar(name.name) // not a domain, i.e. it must be a type variable
       }
-    case PUnkown() =>
+    case PUnknown() =>
       sys.error("unknown type unexpected here")
     case PPredicateType() =>
       sys.error("unexpected use of internal typ")