feat(library/app_builder): new app_builder on top of type_context

The new version is more robust, and invokes type class resolution if needed.

src/frontends/lean/builtin_cmds.cpp

@@ -1141,22 +1141,26 @@ static environment relevant_thms_cmd(parser & p) {
 
 static environment app_builder_cmd(parser & p) {
     environment const & env = p.env();
-    type_checker tc(env);
+    auto pos = p.pos();
-    app_builder b(tc);
+    app_builder b(env);
     name c = p.check_constant_next("invalid #app_builder command, constant expected");
     p.check_token_next(get_lparen_tk(), "invalid #app_builder command, '(' expected");
     buffer<expr> args;
     while (true) {
-        args.push_back(p.parse_expr());
+        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();
     }
     p.check_token_next(get_rparen_tk(), "invalid #app_builder command, ')' expected");
     if (auto r = b.mk_app(c, args.size(), args.data())) {
-        p.regular_stream() << *r << "\n";
+        type_checker tc(env);
+        expr t = tc.check_ignore_undefined_universes(*r).first;
+        p.regular_stream() << *r << " : " << t << "\n";
     } else {
-        p.regular_stream() << "<failed>\n";
+        throw parser_error(sstream() << "failed to build application for '" << c << "'", pos);
     }
     return env;
 }

src/library/app_builder.cpp

@@ -10,241 +10,212 @@ Author: Leonardo de Moura
 #include "library/match.h"
 #include "library/app_builder.h"
 #include "library/kernel_bindings.h"
+#include "library/tmp_type_context.h"
 
 namespace lean {
-
 struct app_builder::imp {
-    // For each declaration we associate the number of explicit arguments provided to
+    tmp_type_context m_ctx;
-    // it, and which of them are used to infer the implicit arguments.
+
-    struct decl_info {
+    struct entry {
-        unsigned       m_nargs; // total number of explicit arguments
+        unsigned             m_num_umeta;
-        list<unsigned> m_used_idxs; // which ones are used to infer implicit arguments
+        unsigned             m_num_emeta;
-        decl_info(unsigned nargs, list<unsigned> const & used_idxs):
+        expr                 m_app;
-            m_nargs(nargs), m_used_idxs(used_idxs) {}
+        list<optional<expr>> m_inst_args; // "mask" of implicit instance arguments
-        decl_info() {}
+        list<expr>           m_expl_args; // metavars for explicit arguments
+
+        /*
+          IMPORTANT: for m_inst_args we store the arguments in reverse order.
+          For example, the first element in the list indicates whether the last argument
+          is an instance implicit argument or not. If it is not none, then the element
+          is the associated metavariable
+
+          m_expl_args are also stored in reverse order
+        */
     };
 
-    struct cache_key {
+    struct key {
-        name         m_name;
+        name       m_name;
-        list<expr>   m_arg_types;
+        unsigned   m_num_expl;
-        unsigned     m_hash;
+        unsigned   m_hash;
-        cache_key(name const & n, unsigned num_arg_types, expr const * arg_types):
+        // If nil, then the mask is composed of the last m_num_expl arguments.
-            m_name(n), m_arg_types(to_list(arg_types, arg_types + num_arg_types)) {
+        // If nonnil, then the mask is NOT of the form [false*, true*]
-            m_hash      = m_name.hash();
+        list<bool> m_mask;
-            for (unsigned i = 0; i < num_arg_types; i++)
+
-                m_hash  = hash(m_hash, arg_types[i].hash());
+        static bool is_simple(list<bool> const & mask) {
+            bool found_true = false;
+            for (bool b : mask) {
+                if (b) {
+                    found_true = true;
+                } else if (found_true) {
+                    // found (true, false)
+                    return false;
+                }
+            }
+            return true;
         }
-    };
+
-    struct cache_key_hash_fn {
+        key(name const & c, unsigned n):
-        unsigned operator()(cache_key const & e) const { return e.m_hash; }
+            m_name(c), m_num_expl(n),
-    };
+            m_hash(::lean::hash(c.hash(), n)) {
-    struct cache_key_equal_fn {
+        }
-        bool operator()(cache_key const & e1, cache_key const & e2) const {
+
-            return
+        key(name const & c, list<bool> const & m):
-                e1.m_name == e2.m_name &&
+            m_name(c), m_num_expl(length(m)) {
-                e1.m_arg_types == e2.m_arg_types;
+            m_hash = ::lean::hash(c.hash(), m_num_expl);
+            if (!is_simple(m)) {
+                m_mask = m;
+                for (bool b : m) {
+                    if (b)
+                        m_hash = ::lean::hash(m_hash, 17u);
+                    else
+                        m_hash = ::lean::hash(m_hash, 31u);
+                }
+            }
+        }
+
+        bool check_invariant() const {
+            lean_assert(empty(m_mask) || length(m_mask) == m_num_expl);
+            lean_assert(empty(m_mask) || !is_simple(m_mask));
+            return true;
+        }
+
+        unsigned hash() const {
+            return m_hash;
+        }
+
+        friend bool operator==(key const & k1, key const & k2) {
+            return k1.m_name == k2.m_name && k1.m_num_expl == k2.m_num_expl && k1.m_mask == k2.m_mask;
         }
     };
 
-    // The cache stores a mapping (decl + type of explicit arguments ==> term t).
+    struct key_hash_fn {
-    // If t is closed term, then we obtain the final application by using
+        unsigned operator()(key const & k) const { return k.hash(); }
-    //       mk_app(t, explicit_args)
+    };
-    // If t contains free variables, then we obtain the final application by using
-    //       instantiate(t, explicit_args)
-    typedef scoped_map<cache_key, expr, cache_key_hash_fn, cache_key_equal_fn> cache;
 
-    type_checker &      m_tc;
+    typedef std::unordered_map<key, entry, key_hash_fn> map;
-    whnf_match_plugin   m_plugin;
-    name_map<decl_info> m_decl_info;
-    cache               m_cache;
-    buffer<levels>      m_levels;
 
-    imp(type_checker & tc):m_tc(tc), m_plugin(tc) {
+    map m_map;
-        m_levels.push_back(levels());
+
+    imp(environment const & env, io_state const & ios, reducible_behavior b):
+        m_ctx(env, ios, b) {
     }
 
-    // Make sure m_levels contains at least nlvls metavariable universe levels
+    levels mk_metavars(declaration const & d, buffer<expr> & mvars, buffer<optional<expr>> & inst_args) {
-    void ensure_levels(unsigned nlvls) {
+        m_ctx.clear();
-        while (m_levels.size() <= nlvls) {
+        unsigned num_univ = d.get_num_univ_params();
-            level new_lvl   = mk_idx_metauniv(m_levels.size() - 1);
+        buffer<level> lvls_buffer;
-            levels new_lvls = append(m_levels.back(), levels(new_lvl));
+        for (unsigned i = 0; i < num_univ; i++) {
-            m_levels.push_back(new_lvls);
+            lvls_buffer.push_back(m_ctx.mk_uvar());
+        }
+        levels lvls = to_list(lvls_buffer);
+        expr type   = m_ctx.whnf(instantiate_type_univ_params(d, lvls));
+        while (is_pi(type)) {
+            expr mvar = m_ctx.mk_mvar(binding_domain(type));
+            if (binding_info(type).is_inst_implicit())
+                inst_args.push_back(some_expr(mvar));
+            else
+                inst_args.push_back(none_expr());
+            mvars.push_back(mvar);
+            type = m_ctx.whnf(instantiate(binding_body(type), mvar));
+        }
+        return lvls;
+    }
+
+    optional<entry> get_entry(name const & c, unsigned nargs) {
+        key k(c, nargs);
+        lean_assert(k.check_invariant());
+        auto it = m_map.find(k);
+        if (it == m_map.end()) {
+            if (auto d = m_ctx.env().find(c)) {
+                buffer<expr> mvars;
+                buffer<optional<expr>> inst_args;
+                levels lvls = mk_metavars(*d, mvars, inst_args);
+                if (nargs > mvars.size())
+                    return optional<entry>(); // insufficient number of arguments
+                entry e;
+                e.m_num_umeta = d->get_num_univ_params();
+                e.m_num_emeta = mvars.size();
+                e.m_app       = ::lean::mk_app(mk_constant(c, lvls), mvars);
+                e.m_inst_args = reverse_to_list(inst_args.begin(), inst_args.end());
+                e.m_expl_args = reverse_to_list(mvars.begin() + mvars.size() - nargs, mvars.end());
+                m_map.insert(mk_pair(k, e));
+                return optional<entry>(e);
+            } else {
+                return optional<entry>(); // unknown decl
+            }
+        } else {
+            return optional<entry>(it->second);
         }
     }
 
-    // We say the given mask is simple if it is of the form (false*, true*).
+    bool check_all_assigned(entry const & e) {
-    // That is, a block of false followed by a blocked of true
+        lean_assert(e.m_num_emeta == length(e.m_inst_args));
-    static bool is_simple_mask(buffer<bool> & explicit_mask) {
+        // recall that the flags at e.m_inst_args are stored in reverse order.
-        bool found_true = false;
+        // For example, the first flag in the list indicates whether the last argument
-        for (bool const & b : explicit_mask) {
+        // is an instance implicit argument or not.
-            if (b)
+        unsigned i = e.m_num_emeta;
-                found_true = true;
+        for (optional<expr> const & inst_arg : e.m_inst_args) {
-            else if (found_true)
+            lean_assert(i > 0);
+            --i;
+            if (inst_arg) {
+                expr type = m_ctx.instantiate_uvars_mvars(mlocal_type(*inst_arg));
+                if (auto v = m_ctx.mk_class_instance(type)) {
+                    if (!m_ctx.force_assign(*inst_arg, *v))
+                        return false;
+                } else {
+                    return false;
+                }
+            }
+            if (!m_ctx.is_mvar_assigned(i))
+                return false;
+        }
+        for (unsigned i = 0; i < e.m_num_umeta; i++) {
+            if (!m_ctx.is_uvar_assigned(i))
                 return false;
         }
         return true;
     }
 
-    void save_decl_info(declaration const & d, unsigned nargs, buffer<unsigned> const & used_idxs) {
+    optional<expr> mk_app(name const & c, unsigned nargs, expr const * args) {
-        if (!m_decl_info.contains(d.get_name())) {
+        optional<entry> e = get_entry(c, nargs);
-            m_decl_info.insert(d.get_name(), decl_info(nargs, to_list(used_idxs)));
+        if (!e)
-        }
-    }
-
-    optional<expr> mk_app_core(declaration const & d, unsigned nargs, expr const * args, bool use_cache) {
-        unsigned num_univs = d.get_num_univ_params();
-        ensure_levels(num_univs);
-        expr type  = instantiate_type_univ_params(d, m_levels[num_univs]);
-        buffer<optional<level>> lsubst;
-        buffer<optional<expr>>  esubst;
-        lsubst.resize(num_univs, none_level());
-        constraint_seq cs;
-        buffer<unsigned> used_idxs;
-        buffer<expr>     used_types;
-        buffer<bool>     explicit_mask;
-        buffer<expr> domain_types;
-        unsigned idx = 0;
-        while (is_pi(type)) {
-            explicit_mask.push_back(is_explicit(binding_info(type)));
-            esubst.push_back(none_expr());
-            domain_types.push_back(binding_domain(type));
-            // TODO(Leo): perhaps, we should cache the result of this while-loop.
-            // The result of this computation can be reused in future calls.
-            expr meta = mk_idx_metavar(idx, binding_domain(type));
-            idx++;
-            type = instantiate(binding_body(type), meta);
-        }
-        unsigned i = domain_types.size();
-        unsigned j = nargs;
-        while (i > 0) {
-            --i;
-            if (explicit_mask[i]) {
-                if (j == 0)
-                    return none_expr();
-                --j;
-                expr arg_type = m_tc.infer(args[j], cs);
-                if (cs)
-                    return none_expr();
-                bool assigned = false;
-                if (!match(domain_types[i], arg_type, lsubst, esubst,
-                           nullptr, nullptr, &m_plugin, &assigned))
-                    return none_expr();
-                if (assigned && use_cache) {
-                    used_idxs.push_back(j);
-                    used_types.push_back(arg_type);
-                }
-                esubst[i] = some_expr(args[j]);
-            } else {
-                if (!esubst[i])
-                    return none_expr();
-                expr arg_type = m_tc.infer(*esubst[i], cs);
-                if (cs)
-                    return none_expr();
-                if (!match(domain_types[i], arg_type, lsubst, esubst,
-                           nullptr, nullptr, &m_plugin))
-                    return none_expr();
-            }
-        }
-        bool has_unassigned_lvls = std::find(lsubst.begin(), lsubst.end(), none_level()) != lsubst.end();
-        if (j > 0 || has_unassigned_lvls)
             return none_expr();
-        if (use_cache)
+        m_ctx.clear();
-            save_decl_info(d, nargs, used_idxs);
+        m_ctx.set_next_uvar_idx(e->m_num_umeta);
-        buffer<level> r_lvls;
+        m_ctx.set_next_mvar_idx(e->m_num_emeta);
-        for (optional<level> const & l : lsubst)
+        unsigned i = nargs;
-            r_lvls.push_back(*l);
+        for (auto m : e->m_expl_args) {
-        buffer<expr> r_args;
+            if (i == 0)
-        for (optional<expr> const & o : esubst)
+                return none_expr();
-            r_args.push_back(*o);
+            --i;
-        lean_assert(explicit_mask.size() == r_args.size());
+            if (!m_ctx.assign(m, args[i]))
-        if (!use_cache) {
+                return none_expr();
-            return some_expr(::lean::mk_app(mk_constant(d.get_name(), to_list(r_lvls)), r_args.size(), r_args.data()));
-        } else if (is_simple_mask(explicit_mask)) {
-            expr f = ::lean::mk_app(mk_constant(d.get_name(), to_list(r_lvls)), r_args.size() - nargs, r_args.data());
-            if (use_cache) {
-                cache_key k(d.get_name(), used_types.size(), used_types.data());
-                m_cache.insert(k, f);
-            }
-            return some_expr(::lean::mk_app(f, nargs, r_args.end() - nargs));
-        } else {
-            buffer<expr> imp_args;
-            buffer<expr> expl_args;
-            for (unsigned i = 0; i < explicit_mask.size(); i++) {
-                if (explicit_mask[i]) {
-                    imp_args.push_back(mk_var(expl_args.size()));
-                    expl_args.push_back(r_args[i]);
-                } else {
-                    imp_args.push_back(r_args[i]);
-                }
-            }
-            expr f = ::lean::mk_app(mk_constant(d.get_name(), to_list(r_lvls)), imp_args.size(), imp_args.data());
-            if (use_cache) {
-                cache_key k(d.get_name(), used_types.size(), used_types.data());
-                m_cache.insert(k, f);
-            }
-            return some_expr(instantiate(f, expl_args.size(), expl_args.data()));
         }
+        if (!check_all_assigned(*e))
+            return none_expr();
+        return some_expr(m_ctx.instantiate_uvars_mvars(e->m_app));
     }
 
-    optional<expr> mk_app(declaration const & d, unsigned nargs, expr const * args, bool use_cache) {
+    optional<expr> mk_app(name const & /* c */, unsigned /* mask_sz */, bool const * /* mask */, expr const * /* args */) {
-        if (use_cache) {
+        return none_expr();
-            if (auto info = m_decl_info.find(d.get_name())) {
-                if (info->m_nargs != nargs)
-                    return none_expr();
-                buffer<expr> arg_types;
-                constraint_seq cs;
-                for (unsigned idx : info->m_used_idxs) {
-                    lean_assert(idx < nargs);
-                    expr t = m_tc.infer(args[idx], cs);
-                    if (cs)
-                        return none_expr(); // constraint was generated
-                    arg_types.push_back(t);
-                }
-                cache_key k(d.get_name(), arg_types.size(), arg_types.data());
-                auto it = m_cache.find(k);
-                if (it != m_cache.end()) {
-                    if (closed(it->second))
-                        return some_expr(::lean::mk_app(it->second, nargs, args));
-                    else
-                        return some_expr(instantiate(it->second, nargs, args));
-                } else {
-                    return mk_app_core(d, nargs, args, use_cache);
-                }
-            }
-        }
-        return mk_app_core(d, nargs, args, use_cache);
-    }
-
-    void push() {
-        m_cache.push();
-    }
-
-    void pop() {
-        m_cache.pop();
     }
 };
 
-app_builder::app_builder(type_checker & tc):m_ptr(new imp(tc)) {}
+app_builder::app_builder(environment const & env, io_state const & ios, reducible_behavior b):
+    m_ptr(new imp(env, ios, b)) {
+}
+
+app_builder::app_builder(environment const & env, reducible_behavior b):
+    app_builder(env, get_dummy_ios(), b) {
+}
+
 app_builder::~app_builder() {}
-optional<expr> app_builder::mk_app(declaration const & d, unsigned nargs, expr const * args, bool use_cache) {
+
-    return m_ptr->mk_app(d, nargs, args, use_cache);
+optional<expr> app_builder::mk_app(name const & c, unsigned nargs, expr const * args) {
+    return m_ptr->mk_app(c, nargs, args);
 }
-optional<expr> app_builder::mk_app(name const & n, unsigned nargs, expr const * args, bool use_cache) {
+
-    declaration const & d = m_ptr->m_tc.env().get(n);
+optional<expr> app_builder::mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args) {
-    return mk_app(d, nargs, args, use_cache);
+    return m_ptr->mk_app(c, mask_sz, mask, args);
 }
-optional<expr> app_builder::mk_app(name const & n, std::initializer_list<expr> const & args, bool use_cache) {
-    return mk_app(n, args.size(), args.begin(), use_cache);
-}
-optional<expr> app_builder::mk_app(name const & n, expr const & a1, bool use_cache) {
-    return mk_app(n, {a1}, use_cache);
-}
-optional<expr> app_builder::mk_app(name const & n, expr const & a1, expr const & a2, bool use_cache) {
-    return mk_app(n, {a1, a2}, use_cache);
-}
-optional<expr> app_builder::mk_app(name const & n, expr const & a1, expr const & a2, expr const & a3, bool use_cache) {
-    return mk_app(n, {a1, a2, a3}, use_cache);
-}
-void app_builder::push() { m_ptr->push(); }
-void app_builder::pop() { m_ptr->pop(); }
 }

src/library/app_builder.h

@@ -6,7 +6,9 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <memory>
-#include "kernel/type_checker.h"
+#include "kernel/environment.h"
+#include "library/io_state.h"
+#include "library/reducible.h"
 
 namespace lean {
 /** \brief Helper for creating simple applications where some arguments are inferred using
@@ -27,7 +29,8 @@ class app_builder {
     struct imp;
     std::unique_ptr<imp> m_ptr;
 public:
-    app_builder(type_checker & tc);
+    app_builder(environment const & env, io_state const & ios, reducible_behavior b = UnfoldReducible);
+    app_builder(environment const & env, reducible_behavior b = UnfoldReducible);
     ~app_builder();
     /** \brief Create an application (d.{_ ... _} _ ... _ args[0] ... args[nargs-1]).
         The missing arguments and universes levels are inferred using type inference.
@@ -38,21 +41,24 @@ public:
 
         \remark This methods uses just higher-order pattern matching.
     */
-    optional<expr> mk_app(declaration const & d, unsigned nargs, expr const * args, bool use_cache = true);
+    optional<expr> mk_app(name const & c, unsigned nargs, expr const * args);
-    optional<expr> mk_app(name const & n, unsigned nargs, expr const * args, bool use_cache = true);
-    optional<expr> mk_app(name const & n, std::initializer_list<expr> const & args, bool use_cache = true);
-    optional<expr> mk_app(name const & n, expr const & a1, bool use_cache = true);
-    optional<expr> mk_app(name const & n, expr const & a1, expr const & a2, bool use_cache = true);
-    optional<expr> mk_app(name const & n, expr const & a1, expr const & a2, expr const & a3, bool use_cache = true);
-    /** \brief Create a backtracking point for cached information.
-        \remark This method does not invoke tc->push()
-    */
-    void push();
-    /** \brief Restore backtracking point, values cached between this push and the corresponding pop
-        are removed from the cache.
 
-        \remark This method does not invoke tc->pop()
+    optional<expr> mk_app(name const & c, std::initializer_list<expr> const & args) {
-    */
+        return mk_app(c, args.size(), args.begin());
-    void pop();
+    }
+
+    optional<expr> mk_app(name const & c, expr const & a1) {
+        return mk_app(c, {a1});
+    }
+
+    optional<expr> mk_app(name const & c, expr const & a1, expr const & a2) {
+        return mk_app(c, {a1, a2});
+    }
+
+    optional<expr> mk_app(name const & c, expr const & a1, expr const & a2, expr const & a3) {
+        return mk_app(c, {a1, a2, a3});
+    }
+
+    optional<expr> mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args);
 };
 }

src/library/type_context.cpp

@@ -722,6 +722,19 @@ bool type_context::process_assignment(expr const & ma, expr const & v) {
     }
 }
 
+bool type_context::assign(expr const & ma, expr const & v) {
+    expr const & f = get_app_fn(ma);
+    if (is_assigned(f)) {
+        return is_def_eq(ma, v);
+    } else {
+        return process_assignment(ma, v);
+    }
+}
+
+bool type_context::force_assign(expr const & ma, expr const & v) {
+    return process_assignment(ma, v);
+}
+
 /** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */
 lbool type_context::quick_is_def_eq(expr const & e1, expr const & e2) {
     if (e1 == e2)

src/library/type_context.h

@@ -334,6 +334,20 @@ public:
     optional<expr> mk_class_instance(expr const & type);
     optional<expr> next_class_instance();
 
+    /** \brief Given \c ma of the form <tt>?m t_1 ... t_n</tt>, (try to) assign
+        ?m to (an abstraction of) v. Return true if success and false otherwise.
+
+        \remark If ?m is already assigned, we just check if ma and v are definitionally
+        equal. */
+    bool assign(expr const & ma, expr const & v);
+
+    /** \brief Similar to \c assign, but it replaces the existing assignment
+        if the metavariable is already assigned.
+
+        Application: for implicit instance arguments, we want the term to be the one
+        generated by type class resolution even when it can be inferred by type inference. */
+    bool force_assign(expr const & ma, expr const & v);
+
     /** \brief Clear internal caches used to speedup computation */
     void clear_cache();
 

tests/lean/run/app_builder.lean

@@ -9,10 +9,16 @@ set_option pp.all true
 #app_builder eq.trans (H1, H2)
 #app_builder eq.symm (H1)
 
-open algebra
+open algebra nat
-variables A : Type
+universe l
-variables [s : comm_ring A]
+constant A : Type.{l}
+constant s : comm_ring A
+attribute s [instance]
 variables x y : A
 
 #app_builder eq.refl (s)
 #app_builder eq.refl (x)
+#app_builder add (x, y)
+#app_builder add (a, b)
+#app_builder mul (a, b)
+#app_builder sub (x, y)