max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/tactic/simplifier): remove simp_extensions

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-06 20:48:12 -07:00
parent d747fcb17c
commit 3fbdb71f3e
12 changed files with 2 additions and 365 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -34,7 +34,6 @@ Author: Leonardo de Moura
#include "library/compiler/vm_compiler.h"
#include "library/tactic/kabstract.h"
#include "library/tactic/elaborate.h"
#include "library/tactic/simplifier/simp_extensions.h"
#include "library/tactic/tactic_state.h"
#include "frontends/lean/util.h"
#include "frontends/lean/parser.h"
@ -375,26 +374,6 @@ static environment init_quotient_cmd(parser & p) {
return module::declare_quotient(p.env());
}
// register_simp_ext <head> <simp_ext_name> ([priority <prio>])
static environment register_simp_ext_cmd(parser & p) {
environment env = p.env();
name head = p.check_constant_next("invalid #register_simp_ext_cmd command, constant expected");
name simp_ext_name = p.check_constant_next("invalid #register_simp_ext_cmd command, constant expected");
unsigned prio = LEAN_DEFAULT_PRIORITY;
auto pos = p.pos();
decl_attributes attrs;
attrs.parse(p);
if (auto const & entry = head_opt(attrs.get_entries()))
throw parser_error(sstream() << "invalid #register_simp_ext_cmd command, unexpected attribute ["
<< entry->m_attr->get_name() << "]", pos);
if (attrs.get_priority())
prio = *attrs.get_priority();
bool persistent = true;
env = add_simp_extension(env, p.ios(), head, simp_ext_name, prio, persistent);
return env;
}
/*
Temporary procedure that converts metavariables in \c e to metavar_context metavariables.
After we convert the frontend to type_context, we will not need to use this procedure.
@ -577,7 +556,6 @@ void init_cmd_table(cmd_table & r) {
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("declare_trace", "declare a new trace class (for debugging Lean tactics)", declare_trace_cmd));
add_cmd(r, cmd_info("register_simp_ext", "register simplifier extension", register_simp_ext_cmd));
add_cmd(r, cmd_info("add_key_equivalence", "register that to symbols are equivalence for key-matching", add_key_equivalence_cmd));
add_cmd(r, cmd_info("run_command", "execute an user defined command at top-level", run_command_cmd));
add_cmd(r, cmd_info("#erase_cache", "erase cached definition (for debugging purposes)", erase_cache_cmd));

1
src/frontends/lean/print_cmd.cpp
View file

@ -27,7 +27,6 @@ Author: Leonardo de Moura
#include "library/rfl_lemmas.h"
#include "library/tactic/kabstract.h"
#include "library/tactic/simplifier/simp_lemmas.h"
#include "library/tactic/simplifier/simp_extensions.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/util.h"
#include "frontends/lean/tokens.h"

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

@ -108,8 +108,7 @@ void init_token_table(token_table & t) {
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
"exit", "set_option", "open", "export", "override", "@[",
"attribute", "persistent", "instance", "include", "omit", "init_quotient",
"init_hits", "declare_trace", "register_simp_ext",
"run_command", "add_key_equivalence", "#erase_cache",
"init_hits", "declare_trace", "run_command", "add_key_equivalence", "#erase_cache",
"#compile", "#unify", nullptr};
pair<char const *, char const *> aliases[] =

1
src/library/inductive_compiler/nested.cpp
View file

@ -1243,7 +1243,6 @@ class add_nested_inductive_decl_fn {
opts = opts.update(get_simplify_nary_assoc_name(), false);
opts = opts.update(get_simplify_memoize_name(), true);
opts = opts.update(get_simplify_contextual_name(), false);
opts = opts.update(get_simplify_user_extensions_name(), false);
opts = opts.update(get_simplify_rewrite_name(), true);
opts = opts.update(get_simplify_unsafe_nary_name(), false);
opts = opts.update(get_simplify_theory_name(), true);

2
src/library/tactic/simplifier/CMakeLists.txt
View file

@ -1,3 +1,3 @@
add_library(simplifier OBJECT init_module.cpp ceqv.cpp simplifier.cpp simp_lemmas.cpp
simp_extensions.cpp prop_simplifier.cpp arith_simplifier.cpp theory_simplifier.cpp util.cpp
prop_simplifier.cpp arith_simplifier.cpp theory_simplifier.cpp util.cpp
)

3
src/library/tactic/simplifier/init_module.cpp
View file

@ -6,7 +6,6 @@ Author: Daniel Selsam
#include "library/trace.h"
#include "library/tactic/simplifier/util.h"
#include "library/tactic/simplifier/simp_lemmas.h"
#include "library/tactic/simplifier/simp_extensions.h"
#include "library/tactic/simplifier/prop_simplifier.h"
#include "library/tactic/simplifier/arith_simplifier.h"
#include "library/tactic/simplifier/theory_simplifier.h"
@ -19,7 +18,6 @@ void initialize_simplifier_module() {
initialize_simp_util();
initialize_simp_lemmas();
initialize_simp_extensions();
initialize_prop_simplifier();
initialize_arith_simplifier();
initialize_theory_simplifier();
@ -31,7 +29,6 @@ void finalize_simplifier_module() {
finalize_theory_simplifier();
finalize_arith_simplifier();
finalize_prop_simplifier();
finalize_simp_extensions();
finalize_simp_lemmas();
finalize_simp_util();
}

124
src/library/tactic/simplifier/simp_extensions.cpp
View file

@ -1,124 +0,0 @@
/*
Copyright (c) 2016 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#include <string>
#include "util/priority_queue.h"
#include "library/trace.h"
#include "library/scoped_ext.h"
#include "library/attribute_manager.h"
#include "library/vm/vm.h"
#include "library/tactic/simplifier/simp_extensions.h"
namespace lean {
static std::string * g_key = nullptr;
struct simp_ext_entry {
unsigned m_prio;
name m_head;
name m_ext_name;
simp_ext_entry(unsigned prio, name head, name ext_name):
m_prio(prio), m_head(head), m_ext_name(ext_name) {}
};
struct simp_ext_record {
name m_ext_name;
unsigned m_ext_id;
simp_ext_record() {}
simp_ext_record(name ext_name, unsigned ext_id): m_ext_name(ext_name), m_ext_id(ext_id) {}
};
struct simp_ext_record_cmp {
int operator()(simp_ext_record const & r1, simp_ext_record const & r2) const {
// If the names are the same and the environments are compatible, then the ids must be the same as well
return quick_cmp(r1.m_ext_name, r2.m_ext_name);
}
};
typedef name_map<priority_queue<simp_ext_record, simp_ext_record_cmp>> simp_ext_state;
struct simp_ext_config {
typedef simp_ext_entry entry;
typedef simp_ext_state state;
static void add_entry(environment const & env, io_state const &, state & s, entry const & e) {
if (optional<unsigned> fn_idx = get_vm_constant_idx(env, e.m_ext_name)) {
priority_queue<simp_ext_record, simp_ext_record_cmp> m;
if (auto q = s.find(e.m_head)) {
m = *q;
}
m.insert(simp_ext_record(e.m_ext_name, *fn_idx), e.m_prio);
s.insert(e.m_head, m);
} else {
throw exception(sstream() << "error in adding simplifier extension: no vm_decl for " << e.m_ext_name << "\n");
}
}
static std::string const & get_serialization_key() {
return *g_key;
}
static void write_entry(serializer & s, entry const & e) {
s << e.m_prio << e.m_head << e.m_ext_name;
}
static entry read_entry(deserializer & d) {
unsigned prio; name head; name ext_name;
d >> prio >> head >> ext_name;
return entry(prio, head, ext_name);
}
static optional<unsigned> get_fingerprint(entry const & e) {
return some(hash(e.m_head.hash(), hash(e.m_ext_name.hash(), e.m_prio)));
}
};
typedef scoped_ext<simp_ext_config> simp_ext_ext;
environment add_simp_extension(environment const & env, io_state const & ios, name const & head, name const & simp_ext_name, unsigned prio, bool persistent) {
return simp_ext_ext::add_entry(env, ios, simp_ext_entry(prio, head, simp_ext_name), persistent);
}
format pp_simp_extensions_for_head(priority_queue<simp_ext_record, simp_ext_record_cmp> const & q) {
format fmt;
q.for_each([&](simp_ext_record const & r) {
fmt += format(r.m_ext_name);
unsigned prio = *q.get_prio(r);
if (prio != LEAN_DEFAULT_PRIORITY)
fmt += space() + paren(format(prio));
fmt += line();
});
return fmt;
}
format pp_simp_extensions(environment const & env) {
simp_ext_state s = simp_ext_ext::get_state(env);
format fmt;
s.for_each([&](name const & head, priority_queue<simp_ext_record, simp_ext_record_cmp> const & q) {
fmt += format("simplification extensions for ") + format(head) + line();
fmt += pp_simp_extensions_for_head(q);
});
return fmt;
}
void get_simp_extensions_for(environment const & env, name const & head, buffer<unsigned> & ext_ids) {
simp_ext_state s = simp_ext_ext::get_state(env);
if (auto q = s.find(head)) {
buffer<simp_ext_record> records;
q->for_each([&](simp_ext_record const & r) {
ext_ids.push_back(r.m_ext_id);
});
}
}
void initialize_simp_extensions() {
g_key = new std::string("SIMP_EXT");
simp_ext_ext::initialize();
}
void finalize_simp_extensions() {
simp_ext_ext::finalize();
delete g_key;
}
}

22
src/library/tactic/simplifier/simp_extensions.h
View file

@ -1,22 +0,0 @@
/*
Copyright (c) 2016 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#pragma once
#include "kernel/expr_pair.h"
#include "library/head_map.h"
#include "library/type_context.h"
namespace lean {
environment add_simp_extension(environment const & env, io_state const & ios, name const & head, name const & ext_name, unsigned prio, bool persistent);
format pp_simp_extensions(environment const & env);
void get_simp_extensions_for(environment const & env, name const & head, buffer<unsigned> & ext_ids);
void initialize_simp_extensions();
void finalize_simp_extensions();
}

94
src/library/tactic/simplifier/simplifier.cpp
View file

@ -37,7 +37,6 @@ Author: Daniel Selsam
#include "library/tactic/app_builder_tactics.h"
#include "library/tactic/simplifier/simplifier.h"
#include "library/tactic/simplifier/simp_lemmas.h"
#include "library/tactic/simplifier/simp_extensions.h"
#include "library/tactic/simplifier/theory_simplifier.h"
#include "library/tactic/simplifier/ceqv.h"
#include "library/tactic/simplifier/util.h"
@ -54,9 +53,6 @@ Author: Daniel Selsam
#ifndef LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL
#define LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL true
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_USER_EXTENSIONS
#define LEAN_DEFAULT_SIMPLIFY_USER_EXTENSIONS true
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_REWRITE
#define LEAN_DEFAULT_SIMPLIFY_REWRITE true
#endif
@ -93,7 +89,6 @@ static name * g_simplify_max_steps = nullptr;
static name * g_simplify_nary_assoc = nullptr;
static name * g_simplify_memoize = nullptr;
static name * g_simplify_contextual = nullptr;
static name * g_simplify_user_extensions = nullptr;
static name * g_simplify_rewrite = nullptr;
static name * g_simplify_unsafe_nary = nullptr;
static name * g_simplify_theory = nullptr;
@ -107,7 +102,6 @@ name get_simplify_max_steps_name() { return *g_simplify_max_steps; }
name get_simplify_nary_assoc_name() { return *g_simplify_nary_assoc; }
name get_simplify_memoize_name() { return *g_simplify_memoize; }
name get_simplify_contextual_name() { return *g_simplify_contextual; }
name get_simplify_user_extensions_name() { return *g_simplify_user_extensions; }
name get_simplify_rewrite_name() { return *g_simplify_rewrite; }
name get_simplify_unsafe_nary_name() { return *g_simplify_unsafe_nary; }
name get_simplify_theory_name() { return *g_simplify_theory; }
@ -133,10 +127,6 @@ static bool get_simplify_contextual(options const & o) {
return o.get_bool(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL);
}
static bool get_simplify_user_extensions(options const & o) {
return o.get_bool(*g_simplify_user_extensions, LEAN_DEFAULT_SIMPLIFY_USER_EXTENSIONS);
}
static bool get_simplify_rewrite(options const & o) {
return o.get_bool(*g_simplify_rewrite, LEAN_DEFAULT_SIMPLIFY_REWRITE);
}
@ -196,7 +186,6 @@ class simplifier {
unsigned m_nary_assoc;
bool m_memoize;
bool m_contextual;
bool m_user_extensions;
bool m_rewrite;
bool m_unsafe_nary;
bool m_theory;
@ -334,41 +323,6 @@ class simplifier {
return r;
}
// Binary simplify methods
simp_result simplify_user_extensions_binary(expr const & old_e) {
expr op = get_app_fn(old_e);
if (!is_constant(op)) return simp_result(old_e);
name head = const_name(op);
buffer<unsigned> ext_ids;
get_simp_extensions_for(m_tctx.env(), head, ext_ids);
for (unsigned ext_id : ext_ids) {
expr old_e_type = m_tctx.infer(old_e);
metavar_context mctx = m_tctx.mctx();
expr result_mvar = mctx.mk_metavar_decl(m_tctx.lctx(), old_e_type);
m_tctx.set_mctx(mctx); // the app-builder needs to know about these metavars
expr goal_type = mk_app(m_tctx, m_rel, old_e, result_mvar);
expr goal_mvar = mctx.mk_metavar_decl(m_tctx.lctx(), goal_type);
vm_obj s = to_obj(tactic_state(m_tctx.env(), m_tctx.get_options(), mctx, list<expr>(goal_mvar), goal_mvar));
vm_obj simp_ext_result = invoke(ext_id, s);
optional<tactic_state> s_new = is_tactic_success(simp_ext_result);
// TODO(dhs): create a bool metavar for the `done` flag
if (s_new) {
m_tctx.set_mctx(s_new->mctx());
expr result = m_tctx.instantiate_mvars(result_mvar);
expr proof = m_tctx.instantiate_mvars(goal_mvar);
if (is_app_of(proof, get_eq_refl_name(), 2) || is_app_of(proof, get_rfl_name(), 2)) {
return simp_result(result);
} else {
return simp_result(result, proof);
}
} else {
lean_trace(name({"simplifier", "extensions"}),
tout() << "extension failed on goal " << goal_type << "\n";);
}
}
return simp_result(old_e);
}
simp_result simplify_rewrite_binary(expr const & e) {
simp_lemmas slss = ::lean::join(m_slss, m_ctx_slss);
simp_lemmas_for const * sr = slss.find(m_rel);
@ -466,14 +420,6 @@ class simplifier {
return r_rewrite;
}
}
if (m_user_extensions) {
simp_result r_user = simplify_user_extensions_binary(e);
if (r_user.get_new() != e) {
lean_trace_d(name({"simplifier", "user_extensions"}), tout() << e << " ==> " << r_user.get_new() << "\n";);
return r_user;
}
}
}
// [1] Simplify subterms using congruence
@ -521,17 +467,6 @@ class simplifier {
return join(r, r_rewrite);
}
}
if (m_user_extensions) {
simp_result r_user = simplify_user_extensions_binary(r.get_new());
if (r_user.get_new() != r.get_new()) {
lean_trace_d(name({"simplifier", "user_extensions"}), tout() << r.get_new() << " ==> " << r_user.get_new() << "\n";);
simp_result r_join_user = join(r, r_user);
if (r_user.is_done())
r_join_user.set_done();
return r_join_user;
}
}
}
// [5] Simplify with the theory simplifier
@ -640,17 +575,6 @@ class simplifier {
return optional<simp_result>(simp_result(new_rhs, pf));
}
optional<simp_result> simplify_user_extensions_nary(expr const & /* assoc */, expr const & old_e, expr const & /* op */, buffer<expr> const & /* nary_args */) {
// For now, user extensions are not aware of the binary/nary distinction, except that they are guaranteed that
// if an operator is an instance of [is_associative] for the relation in question, the user extension will only be
// called on the outermost applications.
simp_result r = simplify_user_extensions_binary(old_e);
if (r.get_new() != old_e)
return optional<simp_result>(r);
else
return optional<simp_result>();
}
simp_result simplify_subterms_app_nary_core(expr const & old_op, expr const & new_op, optional<expr> const & pf_op, expr const & e) {
expr arg1, arg2;
optional<expr> op = get_binary_op(e, arg1, arg2);
@ -700,12 +624,6 @@ class simplifier {
return join(r_flat, *r_rewrite);
}
}
if (m_user_extensions) {
if (optional<simp_result> r_user = simplify_user_extensions_nary(assoc, r_flat.get_new(), op, nary_args)) {
lean_trace_d(name({"simplifier", "user_extensions"}), tout() << old_e << " ==> " << r_user->get_new() << "\n";);
return join(r_flat, *r_user);
}
}
}
simp_result r_congr = simplify_subterms_app_nary(op, old_e);
@ -726,12 +644,6 @@ class simplifier {
return join(r_congr_flat, *r_rewrite);
}
}
if (m_user_extensions) {
if (optional<simp_result> r_user = simplify_user_extensions_nary(assoc, r_congr_flat.get_new(), new_op, new_nary_args)) {
lean_trace_d(name({"simplifier", "user_extensions"}), tout() << old_e << " ==> " << r_user->get_new() << "\n";);
return join(r_congr_flat, *r_user);
}
}
}
// [5] Simplify with the theory simplifier
@ -796,7 +708,6 @@ public:
m_nary_assoc(get_simplify_nary_assoc(tctx.get_options())),
m_memoize(get_simplify_memoize(tctx.get_options())),
m_contextual(get_simplify_contextual(tctx.get_options())),
m_user_extensions(get_simplify_user_extensions(tctx.get_options())),
m_rewrite(get_simplify_rewrite(tctx.get_options())),
m_unsafe_nary(get_simplify_unsafe_nary(tctx.get_options())),
m_theory(get_simplify_theory(tctx.get_options())),
@ -1434,7 +1345,6 @@ vm_obj tactic_simplify_core(vm_obj const & prove_fn, vm_obj const & rel_name, vm
/* Setup and teardown */
void initialize_simplifier() {
register_trace_class(name({"simplifier", "congruence"}));
register_trace_class(name({"simplifier", "user_extensions"}));
register_trace_class(name({"simplifier", "failure"}));
register_trace_class(name({"simplifier", "failed"}));
register_trace_class(name({"simplifier", "perm"}));
@ -1456,7 +1366,6 @@ void initialize_simplifier() {
g_simplify_nary_assoc = new name{*g_simplify_prefix, "nary_assoc"};
g_simplify_memoize = new name{*g_simplify_prefix, "memoize"};
g_simplify_contextual = new name{*g_simplify_prefix, "contextual"};
g_simplify_user_extensions = new name{*g_simplify_prefix, "user_extensions"};
g_simplify_rewrite = new name{*g_simplify_prefix, "rewrite"};
g_simplify_unsafe_nary = new name{*g_simplify_prefix, "unsafe_nary"};
g_simplify_theory = new name{*g_simplify_prefix, "theory"};
@ -1474,8 +1383,6 @@ void initialize_simplifier() {
"(simplify) memoize simplifications");
register_bool_option(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL,
"(simplify) use contextual simplification");
register_bool_option(*g_simplify_user_extensions, LEAN_DEFAULT_SIMPLIFY_USER_EXTENSIONS,
"(simplify) simplify with user_extensions");
register_bool_option(*g_simplify_rewrite, LEAN_DEFAULT_SIMPLIFY_REWRITE,
"(simplify) rewrite with simp_lemmas");
register_bool_option(*g_simplify_unsafe_nary, LEAN_DEFAULT_SIMPLIFY_UNSAFE_NARY,
@ -1508,7 +1415,6 @@ void finalize_simplifier() {
delete g_simplify_theory;
delete g_simplify_unsafe_nary;
delete g_simplify_rewrite;
delete g_simplify_user_extensions;
delete g_simplify_contextual;
delete g_simplify_memoize;
delete g_simplify_nary_assoc;

1
src/library/tactic/simplifier/simplifier.h
View file

@ -20,7 +20,6 @@ name get_simplify_max_steps_name();
name get_simplify_nary_assoc_name();
name get_simplify_memoize_name();
name get_simplify_contextual_name();
name get_simplify_user_extensions_name();
name get_simplify_rewrite_name();
name get_simplify_unsafe_nary_name();
name get_simplify_theory_name();

32
tests/lean/run/simp_ext_refl.lean
View file

@ -1,32 +0,0 @@
open tactic
constants (A : Type.{1}) (x y z : A) (g : A → A) (Hg : g y = z)
attribute [simp] Hg
noncomputable definition f (a : A) := y
lemma f.def : ∀ (a), f a = y := λ a, rfl
meta definition simp_f_to_y : tactic unit := mk_eq_simp_ext $
λ e, if expr.get_app_num_args e = 1
then do res ← mk_const `y,
pf ← mk_app `rfl [e],
return (res, pf)
else fail "expected f applied to one arg"
meta definition simp_f_to_y₂ : tactic unit := mk_eq_simp_ext $
λ e, if expr.get_app_num_args e = 1
then do res ← mk_const `y,
pf ← mk_app `f.def [expr.app_arg e],
return (res, pf)
else fail "expected f applied to one arg"
register_simp_ext f simp_f_to_y
definition foo : g (f x) = z := by simp
register_simp_ext f simp_f_to_y₂
definition foo₂ : g (f x) = z := by simp
print foo
print foo₂

62
tests/lean/run/simp_orderings.lean
View file

@ -1,62 +0,0 @@
open tactic
-------------
namespace simp_lemmas
constants (A : Type.{1}) (x y z : A) (Hxy : x = y) (Hxz : x = z)
attribute [simp] Hxy
attribute [simp] Hxz
example : x = z := by simp
end simp_lemmas
-------------
namespace simp_lemmas_args
constants (A : Type.{1}) (x y z : A) (Hxy : x = y) (Hxz : x = z)
attribute [simp] Hxy
example : x = z :=
by do H ← mk_const `simp_lemmas_args.Hxz,
`[simp [%%H]]
end simp_lemmas_args
-------------
namespace simp_args
constants (A : Type.{1}) (x y z : A) (Hxy : x = y) (Hxz : x = z)
example : x = z :=
by do Hy ← mk_const `simp_args.Hxy,
Hz ← mk_const `simp_args.Hxz,
-- CONFIRM(leo): latter arguments should get priority?
`[simp [%%Hy, %%Hz]]
end simp_args
-------------
namespace simp_extensions
constants (A : Type.{1}) (x y z : A) (Hxy : x = y) (Hxz : x = z)
meta definition simp_x_to_y : tactic unit := mk_eq_simp_ext $
λ e, do res ← mk_const `simp_extensions.y,
pf ← mk_const `simp_extensions.Hxy,
return (res, pf)
meta definition simp_x_to_z : tactic unit := mk_eq_simp_ext $
λ e, do res ← mk_const `simp_extensions.z,
pf ← mk_const `simp_extensions.Hxz,
return (res, pf)
register_simp_ext x simp_x_to_y
register_simp_ext x simp_x_to_z
example : x = z := by simp
end simp_extensions
---------------