From f0a4f518191613f17d64d29b9987b28bec894afa Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 20 Apr 2016 16:09:43 +0200
Subject: [PATCH] Slightly enrich Path API/improve style
---
src/main/scala/leon/purescala/Path.scala | 17 +++++++++--------
1 file changed, 9 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/purescala/Path.scala b/src/main/scala/leon/purescala/Path.scala
index c090d7010..f8a70316e 100644
--- a/src/main/scala/leon/purescala/Path.scala
+++ b/src/main/scala/leon/purescala/Path.scala
@@ -7,7 +7,6 @@ import Common._
import Definitions._
import Expressions._
import Constructors._
-import Extractors._
import ExprOps._
import Types._
@@ -31,7 +30,7 @@ object Path {
* could introduce non-sensical equations.
*/
class Path private[purescala](
- private[purescala] val elements: Seq[Either[(Identifier, Expr), Expr]]) {
+ private[purescala] val elements: Seq[Either[(Identifier, Expr), Expr]]) extends Printable {
def withBinding(p: (Identifier, Expr)) = new Path(elements :+ Left(p))
def withBindings(ps: Iterable[(Identifier, Expr)]) = new Path(elements ++ ps.map(Left(_)))
@@ -69,10 +68,10 @@ class Path private[purescala](
*
* A path is empty iff it contains no let-bindings and its path condition is trivial.
*/
- def isEmpty = elements.filter {
- case Right(BooleanLiteral(true)) => false
- case _ => true
- }.isEmpty
+ def isEmpty = elements.forall {
+ case Right(BooleanLiteral(true)) => true
+ case _ => false
+ }
/** Returns the negation of a path
*
@@ -116,6 +115,8 @@ class Path private[purescala](
)(elements)
lazy val bindings: Seq[(Identifier, Expr)] = elements.collect { case Left(p) => p }
+ lazy val boundIds = bindings map (_._1)
+ lazy val bindingsAsEqs = bindings map { case (id,e) => Equals(id.toVariable, e) }
lazy val conditions: Seq[Expr] = elements.collect { case Right(e) => e }
def isBound(id: Identifier): Boolean = bindings.exists(p => p._1 == id)
@@ -149,7 +150,7 @@ class Path private[purescala](
def and(base: Expr) = distributiveClause(base, Constructors.and(_, _))
/** Fold the path into an implication of `base`, namely `path ==> base` */
- def implies(base: Expr) = distributiveClause(base, Constructors.implies(_, _))
+ def implies(base: Expr) = distributiveClause(base, Constructors.implies)
/** Folds the path into a `require` wrapping the expression `body`
*
@@ -184,7 +185,7 @@ class Path private[purescala](
/** Like [[toClause]] but doesn't simplify final path through constructors
* from [[leon.purescala.Constructors]] */
- lazy val fullClause: Expr = fold[Expr](BooleanLiteral(true), Let(_, _, _), And(_, _))(elements)
+ lazy val fullClause: Expr = fold[Expr](BooleanLiteral(true), Let, And(_, _))(elements)
/** Folds the path into a boolean proposition where let-bindings are
* replaced by equations.
--
GitLab