From 7a033ac07ebe559b9e14504ffb38acd87db51891 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 24 Oct 2014 14:35:03 -0700 Subject: [PATCH] feat(frontends/lean): add 'print axioms' command, close #251 --- src/frontends/lean/builtin_cmds.cpp | 21 +++++++++++++++++++++ src/frontends/lean/tokens.cpp | 4 ++++ src/frontends/lean/tokens.h | 1 + tests/lean/print_ax1.lean | 3 +++ tests/lean/print_ax1.lean.expected.out | 1 + tests/lean/print_ax2.lean | 3 +++ tests/lean/print_ax2.lean.expected.out | 2 ++ 7 files changed, 35 insertions(+) create mode 100644 tests/lean/print_ax1.lean create mode 100644 tests/lean/print_ax1.lean.expected.out create mode 100644 tests/lean/print_ax2.lean create mode 100644 tests/lean/print_ax2.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 0133d66c0..e9c87d84a 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" +#include "kernel/inductive/inductive.h" #include "library/io_state_stream.h" #include "library/scoped_ext.h" #include "library/aliases.h" @@ -53,6 +54,23 @@ static void print_coercions(parser & p, optional const & C) { }); } +static void print_axioms(parser & p) { + bool has_axioms = false; + environment const & env = p.env(); + env.for_each_declaration([&](declaration const & d) { + name const & n = d.get_name(); + if (!d.is_definition() && + !inductive::is_inductive_decl(env, n) && + !inductive::is_elim_rule(env, n) && + !inductive::is_intro_rule(env, n)) { + p.regular_stream() << n << " : " << d.get_type() << endl; + has_axioms = true; + } + }); + if (!has_axioms) + p.regular_stream() << "no axioms" << endl; +} + environment print_cmd(parser & p) { if (p.curr() == scanner::token_kind::String) { p.regular_stream() << p.get_str_val() << endl; @@ -98,6 +116,9 @@ environment print_cmd(parser & p) { if (p.curr_is_identifier()) C = p.check_constant_next("invalid 'print coercions', constant expected"); print_coercions(p, C); + } else if (p.curr_is_token_or_id(get_axioms_tk())) { + p.next(); + print_axioms(p); } else { throw parser_error("invalid print command", p.pos()); } diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 914401575..dda113bf6 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -65,6 +65,7 @@ static name * g_end = nullptr; static name * g_definition = nullptr; static name * g_theorem = nullptr; static name * g_axiom = nullptr; +static name * g_axioms = nullptr; static name * g_variable = nullptr; static name * g_variables = nullptr; static name * g_opaque = nullptr; @@ -150,6 +151,7 @@ void initialize_tokens() { g_theorem = new name("theorem"); g_opaque = new name("opaque"); g_axiom = new name("axiom"); + g_axioms = new name("axioms"); g_variable = new name("variable"); g_variables = new name("variables"); g_instance = new name("[instance]"); @@ -197,6 +199,7 @@ void finalize_tokens() { delete g_theorem; delete g_opaque; delete g_axiom; + delete g_axioms; delete g_variables; delete g_variable; delete g_instance; @@ -318,6 +321,7 @@ name const & get_end_tk() { return *g_end; } name const & get_definition_tk() { return *g_definition; } name const & get_theorem_tk() { return *g_theorem; } name const & get_axiom_tk() { return *g_axiom; } +name const & get_axioms_tk() { return *g_axiom; } name const & get_variable_tk() { return *g_variable; } name const & get_variables_tk() { return *g_variables; } name const & get_opaque_tk() { return *g_opaque; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 8c5251745..13ee6a843 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -67,6 +67,7 @@ name const & get_end_tk(); name const & get_definition_tk(); name const & get_theorem_tk(); name const & get_axiom_tk(); +name const & get_axioms_tk(); name const & get_variable_tk(); name const & get_variables_tk(); name const & get_opaque_tk(); diff --git a/tests/lean/print_ax1.lean b/tests/lean/print_ax1.lean new file mode 100644 index 000000000..7e3deeadc --- /dev/null +++ b/tests/lean/print_ax1.lean @@ -0,0 +1,3 @@ +import data.nat.basic + +print axioms diff --git a/tests/lean/print_ax1.lean.expected.out b/tests/lean/print_ax1.lean.expected.out new file mode 100644 index 000000000..e62ea1048 --- /dev/null +++ b/tests/lean/print_ax1.lean.expected.out @@ -0,0 +1 @@ +no axioms diff --git a/tests/lean/print_ax2.lean b/tests/lean/print_ax2.lean new file mode 100644 index 000000000..e629bda5d --- /dev/null +++ b/tests/lean/print_ax2.lean @@ -0,0 +1,3 @@ +import logic.axioms.hilbert logic.axioms.funext + +print axioms diff --git a/tests/lean/print_ax2.lean.expected.out b/tests/lean/print_ax2.lean.expected.out new file mode 100644 index 000000000..199efe96c --- /dev/null +++ b/tests/lean/print_ax2.lean.expected.out @@ -0,0 +1,2 @@ +funext : ∀ {A : Type} {B : A → Type} {f g : Π (x : A), B x}, (∀ (x : A), f x = g x) → f = g +strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A), (∃ (x : A), P x) → P x }