From 92a7c38260f8e8348b2bb9a431bb963a15b6fe81 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Nov 2015 14:00:57 -0800 Subject: [PATCH] feat(kernel/expr): add mk_app that takes a list of arguments --- src/kernel/expr.cpp | 6 ++++++ src/kernel/expr.h | 1 + 2 files changed, 7 insertions(+) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index c18e29183..f2b96bc66 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -406,6 +406,12 @@ expr mk_app(unsigned num_args, expr const * args, tag g) { return mk_app(mk_app(args[0], args[1], g), num_args - 2, args+2, g); } +expr mk_app(expr const & f, list const & args, tag g) { + buffer _args; + to_buffer(args, _args); + return mk_app(f, _args, g); +} + expr mk_rev_app(expr const & f, unsigned num_args, expr const * args, tag g) { expr r = f; unsigned i = num_args; diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 5f387f654..d148ab433 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -438,6 +438,7 @@ inline expr mk_app(buffer const & args, tag g = nulltag) { return mk_app(a inline expr mk_app(expr const & f, buffer const & args, tag g = nulltag) { return mk_app(f, args.size(), args.data(), g); } +expr mk_app(expr const & f, list const & args, tag g = nulltag); expr mk_rev_app(expr const & f, unsigned num_args, expr const * args, tag g = nulltag); expr mk_rev_app(unsigned num_args, expr const * args, tag g = nulltag); inline expr mk_rev_app(buffer const & args, tag g = nulltag) { return mk_rev_app(args.size(), args.data(), g); }