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

refactor(library/unifier): move m_pattern configuration option to unifier_config

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-03 20:24:18 -08:00
parent 341a9a2010
commit 7db6ed7c14
2 changed files with 13 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/library/unifier.cpp
View file

@ -78,7 +78,8 @@ unifier_config::unifier_config(bool use_exceptions, bool discard):
m_expensive_classes(LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES),
m_discard(discard),
m_conservative(LEAN_DEFAULT_UNIFIER_CONSERVATIVE) {
m_cheap = false;
m_pattern = false;
m_cheap = false;
m_ignore_context_check = false;
}
@ -89,7 +90,8 @@ unifier_config::unifier_config(options const & o, bool use_exceptions, bool disc
m_expensive_classes(get_unifier_expensive_classes(o)),
m_discard(discard),
m_conservative(get_unifier_conservative(o)) {
m_cheap = false;
m_cheap = false;
m_pattern = false;
m_ignore_context_check = false;
}
@ -321,7 +323,6 @@ struct unifier_fn {
// only the definitions from the main module are treated as transparent.
unifier_config m_config;
unsigned m_num_steps;
bool m_pattern; //!< If true, then only higher-order (pattern) matching is used
bool m_first; //!< True if we still have to generate the first solution.
unsigned m_next_assumption_idx; //!< Next assumption index.
unsigned m_next_cidx; //!< Next constraint index.
@ -366,13 +367,12 @@ struct unifier_fn {
expr_map m_type_map;
name_to_cnstrs m_mvar_occs;
owned_map m_owned_map;
bool m_pattern;
/** \brief Save unifier's state */
case_split(unifier_fn & u, justification const & j):
m_assumption_idx(u.m_next_assumption_idx), m_jst(j), m_subst(u.m_subst),
m_postponed(u.m_postponed), m_cnstrs(u.m_cnstrs), m_type_map(u.m_type_map),
m_mvar_occs(u.m_mvar_occs), m_owned_map(u.m_owned_map), m_pattern(u.m_pattern) {
m_mvar_occs(u.m_mvar_occs), m_owned_map(u.m_owned_map) {
u.m_next_assumption_idx++;
}
@ -384,7 +384,6 @@ struct unifier_fn {
u.m_cnstrs = m_cnstrs;
u.m_mvar_occs = m_mvar_occs;
u.m_owned_map = m_owned_map;
u.m_pattern = m_pattern;
u.m_type_map = m_type_map;
m_assumption_idx = u.m_next_assumption_idx;
m_failed_justifications = mk_composite1(m_failed_justifications, *u.m_conflict);
@ -425,7 +424,7 @@ struct unifier_fn {
name_generator const & ngen, substitution const & s,
unifier_config const & cfg):
m_env(env), m_ngen(ngen), m_subst(s), m_plugin(get_unifier_plugin(env)),
m_config(cfg), m_num_steps(0), m_pattern(false) {
m_config(cfg), m_num_steps(0) {
if (m_config.m_cheap) {
m_tc[0] = mk_opaque_type_checker(env, m_ngen.mk_child());
m_tc[1] = m_tc[0];
@ -1411,6 +1410,7 @@ struct unifier_fn {
optional<bool> _has_meta_args;
bool cheap() const { return u.m_config.m_cheap; }
bool pattern() const { return u.m_config.m_pattern; }
type_checker & tc() {
return *u.m_tc[relax];
@ -1628,7 +1628,7 @@ struct unifier_fn {
void mk_app_projections() {
lean_assert(is_metavar(m));
lean_assert(is_app(rhs));
if (!u.m_pattern && !cheap()) {
if (!pattern() && !cheap()) {
expr const & f = get_app_fn(rhs);
lean_assert(is_constant(f) || is_local(f));
if (is_local(f)) {
@ -1825,12 +1825,12 @@ struct unifier_fn {
mk_simple_projections();
break;
case expr_kind::Sort: case expr_kind::Constant:
if (!u.m_pattern && !cheap() && !imitation_only)
if (!pattern() && !cheap() && !imitation_only)
mk_simple_projections();
mk_simple_imitation();
break;
case expr_kind::Pi: case expr_kind::Lambda:
if (!u.m_pattern && !cheap() && !imitation_only)
if (!pattern() && !cheap() && !imitation_only)
mk_simple_projections();
mk_bindings_imitation();
break;

3
src/library/unifier.h
View file

@ -47,6 +47,9 @@ struct unifier_config {
// - Disables reduction case-split on flex-rigid constraints.
// Default is m_conservative == false
bool m_conservative;
// If m_pattern is true, then we restrict the number of cases splits on
// flex-rigid constraints that are *not* in the higher-order pattern case.
bool m_pattern;
// If m_cheap is true, then expensive case-analysis is not performed (e.g., delta).
// It is more restrictive than m_conservative
// Default is m_cheap == false