From b1b49e86e7ae0fe2ae9b4a6262388ef47fd97b15 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Oct 2013 08:16:23 -0700 Subject: [PATCH] test(elaborator): add simple test Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 1 + src/kernel/unification_constraint.cpp | 2 +- src/library/elaborator/elaborator.cpp | 17 +++++- src/tests/library/elaborator/CMakeLists.txt | 3 ++ src/tests/library/elaborator/elaborator.cpp | 60 +++++++++++++++++++++ 5 files changed, 81 insertions(+), 2 deletions(-) create mode 100644 src/tests/library/elaborator/CMakeLists.txt create mode 100644 src/tests/library/elaborator/elaborator.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 43f61e333..19d41ff34 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -149,6 +149,7 @@ add_subdirectory(tests/util/interval) add_subdirectory(tests/kernel) add_subdirectory(tests/library) add_subdirectory(tests/library/rewriter) +add_subdirectory(tests/library/elaborator) add_subdirectory(tests/frontends/lean) # Include style check diff --git a/src/kernel/unification_constraint.cpp b/src/kernel/unification_constraint.cpp index 8987de571..3ab972297 100644 --- a/src/kernel/unification_constraint.cpp +++ b/src/kernel/unification_constraint.cpp @@ -112,7 +112,7 @@ format unification_constraint_choice::pp(formatter const & fmt, options const & format or_op = unicode ? format("\u2295") : format("OR"); format body; for (unsigned i = 0; i < m_num_choices; i++) { - body += format{m_fmt, eq_op, fmt(m_ctx, m_choices[i], false, opts)}; + body += group(paren(format{m_fmt, space(), eq_op, compose(line(), fmt(m_ctx, m_choices[i], false, opts))})); if (i + 1 < m_num_choices) body += format{space(), or_op, line()}; } diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index f7ad3d24a..02f4572af 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -4,21 +4,36 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/pdeque.h" +#include "kernel/formatter.h" #include "library/elaborator/elaborator.h" namespace lean { class elaborator::imp { + typedef pdeque cnstr_queue; + + struct state { + unsigned m_id; + metavar_env m_menv; + cnstr_queue m_queue; + }; + environment const & m_env; std::shared_ptr m_synthesizer; std::shared_ptr m_plugin; bool m_interrupted; public: - imp(environment const & env, metavar_env const &, unsigned, unification_constraint const *, + imp(environment const & env, metavar_env const &, unsigned num_cnstrs, unification_constraint const * cnstrs, std::shared_ptr const & s, std::shared_ptr const & p): m_env(env), m_synthesizer(s), m_plugin(p) { m_interrupted = false; + + formatter fmt = mk_simple_formatter(); + for (unsigned i = 0; i < num_cnstrs; i++) { + std::cout << cnstrs[i].pp(fmt, options(), true) << "\n"; + } } substitution next() { diff --git a/src/tests/library/elaborator/CMakeLists.txt b/src/tests/library/elaborator/CMakeLists.txt new file mode 100644 index 000000000..fac7afc08 --- /dev/null +++ b/src/tests/library/elaborator/CMakeLists.txt @@ -0,0 +1,3 @@ +add_executable(elaborator_tst elaborator.cpp) +target_link_libraries(elaborator_tst ${EXTRA_LIBS}) +add_test(elaborator_tst ${CMAKE_CURRENT_BINARY_DIR}/elaborator_tst) diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp new file mode 100644 index 000000000..2cca32767 --- /dev/null +++ b/src/tests/library/elaborator/elaborator.cpp @@ -0,0 +1,60 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/test.h" +#include "kernel/environment.h" +#include "kernel/type_checker.h" +#include "kernel/abstract.h" +#include "library/arith/arith.h" +#include "library/all/all.h" +#include "library/elaborator/elaborator.h" +using namespace lean; + +static void tst1() { + environment env; + import_all(env); + metavar_env menv; + buffer ucs; + type_checker checker(env); + expr list = Const("list"); + expr nil = Const("nil"); + expr cons = Const("cons"); + expr A = Const("A"); + env.add_var("list", Type() >> Type()); + env.add_var("nil", Pi({A, Type()}, list(A))); + env.add_var("cons", Pi({A, Type()}, A >> (list(A) >> list(A)))); + env.add_var("a", Int); + env.add_var("b", Int); + env.add_var("n", Nat); + env.add_var("m", Nat); + expr a = Const("a"); + expr b = Const("b"); + expr n = Const("n"); + expr m = Const("m"); + expr m1 = menv.mk_metavar(); + expr m2 = menv.mk_metavar(); + expr m3 = menv.mk_metavar(); + expr A1 = menv.mk_metavar(); + expr A2 = menv.mk_metavar(); + expr A3 = menv.mk_metavar(); + expr A4 = menv.mk_metavar(); + expr F = cons(A1, m1(a), cons(A2, m2(n), cons(A3, m3(b), nil(A4)))); + std::cout << F << "\n"; + std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n"; + expr int_id = Fun({a, Int}, a); + expr nat_id = Fun({a, Nat}, a); + ucs.push_back(mk_choice_constraint(context(), m1, { int_id, mk_int_to_real_fn() }, trace())); + ucs.push_back(mk_choice_constraint(context(), m2, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, trace())); + ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, trace())); + elaborator elb(env, menv, ucs.size(), ucs.data()); + substitution s = elb.next(); +} + +int main() { + tst1(); + return has_violations() ? 1 : 0; +} +