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

Add head_reduce

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-23 19:35:33 -07:00
parent be1ea2ddc7
commit bf608a38aa
2 changed files with 29 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/library/beta.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include "beta.h"
#include "instantiate.h"
#include "environment.h"
namespace lean {
bool is_head_beta(expr const & e) {
@ -38,4 +39,20 @@ expr head_beta(expr const & e) {
}
}
}
expr head_reduce(expr const & e, environment const & env, name_set const * defs) {
if (is_head_beta(e)) {
return head_beta(e);
} else if (is_let(e)) {
return instantiate(let_body(e), let_value(e));
} else if (is_constant(e)) {
name const & n = const_name(e);
if (defs == nullptr || defs->find(n) != defs->end()) {
object const & obj = env.find_object(n);
if (obj && obj.is_definition() && !obj.is_opaque())
return obj.get_value();
}
}
return e;
}
}

12
src/library/beta.h
View file

@ -6,8 +6,10 @@ Author: Leonardo de Moura
*/
#pragma once
#include "expr.h"
#include "name_set.h"
namespace lean {
class environment;
/**
\brief Return true iff the given expression is of the form:
@ -16,4 +18,14 @@ namespace lean {
bool is_head_beta(expr const & e);
/** \brief Apply head beta-reduction to the given expression. */
expr head_beta(expr const & e);
/**
\brief Try to reduce the head of the given expression.
The following reductions are tried:
1- Beta reduction
2- Constant unfolding (if constant is defined in env, and defs ==
nullptr or it contains constant).
3- Let expansion
*/
expr head_reduce(expr const & e, environment const & env, name_set const * defs = nullptr);
};