diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index aee9044bbe68572b9c7fb74e26cd08e60bd6c05e..cd63fc299555c81cb3e88b223b3667b47aaa72ed 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -90,6 +90,8 @@ trait CodeExtraction extends Extractors {
var reqCont: Option[Expr] = None
var ensCont: Option[Expr] = None
+ val ps = params.map(p => VarDecl(p.name.toString, st2ps(p.tpt)))
+
realBody match {
case ExEnsuredExpression(body2, resId, contract) => {
varSubsts(resId) = (() => ResultVariable())
@@ -109,7 +111,7 @@ trait CodeExtraction extends Extractors {
case _ => ;
}
- FunDef(name, st2ps(tpt), Nil, s2ps(realBody), reqCont, ensCont)
+ FunDef(name, st2ps(tpt), ps, s2ps(realBody), reqCont, ensCont)
}
// THE EXTRACTION CODE STARTS HERE
@@ -153,7 +155,7 @@ trait CodeExtraction extends Extractors {
def rec(tr: Tree): Expr = tr match {
case ExInt32Literal(v) => IntLiteral(v)
case ExBooleanLiteral(v) => BooleanLiteral(v)
- case ExIntIdentifier(id) => varSubsts.get(id) match {
+ case ExIdentifier(id,tpt) => varSubsts.get(id) match {
case Some(fun) => fun()
case None => Variable(id)
}
@@ -181,6 +183,7 @@ trait CodeExtraction extends Extractors {
private def scalaType2PureScala(unit: CompilationUnit, silent: Boolean)(tree: Tree): funcheck.purescala.TypeTrees.TypeTree = {
tree match {
case tt: TypeTree if tt.tpe == IntClass.tpe => Int32Type
+ case tt: TypeTree if tt.tpe == BooleanClass.tpe => BooleanType
case _ => {
if(!silent) {
@@ -190,30 +193,4 @@ trait CodeExtraction extends Extractors {
}
}
}
-
-// def findContracts(tree: Tree): Unit = tree match {
-// case DefDef(/*mods*/ _, name, /*tparams*/ _, /*vparamss*/ _, /*tpt*/ _, body) => {
-// var realBody = body
-// var reqCont: Option[Tree] = None
-// var ensCont: Option[Function] = None
-//
-// body match {
-// case EnsuredExpression(body2, contract) => realBody = body2; ensCont = Some(contract)
-// case _ => ;
-// }
-//
-// realBody match {
-// case RequiredExpression(body3, contract) => realBody = body3; reqCont = Some(contract)
-// case _ => ;
-// }
-//
-// println("In: " + name)
-// println(" Requires clause: " + reqCont)
-// println(" Ensures clause: " + ensCont)
-// println(" Body: " + realBody)
-// }
-//
-// case _ => ;
-// }
-
}
diff --git a/src/funcheck/Extractors.scala b/src/funcheck/Extractors.scala
index 0e0d200dcb80fb7c069f5a25d5b2cabbff7ad863..81e17eaf196b5df21ccf9a5c4e487eb5dda63a26 100644
--- a/src/funcheck/Extractors.scala
+++ b/src/funcheck/Extractors.scala
@@ -120,6 +120,13 @@ trait Extractors {
}
}
+ object ExIdentifier {
+ def unapply(tree: Tree): Option[(String,Tree)] = tree match {
+ case i: Ident => Some((i.symbol.name.toString, i))
+ case _ => None
+ }
+ }
+
object ExIntIdentifier {
def unapply(tree: Tree): Option[String] = tree match {
case i: Ident if i.symbol.tpe == IntClass.tpe => Some(i.symbol.name.toString)
diff --git a/src/funcheck/purescala/PrettyPrinter.scala b/src/funcheck/purescala/PrettyPrinter.scala
index 35391e4edf679c61949b30d363f567bfddee30c7..6de4afa00952fb4f0f8d932fb98a2207e6d876a0 100644
--- a/src/funcheck/purescala/PrettyPrinter.scala
+++ b/src/funcheck/purescala/PrettyPrinter.scala
@@ -67,7 +67,7 @@ object PrettyPrinter {
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 Equals(l,r) => ppBinary(sb, l, r, " = ")
+ case Equals(l,r) => ppBinary(sb, l, r, " == ")
case IntLiteral(v) => sb.append(v)
case BooleanLiteral(v) => sb.append(v)
case Plus(l,r) => ppBinary(sb, l, r, " + ")
@@ -91,7 +91,7 @@ object PrettyPrinter {
nsb
}
- case ResultVariable() => sb.append("<res>")
+ case ResultVariable() => sb.append("#res")
case _ => sb.append("Expr?")
}
@@ -100,6 +100,7 @@ object PrettyPrinter {
// all type trees are printed in-line
private def pp(tpe: TypeTree, sb: StringBuffer): StringBuffer = tpe match {
case Int32Type => sb.append("Int")
+ case BooleanType => sb.append("Boolean")
case _ => sb.append("Type?")
}
@@ -126,11 +127,15 @@ object PrettyPrinter {
nsb.append(id)
nsb.append(" {\n")
- val sz = defs.size
var c = 0
+ val sz = defs.size
defs.foreach(df => {
- nsb = pp(df, nsb, lvl+1)
+ nsb = pp(df, nsb, lvl+1)
+ if(c < sz - 1) {
+ nsb.append("\n")
+ }
+ c = c + 1
})
ind(nsb); nsb.append("}\n")
@@ -158,8 +163,18 @@ object PrettyPrinter {
nsb.append(id)
nsb.append("(")
- args.foreach(a => {
- nsb.append("ARG ")
+ val sz = args.size
+ var c = 0
+
+ args.foreach(arg => {
+ nsb.append(arg.id)
+ nsb.append(" : ")
+ nsb = pp(arg.tpe, nsb)
+
+ if(c < sz - 1) {
+ nsb.append(", ")
+ }
+ c = c + 1
})
nsb.append(") : ")
diff --git a/src/funcheck/purescala/Symbols.scala b/src/funcheck/purescala/Symbols.scala
deleted file mode 100644
index b1c310f8feee1c581a4fbd0b0a0788885468c315..0000000000000000000000000000000000000000
--- a/src/funcheck/purescala/Symbols.scala
+++ /dev/null
@@ -1,103 +0,0 @@
-package funcheck.purescala
-
-import Common._
-import TypeTrees._
-
-object Symbols { /* dummy */ }
-
-/** There's a need for symbols, as we have purely functional trees with
- * potential recursive calls, and we want references to be resolved once and
- * for all. */
-// object Symbols {
-// trait Symbolic {
-// self =>
-//
-// private var __s: Option[Symbol] = None
-//
-// def symbol: Symbol = __s.getOrElse(throw new Exception("Undefined symbol."))
-//
-// def setSymbol(s: Symbol): self.type = __s match {
-// case Some(_) => throw new Exception("Symbol already set.")
-// case None => { __s = Some(s); this }
-// }
-// }
-//
-// sealed abstract class Symbol {
-// val id: Identifier
-// }
-//
-// class VariableSymbol(val id: Identifier, val tpe: TypeTree) extends Typed {
-// def getType = tpe
-// }
-//
-// // The object and class members have to be known at construction time. The
-// // typed members can be added anytime.
-// class ObjectSymbol(
-// val id: Identifier,
-// val classes: Seq[ClassSymbol],
-// val objects: Seq[ObjectSymbol]) extends Symbol {
-//
-// private var _fields: List[VariableSymbol] = Nil
-// private var _functions: List[FunctionSymbol] = Nil
-//
-// def fields: Seq[VariableSymbol] = _fields
-// def functions: Seq[FunctionSymbol] = _functions
-//
-// def registerField(f: VariableSymbol): ObjectSymbol = {
-// _fields = _fields ::: List(f)
-// this
-// }
-//
-// def registerFunction(f: FunctionSymbol): ObjectSymbol = {
-// _functions = _functions ::: List(f)
-// this
-// }
-//
-// override def toString: String = withInc(0)
-//
-// private def withInc(inc: Int): String = {
-// val ii: String = " " * inc
-// ii + "[object: " + id + "\n" +
-// (if(!fields.isEmpty) {
-// ii + " fields: " + fields.map(_.toString).mkString("{ ", ", ", " }") + "\n"
-// } else { "" }) +
-// (if(!functions.isEmpty) {
-// ii + " functions: " + functions.map(_.toString).mkString("{ ", ", ", " }") + "\n"
-// } else { "" }) +
-// (if(!classes.isEmpty) {
-// ii + " classes: " + classes.map(_.toString).mkString("{ ", ", ", " }") + "\n"
-// } else { "" }) +
-// (if(!objects.isEmpty) {
-// ii + " objects: " + objects.map(_.withInc(inc+1)).mkString("{\n", ",\n", "\n" + ii + " }") + "\n"
-// } else { "" }) +
-// ii + "]"
-// }
-// }
-//
-// sealed abstract class ClassSymbol extends Symbol {
-// val parents: Seq[AbstractClassSymbol]
-//
-// protected val _pfx: String
-//
-// override def toString = "[" + _pfx + ": " + id + (if (!parents.isEmpty) { " extends " + parents.mkString(", ") } else { "" }) + "]"
-// }
-//
-// /** Symbols for abstract classes (or traits) */
-// class AbstractClassSymbol(val id: Identifier, val parents: Seq[AbstractClassSymbol]) extends ClassSymbol {
-// override protected val _pfx = "abstract class"
-// }
-//
-// /** Symbols for "regular" (= non-abstract, non-case) classes */
-// class RefClassSymbol(val id: Identifier, val parents: Seq[AbstractClassSymbol]) extends ClassSymbol {
-// override protected val _pfx = "class"
-// }
-//
-// /** Symbols for case classes. */
-// class CaseClassSymbol(val id: Identifier, val parents: Seq[AbstractClassSymbol]) extends ClassSymbol {
-// override protected val _pfx = "case class"
-// }
-//
-// class FunctionSymbol(val id: Identifier, val params: Seq[VariableSymbol], val returnType: TypeTree) extends Typed {
-// def getType = returnType
-// }
-// }