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

refactor(library): remove abstract_expr and abstract_expr_manager modules

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-24 15:16:57 -07:00
parent 3912da372a
commit 490a116baa
13 changed files with 3 additions and 789 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/CMakeLists.txt
View file

@ -13,7 +13,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
aux_recursors.cpp norm_num.cpp trace.cpp
attribute_manager.cpp error_handling.cpp unification_hint.cpp
local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp lazy_abstraction.cpp
fun_info.cpp congr_lemma.cpp abstract_expr.cpp defeq_canonizer.cpp
fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp
# Legacy -- The following files will be eventually deleted
normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp
unifier.cpp match.cpp class_instance_resolution.cpp old_type_context.cpp
@ -21,6 +21,6 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
old_util.cpp let.cpp metavar_closure.cpp old_local_context.cpp choice_iterator.cpp
tmp_type_context.cpp
# abstract_expr_manager.cpp light_lt_manager.cpp
# light_lt_manager.cpp
# proof_irrel_expr_manager.cpp
)

316
src/library/abstract_expr.cpp
View file

@ -1,316 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/hash.h"
#include "util/interrupt.h"
#include "kernel/expr_maps.h"
#include "kernel/instantiate.h"
#include "library/abstract_expr.h"
#include "library/cache_helper.h"
#include "library/fun_info.h"
namespace lean {
struct abstract_expr_cache {
environment m_env;
expr_map<unsigned> m_hash_cache;
expr_map<unsigned> m_weight_cache;
abstract_expr_cache(environment const & env):m_env(env) {}
environment const & env() const { return m_env; }
};
/* The abstract_expr_cache does not depend on the transparency mode */
typedef transparencyless_cache_compatibility_helper<abstract_expr_cache>
abstract_expr_cache_helper;
MK_THREAD_LOCAL_GET_DEF(abstract_expr_cache_helper, get_aech);
abstract_expr_cache & get_abstract_cache_for(type_context const & ctx) {
return get_aech().get_cache_for(ctx);
}
#define EASY_HASH(e) { \
switch (e.kind()) { \
case expr_kind::Constant: case expr_kind::Local: \
case expr_kind::Meta: case expr_kind::Sort: \
case expr_kind::Var: \
return e.hash(); \
default: \
break; \
} \
}
struct abstract_fn {
type_context & m_ctx;
buffer<expr> m_locals;
type_context::transparency_scope m_scope;
static void check_system() { ::lean::check_system("abstract expression operator"); }
abstract_fn(type_context & ctx):
m_ctx(ctx),
m_scope(m_ctx, transparency_mode::All) {}
expr instantiate_locals(expr const & e) {
return instantiate_rev(e, m_locals.size(), m_locals.data());
}
expr push_local(name const & pp_name, expr const & type) {
expr l = m_ctx.push_local(pp_name, instantiate_locals(type));
m_locals.push_back(l);
return l;
}
expr push_let(name const & pp_name, expr const & type, expr const & value) {
expr l = m_ctx.push_let(pp_name, instantiate_locals(type), instantiate_locals(value));
m_locals.push_back(l);
return l;
}
void pop() {
m_locals.pop_back();
}
};
struct abstract_hash_fn : public abstract_fn {
expr_map<unsigned> & m_cache;
abstract_hash_fn(type_context & ctx):
abstract_fn(ctx),
m_cache(get_abstract_cache_for(ctx).m_hash_cache) {
}
unsigned hash(expr const & e) {
EASY_HASH(e);
auto it = m_cache.find(e);
if (it != m_cache.end())
return it->second;
check_system();
unsigned r = 0;
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Local:
case expr_kind::Meta: case expr_kind::Sort:
case expr_kind::Var:
lean_unreachable();
case expr_kind::Lambda:
case expr_kind::Pi:
r = hash(binding_domain(e));
push_local(binding_name(e), binding_domain(e));
r = ::lean::hash(r, hash(binding_body(e)));
pop();
break;
case expr_kind::Let:
r = ::lean::hash(hash(let_type(e)), hash(let_value(e)));
push_let(let_name(e), let_type(e), let_value(e));
r = ::lean::hash(r, hash(let_body(e)));
pop();
break;
case expr_kind::Macro:
r = lean::hash(macro_num_args(e), [&](unsigned i) { return hash(macro_arg(e, i)); },
macro_def(e).hash());
break;
case expr_kind::App:
buffer<expr> args;
expr const & f = get_app_args(e, args);
r = hash(f);
fun_info info = get_fun_info(m_ctx, instantiate_locals(f), args.size());
unsigned i = 0;
for (param_info const & pinfo : info.get_params_info()) {
lean_assert(i < args.size());
if (!pinfo.is_inst_implicit() && !pinfo.is_prop()) {
r = ::lean::hash(r, hash(args[i]));
}
i++;
}
/* Remark: the property (i == args.size()) does not necessarily hold here.
This can happen whenever the arity of f depends on its arguments. */
break;
}
m_cache.insert(mk_pair(e, r));
return r;
}
unsigned operator()(expr const & e) {
return hash(e);
}
};
unsigned abstract_hash(type_context & ctx, expr const & e) {
EASY_HASH(e);
return abstract_hash_fn(ctx)(e);
}
#define EASY_WEIGHT(e) { \
switch (e.kind()) { \
case expr_kind::Constant: case expr_kind::Local: \
case expr_kind::Meta: case expr_kind::Sort: \
case expr_kind::Var: \
return 1; \
default: \
break; \
} \
}
/* TODO(Leo): this class is too similar to abstract_hash_fn, both are folding expr.
We should try to merge both implementations. */
struct abstract_weight_fn : public abstract_fn {
expr_map<unsigned> & m_cache;
abstract_weight_fn(type_context & ctx):
abstract_fn(ctx),
m_cache(get_abstract_cache_for(ctx).m_weight_cache) {}
unsigned weight(expr const & e) {
EASY_WEIGHT(e);
auto it = m_cache.find(e);
if (it != m_cache.end())
return it->second;
check_system();
unsigned r = 0;
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Local:
case expr_kind::Meta: case expr_kind::Sort:
case expr_kind::Var:
lean_unreachable();
case expr_kind::Lambda:
case expr_kind::Pi:
r = weight(binding_domain(e));
push_local(binding_name(e), binding_domain(e));
r += weight(binding_body(e));
pop();
break;
case expr_kind::Let:
r = weight(let_type(e));
r += weight(let_value(e));
push_let(let_name(e), let_type(e), let_value(e));
r += weight(let_body(e));
pop();
break;
case expr_kind::Macro:
r = 0;
for (unsigned i = 0; i < macro_num_args(e); i++)
r += weight(macro_arg(e, i));
break;
case expr_kind::App:
buffer<expr> args;
expr const & f = get_app_args(e, args);
r = weight(f);
fun_info info = get_fun_info(m_ctx, instantiate_locals(f), args.size());
unsigned i = 0;
for (param_info const & pinfo : info.get_params_info()) {
lean_assert(i < args.size());
if (!pinfo.is_inst_implicit() && !pinfo.is_prop()) {
r += weight(args[i]);
}
i++;
}
/* Remark: the property (i == args.size()) does not necessarily hold here.
This can happen whenever the arity of f depends on its arguments. */
break;
}
m_cache.insert(mk_pair(e, r));
return r;
}
unsigned operator()(expr const & e) {
return weight(e);
}
};
unsigned abstract_weight(type_context & ctx, expr const & e) {
EASY_WEIGHT(e);
return abstract_weight_fn(ctx)(e);
}
struct abstract_eq_fn : public abstract_fn {
abstract_eq_fn(type_context & ctx):
abstract_fn(ctx) {}
bool equal(expr const & a, expr const & b) {
if (is_eqp(a, b))
return true;
if (abstract_hash(m_ctx, a) != abstract_hash(m_ctx, b))
return false;
if (a.kind() != b.kind())
return false;
switch (a.kind()) {
case expr_kind::Var:
case expr_kind::Constant:
case expr_kind::Meta:
case expr_kind::Sort:
case expr_kind::Local:
return a == b;
case expr_kind::Lambda:
case expr_kind::Pi:
check_system();
if (!equal(binding_domain(a), binding_domain(b)))
return false;
push_local(binding_name(a), binding_domain(a));
if (!equal(binding_body(a), binding_body(b)))
return false;
pop();
return true;
case expr_kind::Let:
check_system();
if (!equal(let_type(a), let_type(b)) ||
!equal(let_value(a), let_value(b)))
return false;
push_let(let_name(a), let_type(a), let_value(a));
if (!equal(let_body(a), let_body(b)))
return false;
pop();
return true;
case expr_kind::Macro:
if (macro_def(a) != macro_def(b) || macro_num_args(a) != macro_num_args(b))
return false;
check_system();
for (unsigned i = 0; i < macro_num_args(a); i++) {
if (!equal(macro_arg(a, i), macro_arg(b, i)))
return false;
}
return true;
case expr_kind::App:
check_system();
buffer<expr> a_args;
buffer<expr> b_args;
expr const & a_fn = get_app_args(a, a_args);
expr const & b_fn = get_app_args(b, b_args);
if (a_args.size() != b_args.size() ||
!equal(a_fn, b_fn))
return false;
fun_info info = get_fun_info(m_ctx, instantiate_locals(a_fn), a_args.size());
unsigned i = 0;
for (param_info const & pinfo : info.get_params_info()) {
lean_assert(i < a_args.size());
lean_assert(i < b_args.size());
if (!pinfo.is_inst_implicit() && !pinfo.is_prop() && !equal(a_args[i], b_args[i]))
return false;
i++;
}
/* Remark: the property (i == a_args.size()) does not necessarily hold here.
This can happen whenever the arity of f depends on its arguments. */
return true;
}
lean_unreachable(); // LCOV_EXCL_LINE
}
bool operator()(expr const & a, expr const & b) {
return equal(a, b);
}
};
bool abstract_eq(type_context & ctx, expr const & a, expr const & b) {
if (is_eqp(a, b))
return true;
return abstract_eq_fn(ctx)(a, b);
}
}

24
src/library/abstract_expr.h
View file

@ -1,24 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/type_context.h"
namespace lean {
/** \brief Return a hash code for \c e that ignores instance parameters
(and proofs) in \c e.
Example: the following two instances have the same hashcode
(@add nat nat_has_add a b)
(@add nat (add_monoid_has_add nat nat_is_monoid) a b) */
unsigned abstract_hash(type_context & ctx, expr const & e);
/** \brief Weight function that ignores the type class instances in \c e. */
unsigned abstract_weight(type_context & ctx, expr const & e);
/** \brief Equality function that ignores type class instances. */
bool abstract_eq(type_context & ctx, expr const & e1, expr const & e2);
/** \brief Less than function that ignores type class instances. */
bool abstract_lt(type_context & ctx, expr const & e1, expr const & e2);
}

141
src/library/abstract_expr_manager.cpp
View file

@ -1,141 +0,0 @@
/*
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/abstract_expr_manager.h"
#include "kernel/instantiate.h"
#include "util/safe_arith.h"
#include "util/list_fn.h"
namespace lean {
unsigned abstract_expr_manager::hash(expr const & e) {
unsigned h;
switch (e.kind()) {
case expr_kind::Constant:
case expr_kind::Local:
case expr_kind::Meta:
case expr_kind::Sort:
case expr_kind::Var:
case expr_kind::Macro:
return e.hash();
case expr_kind::Lambda:
case expr_kind::Pi:
h = hash(binding_domain(e));
// Remark binding_domain(e) may contain de-bruijn variables.
// We can instantiate them eagerly as we do here, or lazily.
// The lazy approach is potentially more efficient, but we would have
// to use something more sophisticated than an instantiate_rev at expr_kind::App
m_locals.push_back(instantiate_rev(m_tctx.mk_tmp_local(binding_domain(e)), m_locals.size(), m_locals.data()));
h = ::lean::hash(h, hash(binding_body(e)));
m_locals.pop_back();
return h;
case expr_kind::Let:
// Let-expressions must be unfolded before invoking this method
lean_unreachable();
case expr_kind::App:
buffer<expr> args;
expr const & f = get_app_args(e, args);
unsigned prefix_sz = m_congr_lemma_manager.get_specialization_prefix_size(instantiate_rev(f, m_locals.size(), m_locals.data()), args.size());
expr new_f = e;
unsigned rest_sz = args.size() - prefix_sz;
for (unsigned i = 0; i < rest_sz; i++)
new_f = app_fn(new_f);
new_f = instantiate_rev(new_f, m_locals.size(), m_locals.data());
optional<congr_lemma> congr = m_congr_lemma_manager.mk_congr(new_f, rest_sz);
h = hash(new_f);
if (!congr) {
for (unsigned i = prefix_sz; i < args.size(); i++) {
h = ::lean::hash(h, hash(args[i]));
}
} else {
lean_assert(length(congr->get_arg_kinds()) == rest_sz);
unsigned i = prefix_sz;
for_each(congr->get_arg_kinds(), [&](congr_arg_kind const & c_kind) {
if (c_kind != congr_arg_kind::Cast) {
h = ::lean::hash(h, hash(args[i]));
}
i++;
});
}
return h;
}
lean_unreachable();
}
bool abstract_expr_manager::is_equal(expr const & a, expr const & b) {
if (is_eqp(a, b)) return true;
if (a.kind() != b.kind()) return false;
if (is_var(a)) return var_idx(a) == var_idx(b);
bool is_eq;
switch (a.kind()) {
case expr_kind::Var:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Constant: case expr_kind::Sort:
return a == b;
case expr_kind::Meta: case expr_kind::Local:
return mlocal_name(a) == mlocal_name(b) && is_equal(mlocal_type(a), mlocal_type(b));
case expr_kind::Lambda: case expr_kind::Pi:
if (!is_equal(binding_domain(a), binding_domain(b))) return false;
// see comment at abstract_expr_manager::hash
m_locals.push_back(instantiate_rev(m_tctx.mk_tmp_local(binding_domain(a)), m_locals.size(), m_locals.data()));
is_eq = is_equal(binding_body(a), binding_body(b));
m_locals.pop_back();
return is_eq;
case expr_kind::Let:
// Let-expressions must be unfolded before invoking this method
lean_unreachable();
case expr_kind::Macro:
if (macro_def(a) != macro_def(b) || macro_num_args(a) != macro_num_args(b))
return false;
for (unsigned i = 0; i < macro_num_args(a); i++) {
if (!is_equal(macro_arg(a, i), macro_arg(b, i)))
return false;
}
return true;
case expr_kind::App:
buffer<expr> a_args, b_args;
expr const & f_a = get_app_args(a, a_args);
expr const & f_b = get_app_args(b, b_args);
if (!is_equal(f_a, f_b))
return false;
if (a_args.size() != b_args.size())
return false;
unsigned prefix_sz = m_congr_lemma_manager.get_specialization_prefix_size(instantiate_rev(f_a, m_locals.size(), m_locals.data()), a_args.size());
for (unsigned i = 0; i < prefix_sz; i++) {
if (!is_equal(a_args[i], b_args[i]))
return false;
}
expr new_f_a = a;
unsigned rest_sz = a_args.size() - prefix_sz;
for (unsigned i = 0; i < rest_sz; i++) {
new_f_a = app_fn(new_f_a);
}
new_f_a = instantiate_rev(new_f_a, m_locals.size(), m_locals.data());
optional<congr_lemma> congr = m_congr_lemma_manager.mk_congr(new_f_a, rest_sz);
bool not_equal = false;
if (!congr) {
for (unsigned i = prefix_sz; i < a_args.size(); ++i) {
if (!is_equal(a_args[i], b_args[i])) {
not_equal = true;
break;
}
}
} else {
lean_assert(length(congr->get_arg_kinds()) == rest_sz);
unsigned i = prefix_sz;
for_each(congr->get_arg_kinds(), [&](congr_arg_kind const & c_kind) {
if (not_equal)
return;
if (c_kind != congr_arg_kind::Cast && !is_equal(a_args[i], b_args[i])) {
not_equal = true;
}
i++;
});
}
return !not_equal;
}
lean_unreachable(); // LCOV_EXCL_LINE
}
}

31
src/library/abstract_expr_manager.h
View file

@ -1,31 +0,0 @@
/*
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 <vector>
#include "kernel/expr.h"
#include "library/old_type_context.h"
#include "library/congr_lemma_manager.h"
namespace lean {
/** \brief Abstract expression manager, to allow comparing expressions while ignoring subsingletons. */
class abstract_expr_manager {
/* The [congr_lemma_manager] cannot handle [Var]s since it needs to infer types, and we do not
want to instantiate eagerly for performance reasons. Therefore we track the context ourselves,
and only instantiate on the expressions we pass to the [congr_lemma_manager], which we
expect to be very small in general. */
std::vector<expr> m_locals;
old_type_context & m_tctx;
congr_lemma_manager & m_congr_lemma_manager;
public:
abstract_expr_manager(congr_lemma_manager & c_lemma_manager):
m_tctx(c_lemma_manager.ctx()), m_congr_lemma_manager(c_lemma_manager) {}
unsigned hash(expr const & e);
bool is_equal(expr const & a, expr const & b);
};
}

126
src/library/proof_irrel_expr_manager.cpp
View file

@ -1,126 +0,0 @@
/*
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/proof_irrel_expr_manager.h"
#include "kernel/instantiate.h"
#include "util/safe_arith.h"
#include "util/list_fn.h"
namespace lean {
unsigned proof_irrel_expr_manager::hash(expr const & e) {
unsigned h;
switch (e.kind()) {
case expr_kind::Constant:
case expr_kind::Local:
case expr_kind::Meta:
case expr_kind::Sort:
case expr_kind::Var:
case expr_kind::Macro:
return e.hash();
case expr_kind::Let:
// Let-expressions must be unfolded before invoking this method
lean_unreachable();
case expr_kind::Lambda:
case expr_kind::Pi:
h = hash(binding_domain(e));
// Remark binding_domain(e) may contain de-bruijn variables.
// We can instantiate them eagerly as we do here, or lazily.
// The lazy approach is potentially more efficient, but we would have
// to use something more sophisticated than an instantiate_rev at expr_kind::App
m_locals.push_back(instantiate_rev(m_tctx.mk_tmp_local(binding_domain(e)), m_locals.size(), m_locals.data()));
h = ::lean::hash(h, hash(binding_body(e)));
m_locals.pop_back();
return h;
case expr_kind::App:
buffer<expr> args;
expr const & f = get_app_args(e, args);
unsigned prefix_sz = m_fun_info_manager.get_specialization_prefix_size(instantiate_rev(f, m_locals.size(), m_locals.data()), args.size());
expr new_f = e;
unsigned rest_sz = args.size() - prefix_sz;
for (unsigned i = 0; i < rest_sz; i++)
new_f = app_fn(new_f);
new_f = instantiate_rev(new_f, m_locals.size(), m_locals.data());
h = hash(new_f);
fun_info info = m_fun_info_manager.get(new_f, rest_sz);
lean_assert(length(info.get_params_info()) == rest_sz);
unsigned i = prefix_sz;
for_each(info.get_params_info(), [&](param_info const & p_info) {
if (!p_info.is_prop()) {
h = ::lean::hash(h, hash(args[i]));
}
i++;
});
return h;
}
lean_unreachable();
}
bool proof_irrel_expr_manager::is_equal(expr const & a, expr const & b) {
if (is_eqp(a, b)) return true;
if (a.kind() != b.kind()) return false;
if (is_var(a)) return var_idx(a) == var_idx(b);
bool is_eq;
switch (a.kind()) {
case expr_kind::Var:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Constant: case expr_kind::Sort:
return a == b;
case expr_kind::Meta: case expr_kind::Local:
return mlocal_name(a) == mlocal_name(b) && is_equal(mlocal_type(a), mlocal_type(b));
case expr_kind::Let:
// Let-expressions must be unfolded before invoking this method
lean_unreachable();
case expr_kind::Lambda: case expr_kind::Pi:
if (!is_equal(binding_domain(a), binding_domain(b))) return false;
// see comment at proof_irrel_expr_manager::hash
m_locals.push_back(instantiate_rev(m_tctx.mk_tmp_local(binding_domain(a)), m_locals.size(), m_locals.data()));
is_eq = is_equal(binding_body(a), binding_body(b));
m_locals.pop_back();
return is_eq;
case expr_kind::Macro:
if (macro_def(a) != macro_def(b) || macro_num_args(a) != macro_num_args(b))
return false;
for (unsigned i = 0; i < macro_num_args(a); i++) {
if (!is_equal(macro_arg(a, i), macro_arg(b, i)))
return false;
}
return true;
case expr_kind::App:
buffer<expr> a_args, b_args;
expr const & f_a = get_app_args(a, a_args);
expr const & f_b = get_app_args(b, b_args);
if (!is_equal(f_a, f_b))
return false;
if (a_args.size() != b_args.size())
return false;
unsigned prefix_sz = m_fun_info_manager.get_specialization_prefix_size(instantiate_rev(f_a, m_locals.size(), m_locals.data()), a_args.size());
for (unsigned i = 0; i < prefix_sz; i++) {
if (!is_equal(a_args[i], b_args[i]))
return false;
}
expr new_f_a = a;
unsigned rest_sz = a_args.size() - prefix_sz;
for (unsigned i = 0; i < rest_sz; i++) {
new_f_a = app_fn(new_f_a);
}
new_f_a = instantiate_rev(new_f_a, m_locals.size(), m_locals.data());
fun_info info = m_fun_info_manager.get(new_f_a, rest_sz);
bool not_equal = false;
lean_assert(length(info.get_params_info()) == rest_sz);
unsigned i = prefix_sz;
for_each(info.get_params_info(), [&](param_info const & p_info) {
if (not_equal)
return;
if (!p_info.is_prop() && !is_equal(a_args[i], b_args[i])) {
not_equal = true;
}
i++;
});
return !not_equal;
}
lean_unreachable(); // LCOV_EXCL_LINE
}
}

31
src/library/proof_irrel_expr_manager.h
View file

@ -1,31 +0,0 @@
/*
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 <vector>
#include "kernel/expr.h"
#include "library/old_type_context.h"
#include "library/fun_info_manager.h"
namespace lean {
/** \brief Proof-irrelevant expression manager, to allow comparing expressions while ignoring proofs. */
class proof_irrel_expr_manager {
/* The [fun_info_manager] cannot handle [Var]s since it needs to infer types, and we do not
want to instantiate eagerly for performance reasons. Therefore we track the context ourselves,
and only instantiate on the expressions we pass to the [fun_info_manager], which we
expect to be very small in general. */
std::vector<expr> m_locals;
old_type_context & m_tctx;
fun_info_manager & m_fun_info_manager;
public:
proof_irrel_expr_manager(fun_info_manager & f_info_manager):
m_tctx(f_info_manager.ctx()), m_fun_info_manager(f_info_manager) {}
unsigned hash(expr const & e);
bool is_equal(expr const & a, expr const & b);
};
}

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

@ -2,5 +2,5 @@ add_library(tactic OBJECT tactic_state.cpp intro_tactic.cpp
revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp
app_builder_tactics.cpp subst_tactic.cpp exact_tactic.cpp
change_tactic.cpp assert_tactic.cpp apply_tactic.cpp
fun_info_tactics.cpp congr_lemma_tactics.cpp abstract_expr_tactics.cpp
fun_info_tactics.cpp congr_lemma_tactics.cpp
elaborate.cpp init_module.cpp)

38
src/library/tactic/abstract_expr_tactics.cpp
View file

@ -1,38 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/abstract_expr.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_nat.h"
#include "library/tactic/tactic_state.h"
namespace lean {
vm_obj tactic_abstract_hash(vm_obj const & e, vm_obj const & s) {
type_context_scope ctx(s);
unsigned h = abstract_hash(ctx, to_expr(e)) % LEAN_MAX_SMALL_NAT;
return mk_tactic_success(mk_vm_simple(h), to_tactic_state(s));
}
vm_obj tactic_abstract_weight(vm_obj const & e, vm_obj const & s) {
type_context_scope ctx(s);
unsigned h = abstract_weight(ctx, to_expr(e)) % LEAN_MAX_SMALL_NAT;
return mk_tactic_success(mk_vm_simple(h), to_tactic_state(s));
}
vm_obj tactic_abstract_eq(vm_obj const & e1, vm_obj const & e2, vm_obj const & s) {
type_context_scope ctx(s);
bool r = abstract_eq(ctx, to_expr(e1), to_expr(e2));
return mk_tactic_success(mk_vm_bool(r), to_tactic_state(s));
}
void initialize_abstract_expr_tactics() {
DECLARE_VM_BUILTIN(name({"tactic", "abstract_hash"}), tactic_abstract_hash);
DECLARE_VM_BUILTIN(name({"tactic", "abstract_weight"}), tactic_abstract_weight);
DECLARE_VM_BUILTIN(name({"tactic", "abstract_eq"}), tactic_abstract_eq);
}
void finalize_abstract_expr_tactics() {
}
}

11
src/library/tactic/abstract_expr_tactics.h
View file

@ -1,11 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
namespace lean {
void initialize_abstract_expr_tactics();
void finalize_abstract_expr_tactics();
}

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

@ -17,7 +17,6 @@ Author: Leonardo de Moura
#include "library/tactic/apply_tactic.h"
#include "library/tactic/fun_info_tactics.h"
#include "library/tactic/congr_lemma_tactics.h"
#include "library/tactic/abstract_expr_tactics.h"
#include "library/tactic/elaborate.h"
#include "library/tactic/defeq_simplifier/init_module.h"
@ -36,14 +35,12 @@ void initialize_tactic_module() {
initialize_apply_tactic();
initialize_fun_info_tactics();
initialize_congr_lemma_tactics();
initialize_abstract_expr_tactics();
initialize_elaborate();
initialize_defeq_simplifier_module();
}
void finalize_tactic_module() {
finalize_defeq_simplifier_module();
finalize_elaborate();
finalize_abstract_expr_tactics();
finalize_congr_lemma_tactics();
finalize_fun_info_tactics();
finalize_apply_tactic();

35
tests/lean/run/ahash1.lean
View file

@ -1,35 +0,0 @@
open tactic bool
constant nat_has_add1 : has_add nat
constant nat_has_add2 : has_add nat
example (a b : nat)
(H1 : @add nat nat_has_add1 a b = 0)
(H2 : @add nat nat_has_add2 a b = 0)
(H3 : @add nat nat_has_add1 b a = 0)
: true :=
by do
h₁ ← get_local "H1" >>= infer_type >>= abstract_hash,
h₂ ← get_local "H2" >>= infer_type >>= abstract_hash,
h₃ ← get_local "H3" >>= infer_type >>= abstract_hash,
trace $ to_string h₁ + " " + to_string h₂ + " " + to_string h₃,
if h₁ ≠ h₂ then fail "ERROR" else skip,
if h₁ = h₃ then fail "UNEXPECTED" else skip,
constructor
example (a b : nat)
(H1 : ∀ d c : nat, @add nat nat_has_add1 a b = c + d)
(H2 : ∀ d c : nat, @add nat nat_has_add2 a b = c + d)
(H3 : ∀ d c : nat, @add nat nat_has_add1 a b = d + d)
: true :=
by do
get_local "H1" >>= infer_type >>= abstract_hash >>= trace,
get_local "H2" >>= infer_type >>= abstract_hash >>= trace,
H1 ← get_local "H1" >>= infer_type,
H2 ← get_local "H2" >>= infer_type,
H3 ← get_local "H3" >>= infer_type,
abstract_eq H1 H2 >>= trace,
abstract_eq H1 H3 >>= trace,
abstract_eq H1 H2 >>= (λ b, when (b = ff) (fail "ERROR1")),
abstract_eq H1 H3 >>= (λ b, when (b = tt) (fail "ERROR2")),
constructor

30
tests/lean/run/aweight1.lean
View file

@ -1,30 +0,0 @@
import data.nat
open tactic nat decidable
constant nat_has_add1 : has_add nat
constant nat_has_add2 : nat → has_add nat
constant foo (a : nat) : a > 0 → Prop
set_option pp.all true
example (a b : nat)
(H1 : @add nat nat_has_add1 a b = 0)
(H2 : @add nat (nat_has_add2 (0 + a + b)) a b = 0)
(H3 : @add nat nat_has_add1 b (a + b) = 0)
(H4 : foo (succ (succ (succ zero))) dec_trivial)
(H5 : foo (succ (succ (succ zero))) sorry)
: true :=
by do
h₁ ← get_local "H1" >>= infer_type >>= abstract_weight,
h₂ ← get_local "H2" >>= infer_type >>= abstract_weight,
h₃ ← get_local "H3" >>= infer_type >>= abstract_weight,
h₄ ← get_local "H4" >>= infer_type >>= abstract_weight,
h₅ ← get_local "H5" >>= infer_type >>= abstract_weight,
trace $ to_string h₁ + " " + to_string h₂ + " " + to_string h₃,
trace $ to_string h₄ + " " + to_string h₅,
get_local "H4" >>= infer_type >>= trace,
get_local "H5" >>= infer_type >>= trace,
if h₁ ≠ h₂ then fail "ERROR" else skip,
if h₁ = h₃ then fail "ERROR" else skip,
constructor