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

Add forall, foldl, foldr to sexpr_funcs

Browse source
This commit is contained in:
Soonho Kong 2013-07-30 00:05:30 -07:00
parent 812fdaec6f
commit 5be67bd42c
1 changed files with 36 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/util/sexpr/sexpr_funcs.h
View file

@ -48,6 +48,42 @@ sexpr filter(sexpr const & l, P p) {
} }
} }
template<class T, class BinaryOperation>
T foldl(sexpr const & l, T init, BinaryOperation op) {
lean_assert(is_list(l));
if (is_nil(l)) {
return init;
}
else {
lean_assert(is_cons(l));
return foldl(tail(l), op(init, head(l)), op);
}
}
template<class T, class BinaryOperation>
T foldr(sexpr const & l, T init, BinaryOperation op) {
lean_assert(is_list(l));
if (is_nil(l)) {
return init;
}
else {
lean_assert(is_cons(l));
return op(head(l), foldr(tail(l), init, op));
}
}
template<typename F>
bool forall(sexpr const & l, F f) {
lean_assert(is_list(l));
if (is_nil(l)) {
return true;
}
else {
lean_assert(is_cons(l));
return f(head(l)) && forall(tail(l), f);
}
}
template<typename P> template<typename P>
bool contains(sexpr const & l, P p) { bool contains(sexpr const & l, P p) {
lean_assert(is_list(l)); lean_assert(is_list(l));