diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala index 7db7f3e00a01335f858536ba63558da2807525eb..689b87fe995aee858c6ff7a229bf48bdcc9f4ec4 100644 --- a/src/main/scala/leon/purescala/Extractors.scala +++ b/src/main/scala/leon/purescala/Extractors.scala @@ -2,7 +2,6 @@ package leon package purescala import Trees._ -import xlang.Trees._ object Extractors { import Common._ @@ -24,14 +23,11 @@ object Extractors { case SetMax(s) => Some((s,SetMax)) case CaseClassSelector(cd, e, sel) => Some((e, CaseClassSelector(cd, _, sel))) case CaseClassInstanceOf(cd, e) => Some((e, CaseClassInstanceOf(cd, _))) - case Assignment(id, e) => Some((e, Assignment(id, _))) case TupleSelect(t, i) => Some((t, TupleSelect(_, i))) case ArrayLength(a) => Some((a, ArrayLength)) case ArrayClone(a) => Some((a, ArrayClone)) case ArrayMake(t) => Some((t, ArrayMake)) - case Waypoint(i, t) => Some((t, (expr: Expr) => Waypoint(i, expr))) - case e@Epsilon(t) => Some((t, (expr: Expr) => Epsilon(expr).setType(e.getType).setPosInfo(e))) - case ue: UnaryExtractable => ue.extract + case (ue: UnaryExtractable) => ue.extract case _ => None } } @@ -74,11 +70,9 @@ object Extractors { case ArraySelect(t1, t2) => Some((t1, t2, ArraySelect)) case Concat(t1,t2) => Some((t1,t2,Concat)) case ListAt(t1,t2) => Some((t1,t2,ListAt)) - case Let(binders, e, body) => Some((e, body, (e: Expr, b: Expr) => Let(binders, e, body))) - case LetVar(binders, e, body) => Some((e, body, (e: Expr, b: Expr) => LetVar(binders, e, body))) - case LetTuple(binders, e, body) => Some((e, body, (e: Expr, b: Expr) => LetTuple(binders, e, body))) - case wh@While(t1, t2) => Some((t1,t2, (t1, t2) => While(t1, t2).setInvariant(wh.invariant).setPosInfo(wh))) - case ex: BinaryExtractable => ex.extract + case Let(binders, e, body) => Some((e, body, (e: Expr, b: Expr) => Let(binders, e, body))) //TODO: shouldn't be "b" instead of "body" ? + case LetTuple(binders, e, body) => Some((e, body, (e: Expr, b: Expr) => LetTuple(binders, e, body))) //TODO: shouldn't be "b" instead of "body" ? + case (ex: BinaryExtractable) => ex.extract case _ => None } } @@ -97,11 +91,9 @@ object Extractors { case FiniteSet(args) => Some((args, FiniteSet)) case FiniteMap(args) => Some((args, (as : Seq[Expr]) => FiniteMap(as.asInstanceOf[Seq[SingletonMap]]))) case FiniteMultiset(args) => Some((args, FiniteMultiset)) - case ArrayUpdate(t1, t2, t3) => Some((Seq(t1,t2,t3), (as: Seq[Expr]) => ArrayUpdate(as(0), as(1), as(2)))) case ArrayUpdated(t1, t2, t3) => Some((Seq(t1,t2,t3), (as: Seq[Expr]) => ArrayUpdated(as(0), as(1), as(2)))) case FiniteArray(args) => Some((args, FiniteArray)) case Distinct(args) => Some((args, Distinct)) - case Block(args, rest) => Some((args :+ rest, exprs => Block(exprs.init, exprs.last))) case Tuple(args) => Some((args, Tuple)) case IfExpr(cond, then, elze) => Some((Seq(cond, then, elze), (as: Seq[Expr]) => IfExpr(as(0), as(1), as(2)))) case MatchExpr(scrut, cases) => @@ -153,7 +145,7 @@ object Extractors { case _ => None } - case ex: NAryExtractable => ex.extract + case (ex: NAryExtractable) => ex.extract case _ => None } } diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala index cf472b18374c78931fd46d6a150380652c8bf208..b1b7fffe1bdd28f7f817f6ff4332e47d3646c740 100644 --- a/src/main/scala/leon/xlang/Trees.scala +++ b/src/main/scala/leon/xlang/Trees.scala @@ -9,40 +9,71 @@ import leon.purescala.Extractors._ object Trees { - case class Block(exprs: Seq[Expr], last: Expr) extends Expr { + case class Block(exprs: Seq[Expr], last: Expr) extends Expr with NAryExtractable { //val t = last.getType //if(t != Untyped) // setType(t) + + def extract: Option[(Seq[Expr], (Seq[Expr])=>Expr)] = { + val Block(args, rest) = this + Some((args :+ rest, exprs => Block(exprs.init, exprs.last))) + } } - case class Assignment(varId: Identifier, expr: Expr) extends Expr with FixedType { + case class Assignment(varId: Identifier, expr: Expr) extends Expr with FixedType with UnaryExtractable { val fixedType = UnitType + + def extract: Option[(Expr, (Expr)=>Expr)] = { + Some((expr, Assignment(varId, _))) + } } - case class While(cond: Expr, body: Expr) extends Expr with FixedType with ScalacPositional { + case class While(cond: Expr, body: Expr) extends Expr with FixedType with ScalacPositional with BinaryExtractable { val fixedType = UnitType var invariant: Option[Expr] = None def getInvariant: Expr = invariant.get def setInvariant(inv: Expr) = { invariant = Some(inv); this } def setInvariant(inv: Option[Expr]) = { invariant = inv; this } + + def extract: Option[(Expr, Expr, (Expr, Expr)=>Expr)] = { + Some((cond, body, (t1, t2) => While(t1, t2).setInvariant(this.invariant).setPosInfo(this))) + } } - case class Epsilon(pred: Expr) extends Expr with ScalacPositional + case class Epsilon(pred: Expr) extends Expr with ScalacPositional with UnaryExtractable { + def extract: Option[(Expr, (Expr)=>Expr)] = { + Some((pred, (expr: Expr) => Epsilon(expr).setType(this.getType).setPosInfo(this))) + } + } case class EpsilonVariable(pos: (Int, Int)) extends Expr with Terminal //same as let, buf for mutable variable declaration - case class LetVar(binder: Identifier, value: Expr, body: Expr) extends Expr { + case class LetVar(binder: Identifier, value: Expr, body: Expr) extends Expr with BinaryExtractable { binder.markAsLetBinder val et = body.getType if(et != Untyped) setType(et) + + def extract: Option[(Expr, Expr, (Expr, Expr)=>Expr)] = { + val LetVar(binders, expr, body) = this + Some((expr, body, (e: Expr, b: Expr) => LetVar(binders, e, b))) + } } - case class Waypoint(i: Int, expr: Expr) extends Expr + case class Waypoint(i: Int, expr: Expr) extends Expr with UnaryExtractable { + def extract: Option[(Expr, (Expr)=>Expr)] = { + Some((expr, (e: Expr) => Waypoint(i, e))) + } + } //the difference between ArrayUpdate and ArrayUpdated is that the former has a side effect while the latter is the functional version //ArrayUpdate should be eliminated soon in the analysis while ArrayUpdated is kept all the way to the backend - case class ArrayUpdate(array: Expr, index: Expr, newValue: Expr) extends Expr with ScalacPositional with FixedType { + case class ArrayUpdate(array: Expr, index: Expr, newValue: Expr) extends Expr with ScalacPositional with FixedType with NAryExtractable { val fixedType = UnitType + + def extract: Option[(Seq[Expr], (Seq[Expr])=>Expr)] = { + val ArrayUpdate(t1, t2, t3) = this + Some((Seq(t1,t2,t3), (as: Seq[Expr]) => ArrayUpdate(as(0), as(1), as(2)))) + } } }