diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index 0351c5887..799fb969a 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -143,13 +143,34 @@ struct lean_extension : public environment::extension { /** \brief Two operator (aka notation) denotations are compatible - iff one of the following holds: - - 1) Both do not have implicit arguments - - 2) Both have implicit arguments, and the implicit arguments + iff after ignoring all implicit arguments in the prefix and + explicit arguments in the suffix, the remaining implicit arguments occur in the same positions. + Let us denote implicit arguments with a '_' and explicit with a '*'. + Then a denotation can be associated with a pattern containing one or more + '_' and '*'. + Two denotations are compatible, if we have the same pattern after + removed the '_' from the prefix and '*' from the suffix. + + Here is an example of compatible denotations + f : Int -> Int -> Int Pattern * * + g : Pi {A : Type}, A -> A -> A Pattern _ * * + h : Pi {A B : Type}, A -> B -> A Pattern _ _ * * + They are compatible, because after we remove the _ from the prefix, and * from the suffix, + all of them reduce to the empty sequence + + Here is another example of compatible denotations: + f : Pi {A : Type} (a : A) {B : Type} (b : B), A Pattern _ * _ * + g : Pi (i : Int) {T : Type} (x : T), T Pattern * _ * + They are compatible, because after we remove the _ from the prefix, and * from the suffix, + we get the same sequence: * _ + + The following two are not compatible + f : Pi {A : Type} (a : A) {B : Type} (b : B), A Pattern _ * _ * + g : Pi {A B : Type} (a : A) (b : B), A Pattern _ _ * * + + TODO(Leo): not implemented yet */ bool compatible_denotation(expr const & d1, expr const & d2) { return get_implicit_arguments(d1) == get_implicit_arguments(d2); @@ -243,9 +264,13 @@ struct lean_extension : public environment::extension { while (is_pi(it)) { num_args++; it = abst_body(it); } if (sz > num_args) throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', object has only " << num_args << " arguments, but trying to mark " << sz << " arguments"); + // remove explicit suffix + while (sz > 0 && !implicit[sz - 1]) sz--; + if (sz == 0) + throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', all arguments are explicit"); std::vector v(implicit, implicit+sz); m_implicit_table[n] = mk_pair(v, explicit_version); - expr body = mk_explicit_definition_body(type, n, 0, sz); + expr body = mk_explicit_definition_body(type, n, 0, num_args); if (obj.is_axiom() || obj.is_theorem()) { env.add_theorem(explicit_version, type, body); } else { @@ -445,6 +470,18 @@ operator_info frontend::find_led(name const & n) const { void frontend::mark_implicit_arguments(name const & n, unsigned sz, bool const * implicit) { to_ext(m_env).mark_implicit_arguments(n, sz, implicit, m_env); } +void frontend::mark_implicit_arguments(name const & n, unsigned prefix_sz) { + buffer implicit; implicit.resize(prefix_sz, true); + mark_implicit_arguments(n, implicit.size(), implicit.data()); +} +void frontend::mark_implicit_arguments(expr const & n, unsigned prefix_sz) { + if (is_constant(n)) { + mark_implicit_arguments(const_name(n), prefix_sz); + } else { + lean_assert(is_value(n)); + mark_implicit_arguments(to_value(n).get_name(), prefix_sz); + } +} void frontend::mark_implicit_arguments(name const & n, std::initializer_list const & l) { mark_implicit_arguments(n, l.size(), l.begin()); } diff --git a/src/frontends/lean/frontend.h b/src/frontends/lean/frontend.h index 32ece54fc..4c3765ef0 100644 --- a/src/frontends/lean/frontend.h +++ b/src/frontends/lean/frontend.h @@ -120,6 +120,11 @@ public: void mark_implicit_arguments(name const & n, unsigned sz, bool const * mask); void mark_implicit_arguments(name const & n, std::initializer_list const & l); void mark_implicit_arguments(expr const & n, std::initializer_list const & l); + /** + \brief Syntax sugar for mark_implicit_arguments(n, {true, ..., true}), with prefix_sz true's. + */ + void mark_implicit_arguments(name const & n, unsigned prefix_sz); + void mark_implicit_arguments(expr const & n, unsigned prefix_sz); /** \brief Return true iff \c n has implicit arguments */ bool has_implicit_arguments(name const & n) const; /** \brief Return the position of the arguments that are implicit. */ diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp index a238f90db..3041414ed 100644 --- a/src/frontends/lean/notation.cpp +++ b/src/frontends/lean/notation.cpp @@ -23,8 +23,8 @@ void init_builtin_notation(frontend & f) { if (!f.get_environment().mark_builtin_imported("lean_notation")) return; f.add_infix("=", 50, mk_homo_eq_fn()); - f.mark_implicit_arguments(mk_homo_eq_fn(), {true, false, false}); - f.mark_implicit_arguments(mk_if_fn(), {true, false, false, false}); + f.mark_implicit_arguments(mk_homo_eq_fn(), 1); + f.mark_implicit_arguments(mk_if_fn(), 1); f.add_prefix("\u00ac", 40, mk_not_fn()); // "¬" f.add_infixr("&&", 35, mk_and_fn()); // "&&" @@ -83,41 +83,41 @@ void init_builtin_notation(frontend & f) { f.add_coercion(mk_nat_to_real_fn()); // implicit arguments for builtin axioms - f.mark_implicit_arguments(mk_cast_fn(), {true, true, false, false}); - f.mark_implicit_arguments(mk_mp_fn(), {true, true, false, false}); - f.mark_implicit_arguments(mk_discharge_fn(), {true, true, false}); - f.mark_implicit_arguments(mk_refl_fn(), {true, false}); - f.mark_implicit_arguments(mk_subst_fn(), {true, true, true, true, false, false}); + f.mark_implicit_arguments(mk_cast_fn(), 2); + f.mark_implicit_arguments(mk_mp_fn(), 2); + f.mark_implicit_arguments(mk_discharge_fn(), 2); + f.mark_implicit_arguments(mk_refl_fn(), 1); + f.mark_implicit_arguments(mk_subst_fn(), 4); add_alias(f, "Subst", "SubstP"); - f.mark_implicit_arguments("SubstP", {true, true, true, false, false, false}); - f.mark_implicit_arguments(mk_trans_ext_fn(), {true, true, true, true, true, true, false, false}); - f.mark_implicit_arguments(mk_eta_fn(), {true, true, false}); - f.mark_implicit_arguments(mk_abst_fn(), {true, true, true, true, false}); - f.mark_implicit_arguments(mk_imp_antisym_fn(), {true, true, false, false}); - f.mark_implicit_arguments(mk_dom_inj_fn(), {true, true, true, true, false}); - f.mark_implicit_arguments(mk_ran_inj_fn(), {true, true, true, true, false, false}); + f.mark_implicit_arguments("SubstP", 3); + f.mark_implicit_arguments(mk_trans_ext_fn(), 6); + f.mark_implicit_arguments(mk_eta_fn(), 2); + f.mark_implicit_arguments(mk_abst_fn(), 4); + f.mark_implicit_arguments(mk_imp_antisym_fn(), 2); + f.mark_implicit_arguments(mk_dom_inj_fn(), 4); + f.mark_implicit_arguments(mk_ran_inj_fn(), 4); // implicit arguments for basic theorems - f.mark_implicit_arguments(mk_absurd_fn(), {true, false, false}); - f.mark_implicit_arguments(mk_double_neg_elim_fn(), {true, true, false}); - f.mark_implicit_arguments(mk_mt_fn(), {true, true, false, false}); - f.mark_implicit_arguments(mk_contrapos_fn(), {true, true, false}); - f.mark_implicit_arguments(mk_eq_mp_fn(), {true, true, false, false}); - f.mark_implicit_arguments(mk_not_imp1_fn(), {true, true, false}); - f.mark_implicit_arguments(mk_not_imp2_fn(), {true, true, false}); - f.mark_implicit_arguments(mk_conj_fn(), {true, true, false, false}); - f.mark_implicit_arguments(mk_conjunct1_fn(), {true, true, false}); - f.mark_implicit_arguments(mk_conjunct2_fn(), {true, true, false}); - f.mark_implicit_arguments(mk_disj1_fn(), {true, false, false}); - f.mark_implicit_arguments(mk_disj2_fn(), {true, false, false}); - f.mark_implicit_arguments(mk_disj_cases_fn(), {true, true, true, false, false, false}); - f.mark_implicit_arguments(mk_symm_fn(), {true, true, true, false}); - f.mark_implicit_arguments(mk_trans_fn(), {true, true, true, true, false, false}); - f.mark_implicit_arguments(mk_eqt_elim_fn(), {true, false}); - f.mark_implicit_arguments(mk_eqt_intro_fn(), {true, false}); - f.mark_implicit_arguments(mk_congr1_fn(), {true, true, true, true, false, false}); - f.mark_implicit_arguments(mk_congr2_fn(), {true, true, true, true, false, false}); - f.mark_implicit_arguments(mk_congr_fn(), {true, true, true, true, true, true, false, false}); - f.mark_implicit_arguments(mk_forall_elim_fn(), {true, true, false, false}); + f.mark_implicit_arguments(mk_absurd_fn(), 1); + f.mark_implicit_arguments(mk_double_neg_elim_fn(), 2); + f.mark_implicit_arguments(mk_mt_fn(), 2); + f.mark_implicit_arguments(mk_contrapos_fn(), 2); + f.mark_implicit_arguments(mk_eq_mp_fn(), 2); + f.mark_implicit_arguments(mk_not_imp1_fn(), 2); + f.mark_implicit_arguments(mk_not_imp2_fn(), 2); + f.mark_implicit_arguments(mk_conj_fn(), 2); + f.mark_implicit_arguments(mk_conjunct1_fn(), 2); + f.mark_implicit_arguments(mk_conjunct2_fn(), 2); + f.mark_implicit_arguments(mk_disj1_fn(), 1); + f.mark_implicit_arguments(mk_disj2_fn(), 1); + f.mark_implicit_arguments(mk_disj_cases_fn(), 3); + f.mark_implicit_arguments(mk_symm_fn(), 3); + f.mark_implicit_arguments(mk_trans_fn(), 4); + f.mark_implicit_arguments(mk_eqt_elim_fn(), 1); + f.mark_implicit_arguments(mk_eqt_intro_fn(), 1); + f.mark_implicit_arguments(mk_congr1_fn(), 4); + f.mark_implicit_arguments(mk_congr2_fn(), 4); + f.mark_implicit_arguments(mk_congr_fn(), 6); + f.mark_implicit_arguments(mk_forall_elim_fn(), 2); } } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 14021f45f..1fb7785b9 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -627,6 +627,8 @@ class parser::imp { i++; } } + for (; i < num_args; i++) + new_args.push_back(args[i]); } else { new_args.append(num_args, args); } @@ -765,11 +767,7 @@ class parser::imp { pos_info p = pos(); expr f = (k == object_kind::Builtin) ? obj->get_value() : mk_constant(obj->get_name()); args.push_back(save(f, p)); - // We parse the arguments until we find the last implicit argument. - auto last_imp = std::find(imp_args.rbegin(), imp_args.rend(), true); - lean_assert(last_imp != imp_args.rend()); // it must contain an implicit argument - unsigned num = static_cast(imp_args.rend() - last_imp); - for (unsigned i = 0; i < num; i++) { + for (unsigned i = 0; i < imp_args.size(); i++) { if (imp_args[i]) { args.push_back(save(mk_placeholder(), pos())); } else { diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 63647cfa7..ce49fa2f3 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -525,10 +525,7 @@ class pp_fn { if (has_implicit_arguments(owner, f)) { name const & n = is_constant(f) ? const_name(f) : to_value(f).get_name(); m_implicit_args = &(get_implicit_arguments(env, n)); - auto last_imp = std::find(m_implicit_args->rbegin(), m_implicit_args->rend(), true); - lean_assert(last_imp != m_implicit_args->rend()); // it must contain an implicit argument - unsigned num = static_cast(m_implicit_args->rend() - last_imp); - if (show_implicit || num_args(e) - 1 < num) { + if (show_implicit || num_args(e) - 1 < m_implicit_args->size()) { // we are showing implicit arguments, thus we do // not need the bit-mask for implicit arguments m_implicit_args = nullptr; @@ -796,7 +793,7 @@ class pp_fn { } bool is_implicit(std::vector const * implicit_args, unsigned arg_pos) { - return implicit_args && (*implicit_args)[arg_pos]; + return implicit_args && arg_pos < implicit_args->size() && (*implicit_args)[arg_pos]; } /** diff --git a/src/tests/frontends/lean/frontend.cpp b/src/tests/frontends/lean/frontend.cpp index e9ad1bdb2..b079a4cd6 100644 --- a/src/tests/frontends/lean/frontend.cpp +++ b/src/tests/frontends/lean/frontend.cpp @@ -174,7 +174,7 @@ static void tst11() { name gexp = f.get_explicit_version("g"); lean_assert(f.find_object(gexp)); lean_assert(f.find_object("g")->get_type() == f.find_object(gexp)->get_type()); - lean_assert(f.get_implicit_arguments("g") == std::vector({true, false, false})); + lean_assert(f.get_implicit_arguments("g") == std::vector({true})); // the trailing "false" marks are removed try { f.mark_implicit_arguments("g", {true, false, false}); lean_unreachable(); diff --git a/tests/lean/implicit3.lean b/tests/lean/implicit3.lean new file mode 100644 index 000000000..5d527facc --- /dev/null +++ b/tests/lean/implicit3.lean @@ -0,0 +1,9 @@ +Show 10 = 20 +Variable f : Int -> Int -> Int +Variable g : Int -> Int -> Int -> Int +Notation 10 _ ++ _ : f +Notation 10 _ ++ _ : g +Set pp::implicit true +Set pp::notation false +Show (10 ++ 20) +Show (10 ++ 20) 10 diff --git a/tests/lean/implicit3.lean.expected.out b/tests/lean/implicit3.lean.expected.out new file mode 100644 index 000000000..0e4508787 --- /dev/null +++ b/tests/lean/implicit3.lean.expected.out @@ -0,0 +1,9 @@ + Set: pp::colors + Set: pp::unicode +10 = 20 + Assumed: f + Assumed: g + Set: lean::pp::implicit + Set: lean::pp::notation +f 10 20 +g 10 20 10