feat(library/congr_lemma_manager): add mk_congr_simp that takes the number of expected arguments
Use sorry to be able to test first part
This commit is contained in:
parent
5a48a2cebe
commit
8a7321714a
3 changed files with 52 additions and 12 deletions
|
@ -1291,10 +1291,11 @@ static environment congr_lemma_cmd(parser & p) {
|
|||
auto r = cm.mk_congr_simp(e);
|
||||
if (!r)
|
||||
throw parser_error("failed to generated congruence lemma", pos);
|
||||
p.regular_stream() << r->first << "\n";;
|
||||
p.regular_stream() << r->get_proof() << "\n:\n" << r->get_type() << "\n";;
|
||||
type_checker tc(env);
|
||||
expr type = tc.check(r->first, ls).first;
|
||||
p.regular_stream() << type << "\n";
|
||||
expr type = tc.check(r->get_proof(), ls).first;
|
||||
if (!tc.is_def_eq(type, r->get_type()).first)
|
||||
throw parser_error("congruence lemma reported type does not match given type", pos);
|
||||
return env;
|
||||
}
|
||||
|
||||
|
|
|
@ -16,7 +16,25 @@ class congr_lemma_manager::imp {
|
|||
app_builder & m_builder;
|
||||
fun_info_manager & m_fmanager;
|
||||
type_context & m_ctx;
|
||||
expr_map<result> m_cache;
|
||||
struct key {
|
||||
expr const & m_fn;
|
||||
unsigned m_nargs;
|
||||
unsigned m_hash;
|
||||
key(expr const & fn, unsigned nargs):
|
||||
m_fn(fn), m_nargs(nargs), m_hash(hash(m_fn.hash(), m_nargs)) {}
|
||||
};
|
||||
|
||||
struct key_hash_fn {
|
||||
unsigned operator()(key const & k) const { return k.m_hash; }
|
||||
};
|
||||
|
||||
struct key_eq_fn {
|
||||
bool operator()(key const & k1, key const & k2) const {
|
||||
return k1.m_fn == k2.m_fn && k1.m_nargs == k2.m_nargs;
|
||||
}
|
||||
};
|
||||
|
||||
std::unordered_map<key, result, key_hash_fn, key_eq_fn> m_cache;
|
||||
|
||||
struct failure {
|
||||
unsigned m_arg_idx;
|
||||
|
@ -133,10 +151,11 @@ class congr_lemma_manager::imp {
|
|||
auto eq = m_builder.mk_eq(lhs, rhs);
|
||||
if (!eq)
|
||||
return optional<result>();
|
||||
expr congr_type = Pi(hyps, *eq);
|
||||
std::cout << congr_type << "\n";
|
||||
// TODO(Leo): create proof
|
||||
lean_unreachable();
|
||||
expr congr_type = Pi(hyps, *eq);
|
||||
auto congr_proof = m_builder.mk_sorry(congr_type);
|
||||
if (!congr_proof)
|
||||
return optional<result>();
|
||||
return optional<result>(congr_type, *congr_proof, to_list(kinds));
|
||||
}
|
||||
|
||||
public:
|
||||
|
@ -144,10 +163,15 @@ public:
|
|||
m_builder(b), m_fmanager(fm), m_ctx(fm.ctx()) {}
|
||||
|
||||
optional<result> mk_congr_simp(expr const & fn) {
|
||||
auto r = m_cache.find(fn);
|
||||
fun_info finfo = m_fmanager.get(fn);
|
||||
return mk_congr_simp(fn, finfo.get_arity());
|
||||
}
|
||||
|
||||
optional<result> mk_congr_simp(expr const & fn, unsigned nargs) {
|
||||
auto r = m_cache.find(key(fn, nargs));
|
||||
if (r != m_cache.end())
|
||||
return optional<result>(r->second);
|
||||
fun_info finfo = m_fmanager.get(fn);
|
||||
fun_info finfo = m_fmanager.get(fn, nargs);
|
||||
list<unsigned> const & result_deps = finfo.get_dependencies();
|
||||
buffer<congr_arg_kind> kinds;
|
||||
buffer<param_info> pinfos;
|
||||
|
@ -179,7 +203,7 @@ public:
|
|||
try {
|
||||
auto new_r = mk_congr_simp(fn, pinfos, kinds);
|
||||
if (new_r)
|
||||
m_cache.insert(mk_pair(fn, *new_r));
|
||||
m_cache.insert(mk_pair(key(fn, nargs), *new_r));
|
||||
return new_r;
|
||||
} catch (failure & ex) {
|
||||
kinds[ex.m_arg_idx] = congr_arg_kind::Fixed;
|
||||
|
@ -198,4 +222,7 @@ congr_lemma_manager::~congr_lemma_manager() {
|
|||
auto congr_lemma_manager::mk_congr_simp(expr const & fn) -> optional<result> {
|
||||
return m_ptr->mk_congr_simp(fn);
|
||||
}
|
||||
auto congr_lemma_manager::mk_congr_simp(expr const & fn, unsigned nargs) -> optional<result> {
|
||||
return m_ptr->mk_congr_simp(fn, nargs);
|
||||
}
|
||||
}
|
||||
|
|
|
@ -19,7 +19,19 @@ public:
|
|||
|
||||
enum class congr_arg_kind { Fixed, Eq, Cast };
|
||||
|
||||
typedef pair<expr, list<congr_arg_kind>> result;
|
||||
class result {
|
||||
expr m_type;
|
||||
expr m_proof;
|
||||
list<congr_arg_kind> m_arg_kinds;
|
||||
public:
|
||||
result(expr const & type, expr const & proof, list<congr_arg_kind> const & ks):
|
||||
m_type(type), m_proof(proof), m_arg_kinds(ks) {}
|
||||
expr const & get_type() const { return m_type; }
|
||||
expr const & get_proof() const { return m_proof; }
|
||||
list<congr_arg_kind> const & get_arg_kinds() const { return m_arg_kinds; }
|
||||
};
|
||||
|
||||
optional<result> mk_congr_simp(expr const & fn);
|
||||
optional<result> mk_congr_simp(expr const & fn, unsigned nargs);
|
||||
};
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue