max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove old pretty printer

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-15 12:03:27 +02:00
parent 38c79298ed
commit b0df2be65c
4 changed files with 18 additions and 1928 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/PrettyPrinter.lean
View file

@ -31,6 +31,10 @@ Meta.withLCtx lctx #[] $ do
stx ← delab currNamespace openDecls e;
liftM $ ppTerm stx
@[export lean_pp_expr]
def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
Prod.fst <$> ((ppExpr Name.anonymous [] e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts } { env := env }
def ppCommand (stx : Syntax) : CoreM Format :=
parenthesizeCommand stx >>= formatCommand

1791
src/frontends/lean/pp.cpp
View file

File diff suppressed because it is too large Load diff

147
src/frontends/lean/pp.h
View file

@ -19,153 +19,6 @@ Author: Leonardo de Moura
#include "frontends/lean/token_table.h"
namespace lean {
class notation_entry;
class pretty_fn {
public:
static unsigned max_bp() { return get_max_prec(); }
static unsigned inf_bp() { return std::numeric_limits<unsigned>::max(); }
/** \brief A pretty-printed format together with its left- and right-binding power
*
* The lbp is the binding power of its leftmost token. The invariant is that
* for `bp < m_rbp`, `parse_expr(m_fmt, bp) == parse_expr(m_fmt, 0)`, i.e. the whole input is parsed.
*
* The rbp is (roughly) the binding power of its trailing parse_expr call, if any. The invariant is that
* appending a token with binding power >= rbp should still parse no more than m_fmt.
*/
class result {
unsigned m_lbp;
unsigned m_rbp;
format m_fmt;
public:
result():m_lbp(max_bp()), m_rbp(max_bp()) {}
result(format const & fmt):m_lbp(inf_bp()), m_rbp(inf_bp()), m_fmt(fmt) {}
result(unsigned rbp, format const & fmt):m_lbp(max_bp()), m_rbp(rbp), m_fmt(fmt) {}
result(unsigned lbp, unsigned rbp, format const & fmt):m_lbp(lbp), m_rbp(rbp), m_fmt(fmt) {}
unsigned lbp() const { return m_lbp; }
unsigned rbp() const { return m_rbp; }
format const & fmt() const { return m_fmt; }
};
private:
environment m_env;
abstract_type_context & m_ctx;
token_table const & m_token_table;
unsigned m_num_steps;
unsigned m_depth;
name m_meta_prefix;
unsigned m_next_meta_idx;
name_map<name> m_purify_meta_table;
name_set m_purify_used_metas;
name_map<name> m_purify_local_table;
name_set m_purify_used_locals;
// cached configuration
options m_options;
unsigned m_indent;
unsigned m_max_depth;
unsigned m_max_steps;
bool m_implict; //!< if true show implicit arguments
bool m_proofs; //!< if true show proof terms
bool m_unicode; //!< if true use unicode chars
bool m_coercion; //!< if true show coercions
bool m_num_nat_coe; //!< true when !m_coercion && env has coercion from num -> nat
bool m_notation;
bool m_universes;
bool m_full_names;
bool m_private_names;
bool m_purify_metavars;
bool m_purify_locals;
bool m_locals_full_names;
bool m_beta;
bool m_numerals;
bool m_strings;
bool m_hide_full_terms;
bool m_hide_comp_irrel;
bool m_preterm;
bool m_binder_types;
bool m_delayed_abstraction;
bool m_structure_instances;
bool m_structure_instances_qualifier;
bool m_structure_projections;
bool m_annotations;
bool m_compact_let;
name mk_metavar_name(name const & m, optional<name> const & prefix = optional<name>());
name mk_metavar_name(name const & m, name const & prefix) {
return mk_metavar_name(m, optional<name>(prefix));
}
name mk_local_name(name const & n, name const & suggested);
level purify(level const & l);
expr purify(expr const & e);
bool is_implicit(expr const & f);
bool is_default_arg_app(expr const & e);
bool is_prop(expr const & e);
bool has_implicit_args(expr const & f);
optional<name> is_aliased(name const & n) const;
format escape(name const & n);
format pp_child(level const & l);
format pp_max(level l);
format pp_meta(level const & l);
format pp_level(level const & l);
format pp_binder(expr const & local);
format pp_binder_block(buffer<name> const & names, expr const & type, binder_info bi);
format pp_binders(buffer<expr> const & locals);
bool match(level const & p, level const & l);
bool match(expr const & p, expr const & e, buffer<optional<expr>> & args);
/** \brief pretty-print e parsed with rbp, terminated by a token with lbp */
result pp_notation_child(expr const & e, unsigned rbp, unsigned lbp);
optional<result> pp_notation(notation_entry const & entry, buffer<optional<expr>> & args);
optional<result> pp_notation(expr const & e);
result add_paren_if_needed(result const & r, unsigned bp);
std::pair<bool, token_table const *> needs_space_sep(token_table const * t, std::string const &s1, std::string const &s2) const;
result pp_hide_coercion(expr const & e, unsigned bp, bool ignore_hide = false);
result pp_hide_coercion_fn(expr const & e, unsigned bp, bool ignore_hide = false);
result pp_child_core(expr const & e, unsigned bp, bool ignore_hide = false);
result pp_child(expr const & e, unsigned bp, bool ignore_hide = false);
result pp_subtype(expr const & e);
result pp_sep(expr const & e);
result pp_set_of(expr const & e);
result pp_explicit_collection(buffer<expr> const & elems);
result pp_var(expr const & e);
result pp_sort(expr const & e);
result pp_const(expr const & e, optional<unsigned> const & num_ref_univs = optional<unsigned>());
result pp_meta(expr const & e);
result pp_fvar(expr const & e);
result pp_local(expr const & e);
result pp_app(expr const & e);
result pp_lambda(expr const & e);
result pp_structure_instance(expr const & e);
bool is_field_notation_candidate(expr const & e);
result pp_field_notation(expr const & e);
result pp_pi(expr const & e);
result pp_have(expr const & e);
result pp_show(expr const & e);
format pp_equation(expr const & e);
optional<result> pp_equations(expr const & e);
result pp_explicit(expr const & e);
result pp_delayed_abstraction(expr const & e);
result pp_let(expr e);
result pp_proj(expr const & e);
result pp_mdata(expr const & e);
result pp_num(mpz const & n, unsigned bp);
result pp_prod(expr const & e);
result pp_lit(expr const & e);
void set_options_core(options const & o);
expr infer_type(expr const & e);
public:
pretty_fn(environment const & env, options const & o, abstract_type_context & ctx);
result pp(expr const & e, bool ignore_hide = false);
void set_options(options const & o);
options const & get_options() const { return m_options; }
format operator()(expr const & e);
};
formatter_factory mk_pretty_formatter_factory();
void initialize_pp();
void finalize_pp();

4
tests/lean/envExtensionSealed.lean.expected.out
View file

@ -1,5 +1,5 @@
2
envExtensionSealed.lean:13:7: error: invalid structure notation source, not a structure
privateExt
Lean.privateExt
which has type
EnvExtensionInterfaceImp.ext Nat
Lean.EnvExtensionInterface.ext Lean.EnvExtensionInterfaceImp Nat