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

feat(kernel/abstract): add more Fun functions for simplifying the creation lambda-expressions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-19 09:01:20 -07:00
parent 5566186c34
commit eb409a9ce3
2 changed files with 16 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/kernel/abstract.cpp
View file

@ -57,13 +57,17 @@ expr FName(std::initializer_list<std::pair<expr const &, expr const &>> const &
MkBinder(Fun);
MkBinder(Pi);
expr Pi(unsigned num, expr const * locals, expr const & b) {
expr r = b;
unsigned i = num;
while (i > 0) {
--i;
r = mk_pi(local_pp_name(locals[i]), mlocal_type(locals[i]), abstract(r, locals[i]));
}
return r;
#define MkBinder2(FName, Mk) \
expr FName(unsigned num, expr const * locals, expr const & b) { \
expr r = b; \
unsigned i = num; \
while (i > 0) { \
--i; \
r = Mk(local_pp_name(locals[i]), mlocal_type(locals[i]), abstract(r, locals[i])); \
} \
return r; \
}
MkBinder2(Fun, mk_lambda);
MkBinder2(Pi, mk_pi);
}

4
src/kernel/abstract.h
View file

@ -43,6 +43,10 @@ inline expr Fun(expr const & n, expr const & t, expr const & b, binder_info cons
}
inline expr Fun(std::pair<expr const &, expr const &> const & p, expr const & b) { return Fun(p.first, p.second, b); }
expr Fun(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b);
/** \brief Create a lambda-expression by abstracting the given local constants over b */
expr Fun(unsigned num, expr const * locals, expr const & b);
template<typename T> expr Fun(T const & locals, expr const & b) { return Fun(locals.size(), locals.data(), b); }
inline expr Fun(expr const & local, expr const & b) { return Fun(1, &local, b); }
/**
\brief Create a Pi expression (pi (x : t) b), the term b is abstracted using abstract(b, constant(x)).