From ec18bd93f91ddd998fb9278b272079f98266b46d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Jun 2014 07:03:25 -0700 Subject: [PATCH] feat(frontends/lean): send tactic hint table to elaborator Signed-off-by: Leonardo de Moura --- src/frontends/lean/cmd_table.h | 2 +- src/frontends/lean/elaborator.cpp | 19 +++++++++++-------- src/frontends/lean/elaborator.h | 8 +++++--- src/frontends/lean/hint_table.h | 13 +++++++++++++ src/frontends/lean/parser.cpp | 8 ++++---- src/frontends/lean/parser.h | 2 +- src/library/unifier.cpp | 3 --- src/tests/util/rb_map.cpp | 3 --- src/util/rb_tree.h | 7 +++++++ 9 files changed, 42 insertions(+), 23 deletions(-) create mode 100644 src/frontends/lean/hint_table.h diff --git a/src/frontends/lean/cmd_table.h b/src/frontends/lean/cmd_table.h index a0132059b..f3fa578c6 100644 --- a/src/frontends/lean/cmd_table.h +++ b/src/frontends/lean/cmd_table.h @@ -8,9 +8,9 @@ Author: Leonardo de Moura #include #include #include "kernel/environment.h" +#include "library/tactic/tactic.h" namespace lean { -class tactic {}; // TODO(Leo): remove after tactic framework is ported to Lean 0.2 class parser; typedef std::function command_fn; diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 7cc5d4fe7..87b5d29d2 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -22,6 +22,7 @@ Author: Leonardo de Moura #include "library/explicit.h" #include "library/unifier.h" #include "frontends/lean/parameter.h" +#include "frontends/lean/hint_table.h" namespace lean { class elaborator { @@ -32,6 +33,7 @@ class elaborator { io_state m_ios; unifier_plugin m_plugin; name_generator m_ngen; + hint_table m_hints; type_checker m_tc; substitution m_subst; context m_ctx; @@ -110,10 +112,10 @@ class elaborator { public: elaborator(environment const & env, io_state const & ios, name_generator const & ngen, - substitution const & s = substitution(), context const & ctx = context()): + hint_table const & htable, substitution const & s = substitution(), context const & ctx = context()): m_env(env), m_ios(ios), m_plugin([](constraint const &, name_generator const &) { return lazy_list>(); }), - m_ngen(ngen), m_tc(env, m_ngen.mk_child(), mk_default_converter(m_env, optional(0))), + m_ngen(ngen), m_hints(htable), m_tc(env, m_ngen.mk_child(), mk_default_converter(m_env, optional(0))), m_subst(s), m_ctx(ctx) { } @@ -612,15 +614,16 @@ public: static name g_tmp_prefix = name::mk_internal_unique_name(); expr elaborate(environment const & env, io_state const & ios, expr const & e, name_generator const & ngen, - substitution const & s, list const & ctx) { - return elaborator(env, ios, ngen, s, ctx)(e); + hint_table const & htable, substitution const & s, list const & ctx) { + return elaborator(env, ios, ngen, htable, s, ctx)(e); } -expr elaborate(environment const & env, io_state const & ios, expr const & e) { - return elaborate(env, ios, e, name_generator(g_tmp_prefix), substitution(), list()); +expr elaborate(environment const & env, io_state const & ios, expr const & e, hint_table const & htable) { + return elaborate(env, ios, e, name_generator(g_tmp_prefix), htable, substitution(), list()); } -std::pair elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v) { - return elaborator(env, ios, name_generator(g_tmp_prefix))(t, v, n); +std::pair elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v, + hint_table const & htable) { + return elaborator(env, ios, name_generator(g_tmp_prefix), htable)(t, v, n); } } diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 32623456c..aebf1bd1d 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -10,10 +10,12 @@ Author: Leonardo de Moura #include "kernel/environment.h" #include "kernel/metavar.h" #include "library/io_state.h" +#include "frontends/lean/hint_table.h" namespace lean { expr elaborate(environment const & env, io_state const & ios, expr const & e, name_generator const & ngen, - substitution const & s = substitution(), list const & ctx = list()); -expr elaborate(environment const & env, io_state const & ios, expr const & e); -std::pair elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v); + hint_table const & htable = hint_table(), substitution const & s = substitution(), list const & ctx = list()); +expr elaborate(environment const & env, io_state const & ios, expr const & e, hint_table const & htable = hint_table()); +std::pair elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v, + hint_table const & htable = hint_table()); } diff --git a/src/frontends/lean/hint_table.h b/src/frontends/lean/hint_table.h new file mode 100644 index 000000000..723a78907 --- /dev/null +++ b/src/frontends/lean/hint_table.h @@ -0,0 +1,13 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/rb_map.h" +#include "library/tactic/tactic.h" + +namespace lean { +typedef rb_map hint_table; +} diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 5956ac853..db95990fd 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -546,15 +546,15 @@ expr parser::mk_Type() { } expr parser::elaborate(expr const & e) { - return ::lean::elaborate(m_env, m_ios, e); + return ::lean::elaborate(m_env, m_ios, e, m_hints); } expr parser::elaborate(environment const & env, expr const & e) { - return ::lean::elaborate(env, m_ios, e); + return ::lean::elaborate(env, m_ios, e, m_hints); } std::pair parser::elaborate(name const & n, expr const & t, expr const & v) { - return ::lean::elaborate(m_env, m_ios, n, t, v); + return ::lean::elaborate(m_env, m_ios, n, t, v, m_hints); } /** \brief Parse ID ':' expr, where the expression represents the type of the identifier. */ @@ -973,7 +973,7 @@ tactic parser::parse_tactic(unsigned /* rbp */) { } void parser::save_hint(expr const & e, tactic const & t) { - m_hints.insert(mk_pair(get_tag(e), t)); + m_hints.insert(get_tag(e), t); } void parser::parse_command() { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 34febfbdb..92ff13cea 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -20,6 +20,7 @@ Author: Leonardo de Moura #include "library/io_state_stream.h" #include "library/kernel_bindings.h" #include "frontends/lean/parameter.h" +#include "frontends/lean/hint_table.h" #include "frontends/lean/scanner.h" #include "frontends/lean/local_decls.h" #include "frontends/lean/parser_config.h" @@ -39,7 +40,6 @@ struct interrupt_parser {}; typedef local_decls local_expr_decls; typedef local_decls local_level_decls; typedef environment local_environment; -typedef std::unordered_map hint_table; class parser { environment m_env; diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 607aac711..a2babde6f 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -200,9 +200,6 @@ struct unifier_fn { struct cnstr_cmp { int operator()(cnstr const & c1, cnstr const & c2) const { return c1.second < c2.second ? -1 : (c1.second == c2.second ? 0 : 1); } }; - struct unsigned_cmp { - int operator()(unsigned i1, unsigned i2) const { return i1 < i2 ? -1 : (i1 == i2 ? 0 : 1); } - }; typedef rb_tree cnstr_set; typedef rb_tree cnstr_idx_set; typedef rb_map name_to_cnstrs; diff --git a/src/tests/util/rb_map.cpp b/src/tests/util/rb_map.cpp index ebb1756b2..e3f749768 100644 --- a/src/tests/util/rb_map.cpp +++ b/src/tests/util/rb_map.cpp @@ -10,9 +10,6 @@ Author: Leonardo de Moura #include "util/rb_map.h" #include "util/name.h" using namespace lean; - -struct int_cmp { int operator()(int i1, int i2) const { return i1 < i2 ? -1 : (i1 > i2 ? 1 : 0); } }; - typedef rb_map int2name; static void tst0() { diff --git a/src/util/rb_tree.h b/src/util/rb_tree.h index d334dff2b..b593b4d5a 100644 --- a/src/util/rb_tree.h +++ b/src/util/rb_tree.h @@ -367,4 +367,11 @@ template rb_tree insert(rb_tree const & t, T const & v) { rb_tree r(t); r.insert(v); return r; } template rb_tree erase(rb_tree const & t, T const & v) { rb_tree r(t); r.erase(v); return r; } + +struct unsigned_cmp { + int operator()(unsigned i1, unsigned i2) const { return i1 < i2 ? -1 : (i1 == i2 ? 0 : 1); } +}; +struct int_cmp { + int operator()(int i1, int i2) const { return i1 < i2 ? -1 : (i1 == i2 ? 0 : 1); } +}; }