michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/blast): convert universe metavariables into uref's

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-02 15:48:01 -07:00
parent 442cbff578
commit 0a3fbda050
5 changed files with 60 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

57
src/library/blast/blast.cpp
View file

@ -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<expr> m_mvar2mref; // map goal metavariables to blast mref's
name_map<level> m_uvar2uref; // map global universe metavariables to blast uref's
name_map<expr> m_mvar2mref; // map global metavariables to blast mref's
name_predicate m_not_reducible_pred;
name_map<projection_info> 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<level> & m_uvar2uref;
name_map<pair<expr, expr>> & m_mvar2meta_mref;
name_map<expr> & 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<pair<expr, expr>> & mvar2meta_mref, name_map<expr> & local2href):
m_tc(env), m_state(s), m_mvar2meta_mref(mvar2meta_mref), m_local2href(local2href) {}
name_map<level> & uvar2uref, name_map<pair<expr, expr>> & mvar2meta_mref,
name_map<expr> & local2href):
m_tc(env), m_state(s), m_uvar2uref(uvar2uref), m_mvar2meta_mref(mvar2meta_mref), m_local2href(local2href) {}
};
void init_mvar2mref(name_map<pair<expr, expr>> & m) {
@ -198,7 +208,7 @@ class context {
type_checker_ptr norm_tc = mk_type_checker(m_env, name_generator(*g_prefix), UnfoldReducible);
name_map<pair<expr, expr>> mvar2meta_mref;
name_map<expr> 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<expr> 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);

19
src/library/blast/expr.cpp
View file

@ -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> 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);
}

5
src/library/blast/expr.h
View file

@ -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.

8
src/library/blast/state.cpp
View file

@ -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)

4
src/library/blast/state.h
View file

@ -31,7 +31,7 @@ class state {
typedef metavar_idx_map<expr> eassignment;
typedef metavar_idx_map<level> uassignment;
typedef hypothesis_idx_map<metavar_idx_set> 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);