Update format

1) operator+ is <> (previously, it was a + b = a <> ' ' <> b)
2) using sstream to compute length of text

src/util/format.cpp

@@ -9,9 +9,7 @@
 #include "sexpr_funcs.h"
 
 namespace lean {
-
 static int default_width = 78;
-
 std::ostream & layout(std::ostream & out, sexpr const & s) {
     lean_assert(!is_nil(s));
     switch (format::sexpr_kind(s)) {
@@ -138,17 +136,14 @@ bool format::fits(int w, sexpr const & s) {
     case format_kind::COLOR_BEGIN:
     case format_kind::COLOR_END:
         return fits(w, cdr(s));
-
     case format_kind::TEXT:
     {
-        sexpr const & v = sexpr_text_t(x);
+        size_t l = sexpr_text_length(x);
-        int l = to_string(v).length();
+        if(l - w > 0)
-        if(l > w)
             return false;
         else
             return fits(w - l, cdr(s));
     }
-
     case format_kind::LINE:
         return true;
 
@@ -162,7 +157,7 @@ bool format::fits(int w, sexpr const & s) {
     return false;
 }
 
-sexpr format::be(int w, int k, sexpr const & s, sexpr const & r) {
+sexpr format::be(unsigned w, unsigned k, sexpr const & s, sexpr const & r) {
     /* be w k [] = Nil */
     if(is_nil(s)) {
         if(is_nil(r)) {
@@ -202,10 +197,7 @@ sexpr format::be(int w, int k, sexpr const & s, sexpr const & r) {
         return be(w, k, sexpr(sexpr(i + j, x), z), r);
     }
     case format_kind::TEXT:
-    {
+        return sexpr(v, be(w, k + sexpr_text_length(v), z, r));
-        sexpr const & l = sexpr_text_t(v);
-        return sexpr(v, be(w, k + to_string(l).length(), z, r));
-    }
     case format_kind::LINE:
         return sexpr(v, sexpr(sexpr_text(std::string(i, ' ')), be(w, i, z, r)));
     case format_kind::CHOICE:
@@ -225,7 +217,7 @@ sexpr format::be(int w, int k, sexpr const & s, sexpr const & r) {
     return sexpr();
 }
 
-sexpr format::best(int w, int k, sexpr const & s) {
+sexpr format::best(unsigned w, unsigned k, sexpr const & s) {
     return be(w, k, sexpr{sexpr(0, s)}, sexpr());
 }
 
@@ -235,7 +227,7 @@ std::ostream & operator<<(std::ostream & out, format const & f)
 }
 
 format operator+(format const & f1, format const & f2) {
-    return format{f1, format(" "), f2};
+    return format{f1, f2};
 }
 
 std::ostream & pretty(std::ostream & out, unsigned w, format const & f) {

src/util/format.h

@@ -7,8 +7,9 @@ Author: Soonho Kong
 #pragma once
 #include "sexpr.h"
 #include "debug.h"
-#include <iostream>
 #include <algorithm>
+#include <iostream>
+#include <sstream>
 
 namespace lean {
 /**
@@ -77,6 +78,12 @@ private:
         lean_assert(sexpr_kind(s) == format_kind::TEXT);
         return cdr(s);
     }
+    static inline size_t const sexpr_text_length(sexpr const & s) {
+        lean_assert(sexpr_kind(s) == format_kind::TEXT);
+        std::stringstream ss;
+        ss << cdr(s);
+        return ss.str().length();
+    }
     static inline sexpr sexpr_text(std::string const & s) {
         return sexpr(sexpr(format_kind::TEXT), sexpr(s));
     }
@@ -102,9 +109,9 @@ private:
 
     // Functions used inside of pretty printing
     static bool  fits(int w, sexpr const & s);
-    static sexpr better(int w, int k, sexpr const & s1, sexpr const & s2);
+    static sexpr better(unsigned w, unsigned k, sexpr const & s1, sexpr const & s2);
-    static sexpr be(int w, int k, sexpr const & s, sexpr const & r);
+    static sexpr be(unsigned w, unsigned k, sexpr const & s, sexpr const & r);
-    static sexpr best(int w, int k, sexpr const & s);
+    static sexpr best(unsigned w, unsigned k, sexpr const & s);
 
     static bool is_fnil(format const & f)   {
         return to_int(car(f.m_value)) == format_kind::NIL;
@@ -134,11 +141,9 @@ public:
     explicit format(sexpr const & v):m_value(v) {}
     explicit format(char const * v):m_value(sexpr_text(sexpr(v))) {}
     explicit format(std::string const & v):m_value(sexpr_text(sexpr(v))) {}
-    explicit format(int v):m_value(sexpr_text(sexpr(std::to_string(v)))) {}
+    explicit format(int v):m_value(sexpr_text(sexpr(v))) {}
-    explicit format(double v):m_value(sexpr_text(sexpr(std::to_string(v)))) {}
+    explicit format(double v):m_value(sexpr_text(sexpr(v))) {}
     explicit format(name const & v):m_value(sexpr_text(sexpr(v))) {}
-
-    // TODO: need to convert mpz and mpq to string, and then pass to sexpr
     explicit format(mpz const & v):m_value(sexpr_text(sexpr(v))) {}
     explicit format(mpq const & v):m_value(sexpr_text(sexpr(v))) {}
     format(format const & f1, format const & f2):m_value(sexpr_compose({f1.m_value, f2.m_value})) {}
@@ -173,7 +178,7 @@ public:
     friend format wrap(format const & f1, format const & f2);
 
     format & operator+=(format const & f) {
-        *this = format{*this, format(" "), f};
+        *this = *this + f;
         return *this;
     }
     friend std::ostream & operator<<(std::ostream & out, format const & f);