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

refactor(kernel): add find_fn, replace for_each_fn with find_fn when appropriate, remove unnecessary function has_cached_type

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-19 13:03:46 -08:00
parent 5cfcb7e144
commit 0126fa0499
9 changed files with 111 additions and 145 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/frontends/lean/pp.cpp
View file

@ -16,6 +16,7 @@ Author: Leonardo de Moura
#include "util/interrupt.h"
#include "kernel/context.h"
#include "kernel/for_each_fn.h"
#include "kernel/find_fn.h"
#include "kernel/occurs.h"
#include "kernel/builtin.h"
#include "kernel/free_vars.h"
@ -1119,26 +1120,13 @@ class pp_fn {
m_alias_min_weight = get_pp_alias_min_weight(opts);
}
struct found_prefix {};
bool uses_prefix(expr const & e, name const & prefix) {
auto f = [&](expr const & e, unsigned) {
if (is_constant(e)) {
if (is_prefix_of(prefix, const_name(e))) throw found_prefix();
} else if (is_abstraction(e)) {
if (is_prefix_of(prefix, abst_name(e))) throw found_prefix();
} else if (is_let(e)) {
if (is_prefix_of(prefix, let_name(e))) throw found_prefix();
}
return true;
};
try {
for_each_fn<decltype(f)> visitor(f);
visitor(e);
return false;
} catch (found_prefix) {
return true;
}
return find(e, [&](expr const & e) {
return
(is_constant(e) && is_prefix_of(prefix, const_name(e))) ||
(is_abstraction(e) && is_prefix_of(prefix, abst_name(e))) ||
(is_let(e) && is_prefix_of(prefix, let_name(e)));
});
}
name find_unused_prefix(expr const & e) {

2
src/kernel/CMakeLists.txt
View file

@ -1,7 +1,7 @@
add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
type_checker.cpp builtin.cpp occurs.cpp metavar.cpp justification.cpp
unification_constraint.cpp printer.cpp formatter.cpp has_cached_type.cpp
unification_constraint.cpp printer.cpp formatter.cpp
kernel_exception.cpp type_checker_justification.cpp pos_info_provider.cpp
replace_visitor.cpp)

12
src/kernel/environment.cpp
View file

@ -15,12 +15,12 @@ Author: Leonardo de Moura
#include "util/safe_arith.h"
#include "util/realpath.h"
#include "kernel/for_each_fn.h"
#include "kernel/find_fn.h"
#include "kernel/kernel_exception.h"
#include "kernel/environment.h"
#include "kernel/threadsafe_environment.h"
#include "kernel/type_checker.h"
#include "kernel/normalizer.h"
#include "kernel/has_cached_type.h"
namespace lean {
static name g_builtin_module("builtin_module");
@ -288,8 +288,16 @@ struct environment::imp {
m_uvars.emplace_back();
}
/**
The kernel should *not* accept expressions containing cached types.
Reason: Cached types may introduce unsoundness.
For example, in the environment env, the constant x may have type T.
Now suppose we are trying to add a new definition D that contains x,
and x is associated with a cached type T'. The cached type may allow
us to accept a definition that is type incorrect with respect to env.
*/
void check_no_cached_type(expr const & e, environment const & env) {
if (has_cached_type(e))
if (find(e, [](expr const & a) { return is_constant(a) && const_type(a); }))
throw kernel_exception(env, "expression has a constant with a cached type, this is a bug in one of Lean tactics and/or solvers");
}

67
src/kernel/find_fn.h Normal file
View file

@ -0,0 +1,67 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/for_each_fn.h"
#include "kernel/context.h"
namespace lean {
template<typename P>
class find_fn {
struct pred_fn {
expr & m_result;
P m_p;
pred_fn(expr & result, P const & p):m_result(result), m_p(p) {}
bool operator()(expr const & e, unsigned) {
if (m_result) {
return false; // already found result, stop the search
} else if (m_p(e)) {
m_result = e;
return false; // stop the search
} else {
return true; // continue the search
}
}
};
expr m_result;
for_each_fn<pred_fn> m_proc;
public:
find_fn(P const & p):m_proc(pred_fn(m_result, p)) {}
expr operator()(expr const & e) { m_proc(e); return m_result; }
};
/**
\brief Return a subexpression of \c e that satisfies the predicate \c p.
If there is none, then return the null expression.
*/
template<typename P>
expr find(expr const & e, P p) {
return find_fn<P>(p)(e);
}
/**
\brief Return an expression \c e that satisfies \c p and occurs in \c c or \c es.
*/
template<typename P>
expr find(context const * c, unsigned sz, expr const * es, P p) {
find_fn<P> finder(p);
if (c) {
for (auto const & e : *c) {
if (expr r = finder(e.get_domain())) {
return r;
} else if (e.get_body()) {
if (expr r = finder(e.get_body()))
return r;
}
}
}
for (unsigned i = 0; i < sz; i++) {
if (expr r = finder(es[i]))
return r;
}
return expr();
}
}

5
src/kernel/for_each_fn.h
View file

@ -107,4 +107,9 @@ public:
for_each_fn(F const & f):m_f(f) {}
void operator()(expr const & e) { apply(e, 0); }
};
template<typename F>
void for_each(expr const & e, F f) {
return for_each_fn<F>(f)(e);
}
}

27
src/kernel/has_cached_type.cpp
View file

@ -1,27 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/expr.h"
#include "kernel/for_each_fn.h"
namespace lean {
bool has_cached_type(expr const & e) {
bool result = false;
auto f = [&](expr const & e, unsigned) {
if (result) {
return false; // do not continue the search
} else if (is_constant(e) && const_type(e)) {
result = true;
return false;
} else {
return true;
}
};
for_each_fn<decltype(f)> proc(f);
proc(e);
return result;
}
}

22
src/kernel/has_cached_type.h
View file

@ -1,22 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
namespace lean {
/**
\brief Return true iff \c e contains a constant with a cached type.
The kernel should *not* accept expressions containing cached types.
Reason: Cached types may introduce unsoundness.
For example, in the environment env, the constant x may have type T.
Now suppose we are trying to add a new definition D that contains x,
and x is associated with a cached type T'. The cached type may allow
us to accept a definition that is type incorrect with respect to env.
*/
bool has_cached_type(expr const & e);
}

48
src/kernel/metavar.cpp
View file

@ -14,6 +14,7 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "kernel/occurs.h"
#include "kernel/for_each_fn.h"
#include "kernel/find_fn.h"
namespace lean {
/**
@ -289,19 +290,17 @@ bool has_assigned_metavar(expr const & e, metavar_env const & menv) {
return false;
} else {
bool result = false;
auto proc = [&](expr const & n, unsigned) {
if (result)
return false;
if (!has_metavar(n))
return false;
if (is_metavar(n) && menv.is_assigned(n)) {
result = true;
return false;
}
return true;
};
for_each_fn<decltype(proc)> visitor(proc);
visitor(e);
for_each(e, [&](expr const & n, unsigned) {
if (result)
return false;
if (!has_metavar(n))
return false;
if (is_metavar(n) && menv.is_assigned(n)) {
result = true;
return false;
}
return true;
});
return result;
}
}
@ -365,23 +364,12 @@ bool has_metavar(expr const & e, expr const & m, metavar_env const & menv) {
if (has_metavar(e)) {
lean_assert(is_metavar(m));
lean_assert(!menv.is_assigned(m));
auto f = [&](expr const & m2, unsigned) {
if (is_metavar(m2)) {
if (metavar_name(m) == metavar_name(m2))
throw found_metavar();
if (menv.is_assigned(m2) &&
has_metavar(menv.get_subst(m2), m, menv))
throw found_metavar();
}
return true;
};
try {
for_each_fn<decltype(f)> proc(f);
proc(e);
return false;
} catch (found_metavar) {
return true;
}
return find(e, [&](expr const & m2) {
return
is_metavar(m2) &&
((metavar_name(m) == metavar_name(m2)) ||
(menv.is_assigned(m2) && has_metavar(menv.get_subst(m2), m, menv)));
});
} else {
return false;
}

47
src/kernel/occurs.cpp
View file

@ -5,57 +5,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/occurs.h"
#include "kernel/for_each_fn.h"
#include "kernel/find_fn.h"
namespace lean {
template<typename F>
void for_each(F & f, context const * c, unsigned sz, expr const * es) {
for_each_fn<F> visitor(f);
if (c) {
for (auto const & e : *c) {
visitor(e.get_domain());
if (e.get_body())
visitor(e.get_body());
}
}
for (unsigned i = 0; i < sz; i++)
visitor(es[i]);
}
namespace occurs_ns {
/** \brief Auxiliary struct used to sign (as an exception) that an occurrence was found. */
struct found {};
}
bool occurs(name const & n, context const * c, unsigned sz, expr const * es) {
auto visitor = [&](expr const & e, unsigned) -> bool {
if (is_constant(e)) {
if (const_name(e) == n)
throw occurs_ns::found();
}
return true;
};
try {
for_each(visitor, c, sz, es);
return false;
} catch (occurs_ns::found) {
return true;
}
return find(c, sz, es, [&](expr const & e) { return is_constant(e) && const_name(e) == n; });
}
bool occurs(expr const & n, context const * c, unsigned sz, expr const * es) {
auto visitor = [&](expr const & e, unsigned) -> bool {
if (e == n)
throw occurs_ns::found();
return true;
};
try {
for_each(visitor, c, sz, es);
return false;
} catch (occurs_ns::found) {
return true;
}
return find(c, sz, es, [&](expr const & e) { return e == n; });
}
bool occurs(expr const & n, expr const & m) { return occurs(n, nullptr, 1, &m); }
bool occurs(name const & n, expr const & m) { return occurs(n, nullptr, 1, &m); }
bool occurs(expr const & n, context const & c) { return occurs(n, &c, 0, nullptr); }