diff --git a/src/util/format.cpp b/src/util/format.cpp
index ec195017a..452570928 100644
--- a/src/util/format.cpp
+++ b/src/util/format.cpp
@@ -5,121 +5,92 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Soonho Kong
 */
 #include <cstring>
-#include "rc.h"
-#include "hash.h"
 #include "sexpr.h"
 #include "format.h"
-#include "name.h"
-#include "mpz.h"
-#include "mpq.h"
 
 namespace lean {
+std::ostream & layout(std::ostream & out, sexpr const & s) {
+    if(is_cons(s)) {
+        sexpr v = cdr(s);
 
-struct format_cell {
-    void dealloc();
-    MK_LEAN_RC()
-    format_kind  m_kind;
-    sexpr        m_value;
-    format_cell(format_kind k):m_rc(1), m_kind(k) {}
-    format_cell(char const * v):
-        format_cell(format_kind::TEXT) {
-        m_value = sexpr(v);
-    }
-    format_cell(std::string const & v):
-        format_cell(format_kind::TEXT) {
-        m_value = sexpr(v);
-    }
-    format_cell(int v):
-        format_cell(format_kind::TEXT) {
-        m_value = sexpr(v);
-    }
-    format_cell(double v):
-        format_cell(format_kind::TEXT) {
-        m_value = sexpr(v);
-    }
-    format_cell(name const & v):
-        format_cell(format_kind::TEXT) {
-        m_value = sexpr(v);
-    }
-    format_cell(mpz const & v):
-        format_cell(format_kind::TEXT) {
-        m_value = sexpr(v);
-    }
-    format_cell(mpq const & v):
-        format_cell(format_kind::TEXT) {
-        m_value = sexpr(v);
-    }
-    format_cell(format_cell const * h, format_cell const * t):
-        format_cell(format_kind::COMPOSE) {
-        m_value = sexpr(h->m_value, h->m_value);
-    }
-};
-
-void format_cell::dealloc() {
-    switch (m_kind) {
-    case format_kind::NIL:         lean_unreachable();  break;
-    case format_kind::INDENT:      delete this;         break;
-    case format_kind::COMPOSE:     delete this;         break;
-    case format_kind::CHOICE:      delete this;         break;
-    case format_kind::LINE:        delete this;         break;
-    case format_kind::TEXT:        delete this;         break;
-    }
-}
-
-format::format(char const * v):m_ptr(new format_cell(v)) {}
-format::format(std::string const & v):m_ptr(new format_cell(v)) {}
-format::format(int v):m_ptr(new format_cell(v)) {}
-format::format(double v):m_ptr(new format_cell(v)) {}
-format::format(name const & v):m_ptr(new format_cell(v)) {}
-format::format(mpz const & v):m_ptr(new format_cell(v)) {}
-format::format(mpq const & v):m_ptr(new format_cell(v)) {}
-format::format(format const & h, format const & t):m_ptr(new format_cell(h.m_ptr, t.m_ptr)) {}
-format::format(format const & s):m_ptr(s.m_ptr) {
-    if (m_ptr)
-        m_ptr->inc_ref();
-}
-format::format(format && s):m_ptr(s.m_ptr) {
-    s.m_ptr = 0;
-}
-format::~format() {
-    if (m_ptr)
-        m_ptr->dec_ref();
-}
-
-format_kind format::kind() const { return m_ptr ? m_ptr->m_kind : format_kind::NIL; }
-std::string const & format::get_string() const { return m_ptr->m_value.get_string(); }
-
-unsigned format::hash() const { return m_ptr == nullptr ? 23 : m_ptr->m_value.hash(); }
-
-format & format::operator=(format const & f) {
-    if (f.m_ptr)
-        f.m_ptr->inc_ref();
-    if (m_ptr)
-        m_ptr->dec_ref();
-    m_ptr = f.m_ptr;
-    return *this;
-}
-
-format & format::operator=(format && f) {
-    if (m_ptr)
-        m_ptr->dec_ref();
-    m_ptr   = f.m_ptr;
-    f.m_ptr = 0;
-    return *this;
-}
-
-std::ostream & operator<<(std::ostream & out, format const & s) {
-    switch (s.kind()) {
-    case format_kind::NIL:         out << "nil";  break;
-    case format_kind::INDENT:      out << "nil";  break;
-    case format_kind::TEXT:        out << "TODO"; break;
-    case format_kind::COMPOSE:     out << "TODO"; break;
-    case format_kind::CHOICE:      out << "TODO"; break;
-    case format_kind::LINE:        out << "TODO"; break;
+        switch (to_int(car(s))) {
+        case format::format_kind::NIL:
+            out << "NIL";
+            break;
+        case format::format_kind::NEST:
+            out << "NEST("
+                << car(v)
+                << ", ";
+            layout(out, cdr(v));
+            out << ")";
+            break;
+        case format::format_kind::COMPOSE:
+            out << "COMPOSE(";
+            layout(out, car(v));
+            out << ", ";
+            layout(out, cdr(v));
+            out << ")";
+            break;
+        case format::format_kind::CHOICE:
+            out << "CHOICE(";
+            layout(out, car(v));
+            out << ", ";
+            layout(out, cdr(v));
+            out << ")";
+            break;
+        case format::format_kind::LINE:
+            out << "LINE()";
+            break;
+        }
+    } else {
+        out << s;
     }
     return out;
 }
 
+std::ostream & operator<<(std::ostream & out, format const & f) {
+    return layout(out, f.m_value);
 }
 
-void pp(lean::format const & n) { std::cout << n << "\n"; }
+sexpr flatten(sexpr const & s) {
+    if(is_cons(s)) {
+        sexpr v = cdr(s);
+        switch (to_int(car(s))) {
+        case format::format_kind::NIL:
+            /* flatten NIL = NIL */
+            return s;
+
+        case format::format_kind::NEST:
+            /* flatten (NEST i x) = flatten x */
+            return flatten(cdr(v));
+
+        case format::format_kind::COMPOSE:
+            /* flatten (x <> y) = flatten x <> flatten y */
+            return sexpr(format::format_kind::COMPOSE,
+                         sexpr(flatten(car(v)),
+                               flatten(cdr(v))));
+
+        case format::format_kind::CHOICE:
+            /* flatten (x <|> y) = flatten x */
+            return flatten(car(v));
+
+        case format::format_kind::LINE:
+            return sexpr(" ");
+
+        }
+    }
+    return s;
+}
+
+format flatten(format const & f){
+    return format(flatten(f.m_value));
+}
+
+format group(format const & f) {
+    return choice(flatten(f), f);
+}
+
+}
+
+
+void pp(lean::format const & n) { std::cout << "pp" << "\n"; }
diff --git a/src/util/format.h b/src/util/format.h
index e86d8b4fd..77398d349 100644
--- a/src/util/format.h
+++ b/src/util/format.h
@@ -5,86 +5,97 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Soonho Kong
 */
 #pragma once
+#include "sexpr.h"
 #include <iostream>
 
 namespace lean {
-class name;
-class mpq;
-class mpz;
-struct format_cell;
-
-enum class format_kind { NIL, INDENT, COMPOSE, CHOICE, LINE, TEXT };
-
 /**
-   \brief Simple LISP-like S-expressions.
-   1. Atoms: nil, string, int, name, mpz or mpq
-   2. Pair: (x . y) where x and y are S-expressions.
+   \brief Format
 
-   S-expressions are used for tracking configuration options, statistics, etc.
+   uses `sexpr` as an internal representation.
+
+   nil           = nil sexpr
+   text    s     = ("TEXT"    s    )
+   nest    f     = ("NEST"    f    )
+   choice  f1 f2 = ("CHOICE"  f1 f2)
+   compose f1 f2 = ("COMPOSE" f1 f2)
+   line          = ("LINE")
+   nest    n  f  = ("NEST"    n   f)
 
-   Remark: this datastructure does not allow destructive updates.
 */
+
 class format {
-    format_cell* m_ptr;
+    sexpr m_value;
 
 public:
-    format():m_ptr(nullptr) {}
-    explicit format(char const * v);
-    explicit format(std::string const & v);
-    explicit format(int v);
-    explicit format(double v);
-    explicit format(name const & v);
-    explicit format(mpz const & v);
-    explicit format(mpq const & v);
-    format(format const & h, format const & t);
-    template<typename T>
-    format(T const & h, format const & t):format(format(h), t) {}
-    template<typename T1, typename T2>
-    format(T1 const & h, T2 const & t):format(format(h), format(t)) {}
-    format(format const & s);
-    format(format && s);
-    template<typename T>
-    format(std::initializer_list<T> const & l):format() {
-        auto it = l.end();
-        while (it != l.begin()) {
-            --it;
-            *this = format(*it, *this);
-        }
+    enum format_kind { NIL, NEST, COMPOSE, CHOICE, LINE, TEXT };
+
+    format():m_value(sexpr()) {}
+    explicit format(sexpr const & v):m_value(v) {}
+    explicit format(char const * v):m_value(v) {}
+    explicit format(std::string const & v):m_value(v) {}
+    explicit format(int v):m_value(v) {}
+    explicit format(double v):m_value(v) {}
+    explicit format(name const & v):m_value(v) {}
+    explicit format(mpz const & v):m_value(v) {}
+    explicit format(mpq const & v):m_value(v) {}
+    format(format const & f1, format const & f2) {
+        m_value = sexpr(sexpr(COMPOSE), sexpr(f1.m_value, f2.m_value));
     }
-    ~format();
+    format(format const & f):m_value(f.m_value) {}
 
-    format_kind kind() const;
+    format_kind kind() const {
+        if(is_nil(m_value)) {
+            return NIL;
+        }
+        if(is_cons(m_value)) {
+            /* CHOICE, COMPOSE, LINE, NEST */
+            return static_cast<format_kind>(to_int(car(m_value)));
+        }
+        return TEXT;
+    }
 
-    friend bool is_nil(format const & s) { return s.m_ptr == nullptr; }
-
-    std::string const & get_string() const;
-
-    unsigned hash() const;
+    unsigned hash() const { return m_value.hash(); }
 
     format & operator=(format const & s);
     format & operator=(format&& s);
     template<typename T>
     format & operator=(T const & v) { return operator=(format(v)); }
 
-    friend void swap(format & a, format & b) { std::swap(a.m_ptr, b.m_ptr); }
+    std::ostream & display(std::ostream & out, sexpr const & s);
+    friend std::ostream & operator<<(std::ostream & out, format const & f);
 
-    // Pointer equality
-    friend bool eqp(format const & a, format const & b) { return a.m_ptr == b.m_ptr; }
+    friend format compose(format const & f1, format const & f2) {
+        return format(f1, f2);
+    }
+    friend format choice(format const & f1, format const & f2) {
+        return format(sexpr(sexpr(CHOICE), sexpr(f1.m_value, f2.m_value)));
+    }
+    friend format nest(int i, format const & f) {
+        return format(sexpr(sexpr(NEST), sexpr(sexpr(i), f.m_value)));
+    }
 
-    friend std::ostream & operator<<(std::ostream & out, format const & s);
+    friend bool is_compose(format const & f)   {
+        return is_cons(f.m_value) && to_int(car(f.m_value)) == format_kind::COMPOSE;
+    }
+    friend bool is_nest(format const & f) {
+        return is_cons(f.m_value) && to_int(car(f.m_value)) == format_kind::NEST;
+    }
+    friend bool is_text(format const & f) {
+        return !is_cons(f.m_value);
+    }
+    friend bool is_line(format const & f) {
+        return is_cons(f.m_value) && to_int(car(f.m_value)) == format_kind::LINE;
+    }
+    friend bool is_choice(format const & f) {
+        return is_cons(f.m_value) && to_int(car(f.m_value)) == format_kind::CHOICE;
+    }
 
+    friend format flatten(format const & f);
 };
 
-inline format compose(format const & head, format const & tail) { return format(head, tail); }
-inline format choice(format const & head, format const & tail) { return format(head, tail); }
-inline format indent(format const & f, unsigned i) { return f; }
-inline format line(format const & f) { return f; }
-
-inline bool is_compose(format const & s)   { return s.kind() != format_kind::COMPOSE; }
-inline bool is_indent(format const & s)   { return s.kind() == format_kind::INDENT; }
-inline bool is_text(format const & s) { return s.kind() == format_kind::TEXT; }
-inline bool is_line(format const & s)    { return s.kind() == format_kind::LINE; }
-inline bool is_choice(format const & s) { return s.kind() == format_kind::CHOICE; }
-
-inline std::string const & to_string(format const & s) { return s.get_string(); }
+inline format line() {
+    return format(sexpr(format::format_kind::LINE));
+}
+
 }