1129 lines
49 KiB
C++
1129 lines
49 KiB
C++
/*
|
|
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
*/
|
|
#include <memory>
|
|
#include <utility>
|
|
#include <vector>
|
|
#include <algorithm>
|
|
#include <string>
|
|
#include "util/sstream.h"
|
|
#include "util/fresh_name.h"
|
|
#include "util/sexpr/option_declarations.h"
|
|
#include "kernel/instantiate.h"
|
|
#include "kernel/abstract.h"
|
|
#include "kernel/replace_fn.h"
|
|
#include "kernel/error_msgs.h"
|
|
#include "kernel/inductive/inductive.h"
|
|
#include "library/trace.h"
|
|
#include "library/attribute_manager.h"
|
|
#include "library/scoped_ext.h"
|
|
#include "library/normalize.h"
|
|
#include "library/placeholder.h"
|
|
#include "library/locals.h"
|
|
#include "library/reducible.h"
|
|
#include "library/module.h"
|
|
#include "library/aliases.h"
|
|
#include "library/annotation.h"
|
|
#include "library/explicit.h"
|
|
#include "library/protected.h"
|
|
#include "library/private.h"
|
|
#include "library/class.h"
|
|
#include "library/constants.h"
|
|
#include "library/util.h"
|
|
#include "library/projection.h"
|
|
#include "library/aux_recursors.h"
|
|
#include "library/kernel_serializer.h"
|
|
#include "library/type_context.h"
|
|
#include "library/app_builder.h"
|
|
#include "library/documentation.h"
|
|
#include "library/compiler/vm_compiler.h"
|
|
#include "library/constructions/rec_on.h"
|
|
#include "library/constructions/induction_on.h"
|
|
#include "library/constructions/cases_on.h"
|
|
#include "library/constructions/projection.h"
|
|
#include "library/constructions/no_confusion.h"
|
|
#include "library/inductive_compiler/add_decl.h"
|
|
#include "frontends/lean/elaborator_exception.h"
|
|
#include "frontends/lean/parser.h"
|
|
#include "frontends/lean/util.h"
|
|
#include "frontends/lean/decl_util.h"
|
|
#include "frontends/lean/decl_cmds.h"
|
|
#include "frontends/lean/tokens.h"
|
|
#include "frontends/lean/type_util.h"
|
|
#include "frontends/lean/decl_attributes.h"
|
|
#include "frontends/lean/inductive_cmds.h"
|
|
|
|
|
|
#ifndef LEAN_DEFAULT_STRUCTURE_INTRO
|
|
#define LEAN_DEFAULT_STRUCTURE_INTRO "mk"
|
|
#endif
|
|
|
|
namespace lean {
|
|
/** \brief Return the universe parameters, number of parameters and introduction rule for the given parent structure
|
|
|
|
\pre is_structure_like(env, S) */
|
|
static auto get_structure_info(environment const & env, name const & S)
|
|
-> std::tuple<level_param_names, unsigned, inductive::intro_rule> {
|
|
lean_assert(is_structure_like(env, S));
|
|
inductive::inductive_decl idecl = *inductive::is_inductive_decl(env, S);
|
|
inductive::intro_rule intro = head(idecl.m_intro_rules);
|
|
return std::make_tuple(idecl.m_level_params, idecl.m_num_params, intro);
|
|
}
|
|
|
|
optional<name> has_default_value(environment const & env, name const & full_field_name) {
|
|
name default_name(full_field_name, "_default");
|
|
if (env.find(default_name))
|
|
return optional<name>(default_name);
|
|
else
|
|
return optional<name>();
|
|
}
|
|
|
|
expr mk_field_default_value(environment const & env, name const & full_field_name, std::function<optional<expr>(name const &)> const & get_field_value) {
|
|
optional<name> default_name = has_default_value(env, full_field_name);
|
|
lean_assert(default_name);
|
|
declaration decl = env.get(*default_name);
|
|
expr value = decl.get_value();
|
|
buffer<expr> args;
|
|
while (is_lambda(value)) {
|
|
if (is_explicit(binding_info(value))) {
|
|
name fname = binding_name(value);
|
|
optional<expr> fval = get_field_value(fname);
|
|
if (!fval) {
|
|
throw exception(sstream() << "failed to construct default value for '" << full_field_name << "', "
|
|
<< "it depends on field '" << fname << "', but the value for this field is not available");
|
|
}
|
|
args.push_back(*fval);
|
|
} else {
|
|
args.push_back(mk_expr_placeholder());
|
|
}
|
|
value = binding_body(value);
|
|
}
|
|
return mk_app(mk_explicit(mk_constant(*default_name)), args);
|
|
}
|
|
|
|
struct structure_cmd_fn {
|
|
typedef std::vector<pair<name, name>> rename_vector;
|
|
// field_map[i] contains the position of the \c i-th field of a parent structure into this one.
|
|
typedef std::vector<unsigned> field_map;
|
|
typedef pair<expr, optional<expr>> field_decl;
|
|
|
|
parser & m_p;
|
|
decl_modifiers m_modifiers;
|
|
environment m_env;
|
|
type_context m_ctx;
|
|
name m_namespace;
|
|
name m_name;
|
|
name m_given_name;
|
|
optional<std::string> m_doc_string;
|
|
pos_info m_name_pos;
|
|
buffer<name> m_level_names;
|
|
decl_attributes m_attrs;
|
|
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<field_decl> m_fields;
|
|
std::vector<rename_vector> m_renames;
|
|
std::vector<field_map> m_field_maps;
|
|
bool m_explicit_universe_params;
|
|
bool m_infer_result_universe;
|
|
bool m_inductive_predicate;
|
|
levels m_ctx_levels; // context levels for creating aliases
|
|
buffer<expr> m_ctx_locals; // context local constants for creating aliases
|
|
unsigned m_prio;
|
|
|
|
structure_cmd_fn(parser & p, decl_attributes const & attrs, decl_modifiers const & modifiers):
|
|
m_p(p),
|
|
m_modifiers(modifiers),
|
|
m_env(p.env()),
|
|
m_ctx(p.env()),
|
|
m_namespace(get_namespace(m_env)),
|
|
m_attrs(attrs) {
|
|
m_explicit_universe_params = false;
|
|
m_infer_result_universe = false;
|
|
m_inductive_predicate = false;
|
|
m_prio = get_default_priority(p.get_options());
|
|
m_doc_string = p.get_doc_string();
|
|
}
|
|
|
|
void check_attrs(decl_attributes const & attrs, pos_info const & pos) const {
|
|
if (!attrs.ok_for_inductive_type())
|
|
throw parser_error("only attribute [class] accepted for structures", pos);
|
|
}
|
|
|
|
/** \brief Parse structure name and (optional) universe parameters */
|
|
void parse_decl_name() {
|
|
m_name_pos = m_p.pos();
|
|
m_attrs.parse(m_p);
|
|
check_attrs(m_attrs, m_name_pos);
|
|
buffer<name> ls_buffer;
|
|
if (parse_univ_params(m_p, ls_buffer)) {
|
|
m_explicit_universe_params = true;
|
|
m_level_names.append(ls_buffer);
|
|
} else {
|
|
m_explicit_universe_params = false;
|
|
}
|
|
m_given_name = m_p.check_decl_id_next("invalid 'structure', identifier expected");
|
|
if (m_modifiers.m_is_private) {
|
|
unsigned h = hash(m_name_pos.first, m_name_pos.second);
|
|
auto env_n = add_private_name(m_env, m_given_name, optional<unsigned>(h));
|
|
m_env = env_n.first;
|
|
m_name = env_n.second;
|
|
} else {
|
|
m_name = m_namespace + m_given_name;
|
|
}
|
|
}
|
|
|
|
/** \brief Parse structure parameters */
|
|
void parse_params() {
|
|
if (!m_p.curr_is_token(get_extends_tk()) && !m_p.curr_is_token(get_assign_tk()) &&
|
|
!m_p.curr_is_token(get_colon_tk())) {
|
|
unsigned rbp = 0;
|
|
m_p.parse_binders(m_params, rbp);
|
|
}
|
|
for (expr const & l : m_params)
|
|
m_p.add_local(l);
|
|
}
|
|
|
|
/** \brief Check whether \c parent is really an inductive datatype declaration that can be viewed as a "record".
|
|
That is, it is not part of a mutually recursive declaration, it has only one constructor,
|
|
and it does not have indicies.
|
|
*/
|
|
void check_parent(expr const & parent, pos_info const & pos) {
|
|
expr const & fn = get_app_fn(parent);
|
|
if (!is_constant(fn))
|
|
throw parser_error("invalid 'structure', expression must be a 'parent' structure", pos);
|
|
name const & S = const_name(fn);
|
|
if (!is_structure_like(m_env, S))
|
|
throw parser_error(sstream() << "invalid 'structure' extends, '" << S << "' is not a structure", pos);
|
|
}
|
|
|
|
/** \brief Return the universe parameters, number of parameters and introduction rule for the given parent structure */
|
|
std::tuple<level_param_names, unsigned, inductive::intro_rule> get_parent_info(name const & parent) {
|
|
return get_structure_info(m_env, parent);
|
|
}
|
|
|
|
/** \brief Sign an error if the constructor \c intro_type does not have a field named \c from_id */
|
|
void check_from_rename(name const & parent_name, expr intro_type, name const & from_id, pos_info const & from_pos) {
|
|
while (is_pi(intro_type)) {
|
|
if (binding_name(intro_type) == from_id)
|
|
return;
|
|
intro_type = binding_body(intro_type);
|
|
}
|
|
throw parser_error(sstream() << "invalid 'structure' renaming, parent structure '" << parent_name << "' "
|
|
<< "does not contain field '" << from_id << "'", from_pos);
|
|
}
|
|
|
|
/** \brief Parse optional extends clause */
|
|
void parse_extends() {
|
|
if (m_p.curr_is_token(get_extends_tk())) {
|
|
m_p.next();
|
|
while (true) {
|
|
auto pos = m_p.pos();
|
|
bool is_private_parent = false;
|
|
if (m_p.curr_is_token(get_private_tk())) {
|
|
m_p.next();
|
|
is_private_parent = true;
|
|
}
|
|
pair<optional<name>, expr> qparent = m_p.parse_qualified_expr();
|
|
m_parent_refs.push_back(qparent.first);
|
|
expr const & parent = qparent.second;
|
|
m_parents.push_back(parent);
|
|
m_private_parents.push_back(is_private_parent);
|
|
check_parent(parent, pos);
|
|
name const & parent_name = const_name(get_app_fn(parent));
|
|
auto parent_info = get_parent_info(parent_name);
|
|
unsigned nparams = std::get<1>(parent_info);
|
|
inductive::intro_rule intro = std::get<2>(parent_info);
|
|
expr intro_type = inductive::intro_rule_type(intro);
|
|
for (unsigned i = 0; i < nparams; i++) {
|
|
if (!is_pi(intro_type))
|
|
throw parser_error("invalid 'structure' extends, parent structure seems to be ill-formed", pos);
|
|
intro_type = binding_body(intro_type);
|
|
}
|
|
m_renames.push_back(rename_vector());
|
|
if (m_p.curr_is_token(get_renaming_tk())) {
|
|
m_p.next();
|
|
rename_vector & v = m_renames.back();
|
|
while (m_p.curr_is_identifier()) {
|
|
auto from_pos = m_p.pos();
|
|
name from_id = m_p.get_name_val();
|
|
if (std::find_if(v.begin(), v.end(),
|
|
[&](pair<name, name> const & p) { return p.first == from_id; }) != v.end())
|
|
throw parser_error(sstream() << "invalid 'structure' renaming, a rename from '" <<
|
|
from_id << "' has already been defined", from_pos);
|
|
check_from_rename(parent_name, intro_type, from_id, from_pos);
|
|
m_p.next();
|
|
m_p.check_token_next(get_arrow_tk(), "invalid 'structure' renaming, '->' expected");
|
|
name to_id = m_p.check_id_next("invalid 'structure' renaming, identifier expected");
|
|
if (from_id == to_id)
|
|
throw parser_error(sstream() << "invalid 'structure' renaming, redundant rename", from_pos);
|
|
v.emplace_back(from_id, to_id);
|
|
}
|
|
}
|
|
if (!m_p.curr_is_token(get_comma_tk()))
|
|
break;
|
|
m_p.next();
|
|
}
|
|
}
|
|
}
|
|
|
|
/** \brief Parse resultant universe */
|
|
void parse_result_type() {
|
|
auto pos = m_p.pos();
|
|
if (m_p.curr_is_token(get_colon_tk())) {
|
|
m_p.next();
|
|
m_type = m_p.parse_expr();
|
|
while (is_annotation(m_type))
|
|
m_type = get_annotation_arg(m_type);
|
|
if (!is_sort(m_type))
|
|
throw parser_error("invalid 'structure', 'Type' expected", pos);
|
|
m_inductive_predicate = is_zero(sort_level(m_type));
|
|
if (m_inductive_predicate) {
|
|
m_infer_result_universe = false;
|
|
} else if (is_one_placeholder(sort_level(m_type))) {
|
|
m_infer_result_universe = false;
|
|
m_type = m_p.save_pos(mk_sort(mk_level_one()), pos);
|
|
} else {
|
|
m_infer_result_universe = is_placeholder(sort_level(m_type));
|
|
if (!m_infer_result_universe) {
|
|
if (!is_zero(sort_level(m_type)) && !is_not_zero(sort_level(m_type)))
|
|
throw parser_error("invalid universe polymorphic structure declaration, "
|
|
"the resultant universe is not Prop (i.e., 0), "
|
|
"but it may be Prop for some parameter values "
|
|
"(solution: use 'l+1' or 'max 1 l')", m_p.pos());
|
|
}
|
|
}
|
|
} else {
|
|
m_infer_result_universe = true;
|
|
m_type = m_p.save_pos(mk_sort(mk_level_placeholder()), pos);
|
|
}
|
|
}
|
|
|
|
/** \brief Parse parameters, extends clauses and resultant type */
|
|
void parse_header() {
|
|
parser::local_scope scope(m_p);
|
|
parse_decl_name();
|
|
parse_params();
|
|
parse_extends();
|
|
parse_result_type();
|
|
}
|
|
|
|
/** \brief Update the local constants in \c locals using the content of the Pi expression \c new_tmp.
|
|
This method assumes that new_tmp contains at least locals.size() nested Pi's.
|
|
*/
|
|
expr update_locals(expr new_tmp, buffer<expr> & locals) {
|
|
for (unsigned i = 0; i < locals.size(); i++) {
|
|
expr new_local = mk_local(mlocal_name(locals[i]), binding_name(new_tmp), binding_domain(new_tmp),
|
|
binding_info(new_tmp));
|
|
locals[i] = new_local;
|
|
new_tmp = instantiate(binding_body(new_tmp), new_local);
|
|
}
|
|
return new_tmp;
|
|
}
|
|
|
|
expr update_fields(expr new_tmp, buffer<field_decl> & decls) {
|
|
for (unsigned i = 0; i < decls.size(); i++) {
|
|
if (decls[i].second) {
|
|
lean_assert(is_let(new_tmp));
|
|
expr new_local = mk_local(mlocal_name(decls[i].first), let_name(new_tmp), let_type(new_tmp), binder_info());
|
|
decls[i].first = new_local;
|
|
decls[i].second = let_value(new_tmp);
|
|
new_tmp = instantiate(let_body(new_tmp), new_local);
|
|
} else {
|
|
lean_assert(is_pi(new_tmp));
|
|
expr new_local = mk_local(mlocal_name(decls[i].first), binding_name(new_tmp), binding_domain(new_tmp),
|
|
binding_info(new_tmp));
|
|
decls[i].first = new_local;
|
|
new_tmp = instantiate(binding_body(new_tmp), new_local);
|
|
}
|
|
}
|
|
return new_tmp;
|
|
}
|
|
|
|
expr update_parents(expr new_tmp, bool inst) {
|
|
for (unsigned i = 0; i < m_parents.size(); i++) {
|
|
m_parents[i] = copy_tag(m_parents[i], expr(binding_domain(new_tmp)));
|
|
new_tmp = binding_body(new_tmp);
|
|
if (inst)
|
|
new_tmp = instantiate(new_tmp, mk_parent_expr(i));
|
|
}
|
|
return new_tmp;
|
|
}
|
|
|
|
/** \brief elaborate parameters and "parent" types */
|
|
void elaborate_header() {
|
|
buffer<expr> include_vars;
|
|
m_p.get_include_variables(include_vars);
|
|
buffer<expr> tmp_locals;
|
|
tmp_locals.append(m_params);
|
|
for (expr const & parent : m_parents)
|
|
tmp_locals.push_back(mk_local(mk_fresh_name(), parent));
|
|
|
|
collected_locals dep_set;
|
|
for (expr const & v : include_vars) {
|
|
::lean::collect_locals(mlocal_type(v), dep_set);
|
|
dep_set.insert(v);
|
|
}
|
|
for (expr const & p : m_params)
|
|
::lean::collect_locals(mlocal_type(p), dep_set);
|
|
collect_annonymous_inst_implicit(m_p, dep_set);
|
|
/* Copy the locals from dep_set that are NOT in m_params to dep_set_minus_params */
|
|
buffer<expr> dep_set_minus_params;
|
|
for (auto d : dep_set.get_collected()) {
|
|
if (std::all_of(m_params.begin(), m_params.end(), [&](expr const & p) { return mlocal_name(d) != mlocal_name(p); }))
|
|
dep_set_minus_params.push_back(d);
|
|
}
|
|
/* Sort dep_set_minus_params and store result in ctx */
|
|
buffer<expr> ctx;
|
|
sort_locals(dep_set_minus_params, m_p, ctx);
|
|
|
|
expr tmp = Pi_as_is(ctx, Pi(tmp_locals, m_type, m_p), m_p);
|
|
level_param_names new_ls;
|
|
expr new_tmp;
|
|
std::tie(new_tmp, new_ls) = m_p.elaborate_type(m_name, list<expr>(), tmp);
|
|
levels new_meta_ls = map2<level>(new_ls, [&](name const &) { return m_ctx.mk_univ_metavar_decl(); });
|
|
new_tmp = instantiate_univ_params(new_tmp, new_ls, new_meta_ls);
|
|
new_tmp = update_locals(new_tmp, ctx);
|
|
new_tmp = update_locals(new_tmp, m_params);
|
|
buffer<expr> explicit_params;
|
|
explicit_params.append(m_params);
|
|
m_params.clear();
|
|
m_params.append(ctx);
|
|
m_params.append(explicit_params);
|
|
new_tmp = update_parents(new_tmp, false);
|
|
m_type = new_tmp;
|
|
}
|
|
|
|
void throw_ill_formed_parent(name const & parent_name) {
|
|
throw exception(sstream() << "invalid 'structure' header, parent structure '" << parent_name << "' is ill-formed");
|
|
}
|
|
|
|
/** \brief Check if \c fname has been renamed, and return new name */
|
|
name rename(rename_vector const & v, name const & fname) {
|
|
for (auto const & p : v) {
|
|
if (p.first == fname)
|
|
return p.second;
|
|
}
|
|
return fname;
|
|
}
|
|
|
|
/** \brief If \c fname matches the name of an existing field, then check if
|
|
the types are definitionally equal (store any generated unification constraints in cseq),
|
|
and return the index of the existing field. */
|
|
optional<unsigned> merge(expr const & parent, name const & fname, expr const & ftype, optional<expr> const & fdefault) {
|
|
for (unsigned i = 0; i < m_fields.size(); i++) {
|
|
if (local_pp_name(m_fields[i].first) == fname) {
|
|
if (m_ctx.is_def_eq(mlocal_type(m_fields[i].first), ftype)) {
|
|
if (!m_fields[i].second && fdefault) {
|
|
m_fields[i].second = fdefault;
|
|
} else if (m_fields[i].second && fdefault && !m_ctx.is_def_eq(*m_fields[i].second, *fdefault)) {
|
|
expr prev_default = *m_fields[i].second;
|
|
throw generic_exception(parent, [=](formatter const & fmt) {
|
|
format r = format("invalid 'structure' header, field '");
|
|
r += format(fname);
|
|
r += format("' from '");
|
|
r += format(const_name(get_app_fn(parent)));
|
|
r += format("' has already been declared with a different default value");
|
|
r += pp_indent_expr(fmt, prev_default);
|
|
r += compose(line(), format("and"));
|
|
r += pp_indent_expr(fmt, *fdefault);
|
|
return r;
|
|
});
|
|
}
|
|
return optional<unsigned>(i);
|
|
} else {
|
|
expr prev_ftype = mlocal_type(m_fields[i].first);
|
|
throw generic_exception(parent, [=](formatter const & fmt) {
|
|
format r = format("invalid 'structure' header, field '");
|
|
r += format(fname);
|
|
r += format("' from '");
|
|
r += format(const_name(get_app_fn(parent)));
|
|
r += format("' has already been declared with a different type");
|
|
r += pp_indent_expr(fmt, prev_ftype);
|
|
r += compose(line(), format("and"));
|
|
r += pp_indent_expr(fmt, ftype);
|
|
return r;
|
|
});
|
|
}
|
|
}
|
|
}
|
|
return optional<unsigned>();
|
|
}
|
|
|
|
expr mk_field_default_value(name const & full_field_name) {
|
|
return ::lean::mk_field_default_value(m_env, full_field_name, [&](name const & fname) {
|
|
for (field_decl const & d : m_fields) {
|
|
if (local_pp_name(d.first) == fname)
|
|
return some_expr(d.first);
|
|
}
|
|
return none_expr();
|
|
});
|
|
}
|
|
|
|
/** \brief Process extends clauses.
|
|
This method also populates the vector m_field_maps and m_fields. */
|
|
void process_extends() {
|
|
lean_assert(m_fields.empty());
|
|
lean_assert(m_field_maps.empty());
|
|
for (unsigned i = 0; i < m_parents.size(); i++) {
|
|
expr const & parent = m_parents[i];
|
|
rename_vector const & renames = m_renames[i];
|
|
m_field_maps.push_back(field_map());
|
|
field_map & fmap = m_field_maps.back();
|
|
buffer<expr> args;
|
|
expr const & parent_fn = get_app_args(parent, args);
|
|
level_param_names lparams; unsigned nparams; inductive::intro_rule intro;
|
|
name const & parent_name = const_name(parent_fn);
|
|
std::tie(lparams, nparams, intro) = get_parent_info(parent_name);
|
|
expr intro_type = inductive::intro_rule_type(intro);
|
|
intro_type = instantiate_univ_params(intro_type, lparams, const_levels(parent_fn));
|
|
if (nparams != args.size()) {
|
|
throw elaborator_exception(parent,
|
|
sstream() << "invalid 'structure' header, number of argument "
|
|
"mismatch for parent structure '" << parent_name << "'");
|
|
}
|
|
for (expr const & arg : args) {
|
|
if (!is_pi(intro_type))
|
|
throw_ill_formed_parent(parent_name);
|
|
intro_type = instantiate(binding_body(intro_type), arg);
|
|
}
|
|
while (is_pi(intro_type)) {
|
|
name fname = binding_name(intro_type);
|
|
fname = rename(renames, fname);
|
|
expr const & ftype = binding_domain(intro_type);
|
|
optional<expr> fdefault;
|
|
name full_fname = parent_name + fname;
|
|
if (optional<name> fdefault_name = has_default_value(m_env, full_fname)) {
|
|
fdefault = mk_field_default_value(full_fname);
|
|
}
|
|
expr field;
|
|
if (auto fidx = merge(parent, fname, ftype, fdefault)) {
|
|
fmap.push_back(*fidx);
|
|
field = m_fields[*fidx].first;
|
|
if (local_info(field) != binding_info(intro_type)) {
|
|
throw elaborator_exception(parent,
|
|
sstream() << "invalid 'structure' header, field '" << fname <<
|
|
"' has already been declared with a different binder annotation");
|
|
}
|
|
} else {
|
|
field = mk_local(fname, ftype, binding_info(intro_type));
|
|
fmap.push_back(m_fields.size());
|
|
m_fields.push_back(field_decl(field, fdefault));
|
|
}
|
|
intro_type = instantiate(binding_body(intro_type), field);
|
|
}
|
|
}
|
|
lean_assert(m_parents.size() == m_field_maps.size());
|
|
}
|
|
|
|
void instantiate_mvars() {
|
|
for (expr & parent : m_parents)
|
|
parent = m_ctx.instantiate_mvars(parent);
|
|
for (expr & param : m_params)
|
|
param = m_ctx.instantiate_mvars(param);
|
|
for (field_decl & decl : m_fields) {
|
|
decl.first = m_ctx.instantiate_mvars(decl.first);
|
|
if (decl.second)
|
|
decl.second = m_ctx.instantiate_mvars(*decl.second);
|
|
}
|
|
}
|
|
|
|
/** \brief Parse header, elaborate it, and process parents (aka extends clauses) */
|
|
void process_header() {
|
|
parse_header();
|
|
elaborate_header();
|
|
process_extends();
|
|
instantiate_mvars();
|
|
}
|
|
|
|
/** \brief Create expression of type \c m_parents[i] from corresponding fields */
|
|
expr mk_parent_expr(unsigned i) {
|
|
expr const & parent = m_parents[i];
|
|
field_map const & fmap = m_field_maps[i];
|
|
buffer<expr> parent_params;
|
|
expr const & parent_fn = get_app_args(parent, parent_params);
|
|
levels const & parent_ls = const_levels(parent_fn);
|
|
name const & parent_name = const_name(parent_fn);
|
|
auto parent_info = get_parent_info(parent_name);
|
|
name const & parent_intro_name = inductive::intro_rule_name(std::get<2>(parent_info));
|
|
expr parent_intro = mk_app(mk_constant(parent_intro_name, parent_ls), parent_params);
|
|
for (unsigned idx : fmap) {
|
|
expr const & field = m_fields[idx].first;
|
|
parent_intro = mk_app(parent_intro, field);
|
|
}
|
|
return parent_intro;
|
|
}
|
|
|
|
/** \brief Add params, fields and references to parent structures into parser local scope */
|
|
void add_locals() {
|
|
if (m_explicit_universe_params) {
|
|
for (name const & l : m_level_names)
|
|
m_p.add_local_level(l, mk_param_univ(l));
|
|
}
|
|
for (expr const & param : m_params)
|
|
m_p.add_local(param);
|
|
for (field_decl const & decl : m_fields)
|
|
m_p.add_local(decl.first);
|
|
for (unsigned i = 0; i < m_parents.size(); i++) {
|
|
if (auto n = m_parent_refs[i])
|
|
m_p.add_local_expr(*n, mk_as_is(mk_parent_expr(i)));
|
|
}
|
|
}
|
|
|
|
/** \brief Check if new field names collide with fields inherited from parent datastructures */
|
|
void check_new_field_names(buffer<field_decl> const & new_fields) {
|
|
for (field_decl const & new_field : new_fields) {
|
|
/* TODO(Leo): allow new field to set default value for parent field */
|
|
if (std::find_if(m_fields.begin(), m_fields.end(),
|
|
[&](field_decl const & inherited_field) {
|
|
return local_pp_name(inherited_field.first) == local_pp_name(new_field.first);
|
|
}) != m_fields.end()) {
|
|
throw elaborator_exception(new_field.first,
|
|
sstream() << "field '" << local_pp_name(new_field.first) <<
|
|
"' has been declared in parent structure");
|
|
}
|
|
}
|
|
}
|
|
|
|
void parse_field_block(buffer<field_decl> & new_fields, binder_info const & bi) {
|
|
buffer<pair<pos_info, name>> names;
|
|
auto start_pos = m_p.pos();
|
|
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());
|
|
|
|
expr type;
|
|
optional<expr> default_value;
|
|
if (m_p.curr_is_token(get_assign_tk())) {
|
|
type = m_p.save_pos(mk_expr_placeholder(), m_p.pos());
|
|
m_p.next();
|
|
default_value = m_p.parse_expr();
|
|
} else {
|
|
m_p.check_token_next(get_colon_tk(), "invalid field, ':' expected");
|
|
type = m_p.parse_expr();
|
|
if (m_p.curr_is_token(get_assign_tk())) {
|
|
m_p.next();
|
|
default_value = m_p.parse_expr();
|
|
}
|
|
}
|
|
if (default_value && !is_explicit(bi)) {
|
|
throw parser_error("invalid field, it is not explicit, but it has a default value", start_pos);
|
|
}
|
|
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(field_decl(local, default_value));
|
|
}
|
|
}
|
|
|
|
/** \brief Parse new fields declared in this structure */
|
|
void parse_new_fields(buffer<field_decl> & new_fields) {
|
|
parser::local_scope scope(m_p);
|
|
add_locals();
|
|
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);
|
|
}
|
|
|
|
expr mk_field_binder(buffer<field_decl> const & decls, expr const & type, bool as_is = false) {
|
|
expr r = type;
|
|
unsigned i = decls.size();
|
|
while (i > 0) {
|
|
--i;
|
|
field_decl const & decl = decls[i];
|
|
if (decl.second) {
|
|
expr type = mlocal_type(decl.first);
|
|
expr value = *decl.second;
|
|
if (as_is) {
|
|
type = mk_as_is(type);
|
|
}
|
|
r = mk_let(local_pp_name(decl.first), type, value, r);
|
|
} else if (as_is) {
|
|
r = Pi_as_is(decl.first, r);
|
|
} else {
|
|
r = Pi(decl.first, r);
|
|
}
|
|
}
|
|
return r;
|
|
}
|
|
|
|
expr mk_field_binder_as_is(buffer<field_decl> const & decls, expr const & type) {
|
|
return mk_field_binder(decls, type, true);
|
|
}
|
|
|
|
/** \brief Elaborate new fields, and copy them to m_fields */
|
|
void elaborate_new_fields(buffer<field_decl> & new_fields) {
|
|
expr tmp = mk_field_binder_as_is(m_fields, mk_field_binder(new_fields, mk_Prop()));
|
|
unsigned j = m_parents.size();
|
|
while (j > 0) {
|
|
--j;
|
|
tmp = mk_arrow(mk_as_is(m_parents[j]), tmp);
|
|
}
|
|
tmp = Pi_as_is(m_params, tmp, m_p);
|
|
level_param_names new_ls;
|
|
expr new_tmp;
|
|
metavar_context mctx = m_ctx.mctx();
|
|
std::tie(new_tmp, new_ls) = m_p.elaborate_type(m_name, mctx, tmp);
|
|
m_ctx.set_mctx(mctx);
|
|
for (auto new_l : new_ls)
|
|
m_level_names.push_back(new_l);
|
|
new_tmp = update_locals(new_tmp, m_params);
|
|
new_tmp = update_parents(new_tmp, true);
|
|
new_tmp = update_fields(new_tmp, m_fields);
|
|
new_tmp = update_fields(new_tmp, new_fields);
|
|
lean_assert(new_tmp == mk_Prop());
|
|
m_fields.append(new_fields);
|
|
}
|
|
|
|
/** \brief Parse new fields declared by this structure, and elaborate them. */
|
|
void process_new_fields() {
|
|
buffer<field_decl> new_fields;
|
|
parse_new_fields(new_fields);
|
|
elaborate_new_fields(new_fields);
|
|
}
|
|
|
|
void process_empty_new_fields() {
|
|
buffer<field_decl> new_fields;
|
|
elaborate_new_fields(new_fields);
|
|
}
|
|
|
|
/** \brief Traverse fields and collect the universes they reside in \c r_lvls.
|
|
This information is used to compute the resultant universe level for the inductive datatype declaration. */
|
|
void accumulate_levels(buffer<level> & r_lvls) {
|
|
for (field_decl const & decl : m_fields) {
|
|
level l = get_level(m_ctx, mlocal_type(decl.first));
|
|
if (std::find(r_lvls.begin(), r_lvls.end(), l) == r_lvls.end()) {
|
|
r_lvls.push_back(l);
|
|
}
|
|
}
|
|
}
|
|
|
|
/** \brief Compute resultant universe (if it was not provided explicitly) based on the universes
|
|
where the fields "reside" */
|
|
void infer_resultant_universe() {
|
|
if (m_infer_result_universe) {
|
|
buffer<level> r_lvls;
|
|
accumulate_levels(r_lvls);
|
|
level r_lvl = mk_result_level(r_lvls);
|
|
m_type = mk_sort(r_lvl);
|
|
}
|
|
}
|
|
|
|
/** \brief Display m_fields (for debugging purposes) */
|
|
void display_fields(std::ostream & out) {
|
|
for (field_decl const & decl : m_fields) {
|
|
out << ">> " << mlocal_name(decl.first) << " : " << mlocal_type(decl.first);
|
|
if (decl.second)
|
|
out << " := " << *decl.second;
|
|
out << "\n";
|
|
}
|
|
}
|
|
|
|
/** \brief Collect context local constants used in the declaration. */
|
|
void collect_ctx_locals(buffer<expr> & locals) {
|
|
if (!m_p.has_locals())
|
|
return;
|
|
expr dummy = mk_Prop();
|
|
expr tmp = Pi(m_params, mk_field_binder(m_fields, dummy));
|
|
collected_locals local_set;
|
|
::lean::collect_locals(tmp, local_set);
|
|
collect_annonymous_inst_implicit(m_p, local_set);
|
|
sort_locals(local_set.get_collected(), m_p, locals);
|
|
}
|
|
|
|
/** \brief Add context locals as extra parameters */
|
|
void add_ctx_locals(buffer<expr> const & ctx_locals) {
|
|
buffer<expr> params;
|
|
params.append(m_params);
|
|
m_params.clear();
|
|
m_params.append(ctx_locals);
|
|
m_params.append(params);
|
|
}
|
|
|
|
/** \brief Initialize m_ctx_locals field */
|
|
void set_ctx_locals() {
|
|
buffer<expr> new_ctx_locals;
|
|
collect_ctx_locals(new_ctx_locals);
|
|
add_ctx_locals(new_ctx_locals);
|
|
for (expr const & p : m_params) {
|
|
if (m_p.is_local_decl(p) && !m_p.is_local_variable(p))
|
|
m_ctx_locals.push_back(p);
|
|
}
|
|
}
|
|
|
|
/** \brief Include in m_level_names any local level referenced m_type and m_fields */
|
|
void include_ctx_levels() {
|
|
name_set all_lvl_params;
|
|
all_lvl_params = collect_univ_params(m_type);
|
|
for (expr const & p : m_params)
|
|
all_lvl_params = collect_univ_params(mlocal_type(p), all_lvl_params);
|
|
for (field_decl const & f : m_fields) {
|
|
all_lvl_params = collect_univ_params(mlocal_type(f.first), all_lvl_params);
|
|
if (f.second)
|
|
all_lvl_params = collect_univ_params(*f.second, all_lvl_params);
|
|
}
|
|
buffer<name> section_lvls;
|
|
all_lvl_params.for_each([&](name const & l) {
|
|
if (std::find(m_level_names.begin(), m_level_names.end(), l) == m_level_names.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_level_names);
|
|
m_level_names.clear();
|
|
m_level_names.append(new_levels);
|
|
}
|
|
|
|
expr mk_structure_type() {
|
|
return Pi(m_params, m_type, m_p);
|
|
}
|
|
|
|
expr mk_intro_type() {
|
|
levels ls = param_names_to_levels(to_list(m_level_names.begin(), m_level_names.end()));
|
|
expr r = mk_app(mk_constant(m_name, ls), m_params);
|
|
buffer<expr> field_wo_defaults;
|
|
for (field_decl const & decl : m_fields) field_wo_defaults.push_back(decl.first);
|
|
r = Pi(m_params, Pi(field_wo_defaults, r, m_p), m_p);
|
|
return infer_implicit_params(r, m_params.size(), m_mk_infer);
|
|
}
|
|
|
|
void add_alias(name const & given, name const & n) {
|
|
m_env = ::lean::add_alias(m_p, m_env, given, n, m_ctx_levels, m_ctx_locals);
|
|
}
|
|
|
|
void add_alias(name const & n, bool composite = true) {
|
|
m_env = ::lean::add_alias(m_p, m_env, composite, n, m_ctx_levels, m_ctx_locals);
|
|
}
|
|
|
|
void add_rec_alias(name const & n) {
|
|
levels rec_ctx_levels;
|
|
if (!is_nil(m_ctx_levels))
|
|
rec_ctx_levels = levels(mk_level_placeholder(), m_ctx_levels);
|
|
if (m_modifiers.m_is_private) {
|
|
name given_rec_name = name(m_given_name, n.get_string());
|
|
m_env = ::lean::add_alias(m_p, m_env, given_rec_name, n, rec_ctx_levels, m_ctx_locals);
|
|
} else {
|
|
bool composite = true;
|
|
m_env = ::lean::add_alias(m_p, m_env, composite, n, rec_ctx_levels, m_ctx_locals);
|
|
}
|
|
}
|
|
|
|
void declare_inductive_type() {
|
|
expr structure_type = mk_structure_type();
|
|
expr intro_type = mk_intro_type();
|
|
|
|
level_param_names lnames = to_list(m_level_names.begin(), m_level_names.end());
|
|
inductive::intro_rule intro = inductive::mk_intro_rule(m_mk, intro_type);
|
|
inductive::inductive_decl decl(m_name, lnames, m_params.size(), structure_type, to_list(intro));
|
|
bool is_trusted = !m_modifiers.m_is_meta;
|
|
m_env = module::add_inductive(m_env, decl, is_trusted);
|
|
name rec_name = inductive::get_elim_name(m_name);
|
|
m_env = add_namespace(m_env, m_name);
|
|
m_env = add_protected(m_env, rec_name);
|
|
add_alias(m_given_name, m_name);
|
|
add_alias(m_mk);
|
|
add_rec_alias(rec_name);
|
|
m_env = m_attrs.apply(m_env, m_p.ios(), m_name);
|
|
m_env = add_structure_declaration_aux(m_env, m_p.get_options(), m_level_names, m_params,
|
|
mk_local(m_name, mk_structure_type()),
|
|
mk_local(m_mk, mk_intro_type()));
|
|
}
|
|
|
|
void declare_projections() {
|
|
m_env = mk_projections(m_env, m_name, m_mk_infer, m_attrs.has_class());
|
|
for (field_decl const & field : m_fields) {
|
|
name field_name = m_name + mlocal_name(field.first);
|
|
add_alias(field_name);
|
|
}
|
|
}
|
|
|
|
bool is_field(expr const & local) {
|
|
for (field_decl const & field : m_fields) {
|
|
if (mlocal_name(field.first) == mlocal_name(local))
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
void declare_defaults() {
|
|
for (field_decl const & field : m_fields) {
|
|
if (field.second) {
|
|
collected_locals used_locals;
|
|
collect_locals(mlocal_type(field.first), used_locals);
|
|
collect_locals(*field.second, used_locals);
|
|
buffer<expr> args;
|
|
/* Copy params first */
|
|
for (expr const & local : used_locals.get_collected()) {
|
|
if (!is_field(local)) {
|
|
if (is_explicit(local_info(local)))
|
|
args.push_back(update_local(local, mk_implicit_binder_info()));
|
|
else
|
|
args.push_back(local);
|
|
}
|
|
}
|
|
/* Copy fields it depends on */
|
|
for (expr const & local : used_locals.get_collected()) {
|
|
if (is_field(local))
|
|
args.push_back(local);
|
|
}
|
|
name decl_name = name(m_name + local_pp_name(field.first), "_default");
|
|
expr decl_type = Pi(args, mlocal_type(field.first));
|
|
expr decl_value = Fun(args, mk_explicit(*field.second));
|
|
name_set used_univs;
|
|
used_univs = collect_univ_params(decl_value, used_univs);
|
|
used_univs = collect_univ_params(decl_type, used_univs);
|
|
level_param_names decl_lvls = to_level_param_names(used_univs);
|
|
declaration new_decl = mk_definition_inferring_trusted(m_env, decl_name, decl_lvls,
|
|
decl_type, decl_value, reducibility_hints::mk_abbreviation());
|
|
m_env = module::add(m_env, check(m_env, new_decl));
|
|
m_env = set_reducible(m_env, decl_name, reducible_status::Reducible, true);
|
|
}
|
|
}
|
|
}
|
|
|
|
void add_rec_on_alias(name const & n) {
|
|
name rec_on_name(m_name, "rec_on");
|
|
declaration rec_on_decl = m_env.get(rec_on_name);
|
|
declaration new_decl = mk_definition_inferring_trusted(m_env, n, rec_on_decl.get_univ_params(),
|
|
rec_on_decl.get_type(), rec_on_decl.get_value(),
|
|
reducibility_hints::mk_abbreviation());
|
|
m_env = module::add(m_env, check(m_env, new_decl));
|
|
m_env = set_reducible(m_env, n, reducible_status::Reducible, true);
|
|
add_alias(n);
|
|
}
|
|
|
|
void declare_auxiliary() {
|
|
m_env = mk_rec_on(m_env, m_name);
|
|
name rec_on_name(m_name, "rec_on");
|
|
add_rec_alias(rec_on_name);
|
|
m_env = add_aux_recursor(m_env, rec_on_name);
|
|
m_env = mk_induction_on(m_env, m_name);
|
|
name induction_on_name(m_name, "induction_on");
|
|
add_alias(induction_on_name);
|
|
add_rec_on_alias(name(m_name, "destruct"));
|
|
name cases_on_name(m_name, "cases_on");
|
|
add_rec_on_alias(cases_on_name);
|
|
m_env = add_aux_recursor(m_env, cases_on_name);
|
|
}
|
|
|
|
// Return the parent names without namespace prefix
|
|
void get_truncated_parent_names(buffer<name> & parent_names) {
|
|
for (expr const & parent : m_parents) {
|
|
name n = const_name(get_app_fn(parent));
|
|
if (!n.is_atomic() && n.is_string())
|
|
n = name(n.get_string());
|
|
parent_names.push_back(n);
|
|
}
|
|
}
|
|
|
|
void mk_coercion_names(buffer<name> & coercion_names) {
|
|
buffer<name> parent_names;
|
|
get_truncated_parent_names(parent_names);
|
|
name_set found;
|
|
name_map<unsigned> non_unique;
|
|
for (name const & n : parent_names) {
|
|
if (found.contains(n))
|
|
non_unique.insert(n, 1);
|
|
found.insert(n);
|
|
}
|
|
for (name & n : parent_names) {
|
|
if (auto it = non_unique.find(n)) {
|
|
unsigned idx = *it;
|
|
non_unique.insert(n, idx+1);
|
|
n = n.append_after(idx);
|
|
}
|
|
name coercion_name = m_name + n.append_before("to_");
|
|
coercion_names.push_back(coercion_name);
|
|
}
|
|
}
|
|
|
|
void declare_coercions() {
|
|
lean_assert(m_parents.size() == m_field_maps.size());
|
|
buffer<name> coercion_names;
|
|
mk_coercion_names(coercion_names);
|
|
level_param_names lnames = to_list(m_level_names.begin(), m_level_names.end());
|
|
levels st_ls = param_names_to_levels(lnames);
|
|
for (unsigned i = 0; i < m_parents.size(); i++) {
|
|
expr const & parent = m_parents[i];
|
|
field_map const & fmap = m_field_maps[i];
|
|
buffer<expr> parent_params;
|
|
expr const & parent_fn = get_app_args(parent, parent_params);
|
|
levels const & parent_ls = const_levels(parent_fn);
|
|
name const & parent_name = const_name(parent_fn);
|
|
auto parent_info = get_parent_info(parent_name);
|
|
name const & parent_intro_name = inductive::intro_rule_name(std::get<2>(parent_info));
|
|
expr parent_intro = mk_app(mk_constant(parent_intro_name, parent_ls), parent_params);
|
|
expr parent_type = m_ctx.infer(parent);
|
|
if (!is_sort(parent_type))
|
|
throw_ill_formed_parent(parent_name);
|
|
level parent_rlvl = sort_level(parent_type);
|
|
expr st_type = mk_app(mk_constant(m_name, st_ls), m_params);
|
|
binder_info bi;
|
|
if (m_attrs.has_class())
|
|
bi = mk_inst_implicit_binder_info();
|
|
expr st = mk_local(mk_fresh_name(), "s", st_type, bi);
|
|
expr coercion_type = infer_implicit(Pi(m_params, Pi(st, parent, m_p), m_p), m_params.size(), true);;
|
|
expr coercion_value = parent_intro;
|
|
for (unsigned idx : fmap) {
|
|
expr const & field = m_fields[idx].first;
|
|
name proj_name = m_name + mlocal_name(field);
|
|
expr proj = mk_app(mk_app(mk_constant(proj_name, st_ls), m_params), st);
|
|
coercion_value = mk_app(coercion_value, proj);
|
|
}
|
|
coercion_value = Fun(m_params, Fun(st, coercion_value, m_p), m_p);
|
|
name coercion_name = coercion_names[i];
|
|
bool use_conv_opt = false;
|
|
declaration coercion_decl = mk_definition_inferring_trusted(m_env, coercion_name, lnames,
|
|
coercion_type, coercion_value, use_conv_opt);
|
|
m_env = module::add(m_env, check(m_env, coercion_decl));
|
|
m_env = set_reducible(m_env, coercion_name, reducible_status::Reducible, true);
|
|
add_alias(coercion_name);
|
|
m_env = vm_compile(m_env, m_env.get(coercion_name));
|
|
if (!m_private_parents[i]) {
|
|
if (m_attrs.has_class() && is_class(m_env, parent_name)) {
|
|
// if both are classes, then we also mark coercion_name as an instance
|
|
m_env = add_instance(m_env, coercion_name, m_prio, true);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
void declare_no_confustion() {
|
|
if (!has_eq_decls(m_env))
|
|
return;
|
|
if (!has_heq_decls(m_env))
|
|
return;
|
|
m_env = mk_no_confusion(m_env, m_name);
|
|
name no_confusion_name(m_name, "no_confusion");
|
|
add_alias(no_confusion_name);
|
|
}
|
|
|
|
void add_doc_string() {
|
|
if (m_doc_string)
|
|
m_env = ::lean::add_doc_string(m_env, m_name, *m_doc_string);
|
|
}
|
|
|
|
environment operator()() {
|
|
process_header();
|
|
module::scope_pos_info scope(m_name_pos);
|
|
if (m_p.curr_is_token(get_assign_tk())) {
|
|
m_p.check_token_next(get_assign_tk(), "invalid 'structure', ':=' expected");
|
|
m_mk_pos = m_p.pos();
|
|
if (m_p.curr_is_token(get_lparen_tk()) || m_p.curr_is_token(get_lcurly_tk()) ||
|
|
m_p.curr_is_token(get_lbracket_tk())) {
|
|
m_mk_short = LEAN_DEFAULT_STRUCTURE_INTRO;
|
|
m_mk_infer = implicit_infer_kind::Implicit;
|
|
} else {
|
|
m_mk_short = m_p.check_atomic_id_next("invalid 'structure', atomic identifier expected");
|
|
m_mk_infer = parse_implicit_infer_modifier(m_p);
|
|
if (!m_p.curr_is_command_like())
|
|
m_p.check_token_next(get_dcolon_tk(), "invalid 'structure', '::' expected");
|
|
}
|
|
m_mk = m_name + m_mk_short;
|
|
process_new_fields();
|
|
} else {
|
|
m_mk_pos = m_name_pos;
|
|
m_mk_short = LEAN_DEFAULT_STRUCTURE_INTRO;
|
|
m_mk_infer = implicit_infer_kind::Implicit;
|
|
m_mk = m_name + m_mk_short;
|
|
process_empty_new_fields();
|
|
}
|
|
infer_resultant_universe();
|
|
set_ctx_locals();
|
|
include_ctx_levels();
|
|
m_ctx_levels = collect_local_nonvar_levels(m_p, to_list(m_level_names.begin(), m_level_names.end()));
|
|
declare_inductive_type();
|
|
declare_projections();
|
|
declare_defaults();
|
|
declare_auxiliary();
|
|
declare_coercions();
|
|
add_doc_string();
|
|
if (!m_inductive_predicate) {
|
|
declare_no_confustion();
|
|
}
|
|
return m_env;
|
|
}
|
|
};
|
|
|
|
environment structure_cmd_ex(parser & p, decl_attributes const & attrs, decl_modifiers const & modifiers) {
|
|
p.next();
|
|
return structure_cmd_fn(p, attrs, modifiers)();
|
|
}
|
|
|
|
environment structure_cmd(parser & p) {
|
|
return structure_cmd_ex(p, {}, {});
|
|
}
|
|
|
|
environment class_cmd_ex(parser & p, decl_modifiers const & modifiers) {
|
|
decl_attributes attrs;
|
|
attrs.set_attribute(p.env(), "class");
|
|
p.next();
|
|
if (p.curr_is_token(get_inductive_tk())) {
|
|
return inductive_cmd_ex(p, attrs, modifiers.m_is_meta);
|
|
} else {
|
|
return structure_cmd_fn(p, attrs, modifiers)();
|
|
}
|
|
}
|
|
|
|
environment class_cmd(parser & p) {
|
|
return class_cmd_ex(p, {});
|
|
}
|
|
|
|
void get_structure_fields(environment const & env, name const & S, buffer<name> & fields) {
|
|
lean_assert(is_structure_like(env, S));
|
|
level_param_names ls; unsigned nparams; inductive::intro_rule intro;
|
|
std::tie(ls, nparams, intro) = get_structure_info(env, S);
|
|
expr intro_type = inductive::intro_rule_type(intro);
|
|
unsigned i = 0;
|
|
while (is_pi(intro_type)) {
|
|
if (i >= nparams)
|
|
fields.push_back(S + binding_name(intro_type));
|
|
i++;
|
|
intro_type = binding_body(intro_type);
|
|
}
|
|
}
|
|
|
|
bool is_structure(environment const & env, name const & S) {
|
|
if (!is_structure_like(env, S))
|
|
return false;
|
|
level_param_names ls; unsigned nparams; inductive::intro_rule intro;
|
|
std::tie(ls, nparams, intro) = get_structure_info(env, S);
|
|
expr intro_type = inductive::intro_rule_type(intro);
|
|
for (unsigned i = 0; i < nparams; i++) {
|
|
if (!is_pi(intro_type))
|
|
return false;
|
|
intro_type = binding_body(intro_type);
|
|
}
|
|
if (!is_pi(intro_type))
|
|
return false;
|
|
name field_name = S + binding_name(intro_type);
|
|
return get_projection_info(env, field_name) != nullptr;
|
|
}
|
|
|
|
void register_structure_cmd(cmd_table & r) {
|
|
add_cmd(r, cmd_info("structure", "declare a new structure/record type", structure_cmd, false));
|
|
add_cmd(r, cmd_info("class", "declare a new class", class_cmd, false));
|
|
}
|
|
}
|