max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/type_context): missing case: stuck projections

Browse source 
type_context only unfolds projections when they reduce.
This commit is contained in:
Leonardo de Moura 2016-08-30 08:13:58 -07:00
parent bd99de9bf8
commit 85cf20a5b4
2 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/library/type_context.cpp
View file

@ -599,9 +599,24 @@ expr type_context::relaxed_whnf(expr const & e) {
return whnf(e);
}
optional<expr> type_context::is_stuck_projection(expr const & e) {
expr const & f = get_app_fn(e);
if (!is_constant(f)) return none_expr(); // it is not projection app
projection_info const * info = m_cache->m_proj_info.find(const_name(f));
if (!info) return none_expr(); // it is not projection app
buffer<expr> args;
get_app_args(e, args);
if (args.size() <= info->m_nparams) return none_expr(); // partially applied projection
unsigned mkidx = info->m_nparams;
expr mk = args[mkidx];
return is_stuck(mk);
}
optional<expr> type_context::is_stuck(expr const & e) {
if (is_meta(e)) {
return some_expr(e);
} else if (auto r = is_stuck_projection(e)) {
return r;
} else {
return env().norm_ext().is_stuck(e, *this);
}

1
src/library/type_context.h
View file

@ -250,6 +250,7 @@ public:
virtual expr relaxed_whnf(expr const & e) override;
virtual bool relaxed_is_def_eq(expr const & e1, expr const & e2) override;
optional<expr> is_stuck_projection(expr const & e);
virtual optional<expr> is_stuck(expr const &) override;
virtual expr push_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) override;