diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index b752de5ff..b9ccf7fa8 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -22,6 +22,7 @@ Author: Leonardo de Moura #include "library/protected.h" #include "library/locals.h" #include "library/coercion.h" +#include "library/constants.h" #include "library/reducible.h" #include "library/normalize.h" #include "library/print.h" @@ -1139,12 +1140,33 @@ static environment relevant_thms_cmd(parser & p) { return env; } +static void check_expr_and_print(parser & p, expr const & e) { + environment const & env = p.env(); + type_checker tc(env); + expr t = tc.check_ignore_undefined_universes(e).first; + p.regular_stream() << e << " : " << t << "\n"; +} + static environment app_builder_cmd(parser & p) { environment const & env = p.env(); auto pos = p.pos(); app_builder b(env); name c = p.check_constant_next("invalid #app_builder command, constant expected"); - p.check_token_next(get_lparen_tk(), "invalid #app_builder command, '(' expected"); + bool has_mask = false; + buffer mask; + if (p.curr_is_token(get_lparen_tk())) { + p.next(); + has_mask = true; + while (true) { + name flag = p.check_constant_next("invalid #app_builder command, constant (true, false) expected"); + mask.push_back(flag == get_true_name()); + if (!p.curr_is_token(get_comma_tk())) + break; + p.next(); + } + p.check_token_next(get_rparen_tk(), "invalid #app_builder command, ')' expected"); + } + buffer args; while (true) { expr e; level_param_names ls; @@ -1154,45 +1176,103 @@ static environment app_builder_cmd(parser & p) { break; p.next(); } - p.check_token_next(get_rparen_tk(), "invalid #app_builder command, ')' expected"); - if (auto r = b.mk_app(c, args.size(), args.data())) { - type_checker tc(env); - expr t = tc.check_ignore_undefined_universes(*r).first; - p.regular_stream() << *r << " : " << t << "\n"; + + if (has_mask && args.size() > mask.size()) + throw parser_error(sstream() << "invalid #app_builder command, too many arguments", pos); + + optional r; + if (has_mask) + r = b.mk_app(c, mask.size(), mask.data(), args.data()); + else + r = b.mk_app(c, args.size(), args.data()); + + if (r) { + check_expr_and_print(p, *r); } else { throw parser_error(sstream() << "failed to build application for '" << c << "'", pos); } + + return env; +} + +static environment refl_cmd(parser & p) { + environment const & env = p.env(); + auto pos = p.pos(); + app_builder b(env); + name relname = p.check_constant_next("invalid #refl command, constant expected"); + expr e; level_param_names ls; + std::tie(e, ls) = parse_local_expr(p); + if (auto r = b.mk_refl(relname, e)) { + check_expr_and_print(p, *r); + } else { + throw parser_error(sstream() << "failed to build refl proof", pos); + } + return env; +} + +static environment symm_cmd(parser & p) { + environment const & env = p.env(); + auto pos = p.pos(); + app_builder b(env); + name relname = p.check_constant_next("invalid #symm command, constant expected"); + expr e; level_param_names ls; + std::tie(e, ls) = parse_local_expr(p); + if (auto r = b.mk_symm(relname, e)) { + check_expr_and_print(p, *r); + } else { + throw parser_error(sstream() << "failed to build symm proof", pos); + } + return env; +} + +static environment trans_cmd(parser & p) { + environment const & env = p.env(); + auto pos = p.pos(); + app_builder b(env); + name relname = p.check_constant_next("invalid #trans command, constant expected"); + expr H1, H2; level_param_names ls; + std::tie(H1, ls) = parse_local_expr(p); + p.check_token_next(get_comma_tk(), "invalid #trans command, ',' expected"); + std::tie(H2, ls) = parse_local_expr(p); + if (auto r = b.mk_trans(relname, H1, H2)) { + check_expr_and_print(p, *r); + } else { + throw parser_error(sstream() << "failed to build trans proof", pos); + } return env; } void init_cmd_table(cmd_table & r) { - add_cmd(r, cmd_info("open", "create aliases for declarations, and use objects defined in other namespaces", + add_cmd(r, cmd_info("open", "create aliases for declarations, and use objects defined in other namespaces", open_cmd)); - add_cmd(r, cmd_info("export", "create abbreviations for declarations, " + add_cmd(r, cmd_info("export", "create abbreviations for declarations, " "and export objects defined in other namespaces", export_cmd)); - add_cmd(r, cmd_info("override", "override notation declarations using the ones defined in the given namespace", + add_cmd(r, cmd_info("override", "override notation declarations using the ones defined in the given namespace", override_cmd)); - add_cmd(r, cmd_info("set_option", "set configuration option", set_option_cmd)); - add_cmd(r, cmd_info("exit", "exit", exit_cmd)); - add_cmd(r, cmd_info("print", "print a string", print_cmd)); - add_cmd(r, cmd_info("section", "open a new section", section_cmd)); - add_cmd(r, cmd_info("namespace", "open a new namespace", namespace_cmd)); - add_cmd(r, cmd_info("end", "close the current namespace/section", end_scoped_cmd)); - add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd)); - add_cmd(r, cmd_info("eval", "evaluate given expression", eval_cmd)); - add_cmd(r, cmd_info("find_decl", "find definitions and/or theorems", find_cmd)); - add_cmd(r, cmd_info("local", "define local attributes or notation", local_cmd)); - add_cmd(r, cmd_info("help", "brief description of available commands and options", help_cmd)); - add_cmd(r, cmd_info("init_quotient", "initialize quotient type computational rules", init_quotient_cmd)); - add_cmd(r, cmd_info("init_hits", "initialize builtin HITs", init_hits_cmd)); - add_cmd(r, cmd_info("#erase_cache", "erase cached definition (for debugging purposes)", erase_cache_cmd)); - add_cmd(r, cmd_info("#projections", "generate projections for inductive datatype (for debugging purposes)", projections_cmd)); - add_cmd(r, cmd_info("#telescope_eq", "(for debugging purposes)", telescope_eq_cmd)); - add_cmd(r, cmd_info("#app_builder", "(for debugging purposes)", app_builder_cmd)); - add_cmd(r, cmd_info("#compile", "(for debugging purposes)", compile_cmd)); - add_cmd(r, cmd_info("#accessible", "(for debugging purposes) display number of accessible declarations for blast tactic", accessible_cmd)); - add_cmd(r, cmd_info("#decl_stats", "(for debugging purposes) display declaration statistics", decl_stats_cmd)); - add_cmd(r, cmd_info("#relevant_thms", "(for debugging purposes) select relevant theorems using Meng&Paulson heuristic", relevant_thms_cmd)); + add_cmd(r, cmd_info("set_option", "set configuration option", set_option_cmd)); + add_cmd(r, cmd_info("exit", "exit", exit_cmd)); + add_cmd(r, cmd_info("print", "print a string", print_cmd)); + add_cmd(r, cmd_info("section", "open a new section", section_cmd)); + add_cmd(r, cmd_info("namespace", "open a new namespace", namespace_cmd)); + add_cmd(r, cmd_info("end", "close the current namespace/section", end_scoped_cmd)); + add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd)); + add_cmd(r, cmd_info("eval", "evaluate given expression", eval_cmd)); + add_cmd(r, cmd_info("find_decl", "find definitions and/or theorems", find_cmd)); + add_cmd(r, cmd_info("local", "define local attributes or notation", local_cmd)); + add_cmd(r, cmd_info("help", "brief description of available commands and options", help_cmd)); + add_cmd(r, cmd_info("init_quotient", "initialize quotient type computational rules", init_quotient_cmd)); + add_cmd(r, cmd_info("init_hits", "initialize builtin HITs", init_hits_cmd)); + add_cmd(r, cmd_info("#erase_cache", "erase cached definition (for debugging purposes)", erase_cache_cmd)); + add_cmd(r, cmd_info("#projections", "generate projections for inductive datatype (for debugging purposes)", projections_cmd)); + add_cmd(r, cmd_info("#telescope_eq", "(for debugging purposes)", telescope_eq_cmd)); + add_cmd(r, cmd_info("#app_builder", "(for debugging purposes)", app_builder_cmd)); + add_cmd(r, cmd_info("#refl", "(for debugging purposes)", refl_cmd)); + add_cmd(r, cmd_info("#trans", "(for debugging purposes)", trans_cmd)); + add_cmd(r, cmd_info("#symm", "(for debugging purposes)", symm_cmd)); + add_cmd(r, cmd_info("#compile", "(for debugging purposes)", compile_cmd)); + add_cmd(r, cmd_info("#accessible", "(for debugging purposes) display number of accessible declarations for blast tactic", accessible_cmd)); + add_cmd(r, cmd_info("#decl_stats", "(for debugging purposes) display declaration statistics", decl_stats_cmd)); + add_cmd(r, cmd_info("#relevant_thms", "(for debugging purposes) select relevant theorems using Meng&Paulson heuristic", relevant_thms_cmd)); register_decl_cmds(r); register_inductive_cmd(r); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 3f2c792d2..5783e2251 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -119,7 +119,7 @@ void init_token_table(token_table & t) { "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl", "attribute", "persistent", "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq", - "#compile", "#accessible", "#decl_stats", "#relevant_thms", "#app_builder", nullptr}; + "#compile", "#accessible", "#decl_stats", "#relevant_thms", "#app_builder", "#refl", "#symm", "#trans", nullptr}; pair aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 9b23f2b28..cb9c2d296 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -104,15 +104,18 @@ struct app_builder::imp { map m_map; refl_info_getter m_refl_getter; - trans_info_getter m_trans_getter; symm_info_getter m_symm_getter; - - imp(environment const & env, io_state const & ios, reducible_behavior b): - m_ctx(new tmp_type_context(env, ios, b)) { - } + trans_info_getter m_trans_getter; imp(std::unique_ptr && ctx): - m_ctx(std::move(ctx)) { + m_ctx(std::move(ctx)), + m_refl_getter(mk_refl_info_getter(m_ctx->env())), + m_symm_getter(mk_symm_info_getter(m_ctx->env())), + m_trans_getter(mk_trans_info_getter(m_ctx->env())) { + } + + imp(environment const & env, io_state const & ios, reducible_behavior b): + imp(std::unique_ptr(new tmp_type_context(env, ios, b))) { } levels mk_metavars(declaration const & d, buffer & mvars, buffer> & inst_args) { diff --git a/tests/lean/run/app_builder.lean b/tests/lean/run/app_builder.lean index dcf21a394..f6bacde42 100644 --- a/tests/lean/run/app_builder.lean +++ b/tests/lean/run/app_builder.lean @@ -5,9 +5,9 @@ variables H1 : a = b variables H2 : b = c set_option pp.all true -#app_builder eq.refl (a) -#app_builder eq.trans (H1, H2) -#app_builder eq.symm (H1) +#app_builder eq.refl a +#app_builder eq.trans H1, H2 +#app_builder eq.symm H1 open algebra nat universe l @@ -16,9 +16,9 @@ constant s : comm_ring A attribute s [instance] variables x y : A -#app_builder eq.refl (s) -#app_builder eq.refl (x) -#app_builder add (x, y) -#app_builder add (a, b) -#app_builder mul (a, b) -#app_builder sub (x, y) +#app_builder eq.refl s +#app_builder eq.refl x +#app_builder add x, y +#app_builder add a, b +#app_builder mul a, b +#app_builder sub x, y diff --git a/tests/lean/run/app_builder2.lean b/tests/lean/run/app_builder2.lean new file mode 100644 index 000000000..9313a8d83 --- /dev/null +++ b/tests/lean/run/app_builder2.lean @@ -0,0 +1,24 @@ +import data.list +open perm +variables a b c : nat +variables H1 : a = b +variables H2 : b = c +set_option pp.all true +variables p q r : Prop +variables l1 l2 l3 : list nat +variables H3 : p ↔ q +variables H4 : q ↔ r +variables H5 : l1 ~ l2 +variables H6 : l2 ~ l3 + +#refl eq a +#refl iff p +#refl perm l1 + +#symm eq H1 +#symm iff H3 +#symm perm H5 + +#trans eq H1, H2 +#trans iff H3, H4 +#trans perm H5, H6 diff --git a/tests/lean/run/app_builder3.lean b/tests/lean/run/app_builder3.lean new file mode 100644 index 000000000..b43e9bc39 --- /dev/null +++ b/tests/lean/run/app_builder3.lean @@ -0,0 +1,7 @@ +constant f : ∀ (A : Type) (a b c : A), a = c → A + +variables a b c : nat +variables H : a = b + +#app_builder f (false, false, true, false, true) c, H +#app_builder f (false, true, true, false, true) a, c, H