diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index de4fc2859..86439866e 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -5,6 +5,7 @@ server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp -structure_cmd.cpp info_manager.cpp no_info.cpp extra_info.cpp) +structure_cmd.cpp info_manager.cpp no_info.cpp extra_info.cpp +local_context.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index e9fdcf5d7..b10ec38ea 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -34,11 +34,13 @@ Author: Leonardo de Moura #include "library/error_handling/error_handling.h" #include "frontends/lean/local_decls.h" #include "frontends/lean/class.h" +#include "frontends/lean/util.h" #include "frontends/lean/tactic_hint.h" #include "frontends/lean/info_manager.h" #include "frontends/lean/elaborator.h" #include "frontends/lean/no_info.h" #include "frontends/lean/extra_info.h" +#include "frontends/lean/local_context.h" #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true @@ -54,78 +56,6 @@ bool get_elaborator_local_instances(options const & opts) { } // ========================================== -/** \brief Functional object for converting the universe metavariables in an expression in new universe parameters. - The substitution is updated with the mapping metavar -> new param. - The set of parameter names m_params and the buffer m_new_params are also updated. -*/ -class univ_metavars_to_params_fn { - environment const & m_env; - local_decls const & m_lls; - substitution & m_subst; - name_set & m_params; - buffer & m_new_params; - unsigned m_next_idx; - - /** \brief Create a new universe parameter s.t. the new name does not occur in \c m_params, nor it is - a global universe in \e m_env or in the local_decls m_lls. - The new name is added to \c m_params, and the new level parameter is returned. - The name is of the form "l_i" where \c i >= m_next_idx. - */ - level mk_new_univ_param() { - name l("l"); - name r = l.append_after(m_next_idx); - while (m_lls.contains(r) || m_params.contains(r) || m_env.is_universe(r)) { - m_next_idx++; - r = l.append_after(m_next_idx); - } - m_params.insert(r); - m_new_params.push_back(r); - return mk_param_univ(r); - } - -public: - univ_metavars_to_params_fn(environment const & env, local_decls const & lls, substitution & s, name_set & ps, buffer & new_ps): - m_env(env), m_lls(lls), m_subst(s), m_params(ps), m_new_params(new_ps), m_next_idx(1) {} - - level apply(level const & l) { - return replace(l, [&](level const & l) { - if (!has_meta(l)) - return some_level(l); - if (is_meta(l)) { - if (auto it = m_subst.get_level(meta_id(l))) { - return some_level(*it); - } else { - level new_p = mk_new_univ_param(); - m_subst.assign(l, new_p); - return some_level(new_p); - } - } - return none_level(); - }); - } - - expr apply(expr const & e) { - if (!has_univ_metavar(e)) { - return e; - } else { - return replace(e, [&](expr const & e) { - if (!has_univ_metavar(e)) { - return some_expr(e); - } else if (is_sort(e)) { - return some_expr(update_sort(e, apply(sort_level(e)))); - } else if (is_constant(e)) { - levels ls = map(const_levels(e), [&](level const & l) { return apply(l); }); - return some_expr(update_constant(e, ls)); - } else { - return none_expr(); - } - }); - } - } - - expr operator()(expr const & e) { return apply(e); } -}; - elaborator_context::elaborator_context(environment const & env, io_state const & ios, local_decls const & lls, pos_info_provider const * pp, info_manager * info, bool check_unassigned): m_env(env), m_ios(ios), m_lls(lls), m_pos_provider(pp), m_info_manager(info), m_check_unassigned(check_unassigned) { @@ -163,170 +93,33 @@ list get_local_instances(type_checker & tc, list const & ctx, name c return to_list(buffer.begin(), buffer.end()); } -typedef name_map mvar2meta; typedef std::unique_ptr type_checker_ptr; /** \brief Helper class for implementing the \c elaborate functions. */ class elaborator { - /** \brief Auxiliary data-structure for storing the local context, and creating metavariables in the scope of the local context efficiently */ - class context { - name_generator & m_ngen; - mvar2meta & m_mvar2meta; - list m_ctx; // current local context: a list of local constants - buffer m_ctx_buffer; // m_ctx as a buffer - buffer m_ctx_domain_buffer; // m_ctx_domain_buffer[i] == abstract_locals(m_ctx_buffer[i], i, m_ctx_buffer.beg - public: - context(name_generator & ngen, mvar2meta & m, list const & ctx):m_ngen(ngen), m_mvar2meta(m) { set_ctx(ctx); } - - void set_ctx(list const & ctx) { - m_ctx = ctx; - m_ctx_buffer.clear(); - m_ctx_domain_buffer.clear(); - to_buffer(ctx, m_ctx_buffer); - std::reverse(m_ctx_buffer.begin(), m_ctx_buffer.end()); - for (unsigned i = 0; i < m_ctx_buffer.size(); i++) { - m_ctx_domain_buffer.push_back(abstract_locals(m_ctx_buffer[i], i, m_ctx_buffer.data())); - } - } - - /** \brief Given e[l_1, ..., l_n] and assuming \c m_ctx is - [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], - then the result is - (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), e[x_1, ... x_n]). - */ - expr pi_abstract_context(expr e, tag g) { - e = abstract_locals(e, m_ctx_buffer.size(), m_ctx_buffer.data()); - unsigned i = m_ctx_domain_buffer.size(); - while (i > 0) { - --i; - expr const & l = m_ctx_domain_buffer[i]; - e = save_tag(mk_pi(local_pp_name(l), mlocal_type(l), e, local_info(l)), g); - } - return e; - } - - /** \brief Assuming \c m_ctx is - [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], - return (f l_1 ... l_n). - */ - expr apply_context(expr const & f, tag g) { - expr r = f; - for (unsigned i = 0; i < m_ctx_buffer.size(); i++) - r = save_tag(::lean::mk_app(r, m_ctx_buffer[i]), g); - return r; - } - - /** \brief Assuming \c m_ctx is - [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], - return a fresh metavariable \c ?m with type - (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), - where \c ?u is a fresh universe metavariable. - */ - expr mk_type_metavar(tag g) { - name n = m_ngen.next(); - expr s = save_tag(mk_sort(mk_meta_univ(m_ngen.next())), g); - expr t = pi_abstract_context(s, g); - return save_tag(::lean::mk_metavar(n, t), g); - } - - /** \brief Assuming \c m_ctx is - [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], - return (?m l_1 ... l_n) where \c ?m is a fresh metavariable with type - (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), - and \c ?u is a fresh universe metavariable. - - \remark The type of the resulting expression is Type.{?u} - */ - expr mk_type_meta(tag g) { - return apply_context(mk_type_metavar(g), g); - } - - /** \brief Given type[l_1, ..., l_n] and assuming \c m_ctx is - [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], - then the result is a fresh metavariable \c ?m with type - (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), type[x_1, ... x_n]). - If type is none, then the result is a fresh metavariable \c ?m1 with type - (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), ?m2 x1 .... xn), - where ?m2 is another fresh metavariable with type - (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), - and \c ?u is a fresh universe metavariable. - */ - expr mk_metavar(optional const & type, tag g) { - name n = m_ngen.next(); - expr r_type = type ? *type : mk_type_meta(g); - expr t = pi_abstract_context(r_type, g); - return save_tag(::lean::mk_metavar(n, t), g); - } - - /** \brief Given type[l_1, ..., l_n] and assuming \c m_ctx is - [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], - return (?m l_1 ... l_n), where ?m is a fresh metavariable - created using \c mk_metavar. - - \see mk_metavar - */ - expr mk_meta(optional const & type, tag g) { - expr mvar = mk_metavar(type, g); - expr meta = apply_context(mvar, g); - m_mvar2meta.insert(mlocal_name(mvar), meta); - return meta; - } - - void add_local(expr const & l) { - m_ctx = cons(l, m_ctx); - m_ctx_domain_buffer.push_back(abstract_locals(l, m_ctx_buffer.size(), m_ctx_buffer.data())); - m_ctx_buffer.push_back(l); - } - - list const & get_data() const { - return m_ctx; - } - - /** \brief Scope object for restoring the content of the context */ - class scope { - context & m_main; - list m_old_ctx; - unsigned m_old_sz; - public: - scope(context & main):m_main(main), m_old_ctx(main.m_ctx), m_old_sz(main.m_ctx_buffer.size()) {} - ~scope() { - m_main.m_ctx = m_old_ctx; - m_main.m_ctx_buffer.shrink(m_old_sz); - m_main.m_ctx_domain_buffer.shrink(m_old_sz); - } - }; - - /** \brief Scope object for temporarily replacing the content of the context */ - class scope_replace { - context & m_main; - list m_saved; - public: - scope_replace(context & main, list const & new_ctx):m_main(main), m_saved(m_main.m_ctx) { - m_main.set_ctx(new_ctx); - } - ~scope_replace() { - m_main.set_ctx(m_saved); - } - }; - }; - typedef name_map local_tactic_hints; typedef rb_map, expr_quick_cmp> cache; elaborator_context & m_env; name_generator m_ngen; type_checker_ptr m_tc[2]; - mvar2meta m_mvar2meta; // mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants - // representing the context where ?m was created. - context m_context; // current local context: a list of local constants - context m_full_context; // superset of m_context, it also contains non-contextual locals. + // mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants + // representing the context where ?m was created. + mvar2meta m_mvar2meta; + local_context m_context; // current local context: a list of local constants + local_context m_full_context; // superset of m_context, it also contains non-contextual locals. cache m_cache; - local_tactic_hints m_local_tactic_hints; // mapping from metavariable name ?m to tactic expression that should be used to solve it. - // this mapping is populated by the 'by tactic-expr' expression. - name_set m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned - bool m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent. - bool m_no_info; // when true, we do not collect information when true, we set is to true whenever we find no_info annotation. + // mapping from metavariable name ?m to tactic expression that should be used to solve it. + // this mapping is populated by the 'by tactic-expr' expression. + local_tactic_hints m_local_tactic_hints; + // set of metavariables that we already reported unsolved/unassigned + name_set m_displayed_errors; + // if m_relax_main_opaque is true, then treat opaque definitions from the main module as transparent. + bool m_relax_main_opaque; + // if m_no_info is true, we do not collect information when true, + // we set is to true whenever we find no_info annotation. + bool m_no_info; info_manager m_pre_info_data; // Auxiliary object to "saving" elaborator state @@ -339,21 +132,21 @@ class elaborator { }; struct scope_ctx { - elaborator & m_main; - context::scope m_scope1; - context::scope m_scope2; - cache m_old_cache; + elaborator & m_main; + local_context::scope m_scope1; + local_context::scope m_scope2; + cache m_old_cache; scope_ctx(elaborator & e):m_main(e), m_scope1(e.m_context), m_scope2(e.m_full_context), m_old_cache(e.m_cache) {} ~scope_ctx() { m_main.m_cache = m_old_cache; } }; /** \brief Auxiliary object for creating backtracking points, and replacing the local scopes. */ struct new_scope { - elaborator & m_main; - bool m_old_no_info; - context::scope_replace m_context_scope; - context::scope_replace m_full_context_scope; - cache m_old_cache; + elaborator & m_main; + bool m_old_no_info; + local_context::scope_replace m_context_scope; + local_context::scope_replace m_full_context_scope; + cache m_old_cache; new_scope(elaborator & e, saved_state const & s, bool no_info = false): m_main(e), m_context_scope(e.m_context, s.m_ctx), @@ -586,9 +379,7 @@ public: pair whnf(expr const & e) { return m_tc[m_relax_main_opaque]->whnf(e); } expr infer_type(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->infer(e, s); } expr whnf(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->whnf(e, s); } - - static expr save_tag(expr && e, tag g) { e.set_tag(g); return e; } - expr mk_app(expr const & f, expr const & a, tag g) { return save_tag(::lean::mk_app(f, a), g); } + expr mk_app(expr const & f, expr const & a, tag g) { return ::lean::mk_app(f, a).set_tag(g); } /** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */ void save_type_data(expr const & e, expr const & r) { @@ -1458,7 +1249,7 @@ public: expr apply(substitution & s, expr const & e, name_set & univ_params, buffer & new_params) { expr r = s.instantiate(e); if (has_univ_metavar(r)) - r = univ_metavars_to_params_fn(env(), lls(), s, univ_params, new_params)(r); + r = univ_metavars_to_params(env(), lls(), s, univ_params, new_params, r); r = solve_unassigned_mvars(s, r); display_unassigned_mvars(r, s); return r; diff --git a/src/frontends/lean/local_context.cpp b/src/frontends/lean/local_context.cpp new file mode 100644 index 000000000..bd4845090 --- /dev/null +++ b/src/frontends/lean/local_context.cpp @@ -0,0 +1,94 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/abstract.h" +#include "frontends/lean/local_context.h" + +namespace lean { +local_context::local_context(name_generator & ngen, mvar2meta & m, list const & ctx): + m_ngen(ngen), m_mvar2meta(m) { set_ctx(ctx); } + +void local_context::set_ctx(list const & ctx) { + m_ctx = ctx; + m_ctx_buffer.clear(); + m_ctx_domain_buffer.clear(); + to_buffer(ctx, m_ctx_buffer); + std::reverse(m_ctx_buffer.begin(), m_ctx_buffer.end()); + for (unsigned i = 0; i < m_ctx_buffer.size(); i++) { + m_ctx_domain_buffer.push_back(abstract_locals(m_ctx_buffer[i], i, m_ctx_buffer.data())); + } +} + +expr local_context::pi_abstract_context(expr e, tag g) { + e = abstract_locals(e, m_ctx_buffer.size(), m_ctx_buffer.data()); + unsigned i = m_ctx_domain_buffer.size(); + while (i > 0) { + --i; + expr const & l = m_ctx_domain_buffer[i]; + e = mk_pi(local_pp_name(l), mlocal_type(l), e, local_info(l)).set_tag(g); + } + return e; +} + +expr local_context::apply_context(expr const & f, tag g) { + expr r = f; + for (unsigned i = 0; i < m_ctx_buffer.size(); i++) + r = mk_app(r, m_ctx_buffer[i]).set_tag(g); + return r; +} + +expr local_context::mk_type_metavar(tag g) { + name n = m_ngen.next(); + expr s = mk_sort(mk_meta_univ(m_ngen.next())).set_tag(g); + expr t = pi_abstract_context(s, g); + return ::lean::mk_metavar(n, t).set_tag(g); +} + +expr local_context::mk_type_meta(tag g) { + return apply_context(mk_type_metavar(g), g); +} + +expr local_context::mk_metavar(optional const & type, tag g) { + name n = m_ngen.next(); + expr r_type = type ? *type : mk_type_meta(g); + expr t = pi_abstract_context(r_type, g); + return ::lean::mk_metavar(n, t).set_tag(g); +} + +expr local_context::mk_meta(optional const & type, tag g) { + expr mvar = mk_metavar(type, g); + expr meta = apply_context(mvar, g); + m_mvar2meta.insert(mlocal_name(mvar), meta); + return meta; +} + +void local_context::add_local(expr const & l) { + m_ctx = cons(l, m_ctx); + m_ctx_domain_buffer.push_back(abstract_locals(l, m_ctx_buffer.size(), m_ctx_buffer.data())); + m_ctx_buffer.push_back(l); +} + +list const & local_context::get_data() const { + return m_ctx; +} + +local_context::scope::scope(local_context & main): + m_main(main), m_old_ctx(main.m_ctx), m_old_sz(main.m_ctx_buffer.size()) {} +local_context::scope::~scope() { + m_main.m_ctx = m_old_ctx; + m_main.m_ctx_buffer.shrink(m_old_sz); + m_main.m_ctx_domain_buffer.shrink(m_old_sz); +} + +local_context::scope_replace::scope_replace(local_context & main, + list const & new_ctx): + m_main(main), m_saved(m_main.m_ctx) { + m_main.set_ctx(new_ctx); +} +local_context::scope_replace::~scope_replace() { + m_main.set_ctx(m_saved); +} +} diff --git a/src/frontends/lean/local_context.h b/src/frontends/lean/local_context.h new file mode 100644 index 000000000..889d3badd --- /dev/null +++ b/src/frontends/lean/local_context.h @@ -0,0 +1,104 @@ +/* +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/name_map.h" +#include "kernel/expr.h" + +namespace lean { +/** \brief Mapping from metavariable names to metavariable applications (?M ...) */ +typedef name_map mvar2meta; + +/** \brief Auxiliary data-structure for storing the local context, + and creating metavariables in the scope of the local context efficiently +*/ +class local_context { + name_generator & m_ngen; + mvar2meta & m_mvar2meta; + list m_ctx; // current local context: a list of local constants + buffer m_ctx_buffer; // m_ctx as a buffer + buffer m_ctx_domain_buffer; // m_ctx_domain_buffer[i] == abstract_locals(m_ctx_buffer[i], i, m_ctx_buffer.beg +public: + local_context(name_generator & ngen, mvar2meta & m, list const & ctx); + + void set_ctx(list const & ctx); + + /** \brief Given e[l_1, ..., l_n] and assuming \c m_ctx is + [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], + then the result is + (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), e[x_1, ... x_n]). + */ + expr pi_abstract_context(expr e, tag g); + + /** \brief Assuming \c m_ctx is + [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], + return (f l_1 ... l_n). + */ + expr apply_context(expr const & f, tag g); + + /** \brief Assuming \c m_ctx is + [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], + return a fresh metavariable \c ?m with type + (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), + where \c ?u is a fresh universe metavariable. + */ + expr mk_type_metavar(tag g); + + /** \brief Assuming \c m_ctx is + [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], + return (?m l_1 ... l_n) where \c ?m is a fresh metavariable with type + (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), + and \c ?u is a fresh universe metavariable. + + \remark The type of the resulting expression is Type.{?u} + */ + expr mk_type_meta(tag g); + + /** \brief Given type[l_1, ..., l_n] and assuming \c m_ctx is + [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], + then the result is a fresh metavariable \c ?m with type + (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), type[x_1, ... x_n]). + If type is none, then the result is a fresh metavariable \c ?m1 with type + (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), ?m2 x1 .... xn), + where ?m2 is another fresh metavariable with type + (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), + and \c ?u is a fresh universe metavariable. + */ + expr mk_metavar(optional const & type, tag g); + + /** \brief Given type[l_1, ..., l_n] and assuming \c m_ctx is + [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], + return (?m l_1 ... l_n), where ?m is a fresh metavariable + created using \c mk_metavar. + + \see mk_metavar + */ + expr mk_meta(optional const & type, tag g); + + void add_local(expr const & l); + + list const & get_data() const; + + /** \brief Scope object for restoring the content of the context */ + class scope { + local_context & m_main; + list m_old_ctx; + unsigned m_old_sz; + public: + scope(local_context & main); + ~scope(); + }; + + /** \brief Scope object for temporarily replacing the content of the context */ + class scope_replace { + local_context & m_main; + list m_saved; + public: + scope_replace(local_context & main, list const & new_ctx); + ~scope_replace(); + }; +}; +} diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 8427ae686..ef8c2c843 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "util/sstream.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" +#include "kernel/replace_fn.h" #include "library/scoped_ext.h" #include "library/locals.h" #include "library/explicit.h" @@ -126,4 +127,82 @@ bool occurs(level const & u, level const & l) { }); return found; } + +/** \brief Functional object for converting the universe metavariables in an expression in new universe parameters. + The substitution is updated with the mapping metavar -> new param. + The set of parameter names m_params and the buffer m_new_params are also updated. +*/ +class univ_metavars_to_params_fn { + environment const & m_env; + local_decls const & m_lls; + substitution & m_subst; + name_set & m_params; + buffer & m_new_params; + unsigned m_next_idx; + + /** \brief Create a new universe parameter s.t. the new name does not occur in \c m_params, nor it is + a global universe in \e m_env or in the local_decls m_lls. + The new name is added to \c m_params, and the new level parameter is returned. + The name is of the form "l_i" where \c i >= m_next_idx. + */ + level mk_new_univ_param() { + name l("l"); + name r = l.append_after(m_next_idx); + while (m_lls.contains(r) || m_params.contains(r) || m_env.is_universe(r)) { + m_next_idx++; + r = l.append_after(m_next_idx); + } + m_params.insert(r); + m_new_params.push_back(r); + return mk_param_univ(r); + } + +public: + univ_metavars_to_params_fn(environment const & env, local_decls const & lls, substitution & s, + name_set & ps, buffer & new_ps): + m_env(env), m_lls(lls), m_subst(s), m_params(ps), m_new_params(new_ps), m_next_idx(1) {} + + level apply(level const & l) { + return replace(l, [&](level const & l) { + if (!has_meta(l)) + return some_level(l); + if (is_meta(l)) { + if (auto it = m_subst.get_level(meta_id(l))) { + return some_level(*it); + } else { + level new_p = mk_new_univ_param(); + m_subst.assign(l, new_p); + return some_level(new_p); + } + } + return none_level(); + }); + } + + expr apply(expr const & e) { + if (!has_univ_metavar(e)) { + return e; + } else { + return replace(e, [&](expr const & e) { + if (!has_univ_metavar(e)) { + return some_expr(e); + } else if (is_sort(e)) { + return some_expr(update_sort(e, apply(sort_level(e)))); + } else if (is_constant(e)) { + levels ls = map(const_levels(e), [&](level const & l) { return apply(l); }); + return some_expr(update_constant(e, ls)); + } else { + return none_expr(); + } + }); + } + } + + expr operator()(expr const & e) { return apply(e); } +}; + +expr univ_metavars_to_params(environment const & env, local_decls const & lls, substitution & s, + name_set & ps, buffer & new_ps, expr const & e) { + return univ_metavars_to_params_fn(env, lls, s, ps, new_ps)(e); +} } diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index d4d601cd1..f59394126 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include "kernel/expr.h" #include "kernel/expr_sets.h" +#include "frontends/lean/local_decls.h" namespace lean { class parser; void check_atomic(name const & n); @@ -32,4 +33,11 @@ expr Pi_as_is(buffer const & locals, expr const & e, parser & p); level mk_result_level(environment const & env, buffer const & r_lvls); /** \brief Return true if \c u occurs in \c l */ bool occurs(level const & u, level const & l); + +/** \brief Convert the universe metavariables in \c e in new universe parameters. + The substitution \c s is updated with the mapping metavar -> new param. + The set of parameter names \c ps and the buffer \c new_ps are also updated. +*/ +expr univ_metavars_to_params(environment const & env, local_decls const & lls, substitution & s, + name_set & ps, buffer & new_ps, expr const & e); } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 96014ab3f..0a058a259 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -122,7 +122,7 @@ public: bool has_local() const { return m_ptr->has_local(); } bool has_param_univ() const { return m_ptr->has_param_univ(); } - void set_tag(tag t) { m_ptr->set_tag(t); } + expr set_tag(tag t) { m_ptr->set_tag(t); return *this; } tag get_tag() const { return m_ptr->get_tag(); }