From a61111367ae2b119157238a6817022b9654c498e Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Fri, 21 Nov 2014 16:59:16 +0100
Subject: [PATCH] Introduce LetPattern, LetTuple specializes it for
TuplePatterns
---
project/build.properties | 2 +-
.../scala/leon/codegen/CodeGeneration.scala | 19 ----------
src/main/scala/leon/purescala/Common.scala | 10 ++++++
.../scala/leon/purescala/Constructors.scala | 7 +++-
.../scala/leon/purescala/Extractors.scala | 30 +++++++++++++++-
.../scala/leon/purescala/PrettyPrinter.scala | 36 +++++++++++--------
.../leon/purescala/ScopeSimplifier.scala | 14 +-------
.../leon/purescala/TransformerWithPC.scala | 5 ---
src/main/scala/leon/purescala/TreeOps.scala | 28 +++------------
src/main/scala/leon/purescala/Trees.scala | 9 ++---
.../scala/leon/purescala/TypeTreeOps.scala | 4 ---
.../solvers/templates/TemplateGenerator.scala | 3 +-
.../leon/solvers/z3/AbstractZ3Solver.scala | 26 ++++++++------
.../synthesis/utils/ExpressionGrammar.scala | 2 +-
14 files changed, 92 insertions(+), 103 deletions(-)
diff --git a/project/build.properties b/project/build.properties
index be6c454fb..748703f77 100644
--- a/project/build.properties
+++ b/project/build.properties
@@ -1 +1 @@
-sbt.version=0.13.5
+sbt.version=0.13.7
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index ff969c68b..8a548ecdb 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -224,25 +224,6 @@ trait CodeGeneration {
ch << instr
mkExpr(b, ch)(locals.withVar(i -> slot))
- case LetTuple(is,d,b) =>
- mkExpr(d, ch) // the tuple
- var count = 0
- val withSlots = is.map(i => (i, ch.getFreshVar))
- for((i,s) <- withSlots) {
- ch << DUP
- ch << Ldc(count)
- ch << InvokeVirtual(TupleClass, "get", "(I)Ljava/lang/Object;")
- mkUnbox(i.getType, ch)
- val instr = i.getType match {
- case Int32Type | CharType | BooleanType | UnitType => IStore(s)
- case _ => AStore(s)
- }
- ch << instr
- count += 1
- }
- ch << POP
- mkExpr(b, ch)(locals.withVars(withSlots.toMap))
-
case IntLiteral(v) =>
ch << Ldc(v)
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index a34958333..626bfe4a4 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -91,4 +91,14 @@ object Common {
}
+ def aliased(id1 : Identifier, id2 : Identifier) = {
+ id1.toString == id2.toString
+ }
+
+ def aliased(ids1 : Set[Identifier], ids2 : Set[Identifier]) = {
+ val s1 = ids1.groupBy{ _.toString }.keySet
+ val s2 = ids2.groupBy{ _.toString }.keySet
+ !(s1 & s2).isEmpty
+ }
+
}
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 9ec719e25..f81e359ef 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -30,7 +30,12 @@ object Constructors {
Let(x, tupleSelect(value, 1), body)
}
case xs =>
- LetTuple(xs, value, body)
+ require(
+ value.getType.isInstanceOf[TupleType],
+ s"The definition value in LetTuple must be of some tuple type; yet we got [${value.getType}]. In expr: \n$this"
+ )
+
+ Extractors.LetPattern(TuplePattern(None,binders map { b => WildcardPattern(Some(b)) }), value, body)
}
def tupleChoose(ch: Choose): Expr = {
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index d8ba07c13..d329c6d3b 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -67,7 +67,6 @@ object Extractors {
case MapIsDefinedAt(t1,t2) => Some((t1,t2, MapIsDefinedAt))
case ArraySelect(t1, t2) => Some((t1, t2, ArraySelect))
case Let(binders, e, body) => Some((e, body, (e: Expr, b: Expr) => Let(binders, e, b)))
- case LetTuple(binders, e, body) => Some((e, body, (e: Expr, b: Expr) => LetTuple(binders, e, b)))
case Require(pre, body) => Some((pre, body, Require))
case Ensuring(body, id, post) => Some((body, post, (b: Expr, p: Expr) => Ensuring(b, id, p)))
case Assert(const, oerr, body) => Some((const, body, (c: Expr, b: Expr) => Assert(c, oerr, b)))
@@ -304,4 +303,33 @@ object Extractors {
case other => Seq(other)
}
}
+
+ object LetPattern {
+ def apply(patt : Pattern, value: Expr, body: Expr) : Expr = {
+ patt match {
+ case WildcardPattern(Some(binder)) => Let(binder, value, body)
+ case _ => MatchExpr(value, List(SimpleCase(patt, body)))
+ }
+ }
+
+ def unapply(me : MatchExpr) : Option[(Pattern, Expr, Expr)] = {
+ if (me eq null) None else { me match {
+ case MatchExpr(scrut, List(SimpleCase(pattern, body))) if !aliased(pattern.binders, variablesOf(scrut)) =>
+ Some(( pattern, scrut, body ))
+ case _ => None
+ }}
+ }
+ }
+
+ object LetTuple {
+ def unapply(me : MatchExpr) : Option[(Seq[Identifier], Expr, Expr)] = {
+ if (me eq null) None else { me match {
+ case LetPattern(TuplePattern(None,subPatts), value, body) if
+ subPatts forall { case WildcardPattern(Some(_)) => true; case _ => false } =>
+ Some((subPatts map { _.binder.get }, value, body ))
+ case _ => None
+ }}
+ }
+ }
+
}
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 43d98b758..8127e0af6 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -13,8 +13,9 @@ import utils._
import java.lang.StringBuffer
import PrinterHelpers._
-import TreeOps.{isStringLiteral, isListLiteral, simplestValue}
+import TreeOps.{isStringLiteral, isListLiteral, simplestValue, variablesOf}
import TypeTreeOps.leastUpperBound
+import Extractors.LetPattern
import synthesis.Witnesses._
@@ -174,20 +175,9 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case Variable(id) =>
p"$id"
- case LetTuple(bs,d,e) =>
- optB { e match {
- case _:LetDef | _ : Let | _ : LetTuple =>
- p"""|val ($bs) = {
- | $d
- |}
- |$e"""
- case _ =>
- p"""|val ($bs) = $d;
- |$e"""
- }}
case Let(b,d,e) =>
optB { e match {
- case _:LetDef | _ : Let | _ : LetTuple =>
+ case _:LetDef | _ : Let | LetPattern(_,_,_) =>
p"""|val $b = {
| $d
|}
@@ -436,6 +426,22 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
|}"""
}
+ case LetPattern(p,s,rhs) =>
+ rhs match {
+ case _:LetDef | _ : Let | LetPattern(_,_,_) =>
+ optP {
+ p"""|val $p = {
+ | $s
+ |}
+ |$rhs"""
+ }
+
+ case _ =>
+ optP {
+ p"""|val $p = $s
+ |$rhs"""
+ }
+ }
case MatchExpr(s, csc) =>
optP {
@@ -680,7 +686,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case (_: Require, _) => true
case (_: Assert, Some(_: Definition)) => true
case (_, Some(_: Definition)) => false
- case (_, Some(_: MatchExpr | _: MatchCase | _: Let | _: LetTuple | _: LetDef )) => false
+ case (_, Some(_: MatchExpr | _: MatchCase | _: Let | _: LetDef )) => false
case (_, _) => true
}
@@ -703,7 +709,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case (_, Some(_: Assert)) => false
case (_, Some(_: Require)) => false
case (_, Some(_: Definition)) => false
- case (_, Some(_: MatchExpr | _: MatchCase | _: Let | _: LetTuple | _: LetDef | _: IfExpr | _ : CaseClass)) => false
+ case (_, Some(_: MatchExpr | _: MatchCase | _: Let | _: LetDef | _: IfExpr | _ : CaseClass)) => false
case (b1 @ BinaryMethodCall(_, _, _), Some(b2 @ BinaryMethodCall(_, _, _))) if precedence(b1) > precedence(b2) => false
case (BinaryMethodCall(_, _, _), Some(_: FunctionInvocation)) => true
case (_, Some(_: FunctionInvocation)) => false
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index 97ba8a1fe..fed50fe43 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -62,19 +62,7 @@ class ScopeSimplifier extends Transformer {
}
LetDef(newFd, rec(body, newScope))
-
- case LetTuple(is, e, b) =>
- var newScope = scope
- val sis = for (i <- is) yield {
- val si = genId(i, newScope)
- newScope = newScope.register(i -> si)
- si
- }
-
- val se = rec(e, scope)
- val sb = rec(b, newScope)
- LetTuple(sis, se, sb)
-
+
case MatchExpr(scrut, cases) =>
val rs = rec(scrut, scope)
diff --git a/src/main/scala/leon/purescala/TransformerWithPC.scala b/src/main/scala/leon/purescala/TransformerWithPC.scala
index a3437b69c..10cc17dfe 100644
--- a/src/main/scala/leon/purescala/TransformerWithPC.scala
+++ b/src/main/scala/leon/purescala/TransformerWithPC.scala
@@ -42,11 +42,6 @@ abstract class TransformerWithPC extends Transformer {
}).copiedFrom(e)
- case LetTuple(is, e, b) =>
- val se = rec(e, path)
- val sb = rec(b, register(Equals(Tuple(is.map(Variable(_))), se), path))
- LetTuple(is, se, sb).copiedFrom(e)
-
case IfExpr(cond, thenn, elze) =>
val rc = rec(cond, path)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 2789fb43a..a0313c5dc 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -447,11 +447,6 @@ object TreeOps {
val newID = FreshIdentifier(i.name, true).copiedFrom(i)
Some(Let(newID, e, replace(Map(Variable(i) -> Variable(newID)), b)))
- case lt @ LetTuple(ids,e,b) =>
- val newIDs = ids.map(_.freshen)
- val substsMap: Map[Expr, Expr] = (ids zip newIDs).map { case (id, newId) => (id.toVariable -> newId.toVariable) }.toMap
- Some(LetTuple(newIDs, e, replace(substsMap, b)))
-
case _ => None
})(expr)
}
@@ -482,7 +477,7 @@ object TreeOps {
Some(Let(id, v, tupleSelect(b, ts)))
case TupleSelect(LetTuple(ids, v, b), ts) =>
- Some(LetTuple(ids, v, tupleSelect(b, ts)))
+ Some(letTuple(ids, v, tupleSelect(b, ts)))
case IfExpr(c, thenn, elze) if (thenn == elze) && isDeterministic(e) =>
Some(thenn)
@@ -578,15 +573,8 @@ object TreeOps {
true
}
}.unzip
-
-
- if (remIds.isEmpty) {
- Some(newBody)
- } else if (remIds.tail.isEmpty) {
- Some(Let(remIds.head, remExprs.head, newBody))
- } else {
- Some(LetTuple(remIds, Tuple(remExprs), newBody))
- }
+
+ Some(Constructors.letTuple(remIds, tupleWrap(remExprs), newBody))
case l @ LetTuple(ids, tExpr: Terminal, body) if isDeterministic(body) =>
val substMap : Map[Expr,Expr] = ids.map(Variable(_) : Expr).zipWithIndex.toMap.map {
@@ -1659,14 +1647,6 @@ object TreeOps {
isHomo(v1, v2) &&
isHomo(e1, e2)(map + (id1 -> id2))
- case (LetTuple(ids1, v1, e1), LetTuple(ids2, v2, e2)) =>
- if (ids1.size == ids2.size) {
- isHomo(v1, v2) &&
- isHomo(e1, e2)(map ++ (ids1 zip ids2))
- } else {
- false
- }
-
case (LetDef(fd1, e1), LetDef(fd2, e2)) =>
fdHomo(fd1, fd2) &&
isHomo(e1, e2)(map + (fd1.id -> fd2.id))
@@ -2015,7 +1995,7 @@ object TreeOps {
case Let(i, e, b) =>
Let(i, e, apply(b, args))
case LetTuple(is, es, b) =>
- LetTuple(is, es, apply(b, args))
+ letTuple(is, es, apply(b, args))
case Lambda(params, body) =>
replaceFromIDs((params.map(_.id) zip args).toMap, body)
case _ => Application(expr, args)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 89a23828b..e8999b26b 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -8,6 +8,7 @@ import utils._
/** AST definitions for Pure Scala. */
object Trees {
import Common._
+ import TreeOps.variablesOf
import TypeTrees._
import TypeTreeOps._
import Definitions._
@@ -55,17 +56,11 @@ object Trees {
}
}
+ /* Like vals */
case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr {
def getType = body.getType
}
- case class LetTuple(binders: Seq[Identifier], value: Expr, body: Expr) extends Expr {
- require(value.getType.isInstanceOf[TupleType],
- "The definition value in LetTuple must be of some tuple type; yet we got [%s]. In expr: \n%s".format(value.getType, this))
-
- def getType = body.getType
- }
-
case class LetDef(fd: FunDef, body: Expr) extends Expr {
def getType = body.getType
}
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala
index 46f8be837..518d19370 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeTreeOps.scala
@@ -279,10 +279,6 @@ object TypeTreeOps {
val newId = freshId(id, tpeSub(id.getType))
Let(newId, srec(value), rec(idsMap + (id -> newId))(body)).copiedFrom(l)
- case l @ LetTuple(ids, value, body) =>
- val newIds = ids.map(id => freshId(id, tpeSub(id.getType)))
- LetTuple(newIds, srec(value), rec(idsMap ++ (ids zip newIds))(body)).copiedFrom(l)
-
case c @ Choose(xs, pred, oimpl) =>
val newXs = xs.map(id => freshId(id, tpeSub(id.getType)))
Choose(newXs, rec(idsMap ++ (xs zip newXs))(pred), oimpl.map(srec)).copiedFrom(c)
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index a570d9597..436220efa 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -206,6 +206,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
val rb = rec(pathVar, replace(Map(Variable(i) -> Variable(newExpr)), b))
rb
+ /* TODO: maybe we want this specialization?
case l @ LetTuple(is, e, b) =>
val tuple : Identifier = FreshIdentifier("t", true).setType(TupleType(is.map(_.getType)))
storeExpr(tuple)
@@ -222,7 +223,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
val rb = rec(pathVar, replace(mapping.toMap, b))
rb
-
+ */
case m : MatchExpr => sys.error("'MatchExpr's should have been eliminated before generating templates.")
case p : Passes => sys.error("'Passes's should have been eliminated before generating templates.")
case g : Gives => sys.error("'Gives' should have been eliminated before generating templates.")
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 03201a3eb..0b599a022 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -10,6 +10,7 @@ import solvers._
import purescala.Common._
import purescala.Definitions._
import purescala.Constructors._
+import purescala.Extractors.LetTuple
import purescala.Trees._
import purescala.TypeTreeOps._
import xlang.Trees._
@@ -495,6 +496,20 @@ trait AbstractZ3Solver
}
def rec(ex: Expr): Z3AST = ex match {
+
+ // TODO: Leave that as a specialization?
+ case LetTuple(ids, e, b) => {
+ var ix = 1
+ z3Vars = z3Vars ++ ids.map((id) => {
+ val entry = (id -> rec(tupleSelect(e, ix)))
+ ix += 1
+ entry
+ })
+ val rb = rec(b)
+ z3Vars = z3Vars -- ids
+ rb
+ }
+
case p @ Passes(_, _, _) =>
rec(p.asConstraint)
@@ -524,17 +539,6 @@ trait AbstractZ3Solver
rb
}
- case LetTuple(ids, e, b) => {
- var ix = 1
- z3Vars = z3Vars ++ ids.map((id) => {
- val entry = (id -> rec(tupleSelect(e, ix)))
- ix += 1
- entry
- })
- val rb = rec(b)
- z3Vars = z3Vars -- ids
- rb
- }
case Waypoint(_, e) => rec(e)
case e @ Error(tpe, _) => {
val newAST = z3.mkFreshConst("errorValue", typeToSort(tpe))
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index 2c8be3cb2..97687c425 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -282,7 +282,7 @@ object ExpressionGrammars {
val subs: Seq[(L, Gen)] = (e match {
- case _: Terminal | _: Let | _: LetTuple | _: LetDef | _: MatchExpr =>
+ case _: Terminal | _: Let | _: LetDef | _: MatchExpr =>
gens(e, gl, Nil, { _ => e }) ++ cegis(gl)
case cc @ CaseClass(cct, exprs) =>
--
GitLab