diff --git a/ParseMe.scala b/ParseMe.scala
index c6323a6b7434f83d127e4e5786e72795e395808e..ae05f6291bced543d099d314333a4bbb465a8bba 100644
--- a/ParseMe.scala
+++ b/ParseMe.scala
@@ -2,19 +2,23 @@ import scala.collection.immutable.Set
object ParseMe {
sealed abstract class Tree
- //case class Node(value: Int) extends Tree
case class Node(left: Tree, value: Int, right: Tree) extends Tree
case class Leaf() extends Tree
- def getSet(s: Int): Tree = {
- if (4 + s < 2 + s && s > 4) {
- emptySet()
- } else {
- Node(Leaf(), 1, Leaf())
- }
+ def inside(n: Node): Int = getIt().value
+
+ def getIt() : Node = Node(Leaf(), 12, Leaf())
+
+ def insert(v: Int, t: Tree): Tree = t match {
+ case Leaf() if v == 5 => Leaf()
+ case Leaf() => Node(Leaf(), v, Leaf())
+ case Node(Leaf(), 12, Leaf()) => Leaf()
+ case _ => Leaf()
}
def emptySet() : Tree = {
Leaf()
}
+
+ def withIf(a: Int) : Int = { if(a < 0) -a else if(a > 0) a+1 else a-1 } ensuring (_ > 17)
}
diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index c912c627447d975d5aecb28893932431ee74bdc1..31e711df0b81884013014fc2bfd141719bb20edd 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -18,8 +18,8 @@ trait CodeExtraction extends Extractors {
private lazy val setTraitSym = definitions.getClass("scala.collection.immutable.Set")
- private val varSubsts: scala.collection.mutable.Map[Identifier,Function0[Expr]] =
- scala.collection.mutable.Map.empty[Identifier,Function0[Expr]]
+ private val varSubsts: scala.collection.mutable.Map[Symbol,Function0[Expr]] =
+ scala.collection.mutable.Map.empty[Symbol,Function0[Expr]]
private val classesToClasses: scala.collection.mutable.Map[Symbol,ClassTypeDef] =
scala.collection.mutable.Map.empty[Symbol,ClassTypeDef]
private val defsToDefs: scala.collection.mutable.Map[Symbol,FunDef] =
@@ -64,7 +64,7 @@ trait CodeExtraction extends Extractors {
top.get
}
- def extractObjectDef(name: Identifier, tmpl: Template): ObjectDef = {
+ def extractObjectDef(nameStr: String, tmpl: Template): ObjectDef = {
// we assume that the template actually corresponds to an object
// definition. Typically it should have been obtained from the proper
// extractor (ExObjectDef)
@@ -75,10 +75,10 @@ trait CodeExtraction extends Extractors {
val scalaClassSyms: scala.collection.mutable.Map[Symbol,Identifier] =
scala.collection.mutable.Map.empty[Symbol,Identifier]
- val scalaClassArgs: scala.collection.mutable.Map[Symbol,Seq[(Identifier,Tree)]] =
- scala.collection.mutable.Map.empty[Symbol,Seq[(Identifier,Tree)]]
- val scalaClassNames: scala.collection.mutable.Set[Identifier] =
- scala.collection.mutable.Set.empty[Identifier]
+ val scalaClassArgs: scala.collection.mutable.Map[Symbol,Seq[(String,Tree)]] =
+ scala.collection.mutable.Map.empty[Symbol,Seq[(String,Tree)]]
+ val scalaClassNames: scala.collection.mutable.Set[String] =
+ scala.collection.mutable.Set.empty[String]
// we need the new type definitions before we can do anything...
tmpl.body.foreach(t =>
@@ -87,7 +87,7 @@ trait CodeExtraction extends Extractors {
if(scalaClassNames.contains(o2)) {
unit.error(t.pos, "A class with the same name already exists.")
} else {
- scalaClassSyms += (sym -> o2)
+ scalaClassSyms += (sym -> FreshIdentifier(o2))
scalaClassNames += o2
}
}
@@ -95,7 +95,7 @@ trait CodeExtraction extends Extractors {
if(scalaClassNames.contains(o2)) {
unit.error(t.pos, "A class with the same name already exists.")
} else {
- scalaClassSyms += (sym -> o2)
+ scalaClassSyms += (sym -> FreshIdentifier(o2))
scalaClassNames += o2
scalaClassArgs += (sym -> args)
}
@@ -138,7 +138,10 @@ trait CodeExtraction extends Extractors {
if(p._2.isInstanceOf[CaseClassDef]) {
// this should never fail
val ccargs = scalaClassArgs(p._1)
- p._2.asInstanceOf[CaseClassDef].fields = ccargs.map(cca => VarDecl(cca._1, st2ps(cca._2.tpe)))
+ p._2.asInstanceOf[CaseClassDef].fields = ccargs.map(cca => {
+ val cctpe = st2ps(cca._2.tpe)
+ VarDecl(FreshIdentifier(cca._1).setType(cctpe), cctpe)
+ })
}
})
@@ -185,13 +188,20 @@ trait CodeExtraction extends Extractors {
}
)
+ val name: Identifier = FreshIdentifier(nameStr)
val theDef = new ObjectDef(name, objectDefs.reverse ::: classDefs ::: funDefs, Nil)
theDef
}
- def extractFunSig(name: Identifier, params: Seq[ValDef], tpt: Tree): FunDef = {
- new FunDef(name, st2ps(tpt.tpe), params.map(p => VarDecl(p.name.toString, st2ps(p.tpt.tpe))))
+ def extractFunSig(nameStr: String, params: Seq[ValDef], tpt: Tree): FunDef = {
+ val newParams = params.map(p => {
+ val ptpe = st2ps(p.tpt.tpe)
+ val newID = FreshIdentifier(p.name.toString).setType(ptpe)
+ varSubsts(p.symbol) = (() => Variable(newID))
+ VarDecl(newID, ptpe)
+ })
+ new FunDef(FreshIdentifier(nameStr), st2ps(tpt.tpe), newParams)
}
def extractFunDef(funDef: FunDef, body: Tree): FunDef = {
@@ -200,10 +210,10 @@ trait CodeExtraction extends Extractors {
var ensCont: Option[Expr] = None
realBody match {
- case ExEnsuredExpression(body2, resId, contract) => {
- varSubsts(resId) = (() => ResultVariable())
+ case ExEnsuredExpression(body2, resSym, contract) => {
+ varSubsts(resSym) = (() => ResultVariable())
val c1 = s2ps(contract)
- varSubsts.remove(resId)
+ // varSubsts.remove(resSym)
realBody = body2
ensCont = Some(c1)
}
@@ -230,8 +240,8 @@ trait CodeExtraction extends Extractors {
stopIfErrors
val programName: Identifier = unit.body match {
- case PackageDef(name, _) => name.toString
- case _ => "<program>"
+ case PackageDef(name, _) => FreshIdentifier(name.toString)
+ case _ => FreshIdentifier("<program>")
}
//Program(programName, ObjectDef("Object", Nil, Nil))
@@ -262,12 +272,24 @@ trait CodeExtraction extends Extractors {
* if impossible. If not in 'silent mode', non-pure AST nodes are reported as
* errors. */
private def scala2PureScala(unit: CompilationUnit, silent: Boolean)(tree: Tree): Expr = {
+ def rewriteCaseDef(cd: CaseDef): MatchCase = {
+ def pat2pat(p: Tree): Pattern = {
+ WildcardPattern(None)
+ }
+
+ if(cd.guard == EmptyTree) {
+ SimpleCase(pat2pat(cd.pat), rec(cd.body))
+ } else {
+ GuardedCase(pat2pat(cd.pat), rec(cd.guard), rec(cd.body))
+ }
+ }
+
def rec(tr: Tree): Expr = tr match {
case ExInt32Literal(v) => IntLiteral(v)
case ExBooleanLiteral(v) => BooleanLiteral(v)
- case ExIdentifier(id,tpt) => varSubsts.get(id) match {
+ case ExIdentifier(sym,tpt) => varSubsts.get(sym) match {
case Some(fun) => fun()
- case None => Variable(id)
+ case None => Variable(FreshIdentifier(sym.name.toString)) // TODO this is SO wrong
}
case ExCaseClassConstruction(tpt, args) => {
val cctype = scalaType2PureScala(unit, silent)(tpt.tpe)
@@ -278,27 +300,68 @@ trait CodeExtraction extends Extractors {
throw ImpureCodeEncounteredException(tree)
}
val nargs = args.map(rec(_))
- CaseClass(cctype.asInstanceOf[CaseClassType], nargs)
+ val cct = cctype.asInstanceOf[CaseClassType]
+ CaseClass(cct.classDef, nargs).setType(cct)
+ }
+ case ExAnd(l, r) => And(rec(l), rec(r)).setType(BooleanType)
+ case ExOr(l, r) => Or(rec(l), rec(r)).setType(BooleanType)
+ case ExNot(e) => Not(rec(e)).setType(BooleanType)
+ case ExUMinus(e) => UMinus(rec(e)).setType(Int32Type)
+ case ExPlus(l, r) => Plus(rec(l), rec(r)).setType(Int32Type)
+ case ExMinus(l, r) => Minus(rec(l), rec(r)).setType(Int32Type)
+ case ExTimes(l, r) => Times(rec(l), rec(r)).setType(Int32Type)
+ case ExDiv(l, r) => Division(rec(l), rec(r)).setType(Int32Type)
+ case ExEquals(l, r) => Equals(rec(l), rec(r)).setType(BooleanType)
+ case ExGreaterThan(l, r) => GreaterThan(rec(l), rec(r)).setType(BooleanType)
+ case ExGreaterEqThan(l, r) => GreaterEquals(rec(l), rec(r)).setType(BooleanType)
+ case ExLessThan(l, r) => LessThan(rec(l), rec(r)).setType(BooleanType)
+ case ExLessEqThan(l, r) => LessEquals(rec(l), rec(r)).setType(BooleanType)
+ case ExIfThenElse(t1,t2,t3) => {
+ val r1 = rec(t1)
+ val r2 = rec(t2)
+ val r3 = rec(t3)
+ IfExpr(r1, r2, r3).setType(leastUpperBound(r2.getType, r3.getType))
}
- case ExAnd(l, r) => And(rec(l), rec(r))
- case ExOr(l, r) => Or(rec(l), rec(r))
- case ExNot(e) => Not(rec(e))
- case ExUMinus(e) => UMinus(rec(e))
- case ExPlus(l, r) => Plus(rec(l), rec(r))
- case ExMinus(l, r) => Minus(rec(l), rec(r))
- case ExTimes(l, r) => Times(rec(l), rec(r))
- case ExDiv(l, r) => Division(rec(l), rec(r))
- case ExEquals(l, r) => Equals(rec(l), rec(r))
- case ExGreaterThan(l, r) => GreaterThan(rec(l), rec(r))
- case ExGreaterEqThan(l, r) => GreaterEquals(rec(l), rec(r))
- case ExLessThan(l, r) => LessThan(rec(l), rec(r))
- case ExLessEqThan(l, r) => LessEquals(rec(l), rec(r))
- case ExIfThenElse(t1,t2,t3) => IfExpr(rec(t1), rec(t2), rec(t3))
case ExLocalCall(sy,nm,ar) => {
if(defsToDefs.keysIterator.find(_ == sy).isEmpty) {
- unit.error(tr.pos, "Invoking an invalid function.")
+ if(!silent)
+ unit.error(tr.pos, "Invoking an invalid function.")
+ throw ImpureCodeEncounteredException(tr)
+ }
+ val fd = defsToDefs(sy)
+ FunctionInvocation(fd, ar.map(rec(_))).setType(fd.returnType)
+ }
+ case ExPatternMatching(sel, cses) => {
+ val rs = rec(sel)
+ val rc = cses.map(rewriteCaseDef(_))
+ val rt: purescala.TypeTrees.TypeTree = rc.map(_.rhs.getType).reduceLeft(leastUpperBound(_,_))
+ MatchExpr(rs, rc).setType(rt)
+ }
+
+ // this one should stay after all others, cause it also catches UMinus
+ // and Not, for instance.
+ case ExParameterlessMethodCall(t,n) => {
+ val selector = rec(t)
+ val selType = selector.getType
+
+ if(!selType.isInstanceOf[CaseClassType]) {
+ if(!silent)
+ unit.error(tr.pos, "Invalid method or field invocation (not purescala?)")
+ throw ImpureCodeEncounteredException(tr)
}
- FunctionInvocation(defsToDefs(sy), ar.map(rec(_)))
+
+ val selDef: CaseClassDef = selType.asInstanceOf[CaseClassType].classDef
+
+ val fieldID = selDef.fields.find(_.id.name == n.toString) match {
+ case None => {
+ if(!silent)
+ unit.error(tr.pos, "Invalid method or field invocation (not a case class arg?)")
+ throw ImpureCodeEncounteredException(tr)
+ }
+ case Some(vd) => vd.id
+ }
+
+ CaseClassSelector(selector, fieldID).setType(fieldID.getType)
}
// default behaviour is to complain :)
@@ -319,10 +382,7 @@ trait CodeExtraction extends Extractors {
case tpe if tpe == IntClass.tpe => Int32Type
case tpe if tpe == BooleanClass.tpe => BooleanType
case TypeRef(_, sym, btt :: Nil) if sym == setTraitSym => SetType(rec(btt))
- case TypeRef(_, sym, Nil) if classesToClasses.keySet.contains(sym) => classesToClasses(sym) match {
- case a: AbstractClassDef => AbstractClassType(a)
- case c: CaseClassDef => CaseClassType(c)
- }
+ case TypeRef(_, sym, Nil) if classesToClasses.keySet.contains(sym) => classDefToClassType(classesToClasses(sym))
case _ => {
if(!silent) {
diff --git a/src/funcheck/Extractors.scala b/src/funcheck/Extractors.scala
index d4acfe254e98fe2e45309a28331b4b539e0cc25a..7fba429eb44c65022a17fd0ffcd4fc97e89c7d3b 100644
--- a/src/funcheck/Extractors.scala
+++ b/src/funcheck/Extractors.scala
@@ -23,7 +23,7 @@ trait Extractors {
object ExEnsuredExpression {
/** Extracts the 'ensuring' contract from an expression. */
- def unapply(tree: Apply): Option[(Tree,String,Tree)] = tree match {
+ def unapply(tree: Apply): Option[(Tree,Symbol,Tree)] = tree match {
case Apply(
Select(
Apply(
@@ -32,9 +32,8 @@ trait Extractors {
TypeTree() :: Nil),
body :: Nil),
ensuringName),
- (anonymousFun @ Function(ValDef(_, resultName, resultType, EmptyTree) :: Nil,
- contractBody)) :: Nil)
- if("ensuring".equals(ensuringName.toString)) => Some((body, resultName.toString, contractBody))
+ (Function((vd @ ValDef(_, _, _, EmptyTree)) :: Nil, contractBody)) :: Nil)
+ if("ensuring".equals(ensuringName.toString)) => Some((body, vd.symbol, contractBody))
case _ => None
}
}
@@ -155,8 +154,8 @@ trait Extractors {
}
object ExIdentifier {
- def unapply(tree: Ident): Option[(String,Tree)] = tree match {
- case i: Ident => Some((i.symbol.name.toString, i))
+ def unapply(tree: Ident): Option[(Symbol,Tree)] = tree match {
+ case i: Ident => Some((i.symbol, i))
case _ => None
}
}
@@ -274,5 +273,18 @@ trait Extractors {
case _ => None
}
}
+
+ // used for case classes selectors.
+ object ExParameterlessMethodCall {
+ def unapply(tree: Select): Option[(Tree,Name)] = tree match {
+ case Select(lhs, n) => Some((lhs, n))
+ case _ => None
+ }
+ }
+
+ object ExPatternMatching {
+ def unapply(tree: Match): Option[(Tree,List[CaseDef])] =
+ if(tree != null) Some((tree.selector, tree.cases)) else None
+ }
}
}
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 9c1ad9a6df5c7f16210d02e3dd813f0d2e79a7fc..9026ed4d24eb0b020f63f2ad9890ffe7451f041b 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -15,13 +15,17 @@ class FunCheckPlugin(val global: Global) extends Plugin {
/** The help message displaying the options for that plugin. */
override val optionsHelp: Option[String] = Some(
- " -P:funcheck:with-code Allows the compiler to keep running after the static analysis")
+ " -P:funcheck:uniqid When pretty-printing funcheck trees, show identifiers IDs" +
+ "\n" +
+ " -P:funcheck:with-code Allows the compiler to keep running after the static analysis"
+ )
/** Processes the command-line options. */
override def processOptions(options: List[String], error: String => Unit) {
for(option <- options) {
option match {
case "with-code" => stopAfterAnalysis = false
+ case "uniqid" => purescala.Settings.showIDs = true
case _ => error("Invalid option: " + option)
}
}
diff --git a/src/purescala/Common.scala b/src/purescala/Common.scala
index cfbe10b3a158cd49301e058a11cfdc5d4894d772..ddb2129e10913f3b875af0a5d8c85d7b7ce4b1a6 100644
--- a/src/purescala/Common.scala
+++ b/src/purescala/Common.scala
@@ -1,5 +1,39 @@
package purescala
object Common {
- type Identifier = String
+ import TypeTrees.Typed
+
+ // the type is left blank (NoType) for Identifiers that are not variables
+ class Identifier private[Common](val name: String, val id: Int) extends Typed {
+ override def equals(other: Any): Boolean = {
+ if(other == null || !other.isInstanceOf[Identifier])
+ false
+ else
+ other.asInstanceOf[Identifier].id == this.id
+ }
+
+ override def hashCode: Int = id
+
+ override def toString: String = {
+ if(purescala.Settings.showIDs) {
+ // angle brackets: name + "\u3008" + id + "\u3009"
+ name + "[" + id + "]"
+ } else {
+ name
+ }
+ }
+ }
+
+ private object UniqueCounter {
+ private var soFar: Int = -1
+
+ def next: Int = {
+ soFar = soFar + 1
+ soFar
+ }
+ }
+
+ object FreshIdentifier {
+ def apply(name: String) : Identifier = new Identifier(name, UniqueCounter.next)
+ }
}
diff --git a/src/purescala/Definitions.scala b/src/purescala/Definitions.scala
index cae4ba43106c57a04dd48533c8ef897d4d5cf086..837478e2500e98179687976c7eb694e833f194b6 100644
--- a/src/purescala/Definitions.scala
+++ b/src/purescala/Definitions.scala
@@ -5,50 +5,13 @@ object Definitions {
import Trees._
import TypeTrees._
- private object UniqueID {
- import scala.collection.mutable.HashMap
-
- private val counts: HashMap[String,Int] = new HashMap[String,Int]
-
- def apply(prefix: String): Int = {
- val count = counts.getOrElse(prefix, 0)
- counts(prefix) = count + 1
- count
- }
- }
-
- /** Scopes add new definitions to the surrounding scope. */
- // trait Scope {
- // import scala.collection.immutable.Map
-
- // def parentScope: Option[Scope] = None
- // def lookupVar(id: Identifier): Option[VarDecl] = None
- // def lookupObject(id: Identifier): Option[ObjectDef] = None
- // def lookupClassType(id: Identifier): Option[ClassTypeDef] = None
- // def lookupAbstractClass(id: Identifier): Option[AbstractClassDef] = None
- // def lookupCaseClass(id: Identifier): Option[CaseClassDef] = None
- // def lookupClass(id: Identifier): Option[ClassDef] = None
- // def lookupFun(id: Identifier): Option[FunDef] = None
- // }
-
- /** A declaration is anything "structural", ie. anything that's part of the
- * syntax of a program but not in an expression. */
- sealed abstract class Definition /*extends Scope*/ {
+ sealed abstract class Definition {
val id: Identifier
override def toString: String = PrettyPrinter(this)
}
/** A VarDecl declares a new identifier to be of a certain type. */
case class VarDecl(id: Identifier, tpe: TypeTree) extends Typed {
- val uniqueID: Int = UniqueID(id.toString)
-
- override val toString: String = id + uniqueID
-
- override def equals(other: Any) = other match {
- case v: VarDecl => this.equals(v) && uniqueID == v.uniqueID
- case _ => false
- }
-
override def getType = tpe
override def setType(tt: TypeTree) = scala.Predef.error("Can't set type of VarDecl.")
}
@@ -57,17 +20,7 @@ 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 {
- //override val parentScope = None
-
- // override def lookupObject(id: Identifier) = {
- // if(id == mainObject.id) {
- // Some(mainObject)
- // } else {
- // None
- // }
- // }
- }
+ case class Program(id: Identifier, mainObject: ObjectDef) extends Definition
/** Objects work as containers for class definitions, functions (def's) and
* val's. */
diff --git a/src/purescala/PrettyPrinter.scala b/src/purescala/PrettyPrinter.scala
index 574ae4423c9312afb765a51f115359ddda61f8e9..8f6a5b9562e6c453912f38acb51ce6080cd9baac 100644
--- a/src/purescala/PrettyPrinter.scala
+++ b/src/purescala/PrettyPrinter.scala
@@ -12,12 +12,12 @@ object PrettyPrinter {
import java.lang.StringBuffer
def apply(tree: Expr): String = {
- val retSB = pp(tree, new StringBuffer)
+ val retSB = pp(tree, new StringBuffer, 0)
retSB.toString
}
def apply(tpe: TypeTree): String = {
- val retSB = pp(tpe, new StringBuffer)
+ val retSB = pp(tpe, new StringBuffer, 0)
retSB.toString
}
@@ -26,82 +26,125 @@ object PrettyPrinter {
retSB.toString
}
+ private def ind(sb: StringBuffer, lvl: Int) : StringBuffer = {
+ sb.append(" " * lvl)
+ sb
+ }
+
// EXPRESSIONS
// all expressions are printed in-line
- private def ppUnary(sb: StringBuffer, expr: Expr, op: String): StringBuffer = {
+ private def ppUnary(sb: StringBuffer, expr: Expr, op: String, lvl: Int): StringBuffer = {
var nsb: StringBuffer = sb
nsb.append(op)
nsb.append("(")
- nsb = pp(expr, nsb)
+ nsb = pp(expr, nsb, lvl)
nsb.append(")")
nsb
}
- private def ppBinary(sb: StringBuffer, left: Expr, right: Expr, op: String): StringBuffer = {
+ private def ppBinary(sb: StringBuffer, left: Expr, right: Expr, op: String, lvl: Int): StringBuffer = {
var nsb: StringBuffer = sb
nsb.append("(")
- nsb = pp(left, nsb)
+ nsb = pp(left, nsb, lvl)
nsb.append(op)
- nsb = pp(right, nsb)
+ nsb = pp(right, nsb, lvl)
nsb.append(")")
nsb
}
- private def ppNary(sb: StringBuffer, exprs: Seq[Expr], op: String): StringBuffer = {
+ private def ppNary(sb: StringBuffer, exprs: Seq[Expr], op: String, lvl: Int): StringBuffer = {
var nsb = sb
nsb.append("(")
val sz = exprs.size
var c = 0
exprs.foreach(ex => {
- nsb = pp(ex, nsb) ; c += 1 ; if(c < sz) nsb.append(op)
+ nsb = pp(ex, nsb, lvl) ; c += 1 ; if(c < sz) nsb.append(op)
})
nsb.append(")")
nsb
}
- private def pp(tree: Expr, sb: StringBuffer): StringBuffer = tree match {
+ private def pp(tree: Expr, sb: StringBuffer, lvl: Int): StringBuffer = tree match {
case Variable(id) => sb.append(id)
- case And(exprs) => ppNary(sb, exprs, " \u2227 ") // \land
- case Or(exprs) => ppNary(sb, exprs, " \u2228 ") // \lor
- case Not(Equals(l, r)) => ppBinary(sb, l, r, " \u2260 ") // \neq
- case Not(expr) => ppUnary(sb, expr, "\u00AC") // \neg
- case UMinus(expr) => ppUnary(sb, expr, "-")
- case Equals(l,r) => ppBinary(sb, l, r, " == ")
+ case And(exprs) => ppNary(sb, exprs, " \u2227 ", lvl) // \land
+ case Or(exprs) => ppNary(sb, exprs, " \u2228 ", lvl) // \lor
+ case Not(Equals(l, r)) => ppBinary(sb, l, r, " \u2260 ", lvl) // \neq
+ case Not(expr) => ppUnary(sb, expr, "\u00AC", lvl) // \neg
+ case UMinus(expr) => ppUnary(sb, expr, "-", lvl)
+ case Equals(l,r) => ppBinary(sb, l, r, " == ", lvl)
case IntLiteral(v) => sb.append(v)
case BooleanLiteral(v) => sb.append(v)
case StringLiteral(s) => sb.append("\"" + s + "\"")
case CaseClass(ct, args) => {
var nsb = sb
nsb.append(ct.id)
- nsb = ppNary(nsb, args, ", ")
+ nsb = ppNary(nsb, args, ", ", lvl)
nsb
}
+ case CaseClassSelector(cc, id) => pp(cc, sb, lvl).append("." + id)
case FunctionInvocation(fd, args) => {
var nsb = sb
nsb.append(fd.id)
- nsb = ppNary(nsb, args, ", ")
+ nsb = ppNary(nsb, args, ", ", lvl)
nsb
}
- case Plus(l,r) => ppBinary(sb, l, r, " + ")
- case Minus(l,r) => ppBinary(sb, l, r, " - ")
- case Times(l,r) => ppBinary(sb, l, r, " * ")
- case Division(l,r) => ppBinary(sb, l, r, " / ")
- case LessThan(l,r) => ppBinary(sb, l, r, " < ")
- case GreaterThan(l,r) => ppBinary(sb, l, r, " > ")
- case LessEquals(l,r) => ppBinary(sb, l, r, " \u2264 ") // \leq
- case GreaterEquals(l,r) => ppBinary(sb, l, r, " \u2265 ") // \geq
+ case Plus(l,r) => ppBinary(sb, l, r, " + ", lvl)
+ case Minus(l,r) => ppBinary(sb, l, r, " - ", lvl)
+ case Times(l,r) => ppBinary(sb, l, r, " * ", lvl)
+ case Division(l,r) => ppBinary(sb, l, r, " / ", lvl)
+ case LessThan(l,r) => ppBinary(sb, l, r, " < ", lvl)
+ case GreaterThan(l,r) => ppBinary(sb, l, r, " > ", lvl)
+ case LessEquals(l,r) => ppBinary(sb, l, r, " \u2264 ", lvl) // \leq
+ case GreaterEquals(l,r) => ppBinary(sb, l, r, " \u2265 ", lvl) // \geq
case IfExpr(c, t, e) => {
var nsb = sb
nsb.append("if (")
- nsb = pp(c, nsb)
- nsb.append(") { ")
- nsb.append(t)
- nsb.append(" } else { ")
- nsb.append(e)
- nsb.append(" }")
+ nsb = pp(c, nsb, lvl)
+ nsb.append(") {\n")
+ ind(nsb, lvl+1)
+ nsb = pp(t, nsb, lvl+1)
+ nsb.append("\n")
+ ind(nsb, lvl)
+ nsb.append("} else {\n")
+ ind(nsb, lvl+1)
+ nsb = pp(e, nsb, lvl+1)
+ nsb.append("\n")
+ ind(nsb, lvl)
+ nsb.append("}")
+ nsb
+ }
+
+ case MatchExpr(s, csc) => {
+ def ppc(sb: StringBuffer, p: Pattern): StringBuffer = p match {
+ //case InstanceOfPattern(None, ctd) =>
+ //case InstanceOfPattern(Some(id), ctd) =>
+ //case CaseClassPattern(None, ccd, subps) =>
+ //case CaseClassPattern(Some(id), ccd, subps) =>
+ case WildcardPattern(None) => sb.append("_")
+ case WildcardPattern(Some(id)) => sb.append(id)
+ case _ => sb.append("Pattern?")
+ }
+
+ var nsb = sb
+ nsb == pp(s, nsb, lvl)
+ nsb.append(" match {\n")
+
+ csc.foreach(cs => {
+ ind(nsb, lvl+1)
+ nsb.append("case ")
+ nsb = ppc(nsb, cs.pattern)
+ cs.theGuard.foreach(g => {
+ nsb.append(" if ")
+ nsb = pp(g, nsb, lvl+1)
+ })
+ nsb.append(" => ")
+ nsb = pp(cs.rhs, nsb, lvl+1)
+ nsb.append("\n")
+ })
+ ind(nsb, lvl).append("}")
nsb
}
@@ -112,10 +155,11 @@ object PrettyPrinter {
// TYPE TREES
// all type trees are printed in-line
- private def pp(tpe: TypeTree, sb: StringBuffer): StringBuffer = tpe match {
+ private def pp(tpe: TypeTree, sb: StringBuffer, lvl: Int): StringBuffer = tpe match {
+ case NoType => sb.append("???")
case Int32Type => sb.append("Int")
case BooleanType => sb.append("Boolean")
- case SetType(bt) => pp(bt, sb.append("Set[")).append("]")
+ case SetType(bt) => pp(bt, sb.append("Set["), lvl).append("]")
case c: ClassType => sb.append(c.classDef.id)
case _ => sb.append("Type?")
}
@@ -123,9 +167,6 @@ object PrettyPrinter {
// DEFINITIONS
// all definitions are printed with an end-of-line
private def pp(defn: Definition, sb: StringBuffer, lvl: Int): StringBuffer = {
- def ind(sb: StringBuffer, customLevel: Int = lvl) : Unit = {
- sb.append(" " * customLevel)
- }
defn match {
case Program(id, mainObj) => {
@@ -138,7 +179,7 @@ object PrettyPrinter {
case ObjectDef(id, defs, invs) => {
var nsb = sb
- ind(nsb)
+ ind(nsb, lvl)
nsb.append("object ")
nsb.append(id)
nsb.append(" {\n")
@@ -149,17 +190,18 @@ object PrettyPrinter {
defs.foreach(df => {
nsb = pp(df, nsb, lvl+1)
if(c < sz - 1) {
- nsb.append("\n")
+ nsb.append("\n\n")
}
c = c + 1
})
- ind(nsb); nsb.append("}\n")
+ nsb.append("\n")
+ ind(nsb, lvl).append("}\n")
}
case AbstractClassDef(id, parent) => {
var nsb = sb
- ind(nsb)
+ ind(nsb, lvl)
nsb.append("sealed abstract class ")
nsb.append(id)
parent.foreach(p => nsb.append(" extends " + p.id))
@@ -168,7 +210,7 @@ object PrettyPrinter {
case CaseClassDef(id, parent, varDecls) => {
var nsb = sb
- ind(nsb)
+ ind(nsb, lvl)
nsb.append("case class ")
nsb.append(id)
nsb.append("(")
@@ -176,9 +218,9 @@ object PrettyPrinter {
val sz = varDecls.size
varDecls.foreach(vd => {
- nsb.append(vd.id.toString)
+ nsb.append(vd.id)
nsb.append(": ")
- nsb = pp(vd.tpe, nsb)
+ nsb = pp(vd.tpe, nsb, lvl)
if(c < sz - 1) {
nsb.append(", ")
}
@@ -193,20 +235,20 @@ object PrettyPrinter {
var nsb = sb
pre.foreach(prec => {
- ind(nsb)
+ ind(nsb, lvl)
nsb.append("@pre : ")
- nsb = pp(prec, nsb)
+ nsb = pp(prec, nsb, lvl)
nsb.append("\n")
})
post.foreach(postc => {
- ind(nsb)
+ ind(nsb, lvl)
nsb.append("@post: ")
- nsb = pp(postc, nsb)
+ nsb = pp(postc, nsb, lvl)
nsb.append("\n")
})
- ind(nsb)
+ ind(nsb, lvl)
nsb.append("def ")
nsb.append(id)
nsb.append("(")
@@ -217,7 +259,7 @@ object PrettyPrinter {
args.foreach(arg => {
nsb.append(arg.id)
nsb.append(" : ")
- nsb = pp(arg.tpe, nsb)
+ nsb = pp(arg.tpe, nsb, lvl)
if(c < sz - 1) {
nsb.append(", ")
@@ -226,15 +268,9 @@ object PrettyPrinter {
})
nsb.append(") : ")
- nsb = pp(rt, nsb)
- nsb.append(" = {\n")
-
- ind(nsb, lvl+1)
- nsb = pp(body, nsb)
- nsb.append("\n")
-
- ind(nsb)
- nsb.append("}\n")
+ nsb = pp(rt, nsb, lvl)
+ nsb.append(" = ")
+ pp(body, nsb, lvl)
}
case _ => sb.append("Defn?")
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index b89a6ac1ef3d6cfe33ae454a5a6463601beb6862..17883d57b8e43da5c970f61f148ec2eb51440ec3 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -20,17 +20,23 @@ object Trees {
sealed abstract class MatchCase {
val pattern: Pattern
val rhs: Expr
+ val theGuard: Option[Expr]
}
- case class SimpleCase(pattern: Pattern, rhs: Expr) extends MatchCase
- case class GuardedCase(pattern: Pattern, guard: Expr, rhs: Expr) extends MatchCase
+ case class SimpleCase(pattern: Pattern, rhs: Expr) extends MatchCase {
+ val theGuard = None
+ }
+ case class GuardedCase(pattern: Pattern, guard: Expr, rhs: Expr) extends MatchCase {
+ val theGuard = Some(guard)
+ }
sealed abstract class Pattern
case class InstanceOfPattern(binder: Option[Identifier], classTypeDef: ClassTypeDef) extends Pattern // c: Class
case class WildcardPattern(binder: Option[Identifier]) extends Pattern // c @ _
- case class ExtractorPattern(binder: Option[Identifier],
- extractor : ExtractorTypeDef,
- subPatterns: Seq[Pattern]) extends Pattern // c @ Extractor(...,...)
+ case class CaseClassPattern(binder: Option[Identifier], caseClassDef: CaseClassDef, subPatterns: Seq[Pattern]) extends Pattern
+ // case class ExtractorPattern(binder: Option[Identifier],
+ // extractor : ExtractorTypeDef,
+ // subPatterns: Seq[Pattern]) extends Pattern // c @ Extractor(...,...)
// We don't handle Seq stars for now.
/* Propositional logic */
@@ -60,9 +66,10 @@ object Trees {
case class Equals(left: Expr, right: Expr) extends Expr
/* Literals */
- // to be fixed! Should contain a reference to the definition of that
- // variable, which would also give us its type.
- case class Variable(id: Identifier) extends Expr
+ case class Variable(id: Identifier) extends Expr {
+ override def getType = id.getType
+ override def setType(tt: TypeTree) = { id.setType(tt); this }
+ }
// represents the result in post-conditions
case class ResultVariable() extends Expr
@@ -75,7 +82,8 @@ object Trees {
case class BooleanLiteral(value: Boolean) extends Literal[Boolean]
case class StringLiteral(value: String) extends Literal[String]
- case class CaseClass(classType: CaseClassType, args: Seq[Expr]) extends Expr
+ case class CaseClass(classDef: CaseClassDef, args: Seq[Expr]) extends Expr
+ case class CaseClassSelector(caseClass: Expr, selector: Identifier) extends Expr
/* Arithmetic */
case class Plus(lhs: Expr, rhs: Expr) extends Expr
diff --git a/src/purescala/TypeTrees.scala b/src/purescala/TypeTrees.scala
index 35740fbaa08455b0ea7a5fd1faf4a13179bc48fd..1e7c115bdec57567f6a0c0f9ff660216b4e363f3 100644
--- a/src/purescala/TypeTrees.scala
+++ b/src/purescala/TypeTrees.scala
@@ -25,6 +25,41 @@ object TypeTrees {
override def toString: String = PrettyPrinter(this)
}
+ def leastUpperBound(t1: TypeTree, t2: TypeTree): TypeTree = (t1,t2) match {
+ case (c1: ClassType, c2: ClassType) => {
+ import scala.collection.immutable.Set
+ var c: ClassTypeDef = c1.classDef
+ var visited: Set[ClassTypeDef] = Set(c)
+
+ while(c.parent.isDefined) {
+ c = c.parent.get
+ visited = visited ++ Set(c)
+ }
+
+ c = c2.classDef
+ var found: Option[ClassTypeDef] = if(visited.contains(c)) {
+ Some(c)
+ } else {
+ None
+ }
+
+ while(found.isEmpty && c.parent.isDefined) {
+ c = c.parent.get
+ if(visited.contains(c))
+ found = Some(c)
+ }
+
+ if(found.isEmpty) {
+ scala.Predef.error("Asking for lub of unrelated class types : " + t1 + " and " + t2)
+ } else {
+ classDefToClassType(found.get)
+ }
+ }
+
+ case (o1, o2) if (o1 == o2) => o1
+ case _ => scala.Predef.error("Asking for lub of unrelated types: " + t1 + " and " + t2)
+ }
+
case object NoType extends TypeTree
case object AnyType extends TypeTree
@@ -37,13 +72,17 @@ object TypeTrees {
case class SetType(base: TypeTree) extends TypeTree
// case class MultisetType(base: TypeTree) extends TypeTree
case class MapType(from: TypeTree, to: TypeTree) extends TypeTree
+ case class OptionType(base: TypeTree) extends TypeTree
sealed abstract class ClassType extends TypeTree {
val classDef: ClassTypeDef
val id: Identifier = classDef.id
}
-
case class AbstractClassType(classDef: AbstractClassDef) extends ClassType
- case class CaseClassType(classDef: CaseClassDef) extends ClassType
- case class OptionType(base: TypeTree) extends TypeTree
+ case class CaseClassType(classDef: CaseClassDef) extends ClassType
+
+ def classDefToClassType(cd: ClassTypeDef): ClassType = cd match {
+ case a: AbstractClassDef => AbstractClassType(a)
+ case c: CaseClassDef => CaseClassType(c)
+ }
}