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

feat(kernel/expr): improve get_app_args interface

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-17 19:19:10 -07:00
parent 28e8299f6d
commit 5c7d3c79c4
2 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/kernel/expr.cpp
View file

@ -323,10 +323,13 @@ expr mk_app_vars(expr const & f, unsigned n) {
return r;
}
void get_app_args(expr const & e, buffer<expr> & args) {
expr get_app_args(expr const & e, buffer<expr> & args) {
if (is_app(e)) {
get_app_args(app_fn(e), args);
expr r = get_app_args(app_fn(e), args);
args.push_back(app_arg(e));
return r;
} else {
return e;
}
}

4
src/kernel/expr.h
View file

@ -593,8 +593,10 @@ inline bool has_free_var_ge(expr const & e, unsigned low) { return get_free_var_
/**
\brief Given \c e of the form <tt>(...(f a1) ... an)</tt>, store a1 ... an in args.
If \c e is not an application, then nothing is stored in args.
It returns the f.
*/
void get_app_args(expr const & e, buffer<expr> & args);
expr get_app_args(expr const & e, buffer<expr> & args);
// =======================================