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

feat(frontends/lean): add test commands for new app_builder features

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-01 17:19:57 -08:00
parent 1c2c2a6077
commit f21102a725
6 changed files with 160 additions and 46 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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<bool> 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<expr> 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<expr> 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);

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

@ -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<char const *, char const *> aliases[] =
{{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

15
src/library/app_builder.cpp
View file

@ -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<tmp_type_context> && 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<tmp_type_context>(new tmp_type_context(env, ios, b))) {
}
levels mk_metavars(declaration const & d, buffer<expr> & mvars, buffer<optional<expr>> & inst_args) {

18
tests/lean/run/app_builder.lean
View file

@ -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

24
tests/lean/run/app_builder2.lean Normal file
View file

@ -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

7
tests/lean/run/app_builder3.lean Normal file
View file

@ -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