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

feat(kernel/type_checker): add is_stuck method, and improve ensure_pi method, closes #261

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-27 13:16:50 -07:00
parent 2e5ad274a5
commit 7516fcad97
12 changed files with 81 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/elaborator.cpp
View file

@ -341,7 +341,7 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
if (!is_pi(f_type) && has_metavar(f_type)) {
constraint_seq saved_cs = cs;
expr new_f_type = whnf(f_type, cs);
if (!is_pi(new_f_type) && is_meta(new_f_type)) {
if (!is_pi(new_f_type) && m_tc[m_relax_main_opaque]->is_stuck(new_f_type)) {
cs = saved_cs;
// let type checker add constraint
f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f, cs);

2
src/kernel/converter.cpp
View file

@ -141,7 +141,7 @@ struct default_converter : public converter {
/** \brief Return true if \c e may be reduced later after metavariables are instantiated. */
bool may_reduce_later(expr const & e, type_checker & c) {
return m_env.norm_ext().may_reduce_later(e, get_extension(c));
return static_cast<bool>(m_env.norm_ext().may_reduce_later(e, get_extension(c)));
}
/** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */

12
src/kernel/expr.cpp
View file

@ -583,17 +583,17 @@ bool is_arrow(expr const & t) {
}
}
bool has_expr_metavar_strict(expr const & e) {
optional<expr> has_expr_metavar_strict(expr const & e) {
if (!has_expr_metavar(e))
return false;
bool found = false;
return none_expr();
optional<expr> r;
for_each(e, [&](expr const & e, unsigned) {
if (found || !has_expr_metavar(e)) return false;
if (is_metavar(e)) { found = true; return false; }
if (r || !has_expr_metavar(e)) return false;
if (is_meta(e)) { r = e; return false; }
if (is_local(e)) return false; // do not visit type
return true;
});
return found;
return r;
}
static bool has_free_var_in_domain(expr const & b, unsigned vidx) {

6
src/kernel/expr.h
View file

@ -537,8 +537,10 @@ inline bool is_constant(expr const & e, name const & n) { return is_constant(e)
inline bool has_metavar(expr const & e) { return e.has_metavar(); }
inline bool has_expr_metavar(expr const & e) { return e.has_expr_metavar(); }
inline bool has_univ_metavar(expr const & e) { return e.has_univ_metavar(); }
/** \brief Similar to \c has_expr_metavar, but ignores metavariables occurring in local constant types. */
bool has_expr_metavar_strict(expr const & e);
/** \brief Similar to \c has_expr_metavar, but ignores metavariables occurring in local constant types.
It also returns the meta-variable application found in \c e.
*/
optional<expr> has_expr_metavar_strict(expr const & e);
inline bool has_local(expr const & e) { return e.has_local(); }
inline bool has_param_univ(expr const & e) { return e.has_param_univ(); }
unsigned get_weight(expr const & e);

12
src/kernel/inductive/inductive.cpp
View file

@ -928,29 +928,29 @@ auto inductive_normalizer_extension::operator()(expr const & e, extension_contex
}
template<typename Ctx>
bool is_elim_meta_app_core(Ctx & ctx, expr const & e) {
optional<expr> is_elim_meta_app_core(Ctx & ctx, expr const & e) {
inductive_env_ext const & ext = get_extension(ctx.env());
expr const & elim_fn = get_app_fn(e);
if (!is_constant(elim_fn))
return false;
return none_expr();
auto it1 = ext.m_elim_info.find(const_name(elim_fn));
if (!it1)
return false;
return none_expr();
buffer<expr> elim_args;
get_app_args(e, elim_args);
unsigned major_idx = it1->m_num_ACe + it1->m_num_indices;
if (elim_args.size() < major_idx + 1)
return false;
return none_expr();
expr intro_app = ctx.whnf(elim_args[major_idx]).first;
return has_expr_metavar_strict(intro_app);
}
bool is_elim_meta_app(type_checker & tc, expr const & e) {
return is_elim_meta_app_core(tc, e);
return static_cast<bool>(is_elim_meta_app_core(tc, e));
}
// Return true if \c e is of the form (elim ... (?m ...))
bool inductive_normalizer_extension::may_reduce_later(expr const & e, extension_context & ctx) const {
optional<expr> inductive_normalizer_extension::may_reduce_later(expr const & e, extension_context & ctx) const {
return is_elim_meta_app_core(ctx, e);
}

2
src/kernel/inductive/inductive.h
View file

@ -17,7 +17,7 @@ namespace inductive {
class inductive_normalizer_extension : public normalizer_extension {
public:
virtual optional<pair<expr, constraint_seq>> operator()(expr const & e, extension_context & ctx) const;
virtual bool may_reduce_later(expr const & e, extension_context & ctx) const;
virtual optional<expr> may_reduce_later(expr const & e, extension_context & ctx) const;
virtual bool supports(name const & feature) const;
};

9
src/kernel/normalizer_extension.cpp
View file

@ -12,7 +12,7 @@ public:
virtual optional<pair<expr, constraint_seq>> operator()(expr const &, extension_context &) const {
return optional<pair<expr, constraint_seq>>();
}
virtual bool may_reduce_later(expr const &, extension_context &) const { return false; }
virtual optional<expr> may_reduce_later(expr const &, extension_context &) const { return none_expr(); }
virtual bool supports(name const &) const { return false; }
};
@ -34,8 +34,11 @@ public:
return (*m_ext2)(e, ctx);
}
virtual bool may_reduce_later(expr const & e, extension_context & ctx) const {
return m_ext1->may_reduce_later(e, ctx) || m_ext2->may_reduce_later(e, ctx);
virtual optional<expr> may_reduce_later(expr const & e, extension_context & ctx) const {
if (auto r = m_ext1->may_reduce_later(e, ctx))
return r;
else
return m_ext2->may_reduce_later(e, ctx);
}
virtual bool supports(name const & feature) const {

6
src/kernel/normalizer_extension.h
View file

@ -18,8 +18,10 @@ class normalizer_extension {
public:
virtual ~normalizer_extension() {}
virtual optional<pair<expr, constraint_seq>> operator()(expr const & e, extension_context & ctx) const = 0;
/** \brief Return true if the extension may reduce \c e after metavariables are instantiated. */
virtual bool may_reduce_later(expr const & e, extension_context & ctx) const = 0;
/** \brief Return a non-none expression if the extension may reduce \c e after metavariables are instantiated.
The expression returned is a meta-variable that if instantiated my allow the reduction to continue.
*/
virtual optional<expr> may_reduce_later(expr const & e, extension_context & ctx) const = 0;
/** \brief Return true iff the extension supports a feature with the given name,
this method is only used for sanity checking. */
virtual bool supports(name const & feature) const = 0;

24
src/kernel/type_checker.cpp
View file

@ -121,8 +121,8 @@ pair<expr, constraint_seq> type_checker::ensure_pi_core(expr e, expr const & s)
auto ecs = whnf(e);
if (is_pi(ecs.first)) {
return ecs;
} else if (is_meta(ecs.first)) {
expr r = mk_pi_for(m_gen, ecs.first);
} else if (auto m = is_stuck(ecs.first)) {
expr r = mk_pi_for(m_gen, *m);
justification j = mk_justification(s, [=](formatter const & fmt, substitution const & subst) {
return pp_function_expected(fmt, substitution(subst).instantiate(s));
});
@ -145,11 +145,13 @@ void type_checker::check_level(level const & l, expr const & s) {
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined global universe level '" << *n1 << "'", s);
if (m_params) {
if (auto n2 = get_undef_param(l, *m_params))
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '" << *n2 << "'", s);
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '"
<< *n2 << "'", s);
}
}
app_delayed_justification::app_delayed_justification(expr const & e, expr const & arg, expr const & f_type, expr const & a_type):
app_delayed_justification::app_delayed_justification(expr const & e, expr const & arg, expr const & f_type,
expr const & a_type):
m_e(e), m_arg(arg), m_fn_type(f_type), m_arg_type(a_type) {}
justification mk_app_justification(expr const & e, expr const & arg, expr const & d_type, expr const & a_type) {
@ -174,7 +176,8 @@ expr type_checker::infer_constant(expr const & e, bool infer_only) {
auto const & ps = d.get_univ_params();
auto const & ls = const_levels(e);
if (length(ps) != length(ls))
throw_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '" << const_name(e) << "', #"
throw_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '"
<< const_name(e) << "', #"
<< length(ps) << " expected, #" << length(ls) << " provided");
if (!infer_only) {
for (level const & l : ls)
@ -431,6 +434,14 @@ type_checker::type_checker(environment const & env):
type_checker::~type_checker() {}
optional<expr> type_checker::is_stuck(expr const & e) {
if (is_meta(e)) {
return some_expr(e);
} else {
return m_env.norm_ext().may_reduce_later(e, m_tc_ctx);
}
}
void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type) {
if (has_metavar(e))
throw_kernel_exception(env, e, [=](formatter const & fmt) { return pp_decl_has_metavars(fmt, n, e, is_type); });
@ -457,7 +468,8 @@ static void check_duplicated_params(environment const & env, declaration const &
auto const & p = head(ls);
ls = tail(ls);
if (std::find(ls.begin(), ls.end(), p) != ls.end()) {
throw_kernel_exception(env, sstream() << "failed to add declaration to environment, duplicate universe level parameter: '"
throw_kernel_exception(env, sstream() << "failed to add declaration to environment, "
<< "duplicate universe level parameter: '"
<< p << "'", d.get_type());
}
}

3
src/kernel/type_checker.h
View file

@ -205,6 +205,9 @@ public:
/** \brief Return true iff the constant \c c is opaque with respect to this type checker. */
bool is_opaque(expr const & c) const;
/** \brief Return a metavariable that may be stucking the \c e's reduction. */
optional<expr> is_stuck(expr const & e);
template<typename F>
typename std::result_of<F()>::type with_params(level_param_names const & ps, F && f) {
flet<level_param_names const *> updt(m_params, &ps);

2
src/tests/kernel/environment.cpp
View file

@ -134,7 +134,7 @@ public:
// In a real implementation, we must check if proj1 and mk were defined in the environment.
return optional<pair<expr, constraint_seq>>(app_arg(app_fn(a_n)), constraint_seq());
}
virtual bool may_reduce_later(expr const &, extension_context &) const { return false; }
virtual optional<expr> may_reduce_later(expr const &, extension_context &) const { return none_expr(); }
virtual bool supports(name const &) const { return false; }
};

30
tests/lean/run/vector2.lean Normal file
View file

@ -0,0 +1,30 @@
import logic data.nat.basic
open nat
inductive vector (A : Type) : nat → Type :=
vnil : vector A zero,
vcons : Π {n : nat}, A → vector A n → vector A (succ n)
namespace vector
definition no_confusion_type {A : Type} {n : nat} (P : Type) (v₁ v₂ : vector A n) : Type :=
cases_on v₁
(cases_on v₂
(P → P)
(λ n₂ h₂ t₂, P))
(λ n₁ h₁ t₁, cases_on v₂
P
(λ n₂ h₂ t₂, (Π (H : n₁ = n₂), h₁ = h₂ → eq.rec_on H t₁ = t₂ → P) → P))
definition no_confusion {A : Type} {n : nat} {P : Type} {v₁ v₂ : vector A n} : v₁ = v₂ → no_confusion_type P v₁ v₂ :=
assume H₁₂ : v₁ = v₂,
have aux : v₁ = v₁ → no_confusion_type P v₁ v₁, from
take H₁₁, cases_on v₁
(assume h : P, h)
(take n₁ h₁ t₁, assume h : (Π (H : n₁ = n₁), h₁ = h₁ → t₁ = t₁ → P),
h rfl rfl rfl),
eq.rec aux H₁₂ H₁₂
theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ :=
assume h, no_confusion h (λ n h t, h)
end vector