From fe9d2147d2f4156abce2b9677236eb0df2bc165c Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Thu, 8 Aug 2013 10:34:15 -0700
Subject: [PATCH] Improve performance of format by using
 "space_upto_line_break" instead of "fits"

---
 src/util/format.cpp | 89 ++++++++++++++++++++++++++++++---------------
 src/util/format.h   |  4 +-
 2 files changed, 61 insertions(+), 32 deletions(-)

diff --git a/src/util/format.cpp b/src/util/format.cpp
index 9c3be77da..45ed5b3a9 100644
--- a/src/util/format.cpp
+++ b/src/util/format.cpp
@@ -126,41 +126,70 @@ format wrap(format const & f1, format const & f2) {
                   choice(format(" "), line()),
                   f2};
 }
-bool format::fits(int w, sexpr const & s) {
-    lean_assert(is_list(s));
-    if (is_nil(s))
-        return true;
-    if (w < 0) {
-        return false;
+
+unsigned format::space_upto_line_break_list(sexpr const & r, bool & found) {
+    // r : list of (int * format)
+    lean_assert(!found);
+    if (is_nil(r)) {
+        found = true;
+        return 0;
+    }
+    return format::space_upto_line_break(cdr(car(r)), cdr(r), found);
+}
+
+unsigned format::space_upto_line_break(sexpr const & s, sexpr const & r, bool & found) {
+    // s : format
+    // r : list of (int * format)
+    lean_assert(!found);
+    if(is_nil(s)) {
+        found = true;
+        return 0;
     }
 
-    sexpr const & x = car(s);
-    switch (sexpr_kind(x)) {
+    switch (sexpr_kind(s)) {
     case format_kind::NIL:
     case format_kind::COLOR_BEGIN:
     case format_kind::COLOR_END:
-        return fits(w, cdr(s));
-    case format_kind::TEXT:
-    {
-        size_t l = sexpr_text_length(x);
-        if(w - static_cast<int>(l) < 0) {
-            return false;
-        }
-        else {
-            return fits(w - static_cast<int>(l), cdr(s));
-        }
-    }
-    case format_kind::LINE:
-        return true;
-
+        return 0 + space_upto_line_break_list(r, found);
     case format_kind::COMPOSE:
-    case format_kind::NEST:
-    case format_kind::CHOICE:
-        lean_unreachable();
-        break;
+    {
+        sexpr list  = sexpr_compose_list(s);
+        unsigned len = 0;
+        while(!is_nil(list) && !found) {
+            sexpr const & h = car(list);
+            list = cdr(list);
+            len += space_upto_line_break(h, nil(), found);
+        }
+        if (found) {
+            return len;
+        } else {
+            return len + space_upto_line_break_list(r, found);
+        }
     }
+    case format_kind::NEST:
+    {
+        sexpr const & x = sexpr_nest_s(s);
+        unsigned len = space_upto_line_break(x, nil(), found);
+        if (found) {
+            return len;
+        } else {
+            return len + space_upto_line_break_list(r, found);
+        }
+    }
+    case format_kind::TEXT:
+        return sexpr_text_length(s) + space_upto_line_break_list(r, found);
+    case format_kind::LINE:
+        found = true;
+        return 0;
+    case format_kind::CHOICE:
+    {
+        sexpr const & x = sexpr_choice_1(s);
+        return space_upto_line_break(x, r, found);
+    }
+    }
+    std::cerr << "!!!!!!!!!!!!!!!" << s << std::endl;
     lean_unreachable();
-    return false;
+    return 0;
 }
 
 sexpr format::be(unsigned w, unsigned k, sexpr const & s, sexpr const & r) {
@@ -210,11 +239,11 @@ sexpr format::be(unsigned w, unsigned k, sexpr const & s, sexpr const & r) {
     {
         sexpr const & x = sexpr_choice_1(v);
         sexpr const & y = sexpr_choice_2(v);;
-        int d = static_cast<int>(w) - static_cast<int>(k);
+        bool found = false;
+        int d = static_cast<int>(w) - static_cast<int>(k) - space_upto_line_break(x, r, found);
         if(d >= 0) {
             sexpr const & s1 = be(w, k, sexpr(sexpr(i, x), z), r);
-            if (fits(d, s1))
-                return s1;
+            return s1;
         }
         sexpr const & s2 = be(w, k, sexpr(sexpr(i, y), z), r);
         return s2;
diff --git a/src/util/format.h b/src/util/format.h
index bac73d640..41b999c3e 100644
--- a/src/util/format.h
+++ b/src/util/format.h
@@ -109,8 +109,8 @@ private:
     }
 
     // Functions used inside of pretty printing
-    static bool  fits(int w, sexpr const & s);
-    static sexpr better(unsigned w, unsigned k, sexpr const & s1, sexpr const & s2);
+    static unsigned space_upto_line_break(sexpr const & s, sexpr const & r, bool & found);
+    static unsigned space_upto_line_break_list(sexpr const & r, bool & found);
     static sexpr be(unsigned w, unsigned k, sexpr const & s, sexpr const & r);
     static sexpr best(unsigned w, unsigned k, sexpr const & s);