No commit message

No commit message

src/funcheck/CodeExtraction.scala

@@ -366,6 +366,26 @@ trait CodeExtraction extends Extractors {
         val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
         EmptySet(underlying).setType(SetType(underlying))          
       }
+      case ExSetMin(t) => {
+        val set = rec(t)
+        if(!set.getType.isInstanceOf[SetType]) {
+          if(!silent) {
+            unit.error(t.pos, "Min should be computed on a set.")
+          }
+          throw ImpureCodeEncounteredException(tree)
+        }
+        SetMin(set).setType(set.getType.asInstanceOf[SetType].base)
+      }
+      case ExSetMax(t) => {
+        val set = rec(t)
+        if(!set.getType.isInstanceOf[SetType]) {
+          if(!silent) {
+            unit.error(t.pos, "Max should be computed on a set.")
+          }
+          throw ImpureCodeEncounteredException(tree)
+        }
+        SetMax(set).setType(set.getType.asInstanceOf[SetType].base)
+      }
       case ExUnion(t1,t2) => {
         val rl = rec(t1)
         val rr = rec(t2)

src/funcheck/Extractors.scala

@@ -304,6 +304,24 @@ trait Extractors {
         if(tree != null) Some((tree.selector, tree.cases)) else None
     }
 
+    object ExSetMin {
+      def unapply(tree: Apply) : Option[Tree] = tree match {
+        case Apply(
+          TypeApply(Select(setTree, minName), typeTree :: Nil),
+          ordering :: Nil) if minName.toString == "min" && typeTree.tpe == IntClass.tpe => Some(setTree)
+        case _ => None
+      }
+    }
+
+    object ExSetMax {
+      def unapply(tree: Apply) : Option[Tree] = tree match {
+        case Apply(
+          TypeApply(Select(setTree, maxName), typeTree :: Nil),
+          ordering :: Nil) if maxName.toString == "max" && typeTree.tpe == IntClass.tpe => Some(setTree)
+        case _ => None
+      }
+    }
+
     object ExEmptySet {
       def unapply(tree: TypeApply): Option[Tree] = tree match {
         case TypeApply(

src/purescala/Definitions.scala

@@ -20,7 +20,20 @@ object Definitions {
 
   /** A wrapper for a program. For now a program is simply a single object. The
    * name is meaningless and we just use the package name as id. */
-  case class Program(id: Identifier, mainObject: ObjectDef) extends Definition 
+  case class Program(id: Identifier, mainObject: ObjectDef) extends Definition {
+    lazy val callGraph: Map[FunDef,Seq[FunDef]] = computeCallGraph
+
+    def computeCallGraph: Map[FunDef,Seq[FunDef]] = Map.empty
+
+    // checks whether f2 can be called from f1
+    def calls(f1: FunDef, f2: FunDef) : Boolean = {
+      false
+    }
+
+    def transitivelyCalls(f1: FunDef, f2: FunDef) : Boolean = {
+      false
+    }
+  }
 
   /** Objects work as containers for class definitions, functions (def's) and
    * val's. */
@@ -86,5 +99,9 @@ object Definitions {
     var body: Option[Expr] = None
     var precondition: Option[Expr] = None
     var postcondition: Option[Expr] = None
+
+    def hasImplementation : Boolean = body.isDefined
+    def hasPrecondition : Boolean = precondition.isDefined
+    def hasPostcondition : Boolean = postcondition.isDefined
   }
 }

src/purescala/PrettyPrinter.scala

@@ -103,6 +103,8 @@ object PrettyPrinter {
     case GreaterEquals(l,r) => ppBinary(sb, l, r, " \u2265 ", lvl)   // \geq
     case FiniteSet(rs) => ppNary(sb, rs, "{", ", ", "}", lvl)
     case EmptySet(_) => sb.append("\u2205")                          // Ø
+    case SetMin(s) => pp(s, sb, lvl).append(".min")
+    case SetMax(s) => pp(s, sb, lvl).append(".max")
     case SetUnion(l,r) => ppBinary(sb, l, r, " \u222A ", lvl)        // \cup
     case SetDifference(l,r) => ppBinary(sb, l, r, " \\ ", lvl)       
     case SetIntersection(l,r) => ppBinary(sb, l, r, " \u2229 ", lvl) // \cap