From 9321437a5c0d4aba6dd7fa9924c4207cdc6fb1c7 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 29 Jul 2016 13:34:43 +0200
Subject: [PATCH] Fix bug in isPurelyFunctional, comments
---
src/main/scala/inox/ast/ExprOps.scala | 11 ++++-------
src/main/scala/inox/ast/Trees.scala | 3 +--
2 files changed, 5 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala
index c5d3a275e..21151ac9a 100644
--- a/src/main/scala/inox/ast/ExprOps.scala
+++ b/src/main/scala/inox/ast/ExprOps.scala
@@ -3,10 +3,7 @@
package inox
package ast
-import utils._
-import scala.reflect._
-
-/** Provides functions to manipulate [[purescala.Expressions]].
+/** Provides functions to manipulate [[Expressions.Expr]].
*
* This object provides a few generic operations on Leon expressions,
* as well as some common operations.
@@ -114,9 +111,9 @@ trait ExprOps extends GenTreeOps {
/** Returns if this expression behaves as a purely functional construct,
* i.e. always returns the same value (for the same environment) and has no side-effects
*/
- def isPurelyFunctional(e: Expr): Boolean = exists {
- case _ : Error => false
- case _ => true
+ def isPurelyFunctional(e: Expr): Boolean = !exists {
+ case _ : Error => true
+ case _ => false
}(e)
/** Extracts the body without its specification
diff --git a/src/main/scala/inox/ast/Trees.scala b/src/main/scala/inox/ast/Trees.scala
index 426a6e9c9..321ff6921 100644
--- a/src/main/scala/inox/ast/Trees.scala
+++ b/src/main/scala/inox/ast/Trees.scala
@@ -80,7 +80,6 @@ trait Trees extends Expressions with Extractors with Types with Definitions with
/** Builds a fresh identifier
*
* @param name The name of the identifier
- * @param tpe The type of the identifier
* @param alwaysShowUniqueID If the unique ID should always be shown
*/
def apply(name: String, alwaysShowUniqueID: Boolean = false) : Identifier = {
@@ -92,7 +91,7 @@ trait Trees extends Expressions with Extractors with Types with Definitions with
*
* @param name The name of the identifier
* @param forceId The forced ID of the identifier
- * @param tpe The type of the identifier
+ * @param alwaysShowUniqueID If the unique ID should always be shown
*/
def forceId(name: String, forceId: Int, alwaysShowUniqueID: Boolean = false): Identifier =
new Identifier(decode(name), uniqueCounter.nextGlobal, forceId, alwaysShowUniqueID)
--
GitLab