diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean index cfaef5f975..add87c5e93 100644 --- a/src/Init/Data/Format/Basic.lean +++ b/src/Init/Data/Format/Basic.lean @@ -80,14 +80,6 @@ def isEmpty : Format → Bool def fill (f : Format) : Format := group f (behavior := FlattenBehavior.fill) -@[export lean_format_append] -protected def appendEx (a b : Format) : Format := - append a b - -@[export lean_format_group] -protected def groupEx : Format → Format := - group - instance : Append Format := ⟨Format.append⟩ instance : Coe String Format := ⟨text⟩ diff --git a/src/Lean/Compiler/IR/Format.lean b/src/Lean/Compiler/IR/Format.lean index d63dfd1ad5..ddd7cf7eea 100644 --- a/src/Lean/Compiler/IR/Format.lean +++ b/src/Lean/Compiler/IR/Format.lean @@ -85,7 +85,6 @@ def formatAlt (fmt : FnBody → Format) (indent : Nat) : Alt → Format def formatParams (ps : Array Param) : Format := formatArray ps -@[export lean_ir_format_fn_body_head] def formatFnBodyHead : FnBody → Format | FnBody.vdecl x ty e _ => "let " ++ format x ++ " : " ++ format ty ++ " := " ++ format e | FnBody.jdecl j xs _ _ => format j ++ formatParams xs ++ " := ..." @@ -102,6 +101,10 @@ def formatFnBodyHead : FnBody → Format | FnBody.ret x => "ret " ++ format x | FnBody.unreachable => "⊥" +@[export lean_ir_format_fn_body_head] +private def formatFnBodyHead' (fn : FnBody) : String := + formatFnBodyHead fn |>.pretty + partial def formatFnBody (fnBody : FnBody) (indent : Nat := 2) : Format := let rec loop : FnBody → Format | FnBody.vdecl x ty e b => "let " ++ format x ++ " : " ++ format ty ++ " := " ++ format e ++ ";" ++ Format.line ++ loop b diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 60fea954e5..0371110d33 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -19,7 +19,6 @@ Author: Leonardo de Moura #include "util/nat.h" #include "util/kvmap.h" #include "util/list_fn.h" -#include "util/format.h" #include "kernel/level.h" #include "kernel/expr_eq_fn.h" diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index e1d688fc8b..a475364988 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -363,60 +363,6 @@ std::ostream & operator<<(std::ostream & out, level const & l) { return out; } -format pp(level l, bool unicode, unsigned indent); - -static format pp_child(level const & l, bool unicode, unsigned indent) { - if (is_explicit(l) || is_param(l) || is_mvar(l)) { - return pp(l, unicode, indent); - } else { - return paren(pp(l, unicode, indent)); - } -} - -format pp(level l, bool unicode, unsigned indent) { - if (is_explicit(l)) { - return format(get_depth(l)); - } else { - switch (kind(l)) { - case level_kind::Zero: - lean_unreachable(); // LCOV_EXCL_LINE - case level_kind::Param: - return format(param_id(l)); - case level_kind::MVar: - return format("?") + format(mvar_id(l)); - case level_kind::Succ: { - auto p = to_offset(l); - auto fmt1 = pp_child(p.first, unicode, indent); - return fmt1 + format("+") + format(p.second); - } - case level_kind::Max: case level_kind::IMax: { - format r = format(is_max(l) ? "max" : "imax"); - r += nest(indent, compose(line(), pp_child(level_lhs(l), unicode, indent))); - // max and imax are right associative - while (kind(level_rhs(l)) == kind(l)) { - l = level_rhs(l); - r += nest(indent, compose(line(), pp_child(level_lhs(l), unicode, indent))); - } - r += nest(indent, compose(line(), pp_child(level_rhs(l), unicode, indent))); - return group(r); - }} - lean_unreachable(); // LCOV_EXCL_LINE - } -} - -format pp(level const & l, options const & opts) { - return pp(l, get_pp_unicode(opts), get_pp_indent(opts)); -} - -format pp(level const & lhs, level const & rhs, bool unicode, unsigned indent) { - format leq = unicode ? format("≤") : format("<="); - return group(pp(lhs, unicode, indent) + space() + leq + line() + pp(rhs, unicode, indent)); -} - -format pp(level const & lhs, level const & rhs, options const & opts) { - return pp(lhs, rhs, get_pp_unicode(opts), get_pp_indent(opts)); -} - // A total order on level expressions that has the following properties // - succ(l) is an immediate successor of l. // - zero is the minimal element. diff --git a/src/kernel/level.h b/src/kernel/level.h index e31402458b..7f26ed11ff 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "runtime/list_ref.h" #include "util/name.h" #include "util/options.h" -#include "util/format.h" namespace lean { class environment; @@ -196,15 +195,6 @@ std::ostream & operator<<(std::ostream & out, level const & l); in \c l, l[A] != zero. */ bool is_not_zero(level const & l); -/** \brief Pretty print the given level expression, unicode characters are used if \c unicode is \c true. */ -format pp(level l, bool unicode, unsigned indent); -/** \brief Pretty print the given level expression using the given configuration options. */ -format pp(level const & l, options const & opts = options()); - -/** \brief Pretty print lhs <= rhs, unicode characters are used if \c unicode is \c true. */ -format pp(level const & lhs, level const & rhs, bool unicode, unsigned indent); -/** \brief Pretty print lhs <= rhs using the given configuration options. */ -format pp(level const & lhs, level const & rhs, options const & opts = options()); /** \brief Convert a list of universe level parameter names into a list of levels. */ levels lparams_to_levels(names const & ps); diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp index ff2db4d394..9c4bee5be8 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/src/library/compiler/ir_interpreter.cpp @@ -202,8 +202,8 @@ string_ref name_mangle(name const & n, string_ref const & pre) { } extern "C" object * lean_ir_format_fn_body_head(object * b); -format format_fn_body_head(fn_body const & b) { - return format(lean_ir_format_fn_body_head(b.to_obj_arg())); +std::string format_fn_body_head(fn_body const & b) { + return string_to_std(lean_ir_format_fn_body_head(b.to_obj_arg())); } static bool type_is_scalar(type t) { diff --git a/src/library/trace.cpp b/src/library/trace.cpp index cbb79d44c6..bfa49b7188 100644 --- a/src/library/trace.cpp +++ b/src/library/trace.cpp @@ -183,10 +183,6 @@ std::string pp_expr(environment const & env, options const & opts, expr const & return pp_expr(env, opts, lctx, e); } -void trace_expr(environment const & env, options const & opts, expr const & e) { - tout() << pp_expr(env, opts, e); -} - std::string trace_pp_expr(expr const & e) { return pp_expr(*g_env, *g_opts, e); } diff --git a/src/library/trace.h b/src/library/trace.h index aca633a526..feac201c88 100644 --- a/src/library/trace.h +++ b/src/library/trace.h @@ -51,7 +51,6 @@ if (lean_is_trace_enabled(CName)) { \ tout() << tclass(CName); CODE \ }} -void trace_expr(environment const & env, options const & opts, expr const & e); std::string trace_pp_expr(expr const & e); void initialize_trace(); diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index b3760c408b..06594de367 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -5,5 +5,5 @@ add_library(util OBJECT name.cpp name_set.cpp path.cpp lbool.cpp init_module.cpp list_fn.cpp timeit.cpp timer.cpp name_generator.cpp kvmap.cpp map_foreach.cpp - options.cpp format.cpp option_declarations.cpp shell.cpp + options.cpp option_declarations.cpp shell.cpp "${CMAKE_BINARY_DIR}/util/ffi.cpp") diff --git a/src/util/format.cpp b/src/util/format.cpp deleted file mode 100644 index 692661db5b..0000000000 --- a/src/util/format.cpp +++ /dev/null @@ -1,129 +0,0 @@ -/* - 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 -#include -#include -#include -#include -#include "runtime/interrupt.h" -#include "runtime/sstream.h" -#include "runtime/hash.h" -#include "util/options.h" -#include "util/option_declarations.h" -#include "util/format.h" - -#ifndef LEAN_DEFAULT_PP_INDENTATION -#define LEAN_DEFAULT_PP_INDENTATION 2 -#endif - -#ifndef LEAN_DEFAULT_PP_UNICODE -#define LEAN_DEFAULT_PP_UNICODE true -#endif - -#ifndef LEAN_DEFAULT_PP_WIDTH -#define LEAN_DEFAULT_PP_WIDTH 120 -#endif - -namespace lean { -static name * g_pp_indent = nullptr; -static name * g_pp_unicode = nullptr; -static name * g_pp_width = nullptr; - -unsigned get_pp_indent(options const & o) { - return o.get_unsigned(*g_pp_indent, LEAN_DEFAULT_PP_INDENTATION); -} -bool get_pp_unicode(options const & o) { - return o.get_bool(*g_pp_unicode, LEAN_DEFAULT_PP_UNICODE); -} -unsigned get_pp_width(options const & o) { - return o.get_unsigned(*g_pp_width, LEAN_DEFAULT_PP_WIDTH); -} - -extern "C" object* lean_format_append(object* f1, object* f2); -extern "C" object* lean_format_group(object* f); -extern "C" object* lean_format_pretty(object* f, object* w); - -format compose(format const & f1, format const & f2) { - return format(lean_format_append(f1.to_obj_arg(), f2.to_obj_arg())); -} -format nest(int i, format const & f) { - return format(mk_cnstr(static_cast(format::format_kind::NEST), mk_nat_obj(static_cast(i)), f.to_obj_arg())); -} - -static format * g_line = nullptr; -static format * g_space = nullptr; -format line() { return *g_line; } -format space() { return *g_space; } -format group(format const & f) { - return format(lean_format_group(f.to_obj_arg())); -} -format bracket(std::string const & l, format const & x, std::string const & r) { - return group(nest(l.size(), format(l) + x + format(r))); -} -format paren(format const & x) { - return group(nest(1, format("(") + x + format(")"))); -} -format operator+(format const & f1, format const & f2) { - return compose(f1, f2); -} - -std::ostream & format::pretty(std::ostream & out, unsigned w, format const & f) { - string_ref s(lean_format_pretty(f.to_obj_arg(), mk_nat_obj(w))); - out << s.data(); - return out; -} - -std::ostream & pretty(std::ostream & out, unsigned w, format const & f) { - return format::pretty(out, w, f); -} - -std::ostream & pretty(std::ostream & out, options const & opts, format const & f) { - return pretty(out, get_pp_width(opts), f); -} - -std::ostream & operator<<(std::ostream & out, format const & f) { - return pretty(out, LEAN_DEFAULT_PP_WIDTH, f); -} - -std::ostream & operator<<(std::ostream & out, pair const & p) { - return pretty(out, p.second, p.first); -} - -bool format_pp_eq(format const & f1, format const & f2, options const & o) { - std::ostringstream out1; - std::ostringstream out2; - out1 << mk_pair(f1, o); - out2 << mk_pair(f2, o); - return out1.str() == out2.str(); -} - -format pp(name const & n) { - return format(n.to_string()); -} - -void initialize_format() { - g_pp_indent = new name{"pp", "indent"}; - mark_persistent(g_pp_indent->raw()); - g_pp_unicode = new name{"pp", "unicode"}; - mark_persistent(g_pp_unicode->raw()); - g_pp_width = new name{"pp", "width"}; - mark_persistent(g_pp_width->raw()); - g_line = new format(box(static_cast(format::format_kind::LINE))); - mark_persistent(g_line->raw()); - g_space = new format(" "); - mark_persistent(g_space->raw()); -} - -void finalize_format() { - delete g_line; - delete g_space; - delete g_pp_indent; - delete g_pp_unicode; - delete g_pp_width; -} -} diff --git a/src/util/format.h b/src/util/format.h deleted file mode 100644 index 17b274961d..0000000000 --- a/src/util/format.h +++ /dev/null @@ -1,97 +0,0 @@ -/* -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 -#include -#include -#include -#include -#include -#include -#include "runtime/debug.h" -#include "runtime/object_ref.h" -#include "util/name.h" -#include "util/pair.h" - -namespace lean { -class options; -/** -inductive Format -| nil : Format -| line : Format -| text : String → Format -| nest : Nat → Format → Format -| compose : Bool → Format → Format → Format -| choice : Format → Format → Format -*/ -class format : public object_ref { - enum format_kind { NIL, LINE, TEXT, NEST, COMPOSE, CHOICE }; -public: - // Constructors - format():object_ref(box(static_cast(NIL))) {} - explicit format(object * o):object_ref(o) {} - explicit format(object_ref const & o):object_ref(o) {} - format(object * o, bool b):object_ref(o, b) {} - explicit format(char const * v):object_ref(mk_cnstr(static_cast(TEXT), mk_string(v))) {} - explicit format(std::string const & v):object_ref(mk_cnstr(static_cast(TEXT), mk_string(v))) {} - explicit format(string_ref const & v):object_ref(mk_cnstr(static_cast(TEXT), v)) {} - explicit format(int v):format(std::to_string(v)) {} - explicit format(unsigned v):format(std::to_string(v)) {} - explicit format(name const & v):format(v.to_string()) {} - format(format const & f):object_ref(f) {} - format(format && other):object_ref(other) {} - format & operator=(format const & other) { object_ref::operator=(other); return *this; } - format & operator=(format && other) { object_ref::operator=(other); return *this; } - format(format const & f1, format const & f2); - - format_kind kind() const { return static_cast(cnstr_tag(raw())); } - bool is_nil_fmt() const { return kind() == format_kind::NIL; } - - friend format compose(format const & f1, format const & f2); - friend format nest(int i, format const & f); - friend format group(format const & f); - friend format bracket(std::string const & l, format const & x, std::string const & r); - - // x + y = x <> y - friend format operator+(format const & f1, format const & f2); - format & operator+=(format const & f) { - *this = *this + f; - return *this; - } - - static std::ostream & pretty(std::ostream & out, unsigned w, format const & f); - friend std::ostream & pretty(std::ostream & out, unsigned w, format const & f); - friend std::ostream & pretty(std::ostream & out, options const & o, format const & f); - - friend std::ostream & operator<<(std::ostream & out, format const & f); - friend std::ostream & operator<<(std::ostream & out, pair const & p); - friend void initialize_format(); -}; - -format compose(format const & f1, format const & f2); -format nest(int i, format const & f); -format line(); -format space(); -format bracket(std::string const & l, format const & x, std::string const & r); -format group(format const & f); -format paren(format const & x); - -class options; -/** \brief Extract indentation from options */ -unsigned get_pp_indent(options const & o); -/** \brief Return unicode characters flag */ -bool get_pp_unicode(options const & o); - -/** \brief Format a hierarchical name */ -format pp(name const & n); - -/** \brief Return true iff \c f1 and \c f2 are equal when formatted with options \c o */ -bool format_pp_eq(format const & f1, format const & f2, options const & o); - -void initialize_format(); -void finalize_format(); -} diff --git a/src/util/init_module.cpp b/src/util/init_module.cpp index da0a6f9d6d..caf60ed0cf 100644 --- a/src/util/init_module.cpp +++ b/src/util/init_module.cpp @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include "util/name.h" #include "util/name_generator.h" #include "util/options.h" -#include "util/format.h" namespace lean { void initialize_util_module() { @@ -18,10 +17,8 @@ void initialize_util_module() { initialize_name(); initialize_name_generator(); initialize_options(); - initialize_format(); } void finalize_util_module() { - finalize_format(); finalize_options(); finalize_name_generator(); finalize_name();