test(elaborator): add simple test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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

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()};
     }

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<unification_constraint> cnstr_queue;
+
+    struct state {
+        unsigned    m_id;
+        metavar_env m_menv;
+        cnstr_queue m_queue;
+    };
+
     environment const &                m_env;
     std::shared_ptr<synthesizer>       m_synthesizer;
     std::shared_ptr<elaborator_plugin> 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<synthesizer> const & s, std::shared_ptr<elaborator_plugin> 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() {

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)

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<unification_constraint> 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;
+}
+