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

feat(library/util): add auxiliary functions

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-20 15:42:51 -08:00
parent 8323d580b1
commit b6750e9d29
2 changed files with 35 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/library/util.cpp
View file

@ -12,6 +12,31 @@ Author: Leonardo de Moura
#include "library/locals.h"
namespace lean {
bool is_def_app(environment const & env, expr const & e) {
if (!is_app(e))
return false;
expr const & f = get_app_fn(e);
if (!is_constant(f))
return false;
auto decl = env.find(const_name(f));
return decl && decl->is_definition() && !decl->is_opaque();
}
optional<expr> unfold_app(environment const & env, expr const & e) {
if (!is_app(e))
return none_expr();
expr const & f = get_app_fn(e);
if (!is_constant(f))
return none_expr();
auto decl = env.find(const_name(f));
if (!decl || !decl->is_definition() || decl->is_opaque())
return none_expr();
expr d = instantiate_value_univ_params(*decl, const_levels(f));
buffer<expr> args;
get_app_rev_args(e, args);
return some_expr(apply_beta(d, args.size(), args.data()));
}
optional<level> dec_level(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:

10
src/library/util.h
View file

@ -11,6 +11,16 @@ Author: Leonardo de Moura
namespace lean {
typedef std::unique_ptr<type_checker> type_checker_ptr;
/** \brief Return true iff \c e is of the form <tt>(f ...)</tt> where
\c f is a non-opaque constant definition */
bool is_def_app(environment const & env, expr const & e);
/** \brief If \c e is of the form <tt>(f a_1 ... a_n)</tt>, where \c f is
a non-opaque definition, then unfold \c f, and beta reduce.
Otherwise, return none.
*/
optional<expr> unfold_app(environment const & env, expr const & e);
/** \brief Reduce (if possible) universe level by 1.
\pre is_not_zero(l)
*/