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

feat(library/blast/backward): backward chaining strategy

Browse source
This commit is contained in:
Daniel Selsam 2015-11-18 15:41:44 -08:00
parent 39a9ab6bf8
commit 413989afd6
36 changed files with 525 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/CMakeLists.txt
View file

@ -349,6 +349,8 @@ add_subdirectory(library/definitional)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:definitional>)
add_subdirectory(library/blast)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast>)
add_subdirectory(library/blast/backward)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:backward>)
add_subdirectory(library/error_handling)
set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:error_handling>)
add_subdirectory(compiler)

6
src/emacs/lean-syntax.el
View file

@ -46,8 +46,8 @@
(defconst lean-constants-regexp (regexp-opt lean-constants))
(defconst lean-numerals-regexp
(eval `(rx word-start
(one-or-more digit) (optional (and "." (zero-or-more digit)))
word-end)))
(one-or-more digit) (optional (and "." (zero-or-more digit)))
word-end)))
(defconst lean-modifiers
(--map (s-concat "[" it "]")
@ -55,7 +55,7 @@
"class" "parsing_only" "coercion" "unfold_full" "constructor"
"reducible" "irreducible" "semireducible" "quasireducible" "wf"
"whnf" "multiple_instances" "none" "decls" "declarations"
"coercions" "classes" "symm" "subst" "refl" "trans" "simp" "congr"
"coercions" "classes" "symm" "subst" "refl" "trans" "simp" "congr" "backward"
"notations" "abbreviations" "begin_end_hints" "tactic_hints"
"reduce_hints" "unfold_hints" "aliases" "eqv"
"localrefinfo" "recursor"))

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

@ -48,6 +48,7 @@ Author: Leonardo de Moura
#include "library/simplifier/simp_rule_set.h"
#include "library/blast/blast.h"
#include "library/blast/simplifier.h"
#include "library/blast/backward/backward_rule_set.h"
#include "compiler/preprocess_rec.h"
#include "frontends/lean/util.h"
#include "frontends/lean/parser.h"
@ -257,6 +258,8 @@ static void print_attributes(parser const & p, name const & n) {
out << " [simp]";
if (is_congr_rule(env, n))
out << " [congr]";
if (is_backward_rule(env, n))
out << " [backward]";
switch (get_reducible_status(env, n)) {
case reducible_status::Reducible: out << " [reducible]"; break;
case reducible_status::Irreducible: out << " [irreducible]"; break;
@ -496,6 +499,12 @@ static void print_congr_rules(parser & p) {
out << s.pp_congr(out.get_formatter());
}
static void print_backward_rules(parser & p) {
io_state_stream out = p.regular_stream();
blast::backward_rule_set brs = get_backward_rule_set(p.env());
out << brs;
}
environment print_cmd(parser & p) {
flycheck_information info(p.regular_stream());
if (info.enabled()) {
@ -609,6 +618,9 @@ environment print_cmd(parser & p) {
} else if (p.curr_is_token(get_congr_attr_tk())) {
p.next();
print_congr_rules(p);
} else if (p.curr_is_token(get_backward_attr_tk())) {
p.next();
print_backward_rules(p);
} else if (print_polymorphic(p)) {
} else {
throw parser_error("invalid print command", p.pos());

15
src/frontends/lean/decl_attributes.cpp
View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "library/user_recursors.h"
#include "library/coercion.h"
#include "library/simplifier/simp_rule_set.h"
#include "library/blast/backward/backward_rule_set.h"
#include "frontends/lean/decl_attributes.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/tokens.h"
@ -41,6 +42,7 @@ decl_attributes::decl_attributes(bool is_abbrev, bool persistent):
m_recursor = false;
m_simp = false;
m_congr = false;
m_backward = false;
}
void decl_attributes::parse(parser & p) {
@ -87,8 +89,8 @@ void decl_attributes::parse(parser & p) {
p.next();
} else if (auto it = parse_priority(p)) {
m_priority = *it;
if (!m_is_instance && !m_simp && !m_congr) {
throw parser_error("invalid '[priority]' attribute, declaration must be marked as an '[instance]', '[simp]' or '[congr]'", pos);
if (!m_is_instance && !m_simp && !m_congr && !m_backward) {
throw parser_error("invalid '[priority]' attribute, declaration must be marked as an '[instance]', '[simp]', '[congr], or [backward]'", pos);
}
} else if (p.curr_is_token(get_parsing_only_tk())) {
if (!m_is_abbrev)
@ -133,6 +135,9 @@ void decl_attributes::parse(parser & p) {
} else if (p.curr_is_token(get_congr_attr_tk())) {
p.next();
m_congr = true;
} else if (p.curr_is_token(get_backward_attr_tk())) {
p.next();
m_backward = true;
} else if (p.curr_is_token(get_recursor_tk())) {
p.next();
if (!p.curr_is_token(get_rbracket_tk())) {
@ -213,6 +218,12 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
else
env = add_congr_rule(env, d, LEAN_SIMP_DEFAULT_PRIORITY, m_persistent);
}
if (m_backward) {
if (m_priority)
env = add_backward_rule(env, d, *m_priority, m_persistent);
else
env = add_backward_rule(env, d, LEAN_BACKWARD_DEFAULT_PRIORITY, m_persistent);
}
if (m_has_multiple_instances)
env = mark_multiple_instances(env, d, m_persistent);
return env;

1
src/frontends/lean/decl_attributes.h
View file

@ -31,6 +31,7 @@ class decl_attributes {
bool m_recursor;
bool m_simp;
bool m_congr;
bool m_backward;
optional<unsigned> m_recursor_major_pos;
optional<unsigned> m_priority;
list<unsigned> m_unfold_hint;

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

@ -110,7 +110,7 @@ void init_token_table(token_table & t) {
"[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]",
"evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold_full]", "[unfold_hints]", "[backward]",
"[constructor]", "[unfold", "print",
"end", "namespace", "section", "prelude", "help",
"import", "inductive", "record", "structure", "module", "universe", "universes", "local",

4
src/frontends/lean/tokens.cpp
View file

@ -120,6 +120,7 @@ static name const * g_refl_tk = nullptr;
static name const * g_subst_tk = nullptr;
static name const * g_simp_attr_tk = nullptr;
static name const * g_congr_attr_tk = nullptr;
static name const * g_backward_attr_tk = nullptr;
static name const * g_recursor_tk = nullptr;
static name const * g_attribute_tk = nullptr;
static name const * g_with_tk = nullptr;
@ -274,6 +275,7 @@ void initialize_tokens() {
g_subst_tk = new name{"[subst]"};
g_simp_attr_tk = new name{"[simp]"};
g_congr_attr_tk = new name{"[congr]"};
g_backward_attr_tk = new name{"[backward]"};
g_recursor_tk = new name{"[recursor"};
g_attribute_tk = new name{"attribute"};
g_with_tk = new name{"with"};
@ -429,6 +431,7 @@ void finalize_tokens() {
delete g_subst_tk;
delete g_simp_attr_tk;
delete g_congr_attr_tk;
delete g_backward_attr_tk;
delete g_recursor_tk;
delete g_attribute_tk;
delete g_with_tk;
@ -583,6 +586,7 @@ name const & get_refl_tk() { return *g_refl_tk; }
name const & get_subst_tk() { return *g_subst_tk; }
name const & get_simp_attr_tk() { return *g_simp_attr_tk; }
name const & get_congr_attr_tk() { return *g_congr_attr_tk; }
name const & get_backward_attr_tk() { return *g_backward_attr_tk; }
name const & get_recursor_tk() { return *g_recursor_tk; }
name const & get_attribute_tk() { return *g_attribute_tk; }
name const & get_with_tk() { return *g_with_tk; }

1
src/frontends/lean/tokens.h
View file

@ -122,6 +122,7 @@ name const & get_refl_tk();
name const & get_subst_tk();
name const & get_simp_attr_tk();
name const & get_congr_attr_tk();
name const & get_backward_attr_tk();
name const & get_recursor_tk();
name const & get_attribute_tk();
name const & get_with_tk();

1
src/frontends/lean/tokens.txt
View file

@ -115,6 +115,7 @@ refl [refl]
subst [subst]
simp_attr [simp]
congr_attr [congr]
backward_attr [backward]
recursor [recursor
attribute attribute
with with

15
src/kernel/expr.cpp
View file

@ -666,6 +666,21 @@ unsigned hash_bi(expr const & e) {
return h;
}
std::ostream & operator<<(std::ostream & out, expr_kind const & k) {
switch (k) {
case expr_kind::Var: out << "Var"; break;
case expr_kind::Sort: out << "Sort"; break;
case expr_kind::Constant: out << "Constant"; break;
case expr_kind::Meta: out << "Meta"; break;
case expr_kind::Local: out << "Local"; break;
case expr_kind::App: out << "App"; break;
case expr_kind::Lambda: out << "Lambda"; break;
case expr_kind::Pi: out << "Pi"; break;
case expr_kind::Macro: out << "Macro"; break;
}
return out;
}
void initialize_expr() {
g_dummy = new expr(mk_constant("__expr_for_default_constructor__"));
g_default_name = new name("a");

1
src/kernel/expr.h
View file

@ -617,6 +617,7 @@ expr infer_implicit(expr const & t, unsigned num_params, bool strict);
expr infer_implicit(expr const & t, bool strict);
// =======================================
std::ostream & operator<<(std::ostream & out, expr_kind const & k);
std::ostream & operator<<(std::ostream & out, expr const & e);
void initialize_expr();

2
src/library/blast/CMakeLists.txt
View file

@ -1,6 +1,6 @@
add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp
init_module.cpp simplifier.cpp simple_actions.cpp intros_action.cpp proof_expr.cpp
options.cpp choice_point.cpp simple_strategy.cpp backward_action.cpp util.cpp
options.cpp choice_point.cpp simple_strategy.cpp util.cpp
gexpr.cpp revert.cpp subst_action.cpp no_confusion_action.cpp
simplify_actions.cpp strategy.cpp recursor_action.cpp congruence_closure.cpp
trace.cpp)

1
src/library/blast/backward/CMakeLists.txt Normal file
View file

@ -0,0 +1 @@
add_library(backward OBJECT init_module.cpp backward_action.cpp backward_rule_set.cpp backward_strategy.cpp)

0
src/library/blast/backward_action.cpp → src/library/blast/backward/backward_action.cpp
View file

0
src/library/blast/backward_action.h → src/library/blast/backward/backward_action.h
View file

161
src/library/blast/backward/backward_rule_set.cpp Normal file
View file

@ -0,0 +1,161 @@
/*
Copyright (c) 2015 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#include "library/blast/backward/backward_rule_set.h"
#include "util/sstream.h"
#include "kernel/error_msgs.h"
#include "kernel/instantiate.h"
#include "library/scoped_ext.h"
#include <string>
namespace lean {
using blast::backward_rule;
using blast::backward_rule_set;
using blast::gexpr;
static name * g_class_name = nullptr;
static std::string * g_key = nullptr;
struct brs_state {
backward_rule_set m_backward_rule_set;
name_set m_names;
void add(environment const & env, io_state const & ios, name const & cname, unsigned prio) {
default_type_context tctx(env, ios);
m_backward_rule_set.insert(tctx, cname, prio);
m_names.insert(cname);
}
};
struct brs_entry {
name m_name;
unsigned m_priority;
brs_entry() {}
brs_entry(name const & n, unsigned prio): m_name(n), m_priority(prio) { }
};
struct brs_config {
typedef brs_entry entry;
typedef brs_state state;
static void add_entry(environment const & env, io_state const & ios, state & s, entry const & e) {
s.add(env, ios, e.m_name, e.m_priority);
}
static name const & get_class_name() {
return *g_class_name;
}
static std::string const & get_serialization_key() {
return *g_key;
}
static void write_entry(serializer & s, entry const & e) {
s << e.m_name << e.m_priority;
}
static entry read_entry(deserializer & d) {
entry e; d >> e.m_name >> e.m_priority; return e;
}
static optional<unsigned> get_fingerprint(entry const & e) {
return some(e.m_name.hash());
}
};
template class scoped_ext<brs_config>;
typedef scoped_ext<brs_config> brs_ext;
environment add_backward_rule(environment const & env, name const & n, unsigned priority, bool persistent) {
return brs_ext::add_entry(env, get_dummy_ios(), brs_entry(n, priority), persistent);
}
bool is_backward_rule(environment const & env, name const & n) {
return brs_ext::get_state(env).m_names.contains(n);
}
backward_rule_set get_backward_rule_set(environment const & env) {
return brs_ext::get_state(env).m_backward_rule_set;
}
backward_rule_set get_backward_rule_sets(environment const & env, io_state const & ios, name const & ns) {
backward_rule_set brs;
list<brs_entry> const * entries = brs_ext::get_entries(env, ns);
if (entries) {
for (auto const & e : *entries) {
default_type_context tctx(env, ios);
brs.insert(tctx, e.m_name, e.m_priority);
}
}
return brs;
}
io_state_stream const & operator<<(io_state_stream const & out, backward_rule_set const & brs) {
options const & opts = out.get_options();
out << "backward rules\n";
brs.for_each([&](head_index const & head_idx, backward_rule const & r) {
out << head_idx << " ==> " << r.get_proof() << "\n";
});
return out;
}
namespace blast {
bool operator==(backward_rule const & r1, backward_rule const & r2) {
return r1.get_proof() == r2.get_proof();
}
void backward_rule_set::insert(type_context & tctx, name const & id, gexpr const & proof, expr const & _thm, unsigned prio) {
expr thm = tctx.whnf(_thm);
while (is_pi(thm)) {
expr local = tctx.mk_tmp_local(binding_domain(thm), binding_info(thm));
thm = tctx.whnf(instantiate(binding_body(thm), local));
}
m_set.insert(head_index(thm), backward_rule(id, proof, prio));
}
void backward_rule_set::insert(type_context & tctx, name const & name, unsigned prio) {
gexpr proof(tctx.env(), name);
declaration const & d = tctx.env().get(name);
insert(tctx, name, proof, d.get_type(), prio);
}
void backward_rule_set::erase(name_set const & ids) {
// This method is not very smart and doesn't use any indexing or caching.
// So, it may be a bottleneck in the future
buffer<pair<head_index, backward_rule> > to_delete;
for_each([&](head_index const & h, backward_rule const & r) {
if (ids.contains(r.get_id())) {
to_delete.push_back(mk_pair(h, r));
}
});
for (auto const & hr : to_delete) {
m_set.erase(hr.first, hr.second);
}
}
void backward_rule_set::erase(name const & id) {
name_set ids;
ids.insert(id);
erase(ids);
}
void backward_rule_set::for_each(std::function<void(head_index const & h, backward_rule const & r)> const & fn) const {
m_set.for_each_entry(fn);
}
list<gexpr> backward_rule_set::find(head_index const & h) const {
list<backward_rule> const * rule_list = m_set.find(h);
if (!rule_list) return list<gexpr>();
return map2<gexpr>(*rule_list, [&](backward_rule const & r) { return r.get_proof(); });
}
void initialize_backward_rule_set() {
g_class_name = new name("brs");
g_key = new std::string("brs");
brs_ext::initialize();
}
void finalize_backward_rule_set() {
brs_ext::finalize();
delete g_key;
delete g_class_name;
}
}
}

68
src/library/blast/backward/backward_rule_set.h Normal file
View file

@ -0,0 +1,68 @@
/*
Copyright (c) 2015 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#pragma once
#include "library/type_context.h"
#include "library/head_map.h"
#include "library/io_state_stream.h"
#include "library/blast/gexpr.h"
#include <vector>
#ifndef LEAN_BACKWARD_DEFAULT_PRIORITY
#define LEAN_BACKWARD_DEFAULT_PRIORITY 1000
#endif
namespace lean {
namespace blast {
class backward_rule {
name m_id;
gexpr m_proof;
unsigned m_priority;
public:
backward_rule(name const & id, gexpr const & proof, unsigned priority):
m_id(id), m_proof(proof), m_priority(priority) {}
name const & get_id() const { return m_id; }
gexpr const & get_proof() const { return m_proof; }
unsigned get_priority() const { return m_priority; }
};
bool operator==(backward_rule const & r1, backward_rule const & r2);
inline bool operator!=(backward_rule const & r1, backward_rule const & r2) { return !operator==(r1, r2); }
struct backward_rule_prio_fn { unsigned operator()(backward_rule const & r) const { return r.get_priority(); } };
class backward_rule_set {
head_map_prio<backward_rule, backward_rule_prio_fn> m_set;
public:
void insert(type_context & tctx, name const & id, gexpr const & proof, expr const & thm, unsigned prio);
void insert(type_context & tctx, name const & name, unsigned prio);
void erase(name_set const & ids);
void erase(name const & id);
void for_each(std::function<void(head_index const & h, backward_rule const & r)> const & fn) const;
list<gexpr> find(head_index const & h) const;
};
void initialize_backward_rule_set();
void finalize_backward_rule_set();
}
environment add_backward_rule(environment const & env, name const & n, unsigned priority, bool persistent);
/** \brief Return true if \c n is an active backward rule in \c env */
bool is_backward_rule(environment const & env, name const & n);
/** \brief Get current backward rule set */
blast::backward_rule_set get_backward_rule_set(environment const & env);
/** \brief Get backward rule set in the given namespace. */
blast::backward_rule_set get_backward_rule_sets(environment const & env, io_state const & ios, name const & ns);
io_state_stream const & operator<<(io_state_stream const & out, blast::backward_rule_set const & r);
}

81
src/library/blast/backward/backward_strategy.cpp Normal file
View file

@ -0,0 +1,81 @@
/*
Copyright (c) 2015 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#include "library/blast/blast.h"
#include "library/blast/trace.h"
#include "library/blast/options.h"
#include "library/blast/choice_point.h"
#include "library/blast/simple_actions.h"
#include "library/blast/proof_expr.h"
#include "library/blast/intros_action.h"
#include "library/blast/no_confusion_action.h"
#include "library/blast/subst_action.h"
#include "library/blast/backward/backward_rule_set.h"
#include "library/blast/backward/backward_action.h"
#include "library/blast/strategy.h"
namespace lean {
namespace blast {
static unsigned g_ext_id = 0;
struct backward_branch_extension : public branch_extension {
backward_rule_set m_backward_rule_set;
backward_branch_extension() {}
backward_branch_extension(backward_branch_extension const & b):
m_backward_rule_set(b.m_backward_rule_set) {}
virtual ~backward_branch_extension() {}
virtual branch_extension * clone() override { return new backward_branch_extension(*this); }
virtual void initialized() override { m_backward_rule_set = ::lean::get_backward_rule_set(env()); }
virtual void hypothesis_activated(hypothesis const & h, hypothesis_idx hidx) override {
m_backward_rule_set.insert(get_type_context(), h.get_name(), gexpr(mk_href(hidx)),
h.get_type(), LEAN_BACKWARD_DEFAULT_PRIORITY);
}
virtual void hypothesis_deleted(hypothesis const & h, hypothesis_idx) override {
m_backward_rule_set.erase(h.get_name());
}
backward_rule_set const & get_backward_rule_set() const { return m_backward_rule_set; }
};
void initialize_backward_strategy() {
g_ext_id = register_branch_extension(new backward_branch_extension());
}
void finalize_backward_strategy() {
}
static backward_branch_extension & get_extension() {
return static_cast<backward_branch_extension&>(curr_state().get_extension(g_ext_id));
}
/** \brief Basic backwards chaining, inspired by Coq's [auto]. */
class backward_strategy : public strategy {
virtual optional<expr> preprocess() override { return none_expr(); }
action_result activate_hypothesis() {
optional<hypothesis_idx> hidx = curr_state().activate_hypothesis();
if (!hidx) return action_result::failed();
trace_action("activate");
Try(assumption_contradiction_actions(*hidx));
Try(subst_action(*hidx));
Try(no_confusion_action(*hidx));
Try(discard_action(*hidx));
return action_result::new_branch();
}
virtual action_result next_action() override {
Try(intros_action());
Try(activate_hypothesis());
Try(trivial_action());
Try(assumption_action());
list<gexpr> backward_rules = get_extension().get_backward_rule_set().find(head_index(curr_state().get_target()));
Try(backward_action(backward_rules, true));
return action_result::failed();
}
};
optional<expr> apply_backward_strategy() {
return backward_strategy()();
}
}}

15
src/library/blast/backward/backward_strategy.h Normal file
View file

@ -0,0 +1,15 @@
/*
Copyright (c) 2015 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.h"
namespace lean {
namespace blast {
optional<expr> apply_backward_strategy();
void initialize_backward_strategy();
void finalize_backward_strategy();
}}

23
src/library/blast/backward/init_module.cpp Normal file
View file

@ -0,0 +1,23 @@
/*
Copyright (c) 2015 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#include "library/blast/backward/init_module.h"
#include "library/blast/backward/backward_rule_set.h"
#include "library/blast/backward/backward_strategy.h"
namespace lean {
namespace blast {
void initialize_backward_module() {
initialize_backward_rule_set();
initialize_backward_strategy();
}
void finalize_backward_module() {
finalize_backward_strategy();
finalize_backward_rule_set();
}
}
}

13
src/library/blast/backward/init_module.h Normal file
View file

@ -0,0 +1,13 @@
/*
Copyright (c) 2015 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#pragma once
namespace lean {
namespace blast {
void initialize_backward_module();
void finalize_backward_module();
}
}

9
src/library/blast/gexpr.cpp
View file

@ -26,4 +26,13 @@ expr gexpr::to_expr(type_context & ctx) const {
expr gexpr::to_expr() const {
return to_expr(get_type_context());
}
bool operator==(gexpr const & ge1, gexpr const & ge2) { return ge1.m_expr == ge2.m_expr; }
std::ostream & operator<<(std::ostream & out, gexpr const & ge) {
out << ge.m_expr;
if (ge.is_universe_polymorphic()) out << " (poly)";
return out;
}
}}

11
src/library/blast/gexpr.h
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include "kernel/expr.h"
#include "library/type_context.h"
#include "library/io_state_stream.h"
namespace lean {
namespace blast {
@ -25,6 +26,8 @@ struct gexpr {
public:
gexpr(name const & n):m_univ_poly(true), m_expr(mk_constant(n)) {}
gexpr(expr const & e):m_univ_poly(false), m_expr(e) {}
gexpr(environment const & env, name const & n):
m_univ_poly(env.get(n).get_univ_params()), m_expr(mk_constant(n)) {}
bool is_universe_polymorphic() const {
return m_univ_poly;
@ -38,5 +41,13 @@ public:
/** \brief Similar to previous method, but uses \c mk_fresh_uref to
create fresh universe meta-variables */
expr to_expr() const;
friend bool operator==(gexpr const & ge1, gexpr const & ge2);
friend std::ostream const & operator<<(std::ostream const & out, gexpr const & ge);
};
bool operator==(gexpr const & ge1, gexpr const & ge2);
inline bool operator!=(gexpr const & ge1, gexpr const & ge2) { return !operator==(ge1, ge2); }
std::ostream & operator<<(std::ostream & out, gexpr const & ge);
}}

3
src/library/blast/init_module.cpp
View file

@ -11,6 +11,7 @@ Author: Leonardo de Moura
#include "library/blast/simplifier.h"
#include "library/blast/options.h"
#include "library/blast/recursor_action.h"
#include "library/blast/backward/init_module.h"
namespace lean {
void initialize_blast_module() {
@ -19,12 +20,14 @@ void initialize_blast_module() {
blast::initialize_state();
initialize_blast();
blast::initialize_simplifier();
blast::initialize_backward_module();
initialize_blast_tactic();
blast::initialize_recursor_action();
}
void finalize_blast_module() {
blast::finalize_recursor_action();
finalize_blast_tactic();
blast::finalize_backward_module();
blast::finalize_simplifier();
finalize_blast();
blast::finalize_state();

12
src/library/blast/simple_strategy.cpp
View file

@ -11,7 +11,8 @@ Author: Leonardo de Moura
#include "library/blast/proof_expr.h"
#include "library/blast/intros_action.h"
#include "library/blast/subst_action.h"
#include "library/blast/backward_action.h"
#include "library/blast/backward/backward_action.h"
#include "library/blast/backward/backward_strategy.h"
#include "library/blast/no_confusion_action.h"
#include "library/blast/simplify_actions.h"
#include "library/blast/recursor_action.h"
@ -43,6 +44,10 @@ class simple_strategy : public strategy {
Return an expression if the goal has been proved during preprocessing step. */
virtual optional<expr> preprocess() {
trace("* Preprocess");
// TODO(dhs): make a branch extension
curr_state().set_simp_rule_sets(get_simp_rule_sets(env()));
while (true) {
if (!failed(intros_action()))
continue;
@ -62,6 +67,11 @@ class simple_strategy : public strategy {
Try(assumption_action());
Try(recursor_action());
Try(constructor_action());
TryStrategy(apply_backward_strategy());
// TODO(Leo): add more actions...
return action_result::failed();
}
};

1
src/library/blast/state.cpp
View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "kernel/replace_fn.h"
#include "library/replace_visitor.h"
#include "library/blast/util.h"
#include "library/blast/blast.h"
#include "library/blast/state.h"
namespace lean {

1
src/library/blast/state.h
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "library/head_map.h"
#include "library/tactic/goal.h"
#include "library/simplifier/simp_rule_set.h"
#include "library/blast/backward/backward_rule_set.h"
#include "library/blast/action_result.h"
#include "library/blast/hypothesis.h"

1
src/library/blast/strategy.cpp
View file

@ -92,7 +92,6 @@ optional<expr> strategy::search() {
scope_choice_points scope1;
curr_state().clear_proof_steps();
m_init_num_choices = get_num_choice_points();
curr_state().set_simp_rule_sets(get_simp_rule_sets(env()));
if (auto pr = invoke_preprocess())
return pr;
if (get_num_choice_points() > m_init_num_choices)

8
src/library/blast/strategy.h
View file

@ -7,6 +7,8 @@ Author: Leonardo de Moura
#pragma once
#include "library/blast/action_result.h"
#include "library/blast/options.h"
#include "library/blast/blast.h"
#include "util/flet.h"
namespace lean {
namespace blast {
@ -31,4 +33,10 @@ public:
strategy();
optional<expr> operator()() { return search(); }
};
#define TryStrategy(Code) {\
flet<state> save_state(curr_state(), curr_state());\
curr_state().clear_proof_steps();\
if (optional<expr> pf = Code) { return action_result::solved(*pf); }\
}
}}

8
src/library/head_map.cpp
View file

@ -33,4 +33,12 @@ int head_index::cmp::operator()(head_index const & i1, head_index const & i2) co
else
return quick_cmp(i1.m_name, i2.m_name);
}
std::ostream & operator<<(std::ostream & out, head_index const & head_idx) {
if (head_idx.m_kind == expr_kind::Constant || head_idx.m_kind == expr_kind::Local)
out << head_idx.m_name;
else
out << head_idx.m_kind;
return out;
}
}

3
src/library/head_map.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include "util/rb_map.h"
#include "util/list.h"
#include "kernel/expr.h"
#include "library/io_state_stream.h"
namespace lean {
struct head_index {
@ -20,6 +21,8 @@ struct head_index {
struct cmp {
int operator()(head_index const & i1, head_index const & i2) const;
};
friend std::ostream & operator<<(std::ostream & out, head_index const & head_idx);
};
/**

6
src/library/io_state_stream.cpp
View file

@ -14,6 +14,12 @@ io_state_stream const & operator<<(io_state_stream const & out, endl_class) {
return out;
}
io_state_stream const & operator<<(io_state_stream const & out, expr_kind const & k) {
options const & opts = out.get_options();
out.get_stream() << k;
return out;
}
io_state_stream const & operator<<(io_state_stream const & out, expr const & e) {
options const & opts = out.get_options();
out.get_stream() << mk_pair(group(out.get_formatter()(e)), opts);

11
tests/lean/backward_rule1.lean Normal file
View file

@ -0,0 +1,11 @@
constants (A B C : Prop) (H : A → B) (G : A → B → C)
constants (T : Type) (f : T → A)
attribute H [backward]
attribute G [backward]
attribute f [backward]
print H
print G
print f
print [backward]

7
tests/lean/backward_rule1.lean.expected.out Normal file
View file

@ -0,0 +1,7 @@
constant H [backward] : A → B
constant G [backward] : A → B → C
constant f [backward] : T → A
backward rules
B ==> H
A ==> f (poly)
C ==> G

17
tests/lean/run/blast18.lean Normal file
View file

@ -0,0 +1,17 @@
-- Backward chaining with tagged rules
constants {P Q R S T U : Prop} (Hpq : P → Q) (Hqr : Q → R) (Hrs : R → S) (Hst : S → T)
constants (Huq : U → Q) (Hur : U → R) (Hus : U → S) (Hut : U → T)
attribute Hpq [backward]
attribute Hqr [backward]
attribute Hrs [backward]
attribute Hst [backward]
attribute Huq [backward]
attribute Hur [backward]
attribute Hus [backward]
attribute Hut [backward]
definition lemma1 (p : P) : Q := by blast
definition lemma2 (p : P) : R := by blast
definition lemma3 (p : P) : S := by blast
definition lemma4 (p : P) : T := by blast

12
tests/lean/run/blast19.lean Normal file
View file

@ -0,0 +1,12 @@
-- Backward chaining with hypotheses
constants {P Q R S T U : Prop}
constants (Huq : U → Q) (Hur : U → R) (Hus : U → S) (Hut : U → T)
attribute Huq [backward]
attribute Hur [backward]
attribute Hus [backward]
attribute Hut [backward]
definition lemma1 : (P → Q) → P → Q := by blast
definition lemma2 : (P → Q) → (Q → R) → P → R := by blast
definition lemma3 : (P → Q) → (Q → R) → (R → S) → P → S := by blast
definition lemma4 : (P → Q) → (Q → R) → (R → S) → (S → T) → P → T := by blast