From d836e454527ee6975eac49ea8265a2e356d06bcd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 22 Feb 2014 23:18:51 -0800 Subject: [PATCH] refactor(library): remove unnecessary files Signed-off-by: Leonardo de Moura --- src/library/CMakeLists.txt | 2 +- src/library/io_state_stream.cpp | 1 - src/library/printer.cpp | 274 -------------------------------- src/library/printer.h | 30 ---- 4 files changed, 1 insertion(+), 306 deletions(-) delete mode 100644 src/library/printer.cpp delete mode 100644 src/library/printer.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 4161d4629..e1cbd9de8 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,7 +1,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state_stream.cpp) # kernel_bindings.cpp # context_to_lambda.cpp placeholder.cpp -# fo_unify.cpp bin_op.cpp equality.cpp printer.cpp +# fo_unify.cpp bin_op.cpp equality.cpp # hop_match.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/io_state_stream.cpp b/src/library/io_state_stream.cpp index 6e10331ee..a3b1527ab 100644 --- a/src/library/io_state_stream.cpp +++ b/src/library/io_state_stream.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include "library/io_state_stream.h" #include "kernel/kernel_exception.h" -#include "library/printer.h" namespace lean { io_state_stream const & operator<<(io_state_stream const & out, endl_class) { out.get_stream() << std::endl; diff --git a/src/library/printer.cpp b/src/library/printer.cpp deleted file mode 100644 index ab6cc2ac4..000000000 --- a/src/library/printer.cpp +++ /dev/null @@ -1,274 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/exception.h" -#include "kernel/environment.h" -#include "kernel/formatter.h" -#include "library/printer.h" - -namespace lean { -bool is_atomic(expr const & e) { - switch (e.kind()) { - case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: - case expr_kind::Type: case expr_kind::MetaVar: - return true; - case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: - case expr_kind::Let: case expr_kind::Sigma: case expr_kind::Proj: - case expr_kind::Pair: case expr_kind::HEq: - return false; - } - return false; -} - -/** - \brief Very basic printer for expressions. - It is mainly used when debugging code. -*/ -struct print_expr_fn { - std::ostream & m_out; - - std::ostream & out() { return m_out; } - - void print_child(expr const & a, context const & c) { - if (is_atomic(a)) { - print(a, c); - } else { - out() << "("; - print(a, c); - out() << ")"; - } - } - - void print_value(expr const & a) { - to_value(a).display(out()); - } - - void print_type(expr const & a) { - if (a == Type()) { - out() << "Type"; - } else { - out() << "(Type " << ty_level(a) << ")"; - } - } - - void print_app(expr const & e, context const & c) { - print_child(arg(e, 0), c); - for (unsigned i = 1; i < num_args(e); i++) { - out() << " "; - print_child(arg(e, i), c); - } - } - - void print_arrow_body(expr const & a, context const & c) { - if (is_atomic(a) || is_arrow(a)) - return print(a, c); - else - return print_child(a, c); - } - - void print_metavar(expr const & a, context const &) { - out() << "?" << metavar_name(a); - if (metavar_lctx(a)) { - out() << "["; - bool first = true; - for (local_entry const & e : metavar_lctx(a)) { - if (first) first = false; else out() << ", "; - if (e.is_lift()) { - out() << "lift:" << e.s() << ":" << e.n(); - } else { - lean_assert(e.is_inst()); - out() << "inst:" << e.s() << " "; - print_child(e.v(), context()); - } - } - out() << "]"; - } - } - - void print_pair(expr const & e, context const & c) { - out() << "pair "; - print_child(pair_first(e), c); - out() << " "; - print_child(pair_second(e), c); - out() << " "; - print_child(pair_type(e), c); - } - - void print(expr const & a, context const & c) { - switch (a.kind()) { - case expr_kind::MetaVar: - print_metavar(a, c); - break; - case expr_kind::Var: { - auto e = find(c, var_idx(a)); - if (e) - out() << e->get_name() << "#" << var_idx(a); - else - out() << "#" << var_idx(a); - break; - } - case expr_kind::Constant: - out() << const_name(a); - break; - case expr_kind::App: - print_app(a, c); - break; - case expr_kind::HEq: - print_child(heq_lhs(a), c); - out() << " == "; - print_child(heq_rhs(a), c); - break; - case expr_kind::Pair: - print_pair(a, c); - break; - case expr_kind::Proj: - out() << "proj" << (proj_first(a) ? "1" : "2") << " "; - print_child(proj_arg(a), c); - break; - case expr_kind::Sigma: - out() << "Sigma " << abst_name(a) << " : "; - print_child(abst_domain(a), c); - out() << ", "; - print_child(abst_body(a), extend(c, abst_name(a), abst_domain(a))); - break; - case expr_kind::Lambda: - out() << "fun " << abst_name(a) << " : "; - print_child(abst_domain(a), c); - out() << ", "; - print_child(abst_body(a), extend(c, abst_name(a), abst_domain(a))); - break; - case expr_kind::Pi: - if (!is_arrow(a)) { - out() << "Pi " << abst_name(a) << " : "; - print_child(abst_domain(a), c); - out() << ", "; - print_child(abst_body(a), extend(c, abst_name(a), abst_domain(a))); - break; - } else { - print_child(abst_domain(a), c); - out() << " -> "; - print_arrow_body(abst_body(a), extend(c, abst_name(a), abst_domain(a))); - } - break; - case expr_kind::Let: - out() << "let " << let_name(a); - if (let_type(a)) { - out() << " : "; - print(*let_type(a), c); - } - out() << " := "; - print(let_value(a), c); - out() << " in "; - print_child(let_body(a), extend(c, let_name(a), let_value(a))); - break; - case expr_kind::Type: - print_type(a); - break; - case expr_kind::Value: - print_value(a); - break; - } - } - - print_expr_fn(std::ostream & out):m_out(out) {} - - void operator()(expr const & e, context const & c) { - print(e, c); - } -}; - -std::ostream & operator<<(std::ostream & out, expr const & e) { - print_expr_fn pr(out); - pr(e, context()); - return out; -} - -std::ostream & operator<<(std::ostream & out, std::pair const & p) { - print_expr_fn pr(out); - pr(p.first, p.second); - return out; -} - -static void display_context_core(std::ostream & out, context const & ctx) { - if (!empty(ctx)) { - auto p = lookup_ext(ctx, 0); - context_entry const & head = p.first; - context const & tail_ctx = p.second; - display_context_core(out, tail_ctx); - if (!empty(tail_ctx)) - out << "; "; - out << head.get_name(); - if (optional const & d = head.get_domain()) - out << " : " << mk_pair(*d, tail_ctx); - if (optional const & b = head.get_body()) { - out << " := " << mk_pair(*b, tail_ctx); - } - } -} - -std::ostream & operator<<(std::ostream & out, context const & ctx) { - out << "["; - display_context_core(out, ctx); - out << "]"; - return out; -} - -std::ostream & operator<<(std::ostream & out, object const & obj) { - out << obj.keyword() << " "; - switch (obj.kind()) { - case object_kind::UVarConstraint: - out << obj.get_name() << " >= " << obj.get_cnstr_level(); break; - case object_kind::Postulate: - out << obj.get_name() << " : " << obj.get_type(); break; - case object_kind::Definition: case object_kind::Builtin: - out << obj.get_name() << " : " << obj.get_type() << " :=\n " << obj.get_value(); break; - case object_kind::BuiltinSet: - out << obj.get_name(); break; - case object_kind::Neutral: - break; - } - return out; -} - -std::ostream & operator<<(std::ostream & out, ro_environment const & env) { - std::for_each(env->begin_objects(), - env->end_objects(), - [&](object const & obj) { out << obj << "\n"; }); - return out; -} - -class simple_formatter_cell : public formatter_cell { -public: - virtual format operator()(expr const & e, options const &) { - std::ostringstream s; s << e; return format(s.str()); - } - virtual format operator()(context const & c, options const &) { - std::ostringstream s; s << c; return format(s.str()); - } - virtual format operator()(context const & c, expr const & e, bool format_ctx, options const &) { - std::ostringstream s; - if (format_ctx) - s << c << " |- "; - s << mk_pair(e, c); - return format(s.str()); - } - virtual format operator()(object const & obj, options const &) { - std::ostringstream s; s << obj; return format(s.str()); - } - virtual format operator()(ro_environment const & env, options const &) { - std::ostringstream s; s << env; return format(s.str()); - } -}; -formatter mk_simple_formatter() { - return mk_formatter(simple_formatter_cell()); -} -} -void print(lean::expr const & a) { std::cout << a << std::endl; } -void print(lean::expr const & a, lean::context const & c) { std::cout << mk_pair(a, c) << std::endl; } -void print(lean::context const & c) { std::cout << c << std::endl; } -void print(lean::ro_environment const & e) { std::cout << e << std::endl; } diff --git a/src/library/printer.h b/src/library/printer.h deleted file mode 100644 index 67c225d32..000000000 --- a/src/library/printer.h +++ /dev/null @@ -1,30 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include "kernel/expr.h" -#include "kernel/context.h" -#include "kernel/formatter.h" - -namespace lean { -class ro_environment; -std::ostream & operator<<(std::ostream & out, context const & ctx); -std::ostream & operator<<(std::ostream & out, expr const & e); -std::ostream & operator<<(std::ostream & out, std::pair const & p); -class object; -std::ostream & operator<<(std::ostream & out, object const & obj); -std::ostream & operator<<(std::ostream & out, ro_environment const & env); -/** - \brief Create a simple formatter object based on \c print function. -*/ -formatter mk_simple_formatter(); -} -void print(lean::expr const & a); -void print(lean::expr const & a, lean::context const & c); -void print(lean::context const & c); -void print(lean::ro_environment const & e);