From 71638a8ad4f0901d16bb1cc8b57fa50ee111c650 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Mon, 22 Jul 2013 18:30:25 -0700 Subject: [PATCH] Add pretty-print: format.cpp, format.h --- src/util/CMakeLists.txt | 5 +- src/util/format.cpp | 125 ++++++++++++++++++++++++++++++++++++++++ src/util/format.h | 90 +++++++++++++++++++++++++++++ 3 files changed, 219 insertions(+), 1 deletion(-) create mode 100644 src/util/format.cpp create mode 100644 src/util/format.h diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index cc94ad9a8..fa69d0ec8 100644 --- a/src/util/CMakeLists.txt +++ b/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 + ) diff --git a/src/util/format.cpp b/src/util/format.cpp new file mode 100644 index 000000000..ec195017a --- /dev/null +++ b/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 +#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"; } diff --git a/src/util/format.h b/src/util/format.h new file mode 100644 index 000000000..e86d8b4fd --- /dev/null +++ b/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 + +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 + format(T const & h, format const & t):format(format(h), t) {} + template + format(T1 const & h, T2 const & t):format(format(h), format(t)) {} + format(format const & s); + format(format && s); + template + format(std::initializer_list 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 + 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(); } +}