From 290e50f34a4cb3b6546ccdf71c914a1339efaeb8 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 10 Mar 2016 17:10:08 +0100
Subject: [PATCH] Change reconstruction in DetupleInput
Use a LetPattern
Also reenable printing of LetPattern
---
.../scala/leon/purescala/PrettyPrinter.scala | 2 -
.../leon/synthesis/rules/DetupleInput.scala | 73 ++++++++-----------
2 files changed, 30 insertions(+), 45 deletions(-)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 88f6fd70c..d1975779e 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -392,11 +392,9 @@ class PrettyPrinter(opts: PrinterOptions,
|}"""
}
- /*
case LetPattern(p,s,rhs) =>
p"""|val $p = $s
|$rhs"""
- */
case MatchExpr(s, csc) =>
optP {
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index 0c5385358..28d567e1b 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -8,8 +8,9 @@ import Witnesses.Hint
import purescala.Expressions._
import purescala.Common._
import purescala.Types._
-import purescala.ExprOps._
+import purescala.ExprOps.simplePostTransform
import purescala.Constructors._
+import purescala.Extractors.LetPattern
/** Rule for detupling input variables, to be able to use their sub-expressions. For example, the input variable:
* {{{d: Cons(head: Int, tail: List)}}}
@@ -31,28 +32,24 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
* into a list of fresh typed identifiers, the tuple of these new identifiers,
* and the mapping of those identifiers to their respective expressions.
*/
- def decompose(id: Identifier): (List[Identifier], Expr, Map[Identifier, Expr], Expr => Seq[Expr]) = id.getType match {
+ def decompose(id: Identifier): (List[Identifier], Expr, Expr => Seq[Expr]) = id.getType match {
case cct @ CaseClassType(ccd, _) if !ccd.isAbstract =>
val newIds = cct.fields.map{ vd => FreshIdentifier(vd.id.name, vd.getType, true) }
- val map = (ccd.fields zip newIds).map{ case (vd, nid) => nid -> caseClassSelector(cct, Variable(id), vd.id) }.toMap
-
val tMap: (Expr => Seq[Expr]) = {
case CaseClass(ccd, fields) => fields
}
- (newIds.toList, CaseClass(cct, newIds.map(Variable)), map, tMap)
+ (newIds.toList, CaseClass(cct, newIds.map(Variable)), tMap)
case TupleType(ts) =>
val newIds = ts.zipWithIndex.map{ case (t, i) => FreshIdentifier(id.name+"_"+(i+1), t, true) }
- val map = newIds.zipWithIndex.map{ case (nid, i) => nid -> TupleSelect(Variable(id), i+1) }.toMap
-
val tMap: (Expr => Seq[Expr]) = {
case Tuple(fields) => fields
}
- (newIds.toList, tupleWrap(newIds.map(Variable)), map, tMap)
+ (newIds.toList, tupleWrap(newIds.map(Variable)), tMap)
case _ => sys.error("woot")
}
@@ -62,21 +59,32 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
var subPc = p.pc
var subWs = p.ws
var hints: Seq[Expr] = Nil
-
- var reverseMap = Map[Identifier, Expr]()
+ var patterns = List[(Identifier, Pattern)]()
+ var revMap = Map[Expr, Expr]().withDefault((e: Expr) => e)
var ebMapInfo = Map[Identifier, Expr => Seq[Expr]]()
val subAs = p.as.map { a =>
if (isDecomposable(a)) {
- val (newIds, expr, map, tMap) = decompose(a)
+ val (newIds, expr, tMap) = decompose(a)
subProblem = subst(a -> expr, subProblem)
subPc = subst(a -> expr, subPc)
subWs = subst(a -> expr, subWs)
+ revMap += expr -> Variable(a)
hints +:= Hint(expr)
- reverseMap ++= map
+ val patts = newIds map (id => WildcardPattern(Some(id)))
+
+ patterns +:= ((
+ a,
+ a.getType match {
+ case TupleType(_) =>
+ TuplePattern(None, patts)
+ case cct: CaseClassType =>
+ CaseClassPattern(None, cct, patts)
+ }
+ ))
ebMapInfo += a -> tMap
@@ -99,40 +107,19 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
val newAs = subAs.flatten
- // Recompose CaseClasses and Tuples.
- // E.g. Cons(l.head, l.tail) ~~> l
- // (t._1, t._2, t._3) ~~> t
- def recompose(e : Expr) : Expr = e match {
- case CaseClass(ct, args) =>
- val (cts, es) = args.zip(ct.fields).map {
- case (CaseClassSelector(ct, e, id), field) if field.id == id => (ct, e)
- case _ =>
- return e
- }.unzip
-
- if (cts.distinct.size == 1 && es.distinct.size == 1) {
- es.head
- } else {
- e
- }
- case Tuple(args) =>
- val es = args.zipWithIndex.map {
- case (TupleSelect(e, i), index) if i == index + 1 => e
- case _ => return e
- }
- if (es.distinct.size == 1) {
- es.head
- } else {
- e
- }
- case other => other
- }
-
+ val (as, patts) = patterns.unzip
+
val sub = Problem(newAs, subWs, subPc, subProblem, p.xs, eb).withWs(hints)
- val s = (substAll(reverseMap, _:Expr)) andThen simplePostTransform(recompose)
+ val s = { (e: Expr) =>
+ LetPattern(
+ tuplePatternWrap(patts),
+ tupleWrap(as map Variable),
+ simplePostTransform(revMap)(e)
+ )
+ }
- Some(decomp(List(sub), forwardMap(s), s"Detuple ${reverseMap.keySet.mkString(", ")}"))
+ Some(decomp(List(sub), forwardMap(s), s"Detuple ${as.mkString(", ")}"))
} else {
None
}
--
GitLab