Skip to content
Snippets Groups Projects
Commit 319f3c92 authored by Philippe Suter's avatar Philippe Suter
Browse files

starting to clean up

parent 88241dd7
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/funcheck/CodeExtraction.scala
+ 5
− 28
View file @ 319f3c92
......@@ -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 _ => ;
// }
}
src/funcheck/Extractors.scala
+ 7
− 0
View file @ 319f3c92
......@@ -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)
......
src/funcheck/purescala/PrettyPrinter.scala
+ 21
− 6
View file @ 319f3c92
......@@ -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(") : ")
......
src/funcheck/purescala/Symbols.scala deleted 100644 → 0
+ 0
− 103
View file @ 88241dd7
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
// }
// }
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment