refactor(frontends/lean): do not hard code commands accepting attributes & modifiers
This commit is contained in:
Sebastian Ullrich
Leonardo de Moura
parent
2e142d87ae
commit
95b317fa64
31 changed files with 290 additions and 402 deletions
|
|
@ -8,11 +8,19 @@ Author: Leonardo de Moura
|
|||
#include <string>
|
||||
#include <functional>
|
||||
#include "kernel/environment.h"
|
||||
#include "frontends/lean/decl_util.h"
|
||||
#include "frontends/lean/parser_pos_provider.h"
|
||||
|
||||
namespace lean {
|
||||
class parser;
|
||||
typedef std::function<environment(parser&)> command_fn;
|
||||
|
||||
struct cmd_meta {
|
||||
decl_attributes m_attrs;
|
||||
decl_modifiers m_modifiers;
|
||||
optional<std::string> m_doc_string;
|
||||
};
|
||||
|
||||
typedef std::function<environment(parser&, cmd_meta const &)> command_fn;
|
||||
|
||||
template<typename F>
|
||||
struct cmd_info_tmpl {
|
||||
|
|
@ -23,6 +31,16 @@ struct cmd_info_tmpl {
|
|||
public:
|
||||
cmd_info_tmpl(name const & n, char const * d, F const & fn, bool skip_token = true):
|
||||
m_name(n), m_descr(d), m_fn(fn), m_skip_token(skip_token) {}
|
||||
cmd_info_tmpl(name const & n, char const * d, std::function<environment(parser&)> const & fn, bool skip_token = true):
|
||||
cmd_info_tmpl(n, d, [=](parser & p, cmd_meta const & meta) {
|
||||
if (meta.m_modifiers)
|
||||
throw exception("command does not accept modifiers");
|
||||
if (meta.m_attrs)
|
||||
throw exception("command does not accept attributes");
|
||||
if (meta.m_doc_string)
|
||||
throw exception("command does not accept doc string");
|
||||
return fn(p);
|
||||
}, skip_token) {}
|
||||
cmd_info_tmpl() {}
|
||||
name const & get_name() const { return m_name; }
|
||||
std::string const & get_descr() const { return m_descr; }
|
||||
|
|
|
|||
|
|
@ -36,6 +36,7 @@ public:
|
|||
list<entry> const & get_entries() const { return m_entries; }
|
||||
bool is_parsing_only() const { return m_parsing_only; }
|
||||
optional<unsigned > get_priority() const { return m_prio; }
|
||||
void set_persistent(bool persistent) { m_persistent = persistent; }
|
||||
bool ok_for_inductive_type() const;
|
||||
bool has_class() const;
|
||||
operator bool() const { return static_cast<bool>(m_entries); }
|
||||
|
|
|
|||
|
|
@ -92,7 +92,7 @@ static void check_parameter_type(parser & p, name const & n, expr const & type,
|
|||
static environment declare_var(parser & p, environment env,
|
||||
name const & n, level_param_names const & ls, expr const & type,
|
||||
variable_kind k, optional<binder_info> const & _bi, pos_info const & pos,
|
||||
decl_modifiers const & modifiers) {
|
||||
cmd_meta const & meta) {
|
||||
binder_info bi;
|
||||
if (_bi) bi = *_bi;
|
||||
if (k == variable_kind::Parameter || k == variable_kind::Variable) {
|
||||
|
|
@ -125,18 +125,18 @@ static environment declare_var(parser & p, environment env,
|
|||
if (k == variable_kind::Axiom) {
|
||||
env = module::add(env, check(env, mk_axiom(full_n, ls, new_type)));
|
||||
} else {
|
||||
bool is_trusted = !modifiers.m_is_meta;
|
||||
bool is_trusted = !meta.m_modifiers.m_is_meta;
|
||||
env = module::add(env, check(env, mk_constant_assumption(full_n, ls, new_type, is_trusted)));
|
||||
}
|
||||
if (auto doc = p.get_doc_string())
|
||||
env = add_doc_string(env, full_n, *doc);
|
||||
if (meta.m_doc_string)
|
||||
env = add_doc_string(env, full_n, *meta.m_doc_string);
|
||||
if (!ns.is_anonymous()) {
|
||||
if (modifiers.m_is_protected)
|
||||
if (meta.m_modifiers.m_is_protected)
|
||||
env = add_expr_alias(env, get_protected_shortest_name(full_n), full_n);
|
||||
else
|
||||
env = add_expr_alias(env, n, full_n);
|
||||
}
|
||||
if (modifiers.m_is_protected)
|
||||
if (meta.m_modifiers.m_is_protected)
|
||||
env = add_protected(env, full_n);
|
||||
env = ensure_decl_namespaces(env, full_n);
|
||||
return env;
|
||||
|
|
@ -190,7 +190,7 @@ static bool curr_is_binder_annotation(parser & p) {
|
|||
p.curr_is_token(get_ldcurly_tk()) || p.curr_is_token(get_lbracket_tk());
|
||||
}
|
||||
|
||||
static environment variable_cmd_core(parser & p, variable_kind k, decl_modifiers const & modifiers = decl_modifiers()) {
|
||||
static environment variable_cmd_core(parser & p, variable_kind k, cmd_meta const & meta) {
|
||||
check_variable_kind(p, k);
|
||||
auto pos = p.pos();
|
||||
module::scope_pos_info scope_pos(pos);
|
||||
|
|
@ -284,22 +284,24 @@ static environment variable_cmd_core(parser & p, variable_kind k, decl_modifiers
|
|||
std::tie(type, new_ls) = p.elaborate_type("_variable", ctx, type);
|
||||
if (k == variable_kind::Variable || k == variable_kind::Parameter)
|
||||
update_local_levels(p, new_ls, k == variable_kind::Variable);
|
||||
return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos, modifiers);
|
||||
return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos, meta);
|
||||
}
|
||||
static environment variable_cmd(parser & p) {
|
||||
return variable_cmd_core(p, variable_kind::Variable);
|
||||
static environment variable_cmd(parser & p, cmd_meta const & meta) {
|
||||
return variable_cmd_core(p, variable_kind::Variable, meta);
|
||||
}
|
||||
static environment axiom_cmd(parser & p) {
|
||||
return variable_cmd_core(p, variable_kind::Axiom);
|
||||
static environment axiom_cmd(parser & p, cmd_meta const & meta) {
|
||||
if (meta.m_modifiers.m_is_meta)
|
||||
throw exception("invalid 'meta' modifier for axiom");
|
||||
return variable_cmd_core(p, variable_kind::Axiom, meta);
|
||||
}
|
||||
static environment constant_cmd(parser & p) {
|
||||
return variable_cmd_core(p, variable_kind::Constant);
|
||||
static environment constant_cmd(parser & p, cmd_meta const & meta) {
|
||||
return variable_cmd_core(p, variable_kind::Constant, meta);
|
||||
}
|
||||
static environment parameter_cmd(parser & p) {
|
||||
return variable_cmd_core(p, variable_kind::Parameter);
|
||||
static environment parameter_cmd(parser & p, cmd_meta const & meta) {
|
||||
return variable_cmd_core(p, variable_kind::Parameter, meta);
|
||||
}
|
||||
|
||||
static environment variables_cmd_core(parser & p, variable_kind k, decl_modifiers const & modifiers = decl_modifiers()) {
|
||||
static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta const & meta) {
|
||||
check_variable_kind(p, k);
|
||||
auto pos = p.pos();
|
||||
module::scope_pos_info scope_pos(pos);
|
||||
|
|
@ -325,7 +327,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, decl_modifier
|
|||
p.parse_close_binder_info(bi);
|
||||
update_local_binder_info(p, k, id, bi, pos);
|
||||
if (curr_is_binder_annotation(p))
|
||||
return variables_cmd_core(p, k);
|
||||
return variables_cmd_core(p, k, meta);
|
||||
else
|
||||
return env;
|
||||
} else {
|
||||
|
|
@ -363,7 +365,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, decl_modifier
|
|||
update_local_binder_info(p, k, id, bi, pos);
|
||||
}
|
||||
if (curr_is_binder_annotation(p))
|
||||
return variables_cmd_core(p, k);
|
||||
return variables_cmd_core(p, k, meta);
|
||||
else
|
||||
return env;
|
||||
} else {
|
||||
|
|
@ -388,7 +390,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, decl_modifier
|
|||
if (k == variable_kind::Variable || k == variable_kind::Parameter)
|
||||
update_local_levels(p, new_ls, k == variable_kind::Variable);
|
||||
new_ls = append(ls, new_ls);
|
||||
env = declare_var(p, env, id, new_ls, new_type, k, bi, pos, modifiers);
|
||||
env = declare_var(p, env, id, new_ls, new_type, k, bi, pos, meta);
|
||||
}
|
||||
if (curr_is_binder_annotation(p)) {
|
||||
if (k == variable_kind::Constant || k == variable_kind::Axiom) {
|
||||
|
|
@ -396,125 +398,87 @@ static environment variables_cmd_core(parser & p, variable_kind k, decl_modifier
|
|||
// We must do that to be able to process
|
||||
// constants (A : Type) (a : A)
|
||||
parser::local_scope scope2(p, env);
|
||||
return variables_cmd_core(p, k);
|
||||
return variables_cmd_core(p, k, meta);
|
||||
} else {
|
||||
return variables_cmd_core(p, k);
|
||||
return variables_cmd_core(p, k, meta);
|
||||
}
|
||||
}
|
||||
return env;
|
||||
}
|
||||
static environment variables_cmd(parser & p) {
|
||||
return variables_cmd_core(p, variable_kind::Variable);
|
||||
static environment variables_cmd(parser & p, cmd_meta const & meta) {
|
||||
return variables_cmd_core(p, variable_kind::Variable, meta);
|
||||
}
|
||||
static environment parameters_cmd(parser & p) {
|
||||
return variables_cmd_core(p, variable_kind::Parameter);
|
||||
static environment parameters_cmd(parser & p, cmd_meta const & meta) {
|
||||
return variables_cmd_core(p, variable_kind::Parameter, meta);
|
||||
}
|
||||
static environment constants_cmd(parser & p) {
|
||||
return variables_cmd_core(p, variable_kind::Constant);
|
||||
static environment constants_cmd(parser & p, cmd_meta const & meta) {
|
||||
return variables_cmd_core(p, variable_kind::Constant, meta);
|
||||
}
|
||||
static environment axioms_cmd(parser & p) {
|
||||
return variables_cmd_core(p, variable_kind::Axiom);
|
||||
static environment axioms_cmd(parser & p, cmd_meta const & meta) {
|
||||
return variables_cmd_core(p, variable_kind::Axiom, meta);
|
||||
}
|
||||
|
||||
static environment definition_cmd_ex(parser & p, decl_attributes const & attributes) {
|
||||
decl_modifiers modifiers;
|
||||
static environment definition_cmd(parser & p, cmd_meta const & meta) {
|
||||
return definition_cmd_core(p, def_cmd_kind::Definition, meta);
|
||||
}
|
||||
static environment theorem_cmd(parser & p, cmd_meta const & meta) {
|
||||
return definition_cmd_core(p, def_cmd_kind::Theorem, meta);
|
||||
}
|
||||
static environment example_cmd(parser & p, cmd_meta const & meta) {
|
||||
return definition_cmd_core(p, def_cmd_kind::Example, meta);
|
||||
}
|
||||
static environment instance_cmd(parser & p, cmd_meta const & _meta) {
|
||||
auto meta = _meta;
|
||||
if (meta.m_modifiers.m_is_private)
|
||||
throw exception("invalid 'private' modifier for instance command");
|
||||
if (meta.m_modifiers.m_is_protected)
|
||||
throw exception("invalid 'protected' modifier for instance command");
|
||||
if (meta.m_modifiers.m_is_mutual)
|
||||
throw exception("invalid 'mutual' modifier for instance command");
|
||||
meta.m_modifiers.m_is_protected = true;
|
||||
return definition_cmd_core(p, def_cmd_kind::Instance, meta);
|
||||
}
|
||||
|
||||
static environment modifiers_cmd(parser & p, cmd_meta const & _meta) {
|
||||
auto meta = _meta;
|
||||
if (p.curr_is_token(get_private_tk())) {
|
||||
modifiers.m_is_private = true;
|
||||
meta.m_modifiers.m_is_private = true;
|
||||
p.next();
|
||||
|
||||
if (!attributes && p.curr_is_token(get_structure_tk())) {
|
||||
return structure_cmd_ex(p, attributes, modifiers);
|
||||
}
|
||||
if (!attributes && p.curr_is_token(get_class_tk())) {
|
||||
return class_cmd_ex(p, attributes, modifiers);
|
||||
}
|
||||
} else if (p.curr_is_token(get_protected_tk())) {
|
||||
modifiers.m_is_protected = true;
|
||||
meta.m_modifiers.m_is_protected = true;
|
||||
p.next();
|
||||
if (!attributes) {
|
||||
if (p.curr_is_token_or_id(get_axiom_tk())) {
|
||||
p.next();
|
||||
return variable_cmd_core(p, variable_kind::Axiom, modifiers);
|
||||
} else if (p.curr_is_token_or_id(get_constant_tk())) {
|
||||
p.next();
|
||||
return variable_cmd_core(p, variable_kind::Constant, modifiers);
|
||||
} else if (p.curr_is_token_or_id(get_axioms_tk())) {
|
||||
p.next();
|
||||
return variables_cmd_core(p, variable_kind::Axiom, modifiers);
|
||||
} else if (p.curr_is_token_or_id(get_constants_tk())) {
|
||||
p.next();
|
||||
return variables_cmd_core(p, variable_kind::Constant, modifiers);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (p.curr_is_token(get_noncomputable_tk())) {
|
||||
modifiers.m_is_noncomputable = true;
|
||||
p.next();
|
||||
|
||||
if (!attributes && !modifiers.m_is_private && !modifiers.m_is_protected && p.curr_is_token_or_id(get_theory_tk())) {
|
||||
if (!meta.m_attrs && !meta.m_modifiers && p.curr_is_token_or_id(get_theory_tk())) {
|
||||
// `noncomputable theory`
|
||||
p.next();
|
||||
p.set_ignore_noncomputable();
|
||||
return p.env();
|
||||
} else {
|
||||
meta.m_modifiers.m_is_noncomputable = true;
|
||||
}
|
||||
}
|
||||
if (p.curr_is_token(get_meta_tk())) {
|
||||
modifiers.m_is_meta = true;
|
||||
meta.m_modifiers.m_is_meta = true;
|
||||
p.next();
|
||||
if (!attributes) {
|
||||
if (p.curr_is_token_or_id(get_constant_tk())) {
|
||||
p.next();
|
||||
return variable_cmd_core(p, variable_kind::Constant, modifiers);
|
||||
} else if (p.curr_is_token_or_id(get_constants_tk())) {
|
||||
p.next();
|
||||
return variables_cmd_core(p, variable_kind::Constant, modifiers);
|
||||
}
|
||||
}
|
||||
if (!modifiers.m_is_private && !modifiers.m_is_protected && p.curr_is_token(get_inductive_tk())) {
|
||||
return inductive_cmd_ex(p, attributes, modifiers.m_is_meta);
|
||||
}
|
||||
if (!attributes && !modifiers.m_is_protected && p.curr_is_token(get_structure_tk())) {
|
||||
return structure_cmd_ex(p, attributes, modifiers);
|
||||
}
|
||||
if (!attributes && !modifiers.m_is_protected && p.curr_is_token(get_class_tk())) {
|
||||
return class_cmd_ex(p, attributes, modifiers);
|
||||
}
|
||||
}
|
||||
|
||||
if (p.curr_is_token(get_mutual_tk())) {
|
||||
modifiers.m_is_mutual = true;
|
||||
meta.m_modifiers.m_is_mutual = true;
|
||||
p.next();
|
||||
if (!modifiers.m_is_private && !modifiers.m_is_protected && !modifiers.m_is_noncomputable &&
|
||||
p.curr_is_token(get_inductive_tk())) {
|
||||
return mutual_inductive_cmd_ex(p, attributes, modifiers.m_is_meta);
|
||||
} else if (!modifiers.m_is_private && !modifiers.m_is_protected && !modifiers.m_is_noncomputable &&
|
||||
!modifiers.m_is_meta && p.curr_is_token(get_coinductive_tk())) {
|
||||
return mutual_coinductive_cmd_ex(p, attributes);
|
||||
}
|
||||
}
|
||||
|
||||
def_cmd_kind kind = Definition;
|
||||
if (p.curr_is_token_or_id(get_definition_tk())) {
|
||||
p.next();
|
||||
} else if (p.curr_is_token_or_id(get_theorem_tk())) {
|
||||
p.next();
|
||||
kind = Theorem;
|
||||
} else if (p.curr_is_token_or_id(get_example_tk())) {
|
||||
p.next();
|
||||
kind = Example;
|
||||
} else if (!modifiers.m_is_private && !modifiers.m_is_protected && p.curr_is_token_or_id(get_instance_tk())) {
|
||||
p.next();
|
||||
modifiers.m_is_protected = true;
|
||||
modifiers.m_is_instance = true;
|
||||
} else {
|
||||
throw parser_error("invalid definition/theorem, 'definition' or 'theorem' expected", p.pos());
|
||||
if (p.curr_is_token(get_private_tk()) || p.curr_is_token(get_protected_tk()) || p.curr_is_token(get_noncomputable_tk())
|
||||
|| p.curr_is_token(get_meta_tk()) || p.curr_is_token(get_mutual_tk())) {
|
||||
throw parser_error("unexpected definition modifier", p.pos());
|
||||
}
|
||||
|
||||
return definition_cmd_core(p, kind, modifiers, attributes);
|
||||
}
|
||||
|
||||
static environment definition_cmd(parser & p) {
|
||||
return definition_cmd_ex(p, {});
|
||||
if (p.curr_is_token(get_attribute_tk()) || p.curr_is_token("@[")) {
|
||||
throw parser_error("unexpected attributes declaration", p.pos());
|
||||
}
|
||||
p.parse_command(meta);
|
||||
return p.env();
|
||||
}
|
||||
|
||||
static environment attribute_cmd_core(parser & p, bool persistent) {
|
||||
|
|
@ -523,17 +487,7 @@ static environment attribute_cmd_core(parser & p, bool persistent) {
|
|||
attributes.parse(p);
|
||||
// 'attribute [attr] definition ...'
|
||||
if (p.curr_is_command()) {
|
||||
if (p.curr_is_token_or_id(get_inductive_tk())) {
|
||||
return inductive_cmd_ex(p, attributes, false);
|
||||
} else if (p.curr_is_token_or_id(get_coinductive_tk())) {
|
||||
return coinductive_cmd_ex(p, attributes);
|
||||
} else if (p.curr_is_token_or_id(get_structure_tk())) {
|
||||
return structure_cmd_ex(p, attributes, {});
|
||||
} else if (p.curr_is_token_or_id(get_class_tk())) {
|
||||
return class_cmd_ex(p, attributes, {});
|
||||
} else {
|
||||
return definition_cmd_ex(p, attributes);
|
||||
}
|
||||
return modifiers_cmd(p, {attributes, {}, {}});
|
||||
}
|
||||
name d = p.check_constant_next("invalid 'attribute' command, constant expected");
|
||||
ds.push_back(d);
|
||||
|
|
@ -556,21 +510,11 @@ environment local_attribute_cmd(parser & p) {
|
|||
return attribute_cmd_core(p, false);
|
||||
}
|
||||
|
||||
static environment compact_attribute_cmd(parser & p) {
|
||||
static environment compact_attribute_cmd(parser & p, cmd_meta const & meta) {
|
||||
bool persistent = true;
|
||||
decl_attributes attributes(persistent);
|
||||
attributes.parse_compact(p);
|
||||
if (p.curr_is_token_or_id(get_inductive_tk())) {
|
||||
return inductive_cmd_ex(p, attributes, false);
|
||||
} else if (p.curr_is_token_or_id(get_coinductive_tk())) {
|
||||
return coinductive_cmd_ex(p, attributes);
|
||||
} else if (p.curr_is_token_or_id(get_structure_tk())) {
|
||||
return structure_cmd_ex(p, attributes, {});
|
||||
} else if (p.curr_is_token_or_id(get_class_tk())) {
|
||||
return class_cmd_ex(p, attributes, {});
|
||||
} else {
|
||||
return definition_cmd_ex(p, attributes);
|
||||
}
|
||||
return modifiers_cmd(p, {attributes, meta.m_modifiers, meta.m_doc_string});
|
||||
}
|
||||
|
||||
static environment include_cmd_core(parser & p, bool include) {
|
||||
|
|
@ -614,15 +558,15 @@ void register_decl_cmds(cmd_table & r) {
|
|||
add_cmd(r, cmd_info("parameters", "declare new parameters", parameters_cmd));
|
||||
add_cmd(r, cmd_info("constants", "declare new constants (aka top-level variables)", constants_cmd));
|
||||
add_cmd(r, cmd_info("axioms", "declare new axioms", axioms_cmd));
|
||||
add_cmd(r, cmd_info("definition", "add new definition", definition_cmd, false));
|
||||
add_cmd(r, cmd_info("meta", "add new meta definition/constant", definition_cmd, false));
|
||||
add_cmd(r, cmd_info("mutual", "add new mutal definition/constant/inductive/coinductive", definition_cmd, false));
|
||||
add_cmd(r, cmd_info("noncomputable", "add new noncomputable definition", definition_cmd, false));
|
||||
add_cmd(r, cmd_info("private", "add new private definition/theorem", definition_cmd, false));
|
||||
add_cmd(r, cmd_info("protected", "add new protected definition/theorem/variable", definition_cmd, false));
|
||||
add_cmd(r, cmd_info("theorem", "add new theorem", definition_cmd, false));
|
||||
add_cmd(r, cmd_info("instance", "add new instance", definition_cmd, false));
|
||||
add_cmd(r, cmd_info("example", "add new example", definition_cmd, false));
|
||||
add_cmd(r, cmd_info("meta", "add new meta declaration", modifiers_cmd, false));
|
||||
add_cmd(r, cmd_info("mutual", "add new mutal declaration", modifiers_cmd, false));
|
||||
add_cmd(r, cmd_info("noncomputable", "add new noncomputable definition", modifiers_cmd, false));
|
||||
add_cmd(r, cmd_info("private", "add new private declaration", modifiers_cmd, false));
|
||||
add_cmd(r, cmd_info("protected", "add new protected declaration", modifiers_cmd, false));
|
||||
add_cmd(r, cmd_info("definition", "add new definition", definition_cmd));
|
||||
add_cmd(r, cmd_info("theorem", "add new theorem", theorem_cmd));
|
||||
add_cmd(r, cmd_info("instance", "add new instance", instance_cmd));
|
||||
add_cmd(r, cmd_info("example", "add new example", example_cmd));
|
||||
add_cmd(r, cmd_info("include", "force section parameter/variable to be included", include_cmd));
|
||||
add_cmd(r, cmd_info("attribute", "set declaration attributes", attribute_cmd));
|
||||
add_cmd(r, cmd_info("@[", "declaration attributes", compact_attribute_cmd));
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ namespace lean {
|
|||
class parser;
|
||||
class elaborator;
|
||||
|
||||
enum def_cmd_kind { Theorem, Definition, Example };
|
||||
enum def_cmd_kind { Theorem, Definition, Example, Instance };
|
||||
|
||||
struct decl_modifiers {
|
||||
bool m_is_private{false};
|
||||
|
|
@ -21,8 +21,10 @@ struct decl_modifiers {
|
|||
bool m_is_meta{false};
|
||||
bool m_is_mutual{false};
|
||||
bool m_is_noncomputable{false};
|
||||
bool m_is_instance{false};
|
||||
bool m_is_class{false};
|
||||
|
||||
operator bool() const {
|
||||
return m_is_private || m_is_protected || m_is_meta || m_is_mutual || m_is_noncomputable;
|
||||
}
|
||||
};
|
||||
|
||||
/** \brief In Lean, declarations may contain nested definitions.
|
||||
|
|
|
|||
|
|
@ -242,24 +242,23 @@ static environment compile_decl(parser & p, environment const & env,
|
|||
|
||||
static pair<environment, name>
|
||||
declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffer<name> const & lp_names,
|
||||
name const & c_name, expr type, optional<expr> val, task<expr> const & proof,
|
||||
decl_modifiers const & modifiers, decl_attributes attrs, optional<std::string> const & doc_string,
|
||||
name const & c_name, expr type, optional<expr> val, task<expr> const & proof, cmd_meta const & meta,
|
||||
pos_info const & pos) {
|
||||
auto env_n = mk_real_name(env, c_name, modifiers.m_is_private, pos);
|
||||
auto env_n = mk_real_name(env, c_name, meta.m_modifiers.m_is_private, pos);
|
||||
environment new_env = env_n.first;
|
||||
name c_real_name = env_n.second;
|
||||
if (val && modifiers.m_is_meta) {
|
||||
if (val && meta.m_modifiers.m_is_meta) {
|
||||
/* TODO(Leo): fix fix_rec_fn_name for mutual definitions.
|
||||
We currently do not support meta mutual definitions. Thus, this is not currently an issue. */
|
||||
*val = fix_rec_fn_name(*val, c_name, c_real_name);
|
||||
}
|
||||
if (val && !modifiers.m_is_meta && !type_checker(env).is_prop(type)) {
|
||||
if (val && !meta.m_modifiers.m_is_meta && !type_checker(env).is_prop(type)) {
|
||||
/* We only abstract nested proofs if the type of the definition is not a proposition */
|
||||
std::tie(new_env, type) = abstract_nested_proofs(new_env, c_real_name, type);
|
||||
std::tie(new_env, *val) = abstract_nested_proofs(new_env, c_real_name, *val);
|
||||
}
|
||||
bool use_conv_opt = true;
|
||||
bool is_trusted = !modifiers.m_is_meta;
|
||||
bool is_trusted = !meta.m_modifiers.m_is_meta;
|
||||
auto def =
|
||||
!val ? mk_theorem(c_real_name, to_list(lp_names), type, proof) : (kind == Theorem ?
|
||||
mk_theorem(c_real_name, to_list(lp_names), type, *val) :
|
||||
|
|
@ -267,23 +266,23 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe
|
|||
auto cdef = check(p, new_env, c_name, def, pos);
|
||||
new_env = module::add(new_env, cdef);
|
||||
|
||||
check_noncomputable(p.ignore_noncomputable(), new_env, c_name, c_real_name, modifiers.m_is_noncomputable, p.get_file_name(), pos);
|
||||
check_noncomputable(p.ignore_noncomputable(), new_env, c_name, c_real_name, meta.m_modifiers.m_is_noncomputable, p.get_file_name(), pos);
|
||||
|
||||
if (modifiers.m_is_protected)
|
||||
if (meta.m_modifiers.m_is_protected)
|
||||
new_env = add_protected(new_env, c_real_name);
|
||||
|
||||
new_env = add_alias(new_env, modifiers.m_is_protected, c_name, c_real_name);
|
||||
new_env = add_alias(new_env, meta.m_modifiers.m_is_protected, c_name, c_real_name);
|
||||
|
||||
if (!modifiers.m_is_private) {
|
||||
if (!meta.m_modifiers.m_is_private) {
|
||||
new_env = ensure_decl_namespaces(new_env, c_real_name);
|
||||
}
|
||||
|
||||
new_env = compile_decl(p, new_env, c_name, c_real_name, pos);
|
||||
if (doc_string) {
|
||||
new_env = add_doc_string(new_env, c_real_name, *doc_string);
|
||||
if (meta.m_doc_string) {
|
||||
new_env = add_doc_string(new_env, c_real_name, *meta.m_doc_string);
|
||||
}
|
||||
// note: some attribute handlers rely on the new definition being compiled already
|
||||
new_env = attrs.apply(new_env, p.ios(), c_real_name);
|
||||
new_env = meta.m_attrs.apply(new_env, p.ios(), c_real_name);
|
||||
return mk_pair(new_env, c_real_name);
|
||||
}
|
||||
|
||||
|
|
@ -470,16 +469,16 @@ static environment copy_equation_lemmas(environment const & env, name const & d_
|
|||
return copy_equation_lemmas(env, d_names);
|
||||
}
|
||||
|
||||
environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modifiers const & modifiers, decl_attributes attrs) {
|
||||
static environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta const & meta) {
|
||||
buffer<name> lp_names;
|
||||
buffer<expr> fns, params;
|
||||
declaration_info_scope scope(p, kind, modifiers);
|
||||
declaration_info_scope scope(p, kind, meta.m_modifiers);
|
||||
auto header_pos = p.pos();
|
||||
/* TODO(Leo): allow a different doc string for each function in a mutual definition. */
|
||||
optional<std::string> doc_string = p.get_doc_string();
|
||||
optional<std::string> doc_string = meta.m_doc_string;
|
||||
expr val = parse_mutual_definition(p, lp_names, fns, params);
|
||||
|
||||
if (modifiers.m_is_meta) {
|
||||
if (meta.m_modifiers.m_is_meta) {
|
||||
throw exception("support for mutual meta definitions has not been implemented yet");
|
||||
}
|
||||
|
||||
|
|
@ -505,13 +504,12 @@ environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
|
|||
for (unsigned i = 0; i < num_defs; i++) {
|
||||
expr curr = get_equations_result(val, i);
|
||||
expr curr_type = head_beta_reduce(elab.infer_type(curr));
|
||||
finalize_definition(elab, new_params, curr_type, curr, lp_names, modifiers.m_is_meta);
|
||||
finalize_definition(elab, new_params, curr_type, curr, lp_names, meta.m_modifiers.m_is_meta);
|
||||
environment env = elab.env();
|
||||
name c_name = mlocal_name(fns[i]);
|
||||
name c_real_name;
|
||||
std::tie(env, c_real_name) = declare_definition(p, env, kind, lp_names, c_name,
|
||||
curr_type, some_expr(curr), {}, modifiers, attrs,
|
||||
doc_string, header_pos);
|
||||
curr_type, some_expr(curr), {}, meta, header_pos);
|
||||
new_d_names.push_back(c_real_name);
|
||||
elab.set_env(env);
|
||||
}
|
||||
|
|
@ -768,21 +766,20 @@ static bool is_rfl_preexpr(expr const & e) {
|
|||
return is_constant(e, get_rfl_name());
|
||||
}
|
||||
|
||||
environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modifiers modifiers, decl_attributes attrs) {
|
||||
environment single_definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta meta) {
|
||||
buffer<name> lp_names;
|
||||
buffer<expr> params;
|
||||
expr fn, val;
|
||||
auto header_pos = p.pos();
|
||||
optional<std::string> doc_string = p.get_doc_string();
|
||||
module::scope_pos_info scope_pos(header_pos);
|
||||
declaration_info_scope scope(p, kind, modifiers);
|
||||
declaration_info_scope scope(p, kind, meta.m_modifiers);
|
||||
bool is_example = (kind == def_cmd_kind::Example);
|
||||
bool is_instance = modifiers.m_is_instance;
|
||||
bool is_instance = (kind == def_cmd_kind::Instance);
|
||||
bool aux_lemmas = scope.gen_aux_lemmas();
|
||||
bool is_rfl = false;
|
||||
if (is_instance)
|
||||
attrs.set_attribute(p.env(), "instance");
|
||||
std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance, modifiers.m_is_meta);
|
||||
meta.m_attrs.set_attribute(p.env(), "instance");
|
||||
std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance, meta.m_modifiers.m_is_meta);
|
||||
|
||||
auto begin_pos = p.cmd_pos();
|
||||
auto end_pos = p.pos();
|
||||
|
|
@ -827,8 +824,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
|
|||
new_fn, val, thm_finfo, is_rfl, type,
|
||||
mctx, lctx, pos_provider, use_info_manager, file_name);
|
||||
}), log_tree::ElaborationLevel);
|
||||
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, proof, modifiers, attrs,
|
||||
doc_string, header_pos);
|
||||
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, proof, meta, header_pos);
|
||||
} else if (kind == Example) {
|
||||
auto env = p.env();
|
||||
auto opts = p.get_options();
|
||||
|
|
@ -841,7 +837,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
|
|||
bool noncomputable_theory = p.ignore_noncomputable();
|
||||
std::string file_name = p.get_file_name();
|
||||
add_library_task<unit>([=] {
|
||||
check_example(env, opts, modifiers, noncomputable_theory,
|
||||
check_example(env, opts, meta.m_modifiers, noncomputable_theory,
|
||||
lp_name_list, new_params_list, fn, val, mctx, lctx,
|
||||
pos_provider, use_info_manager, file_name);
|
||||
return unit();
|
||||
|
|
@ -849,7 +845,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
|
|||
return p.env();
|
||||
} else {
|
||||
std::tie(val, type) = elaborate_definition(p, elab, kind, fn, val, header_pos);
|
||||
if (modifiers.m_is_meta) {
|
||||
if (meta.m_modifiers.m_is_meta) {
|
||||
val = fix_rec_fn_macro_args(elab, mlocal_name(fn), new_params, type, val);
|
||||
}
|
||||
eqns = is_equations_result(val);
|
||||
|
|
@ -858,9 +854,9 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
|
|||
lean_assert(get_equations_result_size(val) == 1);
|
||||
val = get_equations_result(val, 0);
|
||||
}
|
||||
finalize_definition(elab, new_params, type, val, lp_names, modifiers.m_is_meta);
|
||||
finalize_definition(elab, new_params, type, val, lp_names, meta.m_modifiers.m_is_meta);
|
||||
env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, some_expr(val),
|
||||
{}, modifiers, attrs, doc_string, header_pos);
|
||||
{}, meta, header_pos);
|
||||
}
|
||||
environment new_env = env_n.first;
|
||||
name c_real_name = env_n.second;
|
||||
|
|
@ -869,9 +865,9 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
|
|||
if (eqns && aux_lemmas) {
|
||||
new_env = copy_equation_lemmas(new_env, c_real_name);
|
||||
}
|
||||
if (!eqns && !modifiers.m_is_meta && kind == Definition) {
|
||||
if (!eqns && !meta.m_modifiers.m_is_meta && (kind == Definition || kind == Instance)) {
|
||||
unsigned arity = new_params.size();
|
||||
new_env = mk_simple_equation_lemma_for(new_env, p.get_options(), modifiers.m_is_private, c_real_name, arity);
|
||||
new_env = mk_simple_equation_lemma_for(new_env, p.get_options(), meta.m_modifiers.m_is_private, c_real_name, arity);
|
||||
}
|
||||
return new_env;
|
||||
};
|
||||
|
|
@ -890,10 +886,10 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
|
|||
}
|
||||
}
|
||||
|
||||
environment definition_cmd_core(parser & p, def_cmd_kind kind, decl_modifiers const & modifiers, decl_attributes attrs) {
|
||||
if (modifiers.m_is_mutual)
|
||||
return mutual_definition_cmd_core(p, kind, modifiers, attrs);
|
||||
environment definition_cmd_core(parser & p, def_cmd_kind kind, cmd_meta const & meta) {
|
||||
if (meta.m_modifiers.m_is_mutual)
|
||||
return mutual_definition_cmd_core(p, kind, meta);
|
||||
else
|
||||
return single_definition_cmd_core(p, kind, modifiers, attrs);
|
||||
return single_definition_cmd_core(p, kind, meta);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Author: Leonardo de Moura
|
|||
#include "frontends/lean/decl_util.h"
|
||||
namespace lean {
|
||||
|
||||
environment definition_cmd_core(parser & p, def_cmd_kind k, decl_modifiers const & modifies, decl_attributes attributes);
|
||||
environment definition_cmd_core(parser & p, def_cmd_kind k, cmd_meta const & meta);
|
||||
|
||||
environment ensure_decl_namespaces(environment const & env, name const & full_n);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -89,8 +89,7 @@ static level subtract_from_max(level const & l, unsigned offset) {
|
|||
class inductive_cmd_fn {
|
||||
parser & m_p;
|
||||
environment m_env;
|
||||
decl_attributes m_attrs;
|
||||
bool m_is_trusted;
|
||||
cmd_meta m_meta_info;
|
||||
buffer<decl_attributes> m_mut_attrs;
|
||||
type_context m_ctx;
|
||||
buffer<name> m_lp_names;
|
||||
|
|
@ -102,7 +101,6 @@ class inductive_cmd_fn {
|
|||
unsigned m_u_param_offset;
|
||||
|
||||
bool m_infer_result_universe{false};
|
||||
optional<std::string> m_doc_string;
|
||||
|
||||
[[ noreturn ]] void throw_error(char const * error_msg) const { throw parser_error(error_msg, m_pos); }
|
||||
[[ noreturn ]] void throw_error(sstream const & strm) const { throw parser_error(strm, m_pos); }
|
||||
|
|
@ -568,9 +566,6 @@ class inductive_cmd_fn {
|
|||
parser::local_scope scope(m_p);
|
||||
m_pos = m_p.pos();
|
||||
|
||||
m_attrs.parse(m_p);
|
||||
check_attrs(m_attrs);
|
||||
|
||||
declaration_name_scope nscope;
|
||||
expr ind = parse_single_header(m_p, nscope, m_lp_names, params);
|
||||
m_explicit_levels = !m_lp_names.empty();
|
||||
|
|
@ -602,9 +597,6 @@ class inductive_cmd_fn {
|
|||
void parse_mutual_inductive(buffer<expr> & params, buffer<expr> & inds, buffer<buffer<expr> > & intro_rules) {
|
||||
parser::local_scope scope(m_p);
|
||||
|
||||
m_attrs.parse(m_p);
|
||||
check_attrs(m_attrs);
|
||||
|
||||
buffer<expr> pre_inds;
|
||||
parse_mutual_header(m_p, m_lp_names, pre_inds, params);
|
||||
m_explicit_levels = !m_lp_names.empty();
|
||||
|
|
@ -641,25 +633,33 @@ class inductive_cmd_fn {
|
|||
if (!attrs.ok_for_inductive_type())
|
||||
throw_error("only attribute [class] accepted for inductive types");
|
||||
}
|
||||
|
||||
void check_modifiers() const {
|
||||
if (m_meta_info.m_modifiers.m_is_noncomputable)
|
||||
throw_error("invalid 'noncomputable' modifier for inductive type");
|
||||
if (m_meta_info.m_modifiers.m_is_private)
|
||||
throw_error("invalid 'private' modifier for inductive type");
|
||||
if (m_meta_info.m_modifiers.m_is_protected)
|
||||
throw_error("invalid 'protected' modifier for inductive type");
|
||||
}
|
||||
public:
|
||||
inductive_cmd_fn(parser & p, decl_attributes const & attrs, bool is_trusted):
|
||||
m_p(p), m_env(p.env()), m_attrs(attrs),
|
||||
m_is_trusted(is_trusted), m_ctx(p.env()) {
|
||||
inductive_cmd_fn(parser & p, cmd_meta const & meta):
|
||||
m_p(p), m_env(p.env()), m_meta_info(meta), m_ctx(p.env()) {
|
||||
m_u_meta = m_ctx.mk_univ_metavar_decl();
|
||||
check_attrs(m_attrs);
|
||||
m_doc_string = p.get_doc_string();
|
||||
check_attrs(m_meta_info.m_attrs);
|
||||
check_modifiers();
|
||||
}
|
||||
|
||||
void post_process(buffer<expr> const & new_params, buffer<expr> const & new_inds, buffer<buffer<expr> > const & new_intro_rules) {
|
||||
add_aliases(new_params, new_inds, new_intro_rules);
|
||||
add_namespaces(new_inds);
|
||||
for (expr const & ind : new_inds) {
|
||||
m_env = m_attrs.apply(m_env, m_p.ios(), mlocal_name(ind));
|
||||
m_env = m_meta_info.m_attrs.apply(m_env, m_p.ios(), mlocal_name(ind));
|
||||
/* TODO(Leo): add support for doc-strings in mutual inductive definitions.
|
||||
We are currently using the same doc string for all elements.
|
||||
*/
|
||||
if (m_doc_string)
|
||||
m_env = add_doc_string(m_env, mlocal_name(ind), *m_doc_string);
|
||||
if (m_meta_info.m_doc_string)
|
||||
m_env = add_doc_string(m_env, mlocal_name(ind), *m_meta_info.m_doc_string);
|
||||
}
|
||||
if (!m_mut_attrs.empty()) {
|
||||
lean_assert(new_inds.size() == m_mut_attrs.size());
|
||||
|
|
@ -668,7 +668,17 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
environment shared_inductive_cmd(buffer<expr> const & params, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules) {
|
||||
environment inductive_cmd() {
|
||||
buffer<expr> params;
|
||||
buffer<expr> inds;
|
||||
buffer<buffer<expr> > intro_rules;
|
||||
if (m_meta_info.m_modifiers.m_is_mutual) {
|
||||
parse_mutual_inductive(params, inds, intro_rules);
|
||||
} else {
|
||||
intro_rules.emplace_back();
|
||||
inds.push_back(parse_inductive(params, intro_rules.back()));
|
||||
}
|
||||
|
||||
buffer<expr> new_params;
|
||||
buffer<expr> new_inds;
|
||||
buffer<buffer<expr> > new_intro_rules;
|
||||
|
|
@ -677,31 +687,21 @@ public:
|
|||
}
|
||||
elaborate_inductive_decls(params, inds, intro_rules, new_params, new_inds, new_intro_rules);
|
||||
m_env = add_inductive_declaration(m_p.env(), m_p.get_options(), m_implicit_infer_map, m_lp_names, new_params,
|
||||
new_inds, new_intro_rules, m_is_trusted);
|
||||
new_inds, new_intro_rules, !m_meta_info.m_modifiers.m_is_meta);
|
||||
post_process(new_params, new_inds, new_intro_rules);
|
||||
return m_env;
|
||||
}
|
||||
|
||||
environment inductive_cmd() {
|
||||
environment coinductive_cmd() {
|
||||
buffer<expr> params;
|
||||
buffer<expr> inds;
|
||||
buffer<buffer<expr> > intro_rules;
|
||||
intro_rules.emplace_back();
|
||||
inds.push_back(parse_inductive(params, intro_rules.back()));
|
||||
return shared_inductive_cmd(params, inds, intro_rules);
|
||||
}
|
||||
|
||||
environment mutual_inductive_cmd() {
|
||||
buffer<expr> params;
|
||||
buffer<expr> inds;
|
||||
buffer<buffer<expr> > intro_rules;
|
||||
parse_mutual_inductive(params, inds, intro_rules);
|
||||
return shared_inductive_cmd(params, inds, intro_rules);
|
||||
}
|
||||
|
||||
environment shared_coinductive_cmd(buffer<expr> const & params,
|
||||
buffer<expr> const & inds,
|
||||
buffer<buffer<expr> > const & intro_rules) {
|
||||
if (m_meta_info.m_modifiers.m_is_mutual) {
|
||||
parse_mutual_inductive(params, inds, intro_rules);
|
||||
} else {
|
||||
intro_rules.emplace_back();
|
||||
inds.push_back(parse_inductive(params, intro_rules.back()));
|
||||
}
|
||||
buffer<expr> new_params;
|
||||
buffer<expr> new_inds;
|
||||
buffer<buffer<expr> > new_intro_rules;
|
||||
|
|
@ -734,59 +734,20 @@ public:
|
|||
|
||||
throw generic_exception(first_ind, "coinduction command failed");
|
||||
}
|
||||
|
||||
environment coinductive_cmd() {
|
||||
buffer<expr> params;
|
||||
buffer<expr> inds;
|
||||
buffer<buffer<expr> > intro_rules;
|
||||
intro_rules.emplace_back();
|
||||
inds.push_back(parse_inductive(params, intro_rules.back()));
|
||||
return shared_coinductive_cmd(params, inds, intro_rules);
|
||||
}
|
||||
|
||||
environment mutual_coinductive_cmd() {
|
||||
buffer<expr> params;
|
||||
buffer<expr> inds;
|
||||
buffer<buffer<expr> > intro_rules;
|
||||
parse_mutual_inductive(params, inds, intro_rules);
|
||||
return shared_coinductive_cmd(params, inds, intro_rules);
|
||||
}
|
||||
};
|
||||
|
||||
environment inductive_cmd_ex(parser & p, decl_attributes const & attrs, bool is_meta) {
|
||||
environment inductive_cmd(parser & p, cmd_meta const & meta) {
|
||||
p.next();
|
||||
auto pos = p.pos();
|
||||
module::scope_pos_info scope_pos(pos);
|
||||
return inductive_cmd_fn(p, attrs, !is_meta).inductive_cmd();
|
||||
return inductive_cmd_fn(p, meta).inductive_cmd();
|
||||
}
|
||||
|
||||
environment mutual_inductive_cmd_ex(parser & p, decl_attributes const & attrs, bool is_meta) {
|
||||
environment coinductive_cmd(parser & p, cmd_meta const & meta) {
|
||||
p.next();
|
||||
auto pos = p.pos();
|
||||
module::scope_pos_info scope_pos(pos);
|
||||
return inductive_cmd_fn(p, attrs, !is_meta).mutual_inductive_cmd();
|
||||
}
|
||||
|
||||
environment coinductive_cmd_ex(parser & p, decl_attributes const & attrs) {
|
||||
p.next();
|
||||
auto pos = p.pos();
|
||||
module::scope_pos_info scope_pos(pos);
|
||||
return inductive_cmd_fn(p, attrs, true).coinductive_cmd();
|
||||
}
|
||||
|
||||
environment mutual_coinductive_cmd_ex(parser & p, decl_attributes const & attrs) {
|
||||
p.next();
|
||||
auto pos = p.pos();
|
||||
module::scope_pos_info scope_pos(pos);
|
||||
return inductive_cmd_fn(p, attrs, true).mutual_coinductive_cmd();
|
||||
}
|
||||
|
||||
environment inductive_cmd(parser & p) {
|
||||
return inductive_cmd_ex(p, {}, false);
|
||||
}
|
||||
|
||||
environment coinductive_cmd(parser & p) {
|
||||
return coinductive_cmd_ex(p, {});
|
||||
return inductive_cmd_fn(p, meta).coinductive_cmd();
|
||||
}
|
||||
|
||||
void register_inductive_cmds(cmd_table & r) {
|
||||
|
|
|
|||
|
|
@ -8,10 +8,8 @@ Author: Daniel Selsam
|
|||
#include "frontends/lean/cmd_table.h"
|
||||
#include "frontends/lean/decl_attributes.h"
|
||||
namespace lean {
|
||||
environment inductive_cmd_ex(parser & p, decl_attributes const & attrs, bool is_meta);
|
||||
environment mutual_inductive_cmd_ex(parser & p, decl_attributes const & attrs, bool is_meta);
|
||||
environment coinductive_cmd_ex(parser & p, decl_attributes const & attrs);
|
||||
environment mutual_coinductive_cmd_ex(parser & p, decl_attributes const & attrs);
|
||||
environment inductive_cmd(parser & p, cmd_meta const & meta);
|
||||
environment coinductive_cmd(parser & p, cmd_meta const & meta);
|
||||
|
||||
void register_inductive_cmds(cmd_table & r);
|
||||
void initialize_inductive_cmds();
|
||||
|
|
|
|||
|
|
@ -2270,22 +2270,15 @@ public:
|
|||
virtual optional<expr> is_stuck(expr const & e) override { return ctx().is_stuck(e); }
|
||||
};
|
||||
|
||||
static name_set * g_documentable_cmds = nullptr;
|
||||
|
||||
static bool support_docummentation(name const & n) {
|
||||
return g_documentable_cmds->contains(n);
|
||||
}
|
||||
|
||||
void parser::parse_command() {
|
||||
lean_assert(curr() == token_kind::CommandKeyword);
|
||||
void parser::parse_command(cmd_meta const & meta) {
|
||||
if (curr() != token_kind::CommandKeyword) {
|
||||
auto p = pos();
|
||||
maybe_throw_error({"expected command", p});
|
||||
return;
|
||||
}
|
||||
m_last_cmd_pos = pos();
|
||||
name cmd_name = get_token_info().value();
|
||||
m_cmd_token = get_token_info().token();
|
||||
if (m_doc_string && !support_docummentation(cmd_name)) {
|
||||
next();
|
||||
reset_doc_string();
|
||||
maybe_throw_error({sstream() << "command '" << cmd_name << "' does not support doc string", m_last_cmd_pos});
|
||||
}
|
||||
if (auto it = cmds().find(cmd_name)) {
|
||||
lazy_type_context tc(m_env, get_options());
|
||||
scope_global_ios scope1(m_ios);
|
||||
|
|
@ -2295,24 +2288,23 @@ void parser::parse_command() {
|
|||
in_notation_ctx ctx(*this);
|
||||
if (it->get_skip_token())
|
||||
next();
|
||||
m_env = it->get_fn()(*this);
|
||||
m_env = it->get_fn()(*this, meta);
|
||||
} else {
|
||||
if (it->get_skip_token())
|
||||
next();
|
||||
m_env = it->get_fn()(*this);
|
||||
m_env = it->get_fn()(*this, meta);
|
||||
}
|
||||
} else {
|
||||
reset_doc_string();
|
||||
auto p = pos();
|
||||
next();
|
||||
maybe_throw_error({sstream() << "unknown command '" << cmd_name << "'", p});
|
||||
}
|
||||
reset_doc_string();
|
||||
}
|
||||
|
||||
void parser::parse_doc_block() {
|
||||
m_doc_string = m_scanner.get_str_val();
|
||||
std::string parser::parse_doc_block() {
|
||||
auto val = m_scanner.get_str_val();
|
||||
next();
|
||||
return val;
|
||||
}
|
||||
|
||||
void parser::parse_mod_doc_block() {
|
||||
|
|
@ -2320,19 +2312,6 @@ void parser::parse_mod_doc_block() {
|
|||
next();
|
||||
}
|
||||
|
||||
void parser::check_no_doc_string() {
|
||||
if (m_doc_string) {
|
||||
auto p = pos();
|
||||
next();
|
||||
reset_doc_string();
|
||||
maybe_throw_error({"invalid occurrence of doc string immediately before current position", p});
|
||||
}
|
||||
}
|
||||
|
||||
void parser::reset_doc_string() {
|
||||
m_doc_string = optional<std::string>();
|
||||
}
|
||||
|
||||
#if defined(__GNUC__) && !defined(__CLANG__)
|
||||
#pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
|
||||
#endif
|
||||
|
|
@ -2494,29 +2473,22 @@ bool parser::parse_command_like() {
|
|||
|
||||
switch (curr()) {
|
||||
case token_kind::CommandKeyword:
|
||||
if (curr_is_token(get_end_tk())) {
|
||||
check_no_doc_string();
|
||||
}
|
||||
parse_command();
|
||||
parse_command({});
|
||||
updt_options();
|
||||
break;
|
||||
case token_kind::DocBlock:
|
||||
check_no_doc_string();
|
||||
parse_doc_block();
|
||||
parse_command({{}, {}, some(parse_doc_block())});
|
||||
break;
|
||||
case token_kind::ModDocBlock:
|
||||
check_no_doc_string();
|
||||
parse_mod_doc_block();
|
||||
break;
|
||||
case token_kind::Eof:
|
||||
check_no_doc_string();
|
||||
if (has_open_scopes(m_env)) {
|
||||
maybe_throw_error({"invalid end of module, expecting 'end'", pos()});
|
||||
}
|
||||
return true;
|
||||
break;
|
||||
case token_kind::Keyword:
|
||||
check_no_doc_string();
|
||||
if (curr_is_token(get_period_tk())) {
|
||||
next();
|
||||
break;
|
||||
|
|
@ -2633,26 +2605,10 @@ void initialize_parser() {
|
|||
register_bool_option(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS,
|
||||
"(lean parser) display error messages in the regular output channel");
|
||||
g_tmp_prefix = new name(name::mk_internal_unique_name());
|
||||
g_documentable_cmds = new name_set();
|
||||
|
||||
g_documentable_cmds->insert("definition");
|
||||
g_documentable_cmds->insert("theorem");
|
||||
g_documentable_cmds->insert("constant");
|
||||
g_documentable_cmds->insert("axiom");
|
||||
g_documentable_cmds->insert("meta");
|
||||
g_documentable_cmds->insert("mutual");
|
||||
g_documentable_cmds->insert("@[");
|
||||
g_documentable_cmds->insert("protected");
|
||||
g_documentable_cmds->insert("class");
|
||||
g_documentable_cmds->insert("instance");
|
||||
g_documentable_cmds->insert("inductive");
|
||||
g_documentable_cmds->insert("coinductive");
|
||||
g_documentable_cmds->insert("structure");
|
||||
}
|
||||
|
||||
void finalize_parser() {
|
||||
delete g_tmp_prefix;
|
||||
delete g_parser_show_errors;
|
||||
delete g_documentable_cmds;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -26,6 +26,7 @@ Author: Leonardo de Moura
|
|||
#include "frontends/lean/local_level_decls.h"
|
||||
#include "frontends/lean/parser_config.h"
|
||||
#include "frontends/lean/local_context_adapter.h"
|
||||
#include "frontends/lean/decl_util.h"
|
||||
|
||||
namespace lean {
|
||||
struct interrupt_parser {};
|
||||
|
|
@ -83,9 +84,6 @@ class parser : public abstract_parser {
|
|||
// noncomputable definitions not tagged as noncomputable.
|
||||
bool m_ignore_noncomputable;
|
||||
|
||||
// Docgen
|
||||
optional<std::string> m_doc_string;
|
||||
|
||||
void sync_command();
|
||||
|
||||
tag get_tag(expr e);
|
||||
|
|
@ -96,13 +94,10 @@ class parser : public abstract_parser {
|
|||
level parse_level_nud();
|
||||
level parse_level_led(level left);
|
||||
|
||||
void parse_doc_block();
|
||||
std::string parse_doc_block();
|
||||
void parse_mod_doc_block();
|
||||
void check_no_doc_string();
|
||||
void reset_doc_string();
|
||||
|
||||
void process_imports();
|
||||
void parse_command();
|
||||
bool parse_command_like();
|
||||
void process_postponed(buffer<expr> const & args, bool is_left, buffer<notation::action_kind> const & kinds,
|
||||
buffer<list<expr>> const & nargs, buffer<expr> const & ps, buffer<pair<unsigned, pos_info>> const & scoped_info,
|
||||
|
|
@ -242,8 +237,6 @@ public:
|
|||
pos_info cmd_pos() const { return m_last_cmd_pos; }
|
||||
name const & get_cmd_token() const { return m_cmd_token; }
|
||||
|
||||
optional<std::string> get_doc_string() const { return m_doc_string; }
|
||||
|
||||
parser_pos_provider get_parser_pos_provider(pos_info const & some_pos) const {
|
||||
return parser_pos_provider(m_pos_table, m_file_name, some_pos, m_next_tag_idx);
|
||||
}
|
||||
|
|
@ -413,6 +406,7 @@ public:
|
|||
expr parse_scoped_expr(buffer<expr> const & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
|
||||
expr parse_expr_with_env(local_environment const & lenv, unsigned rbp = 0);
|
||||
|
||||
void parse_command(cmd_meta const & meta);
|
||||
void parse_imports(unsigned & fingerprint, std::vector<module_name> &);
|
||||
|
||||
struct local_scope {
|
||||
|
|
|
|||
|
|
@ -256,16 +256,14 @@ struct structure_cmd_fn {
|
|||
};
|
||||
|
||||
parser & m_p;
|
||||
decl_modifiers m_modifiers;
|
||||
cmd_meta m_meta_info;
|
||||
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;
|
||||
|
|
@ -286,31 +284,24 @@ struct structure_cmd_fn {
|
|||
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):
|
||||
structure_cmd_fn(parser & p, cmd_meta const & meta):
|
||||
m_p(p),
|
||||
m_modifiers(modifiers),
|
||||
m_meta_info(meta),
|
||||
m_env(p.env()),
|
||||
m_ctx(p.env()),
|
||||
m_namespace(get_namespace(m_env)),
|
||||
m_attrs(attrs) {
|
||||
m_namespace(get_namespace(m_env)) {
|
||||
m_explicit_universe_params = false;
|
||||
m_infer_result_universe = false;
|
||||
m_inductive_predicate = false;
|
||||
m_subobjects = !p.get_options().get_bool("old_structure_cmd", 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);
|
||||
if (!meta.m_attrs.ok_for_inductive_type())
|
||||
throw exception("only attribute [class] accepted for structures");
|
||||
}
|
||||
|
||||
/** \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;
|
||||
|
|
@ -319,7 +310,7 @@ struct structure_cmd_fn {
|
|||
m_explicit_universe_params = false;
|
||||
}
|
||||
m_given_name = m_p.check_decl_id_next("invalid 'structure', identifier expected");
|
||||
if (m_modifiers.m_is_private) {
|
||||
if (m_meta_info.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;
|
||||
|
|
@ -1017,7 +1008,7 @@ struct structure_cmd_fn {
|
|||
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) {
|
||||
if (m_meta_info.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 {
|
||||
|
|
@ -1033,7 +1024,7 @@ struct structure_cmd_fn {
|
|||
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;
|
||||
bool is_trusted = !m_meta_info.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);
|
||||
|
|
@ -1041,7 +1032,7 @@ struct structure_cmd_fn {
|
|||
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 = m_meta_info.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_no_params()),
|
||||
|
|
@ -1052,7 +1043,7 @@ struct structure_cmd_fn {
|
|||
buffer<name> proj_names = get_structure_fields(m_env, m_name);
|
||||
for (auto & n : proj_names)
|
||||
n = m_name + n;
|
||||
m_env = mk_projections(m_env, m_name, proj_names, m_mk_infer, m_attrs.has_class());
|
||||
m_env = mk_projections(m_env, m_name, proj_names, m_mk_infer, m_meta_info.m_attrs.has_class());
|
||||
for (auto const & n : proj_names)
|
||||
add_alias(n);
|
||||
}
|
||||
|
|
@ -1101,7 +1092,8 @@ struct structure_cmd_fn {
|
|||
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 = mk_simple_equation_lemma_for(m_env, m_p.get_options(), m_modifiers.m_is_private, decl_name, args.size());
|
||||
m_env = mk_simple_equation_lemma_for(m_env, m_p.get_options(),
|
||||
m_meta_info.m_modifiers.m_is_private, decl_name, args.size());
|
||||
m_env = set_reducible(m_env, decl_name, reducible_status::Reducible, true);
|
||||
}
|
||||
}
|
||||
|
|
@ -1173,7 +1165,7 @@ struct structure_cmd_fn {
|
|||
name const & parent_name = const_name(parent_fn);
|
||||
if (m_subobjects) {
|
||||
if (!m_private_parents[i]) {
|
||||
if (m_attrs.has_class() && is_class(m_env, parent_name)) {
|
||||
if (m_meta_info.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, m_name + m_fields[i].get_name(), m_prio, true);
|
||||
}
|
||||
|
|
@ -1191,7 +1183,7 @@ struct structure_cmd_fn {
|
|||
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())
|
||||
if (m_meta_info.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);;
|
||||
|
|
@ -1210,7 +1202,7 @@ struct structure_cmd_fn {
|
|||
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 (m_meta_info.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);
|
||||
}
|
||||
|
|
@ -1241,8 +1233,8 @@ struct structure_cmd_fn {
|
|||
}
|
||||
|
||||
void add_doc_string() {
|
||||
if (m_doc_string)
|
||||
m_env = ::lean::add_doc_string(m_env, m_name, *m_doc_string);
|
||||
if (m_meta_info.m_doc_string)
|
||||
m_env = ::lean::add_doc_string(m_env, m_name, *m_meta_info.m_doc_string);
|
||||
}
|
||||
|
||||
environment operator()() {
|
||||
|
|
@ -1288,29 +1280,23 @@ struct structure_cmd_fn {
|
|||
}
|
||||
};
|
||||
|
||||
environment structure_cmd_ex(parser & p, decl_attributes const & attrs, decl_modifiers const & modifiers) {
|
||||
environment structure_cmd(parser & p, cmd_meta const & meta) {
|
||||
p.next();
|
||||
return structure_cmd_fn(p, attrs, modifiers)();
|
||||
return structure_cmd_fn(p, meta)();
|
||||
}
|
||||
|
||||
environment structure_cmd(parser & p) {
|
||||
return structure_cmd_ex(p, {}, {});
|
||||
}
|
||||
|
||||
environment class_cmd_ex(parser & p, decl_attributes attrs, decl_modifiers const & modifiers) {
|
||||
attrs.set_attribute(p.env(), "class");
|
||||
environment class_cmd(parser & p, cmd_meta const & _meta) {
|
||||
auto meta = _meta;
|
||||
meta.m_attrs.set_persistent(true);
|
||||
meta.m_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);
|
||||
return inductive_cmd(p, meta);
|
||||
} else {
|
||||
return structure_cmd_fn(p, attrs, modifiers)();
|
||||
return structure_cmd_fn(p, meta)();
|
||||
}
|
||||
}
|
||||
|
||||
environment class_cmd(parser & p) {
|
||||
return class_cmd_ex(p, {}, {});
|
||||
}
|
||||
|
||||
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));
|
||||
|
|
|
|||
|
|
@ -9,8 +9,8 @@ Author: Leonardo de Moura
|
|||
#include "frontends/lean/decl_util.h"
|
||||
#include "frontends/lean/cmd_table.h"
|
||||
namespace lean {
|
||||
environment structure_cmd_ex(parser & p, decl_attributes const & attrs, decl_modifiers const & modifiers);
|
||||
environment class_cmd_ex(parser & p, decl_attributes attrs, decl_modifiers const & modifiers);
|
||||
environment structure_cmd(parser & p, cmd_meta const & meta);
|
||||
environment class_cmd(parser & p, cmd_meta const & meta);
|
||||
buffer<name> get_structure_fields(environment const & env, name const & S);
|
||||
void register_structure_cmd(cmd_table & r);
|
||||
/** \brief Return true iff \c S is a structure created with the structure command */
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
bad_unification_hint.lean:7:0: error: invalid unification hint, failed to unify pattern after unifying constraints
|
||||
bad_unification_hint.lean:7:0: warning: declaration 'append_cons_hint' uses sorry
|
||||
bad_unification_hint.lean:12:0: error: invalid unification hint, failed to unify constraint #1
|
||||
bad_unification_hint.lean:12:0: warning: declaration 'cons_append_hint'' uses sorry
|
||||
bad_unification_hint.lean:7:9: error: invalid unification hint, failed to unify pattern after unifying constraints
|
||||
bad_unification_hint.lean:7:9: warning: declaration 'append_cons_hint' uses sorry
|
||||
bad_unification_hint.lean:12:9: error: invalid unification hint, failed to unify constraint #1
|
||||
bad_unification_hint.lean:12:9: warning: declaration 'cons_append_hint'' uses sorry
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
--
|
||||
universe variables u
|
||||
inductive [class] H (A : Type u)
|
||||
class inductive H (A : Type u)
|
||||
| mk : A → H
|
||||
|
||||
definition foo {A : Type u} [h : H A] : A :=
|
||||
|
|
|
|||
20
tests/lean/cmd_meta_errors.lean
Normal file
20
tests/lean/cmd_meta_errors.lean
Normal file
|
|
@ -0,0 +1,20 @@
|
|||
/-- docs -/
|
||||
run_cmd
|
||||
|
||||
@[class]
|
||||
run_cmd
|
||||
|
||||
private run_cmd
|
||||
|
||||
meta axiom
|
||||
|
||||
private protected def f := 42
|
||||
private private def f := 42
|
||||
|
||||
private inductive
|
||||
protected inductive
|
||||
noncomputable inductive
|
||||
|
||||
private instance
|
||||
protected instance
|
||||
mutual instance
|
||||
12
tests/lean/cmd_meta_errors.lean.expected.out
Normal file
12
tests/lean/cmd_meta_errors.lean.expected.out
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
cmd_meta_errors.lean:2:0: error: command does not accept doc string
|
||||
cmd_meta_errors.lean:5:0: error: command does not accept attributes
|
||||
cmd_meta_errors.lean:7:8: error: command does not accept modifiers
|
||||
cmd_meta_errors.lean:9:5: error: invalid 'meta' modifier for axiom
|
||||
cmd_meta_errors.lean:11:8: error: unexpected definition modifier
|
||||
cmd_meta_errors.lean:12:8: error: unexpected definition modifier
|
||||
cmd_meta_errors.lean:14:0: error: invalid 'private' modifier for inductive type
|
||||
cmd_meta_errors.lean:15:0: error: invalid 'protected' modifier for inductive type
|
||||
cmd_meta_errors.lean:16:0: error: invalid 'noncomputable' modifier for inductive type
|
||||
cmd_meta_errors.lean:18:8: error: invalid 'private' modifier for instance command
|
||||
cmd_meta_errors.lean:19:10: error: invalid 'protected' modifier for instance command
|
||||
cmd_meta_errors.lean:20:7: error: invalid 'mutual' modifier for instance command
|
||||
|
|
@ -8,7 +8,7 @@ but is expected to have type
|
|||
?m_1 → ?m_2 → ?m_4
|
||||
Additional information:
|
||||
elab_error_msgs.lean:2:0: context: 'eliminator' elaboration was not used for 'and.rec' because it is not fully applied, #2 explicit arguments expected
|
||||
elab_error_msgs.lean:4:0: warning: declaration 'bogus_elim' uses sorry
|
||||
elab_error_msgs.lean:5:0: warning: declaration 'bogus_elim' uses sorry
|
||||
elab_error_msgs.lean:9:0: error: type mismatch at application
|
||||
bogus_elim trivial
|
||||
term
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
hole_issue2.lean:12:0: warning: declaration 'count' uses sorry
|
||||
hole_issue2.lean:12:14: warning: declaration 'count' uses sorry
|
||||
hole_issue2.lean:22:74: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
A : Type,
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
set_option pp.notation false
|
||||
|
||||
inductive [class] C (A : Type*)
|
||||
class inductive C (A : Type*)
|
||||
| mk : A → C
|
||||
|
||||
definition val {A : Type*} (c : C A) : A :=
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
inductive [class] C {A : Type} : A → Prop
|
||||
class inductive C {A : Type} : A → Prop
|
||||
|
||||
constant f {A : Type} (a : A) [H : C a] : Prop
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
structure [class] is_equiv {A B : Type} (f : A → B) :=
|
||||
class is_equiv {A B : Type} (f : A → B) :=
|
||||
(inv : B → A)
|
||||
|
||||
#check @is_equiv.inv
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
open nat
|
||||
|
||||
structure [class] A := (n : ℕ)
|
||||
class A := (n : ℕ)
|
||||
|
||||
definition f [A] := A.n
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
open nat
|
||||
|
||||
structure [class] foo :=
|
||||
class foo :=
|
||||
(a : nat) (b : nat)
|
||||
|
||||
attribute [instance, priority std.priority.default-2]
|
||||
|
|
|
|||
|
|
@ -4,12 +4,12 @@ set_option old_structure_cmd true
|
|||
|
||||
#print "======================="
|
||||
|
||||
structure [class] has_two_muls (A : Type) extends has_mul A renaming mul→mul1,
|
||||
private has_mul A renaming mul→mul2
|
||||
class has_two_muls (A : Type) extends has_mul A renaming mul→mul1,
|
||||
private has_mul A renaming mul→mul2
|
||||
|
||||
#print prefix has_two_muls
|
||||
|
||||
#print "======================="
|
||||
|
||||
structure [class] another_two_muls (A : Type) extends has_mul A renaming mul→mul1,
|
||||
has_mul A renaming mul→mul2
|
||||
class another_two_muls (A : Type) extends has_mul A renaming mul→mul1,
|
||||
has_mul A renaming mul→mul2
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ section foo
|
|||
|
||||
#check foo
|
||||
|
||||
structure [class] point :=
|
||||
class point :=
|
||||
(x : A) (y : A)
|
||||
end foo
|
||||
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
namespace foo
|
||||
|
||||
structure [class] structA :=
|
||||
class structA :=
|
||||
mk :: (a : nat)
|
||||
|
||||
structure [class] structB extends structA :=
|
||||
class structB extends structA :=
|
||||
mk :: (b : nat)
|
||||
|
||||
#check @structA.a
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ namespace nsimp
|
|||
-- set_option pp.implicit true
|
||||
|
||||
-- first define a class of homogeneous equality
|
||||
inductive [class] simplifies_to {T : Type} (t1 t2 : T) : Prop
|
||||
class inductive simplifies_to {T : Type} (t1 t2 : T) : Prop
|
||||
| mk : t1 = t2 → simplifies_to
|
||||
|
||||
theorem get_eq {T : Type} {t1 t2 : T} (C : simplifies_to t1 t2) : t1 = t2 :=
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
open nat
|
||||
|
||||
-- first define a class of homogeneous equality
|
||||
inductive [class] simplifies_to {T : Type} (t1 t2 : T) : Prop
|
||||
class inductive simplifies_to {T : Type} (t1 t2 : T) : Prop
|
||||
| mk : t1 = t2 → simplifies_to
|
||||
|
||||
namespace simplifies_to
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
prelude
|
||||
import init.core
|
||||
|
||||
structure [class] point (A : Type*) (B : Type*) :=
|
||||
class point (A : Type*) (B : Type*) :=
|
||||
mk :: (x : A) (y : B)
|
||||
|
||||
#print classes
|
||||
|
|
|
|||
|
|
@ -7,11 +7,11 @@ eq.refl
|
|||
@[foo, foo.baz, refl]
|
||||
constructor eq.refl : ∀ {α : Sort u} (a : α), a = a
|
||||
[eq.refl]
|
||||
user_attribute.lean:22:0: error: an attribute named [reducible] has already been registered
|
||||
user_attribute.lean:22:0: warning: declaration 'duplicate' uses sorry
|
||||
user_attribute.lean:27:0: error: invalid [user_attribute], must be applied to definition of type user_attribute
|
||||
user_attribute.lean:23:0: error: an attribute named [reducible] has already been registered
|
||||
user_attribute.lean:23:0: warning: declaration 'duplicate' uses sorry
|
||||
user_attribute.lean:28:0: error: invalid [user_attribute], must be applied to definition of type user_attribute
|
||||
user_attribute.lean:28:11: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
⊢ Sort ?
|
||||
user_attribute.lean:33:2: error: invalid [user_attribute], must be applied to definition of type user_attribute
|
||||
user_attribute.lean:33:2: warning: declaration 'baz_attr' uses sorry
|
||||
user_attribute.lean:34:2: error: invalid [user_attribute], must be applied to definition of type user_attribute
|
||||
user_attribute.lean:34:2: warning: declaration 'baz_attr' uses sorry
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
2
|
||||
0 + (1 + 0) + (1 + 1) + (1 + 2) + (1 + 3) + (1 + 4) + (1 + 5) + (1 + 6) + (1 + 7) + (1 + 8) + (1 + 9) : ℕ
|
||||
user_notation.lean:21:0: error: invalid user-defined notation, must start with `interactive.parse (lean.parser.tk c)` parameter, optionally preceded by `interactive.parse lean.parser.pexpr` parameter
|
||||
user_notation.lean:22:5: error: invalid user-defined notation, must start with `interactive.parse (lean.parser.tk c)` parameter, optionally preceded by `interactive.parse lean.parser.pexpr` parameter
|
||||
user_notation.lean:22:9: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
e₁ : parse lean.parser.pexpr
|
||||
⊢ Sort ?
|
||||
user_notation.lean:24:0: error: invalid user-defined notation, must return type `lean.parser p`
|
||||
user_notation.lean:25:5: error: invalid user-defined notation, must return type `lean.parser p`
|
||||
user_notation.lean:25:9: error: don't know how to synthesize placeholder
|
||||
context:
|
||||
e₁ : parse (tk "(")
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue