From 56f5657ee76ce1e51e2e941f5a25abaf064fce98 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Jan 2014 13:13:16 -0800
Subject: [PATCH] fix(library/simplifier): ordered rewriting

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/simplifier/simplifier.cpp | 19 ++++---------------
 1 file changed, 4 insertions(+), 15 deletions(-)

diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp
index 0da0a0342..f1b9765d4 100644
--- a/src/library/simplifier/simplifier.cpp
+++ b/src/library/simplifier/simplifier.cpp
@@ -478,14 +478,6 @@ class simplifier_fn {
         return true;
     }
 
-    bool sorted_args(unsigned num, expr const * args) {
-        for (unsigned i = 1; i < num; i++) {
-            if (!is_lt(args[i-1], args[i], false))
-                return false;
-        }
-        return true;
-    }
-
     /**
        \brief Auxiliary function used by m_match_fn, it tries to match the given rule and
        the expression in the temporary field \c m_target.
@@ -500,10 +492,10 @@ class simplifier_fn {
             m_new_args.clear();
             m_new_args.resize(num+1);
             if (found_all_args(num)) {
-                if (rule.is_permutation() && sorted_args(num, m_new_args.begin()+1))
-                    return false;
                 // easy case: all arguments found
                 m_new_rhs   = instantiate(rule.get_rhs(), num, m_new_args.data() + 1);
+                if (rule.is_permutation() && !is_lt(m_new_rhs, m_target, false))
+                    return false;
                 if (m_proofs_enabled) {
                     if (num > 0) {
                         m_new_args[0] = rule.get_proof();
@@ -561,9 +553,9 @@ class simplifier_fn {
 
     result simplify_constant(expr const & e) {
         lean_assert(is_constant(e));
-        if (m_unfold || m_eval) {
+        if (m_unfold) {
             auto obj = m_env->find_object(const_name(e));
-            if (m_unfold && should_unfold(obj)) {
+            if (should_unfold(obj)) {
                 expr e = obj->get_value();
                 if (m_single_pass) {
                     return result(e);
@@ -571,9 +563,6 @@ class simplifier_fn {
                     return simplify(e);
                 }
             }
-            if (m_eval && obj->is_builtin()) {
-                return result(obj->get_value());
-            }
         }
         return rewrite(e, result(e));
     }