From 72e99ea3ee2fc2c10ad7607201780a619ea4ebf7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 11 Sep 2018 17:55:06 -0700 Subject: [PATCH] fix(library/compiler/lcnf): `apply_beta` takes arguments in reverse order --- src/library/compiler/lcnf.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp index b749b1155e..8b9e215663 100644 --- a/src/library/compiler/lcnf.cpp +++ b/src/library/compiler/lcnf.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "runtime/flet.h" #include "kernel/type_checker.h" #include "kernel/instantiate.h" @@ -69,9 +70,10 @@ public: return m_lctx.mk_lambda(args, mk_app(e, args)); } - expr visit_projection(expr const & fn, buffer const & args, bool root) { + expr visit_projection(expr const & fn, buffer & args, bool root) { constant_info info = m_env.get(const_name(fn)); expr fn_val = instantiate_value_lparams(info, const_levels(fn)); + std::reverse(args.begin(), args.end()); return visit(apply_beta(fn_val, args.size(), args.data()), root); }