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

feat(frontends/lean/structure_cmd): add implicit_infer_kind annotation to structure command

Browse source 
closes #354
This commit is contained in:
Leonardo de Moura 2015-01-21 18:12:29 -08:00
parent a53098385c
commit 880faf89e0
4 changed files with 96 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

86
src/frontends/lean/structure_cmd.cpp
View file

@ -81,34 +81,34 @@ struct structure_cmd_fn {
typedef std::vector<unsigned> field_map;
typedef type_modifiers modifiers;
parser & m_p;
environment m_env;
name_generator m_ngen;
type_checker_ptr m_tc;
name m_namespace;
name m_name;
pos_info m_name_pos;
buffer<name> m_level_names;
modifiers m_modifiers;
buffer<expr> m_params;
expr m_type;
buffer<optional<name>> m_parent_refs;
buffer<expr> m_parents;
buffer<bool> m_private_parents;
name m_mk;
name m_mk_short;
pos_info m_mk_pos;
implicit_infer_kind m_mk_infer;
buffer<expr> m_fields;
std::vector<rename_vector> m_renames;
std::vector<field_map> m_field_maps;
bool m_infer_result_universe;
bool m_using_explicit_levels;
levels m_ctx_levels; // context levels for creating aliases
buffer<expr> m_ctx_locals; // context local constants for creating aliases
parser & m_p;
environment m_env;
name_generator m_ngen;
type_checker_ptr m_tc;
name m_namespace;
name m_name;
pos_info m_name_pos;
buffer<name> m_level_names;
modifiers m_modifiers;
buffer<expr> m_params;
expr m_type;
buffer<optional<name>> m_parent_refs;
buffer<expr> m_parents;
buffer<bool> m_private_parents;
name m_mk;
name m_mk_short;
pos_info m_mk_pos;
implicit_infer_kind m_mk_infer;
buffer<expr> m_fields;
std::vector<rename_vector> m_renames;
std::vector<field_map> m_field_maps;
bool m_infer_result_universe;
bool m_using_explicit_levels;
levels m_ctx_levels; // context levels for creating aliases
buffer<expr> m_ctx_locals; // context local constants for creating aliases
bool m_gen_eta;
bool m_gen_proj_mk;
bool m_gen_eta;
bool m_gen_proj_mk;
structure_cmd_fn(parser & p):m_p(p), m_env(p.env()), m_ngen(p.mk_ngen()), m_namespace(get_namespace(m_env)) {
m_tc = mk_type_checker(m_env, m_p.mk_ngen(), false);
@ -479,15 +479,41 @@ struct structure_cmd_fn {
}
}
void parse_field_block(buffer<expr> & new_fields, binder_info const & bi) {
buffer<pair<pos_info, name>> names;
while (m_p.curr_is_identifier()) {
auto p = m_p.pos();
names.emplace_back(p, m_p.check_atomic_id_next("invalid field, atomic identifier expected"));
}
if (names.empty())
throw parser_error("invalid field, identifier expected", m_p.pos());
m_p.check_token_next(get_colon_tk(), "invalid field, ':' expected");
expr type = m_p.parse_expr();
for (auto p : names) {
expr local = m_p.save_pos(mk_local(p.second, type, bi), p.first);
m_p.add_local(local);
new_fields.push_back(local);
}
}
/** \brief Parse new fields declared in this structure */
void parse_new_fields(buffer<expr> & new_fields) {
parser::local_scope scope(m_p);
add_locals();
m_p.parse_optional_binders(new_fields);
while (!m_p.curr_is_command_like()) {
if (m_p.curr_is_identifier()) {
parse_field_block(new_fields, binder_info());
} else {
binder_info bi = m_p.parse_binder_info();
parse_field_block(new_fields, bi);
m_p.parse_close_binder_info(bi);
}
}
check_new_field_names(new_fields);
}
/** \brief Elaborate new fields, and copy them to m_fields */
void elaborate_new_fields(buffer<expr> & new_fields) {
list<expr> ctx = m_p.locals_to_context();
@ -657,7 +683,7 @@ struct structure_cmd_fn {
}
void declare_projections() {
m_env = mk_projections(m_env, m_name, m_modifiers.is_class());
m_env = mk_projections(m_env, m_name, m_mk_infer, m_modifiers.is_class());
for (expr const & field : m_fields) {
name field_name = m_name + mlocal_name(field);
save_proj_info(field_name);

11
src/library/definitional/projection.cpp
View file

@ -273,7 +273,8 @@ static bool is_prop(expr type) {
return is_sort(type) && is_zero(sort_level(type));
}
environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names, bool inst_implicit) {
environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names,
implicit_infer_kind infer_k, bool inst_implicit) {
// Given an inductive datatype C A (where A represent parameters)
// intro : Pi A (x_1 : B_1[A]) (x_2 : B_2[A, x_1]) ..., C A
//
@ -335,8 +336,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
rec_args.push_back(major_premise);
expr rec_app = mk_app(rec, rec_args);
expr proj_type = Pi(proj_args, result_type);
bool strict = true;
proj_type = infer_implicit(proj_type, nparams, strict);
proj_type = infer_implicit_params(proj_type, nparams, infer_k);
expr proj_val = Fun(proj_args, rec_app);
bool opaque = false;
bool use_conv_opt = false;
@ -364,7 +364,8 @@ static name mk_fresh_name(environment const & env, buffer<name> const & names, n
}
}
environment mk_projections(environment const & env, name const & n, bool inst_implicit) {
environment mk_projections(environment const & env, name const & n,
implicit_infer_kind infer_k, bool inst_implicit) {
auto p = get_nparam_intro_rule(env, n);
unsigned num_params = p.first;
inductive::intro_rule ir = p.second;
@ -377,6 +378,6 @@ environment mk_projections(environment const & env, name const & n, bool inst_im
i++;
type = binding_body(type);
}
return mk_projections(env, n, proj_names, inst_implicit);
return mk_projections(env, n, proj_names, infer_k, inst_implicit);
}
}

15
src/library/definitional/projection.h
View file

@ -8,9 +8,20 @@ Author: Leonardo de Moura
#include "kernel/environment.h"
namespace lean {
/** \brief Create projections operators for the structure named \c n.
The procedure assumes \c n is a structure.
The argument \c infer_k specifies the implicit argument inference strategy used for the
structure parameters.
If \c inst_implicit == true, then the structure argument of the projection is decorated as
"instance implicit"
[s : n]
*/
environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names,
bool inst_implicit = false);
environment mk_projections(environment const & env, name const & n, bool inst_implicit = false);
implicit_infer_kind infer_k = implicit_infer_kind::Implicit, bool inst_implicit = false);
environment mk_projections(environment const & env, name const & n,
implicit_infer_kind infer_k = implicit_infer_kind::Implicit, bool inst_implicit = false);
/** \brief Return true iff the type named \c S can be viewed as
a structure in the given environment.

21
tests/lean/run/struct_infer.lean Normal file
View file

@ -0,0 +1,21 @@
import data.nat.basic
open nat
definition associative {A : Type} (op : A → A → A) := ∀a b c, op (op a b) c = op a (op b c)
structure semigroup [class] (A : Type) :=
mk {} :: (mul: A → A → A) (mul_assoc : associative mul)
definition nat_semigroup [instance] : semigroup nat :=
semigroup.mk nat.mul nat.mul.assoc
example (a b c : nat) : (a * b) * c = a * (b * c) :=
semigroup.mul_assoc a b c
structure semigroup2 (A : Type) :=
mk () :: (mul: A → A → A) (mul_assoc : associative mul)
definition s := semigroup2.mk nat nat.mul nat.mul.assoc
example (a b c : nat) : (a * b) * c = a * (b * c) :=
semigroup2.mul_assoc nat s a b c