refactor(frontends/lean/pp): use abstract_type_context instead of type_checker

src/frontends/lean/builtin_cmds.cpp

@@ -487,69 +487,6 @@ static environment init_hits_cmd(parser & p) {
     return module::declare_hits(p.env());
 }
 
-static environment compile_cmd(parser & p) {
-    name n = p.check_constant_next("invalid #compile command, constant expected");
-    declaration d = p.env().get(n);
-    buffer<name> aux_decls;
-    preprocess_rec(p.env(), d, aux_decls);
-    return p.env();
-}
-
-static void check_expr_and_print(parser & p, expr const & e) {
-    environment const & env = p.env();
-    type_checker tc(env);
-    expr t = tc.check_ignore_undefined_universes(e).first;
-    regular(env, p.ios(), tc.get_type_context()) << e << " : " << t << "\n";
-}
-
-static environment app_builder_cmd(parser & p) {
-    environment const & env = p.env();
-    auto pos = p.pos();
-    app_builder b(env);
-    name c = p.check_constant_next("invalid #app_builder command, constant expected");
-    bool has_mask = false;
-    buffer<bool> mask;
-    if (p.curr_is_token(get_lbracket_tk())) {
-        p.next();
-        has_mask = true;
-        while (true) {
-            name flag = p.check_constant_next("invalid #app_builder command, constant (true, false) expected");
-            mask.push_back(flag == get_true_name());
-            if (!p.curr_is_token(get_comma_tk()))
-                break;
-            p.next();
-        }
-        p.check_token_next(get_rbracket_tk(), "invalid #app_builder command, ']' expected");
-    }
-
-    buffer<expr> args;
-    while (true) {
-        expr e; level_param_names ls;
-        std::tie(e, ls) = parse_local_expr(p);
-        args.push_back(e);
-        if (!p.curr_is_token(get_comma_tk()))
-            break;
-        p.next();
-    }
-
-    if (has_mask && args.size() > mask.size())
-        throw parser_error(sstream() << "invalid #app_builder command, too many arguments", pos);
-
-    optional<expr> r;
-    if (has_mask)
-        r = b.mk_app(c, mask.size(), mask.data(), args.data());
-    else
-        r = b.mk_app(c, args.size(), args.data());
-
-    if (r) {
-        check_expr_and_print(p, *r);
-    } else {
-        throw parser_error(sstream() << "failed to build application for '" << c << "'", pos);
-    }
-
-    return env;
-}
-
 static environment simplify_cmd(parser & p) {
     name rel = p.check_constant_next("invalid #simplify command, constant expected");
     name ns = p.check_id_next("invalid #simplify command, id expected");

src/frontends/lean/pp.cpp

@@ -252,9 +252,9 @@ expr pretty_fn::purify(expr const & e) {
             if (!has_expr_metavar(e) && !has_local(e) && (!m_universes || !has_univ_metavar(e)))
                 return some_expr(e);
             else if (is_metavar(e) && m_purify_metavars)
-                return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e)), mlocal_type(e)));
+                return some_expr(mk_metavar(mk_metavar_name(mlocal_name(e)), m_ctx.infer(e)));
             else if (is_local(e))
-                return some_expr(mk_local(mlocal_name(e), mk_local_name(mlocal_name(e), local_pp_name(e)), mlocal_type(e), local_info(e)));
+                return some_expr(mk_local(mlocal_name(e), mk_local_name(mlocal_name(e), m_ctx.get_local_pp_name(e)), m_ctx.infer(e), local_info(e)));
             else if (is_constant(e))
                 return some_expr(update_constant(e, map(const_levels(e), [&](level const & l) { return purify(l); })));
             else if (is_sort(e))
@@ -321,8 +321,13 @@ bool pretty_fn::is_implicit(expr const & f) {
         return false;
     }
     try {
-        binder_info bi = binding_info(m_tc.ensure_pi(m_tc.infer(f).first).first);
+        expr t = m_ctx.relaxed_whnf(m_ctx.infer(f));
-        return bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit();
+        if (is_pi(t)) {
+            binder_info bi = binding_info(t);
+            return bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit();
+        } else {
+            return false;
+        }
     } catch (exception &) {
         return false;
     }
@@ -330,7 +335,10 @@ bool pretty_fn::is_implicit(expr const & f) {
 
 bool pretty_fn::is_prop(expr const & e) {
     try {
-        return m_env.impredicative() && m_tc.is_prop(e).first;
+        if (!m_env.impredicative())
+            return false;
+        expr t = m_ctx.relaxed_whnf(m_ctx.infer(e));
+        return t == mk_Prop();
     } catch (exception &) {
         return false;
     }
@@ -625,13 +633,13 @@ bool pretty_fn::has_implicit_args(expr const & f) {
         return false;
     }
     try {
-        expr type = m_tc.whnf(m_tc.infer(f).first).first;
+        expr type = m_ctx.relaxed_whnf(m_ctx.infer(f));
         while (is_pi(type)) {
             binder_info bi = binding_info(type);
             if (bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit())
                 return true;
-            expr local = mk_local(mk_fresh_name(), binding_name(type), binding_domain(type), binding_info(type));
+            expr local = m_ctx.mk_tmp_local(binding_name(type), binding_domain(type), binding_info(type));
-            type = m_tc.whnf(instantiate(binding_body(type), local)).first;
+            type = m_ctx.relaxed_whnf(instantiate(binding_body(type), local));
         }
         return false;
     } catch (exception &) {
@@ -950,10 +958,12 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & a
             return true;
         } else {
             try {
-                expr fn_type = m_tc.infer(e_fn).first;
+                expr fn_type = m_ctx.infer(e_fn);
                 unsigned j = 0;
                 for (unsigned i = 0; i < e_args.size(); i++) {
-                    fn_type                  = m_tc.ensure_pi(fn_type).first;
+                    fn_type = m_ctx.relaxed_whnf(fn_type);
+                    if (!is_pi(fn_type))
+                        return false;
                     expr const & body        = binding_body(fn_type);
                     binder_info const & info = binding_info(fn_type);
                     if ((!consume || closed(body)) && is_explicit(info)) {
@@ -966,7 +976,7 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & a
                     fn_type = instantiate(body, e_args[i]);
                 }
                 return j == p_args.size();
-            } catch (exception&) {
+            } catch (exception &) {
                 return false;
             }
         }
@@ -1279,8 +1289,8 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
-pretty_fn::pretty_fn(environment const & env, options const & o):
+pretty_fn::pretty_fn(environment const & env, options const & o, abstract_type_context & ctx):
-    m_env(env), m_tc(env), m_token_table(get_token_table(env)) {
+    m_env(env), m_ctx(ctx), m_token_table(get_token_table(env)) {
     set_options_core(o);
     m_meta_prefix   = "M";
     m_next_meta_idx = 1;
@@ -1380,8 +1390,8 @@ format pretty_fn::operator()(expr const & e) {
 }
 
 formatter_factory mk_pretty_formatter_factory() {
-    return [](environment const & env, options const & o, abstract_type_context &) { // NOLINT
+    return [](environment const & env, options const & o, abstract_type_context & ctx) { // NOLINT
-        auto fn_ptr = std::make_shared<pretty_fn>(env, o);
+        auto fn_ptr = std::make_shared<pretty_fn>(env, o, ctx);
         return formatter(o, [=](expr const & e, options const & new_o) {
                 fn_ptr->set_options(new_o);
                 return (*fn_ptr)(e);

src/frontends/lean/pp.h

@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 #include "util/sexpr/options.h"
 #include "util/sexpr/format.h"
 #include "kernel/environment.h"
-#include "kernel/type_checker.h"
+#include "kernel/abstract_type_context.h"
 #include "frontends/lean/token_table.h"
 
 namespace lean {
@@ -38,38 +38,38 @@ public:
         format const & fmt() const { return m_fmt; }
     };
 private:
-    environment         m_env;
+    environment             m_env;
-    type_checker        m_tc;
+    abstract_type_context & m_ctx;
-    token_table const & m_token_table;
+    token_table const &     m_token_table;
-    unsigned            m_num_steps;
+    unsigned                m_num_steps;
-    unsigned            m_depth;
+    unsigned                m_depth;
-    name                m_meta_prefix;
+    name                    m_meta_prefix;
-    unsigned            m_next_meta_idx;
+    unsigned                m_next_meta_idx;
-    name_map<name>      m_purify_meta_table;
+    name_map<name>          m_purify_meta_table;
-    name_set            m_purify_used_metas;
+    name_set                m_purify_used_metas;
-    name_map<name>      m_purify_local_table;
+    name_map<name>          m_purify_local_table;
-    name_set            m_purify_used_locals;
+    name_set                m_purify_used_locals;
     // cached configuration
-    options             m_options;
+    options                 m_options;
-    unsigned            m_indent;
+    unsigned                m_indent;
-    unsigned            m_max_depth;
+    unsigned                m_max_depth;
-    unsigned            m_max_steps;
+    unsigned                m_max_steps;
-    bool                m_implict;          //!< if true show implicit arguments
+    bool                    m_implict;          //!< if true show implicit arguments
-    bool                m_unicode;          //!< if true use unicode chars
+    bool                    m_unicode;          //!< if true use unicode chars
-    bool                m_coercion;         //!< if true show coercions
+    bool                    m_coercion;         //!< if true show coercions
-    bool                m_num_nat_coe;      //!< truen when !m_coercion && env has coercion from num -> nat
+    bool                    m_num_nat_coe;      //!< truen when !m_coercion && env has coercion from num -> nat
-    bool                m_notation;
+    bool                    m_notation;
-    bool                m_universes;
+    bool                    m_universes;
-    bool                m_full_names;
+    bool                    m_full_names;
-    bool                m_private_names;
+    bool                    m_private_names;
-    bool                m_metavar_args;
+    bool                    m_metavar_args;
-    bool                m_purify_metavars;
+    bool                    m_purify_metavars;
-    bool                m_purify_locals;
+    bool                    m_purify_locals;
-    bool                m_beta;
+    bool                    m_beta;
-    bool                m_numerals;
+    bool                    m_numerals;
-    bool                m_abbreviations;
+    bool                    m_abbreviations;
-    bool                m_hide_full_terms;
+    bool                    m_hide_full_terms;
-    bool                m_preterm;
+    bool                    m_preterm;
 
     name mk_metavar_name(name const & m);
     name mk_local_name(name const & n, name const & suggested);
@@ -122,7 +122,7 @@ private:
     void set_options_core(options const & o);
 
 public:
-    pretty_fn(environment const & env, options const & o);
+    pretty_fn(environment const & env, options const & o, abstract_type_context & ctx);
     result pp(expr const & e, bool ignore_hide = false);
     void set_options(options const & o);
     options const & get_options() const { return m_options; }

src/frontends/lean/token_table.cpp

@@ -119,8 +119,7 @@ void init_token_table(token_table & t) {
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
          "multiple_instances", "find_decl", "attribute", "persistent",
          "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
-         "#compile", "#decl_stats", "#relevant_thms", "#simplify", "#app_builder", "#refl", "#symm",
+         "#compile", "#decl_stats", "#relevant_thms", "#simplify", "#normalizer", "#abstract_expr", "#unify",
-         "#trans", "#congr", "#hcongr", "#congr_simp", "#congr_rel", "#normalizer", "#abstract_expr", "#unify",
          "#defeq_simplify", nullptr};
 
     pair<char const *, char const *> aliases[] =

src/kernel/abstract_type_context.h

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "util/fresh_name.h"
 #include "kernel/expr.h"
 
 namespace lean {
@@ -20,11 +21,17 @@ public:
     virtual ~abstract_type_context() {}
     virtual environment const & env() const = 0;
     virtual expr whnf(expr const & e) = 0;
+    virtual expr relaxed_whnf(expr const & e) { return whnf(e); }
     virtual bool is_def_eq(expr const & e1, expr const & e2) = 0;
+    virtual bool relaxed_is_def_eq(expr const & e1, expr const & e2) { return is_def_eq(e1, e2); }
     virtual expr infer(expr const & e) = 0;
     /** \brief Simular to \c infer, but also performs type checking.
         \remark Default implementation just invokes \c infer. */
     virtual expr check(expr const & e) { return infer(e); }
     virtual optional<expr> is_stuck(expr const &) { return none_expr(); }
+    virtual name get_local_pp_name(expr const & e) { return local_pp_name(e); }
+    virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) {
+        return mk_local(mk_fresh_name(), pp_name, type, bi);
+    }
 };
 }

src/library/blast/blast.cpp

@@ -245,11 +245,14 @@ class blastenv {
 
         virtual expr infer_metavar(expr const & m) const override {
             // Remark: we do not tolerate external meta-variables here.
-            lean_assert(is_mref(m));
+            if (is_mref(m)) {
-            state const & s = m_benv.m_curr_state;
+                state const & s = m_benv.m_curr_state;
-            metavar_decl const * d = s.get_metavar_decl(m);
+                metavar_decl const * d = s.get_metavar_decl(m);
-            lean_assert(d);
+                lean_assert(d);
-            return d->get_type();
+                return d->get_type();
+            } else {
+                return mlocal_type(m);
+            }
         }
 
         virtual level mk_uvar() override {

src/library/tactic/contradiction_tactic.cpp

@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 tactic contradiction_tactic() {
-    auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
+    auto fn = [=](environment const & env, io_state const &, proof_state const & s) {
         goals const & gs = s.get_goals();
         if (empty(gs)) {
             throw_no_goal_if_enabled(s);

src/library/type_context.h

@@ -329,7 +329,7 @@ public:
 
     /** \brief Create a temporary local constant using the given pretty print name.
         The pretty printing name has not semantic significance. */
-    expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info());
+    virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) override;
 
     /** \brief Create a temporary local constant based on the domain of the given binding (lambda/Pi) expression */
     expr mk_tmp_local_from_binding(expr const & b) {
@@ -440,10 +440,10 @@ public:
     expr instantiate_uvars_mvars(expr const & e);
 
     /** \brief Put the given term in weak-head-normal-form (modulo is_opaque predicate) */
-    expr whnf(expr const & e);
+    virtual expr whnf(expr const & e) override;
 
     /** \brief Similar to previous method but ignores the is_extra_opaque predicate. */
-    expr relaxed_whnf(expr const & e);
+    virtual expr relaxed_whnf(expr const & e) override;
 
     /** \brief Return true if \c e is a proposition */
     bool is_prop(expr const & e);
@@ -462,9 +462,9 @@ public:
 
         It is precise if \c e1 and \c e2 do not contain metavariables.
      */
-    bool is_def_eq(expr const & e1, expr const & e2);
+    virtual bool is_def_eq(expr const & e1, expr const & e2) override;
     /** \brief Similar to \c is_def_eq, but sets m_relax_is_opaque */
-    bool relaxed_is_def_eq(expr const & e1, expr const & e2);
+    virtual bool relaxed_is_def_eq(expr const & e1, expr const & e2) override;
 
     /** \brief Return the universe level for type A. If A is not a type return none. */
     optional<level> get_level_core(expr const & A);