feat(kernel): add telescope instantiate procedure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-16 11:52:43 -07:00
parent 40b3129e7b
commit 9a689ab0c3
4 changed files with 22 additions and 2 deletions

View file

@ -11,8 +11,8 @@ Author: Leonardo de Moura
#include "kernel/expr.h" #include "kernel/expr.h"
namespace lean { namespace lean {
// Remark: in a nonempty context C, variable 0 is head(C)
typedef list<binder> context; typedef list<binder> context;
typedef context telescope;
inline context extend(context const & c, name const & n, expr const & t) { return cons(binder(n, t), c); } inline context extend(context const & c, name const & n, expr const & t) { return cons(binder(n, t), c); }
inline context extend(context const & c, binder const & b) { return cons(b, c); } inline context extend(context const & c, binder const & b) { return cons(b, c); }
binder const & lookup(context const & c, unsigned i); binder const & lookup(context const & c, unsigned i);

View file

@ -242,15 +242,19 @@ class binder {
friend class expr_binding; friend class expr_binding;
name m_name; name m_name;
expr m_type; expr m_type;
binder_info m_info; binder_info m_info;
public: public:
binder(name const & n, expr const & t, binder_info const & bi = binder_info()): binder(name const & n, expr const & t, binder_info const & bi = binder_info()):
m_name(n), m_type(t), m_info(bi) {} m_name(n), m_type(t), m_info(bi) {}
name const & get_name() const { return m_name; } name const & get_name() const { return m_name; }
expr const & get_type() const { return m_type; } expr const & get_type() const { return m_type; }
binder_info const & get_info() const { return m_info; } binder_info const & get_info() const { return m_info; }
binder update_type(expr const & t) const { return binder(m_name, t, m_info); }
}; };
// Remark: in a telescope T, variable 0 is the last element of the list, and head(T) is variable #(length(T) - 1)
typedef list<binder> telescope;
/** \brief Lambda and Pi expressions */ /** \brief Lambda and Pi expressions */
class expr_binding : public expr_composite { class expr_binding : public expr_composite {
binder m_binder; binder m_binder;

View file

@ -40,6 +40,17 @@ expr instantiate(expr const & e, std::initializer_list<expr> const & l) { retur
expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s); } expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s); }
expr instantiate(expr const & e, expr const & s) { return instantiate(e, 0, s); } expr instantiate(expr const & e, expr const & s) { return instantiate(e, 0, s); }
telescope instantiate(telescope const & t, unsigned i, expr const & s) {
if (is_nil(t)) {
return t;
} else {
binder const & b = head(t);
return telescope(b.update_type(instantiate(b.get_type(), i, s)),
instantiate(tail(t), i+1, s));
}
}
telescope instantiate(telescope const & t, expr const & s) { return instantiate(t, s); }
bool is_head_beta(expr const & t) { bool is_head_beta(expr const & t) {
expr const * it = &t; expr const * it = &t;
while (is_app(*it)) { while (is_app(*it)) {

View file

@ -18,6 +18,11 @@ expr instantiate(expr const & e, unsigned i, expr const & s);
/** \brief Replace free variable \c 0 with \c s in \c e. */ /** \brief Replace free variable \c 0 with \c s in \c e. */
expr instantiate(expr const & e, expr const & s); expr instantiate(expr const & e, expr const & s);
/** \brief Replace free variable \c i with \c s in the telescope t. */
telescope instantiate(telescope const & t, unsigned i, expr const & s);
/** \brief Replace free variable \c 0 with \c s in the telescope t. */
telescope instantiate(telescope const & t, expr const & s);
expr apply_beta(expr f, unsigned num_args, expr const * args); expr apply_beta(expr f, unsigned num_args, expr const * args);
bool is_head_beta(expr const & t); bool is_head_beta(expr const & t);
expr head_beta_reduce(expr const & t); expr head_beta_reduce(expr const & t);