fix(frontends/lean): add 'eval' command

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<expr, level_param_names> parse_local_expr(parser & p) {
     expr e   = p.parse_expr();
     list<expr> 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));

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",

src/kernel/type_checker.h

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <memory>
 #include <utility>
 #include <algorithm>
+#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 F>
+    typename std::result_of<F()>::type with_params(level_param_names const & ps, F && f) {
+        flet<level_param_names const *> updt(m_params, &ps);
+        return f();
+    }
 };
 
 typedef std::shared_ptr<type_checker> type_checker_ref;

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

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;
+    std::unique_ptr<type_checker> m_tc;
-    name_generator m_ngen;
+    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); }
 }

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();
+expr normalize(environment const & env, level_param_names const & ls, expr const & e);
-void finalize_normalize();
 }

src/library/reducible.cpp

@@ -71,14 +71,18 @@ struct reducible_config {
 template class scoped_ext<reducible_config>;
 typedef scoped_ext<reducible_config> 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<type_checker> mk_type_checker(environment const & env, name_gene
                                                                                               true, pred)));
     }
 }
+std::unique_ptr<type_checker> 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);
+}
 }

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<type_checker> mk_type_checker(environment const & env, name_generator const & ngen,
                                               bool relax_main_opaque, bool only_main_reducible = false);
+std::unique_ptr<type_checker> mk_type_checker(environment const & env, bool relax_main_opaque, bool only_main_reducible = false);
 
 void initialize_reducible();
 void finalize_reducible();

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)

tests/lean/num5.lean.expected.out

@@ -0,0 +1,4 @@
+5
+13
+25
+eq.refl 2