From ad6aeaa2d58334a75d2303270101751b8a8505e1 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 18 Aug 2014 18:17:33 +0200
Subject: [PATCH] Remove Let/LetTuple madness, rely on constructors
---
src/main/scala/leon/synthesis/ConvertHoles.scala | 7 ++-----
src/main/scala/leon/synthesis/ConvertWithOracles.scala | 7 ++-----
.../scala/leon/synthesis/rules/DetupleOutput.scala | 4 ++--
src/main/scala/leon/synthesis/rules/OnePoint.scala | 10 +++-------
.../leon/synthesis/rules/UnconstrainedOutput.scala | 10 +++-------
5 files changed, 12 insertions(+), 26 deletions(-)
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 60a6f8ea0..be878918a 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -8,6 +8,7 @@ import purescala.Trees._
import purescala.TypeTrees._
import purescala.TreeOps._
import purescala.Definitions._
+import purescala.Constructors._
object ConvertHoles extends LeonPhase[Program, Program] {
val name = "Convert Holes to Choose"
@@ -62,11 +63,7 @@ object ConvertHoles extends LeonPhase[Program, Program] {
BooleanLiteral(true)
}
- val withChoose = if (holes.size > 1) {
- LetTuple(holes, Choose(cids, pred), newBody)
- } else {
- Let(holes.head, Choose(cids, pred), newBody)
- }
+ val withChoose = letTuple(holes, Choose(cids, pred), newBody)
fd.body = Some(withChoose)
}
diff --git a/src/main/scala/leon/synthesis/ConvertWithOracles.scala b/src/main/scala/leon/synthesis/ConvertWithOracles.scala
index d7c1b6853..f8072b71a 100644
--- a/src/main/scala/leon/synthesis/ConvertWithOracles.scala
+++ b/src/main/scala/leon/synthesis/ConvertWithOracles.scala
@@ -7,6 +7,7 @@ import purescala.Common._
import purescala.Trees._
import purescala.TreeOps._
import purescala.Definitions._
+import purescala.Constructors._
object ConvertWithOracle extends LeonPhase[Program, Program] {
val name = "Convert WithOracle to Choose"
@@ -53,11 +54,7 @@ object ConvertWithOracle extends LeonPhase[Program, Program] {
BooleanLiteral(true)
}
- if (chooseOs.size > 1) {
- Some(LetTuple(os, Choose(chooseOs, pred), b))
- } else {
- Some(Let(os.head, Choose(chooseOs, pred), b))
- }
+ Some(letTuple(os, Choose(chooseOs, pred), b))
case None =>
None
}
diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
index a042753a6..f64f3f31b 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
@@ -10,6 +10,7 @@ import purescala.Common._
import purescala.TypeTrees._
import purescala.TreeOps._
import purescala.Extractors._
+import purescala.Constructors._
case object DetupleOutput extends Rule("Detuple Out") {
@@ -39,13 +40,12 @@ case object DetupleOutput extends Rule("Detuple Out") {
}.unzip
val newOuts = subOuts.flatten
- //sctx.reporter.warning("newOuts: " + newOuts.toString)
val sub = Problem(p.as, p.pc, subProblem, newOuts)
val onSuccess: List[Solution] => Option[Solution] = {
case List(sol) =>
- Some(Solution(sol.pre, sol.defs, LetTuple(newOuts, sol.term, Tuple(outerOuts))))
+ Some(Solution(sol.pre, sol.defs, letTuple(newOuts, sol.term, Tuple(outerOuts))))
case _ =>
None
}
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 7deff8fe6..39286e3c1 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -8,6 +8,7 @@ import purescala.Common._
import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
+import purescala.Constructors._
case object OnePoint extends NormalizingRule("One-point") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
@@ -32,14 +33,9 @@ case object OnePoint extends NormalizingRule("One-point") {
val newProblem = Problem(p.as, p.pc, subst(x -> e, And(others)), oxs)
- val onSuccess: List[Solution] => Option[Solution] = {
+ val onSuccess: List[Solution] => Option[Solution] = {
case List(Solution(pre, defs, term)) =>
- if (oxs.isEmpty) {
- Some(Solution(pre, defs, Tuple(e :: Nil)))
- } else {
- Some(Solution(pre, defs, LetTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_)))))))
- }
-
+ Some(Solution(pre, defs, letTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_)))))))
case _ =>
None
}
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 1e5a3a331..b349279c5 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -7,6 +7,7 @@ package rules
import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
+import purescala.Constructors._
case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
@@ -17,13 +18,8 @@ case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
val onSuccess: List[Solution] => Option[Solution] = {
case List(s) =>
- val term = if (sub.xs.size > 1) {
- LetTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(id.getType) else Variable(id))))
- } else if (sub.xs.size == 1) {
- Let(sub.xs.head, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(id.getType) else Variable(id))))
- } else {
- Tuple(p.xs.map(id => simplestValue(id.getType)))
- }
+ val term = letTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(id.getType) else Variable(id))))
+
Some(Solution(s.pre, s.defs, term))
case _ =>
None
--
GitLab