michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): add #congr debugging command

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-06 19:13:11 -08:00
parent 22dcf6825e
commit 9b34526030
2 changed files with 25 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/frontends/lean/builtin_cmds.cpp
View file

@ -42,6 +42,7 @@ Author: Leonardo de Moura
#include "library/app_builder.h"
#include "library/meng_paulson.h"
#include "library/fun_info_manager.h"
#include "library/congr_lemma_manager.h"
#include "library/definitional/projection.h"
#include "library/simplifier/simp_rule_set.h"
#include "compiler/preprocess_rec.h"
@ -1259,7 +1260,6 @@ static void parse_expr_vector(parser & p, buffer<expr> & r) {
static environment replace_cmd(parser & p) {
environment const & env = p.env();
auto pos = p.pos();
app_builder b(env);
expr e; level_param_names ls;
buffer<expr> from;
buffer<expr> to;
@ -1279,6 +1279,25 @@ static environment replace_cmd(parser & p) {
return env;
}
static environment congr_lemma_cmd(parser & p) {
environment const & env = p.env();
auto pos = p.pos();
expr e; level_param_names ls;
std::tie(e, ls) = parse_local_expr(p);
tmp_type_context ctx(env, p.ios());
app_builder b(ctx);
fun_info_manager infom(ctx);
congr_lemma_manager cm(b, infom);
auto r = cm.mk_congr_simp(e);
if (!r)
throw parser_error("failed to generated congruence lemma", pos);
p.regular_stream() << r->first << "\n";;
type_checker tc(env);
expr type = tc.check(r->first, ls).first;
p.regular_stream() << type << "\n";
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",
open_cmd));
@ -1308,6 +1327,7 @@ void init_cmd_table(cmd_table & r) {
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("#replace", "(for debugging purposes)", replace_cmd));
add_cmd(r, cmd_info("#congr", "(for debugging purposes)", congr_lemma_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));

6
src/frontends/lean/token_table.cpp
View file

@ -106,7 +106,8 @@ void init_token_table(token_table & t) {
char const * commands[] =
{"theorem", "axiom", "axioms", "variable", "protected", "private", "reveal",
"definition", "example", "coercion", "abbreviation", "noncomputable",
"variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", "[trans_instance]",
"variables", "parameter", "parameters", "constant", "constants",
"[persistent]", "[visible]", "[instance]", "[trans_instance]",
"[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
"[simp]", "[congr]", "[parsing_only]", "[multiple_instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor",
"evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold_full]", "[unfold_hints]",
@ -119,7 +120,8 @@ 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", "#refl", "#symm", "#trans", "#replace", nullptr};
"#compile", "#accessible", "#decl_stats", "#relevant_thms", "#app_builder", "#refl", "#symm",
"#trans", "#replace", "#congr", nullptr};
pair<char const *, char const *> aliases[] =
{{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},