chore: remove remnants of C++ `format`
diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean index cfaef5f..add87c5 100644 --- a/src/Init/Data/Format/Basic.lean +++ b/src/Init/Data/Format/Basic.lean
@@ -80,14 +80,6 @@ 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 d63dfd1..ddd7cf7 100644 --- a/src/Lean/Compiler/IR/Format.lean +++ b/src/Lean/Compiler/IR/Format.lean
@@ -85,7 +85,6 @@ 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 @@ | 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 60fea95..0371110 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h
@@ -19,7 +19,6 @@ #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 e1d688f..a475364 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp
@@ -363,60 +363,6 @@ 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 e314024..7f26ed1 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h
@@ -12,7 +12,6 @@ #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 @@ 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 ff2db4d..9c4bee5 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/src/library/compiler/ir_interpreter.cpp
@@ -202,8 +202,8 @@ } 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 dd6a653..2344daf 100644 --- a/src/library/trace.cpp +++ b/src/library/trace.cpp
@@ -183,10 +183,6 @@ 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 3eae4a7..8590a44 100644 --- a/src/library/trace.h +++ b/src/library/trace.h
@@ -51,7 +51,6 @@ 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 b3760c4..06594de 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt
@@ -5,5 +5,5 @@ 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 692661d..0000000 --- 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 <sstream> -#include <string> -#include <cstring> -#include <utility> -#include <vector> -#include <unordered_map> -#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<unsigned>(format::format_kind::NEST), mk_nat_obj(static_cast<unsigned>(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<format const &, options const &> 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<unsigned>(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 17b2749..0000000 --- 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 <algorithm> -#include <iostream> -#include <numeric> -#include <sstream> -#include <utility> -#include <string> -#include <vector> -#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<unsigned>(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<unsigned>(TEXT), mk_string(v))) {} - explicit format(std::string const & v):object_ref(mk_cnstr(static_cast<unsigned>(TEXT), mk_string(v))) {} - explicit format(string_ref const & v):object_ref(mk_cnstr(static_cast<unsigned>(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<format_kind>(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<format const &, options const &> 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 da0a6f9..caf60ed 100644 --- a/src/util/init_module.cpp +++ b/src/util/init_module.cpp
@@ -9,7 +9,6 @@ #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 @@ initialize_name(); initialize_name_generator(); initialize_options(); - initialize_format(); } void finalize_util_module() { - finalize_format(); finalize_options(); finalize_name_generator(); finalize_name();