From 92f5a31976300a124eb72cf55990cf5c09769072 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 26 Oct 2013 14:46:12 -0700 Subject: [PATCH] feat(kernel/expr): add new mk_app template for creating applications using a collection Signed-off-by: Leonardo de Moura --- src/frontends/lean/frontend.cpp | 2 +- src/frontends/lean/frontend_elaborator.cpp | 4 ++-- src/frontends/lean/parser.cpp | 4 ++-- src/kernel/expr.h | 1 + src/kernel/instantiate.cpp | 2 +- src/kernel/normalizer.cpp | 2 +- src/library/cast/cast.cpp | 4 ++-- src/library/deep_copy.cpp | 2 +- src/library/elaborator/elaborator.cpp | 8 ++++---- src/library/update_expr.cpp | 2 +- 10 files changed, 16 insertions(+), 15 deletions(-) diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index b17de6ab5..e65645bc8 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -230,7 +230,7 @@ struct frontend::imp { args.push_back(mk_constant(n)); unsigned j = sz; while (j > 0) { --j; args.push_back(mk_var(j)); } - return mk_app(args.size(), args.data()); + return mk_app(args); } else { lean_assert(is_pi(type)); return mk_lambda(abst_name(type), abst_domain(type), mk_explicit_definition_body(abst_body(type), n, i+1, sz)); diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp index ac32b8114..bc64c6a75 100644 --- a/src/frontends/lean/frontend_elaborator.cpp +++ b/src/frontends/lean/frontend_elaborator.cpp @@ -241,7 +241,7 @@ class frontend_elaborator::imp { } } } - return mk_app(args.size(), args.data()); + return mk_app(args); } else { buffer new_args; expr new_f = visit(f, ctx); @@ -273,7 +273,7 @@ class frontend_elaborator::imp { if (new_f_t) new_f_t = ::lean::instantiate(abst_body(new_f_t), new_a); } - return mk_app(new_args.size(), new_args.data()); + return mk_app(new_args); } } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 1883f3802..c9d81b484 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -417,7 +417,7 @@ class parser::imp { } else { new_args.append(num_args, args); } - return save(mk_app(new_args.size(), new_args.data()), pos); + return save(mk_app(new_args), pos); } expr mk_application(operator_info const & op, pos_info const & pos, std::initializer_list const & l) { return mk_application(op, pos, l.size(), l.begin()); @@ -560,7 +560,7 @@ class parser::imp { args.push_back(parse_expr(1)); } } - return mk_app(args.size(), args.data()); + return mk_app(args); } else { return mk_constant(obj.get_name()); } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index bead5697c..ee991067c 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -365,6 +365,7 @@ inline expr mk_value(value & v) { return expr(new expr_value(v)); } inline expr to_expr(value & v) { return mk_value(v); } expr mk_app(unsigned num_args, expr const * args); inline expr mk_app(std::initializer_list const & l) { return mk_app(l.size(), l.begin()); } +template expr mk_app(T const & args) { return mk_app(args.size(), args.data()); } inline expr mk_app(expr const & e1, expr const & e2) { return mk_app({e1, e2}); } inline expr mk_app(expr const & e1, expr const & e2, expr const & e3) { return mk_app({e1, e2, e3}); } inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({e1, e2, e3, e4}); } diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index d42d64563..b5a5ce512 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -85,7 +85,7 @@ expr apply_beta(expr f, unsigned num_args, expr const * args) { new_args.push_back(r); for (; m < num_args; m++) new_args.push_back(args[m]); - return mk_app(new_args.size(), new_args.data()); + return mk_app(new_args); } } diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index d9fc0875b..ae84649cf 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -245,7 +245,7 @@ class normalizer::imp { break; } } - r = svalue(mk_app(new_args.size(), new_args.data())); + r = svalue(mk_app(new_args)); break; } } diff --git a/src/library/cast/cast.cpp b/src/library/cast/cast.cpp index 2820e9438..84d687a37 100644 --- a/src/library/cast/cast.cpp +++ b/src/library/cast/cast.cpp @@ -54,7 +54,7 @@ public: buffer new_as; new_as.push_back(c); new_as.append(num_as - 5, as + 5); - r = mk_app(new_as.size(), new_as.data()); + r = mk_app(new_as); } return true; } else if (num_as > 5 && is_pi(as[1]) && is_pi(as[2])) { @@ -91,7 +91,7 @@ public: buffer new_as; new_as.push_back(fa_1_B2); new_as.append(num_as - 6, as + 6); - r = mk_app(new_as.size(), new_as.data()); + r = mk_app(new_as); } return true; } else { diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp index de41eadda..f39905a38 100644 --- a/src/library/deep_copy.cpp +++ b/src/library/deep_copy.cpp @@ -30,7 +30,7 @@ class deep_copy_fn { buffer new_args; for (expr const & old_arg : args(a)) new_args.push_back(apply(old_arg)); - r = mk_app(new_args.size(), new_args.data()); + r = mk_app(new_args); break; } case expr_kind::Eq: r = mk_eq(apply(eq_lhs(a)), apply(eq_rhs(a))); break; diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 10e91459e..04ab6e670 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -280,7 +280,7 @@ class elaborator::imp { --i; args.push_back(mk_var(i)); } - return mk_app(args.size(), args.data()); + return mk_app(args); } /** @@ -552,7 +552,7 @@ class elaborator::imp { } } if (modified) { - a = mk_app(new_args.size(), new_args.data()); + a = mk_app(new_args); return; } } else { @@ -748,7 +748,7 @@ class elaborator::imp { imitation_args.push_back(mk_app_vars(h_i, num_a - 1)); push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_i), arg(b, i), new_assumption); } - imitation = mk_lambda(arg_types, mk_app(imitation_args.size(), imitation_args.data())); + imitation = mk_lambda(arg_types, mk_app(imitation_args)); } else if (is_eq(b)) { // Imitation for equality // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), (h_1 x_1 ... x_{num_a-1}) = (h_2 x_1 ... x_{num_a-1}) @@ -866,7 +866,7 @@ class elaborator::imp { expr h_i = new_state.m_menv.mk_metavar(ctx); imitation_args.push_back(h_i); } - imitation = mk_app(imitation_args.size(), imitation_args.data()); + imitation = mk_app(imitation_args); } else if (is_eq(b)) { // Imitation for equality b == Eq(s1, s2) // mname <- Eq(?h_1, ?h_2) diff --git a/src/library/update_expr.cpp b/src/library/update_expr.cpp index 29cb355d0..56ae2a758 100644 --- a/src/library/update_expr.cpp +++ b/src/library/update_expr.cpp @@ -20,7 +20,7 @@ expr update_app(expr const & app, unsigned i, expr const & new_arg) { else new_args.push_back(arg(app, j)); } - return mk_app(new_args.size(), new_args.data()); + return mk_app(new_args); } }