From becae01db52f6c634c3c79909720ba645f99132d Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Tue, 29 Jun 2010 14:15:04 +0000
Subject: [PATCH]
---
src/funcheck/CodeExtraction.scala | 20 ++++++++++++++++++++
src/funcheck/Extractors.scala | 18 ++++++++++++++++++
src/purescala/Definitions.scala | 19 ++++++++++++++++++-
src/purescala/PrettyPrinter.scala | 2 ++
4 files changed, 58 insertions(+), 1 deletion(-)
diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index c8c887a13..83fa2d608 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/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)
diff --git a/src/funcheck/Extractors.scala b/src/funcheck/Extractors.scala
index da04302b6..1081ec2a5 100644
--- a/src/funcheck/Extractors.scala
+++ b/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(
diff --git a/src/purescala/Definitions.scala b/src/purescala/Definitions.scala
index 42e2807c5..917879362 100644
--- a/src/purescala/Definitions.scala
+++ b/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
}
}
diff --git a/src/purescala/PrettyPrinter.scala b/src/purescala/PrettyPrinter.scala
index 4e312210a..f273e877f 100644
--- a/src/purescala/PrettyPrinter.scala
+++ b/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
--
GitLab