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

fix(frontends/lean): fix (and simplify) parameter universe inference

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-06 16:46:34 -07:00
parent 9be1a4ab46
commit 9a13bef4f3
12 changed files with 854 additions and 471 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/frontends/lean/builtin_cmds.cpp
View file

@ -83,9 +83,10 @@ environment check_cmd(parser & p) {
mk_section_params(collect_locals(e), p, section_ps);
e = p.lambda_abstract(section_ps, e);
level_param_names ls = to_level_param_names(collect_univ_params(e));
e = p.elaborate(e, false);
type_checker tc(p.env(), p.mk_ngen(), mk_default_converter(p.env(), true));
expr type = tc.check(e, ls);
level_param_names new_ls;
std::tie(e, new_ls) = p.elaborate(e, false);
auto tc = mk_type_checker_with_hints(p.env(), p.mk_ngen());
expr type = tc->check(e, append(ls, new_ls));
p.regular_stream() << e << " : " << type << endl;
return p.env();
}

54
src/frontends/lean/decl_cmds.cpp
View file

@ -90,6 +90,14 @@ static environment declare_var(parser & p, environment env,
}
}
/** \brief If we are in a section, then add the new local levels to it. */
static void update_section_local_levels(parser & p, level_param_names const & new_ls) {
if (in_section(p.env())) {
for (auto const & l : new_ls)
p.add_local_level(l, mk_param_univ(l));
}
}
optional<binder_info> parse_binder_info(parser & p) {
optional<binder_info> bi = p.parse_optional_binder_info();
if (bi)
@ -109,7 +117,6 @@ environment variable_cmd_core(parser & p, bool is_axiom) {
if (!in_section(p.env()))
scope1.emplace(p);
parse_univ_params(p, ls_buffer);
parser::param_universe_scope scope2(p);
expr type;
if (!p.curr_is_token(g_colon)) {
buffer<expr> ps;
@ -129,8 +136,10 @@ environment variable_cmd_core(parser & p, bool is_axiom) {
update_univ_parameters(ls_buffer, collect_univ_params(type), p);
ls = to_list(ls_buffer.begin(), ls_buffer.end());
}
type = p.elaborate(type);
return declare_var(p, p.env(), n, ls, type, is_axiom, bi, pos);
level_param_names new_ls;
std::tie(type, new_ls) = p.elaborate(type);
update_section_local_levels(p, new_ls);
return declare_var(p, p.env(), n, append(ls, new_ls), type, is_axiom, bi, pos);
}
environment variable_cmd(parser & p) {
return variable_cmd_core(p, false);
@ -235,24 +244,18 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
value = p.parse_expr();
} else if (p.curr_is_token(g_colon)) {
p.next();
{
parser::param_universe_scope scope2(p);
type = p.parse_expr();
}
type = p.parse_expr();
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
value = p.parse_expr();
} else {
buffer<expr> ps;
optional<local_environment> lenv;
{
parser::param_universe_scope scope2(p);
lenv = p.parse_binders(ps);
if (p.curr_is_token(g_colon)) {
p.next();
type = p.parse_scoped_expr(ps, *lenv);
} else {
type = p.save_pos(mk_expr_placeholder(), p.pos());
}
lenv = p.parse_binders(ps);
if (p.curr_is_token(g_colon)) {
p.next();
type = p.parse_scoped_expr(ps, *lenv);
} else {
type = p.save_pos(mk_expr_placeholder(), p.pos());
}
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
value = p.parse_scoped_expr(ps, *lenv);
@ -274,17 +277,14 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
if (real_n != n)
env = add_alias(env, n, mk_constant(real_n));
}
level_param_names new_ls;
if (is_theorem) {
// TODO(Leo): delay theorems
auto type_value = p.elaborate(n, type, value);
type = type_value.first;
value = type_value.second;
env = module::add(env, check(env, mk_theorem(real_n, ls, type, value)));
std::tie(type, value, new_ls) = p.elaborate(n, type, value);
env = module::add(env, check(env, mk_theorem(real_n, append(ls, new_ls), type, value)));
} else {
auto type_value = p.elaborate(n, type, value);
type = type_value.first;
value = type_value.second;
env = module::add(env, check(env, mk_definition(env, real_n, ls, type, value, modifiers.m_is_opaque)));
std::tie(type, value, new_ls) = p.elaborate(n, type, value);
env = module::add(env, check(env, mk_definition(env, real_n, append(ls, new_ls), type, value, modifiers.m_is_opaque)));
}
if (modifiers.m_is_class)
env = add_class(env, real_n);
@ -315,11 +315,13 @@ static environment variables_cmd(parser & p) {
optional<parser::local_scope> scope1;
if (!in_section(p.env()))
scope1.emplace(p);
parser::param_universe_scope scope2(p);
expr type = p.parse_expr();
p.parse_close_binder_info(bi);
level_param_names ls = to_level_param_names(collect_univ_params(type));
type = p.elaborate(type);
level_param_names new_ls;
std::tie(type, new_ls) = p.elaborate(type);
update_section_local_levels(p, new_ls);
ls = append(ls, new_ls);
environment env = p.env();
for (auto id : ids)
env = declare_var(p, env, id, ls, type, true, bi, pos);

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

@ -15,6 +15,7 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "kernel/type_checker.h"
#include "kernel/for_each_fn.h"
#include "kernel/replace_fn.h"
#include "kernel/kernel_exception.h"
#include "kernel/error_msgs.h"
#include "kernel/expr_maps.h"
@ -24,9 +25,11 @@ Author: Leonardo de Moura
#include "library/explicit.h"
#include "library/unifier.h"
#include "library/opaque_hints.h"
#include "library/locals.h"
#include "library/tactic/tactic.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/error_handling/error_handling.h"
#include "frontends/lean/local_decls.h"
#include "frontends/lean/class.h"
#ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES
@ -43,6 +46,79 @@ 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<level> const & m_lls;
substitution & m_subst;
name_set & m_params;
buffer<name> & 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<level> 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<level> const & lls, substitution & s, name_set & ps, buffer<name> & 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.d_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, unsigned) {
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); }
};
/** \brief Helper class for implementing the \c elaborate functions. */
class elaborator {
typedef list<expr> context;
typedef std::vector<constraint> constraint_vect;
@ -51,23 +127,24 @@ class elaborator {
typedef std::unique_ptr<type_checker> type_checker_ptr;
environment m_env;
local_decls<level> m_lls;
io_state m_ios;
name_generator m_ngen;
type_checker_ptr m_tc;
substitution m_subst;
context m_ctx;
pos_info_provider * m_pos_provider;
context m_ctx; // current local context: a list of local constants
pos_info_provider * m_pos_provider; // optional expression position information used when reporting errors.
justification m_accumulated; // accumulate justification of eagerly used substitutions
constraint_vect m_constraints;
tactic_hints m_tactic_hints;
mvar2meta m_mvar2meta;
constraint_vect m_constraints; // constraints that must be solved for the elaborated term to be type correct.
tactic_hints m_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.
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.
name_set m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned
bool m_check_unassigned;
bool m_use_local_instances;
/**
\brief Auxiliary object for creating backtracking points.
bool m_check_unassigned; // if true if display error messages if elaborated term still contains metavariables
bool m_use_local_instances; // if true class-instance resolution will use the local context
/** \brief Auxiliary object for creating backtracking points.
\remark A scope can only be created when m_constraints and m_subst are empty,
and m_accumulated is none.
*/
@ -93,6 +170,7 @@ class elaborator {
}
};
/* \brief Move all constraints generated by the type checker to the buffer m_constraints. */
void consume_tc_cnstrs() {
while (auto c = m_tc->next_cnstr())
m_constraints.push_back(*c);
@ -102,6 +180,12 @@ class elaborator {
virtual optional<constraints> next() = 0;
};
/** \brief 'Choice' expressions <tt>(choice e_1 ... e_n)</tt> are mapped into a metavariable \c ?m
and a choice constraints <tt>(?m in fn)</tt> where \c fn is a choice function.
The choice function produces a stream of alternatives. In this case, it produces a stream of
size \c n, one alternative for each \c e_i.
This is a helper class for implementing this choice functions.
*/
struct choice_expr_elaborator : public choice_elaborator {
elaborator & m_elab;
expr m_mvar;
@ -131,13 +215,24 @@ class elaborator {
}
};
/** \brief Whenever the elaborator finds a placeholder '_' or introduces an implicit argument, it creates
a metavariable \c ?m. If the expected type of ?m is unknown (e.g., it is another metavariable),
or if it is a 'class', then we also create a delayed choice constraint (?m in fn).
The unifier only process delayed choice constraints when there are no other kind of constraint to be
processed. The function \c fn produces a stream of alternative solutions for ?m.
In this case, \c fn will do the following:
1) if the elaborated type of ?m is a 'class' C, then the stream will contain all 'instances' of class C.
2) if the elaborated type of ?m is not a 'class', then fn produces a single empty solution.
This is a helper class for implementing this choice function.
*/
struct class_elaborator : public choice_elaborator {
elaborator & m_elab;
expr m_mvar;
expr m_mvar_type;
list<expr> m_local_instances;
list<name> m_instances;
context m_ctx;
expr m_mvar_type; // elaborated type of the metavariable
list<expr> m_local_instances; // local instances that should also be included in the class-instance resolution.
list<name> m_instances; // global declaration names that are class instances. This information is retrieved using #get_class_instances.
context m_ctx; // local context for m_mvar
substitution m_subst;
justification m_jst;
@ -193,9 +288,9 @@ class elaborator {
}
public:
elaborator(environment const & env, io_state const & ios, name_generator const & ngen, pos_info_provider * pp,
bool check_unassigned):
m_env(env), m_ios(ios),
elaborator(environment const & env, local_decls<level> const & lls, io_state const & ios, name_generator const & ngen,
pos_info_provider * pp, bool check_unassigned):
m_env(env), m_lls(lls), m_ios(ios),
m_ngen(ngen), m_tc(mk_type_checker_with_hints(env, m_ngen.mk_child())),
m_pos_provider(pp) {
m_check_unassigned = check_unassigned;
@ -231,8 +326,7 @@ public:
m_constraints.push_back(c);
}
/**
\brief Add \c c to \c m_constraints, but also tries to update \c m_subst using \c c.
/** \brief Add \c c to \c m_constraints, but also tries to update \c m_subst using \c c.
The idea is to "populate" \c m_subst using easy/simple constraints.
This trick improves the number of places where coercions can be applied.
In the future, we may also use this information to implement eager pruning of choice
@ -254,9 +348,7 @@ public:
throw unifier_exception(c.get_justification(), m_subst);
}
/**
\brief Eagerly instantiate metavars using \c m_subst.
/** \brief Eagerly instantiate metavars using \c m_subst.
\remark We update \c m_accumulated with any justifications used.
*/
expr instantiate_metavars(expr const & e) {
@ -270,11 +362,10 @@ public:
return e;
}
/**
\brief Given <tt>e[l_1, ..., l_n]</tt> and assuming \c m_ctx is
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
then the result is
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), e[x_1, ... x_n])</tt>.
/** \brief Given <tt>e[l_1, ..., l_n]</tt> and assuming \c m_ctx is
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
then the result is
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), e[x_1, ... x_n])</tt>.
*/
expr pi_abstract_context(expr e, tag g) {
for (auto const & p : m_ctx)
@ -286,8 +377,7 @@ public:
return save_tag(::lean::mk_app(f, a), g);
}
/**
\brief Assuming \c m_ctx is
/** \brief Assuming \c m_ctx is
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
return <tt>(f l_1 ... l_n)</tt>.
*/
@ -304,12 +394,11 @@ public:
return r;
}
/**
\brief Assuming \c m_ctx is
/** \brief Assuming \c m_ctx is
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
return a fresh metavariable \c ?m with type
return a fresh metavariable \c ?m with type
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u})</tt>,
where \c ?u is a fresh universe metavariable.
where \c ?u is a fresh universe metavariable.
*/
expr mk_type_metavar(tag g) {
name n = m_ngen.next();
@ -318,12 +407,11 @@ public:
return save_tag(::lean::mk_metavar(n, t), g);
}
/**
\brief Assuming \c m_ctx is
/** \brief Assuming \c m_ctx is
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
return <tt>(?m l_1 ... l_n)</tt> where \c ?m is a fresh metavariable with type
return <tt>(?m l_1 ... l_n)</tt> where \c ?m is a fresh metavariable with type
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u})</tt>,
and \c ?u is a fresh universe metavariable.
and \c ?u is a fresh universe metavariable.
\remark The type of the resulting expression is <tt>Type.{?u}</tt>
*/
@ -331,16 +419,15 @@ public:
return apply_context(mk_type_metavar(g), g);
}
/**
\brief Given <tt>type[l_1, ..., l_n]</tt> and assuming \c m_ctx is
/** \brief Given <tt>type[l_1, ..., l_n]</tt> and assuming \c m_ctx is
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
then the result is a fresh metavariable \c ?m with type
then the result is a fresh metavariable \c ?m with type
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), type[x_1, ... x_n])</tt>.
If <tt>type</tt> is none, then the result is a fresh metavariable \c ?m1 with type
If <tt>type</tt> is none, then the result is a fresh metavariable \c ?m1 with type
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), ?m2 x1 .... xn)</tt>,
where ?m2 is another fresh metavariable with type
where ?m2 is another fresh metavariable with type
<tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u})</tt>,
and \c ?u is a fresh universe metavariable.
and \c ?u is a fresh universe metavariable.
*/
expr mk_metavar(optional<expr> const & type, tag g) {
name n = m_ngen.next();
@ -349,13 +436,12 @@ public:
return save_tag(::lean::mk_metavar(n, t), g);
}
/**
\brief Given <tt>type[l_1, ..., l_n]</tt> and assuming \c m_ctx is
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
return (?m l_1 ... l_n), where ?m is a fresh metavariable
created using \c mk_metavar.
/** \brief Given <tt>type[l_1, ..., l_n]</tt> and assuming \c m_ctx is
<tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
return (?m l_1 ... l_n), where ?m is a fresh metavariable
created using \c mk_metavar.
\see mk_metavar
\see mk_metavar
*/
expr mk_meta(optional<expr> const & type, tag g) {
expr mvar = mk_metavar(type, g);
@ -385,9 +471,8 @@ public:
return is_class(type);
}
/**
\brief Create a metavariable, but also add a class-constraint if type is a class
or a metavariable.
/** \brief Create a metavariable, but also add a class-constraint if type is a class
or a metavariable.
*/
expr mk_placeholder_meta(optional<expr> const & type, tag g) {
expr m = mk_meta(type, g);
@ -422,10 +507,8 @@ public:
return m;
}
/**
\brief Convert the metavariable to the metavariable application that captures
/** \brief Convert the metavariable to the metavariable application that captures
the context where it was defined.
*/
optional<expr> mvar_to_meta(expr mvar) {
if (auto it = m_mvar2meta.find(mlocal_name(mvar)))
@ -473,8 +556,7 @@ public:
return m;
}
/**
\brief Make sure \c f is really a function, if it is not, try to apply coercions.
/** \brief Make sure \c f is really a function, if it is not, try to apply coercions.
The result is a pair <tt>new_f, f_type</tt>, where new_f is the new value for \c f,
and \c f_type is its type (and a Pi-expression)
*/
@ -527,10 +609,9 @@ public:
return a;
}
/**
\brief Given an application \c e, where the expected type is d_type, and the argument type is a_type,
create a "delayed coercion". The idea is to create a choice constraint and postpone the coercion
search. We do that whenever d_type or a_type is a metavar application, and d_type or a_type is a coercion source/target.
/** \brief Given an application \c e, where the expected type is d_type, and the argument type is a_type,
create a "delayed coercion". The idea is to create a choice constraint and postpone the coercion
search. We do that whenever d_type or a_type is a metavar application, and d_type or a_type is a coercion source/target.
*/
expr mk_delayed_coercion(expr const & e, expr const & d_type, expr const & a_type) {
expr a = app_arg(e);
@ -884,14 +965,23 @@ public:
}
/** \brief Apply substitution and solve remaining metavariables using tactics. */
expr apply(substitution & s, expr const & e) {
expr apply(substitution & s, expr const & e, name_set & univ_params, buffer<name> & new_params) {
expr r = s.instantiate(e);
if (has_univ_metavar(r))
r = univ_metavars_to_params_fn(m_env, m_lls, s, univ_params, new_params)(r);
r = solve_unassigned_mvars(s, r);
display_unassigned_mvars(r, s);
return r;
}
expr operator()(expr const & e) {
std::tuple<expr, level_param_names> apply(substitution & s, expr const & e) {
auto ps = collect_univ_params(e);
buffer<name> new_ps;
expr r = apply(s, e, ps, new_ps);
return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end()));
}
std::tuple<expr, level_param_names> operator()(expr const & e) {
expr r = visit(e);
auto p = solve().pull();
lean_assert(p);
@ -908,7 +998,7 @@ public:
return r;
}
expr operator()(expr const & e, expr const & expected_type) {
std::tuple<expr, level_param_names> operator()(expr const & e, expr const & expected_type) {
expr r = visit(e);
expr r_type = infer_type(r);
environment env = m_env;
@ -927,7 +1017,7 @@ public:
return apply(s, r);
}
std::pair<expr, expr> operator()(expr const & t, expr const & v, name const & n) {
std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n) {
expr r_t = visit(t);
expr r_v = visit(v);
expr r_v_type = infer_type(r_v);
@ -944,18 +1034,23 @@ public:
auto p = solve().pull();
lean_assert(p);
substitution s = p->first;
return mk_pair(apply(s, r_t), apply(s, r_v));
name_set univ_params = collect_univ_params(r_v, collect_univ_params(r_t));
buffer<name> new_params;
expr new_r_t = apply(s, r_t, univ_params, new_params);
expr new_r_v = apply(s, r_v, univ_params, new_params);
return std::make_tuple(new_r_t, new_r_v, to_list(new_params.begin(), new_params.end()));
}
};
static name g_tmp_prefix = name::mk_internal_unique_name();
expr elaborate(environment const & env, io_state const & ios, expr const & e, pos_info_provider * pp, bool check_unassigned) {
return elaborator(env, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e);
std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios,
expr const & e, pos_info_provider * pp, bool check_unassigned) {
return elaborator(env, lls, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e);
}
std::pair<expr, expr> elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v,
pos_info_provider * pp) {
return elaborator(env, ios, name_generator(g_tmp_prefix), pp, true)(t, v, n);
std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios,
name const & n, expr const & t, expr const & v, pos_info_provider * pp) {
return elaborator(env, lls, ios, name_generator(g_tmp_prefix), pp, true)(t, v, n);
}
}

8
src/frontends/lean/elaborator.h
View file

@ -10,9 +10,11 @@ Author: Leonardo de Moura
#include "kernel/environment.h"
#include "kernel/metavar.h"
#include "library/io_state.h"
#include "frontends/lean/local_decls.h"
namespace lean {
expr elaborate(environment const & env, io_state const & ios, expr const & e, pos_info_provider * pp = nullptr, bool check_unassigned = true);
std::pair<expr, expr> elaborate(environment const & env, io_state const & ios, name const & n, expr const & t, expr const & v,
pos_info_provider * pp = nullptr);
std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios, expr const & e,
pos_info_provider * pp = nullptr, bool check_unassigned = true);
std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios,
name const & n, expr const & t, expr const & v, pos_info_provider * pp = nullptr);
}

798
src/frontends/lean/inductive_cmd.cpp
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include "util/sstream.h"
#include "util/name_map.h"
#include "kernel/replace_fn.h"
@ -16,6 +17,7 @@ Author: Leonardo de Moura
#include "library/placeholder.h"
#include "library/aliases.h"
#include "library/explicit.h"
#include "library/opaque_hints.h"
#include "frontends/lean/decl_cmds.h"
#include "frontends/lean/util.h"
#include "frontends/lean/parser.h"
@ -36,72 +38,6 @@ using inductive::inductive_decl_intros;
using inductive::intro_rule_name;
using inductive::intro_rule_type;
// Make sure that every inductive datatype (in decls) occurring in \c type has
// the universe levels \c lvl_params and section parameters \c section_params
static expr fix_inductive_occs(expr const & type, buffer<inductive_decl> const & decls,
buffer<name> const & lvl_params, buffer<expr> const & section_params) {
return replace(type, [&](expr const & e, unsigned) {
if (!is_constant(e))
return none_expr();
if (!std::any_of(decls.begin(), decls.end(),
[&](inductive_decl const & d) { return const_name(e) == inductive_decl_name(d); }))
return none_expr();
// found target
levels ls = const_levels(e);
unsigned n = length(ls);
if (n < lvl_params.size()) {
unsigned i = lvl_params.size() - n;
while (i > 0) {
--i;
ls = cons(mk_param_univ(lvl_params[i]), ls);
}
}
expr r = update_constant(e, ls);
for (unsigned i = 0; i < section_params.size(); i++)
r = mk_app(r, section_params[i]);
return some_expr(r);
});
}
static level mk_result_level(bool impredicative, buffer<level> const & ls) {
if (ls.empty()) {
return impredicative ? mk_level_one() : mk_level_zero();
} else {
level r = ls[0];
for (unsigned i = 1; i < ls.size(); i++)
r = mk_max(r, ls[i]);
if (is_not_zero(r))
return r;
else
return impredicative ? mk_max(r, mk_level_one()) : r;
}
}
static expr update_result_sort(type_checker & tc, expr t, level const & l) {
t = tc.whnf(t);
if (is_pi(t)) {
return update_binding(t, binding_domain(t), update_result_sort(tc, binding_body(t), l));
} else if (is_sort(t)) {
return update_sort(t, l);
} else {
lean_unreachable();
}
}
/** \brief Return the universe level of the given inductive datatype declaration. */
level get_datatype_result_level(type_checker & tc, inductive_decl const & d) {
expr d_t = tc.whnf(inductive_decl_type(d));
while (is_pi(d_t)) {
d_t = tc.whnf(binding_body(d_t));
}
if (!is_sort(d_t)) {
std::cout << "ERROR: " << inductive_decl_type(d) << "\n";
throw exception(sstream() << "invalid inductive datatype '" << inductive_decl_name(d) << "', "
"resultant type is not a sort");
}
return sort_level(d_t);
}
/** \brief Return true if \c u occurs in \c l */
bool occurs(level const & u, level const & l) {
bool found = false;
@ -113,37 +49,6 @@ bool occurs(level const & u, level const & l) {
return found;
}
static name g_tmp_prefix = name::mk_internal_unique_name();
/**
\brief Given a type \c t for an introduction rule, store the universe of the types of non-parameters in \c ls.
\remark aux_u is an temporary universe used for inductive decls. It should be ignored.
*/
static void accumulate_levels(type_checker & tc, expr t, unsigned num_params, level const & aux_u, buffer<level> & ls) {
name_generator ngen(g_tmp_prefix);
unsigned i = 0;
while (is_pi(t)) {
if (i >= num_params) {
expr s = tc.ensure_type(binding_domain(t));
level l = sort_level(s);
if (l == aux_u) {
// ignore, this is the auxiliary level
} else if (occurs(aux_u, l)) {
throw exception("failed to infer inductive datatype resultant universe, provide the universe levels explicitly");
} else if (std::find(ls.begin(), ls.end(), l) == ls.end()) {
ls.push_back(l);
}
}
t = instantiate(binding_body(t), mk_local(ngen.next(), binding_name(t), binding_domain(t), binding_info(t)));
i++;
}
}
void throw_all_or_nothing() {
throw exception("invalid mutually recursive datatype declaration, "
"if the universe level of one type is provided, then all of them should be");
}
inductive_decl update_inductive_decl(inductive_decl const & d, expr const & t) {
return inductive_decl(inductive_decl_name(d), t, inductive_decl_intros(d));
}
@ -156,231 +61,522 @@ intro_rule update_intro_rule(intro_rule const & r, expr const & t) {
return intro_rule(intro_rule_name(r), t);
}
static void elaborate_inductive(buffer<inductive_decl> & decls, level_param_names const & lvls, unsigned num_params, parser & p) {
// temporary environment used during elaboration
environment env = p.env();
// add fake universe level
name u_name(g_tmp_prefix, "u");
env = env.add_universe(u_name);
level u = mk_global_univ(u_name);
std::unique_ptr<type_checker> tc(new type_checker(env));
bool infer_result_universe = false;
unsigned first = true;
// elaborate inductive datatype types, and declare them in temporary environment.
for (inductive_decl & d : decls) {
level l = get_datatype_result_level(*tc, d);
expr t = inductive_decl_type(d);
if (is_placeholder(l)) {
if (first)
infer_result_universe = true;
else if (!infer_result_universe)
throw_all_or_nothing();
t = update_result_sort(*tc, t, u);
} else if (!first && infer_result_universe) {
throw_all_or_nothing();
}
t = p.elaborate(env, t);
env = env.add(check(env, mk_var_decl(inductive_decl_name(d), lvls, t)));
d = update_inductive_decl(d, t);
first = false;
}
tc.reset(new type_checker(env));
buffer<level> r_lvls; // used for inferring the universe level of resultant datatypes.
// elaborate introduction rules using temporary environment
for (inductive_decl & d : decls) {
buffer<intro_rule> intros;
for (intro_rule const & ir : inductive_decl_intros(d)) {
expr t = p.elaborate(env, intro_rule_type(ir));
if (infer_result_universe)
accumulate_levels(*tc, t, num_params, u, r_lvls);
intros.push_back(update_intro_rule(ir, t));
}
d = update_inductive_decl(d, intros);
}
if (infer_result_universe) {
level r_lvl = normalize(mk_result_level(env.impredicative(), r_lvls));
for (inductive_decl & d : decls) {
expr t = inductive_decl_type(d);
t = update_result_sort(*tc, t, r_lvl);
d = update_inductive_decl(d, t);
}
}
}
static name g_tmp_prefix = name::mk_internal_unique_name();
static environment create_alias(environment const & env, name const & full_id, name const & id, levels const & section_leves,
buffer<expr> const & section_params, parser & p) {
if (in_section(env)) {
expr r = mk_explicit(mk_constant(full_id, section_leves));
for (unsigned i = 0; i < section_params.size(); i++)
r = mk_app(r, section_params[i]);
p.add_local_expr(id, r);
return env;
} else if (full_id != id) {
return add_alias(env, id, mk_constant(full_id));
} else {
return env;
}
}
struct inductive_cmd_fn {
typedef std::unique_ptr<type_checker> type_checker_ptr;
parser & m_p;
environment m_env;
type_checker_ptr m_tc;
name m_namespace; // current namespace
pos_info m_pos; // current position for reporting errors
bool m_first; // true if parsing the first inductive type in a mutually recursive inductive decl.
buffer<name> m_explict_levels;
buffer<name> m_levels;
bool m_using_explicit_levels; // true if the user is providing explicit universe levels
unsigned m_num_params; // number of parameters
level m_u; // temporary auxiliary global universe used for inferring the result universe of an inductive datatype declaration.
bool m_infer_result_universe;
name_set m_relaxed_implicit_infer; // set of introduction rules where we do not use strict implicit parameter infererence
environment inductive_cmd(parser & p) {
parser::no_undef_id_error_scope err_scope(p);
environment env = p.env();
name const & ns = get_namespace(env);
bool first = true;
buffer<name> ls_buffer;
name_map<name> id_to_short_id;
// store intro rule name that are markes for relaxed implicit argument inference.
name_set relaxed_implicit_inference;
unsigned num_params = 0;
bool explicit_levels = false;
buffer<inductive_decl> decls;
while (true) {
parser::local_scope l_scope(p);
auto id_pos = p.pos();
name id = p.check_id_next("invalid inductive declaration, identifier expected");
inductive_cmd_fn(parser & p):m_p(p) {
m_env = p.env();
m_first = true;
m_using_explicit_levels = false;
m_num_params = 0;
name u_name(g_tmp_prefix, "u");
m_env = m_env.add_universe(u_name);
m_u = mk_global_univ(u_name);
m_infer_result_universe = false;
m_namespace = get_namespace(m_env);
m_tc = mk_type_checker_with_hints(m_env, m_p.mk_ngen());
}
[[ noreturn ]] void throw_error(char const * error_msg) { throw parser_error(error_msg, m_pos); }
[[ noreturn ]] void throw_error(sstream const & strm) { throw parser_error(strm, m_pos); }
/** \brief Parse the name of an inductive datatype or introduction rule,
prefix the current namespace to it and return it.
*/
name parse_decl_name() {
m_pos = m_p.pos();
name id = m_p.check_id_next("invalid declaration, identifier expected");
check_atomic(id);
name full_id = ns + id;
id_to_short_id.insert(full_id, id);
return m_namespace + id;
}
/** \brief Parse inductive declaration universe parameters.
If this is the first declaration in a mutually recursive block, then this method
stores the levels in m_explict_levels, and set m_using_explicit_levels to true (iff they were provided).
If this is not the first declaration, then this function just checks if the parsed parameters
match the ones in the first declaration (stored in \c m_explict_levels)
*/
void parse_inductive_univ_params() {
buffer<name> curr_ls_buffer;
expr type;
optional<parser::param_universe_scope> pu_scope;
if (parse_univ_params(p, curr_ls_buffer)) {
if (first) {
explicit_levels = true;
ls_buffer.append(curr_ls_buffer);
} else if (!explicit_levels) {
throw parser_error("invalid mutually recursive declaration, "
"explicit universe levels were not provided for previous inductive types in this declaration",
id_pos);
} else if (curr_ls_buffer.size() != ls_buffer.size()) {
throw parser_error("invalid mutually recursive declaration, "
"all inductive types must have the same number of universe paramaters", id_pos);
if (parse_univ_params(m_p, curr_ls_buffer)) {
if (m_first) {
m_using_explicit_levels = true;
m_explict_levels.append(curr_ls_buffer);
} else if (!m_using_explicit_levels) {
throw_error("invalid mutually recursive declaration, "
"explicit universe levels were not provided for previous inductive types in this declaration");
} else if (curr_ls_buffer.size() != m_explict_levels.size()) {
throw_error("invalid mutually recursive declaration, "
"all inductive types must have the same number of universe paramaters");
} else {
for (unsigned i = 0; i < ls_buffer.size(); i++) {
if (curr_ls_buffer[i] != ls_buffer[i])
throw parser_error("invalid mutually recursive inductive declaration, "
"all inductive types must have the same universe paramaters", id_pos);
for (unsigned i = 0; i < m_explict_levels.size(); i++) {
if (curr_ls_buffer[i] != m_explict_levels[i])
throw_error("invalid mutually recursive inductive declaration, "
"all inductive types must have the same universe paramaters");
}
}
} else {
if (first) {
explicit_levels = false;
} else if (explicit_levels) {
throw parser_error("invalid mutually recursive declaration, "
"explicit universe levels were provided for previous inductive types in this declaration",
id_pos);
if (m_first) {
m_using_explicit_levels = false;
} else if (m_using_explicit_levels) {
throw_error("invalid mutually recursive declaration, "
"explicit universe levels were provided for previous inductive types in this declaration");
}
// initialize param_universe_scope, we are using implicit universe levels
pu_scope.emplace(p);
}
}
/** \brief Parse the type of an inductive datatype */
expr parse_datatype_type() {
expr type;
buffer<expr> ps;
local_environment lenv = env;
auto params_pos = p.pos();
if (!p.curr_is_token(g_colon)) {
lenv = p.parse_binders(ps);
p.check_token_next(g_colon, "invalid inductive declaration, ':' expected");
{
parser::placeholder_universe_scope place_scope(p);
type = p.parse_scoped_expr(ps, lenv);
}
type = p.pi_abstract(ps, type);
m_pos = m_p.pos();
if (!m_p.curr_is_token(g_colon)) {
m_p.parse_binders(ps);
m_p.check_token_next(g_colon, "invalid inductive declaration, ':' expected");
type = m_p.parse_scoped_expr(ps);
type = m_p.pi_abstract(ps, type);
} else {
p.next();
parser::placeholder_universe_scope place_scope(p);
type = p.parse_scoped_expr(ps, lenv);
m_p.next();
type = m_p.parse_expr();
}
// check if number of parameters
if (first) {
num_params = ps.size();
} else {
if (m_first) {
m_num_params = ps.size();
} else if (m_num_params != ps.size()) {
// mutually recursive declaration checks
if (num_params != ps.size()) {
throw parser_error("invalid mutually recursive inductive declaration, "
"all inductive types must have the same number of arguments",
params_pos);
}
throw_error("invalid mutually recursive inductive declaration, all inductive types must have the same number of arguments");
}
// parse introduction rules
p.check_token_next(g_assign, "invalid inductive declaration, ':=' expected");
buffer<intro_rule> intros;
while (p.curr_is_token(g_bar)) {
p.next();
name intro_id = p.check_id_next("invalid introduction rule, identifier expected");
check_atomic(intro_id);
name full_intro_id = ns + intro_id;
id_to_short_id.insert(full_intro_id, intro_id);
bool strict = true;
if (p.curr_is_token(g_lcurly)) {
p.next();
p.check_token_next(g_rcurly, "invalid introduction rule, '}' expected");
strict = false;
relaxed_implicit_inference.insert(full_intro_id);
}
p.check_token_next(g_colon, "invalid introduction rule, ':' expected");
expr intro_type = p.parse_scoped_expr(ps, lenv);
intro_type = p.pi_abstract(ps, intro_type);
intro_type = infer_implicit(intro_type, ps.size(), strict);
intros.push_back(intro_rule(full_intro_id, intro_type));
}
decls.push_back(inductive_decl(full_id, type, to_list(intros.begin(), intros.end())));
if (!p.curr_is_token(g_with))
break;
p.next();
first = false;
return type;
}
// Collect (section) locals occurring in inductive_decls, and abstract them
// using these additional parameters.
name_set used_levels;
name_set section_locals;
for (inductive_decl const & d : decls) {
used_levels = collect_univ_params(inductive_decl_type(d), used_levels);
section_locals = collect_locals(inductive_decl_type(d), section_locals);
for (auto const & ir : inductive_decl_intros(d)) {
used_levels = collect_univ_params(intro_rule_type(ir), used_levels);
section_locals = collect_locals(intro_rule_type(ir), section_locals);
}
}
update_univ_parameters(ls_buffer, used_levels, p);
buffer<expr> section_params;
mk_section_params(section_locals, p, section_params);
// First, add section_params to inductive types type.
// We don't update the introduction rules in the first pass, because
// we will mark all section_params as implicit for them.
for (inductive_decl & d : decls) {
d = update_inductive_decl(d, p.pi_abstract(section_params, inductive_decl_type(d)));
}
// Add section_params to introduction rules type, and also "fix"
// occurrences of inductive types.
for (inductive_decl & d : decls) {
buffer<intro_rule> new_irs;
for (auto const & ir : inductive_decl_intros(d)) {
expr type = intro_rule_type(ir);
type = fix_inductive_occs(type, decls, ls_buffer, section_params);
type = p.pi_abstract(section_params, type);
bool strict = relaxed_implicit_inference.contains(intro_rule_name(ir));
type = infer_implicit(type, section_params.size(), strict);
new_irs.push_back(update_intro_rule(ir, type));
}
d = update_inductive_decl(d, new_irs);
}
num_params += section_params.size();
level_param_names ls = to_list(ls_buffer.begin(), ls_buffer.end());
elaborate_inductive(decls, ls, num_params, p);
env = module::add_inductive(env, ls, num_params, to_list(decls.begin(), decls.end()));
// Create aliases/local refs
levels section_levels = collect_section_levels(ls, p);
for (inductive_decl const & d : decls) {
name const & n = inductive_decl_name(d);
env = create_alias(env, n, *id_to_short_id.find(n), section_levels, section_params, p);
env = create_alias(env, n.append_after("_rec"), id_to_short_id.find(n)->append_after("_rec"), section_levels, section_params, p);
for (intro_rule const & ir : inductive_decl_intros(d)) {
name const & n = intro_rule_name(ir);
env = create_alias(env, n, *id_to_short_id.find(n), section_levels, section_params, p);
/** \brief Return the universe level of the given type, if it is not a sort, then raise an exception. */
level get_datatype_result_level(expr d_type) {
d_type = m_tc->whnf(d_type);
while (is_pi(d_type)) {
d_type = m_tc->whnf(binding_body(d_type));
}
if (!is_sort(d_type))
throw_error(sstream() << "invalid inductive datatype, resultant type is not a sort");
return sort_level(d_type);
}
/** \brief Update the result sort of the given type */
expr update_result_sort(expr t, level const & l) {
t = m_tc->whnf(t);
if (is_pi(t)) {
return update_binding(t, binding_domain(t), update_result_sort(binding_body(t), l));
} else if (is_sort(t)) {
return update_sort(t, l);
} else {
lean_unreachable();
}
}
return env;
/** \brief Elaborate the type of an inductive declaration. */
std::tuple<expr, level_param_names> elaborate_inductive_type(expr d_type) {
level l = get_datatype_result_level(d_type);
if (is_placeholder(l)) {
if (m_using_explicit_levels)
throw_error("resultant universe must be provided, when using explicit universe levels");
d_type = update_result_sort(d_type, m_u);
m_infer_result_universe = true;
}
return m_p.elaborate(m_env, d_type);
}
/** \brief Create a local constant based on the given binding */
expr mk_local_for(expr const & b) {
return mk_local(m_p.mk_fresh_name(), binding_name(b), binding_domain(b), binding_info(b));
}
/** \brief Check if the parameters of \c d_type and \c first_d_type are equal. */
void check_params(expr d_type, expr first_d_type) {
for (unsigned i = 0; i < m_num_params; i++) {
if (!m_tc->is_def_eq(binding_domain(d_type), binding_domain(first_d_type)))
throw_error(sstream() << "invalid parameter #" << (i+1) << " in mutually recursive inductive declaration, "
<< "all inductive types must have equivalent parameters");
expr l = mk_local_for(d_type);
d_type = instantiate(binding_body(d_type), l);
first_d_type = instantiate(binding_body(first_d_type), l);
}
}
/** \brief Check if the level names in d_lvls and \c first_d_lvls are equal. */
void check_levels(level_param_names d_lvls, level_param_names first_d_lvls) {
while (!is_nil(d_lvls) && !is_nil(first_d_lvls)) {
if (head(d_lvls) != head(first_d_lvls))
throw_error(sstream() << "invalid mutually recursive inductive declaration, "
<< "all declarations must use the same universe parameter names, mismatch: '"
<< head(d_lvls) << "' and '" << head(first_d_lvls) << "' "
<< "(if the universe parameters were inferred, then provide them explicitly to fix the problem)");
d_lvls = tail(d_lvls);
first_d_lvls = tail(first_d_lvls);
}
if (!is_nil(d_lvls) || !is_nil(first_d_lvls))
throw_error("invalid mutually recursive inductive declaration, "
"all declarations must have the same number of arguments "
"(this is error is probably due to inferred implicit parameters, provide all parameters explicitly to fix the problem");
}
/** \brief Add the parameters of the inductive decl type to the local scoped.
This method is executed before parsing introduction rules.
*/
void add_params_to_local_scope(expr d_type, buffer<expr> & params) {
for (unsigned i = 0; i < m_num_params; i++) {
expr l = mk_local_for(d_type);
m_p.add_local(l);
params.push_back(l);
d_type = instantiate(binding_body(d_type), l);
}
}
/** \brief Parse introduction rules in the scope of the given parameters.
Introduction rules with the annotation '{}' are marked for relaxed (aka non-strict) implicit parameter inference.
*/
list<intro_rule> parse_intro_rules(buffer<expr> & params) {
buffer<intro_rule> intros;
while (m_p.curr_is_token(g_bar)) {
m_p.next();
name intro_name = parse_decl_name();
bool strict = true;
if (m_p.curr_is_token(g_lcurly)) {
m_p.next();
m_p.check_token_next(g_rcurly, "invalid introduction rule, '}' expected");
strict = false;
m_relaxed_implicit_infer.insert(intro_name);
}
m_p.check_token_next(g_colon, "invalid introduction rule, ':' expected");
expr intro_type = m_p.parse_scoped_expr(params, m_env);
intro_type = m_p.pi_abstract(params, intro_type);
intro_type = infer_implicit(intro_type, params.size(), strict);
intros.push_back(intro_rule(intro_name, intro_type));
}
return to_list(intros.begin(), intros.end());
}
void parse_inductive_decls(buffer<inductive_decl> & decls) {
optional<expr> first_d_type;
optional<level_param_names> first_d_lvls;
while (true) {
parser::local_scope l_scope(m_p);
name d_name = parse_decl_name();
parse_inductive_univ_params();
expr d_type = parse_datatype_type();
m_p.check_token_next(g_assign, "invalid inductive declaration, ':=' expected");
level_param_names d_lvls;
std::tie(d_type, d_lvls) = elaborate_inductive_type(d_type);
if (!m_first) {
check_params(d_type, *first_d_type);
check_levels(d_lvls, *first_d_lvls);
}
buffer<expr> params;
add_params_to_local_scope(d_type, params);
auto d_intro_rules = parse_intro_rules(params);
decls.push_back(inductive_decl(d_name, d_type, d_intro_rules));
if (!m_p.curr_is_token(g_with)) {
m_levels.append(m_explict_levels);
for (auto l : d_lvls) m_levels.push_back(l);
break;
}
m_p.next();
m_first = false;
first_d_type = d_type;
first_d_lvls = d_lvls;
}
}
/** \brief Include in m_levels any section level referenced by decls. */
void include_section_levels(buffer<inductive_decl> const & decls) {
if (!in_section(m_env))
return;
name_set all_lvl_params;
for (auto const & d : decls) {
all_lvl_params = collect_univ_params(inductive_decl_type(d), all_lvl_params);
for (auto const & ir : inductive_decl_intros(d)) {
all_lvl_params = collect_univ_params(intro_rule_type(ir), all_lvl_params);
}
}
buffer<name> section_lvls;
all_lvl_params.for_each([&](name const & l) {
if (std::find(m_levels.begin(), m_levels.end(), l) == m_levels.end())
section_lvls.push_back(l);
});
std::sort(section_lvls.begin(), section_lvls.end(), [&](name const & n1, name const & n2) {
return m_p.get_local_level_index(n1) < m_p.get_local_level_index(n2);
});
buffer<name> new_levels;
new_levels.append(section_lvls);
new_levels.append(m_levels);
m_levels.clear();
m_levels.append(new_levels);
}
/** \brief Collect section local parameters used in the inductive decls */
name_set collect_section_locals(buffer<inductive_decl> const & decls) {
name_set section_locals;
for (auto const & d : decls) {
section_locals = collect_locals(inductive_decl_type(d), section_locals);
for (auto const & ir : inductive_decl_intros(d)) {
section_locals = collect_locals(intro_rule_type(ir), section_locals);
}
}
return section_locals;
}
/** \brief Make sure that every occurrence of an inductive datatype (in decls) in \c type has
section parameters \c section_params as arguments.
*/
expr fix_inductive_occs(expr const & type, buffer<inductive_decl> const & decls, buffer<expr> const & section_params) {
return replace(type, [&](expr const & e, unsigned) {
if (!is_constant(e))
return none_expr();
if (!std::any_of(decls.begin(), decls.end(),
[&](inductive_decl const & d) { return const_name(e) == inductive_decl_name(d); }))
return none_expr();
// found target
expr r = mk_app(mk_explicit(e), section_params);
return some_expr(r);
});
}
/** \brief Include the used section parameters as additional arguments.
The section parameters are stored in section_params
*/
void abstract_section_locals(buffer<inductive_decl> & decls, buffer<expr> & section_params) {
if (!in_section(m_env))
return;
name_set section_locals = collect_section_locals(decls);
if (section_locals.empty())
return;
mk_section_params(section_locals, m_p, section_params);
// First, add section_params to inductive types type.
for (inductive_decl & d : decls) {
d = update_inductive_decl(d, m_p.pi_abstract(section_params, inductive_decl_type(d)));
}
// Add section_params to introduction rules type, and also "fix"
// occurrences of inductive types.
for (inductive_decl & d : decls) {
buffer<intro_rule> new_irs;
for (auto const & ir : inductive_decl_intros(d)) {
expr type = intro_rule_type(ir);
type = fix_inductive_occs(type, decls, section_params);
type = m_p.pi_abstract(section_params, type);
bool strict = m_relaxed_implicit_infer.contains(intro_rule_name(ir));
type = infer_implicit(type, section_params.size(), strict);
new_irs.push_back(update_intro_rule(ir, type));
}
d = update_inductive_decl(d, new_irs);
}
}
/** \brief Declare inductive types in the scratch environment as var_decls.
We use this trick to be able to elaborate the introduction rules.
*/
void declare_inductive_types(buffer<inductive_decl> & decls) {
level_param_names ls = to_list(m_levels.begin(), m_levels.end());
for (auto const & d : decls) {
name d_name; expr d_type;
std::tie(d_name, d_type, std::ignore) = d;
m_env = m_env.add(check(m_env, mk_var_decl(d_name, ls, d_type)));
}
m_tc = mk_type_checker_with_hints(m_env, m_p.mk_ngen());
}
/** \brief Traverse the introduction rule type and collect the universes where non-parameters reside in \c r_lvls.
This information is used to compute the resultant universe level for the inductive datatype declaration.
*/
void accumulate_levels(expr intro_type, buffer<level> & r_lvls) {
unsigned i = 0;
while (is_pi(intro_type)) {
if (i >= m_num_params) {
expr s = m_tc->ensure_type(binding_domain(intro_type));
level l = sort_level(s);
if (l == m_u) {
// ignore, this is the auxiliary level
} else if (occurs(m_u, l)) {
throw exception("failed to infer inductive datatype resultant universe, provide the universe levels explicitly");
} else if (std::find(r_lvls.begin(), r_lvls.end(), l) == r_lvls.end()) {
r_lvls.push_back(l);
}
}
intro_type = instantiate(binding_body(intro_type), mk_local_for(intro_type));
i++;
}
}
/** \brief Elaborate introduction rules and destructively update \c decls with the elaborated versions.
\remark This method is invoked only after all inductive datatype types have been elaborated and
inserted into the scratch environment m_env.
This method also store in r_lvls inferred levels that must be in the resultant universe.
*/
void elaborate_intro_rules(buffer<inductive_decl> & decls, buffer<level> & r_lvls) {
for (auto & d : decls) {
name d_name; expr d_type; list<intro_rule> d_intros;
std::tie(d_name, d_type, d_intros) = d;
buffer<intro_rule> new_irs;
for (auto const & ir : d_intros) {
name ir_name; expr ir_type;
std::tie(ir_name, ir_type) = ir;
level_param_names new_ls;
std::tie(ir_type, new_ls) = m_p.elaborate(m_env, ir_type);
for (auto l : new_ls) m_levels.push_back(l);
accumulate_levels(ir_type, r_lvls);
new_irs.push_back(intro_rule(ir_name, ir_type));
}
d = inductive_decl(d_name, d_type, to_list(new_irs.begin(), new_irs.end()));
}
}
/** \brief If old_num_univ_params < m_levels.size(), then new universe params were collected when elaborating
the introduction rules. This method include them in all occurrences of the inductive datatype decls.
*/
void include_extra_univ_levels(buffer<inductive_decl> & decls, unsigned old_num_univ_params) {
if (m_levels.size() == old_num_univ_params)
return;
buffer<level> tmp;
for (auto l : m_levels) tmp.push_back(mk_param_univ(l));
levels new_ls = to_list(tmp.begin(), tmp.end());
for (auto & d : decls) {
buffer<intro_rule> new_irs;
for (auto & ir : inductive_decl_intros(d)) {
expr new_type = replace(intro_rule_type(ir), [&](expr const & e, unsigned) {
if (!is_constant(e))
return none_expr();
if (!std::any_of(decls.begin(), decls.end(),
[&](inductive_decl const & d) { return const_name(e) == inductive_decl_name(d); }))
return none_expr();
// found target
expr r = update_constant(e, new_ls);
return some_expr(r);
});
new_irs.push_back(update_intro_rule(ir, new_type));
}
d = update_inductive_decl(d, new_irs);
}
}
/** \brief Create the resultant universe level using the levels computed during introduction rule elaboration */
level mk_result_level(buffer<level> const & r_lvls) {
bool impredicative = m_env.impredicative();
if (r_lvls.empty()) {
return impredicative ? mk_level_one() : mk_level_zero();
} else {
level r = r_lvls[0];
for (unsigned i = 1; i < r_lvls.size(); i++)
r = mk_max(r, r_lvls[i]);
if (is_not_zero(r))
return normalize(r);
else
return impredicative ? normalize(mk_max(r, mk_level_one())) : normalize(r);
}
}
/** \brief Update the resultant universe level of the inductive datatypes using the inferred universe \c r_lvl */
void update_resultant_universe(buffer<inductive_decl> & decls, level const & r_lvl) {
for (inductive_decl & d : decls) {
expr t = inductive_decl_type(d);
t = update_result_sort(t, r_lvl);
d = update_inductive_decl(d, t);
}
}
/** \brief Create an alias for the fully qualified name \c full_id. */
environment create_alias(environment const & env, name const & full_id, levels const & section_leves, buffer<expr> const & section_params) {
name id(full_id.get_string());
if (in_section(env)) {
expr r = mk_explicit(mk_constant(full_id, section_leves));
r = mk_app(r, section_params);
m_p.add_local_expr(id, r);
return env;
} else if (full_id != id) {
return add_alias(env, id, mk_constant(full_id));
} else {
return env;
}
}
/** \brief Add aliases for the inductive datatype, introduction and elimination rules */
environment add_aliases(environment env, level_param_names const & ls, buffer<expr> const & section_params,
buffer<inductive_decl> const & decls) {
// Create aliases/local refs
levels section_levels = collect_section_levels(ls, m_p);
for (auto & d : decls) {
name d_name = inductive_decl_name(d);
name d_short_name(d_name.get_string());
env = create_alias(env, d_name, section_levels, section_params);
env = create_alias(env, d_name.append_after("_rec"), section_levels, section_params);
for (intro_rule const & ir : inductive_decl_intros(d)) {
name ir_name = intro_rule_name(ir);
env = create_alias(env, ir_name, section_levels, section_params);
}
}
return env;
}
/** \brief Auxiliary method used for debugging */
void display(std::ostream & out, buffer<inductive_decl> const & decls) {
if (!m_levels.empty()) {
out << "inductive level params:";
for (auto l : m_levels) out << " " << l;
out << "\n";
}
for (auto const & d : decls) {
name d_name; expr d_type; list<intro_rule> d_irules;
std::tie(d_name, d_type, d_irules) = d;
out << "inductive " << d_name << " : " << d_type << "\n";
for (auto const & ir : d_irules) {
name ir_name; expr ir_type;
std::tie(ir_name, ir_type) = ir;
out << " | " << ir_name << " : " << ir_type << "\n";
}
}
out << "\n";
}
environment operator()() {
parser::no_undef_id_error_scope err_scope(m_p);
buffer<inductive_decl> decls;
parse_inductive_decls(decls);
include_section_levels(decls);
buffer<expr> section_params;
abstract_section_locals(decls, section_params);
m_num_params += section_params.size();
declare_inductive_types(decls);
unsigned num_univ_params = m_levels.size();
buffer<level> r_lvls;
elaborate_intro_rules(decls, r_lvls);
include_extra_univ_levels(decls, num_univ_params);
if (m_infer_result_universe) {
level r_lvl = mk_result_level(r_lvls);
update_resultant_universe(decls, r_lvl);
}
level_param_names ls = to_list(m_levels.begin(), m_levels.end());
environment env = module::add_inductive(m_p.env(), ls, m_num_params, to_list(decls.begin(), decls.end()));
return add_aliases(env, ls, section_params, decls);
}
};
environment inductive_cmd(parser & p) {
return inductive_cmd_fn(p)();
}
void register_inductive_cmd(cmd_table & r) {
add_cmd(r, cmd_info("inductive", "declare an inductive datatype", inductive_cmd));
}

48
src/frontends/lean/parser.cpp
View file

@ -57,20 +57,6 @@ parser::local_scope::~local_scope() {
m_p.m_env = m_env;
}
parser::param_universe_scope::param_universe_scope(parser & p):m_p(p), m_old(m_p.m_type_use_placeholder) {
m_p.m_type_use_placeholder = false;
}
parser::param_universe_scope::~param_universe_scope() {
m_p.m_type_use_placeholder = m_old;
}
parser::placeholder_universe_scope::placeholder_universe_scope(parser & p):m_p(p), m_old(m_p.m_type_use_placeholder) {
m_p.m_type_use_placeholder = true;
}
parser::placeholder_universe_scope::~placeholder_universe_scope() {
m_p.m_type_use_placeholder = m_old;
}
parser::no_undef_id_error_scope::no_undef_id_error_scope(parser & p):m_p(p), m_old(m_p.m_no_undef_id_error) {
m_p.m_no_undef_id_error = true;
}
@ -91,7 +77,6 @@ parser::parser(environment const & env, io_state const & ios,
m_pos_table(std::make_shared<pos_info_table>()) {
m_scanner.set_line(line);
m_num_threads = num_threads;
m_type_use_placeholder = true;
m_no_undef_id_error = false;
m_found_errors = false;
updt_options();
@ -314,14 +299,12 @@ expr parser::mk_app(std::initializer_list<expr> const & args, pos_info const & p
}
void parser::push_local_scope() {
if (m_type_use_placeholder)
m_local_level_decls.push();
m_local_level_decls.push();
m_local_decls.push();
}
void parser::pop_local_scope() {
if (m_type_use_placeholder)
m_local_level_decls.pop();
m_local_level_decls.pop();
m_local_decls.pop();
}
@ -481,35 +464,22 @@ level parser::parse_level(unsigned rbp) {
}
expr parser::mk_Type() {
if (m_type_use_placeholder) {
return mk_sort(mk_level_placeholder());
} else {
unsigned i = 1;
name l("l");
name r = l.append_after(i);
while (m_local_level_decls.contains(r) || m_env.is_universe(r)) {
i++;
r = l.append_after(i);
}
level lvl = mk_param_univ(r);
add_local_level(r, lvl);
return mk_sort(lvl);
}
return mk_sort(mk_level_placeholder());
}
expr parser::elaborate(expr const & e, bool check_unassigned) {
std::tuple<expr, level_param_names> parser::elaborate(expr const & e, bool check_unassigned) {
parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
return ::lean::elaborate(m_env, m_ios, e, &pp, check_unassigned);
return ::lean::elaborate(m_env, m_local_level_decls, m_ios, e, &pp, check_unassigned);
}
expr parser::elaborate(environment const & env, expr const & e) {
std::tuple<expr, level_param_names> parser::elaborate(environment const & env, expr const & e) {
parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
return ::lean::elaborate(env, m_ios, e, &pp);
return ::lean::elaborate(env, m_local_level_decls, m_ios, e, &pp);
}
std::pair<expr, expr> parser::elaborate(name const & n, expr const & t, expr const & v) {
std::tuple<expr, expr, level_param_names> parser::elaborate(name const & n, expr const & t, expr const & v) {
parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
return ::lean::elaborate(m_env, m_ios, n, t, v, &pp);
return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, &pp);
}
[[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) {

20
src/frontends/lean/parser.h
View file

@ -56,10 +56,6 @@ class parser {
unsigned m_next_tag_idx;
bool m_found_errors;
pos_info_table_ptr m_pos_table;
// If m_type_use_placeholder is true, then the token Type is parsed as Type.{_}.
// if it is false, then it is parsed as Type.{l} where l is a fresh parameter,
// and is automatically inserted into m_local_level_decls.
bool m_type_use_placeholder;
// By default, when the parser finds a unknown identifier, it signs an error.
// When the following flag is true, it creates a constant.
// This flag is when we are trying to parse mutually recursive declarations.
@ -243,16 +239,6 @@ public:
unsigned get_local_index(name const & n) const;
/** \brief Return the local parameter named \c n */
expr const * get_local(name const & n) const { return m_local_decls.find(n); }
/**
\brief By default, \c mk_Type returns <tt>Type.{_}</tt> where '_' is a new placeholder.
This scope object allows us to temporarily change this behavior.
In any scope containing this object, \c mk_Type returns <tt>Type.{l}</tt>, where
\c l is a fresh universe level parameter.
The new parameter is automatically added to \c m_local_level_decls.
*/
struct param_universe_scope { parser & m_p; bool m_old; param_universe_scope(parser &); ~param_universe_scope(); };
/** \brief Switch back to <tt>Type.{_}</tt>, see \c param_universe_scope */
struct placeholder_universe_scope { parser & m_p; bool m_old; placeholder_universe_scope(parser &); ~placeholder_universe_scope(); };
expr mk_Type();
/**
@ -263,9 +249,9 @@ public:
*/
struct no_undef_id_error_scope { parser & m_p; bool m_old; no_undef_id_error_scope(parser &); ~no_undef_id_error_scope(); };
expr elaborate(expr const & e, bool check_unassigned = true);
expr elaborate(environment const & env, expr const & e);
std::pair<expr, expr> elaborate(name const & n, expr const & t, expr const & v);
std::tuple<expr, level_param_names> elaborate(expr const & e, bool check_unassigned = true);
std::tuple<expr, level_param_names> elaborate(environment const & env, expr const & e);
std::tuple<expr, expr, level_param_names> elaborate(name const & n, expr const & t, expr const & v);
/** parse all commands in the input stream */
bool operator()() { return parse_commands(); }

13
src/util/list_fn.h
View file

@ -130,15 +130,10 @@ list<To> map2(list<From> const & l, F && f) {
if (is_nil(l)) {
return list<To>();
} else {
buffer<typename list<From>::cell*> tmp;
to_buffer(l, tmp);
unsigned i = tmp.size();
list<To> r;
while (i > 0) {
--i;
r = cons(f(tmp[i]->head()), r);
}
return r;
buffer<To> new_vs;
for (auto const & v : l)
new_vs.push_back(f(v));
return to_list(new_vs.begin(), new_vs.end());
}
}

76
tests/lean/run/basic.lean Normal file
View file

@ -0,0 +1,76 @@
variable A.{l1 l2} : Type.{l1} → Type.{l2}
check A
definition tst.{l} (A : Type) (B : Type) (C : Type.{l}) : Type := A → B → C
check tst
variable group.{l} : Type.{l+1}
variable carrier.{l} : group.{l} → Type.{l}
definition to_carrier (g : group) := carrier g
check to_carrier.{1}
section
parameter A : Type
check A
definition B := A → A
end
variable N : Type.{1}
check B N
variable f : B N
check f
variable a : N
check f a
section
parameter T1 : Type
parameter T2 : Type
parameter f : T1 → T2 → T2
definition double (a : T1) (b : T2) := f a (f a b)
end
check double
check double.{1 2}
definition Bool [inline] := Type.{0}
variable eq : Π {A : Type}, A → A → Bool
infix `=`:50 := eq
check eq.{1}
section
universe l
universe u
parameter {T1 : Type.{l}}
parameter {T2 : Type.{l}}
parameter {T3 : Type.{u}}
parameter f : T1 → T2 → T2
definition is_proj2 := ∀ x y, f x y = y
definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z
end
check @is_proj2.{1}
check @is_proj3.{1 2}
namespace foo
section
parameters {T1 T2 : Type}
parameter {T3 : Type}
parameter f : T1 → T2 → T2
definition is_proj2 := ∀ x y, f x y = y
definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z
end
check @foo.is_proj2.{1}
check @foo.is_proj3.{1 2}
end
namespace bla
section
parameter {T1 : Type}
parameter {T2 : Type}
parameter {T3 : Type}
parameter f : T1 → T2 → T2
definition is_proj2 := ∀ x y, f x y = y
definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z
end
check @bla.is_proj2.{1 2}
check @bla.is_proj3.{1 2 3}
end

5
tests/lean/run/group.lean
View file

@ -24,10 +24,11 @@ inductive group : Type :=
definition carrier (g : group) : Type
:= group_rec (λ c s, c) g
-- TODO: improve elaborator and avoid the .{l} in this declaration
definition group_to_struct.{l} [instance] (g : group.{l}) : group_struct (carrier g)
definition group_to_struct [instance] (g : group) : group_struct (carrier g)
:= group_rec (λ (A : Type) (s : group_struct A), s) g
check group_struct
definition mul {A : Type} {s : group_struct A} : A → A → A
:= group_struct_rec (λ mul one inv h1 h2 h3, mul) s

51
tests/lean/run/induniv.lean Normal file
View file

@ -0,0 +1,51 @@
inductive list (A : Type) : Type :=
| nil {} : list A
| cons : A → list A → list A
section
parameter A : Type
inductive list2 : Type :=
| nil2 {} : list2
| cons2 : A → list2 → list2
end
variable num : Type.{1}
namespace Tree
inductive tree (A : Type) : Type :=
| node : A → forest A → tree A
with forest (A : Type) : Type :=
| nil : forest A
| cons : tree A → forest A → forest A
end
inductive group_struct (A : Type) : Type :=
| mk_group_struct : (A → A → A) → A → group_struct A
inductive group : Type :=
| mk_group : Π (A : Type), (A → A → A) → A → group
section
parameter A : Type
parameter B : Type
inductive pair : Type :=
| mk_pair : A → B → pair
end
definition Bool [inline] := Type.{0}
inductive eq {A : Type} (a : A) : A → Bool :=
| refl : eq a a
section
parameter {A : Type}
inductive eq2 (a : A) : A → Bool :=
| refl2 : eq2 a a
end
section
parameter A : Type
parameter B : Type
inductive triple (C : Type) : Type :=
| mk_triple : A → B → C → triple C
end

8
tests/lean/run/uni_issue1.lean Normal file
View file

@ -0,0 +1,8 @@
import standard
inductive nat : Type :=
| zero : nat
| succ : nat → nat
definition is_zero (n : nat)
:= nat_rec true (λ n r, false) n