From ed632f4da84b18eb36dfcc02e0e9e617082cea10 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 26 Apr 2010 19:27:57 +0000
Subject: [PATCH] still in the
"breaking-before-I'll-fix-it-all-again-and-like-will-be-wonderful-with-rainbows-and-unicorns"
phase.
---
src/funcheck/CodeExtraction.scala | 14 +-
src/funcheck/purescala/Definitions.scala | 11 +-
src/funcheck/purescala/Symbols.scala | 188 ++++++------
src/funcheck/purescala/Trees.scala | 357 +++++------------------
src/funcheck/purescala/TypeTrees.scala | 18 +-
5 files changed, 198 insertions(+), 390 deletions(-)
diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index e50d91ffe..b9b50f6cc 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -19,7 +19,7 @@ trait CodeExtraction extends Extractors {
import scala.collection.mutable.HashMap
// register where the symbols where extracted from
- val symbolDefMap = new HashMap[purescala.Symbols.Symbol,Tree]
+ // val symbolDefMap = new HashMap[purescala.Symbols.Symbol,Tree]
def s2ps(tree: Tree): Expr = toPureScala(unit)(tree) match {
case Some(ex) => ex
@@ -28,7 +28,7 @@ trait CodeExtraction extends Extractors {
/** Populates the symbolDefMap with object and class symbols, and returns
* the symbol corresponding to the expected single top-level object. */
- def extractClassSymbols: purescala.Symbols.ObjectSymbol = {
+ def extractClassSymbols: ObjectDef = {
val top = unit.body match {
case p @ PackageDef(name, lst) if lst.size == 0 => {
unit.error(p.pos, "No top-level definition found.")
@@ -54,13 +54,13 @@ trait CodeExtraction extends Extractors {
top.get
}
- def extractObjectSym(name: Identifier, tmpl: Template): purescala.Symbols.ObjectSymbol = {
+ def extractObjectSym(name: Identifier, 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)
- var classSyms: List[purescala.Symbols.ClassSymbol] = Nil
- var objectSyms: List[purescala.Symbols.ObjectSymbol] = Nil
+ var classDefs: List[ClassTypeDef] = Nil
+ var objectDefs: List[purescala.Symbols.ObjectSymbol] = Nil
tmpl.body.foreach(tree => tree match {
case ExObjectDef(o2, t2) => { objectSyms = extractObjectSym(o2, t2) :: objectSyms }
@@ -68,10 +68,10 @@ trait CodeExtraction extends Extractors {
case _ => ;
})
- val theSym = new purescala.Symbols.ObjectSymbol(name, classSyms.reverse, objectSyms.reverse)
+ // val theSym = new purescala.Symbols.ObjectSymbol(name, classSyms.reverse, objectSyms.reverse)
// we register the tree associated to the symbol to be able to fill in
// the rest later
- symbolDefMap(theSym) = tmpl
+ // symbolDefMap(theSym) = tmpl
theSym
}
diff --git a/src/funcheck/purescala/Definitions.scala b/src/funcheck/purescala/Definitions.scala
index dc5d6a206..fcc92c6d0 100644
--- a/src/funcheck/purescala/Definitions.scala
+++ b/src/funcheck/purescala/Definitions.scala
@@ -39,20 +39,25 @@ object Definitions {
}
/** A VarDecl declares a new identifier to be of a certain type. */
- final case class VarDecl(id: Identifier, tpe: TypeTree) {
+ 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.")
}
type VarDecls = Seq[VarDecl]
/** 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. */
- final case class Program(id: Identifier, mainObject: ObjectDef) extends Definition {
+ * 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) = {
diff --git a/src/funcheck/purescala/Symbols.scala b/src/funcheck/purescala/Symbols.scala
index 42fcc1c4f..b1c310f8f 100644
--- a/src/funcheck/purescala/Symbols.scala
+++ b/src/funcheck/purescala/Symbols.scala
@@ -3,99 +3,101 @@ 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
- }
-}
+// 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
+// }
+// }
diff --git a/src/funcheck/purescala/Trees.scala b/src/funcheck/purescala/Trees.scala
index 912765cee..f995ded93 100644
--- a/src/funcheck/purescala/Trees.scala
+++ b/src/funcheck/purescala/Trees.scala
@@ -9,66 +9,30 @@ object Trees {
/* EXPRESSIONS */
- /** There's no such thing as a typing phase for these trees, they need to be
- * correctly typed at construction time. Each AST node checks that the
- * children provided satisfy whatever typing constraints are required by the
- * node, and each node is then responsible for communicating its type. */
sealed abstract class Expr extends Typed {
override def toString: String = PrettyPrinter(this)
- private var _scope: Option[Scope] = None
+ // private var _scope: Option[Scope] = None
+ //
+ // def scope: Scope =
+ // if(_scope.isEmpty)
+ // throw new Exception("Undefined scope.")
+ // else
+ // _scope.get
- def scope: Scope =
- if(_scope.isEmpty)
- throw new Exception("Undefined scope.")
- else
- _scope.get
-
- def scope_=(s: Scope): Unit = {
- if(_scope.isEmpty) {
- _scope = Some(s)
- } else {
- throw new Exception("Redefining scope.")
- }
- }
+ // def scope_=(s: Scope): Unit = {
+ // if(_scope.isEmpty) {
+ // _scope = Some(s)
+ // } else {
+ // throw new Exception("Redefining scope.")
+ // }
+ // }
}
- /**
- equality on sets, ADTs etc. (equality on function types?!)
-
- forall, exists - optionally bounded quantifiers
- * comes with type A of bound variable
- * also comes with an optional Set[A] that gives more precise description of the range of this variable
-
- Without Set[A] bound, the variable ranges over all constructible (not only allocated) objects.
-
-see examples in:
- http://code.google.com/p/scalacheck/wiki/UserGuide
- */
-
/* Control flow */
- case class FunctionInvocation(funDef: FunDef, args: Seq[Expr]) extends Expr {
- assert(args.map(_.getType).corresponds(funDef.argTypes)(_ == _))
- lazy val getType = funDef.returnType
- }
-
- case class IfExpr(cond: Expr, then: Expr, elze: Expr) extends Expr {
- assert(cond.getType == BooleanType)
- assert(then.getType == elze.getType)
- def getType = then.getType
- }
-
- case class MatchExpr(scrutinee: Expr, cases: Seq[MatchCase]) extends Expr {
- // there can be no assumption about the type of the scrutinee.. Scala
- // gives nice errors "constructor cannot be instantiated to expected type"
- // but that seems relatively hard to check at construction for now...
- // Actually it only gives that error when the pattern is unapply (ie. not
- // an "instanceOf" one), so there's hope.
-
- // we should assert that the rhs types of all MatchCases match !
-
- lazy val getType = cases(0).rhs.getType
- }
+ case class FunctionInvocation(funDef: FunDef, args: Seq[Expr]) extends Expr
+ case class IfExpr(cond: Expr, then: Expr, elze: Expr) extends Expr
+ case class MatchExpr(scrutinee: Expr, cases: Seq[MatchCase]) extends Expr
sealed abstract class MatchCase {
val pattern: Pattern
@@ -76,9 +40,7 @@ see examples in:
}
case class SimpleCase(pattern: Pattern, rhs: Expr) extends MatchCase
- case class GuardedCase(pattern: Pattern, guard: Expr, rhs: Expr) extends MatchCase {
- assert(guard.getType == BooleanType)
- }
+ case class GuardedCase(pattern: Pattern, guard: Expr, rhs: Expr) extends MatchCase
sealed abstract class Pattern
case class InstanceOfPattern(binder: Option[Identifier], classTypeDef: ClassTypeDef) extends Pattern // c: Class
@@ -86,257 +48,82 @@ see examples in:
case class ExtractorPattern(binder: Option[Identifier],
extractor : ExtractorTypeDef,
subPatterns: Seq[Pattern]) extends Pattern // c @ Extractor(...,...)
- // I suggest we skip Seq stars for now.
+ // We don't handle Seq stars for now.
/* Propositional logic */
- case class And(exprs: Seq[Expr]) extends Expr {
- assert(exprs.forall(_.getType == BooleanType))
- def getType = BooleanType
- }
-
- case class Or(exprs: Seq[Expr]) extends Expr {
- assert(exprs.forall(_.getType == BooleanType))
- def getType = BooleanType
- }
-
- case class Not(expr: Expr) extends Expr {
- assert(expr.getType == BooleanType)
- def getType = BooleanType
- }
-
- /* Not sure if we should really have these.. I suppose they could be of some
- * help to some theorem provers? *
- case class Implies(lhs: Expr, rhs: Expr) extends Expr {
- assert(lhs.getType == BooleanType && rhs.getType == BooleanType)
- def getType = BooleanType
- }
-
- case class Iff(lhs: Expr, rhs: Expr) extends Expr {
- assert(lhs.getType == BooleanType && rhs.getType == BooleanType)
- def getType = BooleanType
- } */
+ case class And(exprs: Seq[Expr]) extends Expr
+ case class Or(exprs: Seq[Expr]) extends Expr
+ case class Not(expr: Expr) extends Expr
/* Maybe we should split this one depending on types? */
- case class Equals(left: Expr, right: Expr) extends Expr {
- assert(left.getType == right.getType)
- val getType = BooleanType
- }
+ 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 {
- val getType = AnyType
- }
+ case class Variable(id: Identifier) extends Expr
- case class IntLiteral(value: Int) extends Expr {
- val getType = Int32Type
+ sealed abstract class Literal[T] extends Expr {
+ val value: T
}
- case class BooleanLiteral(value: Boolean) extends Expr {
- val getType = BooleanType
- }
+ case class IntLiteral(value: Int) extends Literal[Int]
+ case class BooleanLiteral(value: Boolean) extends Literal[Boolean]
/* Arithmetic */
- case class Plus(lhs: Expr, rhs: Expr) extends Expr {
- assert(lhs.getType == Int32Type && rhs.getType == Int32Type)
- val getType = Int32Type
- }
-
- case class Minus(lhs: Expr, rhs: Expr) extends Expr {
- assert(lhs.getType == Int32Type && rhs.getType == Int32Type)
- val getType = Int32Type
- }
-
- case class UMinus(expr: Expr) extends Expr {
- assert(expr.getType == Int32Type)
- val getType = Int32Type
- }
-
- case class Times(lhs: Expr, rhs: Expr) extends Expr {
- assert(lhs.getType == Int32Type && rhs.getType == Int32Type)
- val getType = Int32Type
- }
-
- case class Division(lhs: Expr, rhs: Expr) extends Expr {
- assert(lhs.getType == Int32Type && rhs.getType == Int32Type)
- val getType = Int32Type
- }
-
- case class LessThan(lhs: Expr, rhs: Expr) extends Expr {
- assert(lhs.getType == Int32Type && rhs.getType == Int32Type)
- val getType = BooleanType
- }
-
- case class GreaterThan(lhs: Expr, rhs: Expr) extends Expr {
- assert(lhs.getType == Int32Type && rhs.getType == Int32Type)
- val getType = BooleanType
- }
-
- case class LessEquals(lhs: Expr, rhs: Expr) extends Expr {
- assert(lhs.getType == Int32Type && rhs.getType == Int32Type)
- val getType = BooleanType
- }
-
- case class GreaterEquals(lhs: Expr, rhs: Expr) extends Expr {
- assert(lhs.getType == Int32Type && rhs.getType == Int32Type)
- val getType = BooleanType
- }
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class UMinus(expr: Expr) extends Expr
+ case class Times(lhs: Expr, rhs: Expr) extends Expr
+ case class Division(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class GreaterThan(lhs: Expr, rhs: Expr) extends Expr
+ case class LessEquals(lhs: Expr, rhs: Expr) extends Expr
+ case class GreaterEquals(lhs: Expr, rhs: Expr) extends Expr
/* Option expressions */
- case class OptionSome(value: Expr) extends Expr {
- lazy val getType = OptionType(value.getType)
- }
-
- case class OptionNone(baseType: TypeTree) extends Expr {
- lazy val getType = OptionType(baseType)
- }
+ case class OptionSome(value: Expr) extends Expr
+ case class OptionNone(baseType: TypeTree) extends Expr
/* Set expressions */
- case class EmptySet(baseType: TypeTree) extends Expr {
- lazy val getType = SetType(baseType)
- }
- case class FiniteSet(elements: Seq[Expr]) extends Expr {
- assert(elements.size > 0)
- assert(elements.drop(1).forall(_.getType == elements(0).getType))
- lazy val getType = SetType(elements(0).getType)
- }
- case class ElementOfSet(element: Expr, set: Expr) extends Expr {
- assert(set.getType == SetType(element.getType))
- val getType = BooleanType
- }
- case class IsEmptySet(set: Expr) extends Expr {
- assert(set.getType.isInstanceOf[SetType])
- val getType = BooleanType
- }
- case class SetEquals(set1: Expr, set2: Expr) extends Expr {
- assert(set1.getType == set2.getType && set1.getType.isInstanceOf[SetType])
- val getType = BooleanType
- }
- case class SetCardinality(set: Expr) extends Expr {
- assert(set.getType.isInstanceOf[SetType])
- val getType = Int32Type
- }
- case class SubsetOf(set1: Expr, set2: Expr) extends Expr {
- assert(set1.getType == set2.getType && set1.getType.isInstanceOf[SetType])
- val getType = BooleanType
- }
- case class SetIntersection(set1: Expr, set2: Expr) extends Expr {
- assert(set1.getType == set2.getType && set1.getType.isInstanceOf[SetType])
- lazy val getType = set1.getType
- }
- case class SetUnion(set1: Expr, set2: Expr) extends Expr {
- assert(set1.getType == set2.getType && set1.getType.isInstanceOf[SetType])
- lazy val getType = set1.getType
- }
- case class SetDifference(set1: Expr, set2: Expr) extends Expr {
- assert(set1.getType == set2.getType && set1.getType.isInstanceOf[SetType])
- lazy val getType = set1.getType
- }
+ case class EmptySet(baseType: TypeTree) extends Expr
+ case class FiniteSet(elements: Seq[Expr]) extends Expr
+ case class ElementOfSet(element: Expr, set: Expr) extends Expr
+ case class IsEmptySet(set: Expr) extends Expr
+ case class SetEquals(set1: Expr, set2: Expr) extends Expr
+ case class SetCardinality(set: Expr) extends Expr
+ case class SubsetOf(set1: Expr, set2: Expr) extends Expr
+ case class SetIntersection(set1: Expr, set2: Expr) extends Expr
+ case class SetUnion(set1: Expr, set2: Expr) extends Expr
+ case class SetDifference(set1: Expr, set2: Expr) extends Expr
/* Multiset expressions */
- case class EmptyMultiset(baseType: TypeTree) extends Expr {
- lazy val getType = MultisetType(baseType)
- }
- case class FiniteMultiset(elements: Seq[Expr]) extends Expr {
- assert(elements.size > 0)
- assert(elements.drop(1).forall(_.getType == elements(0).getType))
- lazy val getType = MultisetType(elements(0).getType)
- }
- case class Multiplicity(element: Expr, multiset: Expr) extends Expr {
- assert(multiset.getType == MultisetType(element.getType))
- val getType = Int32Type
- }
- case class IsEmptyMultiset(multiset: Expr) extends Expr {
- assert(multiset.getType.isInstanceOf[MultisetType])
- val getType = BooleanType
- }
- case class MultisetEquals(multiset1: Expr, multiset2: Expr) extends Expr {
- assert(multiset1.getType == multiset2.getType && multiset1.getType.isInstanceOf[MultisetType])
- val getType = BooleanType
- }
- case class MultisetCardinality(multiset: Expr) extends Expr {
- assert(multiset.getType.isInstanceOf[MultisetType])
- val getType = Int32Type
- }
- case class SubmultisetOf(multiset1: Expr, multiset2: Expr) extends Expr {
- assert(multiset1.getType == multiset2.getType && multiset1.getType.isInstanceOf[MultisetType])
- val getType = BooleanType
- }
- case class MultisetIntersection(multiset1: Expr, multiset2: Expr) extends Expr {
- assert(multiset1.getType == multiset2.getType && multiset1.getType.isInstanceOf[MultisetType])
- lazy val getType = multiset1.getType
- }
- case class MultisetUnion(multiset1: Expr, multiset2: Expr) extends Expr {
- assert(multiset1.getType == multiset2.getType && multiset1.getType.isInstanceOf[MultisetType])
- lazy val getType = multiset1.getType
- }
- case class MultisetPlus(multiset1: Expr, multiset2: Expr) extends Expr { // disjoint union
- assert(multiset1.getType == multiset2.getType && multiset1.getType.isInstanceOf[MultisetType])
- lazy val getType = multiset1.getType
- }
- case class MultisetDifference(multiset1: Expr, multiset2: Expr) extends Expr {
- assert(multiset1.getType == multiset2.getType && multiset1.getType.isInstanceOf[MultisetType])
- lazy val getType = multiset1.getType
- }
+ // case class EmptyMultiset(baseType: TypeTree) extends Expr
+ // case class FiniteMultiset(elements: Seq[Expr]) extends Expr
+ // case class Multiplicity(element: Expr, multiset: Expr) extends Expr
+ // case class IsEmptyMultiset(multiset: Expr) extends Expr
+ // case class MultisetEquals(multiset1: Expr, multiset2: Expr) extends Expr
+ // case class MultisetCardinality(multiset: Expr) extends Expr
+ // case class SubmultisetOf(multiset1: Expr, multiset2: Expr) extends Expr
+ // case class MultisetIntersection(multiset1: Expr, multiset2: Expr) extends Expr
+ // case class MultisetUnion(multiset1: Expr, multiset2: Expr) extends Expr
+ // case class MultisetPlus(multiset1: Expr, multiset2: Expr) extends Expr // disjoint union
+ // case class MultisetDifference(multiset1: Expr, multiset2: Expr) extends Expr
/* Map operations. */
- case class EmptyMap(fromType: TypeTree, toType: TypeTree) extends Expr {
- lazy val getType = MapType(fromType, toType)
- }
-
- case class SingletonMap(from: Expr, to: Expr) extends Expr {
- lazy val getType = MapType(from.getType, to.getType)
- }
+ case class EmptyMap(fromType: TypeTree, toType: TypeTree) extends Expr
+ case class SingletonMap(from: Expr, to: Expr) extends Expr
+ case class FiniteMap(singletons: Seq[SingletonMap]) extends Expr
- case class FiniteMap(singletons: Seq[SingletonMap]) extends Expr {
- assert(singletons.size > 0
- && singletons.drop(1).forall(_.getType == singletons(0).getType))
- lazy val getType = singletons(0).getType
- }
-
- case class MapGet(map: Expr, key: Expr) extends Expr {
- assert(map.getType.isInstanceOf[MapType] && key.getType == map.getType.asInstanceOf[MapType].from)
- lazy val getType = OptionType(map.getType.asInstanceOf[MapType].to)
- }
-
- case class MapUnion(map1: Expr, map2: Expr) extends Expr {
- assert(map1.getType.isInstanceOf[MapType] && map1.getType == map2.getType)
- lazy val getType = map1.getType
- }
-
- case class MapDiffrence(map: Expr, keys: Expr) extends Expr {
- assert(map.getType.isInstanceOf[MapType] && keys.isInstanceOf[SetType] && map.getType.asInstanceOf[MapType].from == keys.getType.asInstanceOf[SetType].base)
- lazy val getType = map.getType
- }
+ case class MapGet(map: Expr, key: Expr) extends Expr
+ case class MapUnion(map1: Expr, map2: Expr) extends Expr
+ case class MapDiffrence(map: Expr, keys: Expr) extends Expr
/* List operations */
- case class NilList(baseType: TypeTree) extends Expr {
- lazy val getType = ListType(baseType)
- }
-
- case class Cons(head: Expr, tail: Expr) extends Expr {
- assert(tail.isInstanceOf[ListType] && tail.getType.asInstanceOf[ListType].base == head.getType)
- lazy val getType = tail.getType
- }
-
- case class Car(list: Expr) extends Expr {
- assert(list.getType.isInstanceOf[ListType])
- lazy val getType = list.getType.asInstanceOf[ListType].base
- }
-
- case class Cdr(list: Expr) extends Expr {
- assert(list.getType.isInstanceOf[ListType])
- lazy val getType = list.getType
- }
-
- case class Concat(list1: Expr, list2: Expr) extends Expr {
- assert(list1.getType.isInstanceOf[ListType] && list1.getType == list2.getType)
- lazy val getType = list1.getType
- }
-
- case class ListAt(list: Expr, index: Expr) extends Expr {
- assert(list.getType.isInstanceOf[ListType] && index.getType == Int32Type)
- lazy val getType = OptionType(list.getType.asInstanceOf[ListType].base)
- }
+ case class NilList(baseType: TypeTree) extends Expr
+ case class Cons(head: Expr, tail: Expr) extends Expr
+ case class Car(list: Expr) extends Expr
+ case class Cdr(list: Expr) extends Expr
+ case class Concat(list1: Expr, list2: Expr) extends Expr
+ case class ListAt(list: Expr, index: Expr) extends Expr
}
diff --git a/src/funcheck/purescala/TypeTrees.scala b/src/funcheck/purescala/TypeTrees.scala
index 54ec17162..1ff91b436 100644
--- a/src/funcheck/purescala/TypeTrees.scala
+++ b/src/funcheck/purescala/TypeTrees.scala
@@ -6,13 +6,27 @@ object TypeTrees {
import Definitions._
trait Typed {
- def getType: TypeTree
+ self =>
+
+ var _type: Option[TypeTree] = None
+
+ def getType: TypeTree = _type match {
+ case None => NoType
+ case Some(t) => t
+ }
+
+ def setType(tt: TypeTree): self.type = _type match {
+ case None => _type = Some(tt); this
+ case Some(_) => scala.Predef.error("Resetting type information.")
+ }
}
sealed abstract class TypeTree {
override def toString: String = PrettyPrinter(this)
}
+ case object NoType extends TypeTree
+
case object AnyType extends TypeTree
case object BooleanType extends TypeTree
case object Int32Type extends TypeTree
@@ -21,7 +35,7 @@ object TypeTrees {
case class TupleType(bases: Seq[TypeTree]) extends TypeTree { lazy val dimension: Int = bases.length }
case class FunctionType(arg: TypeTree, res: TypeTree) extends TypeTree
case class SetType(base: TypeTree) extends TypeTree
- case class MultisetType(base: TypeTree) extends TypeTree
+ // case class MultisetType(base: TypeTree) extends TypeTree
case class MapType(from: TypeTree, to: TypeTree) extends TypeTree
case class ClassType(id: Identifier) extends TypeTree
case class CaseClassType(id: Identifier) extends TypeTree
--
GitLab