From 3b7b268e403baa4837983783c19e48cfd381c068 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 May 2015 14:07:38 -0700 Subject: [PATCH] fix(frontends/lean/pp): fixes #634 trying again... --- src/frontends/lean/decl_cmds.cpp | 2 + src/frontends/lean/local_ref_info.cpp | 24 +++-- src/frontends/lean/local_ref_info.h | 4 +- src/frontends/lean/parser.cpp | 9 +- src/frontends/lean/pp.cpp | 134 ++++++++++++++++++++++---- src/frontends/lean/pp.h | 6 +- tests/lean/634.lean.expected.out | 6 +- tests/lean/634b.lean | 41 ++++++++ tests/lean/634b.lean.expected.out | 23 +++++ tests/lean/634c.lean | 38 ++++++++ tests/lean/634c.lean.expected.out | 22 +++++ 11 files changed, 267 insertions(+), 42 deletions(-) create mode 100644 tests/lean/634b.lean create mode 100644 tests/lean/634b.lean.expected.out create mode 100644 tests/lean/634c.lean create mode 100644 tests/lean/634c.lean.expected.out diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index a0391894a..b9af33442 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -41,6 +41,8 @@ namespace lean { static environment declare_universe(parser & p, environment env, name const & n, bool local) { if (local) { p.add_local_level(n, mk_param_univ(n), local); + } else if (in_section(env)) { + p.add_local_level(n, mk_param_univ(n), false); } else { name const & ns = get_namespace(env); name full_n = ns + n; diff --git a/src/frontends/lean/local_ref_info.cpp b/src/frontends/lean/local_ref_info.cpp index 87a61f737..daf56fcde 100644 --- a/src/frontends/lean/local_ref_info.cpp +++ b/src/frontends/lean/local_ref_info.cpp @@ -13,25 +13,23 @@ When we declare a definition in a section, we create an alias for it that fixes universe parameters. We have to store the number of parameters and universes that have been fixed to be able to correctly pretty print terms. */ - struct local_ref_entry { name m_name; - unsigned m_num_fix_univs; - unsigned m_num_fix_args; + expr m_ref; local_ref_entry() {} - local_ref_entry(name const & n, unsigned u, unsigned p): - m_name(n), m_num_fix_univs(u), m_num_fix_args(p) {} + local_ref_entry(name const & n, expr const & ref): + m_name(n), m_ref(ref) {} }; static name * g_local_ref_name = nullptr; static std::string * g_key = nullptr; struct local_ref_config { - typedef name_map> state; - typedef local_ref_entry entry; + typedef name_map state; + typedef local_ref_entry entry; static void add_entry(environment const &, io_state const &, state & s, entry const & e) { - s.insert(e.m_name, mk_pair(e.m_num_fix_univs, e.m_num_fix_args)); + s.insert(e.m_name, e.m_ref); } static name const & get_class_name() { return *g_local_ref_name; @@ -53,16 +51,16 @@ struct local_ref_config { template class scoped_ext; typedef scoped_ext local_ref_ext; -environment save_local_ref_info(environment const & env, name const & n, unsigned num_fix_univs, unsigned num_fix_args) { +environment save_local_ref_info(environment const & env, name const & n, expr const & ref) { bool persistent = false; - return local_ref_ext::add_entry(env, get_dummy_ios(), local_ref_entry(n, num_fix_univs, num_fix_args), persistent); + return local_ref_ext::add_entry(env, get_dummy_ios(), local_ref_entry(n, ref), persistent); } -optional> get_local_ref_info(environment const & env, name const & n) { +optional get_local_ref_info(environment const & env, name const & n) { if (auto r = local_ref_ext::get_state(env).find(n)) - return optional>(*r); + return some_expr(*r); else - return optional>(); + return none_expr(); } void initialize_local_ref_info() { diff --git a/src/frontends/lean/local_ref_info.h b/src/frontends/lean/local_ref_info.h index c7441c3e3..2866036b6 100644 --- a/src/frontends/lean/local_ref_info.h +++ b/src/frontends/lean/local_ref_info.h @@ -7,8 +7,8 @@ Author: Leonardo de Moura #pragma once namespace lean { -environment save_local_ref_info(environment const & env, name const & n, unsigned num_fix_univs, unsigned num_fix_args); -optional> get_local_ref_info(environment const & env, name const & n); +environment save_local_ref_info(environment const & env, name const & n, expr const & ref); +optional get_local_ref_info(environment const & env, name const & n); void initialize_local_ref_info(); void finalize_local_ref_info(); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 9bc741d33..8afffcaa8 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -510,10 +510,15 @@ environment parser::add_local_ref(environment const & env, name const & n, expr if (is_explicit(f)) f = get_explicit_arg(f); if (is_constant(f)) { - return save_local_ref_info(env, const_name(f), length(const_levels(f)), args.size()); + return save_local_ref_info(env, const_name(f), ref); + } else { + return env; } + } else if (is_constant(ref) && const_levels(ref)) { + return save_local_ref_info(env, const_name(ref), ref); + } else { + return env; } - return env; } void parser::add_parameter(name const & n, expr const & p) { diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 47c2550e1..7c5377eb0 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -365,8 +365,7 @@ auto pretty_fn::pp_coercion(expr const & e, unsigned bp, bool ignore_hide) -> re } } -auto pretty_fn::pp_child_core(expr const & e, unsigned bp, bool ignore_hide) -> result { - result r = pp(e, ignore_hide); +auto pretty_fn::add_paren_if_needed(result const & r, unsigned bp) -> result { if (r.rbp() < bp) { return result(paren(r.fmt())); } else { @@ -374,24 +373,110 @@ auto pretty_fn::pp_child_core(expr const & e, unsigned bp, bool ignore_hide) -> } } +auto pretty_fn::pp_child_core(expr const & e, unsigned bp, bool ignore_hide) -> result { + return add_paren_if_needed(pp(e, ignore_hide), bp); +} + +static expr consume_ref_annotations(expr const & e) { + if (is_explicit(e)) + return consume_ref_annotations(get_explicit_arg(e)); + else + return e; +} + +enum local_ref_kind { LocalRef, OverridenLocalRef, NotLocalRef }; + +static local_ref_kind check_local_ref(environment const & env, expr const & e, unsigned & num_ref_univ_params) { + expr const & rfn = get_app_fn(e); + if (!is_constant(rfn)) + return NotLocalRef; + auto ref = get_local_ref_info(env, const_name(rfn)); + if (!ref) + return NotLocalRef; + if (is_as_atomic(*ref)) + ref = get_as_atomic_arg(*ref); + buffer ref_args, e_args; + expr ref_fn = consume_ref_annotations(get_app_args(*ref, ref_args)); + get_app_args(e, e_args); + if (!is_constant(ref_fn) || e_args.size() != ref_args.size()) { + return NotLocalRef; + } + for (unsigned i = 0; i < e_args.size(); i++) { + expr e_arg = e_args[i]; + expr ref_arg = consume_ref_annotations(ref_args[i]); + if (!is_local(e_arg) || !is_local(ref_arg) || local_pp_name(e_arg) != local_pp_name(ref_arg)) + return OverridenLocalRef; + } + num_ref_univ_params = length(const_levels(ref_fn)); + buffer lvls; + to_buffer(const_levels(rfn), lvls); + if (lvls.size() < num_ref_univ_params) { + return NotLocalRef; + } + for (unsigned i = 0; i < num_ref_univ_params; i++) { + level const & l = lvls[i]; + if (!is_param(l)) { + return OverridenLocalRef; + } + for (unsigned j = 0; j < i; j++) + if (lvls[i] == lvls[j]) { + return OverridenLocalRef; + } + } + return LocalRef; +} + +static bool is_local_ref(environment const & env, expr const & e) { + unsigned num_ref_univ_params; + return check_local_ref(env, e, num_ref_univ_params) == LocalRef; +} + +auto pretty_fn::pp_overriden_local_ref(expr const & e) -> result { + buffer args; + expr const & fn = get_app_args(e, args); + result res_fn; + { + flet set1(m_full_names, true); + res_fn = pp_const(fn, some(0u)); + } + format fn_fmt = res_fn.fmt(); + if (const_name(fn).is_atomic()) + fn_fmt = compose(format("_root_."), fn_fmt); + if (m_implict && has_implicit_args(fn)) + fn_fmt = compose(*g_explicit_fmt, fn_fmt); + format r_fmt = fn_fmt; + expr curr_fn = fn; + for (unsigned i = 0; i < args.size(); i++) { + expr const & arg = args[i]; + if (m_implict || !is_implicit(curr_fn)) { + result res_arg = pp_child(arg, max_bp()); + r_fmt = group(compose(r_fmt, nest(m_indent, compose(line(), res_arg.fmt())))); + } + curr_fn = mk_app(curr_fn, arg); + } + return result(max_bp()-1, r_fmt); +} + +bool pretty_fn::ignore_local_ref(expr const & e) { + expr const & fn = get_app_fn(e); + return m_full_names && (!is_constant(fn) || !const_name(fn).is_atomic()); +} + // Return some result if \c e is of the form (c p_1 ... p_n) where // c is a constant, and p_i's are parameters fixed in a section. auto pretty_fn::pp_local_ref(expr const & e) -> optional { - if (m_full_names) + if (ignore_local_ref(e)) return optional(); - lean_assert(is_app(e)); - expr const & rfn = get_app_fn(e); - if (is_constant(rfn)) { - if (auto info = get_local_ref_info(m_env, const_name(rfn))) { - buffer args; - get_app_args(e, args); - if (args.size() == info->second) { - // TODO(Leo): must check if the arguments are really the fixed parameters. - return some(pp_const(rfn)); - } - } + unsigned num_ref_univ_params; + switch (check_local_ref(m_env, e, num_ref_univ_params)) { + case NotLocalRef: + return optional(); + case LocalRef: + return some(pp_const(get_app_fn(e), optional(num_ref_univ_params))); + case OverridenLocalRef: + return some(pp_overriden_local_ref(e)); } - return optional(); + lean_unreachable(); } auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> result { @@ -399,7 +484,7 @@ auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> resul return pp_abbreviation(e, *it, false, bp, ignore_hide); if (is_app(e)) { if (auto r = pp_local_ref(e)) - return *r; + return add_paren_if_needed(*r, bp); expr const & f = app_fn(e); if (auto it = is_abbreviated(f)) { return pp_abbreviation(e, *it, true, bp, ignore_hide); @@ -446,7 +531,14 @@ optional pretty_fn::is_abbreviated(expr const & e) const { return optional(); } -auto pretty_fn::pp_const(expr const & e) -> result { +auto pretty_fn::pp_const(expr const & e, optional const & num_ref_univ_params) -> result { + if (!num_ref_univ_params) { + if (auto r = pp_local_ref(e)) + return *r; + } + // Remark: if num_ref_univ_params is "some", then it contains the number of + // universe levels that are fixed in a section. That is, \c e corresponds to + // a constant in a section which has fixed levels. name n = const_name(e); if (!m_full_names) { if (auto it = is_aliased(n)) { @@ -474,11 +566,11 @@ auto pretty_fn::pp_const(expr const & e) -> result { unsigned first_idx = 0; buffer ls; to_buffer(const_levels(e), ls); - if (auto info = get_local_ref_info(m_env, n)) { - if (ls.size() <= info->first) + if (num_ref_univ_params) { + if (ls.size() <= *num_ref_univ_params) return result(format(n)); else - first_idx = info->first; + first_idx = *num_ref_univ_params; } format r = compose(format(n), format(".{")); bool first = true; @@ -547,7 +639,7 @@ auto pretty_fn::pp_app(expr const & e) -> result { bool ignore_hide = true; result res_fn = pp_child(fn, max_bp()-1, ignore_hide); format fn_fmt = res_fn.fmt(); - if (m_implict && !is_app(fn) && has_implicit_args(fn)) + if (m_implict && (!is_app(fn) || (!ignore_local_ref(fn) && is_local_ref(m_env, fn))) && has_implicit_args(fn)) fn_fmt = compose(*g_explicit_fmt, fn_fmt); result res_arg = pp_child(app_arg(e), max_bp()); return result(max_bp()-1, group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.fmt()))))); diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index 8e8cac130..cdeaecd5e 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -91,6 +91,10 @@ private: optional pp_notation(notation_entry const & entry, buffer> & args); optional pp_notation(expr const & e); + result add_paren_if_needed(result const & r, unsigned bp); + + result pp_overriden_local_ref(expr const & e); + bool ignore_local_ref(expr const & e); optional pp_local_ref(expr const & e); result pp_coercion_fn(expr const & e, unsigned sz, bool ignore_hide = false); @@ -99,7 +103,7 @@ private: result pp_child(expr const & e, unsigned bp, bool ignore_hide = false); result pp_var(expr const & e); result pp_sort(expr const & e); - result pp_const(expr const & e); + result pp_const(expr const & e, optional const & num_ref_univs = optional()); result pp_meta(expr const & e); result pp_local(expr const & e); result pp_app(expr const & e); diff --git a/tests/lean/634.lean.expected.out b/tests/lean/634.lean.expected.out index 99a07c0e0..22408b39e 100644 --- a/tests/lean/634.lean.expected.out +++ b/tests/lean/634.lean.expected.out @@ -1,5 +1,5 @@ -A n : Type₁ +@A n : Type₁ @foo.A X n : Type₁ @foo.A X n : Type₁ -A n : Type₁ -A n : Type₁ +@A n : Type₁ +@A n : Type₁ diff --git a/tests/lean/634b.lean b/tests/lean/634b.lean new file mode 100644 index 000000000..097699ca2 --- /dev/null +++ b/tests/lean/634b.lean @@ -0,0 +1,41 @@ +open nat +namespace foo +section + parameter (X : Type₁) + definition A {n : ℕ} : Type₁ := X + definition B : Type₁ := X + variable {n : ℕ} + check @A n + check foo.A nat + check foo.A (X × B) + check @foo.A (X × B) 10 + check @foo.A (@foo.B (@A n)) n + check @foo.A (@foo.B (@foo.A X n)) n + check @foo.A (@foo.B (@foo.A nat n)) n + + set_option pp.full_names true + check A + check foo.A nat + check @foo.A (X × B) 10 + check @foo.A (@foo.B (@foo.A X n)) n + check @foo.A (@foo.B (@foo.A nat n)) n + + set_option pp.full_names false + + set_option pp.implicit true + check @A n + check @foo.A nat 10 + check @foo.A X n + set_option pp.full_names true + check @foo.A X n + check @A n + + set_option pp.full_names false + check @foo.A X n + check @foo.A B n + check @foo.A (@foo.B (@A n)) n + check @foo.A (@foo.B (@foo.A X n)) n + check @foo.A (@foo.B (@foo.A nat n)) n + check @A n +end +end foo diff --git a/tests/lean/634b.lean.expected.out b/tests/lean/634b.lean.expected.out new file mode 100644 index 000000000..26bc0b02d --- /dev/null +++ b/tests/lean/634b.lean.expected.out @@ -0,0 +1,23 @@ +A : Type₁ +foo.A ℕ : Type₁ +foo.A (X × B) : Type₁ +foo.A (X × B) : Type₁ +foo.A (foo.B A) : Type₁ +foo.A (foo.B A) : Type₁ +foo.A (foo.B (foo.A ℕ)) : Type₁ +foo.A X : Type₁ +foo.A ℕ : Type₁ +foo.A (X × foo.B X) : Type₁ +foo.A (foo.B (foo.A X)) : Type₁ +foo.A (foo.B (foo.A ℕ)) : Type₁ +@A n : Type₁ +@foo.A ℕ 10 : Type₁ +@A n : Type₁ +@foo.A X n : Type₁ +@foo.A X n : Type₁ +@A n : Type₁ +@foo.A B n : Type₁ +@foo.A (foo.B (@A n)) n : Type₁ +@foo.A (foo.B (@A n)) n : Type₁ +@foo.A (foo.B (@foo.A ℕ n)) n : Type₁ +@A n : Type₁ diff --git a/tests/lean/634c.lean b/tests/lean/634c.lean new file mode 100644 index 000000000..40c6a6bc6 --- /dev/null +++ b/tests/lean/634c.lean @@ -0,0 +1,38 @@ +open nat +section + parameter (X : Type₁) + definition A {n : ℕ} : Type₁ := X + definition B : Type₁ := X + variable {n : ℕ} + check @A n + check _root_.A nat + check _root_.A (X × B) + check @_root_.A (X × B) 10 + check @_root_.A (_root_.B (@_root_.A X n)) n + check @_root_.A (@_root_.B (@_root_.A nat n)) n + + set_option pp.full_names true + check A + check _root_.A nat + check @_root_.A (X × B) 10 + check @_root_.A (@_root_.B (@_root_.A X n)) n + check @_root_.A (@_root_.B (@_root_.A nat n)) n + + set_option pp.full_names false + + set_option pp.implicit true + check @A n + check @_root_.A nat 10 + check @_root_.A X n + set_option pp.full_names true + check @_root_.A X n + check @_root_.A B n + + set_option pp.full_names false + check @_root_.A X n + check @_root_.A B n + check @_root_.A (@_root_.B (@A n)) n + check @_root_.A (@_root_.B (@_root_.A X n)) n + check @_root_.A (@_root_.B (@_root_.A nat n)) n + check @A n +end diff --git a/tests/lean/634c.lean.expected.out b/tests/lean/634c.lean.expected.out new file mode 100644 index 000000000..1bf0eee20 --- /dev/null +++ b/tests/lean/634c.lean.expected.out @@ -0,0 +1,22 @@ +A : Type₁ +_root_.A ℕ : Type₁ +_root_.A (X × B) : Type₁ +_root_.A (X × B) : Type₁ +_root_.A (_root_.B A) : Type₁ +_root_.A (_root_.B (_root_.A ℕ)) : Type₁ +A : Type₁ +_root_.A ℕ : Type₁ +_root_.A (X × B) : Type₁ +_root_.A (_root_.B A) : Type₁ +_root_.A (_root_.B (_root_.A ℕ)) : Type₁ +@A n : Type₁ +@_root_.A ℕ 10 : Type₁ +@A n : Type₁ +@A n : Type₁ +@_root_.A B n : Type₁ +@A n : Type₁ +@_root_.A B n : Type₁ +@_root_.A (_root_.B (@A n)) n : Type₁ +@_root_.A (_root_.B (@A n)) n : Type₁ +@_root_.A (_root_.B (@_root_.A ℕ n)) n : Type₁ +@A n : Type₁