From 8e7aac1eb4f3e720797f2647014ab6de3d9ca51a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Sep 2014 20:16:03 -0700 Subject: [PATCH] fix(frontends/lean): add 'eval' command --- src/frontends/lean/builtin_cmds.cpp | 21 +++++++++++++++++++-- src/frontends/lean/token_table.cpp | 2 +- src/kernel/type_checker.h | 7 +++++++ src/library/init_module.cpp | 3 --- src/library/normalize.cpp | 25 +++++++++++-------------- src/library/normalize.h | 3 +-- src/library/reducible.cpp | 7 +++++++ src/library/reducible.h | 1 + tests/lean/num5.lean | 7 +++++++ tests/lean/num5.lean.expected.out | 4 ++++ 10 files changed, 58 insertions(+), 22 deletions(-) create mode 100644 tests/lean/num5.lean create mode 100644 tests/lean/num5.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 47f4d80f5..91350c1c7 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "library/locals.h" #include "library/coercion.h" #include "library/reducible.h" +#include "library/normalize.h" #include "frontends/lean/util.h" #include "frontends/lean/parser.h" #include "frontends/lean/calc.h" @@ -83,14 +84,21 @@ environment end_scoped_cmd(parser & p) { } } -environment check_cmd(parser & p) { +/** \brief Auxiliary function for check/eval */ +static std::tuple parse_local_expr(parser & p) { expr e = p.parse_expr(); list ctx = locals_to_context(e, p); level_param_names ls = to_level_param_names(collect_univ_params(e)); level_param_names new_ls; std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx); + return std::make_tuple(e, append(ls, new_ls)); +} + +environment check_cmd(parser & p) { + expr e; level_param_names ls; + std::tie(e, ls) = parse_local_expr(p); auto tc = mk_type_checker(p.env(), p.mk_ngen(), true); - expr type = tc->check(e, append(ls, new_ls)).first; + expr type = tc->check(e, ls).first; auto reg = p.regular_stream(); formatter const & fmt = reg.get_formatter(); options opts = p.ios().get_options(); @@ -100,6 +108,14 @@ environment check_cmd(parser & p) { return p.env(); } +environment eval_cmd(parser & p) { + expr e; level_param_names ls; + std::tie(e, ls) = parse_local_expr(p); + expr r = normalize(p.env(), ls, e); + p.regular_stream() << r << endl; + return p.env(); +} + environment exit_cmd(parser &) { throw interrupt_parser(); } @@ -358,6 +374,7 @@ void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("namespace", "open a new namespace", namespace_cmd)); add_cmd(r, cmd_info("end", "close the current namespace/section", end_scoped_cmd)); add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd)); + add_cmd(r, cmd_info("eval", "evaluate given expression", eval_cmd)); add_cmd(r, cmd_info("coercion", "add a new coercion", coercion_cmd)); add_cmd(r, cmd_info("reducible", "mark definitions as reducible/irreducible for automation", reducible_cmd)); add_cmd(r, cmd_info("irreducible", "mark definitions as irreducible for automation", irreducible_cmd)); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 9f45b84d8..aa125d020 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -79,7 +79,7 @@ void init_token_table(token_table & t) { char const * commands[] = {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion", "variables", "[persistent]", "[visible]", "[instance]", "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "reducible", "irreducible", - "evaluate", "check", "print", "end", "namespace", "section", "import", + "evaluate", "check", "eval", "print", "end", "namespace", "section", "import", "inductive", "record", "renaming", "extends", "structure", "module", "universe", "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context", "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "tactic_hint", diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index a07358eac..c631cb7e4 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include "util/flet.h" #include "util/name_generator.h" #include "util/name_set.h" #include "kernel/environment.h" @@ -204,6 +205,12 @@ public: bool is_opaque(declaration const & d) const; /** \brief Return true iff the constant \c c is opaque with respect to this type checker. */ bool is_opaque(expr const & c) const; + + template + typename std::result_of::type with_params(level_param_names const & ps, F && f) { + flet updt(m_params, &ps); + return f(); + } }; typedef std::shared_ptr type_checker_ref; diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index a4ff4c763..184fe6a52 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -25,7 +25,6 @@ Author: Leonardo de Moura #include "library/io_state.h" #include "library/kernel_bindings.h" #include "library/match.h" -#include "library/normalize.h" #include "library/sorry.h" #include "library/placeholder.h" #include "library/print.h" @@ -35,7 +34,6 @@ void initialize_library_module() { initialize_print(); initialize_placeholder(); initialize_match(); - initialize_normalize(); initialize_kernel_bindings(); initialize_io_state(); initialize_unifier(); @@ -81,7 +79,6 @@ void finalize_library_module() { finalize_unifier(); finalize_io_state(); finalize_kernel_bindings(); - finalize_normalize(); finalize_match(); finalize_placeholder(); finalize_print(); diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index 1a9510f7c..401b48a73 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -8,21 +8,12 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" +#include "library/reducible.h" namespace lean { -static name * g_tmp_prefix = nullptr; - -void initialize_normalize() { - g_tmp_prefix = new name(name::mk_internal_unique_name()); -} - -void finalize_normalize() { - delete g_tmp_prefix; -} - class normalize_fn { - type_checker m_tc; - name_generator m_ngen; + std::unique_ptr m_tc; + name_generator m_ngen; expr normalize_binding(expr const & e) { expr d = normalize(binding_domain(e)); @@ -40,7 +31,7 @@ class normalize_fn { } expr normalize(expr e) { - e = m_tc.whnf(e).first; + e = m_tc->whnf(e).first; switch (e.kind()) { case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Macro: @@ -54,9 +45,15 @@ class normalize_fn { } public: - normalize_fn(environment const & env):m_tc(env), m_ngen(*g_tmp_prefix) {} + normalize_fn(environment const & env):m_tc(mk_type_checker(env, true)), m_ngen(m_tc->mk_ngen()) {} expr operator()(expr const & e) { return normalize(e); } + expr operator()(level_param_names const & ls, expr const & e) { + return m_tc->with_params(ls, [&]() { + return normalize(e); + }); + } }; expr normalize(environment const & env, expr const & e) { return normalize_fn(env)(e); } +expr normalize(environment const & env, level_param_names const & ls, expr const & e) { return normalize_fn(env)(ls, e); } } diff --git a/src/library/normalize.h b/src/library/normalize.h index a0140b07d..be8f77cce 100644 --- a/src/library/normalize.h +++ b/src/library/normalize.h @@ -10,6 +10,5 @@ Author: Leonardo de Moura namespace lean { /** \brief Return the \c e normal form with respect to the environment \c env. */ expr normalize(environment const & env, expr const & e); -void initialize_normalize(); -void finalize_normalize(); +expr normalize(environment const & env, level_param_names const & ls, expr const & e); } diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp index c5f90304e..5fda39735 100644 --- a/src/library/reducible.cpp +++ b/src/library/reducible.cpp @@ -71,14 +71,18 @@ struct reducible_config { template class scoped_ext; typedef scoped_ext reducible_ext; +static name * g_tmp_prefix = nullptr; + void initialize_reducible() { g_class_name = new name("reducible"); g_key = new std::string("redu"); + g_tmp_prefix = new name(name::mk_internal_unique_name()); reducible_ext::initialize(); } void finalize_reducible() { reducible_ext::finalize(); + delete g_tmp_prefix; delete g_key; delete g_class_name; } @@ -128,4 +132,7 @@ std::unique_ptr mk_type_checker(environment const & env, name_gene true, pred))); } } +std::unique_ptr mk_type_checker(environment const & env, bool relax_main_opaque, bool only_main_reducible) { + return mk_type_checker(env, name_generator(*g_tmp_prefix), relax_main_opaque, only_main_reducible); +} } diff --git a/src/library/reducible.h b/src/library/reducible.h index ce640a392..6b35cea2e 100644 --- a/src/library/reducible.h +++ b/src/library/reducible.h @@ -36,6 +36,7 @@ bool is_reducible_off(environment const & env, name const & n); /** \brief Create a type checker that takes the "reducibility" hints into account. */ std::unique_ptr mk_type_checker(environment const & env, name_generator const & ngen, bool relax_main_opaque, bool only_main_reducible = false); +std::unique_ptr mk_type_checker(environment const & env, bool relax_main_opaque, bool only_main_reducible = false); void initialize_reducible(); void finalize_reducible(); diff --git a/tests/lean/num5.lean b/tests/lean/num5.lean new file mode 100644 index 000000000..e10ac4cfb --- /dev/null +++ b/tests/lean/num5.lean @@ -0,0 +1,7 @@ +import data.num +open num + +eval 3+2 +eval 3+2*5 +eval 5*5 +eval eq.rec (eq.refl 2) (eq.refl 2) diff --git a/tests/lean/num5.lean.expected.out b/tests/lean/num5.lean.expected.out new file mode 100644 index 000000000..c689d498a --- /dev/null +++ b/tests/lean/num5.lean.expected.out @@ -0,0 +1,4 @@ +5 +13 +25 +eq.refl 2