From 0a3fbda0504e072eeefd15e4b8f203f63f09b3cd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Oct 2015 15:48:01 -0700 Subject: [PATCH] feat(library/blast): convert universe metavariables into uref's --- src/library/blast/blast.cpp | 57 +++++++++++++++++++++---------------- src/library/blast/expr.cpp | 19 +++++++++---- src/library/blast/expr.h | 5 +++- src/library/blast/state.cpp | 8 +++++- src/library/blast/state.h | 4 ++- 5 files changed, 60 insertions(+), 33 deletions(-) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 33bcfe6fd4..9ea7991a7e 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -20,24 +20,6 @@ Author: Leonardo de Moura namespace lean { namespace blast { -level to_blast_level(level const & l) { - level lhs; - switch (l.kind()) { - case level_kind::Succ: return blast::mk_succ(to_blast_level(succ_of(l))); - case level_kind::Zero: return blast::mk_level_zero(); - case level_kind::Param: return blast::mk_param_univ(param_id(l)); - case level_kind::Meta: return blast::mk_meta_univ(meta_id(l)); - case level_kind::Global: return blast::mk_global_univ(global_id(l)); - case level_kind::Max: - lhs = to_blast_level(max_lhs(l)); - return blast::mk_max(lhs, to_blast_level(max_rhs(l))); - case level_kind::IMax: - lhs = to_blast_level(imax_lhs(l)); - return blast::mk_imax(lhs, to_blast_level(imax_rhs(l))); - } - lean_unreachable(); -} - static name * g_prefix = nullptr; class context { @@ -45,7 +27,8 @@ class context { io_state m_ios; name_set m_lemma_hints; name_set m_unfold_hints; - name_map m_mvar2mref; // map goal metavariables to blast mref's + name_map m_uvar2uref; // map global universe metavariables to blast uref's + name_map m_mvar2mref; // map global metavariables to blast mref's name_predicate m_not_reducible_pred; name_map m_projection_info; state m_curr_state; // current state @@ -54,9 +37,35 @@ class context { type_checker m_tc; state & m_state; // We map each metavariable to a metavariable application and the mref associated with it. + name_map & m_uvar2uref; name_map> & m_mvar2meta_mref; name_map & m_local2href; + level to_blast_level(level const & l) { + level lhs; + switch (l.kind()) { + case level_kind::Succ: return blast::mk_succ(to_blast_level(succ_of(l))); + case level_kind::Zero: return blast::mk_level_zero(); + case level_kind::Param: return blast::mk_param_univ(param_id(l)); + case level_kind::Global: return blast::mk_global_univ(global_id(l)); + case level_kind::Max: + lhs = to_blast_level(max_lhs(l)); + return blast::mk_max(lhs, to_blast_level(max_rhs(l))); + case level_kind::IMax: + lhs = to_blast_level(imax_lhs(l)); + return blast::mk_imax(lhs, to_blast_level(imax_rhs(l))); + case level_kind::Meta: + if (auto r = m_uvar2uref.find(meta_id(l))) { + return *r; + } else { + level uref = m_state.mk_uref(); + m_uvar2uref.insert(meta_id(l), uref); + return uref; + } + } + lean_unreachable(); + } + expr visit_sort(expr const & e) { return blast::mk_sort(to_blast_level(sort_level(e))); } @@ -183,8 +192,9 @@ class context { public: to_blast_expr_fn(environment const & env, state & s, - name_map> & mvar2meta_mref, name_map & local2href): - m_tc(env), m_state(s), m_mvar2meta_mref(mvar2meta_mref), m_local2href(local2href) {} + name_map & uvar2uref, name_map> & mvar2meta_mref, + name_map & local2href): + m_tc(env), m_state(s), m_uvar2uref(uvar2uref), m_mvar2meta_mref(mvar2meta_mref), m_local2href(local2href) {} }; void init_mvar2mref(name_map> & m) { @@ -198,7 +208,7 @@ class context { type_checker_ptr norm_tc = mk_type_checker(m_env, name_generator(*g_prefix), UnfoldReducible); name_map> mvar2meta_mref; name_map local2href; - to_blast_expr_fn to_blast_expr(m_env, s, mvar2meta_mref, local2href); + to_blast_expr_fn to_blast_expr(m_env, s, m_uvar2uref, mvar2meta_mref, local2href); buffer hs; g.get_hyps(hs); for (expr const & h : hs) { @@ -247,9 +257,6 @@ public: projection_info const * get_projection_info(name const & n) const { return m_projection_info.find(n); } - - name mk_fresh_local_name() { - } }; LEAN_THREAD_PTR(context, g_context); diff --git a/src/library/blast/expr.cpp b/src/library/blast/expr.cpp index 2c6ecf6e4e..416ded85a8 100644 --- a/src/library/blast/expr.cpp +++ b/src/library/blast/expr.cpp @@ -19,6 +19,9 @@ Author: Leonardo de Moura namespace lean { namespace blast { +static name * g_prefix = nullptr; +static expr * g_dummy_type = nullptr; // dummy type for href/mref + typedef typename std::vector expr_array; LEAN_THREAD_PTR(expr_array, g_var_array); LEAN_THREAD_PTR(expr_array, g_mref_array); @@ -76,8 +79,17 @@ level mk_global_univ(name const & n) { return lean::mk_global_univ(n); } -level mk_meta_univ(name const & n) { - return lean::mk_meta_univ(n); +level mk_uref(unsigned idx) { + return lean::mk_meta_univ(name(*g_prefix, idx)); +} + +bool is_uref(level const & l) { + return is_meta(l) && meta_id(l).is_numeral(); +} + +unsigned uref_index(level const & l) { + lean_assert(is_uref(l)); + return meta_id(l).get_numeral(); } level update_succ(level const & l, level const & new_arg) { @@ -101,9 +113,6 @@ level update_max(level const & l, level const & new_lhs, level const & new_rhs) } } -static name * g_prefix = nullptr; -static expr * g_dummy_type = nullptr; // dummy type for href/mref - static expr mk_href_core(unsigned idx) { return lean::mk_local(name(*g_prefix, idx), *g_dummy_type); } diff --git a/src/library/blast/expr.h b/src/library/blast/expr.h index a3ae1fc58f..98e6a7471b 100644 --- a/src/library/blast/expr.h +++ b/src/library/blast/expr.h @@ -33,7 +33,10 @@ level mk_imax(level const & l1, level const & l2); level mk_succ(level const & l); level mk_param_univ(name const & n); level mk_global_univ(name const & n); -level mk_meta_univ(name const & n); +level mk_uref(unsigned idx); + +bool is_uref(level const & l); +unsigned uref_index(level const & l); expr mk_var(unsigned idx); // mk_href and mk_mref are helper functions for creating hypotheses and meta-variables used in the blast tactic. diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index da509da7c6..e9d8c8ca6f 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -11,7 +11,7 @@ Author: Leonardo de Moura namespace lean { namespace blast { -state::state():m_next_uvar_index(0), m_next_mref_index(0) {} +state::state():m_next_uref_index(0), m_next_mref_index(0) {} /** \brief Mark that hypothesis h with index hidx is fixed by the meta-variable midx. That is, `h` occurs in the type of `midx`. */ @@ -29,6 +29,12 @@ void state::add_fixed_by(unsigned hidx, unsigned midx) { } } +level state::mk_uref() { + unsigned idx = m_next_mref_index; + m_next_mref_index++; + return blast::mk_uref(idx); +} + expr state::mk_metavar(hypothesis_idx_buffer const & ctx, expr const & type) { hypothesis_idx_set ctx_as_set; for (unsigned const & hidx : ctx) diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 390f28d33f..f00f6f0e40 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -31,7 +31,7 @@ class state { typedef metavar_idx_map eassignment; typedef metavar_idx_map uassignment; typedef hypothesis_idx_map fixed_by; - unsigned m_next_uvar_index; // index of the next universe metavariable + unsigned m_next_uref_index; // index of the next universe metavariable uassignment m_uassignment; unsigned m_next_mref_index; // index of the next metavariable metavar_decls m_metavar_decls; @@ -59,6 +59,8 @@ class state { #endif public: state(); + level mk_uref(); + /** \brief Create a new metavariable using the given type and context. \pre ctx must be a subset of the hypotheses in the main branch. */ expr mk_metavar(hypothesis_idx_buffer const & ctx, expr const & type);