diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index 1563e5251bb87a62d8b1ae3127f4eb2795719168..c63e61cd43709e0ffc9fd76d82fd2839ac94c5e0 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -21,32 +21,45 @@ trait CodeExtraction extends Extractors {
case None => stopIfErrors; throw new Error("unreachable")
}
- def trav(tree: Tree): Unit = tree match {
- case t : Tree if t.symbol != null && t.symbol.hasFlag(symtab.Flags.SYNTHETIC) => {
- println("Synth! " + t)
- }
- case d @ DefDef(mods, name, tparams, vparamss, tpt, body) if !(d.symbol.hasFlag(symtab.Flags.SYNTHETIC) || d.symbol.isConstructor) => {
- println("In: " + name)
- println(d.symbol)
- println(d.mods)
-
- toPureScala(unit)(body) match {
- case Some(t) => println(" the body was extracted as: " + t)
- case None => println(" the body could not be extracted. Is it pure Scala?")
- }
- }
- case _ => ;
- }
+// def trav(tree: Tree): Unit = tree match {
+// case t : Tree if t.symbol != null && t.symbol.hasFlag(symtab.Flags.SYNTHETIC) => {
+// println("Synth! " + t)
+// }
+// case d @ DefDef(mods, name, tparams, vparamss, tpt, body) if !(d.symbol.hasFlag(symtab.Flags.SYNTHETIC) || d.symbol.isConstructor) => {
+// println("In: " + name)
+// println(d.symbol)
+// println(d.mods)
+//
+// toPureScala(unit)(body) match {
+// case Some(t) => println(" the body was extracted as: " + t)
+// case None => println(" the body could not be extracted. Is it pure Scala?")
+// }
+// }
+// case _ => ;
+// }
- // Finds all vals in a template
+ def extractObject(name: Identifier, tmpl: Template): ObjectDef = {
+ var funDefs: List[FunDef] = Nil
+ var valDefs: List[ValDef] = Nil
+ var asserts: List[Expr] = Nil
- // Finds all defs in a template
+ val tTrees: List[Tree] = tmpl.body
- // Finds all class definitions in a template
+ println(tTrees)
- // Finds all assertions in a template
+ tTrees.foreach(tree => tree match {
+ case cd @ ClassDef(_, name, tparams, impl) => {
+ println("--- " + name.toString)
+ println(cd.symbol.info)
+ println(cd.symbol.info.parents)
+ }
+ case _ => ;
+ })
- // Extraction of the program.
+ ObjectDef(name, Nil, Nil)
+ }
+
+ // Extraction of the definitions.
val program = unit.body match {
case p @ PackageDef(name, lst) if lst.size == 0 => {
unit.error(p.pos, "No top-level definition found.")
@@ -61,14 +74,16 @@ trait CodeExtraction extends Extractors {
case PackageDef(name, lst) => {
assert(lst.size == 1)
lst(0) match {
- case ExObjectDef(n, templ) => Some(Program(name.toString, ObjectDef(n.toString, Nil, Nil)))
+ case ExObjectDef(n, templ) => Some(Program(name.toString, extractObject(n.toString, templ)))
case other @ _ => unit.error(other.pos, "Expected: top-level single object.")
None
}
}
}
- (new ForeachTreeTraverser(trav)).traverse(unit.body)
+ // Extraction of the expressions.
+
+// (new ForeachTreeTraverser(trav)).traverse(unit.body)
stopIfErrors
program.get
diff --git a/src/funcheck/Extractors.scala b/src/funcheck/Extractors.scala
index cd44ac23c68213c2fef7aa4ef0ebd76c5509fb08..69fe4dec6cbee58317acf6ba3968fa038ece6d19 100644
--- a/src/funcheck/Extractors.scala
+++ b/src/funcheck/Extractors.scala
@@ -58,6 +58,22 @@ trait Extractors {
}
}
+ object ExAbstractClass {
+ /** Matches an abstract class with no type parameters, no constructor
+ * arguments, at most one parent class and an empty template. (Does _not_
+ * match such a trait). */
+ def unapply(cd: ClassDef): Option[(String)] = cd match {
+ case _ => None
+ }
+ }
+
+ object ExCaseClass {
+ /** Matches a case class definition with no type parameters, at most one
+ * parent class and an empty template. */
+
+
+ }
+
object ExFunctionDef {
/** Matches a function with a single list of arguments, no type
* parameters and regardless of its visibility. */
diff --git a/src/funcheck/purescala/Definitions.scala b/src/funcheck/purescala/Definitions.scala
index 3debcbc321b9084262ada42e7a9096e228007210..dc5d6a2069033c62c07ab4174e64ada7dda19006 100644
--- a/src/funcheck/purescala/Definitions.scala
+++ b/src/funcheck/purescala/Definitions.scala
@@ -5,32 +5,53 @@ 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
- val parentScope: Option[Scope] = None
+ 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 lookupVal(id: Identifier): Option[ValDef] = None
def lookupFun(id: Identifier): Option[FunDef] = None
}
- /** A definition is anything "structural", ie. anything that's part of the
+ /** 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 {
val id: Identifier
override def toString: String = PrettyPrinter(this)
}
- final case class VarDecl(id: Identifier, tpe: TypeTree)
+ /** A VarDecl declares a new identifier to be of a certain type. */
+ final case class VarDecl(id: Identifier, tpe: TypeTree) {
+ 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
+ }
+ }
+
type VarDecls = Seq[VarDecl]
/** A wrapper for a program. For now a program is simply a single object. The
- * name is meaningless and we can just the package name. */
+ * name is meaningless and we just use the package name. */
final case class Program(id: Identifier, mainObject: ObjectDef) extends Definition {
override val parentScope = None
@@ -45,7 +66,7 @@ object Definitions {
/** Objects work as containers for class definitions, functions (def's) and
* val's. */
- case class ObjectDef(id: Identifier, defs : Seq[Definition], invariants: Seq[Expr]) extends Definition
+ case class ObjectDef(id: Identifier, defs : Seq[Definition], invariants: Seq[Expr]) extends Definition
/** Useful because case classes and classes are somewhat unified in some
* patterns (of pattern-matching, that is) */
@@ -69,7 +90,9 @@ object Definitions {
case class ClassDef(id: Identifier, parent: Option[AbstractClassDef], fields: VarDecls) extends ClassTypeDef
/** Values */
- case class ValDef(id: Identifier, value: Expr) extends Definition
+ case class ValDef(varDecl: VarDecl, value: Expr) extends Definition {
+ val id: Identifier = varDecl.id
+ }
/** Functions (= 'methods' of objects) */
case class FunDef(id: Identifier, args: VarDecls, body: Expr, precondition: Option[Expr], postcondition: Option[Expr]) extends Definition {
diff --git a/src/funcheck/purescala/Trees.scala b/src/funcheck/purescala/Trees.scala
index c2086f23696f83ad0d67a98cc9bee9b1cd8e3c4c..7c1739e1bbd9572fb19edbc75eb892448de03ec1 100644
--- a/src/funcheck/purescala/Trees.scala
+++ b/src/funcheck/purescala/Trees.scala
@@ -16,13 +16,21 @@ object Trees {
sealed abstract class Expr extends Typed {
override def toString: String = PrettyPrinter(this)
- var _scope: Scope = null
+ private var _scope: Option[Scope] = None
def scope: Scope =
- if(_scope == null)
+ if(_scope.isEmpty)
throw new Exception("Undefined scope.")
else
- _scope
+ _scope.get
+
+ def scope_=(s: Scope): Unit = {
+ if(_scope.isEmpty) {
+ _scope = Some(s)
+ } else {
+ throw new Exception("Redefining scope.")
+ }
+ }
}
/**