diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 9d67de26c..676891af9 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -272,34 +272,34 @@ bool print_polymorphic(parser & p) { name id = p.check_id_next(""); // declarations try { - name c = p.to_constant(id, "", pos); - declaration const & d = env.get(c); - if (d.is_theorem()) { - print_constant(p, "theorem", d); - print_definition(p, c, pos); - return true; - } else if (d.is_axiom() || d.is_constant_assumption()) { - if (inductive::is_inductive_decl(env, c)) { - print_inductive(p, c, pos); - return true; - } else if (inductive::is_intro_rule(env, c)) { - return print_constant(p, "constructor", d); - } else if (inductive::is_elim_rule(env, c)) { - return print_constant(p, "eliminator", d); - } else if (is_quotient_decl(env, c)) { - return print_constant(p, "builtin-quotient-type-constant", d); - } else if (is_hits_decl(env, c)) { - return print_constant(p, "builtin-HIT-constant", d); - } else if (d.is_axiom()) { - return print_constant(p, "axiom", d); - } else if (d.is_constant_assumption()) { - return print_constant(p, "constant", d); + list cs = p.to_constants(id, "", pos); + for (name const & c : cs) { + declaration const & d = env.get(c); + if (d.is_theorem()) { + print_constant(p, "theorem", d); + print_definition(p, c, pos); + } else if (d.is_axiom() || d.is_constant_assumption()) { + if (inductive::is_inductive_decl(env, c)) { + print_inductive(p, c, pos); + } else if (inductive::is_intro_rule(env, c)) { + print_constant(p, "constructor", d); + } else if (inductive::is_elim_rule(env, c)) { + print_constant(p, "eliminator", d); + } else if (is_quotient_decl(env, c)) { + print_constant(p, "builtin-quotient-type-constant", d); + } else if (is_hits_decl(env, c)) { + print_constant(p, "builtin-HIT-constant", d); + } else if (d.is_axiom()) { + print_constant(p, "axiom", d); + } else { + print_constant(p, "constant", d); + } + } else if (d.is_definition()) { + print_constant(p, "definition", d); + print_definition(p, c, pos); } - } else if (d.is_definition()) { - print_constant(p, "definition", d); - print_definition(p, c, pos); - return true; } + return true; } catch (exception & ex) {} // variables and parameters @@ -371,8 +371,20 @@ environment print_cmd(parser & p) { } else if (p.curr_is_token_or_id(get_definition_tk())) { p.next(); auto pos = p.pos(); - name c = p.check_constant_next("invalid 'print definition', constant expected"); - print_definition(p, c, pos); + name id = p.check_id_next("invalid 'print definition', constant expected"); + list cs = p.to_constants(id, "invalid 'print definition', constant expected", pos); + for (name const & c : cs) { + declaration const & d = p.env().get(c); + if (d.is_theorem()) { + print_constant(p, "theorem", d); + print_definition(p, c, pos); + } else if (d.is_definition()) { + print_constant(p, "definition", d); + print_definition(p, c, pos); + } else { + throw parser_error(sstream() << "invalid 'print definition', '" << c << "' is not a definition", pos); + } + } } else if (p.curr_is_token_or_id(get_instances_tk())) { p.next(); name c = p.check_constant_next("invalid 'print instances', constant expected"); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 8a8657d08..56e222404 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1230,22 +1230,30 @@ expr parser::id_to_expr(name const & id, pos_info const & p) { return *r; } -name parser::to_constant(name const & id, char const * msg, pos_info const & p) { +list parser::to_constants(name const & id, char const * msg, pos_info const & p) { expr e = id_to_expr(id, p); - if (in_section(m_env) && is_as_atomic(e)) { - e = get_app_fn(get_as_atomic_arg(e)); - if (is_explicit(e)) - e = get_explicit_arg(e); - } - while (is_choice(e)) - e = get_choice(e, 0); + buffer rs; + std::function visit = [&](expr const & e) { + if (in_section(m_env) && is_as_atomic(e)) { + visit(get_app_fn(get_as_atomic_arg(e))); + } else if (is_explicit(e)) { + visit(get_explicit_arg(e)); + } else if (is_choice(e)) { + for (unsigned i = 0; i < get_num_choices(e); i++) + visit(get_choice(e, i)); + } else if (is_constant(e)) { + rs.push_back(const_name(e)); + } else { + throw parser_error(msg, p); + } + }; + visit(e); + return to_list(rs); +} - if (is_constant(e)) { - return const_name(e); - } else { - throw parser_error(msg, p); - } +name parser::to_constant(name const & id, char const * msg, pos_info const & p) { + return head(to_constants(id, msg, p)); } name parser::check_constant_next(char const * msg) { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 05dcf83d7..b904fc68c 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -345,6 +345,7 @@ public: /** \brief Check if the current token is an atomic identifier, if it is, return it and move to next token, otherwise throw an exception. */ name check_atomic_id_next(char const * msg); + list to_constants(name const & id, char const * msg, pos_info const & p); name to_constant(name const & id, char const * msg, pos_info const & p); /** \brief Check if the current token is a constant, if it is, return it and move to next token, otherwise throw an exception. */ name check_constant_next(char const * msg); diff --git a/tests/lean/608.hlean b/tests/lean/608.hlean new file mode 100644 index 000000000..6c790b37c --- /dev/null +++ b/tests/lean/608.hlean @@ -0,0 +1,8 @@ +import algebra.category.precategory +open function category + +print id + +print "-----------" + +print definition id diff --git a/tests/lean/608.hlean.expected.out b/tests/lean/608.hlean.expected.out new file mode 100644 index 000000000..704c6fbad --- /dev/null +++ b/tests/lean/608.hlean.expected.out @@ -0,0 +1,9 @@ +definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a +λ (ob : Type) (C : precategory ob) (a : ob), ID a +definition function.id [reducible] : Π {A : Type}, A → A +is_typeof +----------- +definition category.id [reducible] : Π {ob : Type} [C : precategory ob] {a : ob}, hom a a +λ (ob : Type) (C : precategory ob) (a : ob), ID a +definition function.id [reducible] : Π {A : Type}, A → A +is_typeof diff --git a/tests/lean/abbrev1.lean.expected.out b/tests/lean/abbrev1.lean.expected.out index 7b14670e6..ea7e7e818 100644 --- a/tests/lean/abbrev1.lean.expected.out +++ b/tests/lean/abbrev1.lean.expected.out @@ -1,3 +1,6 @@ +definition tst : ℕ (λ (a : Type₁), 2 + 3) ℕ +definition tst : ℕ foo ℕ +definition tst1 : num is_typeof num 10 diff --git a/tests/lean/abbrev2.lean.expected.out b/tests/lean/abbrev2.lean.expected.out index b19ad9cf8..fe6911553 100644 --- a/tests/lean/abbrev2.lean.expected.out +++ b/tests/lean/abbrev2.lean.expected.out @@ -1,9 +1,16 @@ +definition bla.tst : ℕ foo +definition bla.tst : ℕ 10 + 1 abbrev2.lean:12:6: error: unknown identifier 'bla.foo' abbrev2.lean:14:6: error: unknown identifier 'foo' +definition bla.tst : ℕ 10 + 1 +definition bla2.tst2 : ℕ foo2 +definition bla2.tst2 : ℕ 1 +definition bla2.tst2 : ℕ foo2 +definition bla2.tst2 : ℕ foo2