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

fet(frontends/lean): allow coercions to sort-class in the types of variable and definitions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-06 21:54:16 -07:00
parent 67363c893e
commit e8bd267a00
8 changed files with 40 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -84,7 +84,7 @@ environment check_cmd(parser & p) {
e = p.lambda_abstract(section_ps, e);
level_param_names ls = to_level_param_names(collect_univ_params(e));
level_param_names new_ls;
std::tie(e, new_ls) = p.elaborate(e, false);
std::tie(e, new_ls) = p.elaborate_relaxed(e);
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;

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

@ -137,7 +137,7 @@ environment variable_cmd_core(parser & p, bool is_axiom) {
ls = to_list(ls_buffer.begin(), ls_buffer.end());
}
level_param_names new_ls;
std::tie(type, new_ls) = p.elaborate(type);
std::tie(type, new_ls) = p.elaborate_type(type);
update_section_local_levels(p, new_ls);
return declare_var(p, p.env(), n, append(ls, new_ls), type, is_axiom, bi, pos);
}
@ -280,10 +280,10 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
level_param_names new_ls;
if (is_theorem) {
// TODO(Leo): delay theorems
std::tie(type, value, new_ls) = p.elaborate(n, type, value);
std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value);
env = module::add(env, check(env, mk_theorem(real_n, append(ls, new_ls), type, value)));
} else {
std::tie(type, value, new_ls) = p.elaborate(n, type, value);
std::tie(type, value, new_ls) = p.elaborate_definition(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)
@ -319,7 +319,7 @@ static environment variables_cmd(parser & p) {
p.parse_close_binder_info(bi);
level_param_names ls = to_level_param_names(collect_univ_params(type));
level_param_names new_ls;
std::tie(type, new_ls) = p.elaborate(type);
std::tie(type, new_ls) = p.elaborate_type(type);
update_section_local_levels(p, new_ls);
ls = append(ls, new_ls);
environment env = p.env();

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

@ -981,8 +981,10 @@ public:
return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end()));
}
std::tuple<expr, level_param_names> operator()(expr const & e) {
std::tuple<expr, level_param_names> operator()(expr const & e, bool _ensure_type) {
expr r = visit(e);
if (_ensure_type)
r = ensure_type(r);
auto p = solve().pull();
lean_assert(p);
substitution s = p->first;
@ -999,7 +1001,7 @@ public:
}
std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n) {
expr r_t = visit(t);
expr r_t = ensure_type(visit(t));
expr r_v = visit(v);
expr r_v_type = infer_type(r_v);
environment env = m_env;
@ -1026,8 +1028,8 @@ public:
static name g_tmp_prefix = name::mk_internal_unique_name();
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);
expr const & e, pos_info_provider * pp, bool check_unassigned, bool ensure_type) {
return elaborator(env, lls, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e, ensure_type);
}
std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios,

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

@ -14,7 +14,7 @@ Author: Leonardo de Moura
namespace lean {
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);
pos_info_provider * pp = nullptr, bool check_unassigned = true, bool ensure_type = false);
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);
}

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

@ -197,7 +197,7 @@ struct inductive_cmd_fn {
d_type = update_result_sort(d_type, m_u);
m_infer_result_universe = true;
}
return m_p.elaborate(m_env, d_type);
return m_p.elaborate_at(m_env, d_type);
}
/** \brief Create a local constant based on the given binding */
@ -435,7 +435,7 @@ struct inductive_cmd_fn {
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);
std::tie(ir_type, new_ls) = m_p.elaborate_at(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));

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

@ -467,17 +467,22 @@ expr parser::mk_Type() {
return mk_sort(mk_level_placeholder());
}
std::tuple<expr, level_param_names> parser::elaborate(expr const & e, bool check_unassigned) {
std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e) {
parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
return ::lean::elaborate(m_env, m_local_level_decls, m_ios, e, &pp, check_unassigned);
return ::lean::elaborate(m_env, m_local_level_decls, m_ios, e, &pp, false);
}
std::tuple<expr, level_param_names> parser::elaborate(environment const & env, expr const & e) {
std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e) {
parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
return ::lean::elaborate(m_env, m_local_level_decls, m_ios, e, &pp, true, true);
}
std::tuple<expr, level_param_names> parser::elaborate_at(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_local_level_decls, m_ios, e, &pp);
}
std::tuple<expr, expr, level_param_names> parser::elaborate(name const & n, expr const & t, expr const & v) {
std::tuple<expr, expr, level_param_names> parser::elaborate_definition(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_local_level_decls, m_ios, n, t, v, &pp);
}

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

@ -249,9 +249,14 @@ public:
*/
struct no_undef_id_error_scope { parser & m_p; bool m_old; no_undef_id_error_scope(parser &); ~no_undef_id_error_scope(); };
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);
/** \brief Elaborate \c e, and tolerate metavariables in the result. */
std::tuple<expr, level_param_names> elaborate_relaxed(expr const & e);
/** \brief Elaborate \c e, and ensure it is a type. */
std::tuple<expr, level_param_names> elaborate_type(expr const & e);
/** \brief Elaborate \c e in the given environment. */
std::tuple<expr, level_param_names> elaborate_at(environment const & env, expr const & e);
/** \brief Elaborate the definition n : t := v */
std::tuple<expr, expr, level_param_names> elaborate_definition(name const & n, expr const & t, expr const & v);
/** parse all commands in the input stream */
bool operator()() { return parse_commands(); }

11
tests/lean/run/group2.lean
View file

@ -24,6 +24,8 @@ inductive group : Type :=
definition carrier (g : group) : Type
:= group_rec (λ c s, c) g
coercion carrier
definition group_to_struct [instance] (g : group) : group_struct (carrier g)
:= group_rec (λ (A : Type) (s : group_struct A), s) g
@ -37,12 +39,17 @@ infixl `*`:75 := mul
section
variable G1 : group
variable G2 : group
variables a b c : (carrier G2)
variables d e : (carrier G1)
variables a b c : G2
variables d e : G1
check a * b * b
check d * e
end
variable G : group.{1}
variables a b : G
definition val : G := a*b
check val
variable pos_real : Type.{1}
variable rmul : pos_real → pos_real → pos_real
variable rone : pos_real