diff --git a/src/purescala/Common.scala b/src/purescala/Common.scala
index a528df50db387cdc6799c14040c61753259efec3..fb01de0f1f1e53b7603f49ad3344b806f7dbb93c 100644
--- a/src/purescala/Common.scala
+++ b/src/purescala/Common.scala
@@ -48,7 +48,7 @@ object Common {
def apply(name: String, alwaysShowUniqueID: Boolean = false) : Identifier = new Identifier(name, UniqueCounter.next, alwaysShowUniqueID)
}
- trait ScalacPositional {
+ @serializable trait ScalacPositional {
self =>
private var prow: Int = -1078
diff --git a/src/purescala/Definitions.scala b/src/purescala/Definitions.scala
index 9faaa6b03db2f8be9951e51251c53fd03b767b55..2384edf71847be45e377a62bf212c17a96129dee 100644
--- a/src/purescala/Definitions.scala
+++ b/src/purescala/Definitions.scala
@@ -5,24 +5,35 @@ object Definitions {
import Trees._
import TypeTrees._
- sealed abstract class Definition {
+ @serializable sealed abstract class Definition {
val id: Identifier
override def toString: String = PrettyPrinter(this)
+ override def hashCode : Int = id.hashCode
+ override def equals(that : Any) : Boolean = that match {
+ case t : Definition => t.id == this.id
+ case _ => false
+ }
}
/** A VarDecl declares a new identifier to be of a certain type. */
- case class VarDecl(id: Identifier, tpe: TypeTree) extends Typed {
+ @serializable case class VarDecl(id: Identifier, tpe: TypeTree) extends Typed {
override def getType = tpe
override def setType(tt: TypeTree) = scala.Predef.error("Can't set type of VarDecl.")
+ override def hashCode : Int = id.hashCode
+ override def equals(that : Any) : Boolean = that match {
+ case t : VarDecl => t.id == this.id
+ case _ => false
+ }
+
def toVariable : Variable = Variable(id).setType(tpe)
}
- type VarDecls = Seq[VarDecl]
+ @serializable 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 as id. */
- case class Program(id: Identifier, mainObject: ObjectDef) extends Definition {
+ @serializable case class Program(id: Identifier, mainObject: ObjectDef) extends Definition {
def definedFunctions = mainObject.definedFunctions
def definedClasses = mainObject.definedClasses
def classHierarchyRoots = mainObject.classHierarchyRoots
@@ -40,7 +51,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 {
+ @serializable case class ObjectDef(id: Identifier, defs : Seq[Definition], invariants: Seq[Expr]) extends Definition {
lazy val definedFunctions : Seq[FunDef] = defs.filter(_.isInstanceOf[FunDef]).map(_.asInstanceOf[FunDef])
lazy val definedClasses : Seq[ClassTypeDef] = defs.filter(_.isInstanceOf[ClassTypeDef]).map(_.asInstanceOf[ClassTypeDef])
@@ -127,7 +138,7 @@ object Definitions {
/** Useful because case classes and classes are somewhat unified in some
* patterns (of pattern-matching, that is) */
- sealed trait ClassTypeDef extends Definition {
+ @serializable sealed trait ClassTypeDef extends Definition {
self =>
val id: Identifier
@@ -135,11 +146,12 @@ object Definitions {
def setParent(parent: AbstractClassDef) : self.type
def hasParent: Boolean = parent.isDefined
val isAbstract: Boolean
+
}
/** Will be used at some point as a common ground for case classes (which
* implicitely define extractors) and explicitely defined unapply methods. */
- sealed trait ExtractorTypeDef
+ @serializable sealed trait ExtractorTypeDef
/** Abstract classes. */
object AbstractClassDef {
@@ -228,7 +240,7 @@ object Definitions {
//}
/** Values */
- case class ValDef(varDecl: VarDecl, value: Expr) extends Definition {
+ @serializable case class ValDef(varDecl: VarDecl, value: Expr) extends Definition {
val id: Identifier = varDecl.id
}
@@ -251,7 +263,7 @@ object Definitions {
def hasBody = hasImplementation
def hasPrecondition : Boolean = precondition.isDefined
def hasPostcondition : Boolean = postcondition.isDefined
-
+
private var annots: Set[String] = Set.empty[String]
def addAnnotation(as: String*) : FunDef = {
annots = annots ++ as
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 7e62e89965e7ea9702afedd0b1652da97a091cf2..c26e46adf5e16da3e1b812c6bf6dbc370932c02e 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -11,6 +11,7 @@ import scala.collection.mutable.{Map => MutableMap}
import scala.collection.mutable.{Set => MutableSet}
class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with AbstractZ3Solver with Z3ModelReconstruction {
+ // have to comment this to use the solver for constraint solving...
// assert(Settings.useFairInstantiator)
private final val UNKNOWNASSAT : Boolean = false
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index ee4f69d10b986d6ba9f5fbd9ba6b31deae18fe4a..3e037816931f9a2443386d5035a53827142ae284 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -8,21 +8,21 @@ object Trees {
/* EXPRESSIONS */
- sealed abstract class Expr extends Typed {
+ @serializable sealed abstract class Expr extends Typed {
override def toString: String = PrettyPrinter(this)
}
- sealed trait Terminal {
+ @serializable sealed trait Terminal {
self: Expr =>
}
/* This describes computational errors (unmatched case, taking min of an
* empty set, division by zero, etc.). It should always be typed according to
* the expected type. */
- case class Error(description: String) extends Expr with Terminal with ScalacPositional
+ @serializable case class Error(description: String) extends Expr with Terminal with ScalacPositional
/* Like vals */
- case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr {
+ @serializable case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr {
binder.markAsLetBinder
val et = body.getType
if(et != Untyped)
@@ -30,10 +30,10 @@ object Trees {
}
/* Control flow */
- case class FunctionInvocation(funDef: FunDef, args: Seq[Expr]) extends Expr with FixedType with ScalacPositional {
+ @serializable case class FunctionInvocation(funDef: FunDef, args: Seq[Expr]) extends Expr with FixedType with ScalacPositional {
val fixedType = funDef.returnType
}
- case class IfExpr(cond: Expr, then: Expr, elze: Expr) extends Expr
+ @serializable case class IfExpr(cond: Expr, then: Expr, elze: Expr) extends Expr
object MatchExpr {
def apply(scrutinee: Expr, cases: Seq[MatchCase]) : MatchExpr = {
@@ -54,7 +54,7 @@ object Trees {
def scrutineeClassType: ClassType = scrutinee.getType.asInstanceOf[ClassType]
}
- sealed abstract class MatchCase {
+ @serializable sealed abstract class MatchCase {
val pattern: Pattern
val rhs: Expr
val theGuard: Option[Expr]
@@ -62,29 +62,29 @@ object Trees {
def expressions: Seq[Expr]
}
- case class SimpleCase(pattern: Pattern, rhs: Expr) extends MatchCase {
+ @serializable case class SimpleCase(pattern: Pattern, rhs: Expr) extends MatchCase {
val theGuard = None
def expressions = List(rhs)
}
- case class GuardedCase(pattern: Pattern, guard: Expr, rhs: Expr) extends MatchCase {
+ @serializable case class GuardedCase(pattern: Pattern, guard: Expr, rhs: Expr) extends MatchCase {
val theGuard = Some(guard)
def expressions = List(guard, rhs)
}
- sealed abstract class Pattern {
+ @serializable sealed abstract class Pattern {
val subPatterns: Seq[Pattern]
val binder: Option[Identifier]
private def subBinders = subPatterns.map(_.binders).foldLeft[Set[Identifier]](Set.empty)(_ ++ _)
def binders: Set[Identifier] = subBinders ++ (if(binder.isDefined) Set(binder.get) else Set.empty)
}
- case class InstanceOfPattern(binder: Option[Identifier], classTypeDef: ClassTypeDef) extends Pattern { // c: Class
+ @serializable case class InstanceOfPattern(binder: Option[Identifier], classTypeDef: ClassTypeDef) extends Pattern { // c: Class
val subPatterns = Seq.empty
}
- case class WildcardPattern(binder: Option[Identifier]) extends Pattern { // c @ _
+ @serializable case class WildcardPattern(binder: Option[Identifier]) extends Pattern { // c @ _
val subPatterns = Seq.empty
}
- case class CaseClassPattern(binder: Option[Identifier], caseClassDef: CaseClassDef, subPatterns: Seq[Pattern]) extends Pattern
+ @serializable 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(...,...)
@@ -164,7 +164,7 @@ object Trees {
val fixedType = BooleanType
}
- case class Not(expr: Expr) extends Expr with FixedType {
+ @serializable case class Not(expr: Expr) extends Expr with FixedType {
val fixedType = BooleanType
}
@@ -196,63 +196,63 @@ object Trees {
val fixedType = BooleanType
}
- case class Variable(id: Identifier) extends Expr with Terminal {
+ @serializable case class Variable(id: Identifier) extends Expr with Terminal {
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 with Terminal
+ @serializable case class ResultVariable() extends Expr with Terminal
/* Literals */
- sealed abstract class Literal[T] extends Expr with Terminal {
+ @serializable sealed abstract class Literal[T] extends Expr with Terminal {
val value: T
}
- case class IntLiteral(value: Int) extends Literal[Int] with FixedType {
+ @serializable case class IntLiteral(value: Int) extends Literal[Int] with FixedType {
val fixedType = Int32Type
}
- case class BooleanLiteral(value: Boolean) extends Literal[Boolean] with FixedType {
+ @serializable case class BooleanLiteral(value: Boolean) extends Literal[Boolean] with FixedType {
val fixedType = BooleanType
}
- case class StringLiteral(value: String) extends Literal[String]
+ @serializable case class StringLiteral(value: String) extends Literal[String]
- case class CaseClass(classDef: CaseClassDef, args: Seq[Expr]) extends Expr with FixedType {
+ @serializable case class CaseClass(classDef: CaseClassDef, args: Seq[Expr]) extends Expr with FixedType {
val fixedType = CaseClassType(classDef)
}
- case class CaseClassInstanceOf(classDef: CaseClassDef, expr: Expr) extends Expr with FixedType {
+ @serializable case class CaseClassInstanceOf(classDef: CaseClassDef, expr: Expr) extends Expr with FixedType {
val fixedType = BooleanType
}
- case class CaseClassSelector(classDef: CaseClassDef, caseClass: Expr, selector: Identifier) extends Expr with FixedType {
+ @serializable case class CaseClassSelector(classDef: CaseClassDef, caseClass: Expr, selector: Identifier) extends Expr with FixedType {
val fixedType = classDef.fields.find(_.id == selector).get.getType
}
/* Arithmetic */
- case class Plus(lhs: Expr, rhs: Expr) extends Expr with FixedType {
+ @serializable case class Plus(lhs: Expr, rhs: Expr) extends Expr with FixedType {
val fixedType = Int32Type
}
- case class Minus(lhs: Expr, rhs: Expr) extends Expr with FixedType {
+ @serializable case class Minus(lhs: Expr, rhs: Expr) extends Expr with FixedType {
val fixedType = Int32Type
}
- case class UMinus(expr: Expr) extends Expr with FixedType {
+ @serializable case class UMinus(expr: Expr) extends Expr with FixedType {
val fixedType = Int32Type
}
- case class Times(lhs: Expr, rhs: Expr) extends Expr with FixedType {
+ @serializable case class Times(lhs: Expr, rhs: Expr) extends Expr with FixedType {
val fixedType = Int32Type
}
- case class Division(lhs: Expr, rhs: Expr) extends Expr with FixedType {
+ @serializable case class Division(lhs: Expr, rhs: Expr) extends Expr with FixedType {
val fixedType = Int32Type
}
- case class LessThan(lhs: Expr, rhs: Expr) extends Expr with FixedType {
+ @serializable case class LessThan(lhs: Expr, rhs: Expr) extends Expr with FixedType {
val fixedType = BooleanType
}
- case class GreaterThan(lhs: Expr, rhs: Expr) extends Expr with FixedType {
+ @serializable case class GreaterThan(lhs: Expr, rhs: Expr) extends Expr with FixedType {
val fixedType = BooleanType
}
- case class LessEquals(lhs: Expr, rhs: Expr) extends Expr with FixedType {
+ @serializable case class LessEquals(lhs: Expr, rhs: Expr) extends Expr with FixedType {
val fixedType = BooleanType
}
- case class GreaterEquals(lhs: Expr, rhs: Expr) extends Expr with FixedType {
+ @serializable case class GreaterEquals(lhs: Expr, rhs: Expr) extends Expr with FixedType {
val fixedType = BooleanType
}
@@ -261,53 +261,53 @@ object Trees {
// case class OptionNone(baseType: TypeTree) extends Expr with Terminal
/* Set expressions */
- case class EmptySet(baseType: TypeTree) extends Expr with Terminal
- case class FiniteSet(elements: Seq[Expr]) extends Expr
- case class ElementOfSet(element: Expr, set: Expr) extends Expr with FixedType {
+ @serializable case class EmptySet(baseType: TypeTree) extends Expr with Terminal
+ @serializable case class FiniteSet(elements: Seq[Expr]) extends Expr
+ @serializable case class ElementOfSet(element: Expr, set: Expr) extends Expr with FixedType {
val fixedType = BooleanType
}
- case class SetCardinality(set: Expr) extends Expr with FixedType {
+ @serializable case class SetCardinality(set: Expr) extends Expr with FixedType {
val fixedType = Int32Type
}
- case class SubsetOf(set1: Expr, set2: Expr) extends Expr with FixedType {
+ @serializable case class SubsetOf(set1: Expr, set2: Expr) extends Expr with FixedType {
val fixedType = BooleanType
}
- 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
- case class SetMin(set: Expr) extends Expr
- case class SetMax(set: Expr) extends Expr
+ @serializable case class SetIntersection(set1: Expr, set2: Expr) extends Expr
+ @serializable case class SetUnion(set1: Expr, set2: Expr) extends Expr
+ @serializable case class SetDifference(set1: Expr, set2: Expr) extends Expr
+ @serializable case class SetMin(set: Expr) extends Expr
+ @serializable case class SetMax(set: Expr) extends Expr
/* Multiset expressions */
- case class EmptyMultiset(baseType: TypeTree) extends Expr with Terminal
- case class FiniteMultiset(elements: Seq[Expr]) extends Expr
- case class Multiplicity(element: Expr, multiset: Expr) extends Expr
- case class MultisetCardinality(multiset: Expr) extends Expr with FixedType {
+ @serializable case class EmptyMultiset(baseType: TypeTree) extends Expr with Terminal
+ @serializable case class FiniteMultiset(elements: Seq[Expr]) extends Expr
+ @serializable case class Multiplicity(element: Expr, multiset: Expr) extends Expr
+ @serializable case class MultisetCardinality(multiset: Expr) extends Expr with FixedType {
val fixedType = Int32Type
}
- 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
- case class MultisetToSet(multiset: Expr) extends Expr
+ @serializable case class SubmultisetOf(multiset1: Expr, multiset2: Expr) extends Expr
+ @serializable case class MultisetIntersection(multiset1: Expr, multiset2: Expr) extends Expr
+ @serializable case class MultisetUnion(multiset1: Expr, multiset2: Expr) extends Expr
+ @serializable case class MultisetPlus(multiset1: Expr, multiset2: Expr) extends Expr // disjoint union
+ @serializable case class MultisetDifference(multiset1: Expr, multiset2: Expr) extends Expr
+ @serializable case class MultisetToSet(multiset: Expr) extends Expr
/* Map operations. */
- case class EmptyMap(fromType: TypeTree, toType: TypeTree) extends Expr with Terminal
- case class SingletonMap(from: Expr, to: Expr) extends Expr
- case class FiniteMap(singletons: Seq[SingletonMap]) extends Expr
+ @serializable case class EmptyMap(fromType: TypeTree, toType: TypeTree) extends Expr with Terminal
+ @serializable case class SingletonMap(from: Expr, to: Expr) extends Expr
+ @serializable case class FiniteMap(singletons: Seq[SingletonMap]) extends Expr
- case class MapGet(map: Expr, key: Expr) extends Expr
- case class MapUnion(map1: Expr, map2: Expr) extends Expr
- case class MapDifference(map: Expr, keys: Expr) extends Expr
+ @serializable case class MapGet(map: Expr, key: Expr) extends Expr
+ @serializable case class MapUnion(map1: Expr, map2: Expr) extends Expr
+ @serializable case class MapDifference(map: Expr, keys: Expr) extends Expr
/* List operations */
- case class NilList(baseType: TypeTree) extends Expr with Terminal
- 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
+ @serializable case class NilList(baseType: TypeTree) extends Expr with Terminal
+ @serializable case class Cons(head: Expr, tail: Expr) extends Expr
+ @serializable case class Car(list: Expr) extends Expr
+ @serializable case class Cdr(list: Expr) extends Expr
+ @serializable case class Concat(list1: Expr, list2: Expr) extends Expr
+ @serializable case class ListAt(list: Expr, index: Expr) extends Expr
object UnaryOperator {
def unapply(expr: Expr) : Option[(Expr,(Expr)=>Expr)] = expr match {
@@ -732,8 +732,8 @@ object Trees {
// Pulls out all let constructs to the top level, and makes sure they're
// properly ordered.
- private type DefPair = (Identifier,Expr)
- private type DefPairs = List[DefPair]
+ @serializable private type DefPair = (Identifier,Expr)
+ @serializable private type DefPairs = List[DefPair]
private def allLetDefinitions(expr: Expr) : DefPairs = treeCatamorphism[DefPairs](
(e: Expr) => Nil,
(s1: DefPairs, s2: DefPairs) => s1 ::: s2,
diff --git a/src/purescala/TypeTrees.scala b/src/purescala/TypeTrees.scala
index da29f67f0ca7ddd79f17f3c6d6945cc3ff600cc3..6f65972d3343aac47fd55098cf928695d30b7b48 100644
--- a/src/purescala/TypeTrees.scala
+++ b/src/purescala/TypeTrees.scala
@@ -5,7 +5,7 @@ object TypeTrees {
import Trees._
import Definitions._
- trait Typed {
+ @serializable trait Typed {
self =>
private var _type: Option[TypeTree] = None
@@ -22,7 +22,7 @@ object TypeTrees {
}
}
- trait FixedType extends Typed {
+ @serializable trait FixedType extends Typed {
self =>
val fixedType: TypeTree
@@ -87,9 +87,9 @@ object TypeTrees {
}
// returns the number of distinct values that inhabit a type
- sealed abstract class TypeSize
- case class FiniteSize(size: Int) extends TypeSize
- case object InfiniteSize extends TypeSize
+ @serializable sealed abstract class TypeSize
+ @serializable case class FiniteSize(size: Int) extends TypeSize
+ @serializable case object InfiniteSize extends TypeSize
def domainSize(typeTree: TypeTree) : TypeSize = typeTree match {
case Untyped => FiniteSize(0)
@@ -122,25 +122,31 @@ object TypeTrees {
case c: ClassType => InfiniteSize
}
- case object Untyped extends TypeTree
- case object AnyType extends TypeTree
- case object NoType extends TypeTree // This is the type of errors (ie. subtype of anything)
- case object BooleanType extends TypeTree
- case object Int32Type extends TypeTree
+ @serializable case object Untyped extends TypeTree
+ @serializable case object AnyType extends TypeTree
+ @serializable case object NoType extends TypeTree // This is the type of errors (ie. subtype of anything)
+ @serializable case object BooleanType extends TypeTree
+ @serializable case object Int32Type extends TypeTree
- case class ListType(base: TypeTree) extends TypeTree
- case class TupleType(bases: Seq[TypeTree]) extends TypeTree { lazy val dimension: Int = bases.length }
- 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
+ @serializable case class ListType(base: TypeTree) extends TypeTree
+ @serializable case class TupleType(bases: Seq[TypeTree]) extends TypeTree { lazy val dimension: Int = bases.length }
+ @serializable case class SetType(base: TypeTree) extends TypeTree
+ @serializable case class MultisetType(base: TypeTree) extends TypeTree
+ @serializable case class MapType(from: TypeTree, to: TypeTree) extends TypeTree
+ @serializable case class OptionType(base: TypeTree) extends TypeTree
@serializable sealed abstract class ClassType extends TypeTree {
val classDef: ClassTypeDef
val id: Identifier = classDef.id
+
+ override def hashCode : Int = id.hashCode
+ override def equals(that : Any) : Boolean = that match {
+ case t : ClassType => t.id == this.id
+ case _ => false
+ }
}
- case class AbstractClassType(classDef: AbstractClassDef) extends ClassType
- case class CaseClassType(classDef: CaseClassDef) extends ClassType
+ @serializable case class AbstractClassType(classDef: AbstractClassDef) extends ClassType
+ @serializable case class CaseClassType(classDef: CaseClassDef) extends ClassType
def classDefToClassType(cd: ClassTypeDef): ClassType = cd match {
case a: AbstractClassDef => AbstractClassType(a)