Skip to content
Snippets Groups Projects
Commit 56a937c3 authored by Emmanouil (Manos) Koukoutos's avatar Emmanouil (Manos) Koukoutos Committed by Etienne Kneuss
Browse files

Some consistency changes in Trees

parent 0cad3d1c
No related branches found
No related tags found
No related merge requests found
......@@ -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) {
......
......@@ -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 =>
......
......@@ -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
}
......
......@@ -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._
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment