Skip to content
Snippets Groups Projects
Commit 99e0058c authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Simplify outer If in case it's not necessary

parent 27e1cbea
No related branches found
No related tags found
No related merge requests found
...@@ -7,6 +7,16 @@ import leon.purescala.Trees._ ...@@ -7,6 +7,16 @@ import leon.purescala.Trees._
// ⟨ P | T ⟩ // ⟨ P | T ⟩
case class Solution(pre: Expr, term: Expr, score: Score = 0) { case class Solution(pre: Expr, term: Expr, score: Score = 0) {
override def toString = "⟨ "+pre+" | "+term+" ⟩" override def toString = "⟨ "+pre+" | "+term+" ⟩"
def toExpr = {
if (pre == BooleanLiteral(true)) {
term
} else if (pre == BooleanLiteral(false)) {
Error("Impossible program").setType(term.getType)
} else {
IfExpr(pre, term, Error("Precondition failed").setType(term.getType))
}
}
} }
object Solution { object Solution {
......
...@@ -96,7 +96,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) { ...@@ -96,7 +96,7 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
val sol = synthesize(Problem(as, phi, xs), rules) val sol = synthesize(Problem(as, phi, xs), rules)
info("Scala code:") info("Scala code:")
info(ScalaPrinter(IfExpr(sol.pre, sol.term, Error("Precondition failed").setType(sol.term.getType)))) info(ScalaPrinter(sol.toExpr))
a a
case _ => case _ =>
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment