diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 64851adca1d389b976dd853658014559b0e9947f..5bf34b1f70f3bd0b3ec4e52b3eb9713a17fc7685 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -163,7 +163,7 @@ class CompilationUnit(val ctx: LeonContext,
}
m
- case f @ FiniteLambda(dflt, els) =>
+ case f @ purescala.Extractors.FiniteLambda(dflt, els) =>
val l = new leon.codegen.runtime.FiniteLambda(exprToJVM(dflt))
for ((k,v) <- els) {
val jvmK = if (f.getType.from.size == 1) {
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index d329c6d3bf44dd4c689242ceeee4ba8d45423cfb..9e516807e9e337f6be0d2c7f3be1b7b123494e71 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -249,6 +249,51 @@ object Extractors {
def unapply[T <: Typed](e: T): Option[(T, TypeTree)] = Some((e, e.getType))
}
+ object FiniteLambda {
+ def unapply(lambda: Lambda): Option[(Expr, Seq[(Expr, Expr)])] = {
+ val args = lambda.args.map(_.toVariable)
+ lazy val argsTuple = if (lambda.args.size > 1) Tuple(args) else args.head
+
+ def rec(body: Expr): Option[(Expr, Seq[(Expr, Expr)])] = body match {
+ case _ : IntLiteral | _ : UMinus | _ : BooleanLiteral | _ : GenericValue | _ : Tuple |
+ _ : CaseClass | _ : FiniteArray | _ : FiniteSet | _ : FiniteMap | _ : Lambda =>
+ Some(body -> Seq.empty)
+ case IfExpr(Equals(tpArgs, key), expr, elze) if tpArgs == argsTuple =>
+ rec(elze).map { case (dflt, mapping) => dflt -> ((key -> expr) +: mapping) }
+ case _ => None
+ }
+
+ rec(lambda.body)
+ }
+
+ def apply(dflt: Expr, els: Seq[(Expr, Expr)], tpe: FunctionType): Lambda = {
+ val args = tpe.from.zipWithIndex.map { case (tpe, idx) =>
+ ValDef(FreshIdentifier(s"x${idx + 1}").setType(tpe), tpe)
+ }
+
+ assume(els.isEmpty || !tpe.from.isEmpty, "Can't provide finite mapping for lambda without parameters")
+
+ lazy val (tupleArgs, tupleKey) = if (tpe.from.size > 1) {
+ val tpArgs = Tuple(args.map(_.toVariable))
+ val key = (x: Expr) => x
+ (tpArgs, key)
+ } else { // note that value is lazy, so if tpe.from.size == 0, foldRight will never access (tupleArgs, tupleKey)
+ val tpArgs = args.head.toVariable
+ val key = (x: Expr) => {
+ if (isSubtypeOf(x.getType, tpe.from.head)) x
+ else if (isSubtypeOf(x.getType, TupleType(tpe.from))) x.asInstanceOf[Tuple].exprs.head
+ else throw new RuntimeException("Can't determine key tuple state : " + x + " of " + tpe)
+ }
+ (tpArgs, key)
+ }
+
+ val body = els.toSeq.foldRight(dflt) { case ((k, v), elze) =>
+ IfExpr(Equals(tupleArgs, tupleKey(k)), v, elze)
+ }
+
+ Lambda(args, body)
+ }
+ }
object MatchLike {
def unapply(m : MatchLike) : Option[(Expr, Seq[MatchCase], (Expr, Seq[MatchCase]) => Expr)] = {
Option(m) map { m =>
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index e8999b26b12704c7d222488bffce7e1c4b45947d..5879c42da0a7d30fde9fcb669c0766d4edc6db28 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -91,7 +91,7 @@ object Trees {
}
case class Application(caller: Expr, args: Seq[Expr]) extends Expr {
- assert(caller.getType.isInstanceOf[FunctionType])
+ require(caller.getType.isInstanceOf[FunctionType])
def getType = caller.getType.asInstanceOf[FunctionType].to
}
@@ -99,54 +99,8 @@ object Trees {
def getType = FunctionType(args.map(_.tpe), body.getType)
}
- object FiniteLambda {
- def unapply(lambda: Lambda): Option[(Expr, Seq[(Expr, Expr)])] = {
- val args = lambda.args.map(_.toVariable)
- lazy val argsTuple = if (lambda.args.size > 1) Tuple(args) else args.head
-
- def rec(body: Expr): Option[(Expr, Seq[(Expr, Expr)])] = body match {
- case _ : IntLiteral | _ : UMinus | _ : BooleanLiteral | _ : GenericValue | _ : Tuple |
- _ : CaseClass | _ : FiniteArray | _ : FiniteSet | _ : FiniteMap | _ : Lambda =>
- Some(body -> Seq.empty)
- case IfExpr(Equals(tpArgs, key), expr, elze) if tpArgs == argsTuple =>
- rec(elze).map { case (dflt, mapping) => dflt -> ((key -> expr) +: mapping) }
- case _ => None
- }
-
- rec(lambda.body)
- }
-
- def apply(dflt: Expr, els: Seq[(Expr, Expr)], tpe: FunctionType): Lambda = {
- val args = tpe.from.zipWithIndex.map { case (tpe, idx) =>
- ValDef(FreshIdentifier(s"x${idx + 1}").setType(tpe), tpe)
- }
-
- assert(els.isEmpty || !tpe.from.isEmpty, "Can't provide finite mapping for lambda without parameters")
-
- lazy val (tupleArgs, tupleKey) = if (tpe.from.size > 1) {
- val tpArgs = Tuple(args.map(_.toVariable))
- val key = (x: Expr) => x
- (tpArgs, key)
- } else { // note that value is lazy, so if tpe.from.size == 0, foldRight will never access (tupleArgs, tupleKey)
- val tpArgs = args.head.toVariable
- val key = (x: Expr) => {
- if (isSubtypeOf(x.getType, tpe.from.head)) x
- else if (isSubtypeOf(x.getType, TupleType(tpe.from))) x.asInstanceOf[Tuple].exprs.head
- else throw new RuntimeException("Can't determine key tuple state : " + x + " of " + tpe)
- }
- (tpArgs, key)
- }
-
- val body = els.toSeq.foldRight(dflt) { case ((k, v), elze) =>
- IfExpr(Equals(tupleArgs, tupleKey(k)), v, elze)
- }
-
- Lambda(args, body)
- }
- }
-
case class Forall(args: Seq[ValDef], body: Expr) extends Expr {
- assert(body.getType == BooleanType)
+ require(body.getType == BooleanType)
def getType = BooleanType
}
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 0b599a0222c06481c1bccda3d0309af29010c255..6e99fbfa6bfd8fc233ff32cebb2ce039f81bb294 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -10,7 +10,7 @@ import solvers._
import purescala.Common._
import purescala.Definitions._
import purescala.Constructors._
-import purescala.Extractors.LetTuple
+import purescala.Extractors._
import purescala.Trees._
import purescala.TypeTreeOps._
import xlang.Trees._