Add pretty-print: format.cpp, format.h

src/util/CMakeLists.txt

@@ -1 +1,4 @@
-add_library(util trace.cpp debug.cpp name.cpp exception.cpp verbosity.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp)
+add_library(util trace.cpp debug.cpp name.cpp exception.cpp
+  verbosity.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp
+  format.cpp
+  )

src/util/format.cpp

@@ -0,0 +1,125 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+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 {
+
+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;
+    }
+    return out;
+}
+
+}
+
+void pp(lean::format const & n) { std::cout << n << "\n"; }

src/util/format.h

@@ -0,0 +1,90 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Soonho Kong
+*/
+#pragma once
+#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.
+
+   S-expressions are used for tracking configuration options, statistics, etc.
+
+   Remark: this datastructure does not allow destructive updates.
+*/
+class format {
+    format_cell* m_ptr;
+
+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);
+        }
+    }
+    ~format();
+
+    format_kind kind() const;
+
+    friend bool is_nil(format const & s) { return s.m_ptr == nullptr; }
+
+    std::string const & get_string() const;
+
+    unsigned hash() const;
+
+    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); }
+
+    // Pointer equality
+    friend bool eqp(format const & a, format const & b) { return a.m_ptr == b.m_ptr; }
+
+    friend std::ostream & operator<<(std::ostream & out, format const & s);
+
+};
+
+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(); }
+}