2014-06-18 17:36:21 +00:00
|
|
|
/*
|
|
|
|
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 <algorithm>
|
|
|
|
#include "util/sstream.h"
|
|
|
|
#include "kernel/type_checker.h"
|
2014-07-14 04:41:44 +00:00
|
|
|
#include "kernel/abstract.h"
|
2014-06-18 17:36:21 +00:00
|
|
|
#include "library/scoped_ext.h"
|
|
|
|
#include "library/aliases.h"
|
|
|
|
#include "library/private.h"
|
2014-09-03 22:01:13 +00:00
|
|
|
#include "library/protected.h"
|
2014-06-25 15:39:14 +00:00
|
|
|
#include "library/placeholder.h"
|
2014-06-18 17:36:21 +00:00
|
|
|
#include "library/locals.h"
|
2014-06-25 15:30:09 +00:00
|
|
|
#include "library/explicit.h"
|
2014-09-19 20:30:08 +00:00
|
|
|
#include "library/reducible.h"
|
2014-07-08 00:48:20 +00:00
|
|
|
#include "library/coercion.h"
|
2014-06-18 17:36:21 +00:00
|
|
|
#include "frontends/lean/parser.h"
|
|
|
|
#include "frontends/lean/util.h"
|
2014-07-04 21:25:44 +00:00
|
|
|
#include "frontends/lean/class.h"
|
2014-09-23 17:00:36 +00:00
|
|
|
#include "frontends/lean/tokens.h"
|
2014-06-18 17:36:21 +00:00
|
|
|
|
|
|
|
namespace lean {
|
|
|
|
environment universe_cmd(parser & p) {
|
|
|
|
name n = p.check_id_next("invalid universe declaration, identifier expected");
|
|
|
|
environment env = p.env();
|
2014-08-23 22:44:28 +00:00
|
|
|
if (in_section_or_context(env)) {
|
2014-06-18 17:36:21 +00:00
|
|
|
p.add_local_level(n, mk_param_univ(n));
|
|
|
|
} else {
|
|
|
|
name const & ns = get_namespace(env);
|
|
|
|
name full_n = ns + n;
|
|
|
|
env = module::add_universe(env, full_n);
|
|
|
|
if (!ns.is_anonymous())
|
2014-07-28 04:01:59 +00:00
|
|
|
env = add_level_alias(env, n, full_n);
|
2014-06-18 17:36:21 +00:00
|
|
|
}
|
|
|
|
return env;
|
|
|
|
}
|
|
|
|
|
2014-06-18 20:55:48 +00:00
|
|
|
bool parse_univ_params(parser & p, buffer<name> & ps) {
|
2014-09-23 17:00:36 +00:00
|
|
|
if (p.curr_is_token(get_llevel_curly_tk())) {
|
2014-06-18 17:36:21 +00:00
|
|
|
p.next();
|
2014-09-23 17:00:36 +00:00
|
|
|
while (!p.curr_is_token(get_rcurly_tk())) {
|
2014-06-18 17:36:21 +00:00
|
|
|
name l = p.check_id_next("invalid universe parameter, identifier expected");
|
|
|
|
p.add_local_level(l, mk_param_univ(l));
|
|
|
|
ps.push_back(l);
|
|
|
|
}
|
|
|
|
p.next();
|
2014-06-18 20:55:48 +00:00
|
|
|
return true;
|
|
|
|
} else{
|
|
|
|
return false;
|
2014-06-18 17:36:21 +00:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2014-06-18 20:55:48 +00:00
|
|
|
void update_univ_parameters(buffer<name> & ls_buffer, name_set const & found, parser const & p) {
|
2014-06-18 17:36:21 +00:00
|
|
|
unsigned old_sz = ls_buffer.size();
|
|
|
|
found.for_each([&](name const & n) {
|
|
|
|
if (std::find(ls_buffer.begin(), ls_buffer.begin() + old_sz, n) == ls_buffer.begin() + old_sz)
|
|
|
|
ls_buffer.push_back(n);
|
|
|
|
});
|
|
|
|
std::sort(ls_buffer.begin(), ls_buffer.end(), [&](name const & n1, name const & n2) {
|
|
|
|
return p.get_local_level_index(n1) < p.get_local_level_index(n2);
|
|
|
|
});
|
|
|
|
}
|
|
|
|
|
|
|
|
static environment declare_var(parser & p, environment env,
|
|
|
|
name const & n, level_param_names const & ls, expr const & type,
|
2014-06-30 23:52:20 +00:00
|
|
|
bool is_axiom, optional<binder_info> const & _bi, pos_info const & pos) {
|
|
|
|
binder_info bi;
|
|
|
|
if (_bi) bi = *_bi;
|
2014-08-23 22:44:28 +00:00
|
|
|
if (in_section_or_context(p.env())) {
|
2014-09-11 23:37:23 +00:00
|
|
|
name u = p.mk_fresh_name();
|
|
|
|
expr l = p.save_pos(mk_local(u, n, type, bi), pos);
|
|
|
|
p.add_local_expr(n, l);
|
2014-06-18 17:36:21 +00:00
|
|
|
return env;
|
|
|
|
} else {
|
|
|
|
name const & ns = get_namespace(env);
|
|
|
|
name full_n = ns + n;
|
2014-08-23 19:39:59 +00:00
|
|
|
if (is_axiom) {
|
2014-06-18 17:36:21 +00:00
|
|
|
env = module::add(env, check(env, mk_axiom(full_n, ls, type)));
|
2014-09-23 17:00:36 +00:00
|
|
|
p.add_decl_index(full_n, pos, get_axiom_tk(), type);
|
2014-08-23 19:39:59 +00:00
|
|
|
} else {
|
2014-06-18 17:36:21 +00:00
|
|
|
env = module::add(env, check(env, mk_var_decl(full_n, ls, type)));
|
2014-09-23 17:00:36 +00:00
|
|
|
p.add_decl_index(full_n, pos, get_variable_tk(), type);
|
2014-08-23 19:39:59 +00:00
|
|
|
}
|
2014-06-18 17:36:21 +00:00
|
|
|
if (!ns.is_anonymous())
|
2014-07-28 04:01:59 +00:00
|
|
|
env = add_expr_alias(env, n, full_n);
|
2014-06-18 17:36:21 +00:00
|
|
|
return env;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2014-07-06 23:46:34 +00:00
|
|
|
/** \brief If we are in a section, then add the new local levels to it. */
|
|
|
|
static void update_section_local_levels(parser & p, level_param_names const & new_ls) {
|
2014-08-23 22:44:28 +00:00
|
|
|
if (in_section_or_context(p.env())) {
|
2014-07-06 23:46:34 +00:00
|
|
|
for (auto const & l : new_ls)
|
|
|
|
p.add_local_level(l, mk_param_univ(l));
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2014-06-30 23:52:20 +00:00
|
|
|
optional<binder_info> parse_binder_info(parser & p) {
|
|
|
|
optional<binder_info> bi = p.parse_optional_binder_info();
|
|
|
|
if (bi)
|
2014-08-23 22:44:28 +00:00
|
|
|
check_in_section_or_context(p);
|
2014-06-30 23:52:20 +00:00
|
|
|
return bi;
|
|
|
|
}
|
|
|
|
|
2014-06-23 00:51:00 +00:00
|
|
|
environment variable_cmd_core(parser & p, bool is_axiom) {
|
2014-06-18 17:36:21 +00:00
|
|
|
auto pos = p.pos();
|
2014-06-30 23:52:20 +00:00
|
|
|
optional<binder_info> bi = parse_binder_info(p);
|
2014-06-18 17:36:21 +00:00
|
|
|
name n = p.check_id_next("invalid declaration, identifier expected");
|
|
|
|
buffer<name> ls_buffer;
|
2014-09-23 17:00:36 +00:00
|
|
|
if (p.curr_is_token(get_llevel_curly_tk()) && in_section_or_context(p.env()))
|
2014-06-18 17:36:21 +00:00
|
|
|
throw parser_error("invalid declaration, axioms/parameters occurring in sections cannot be universe polymorphic", p.pos());
|
|
|
|
optional<parser::local_scope> scope1;
|
2014-08-23 22:44:28 +00:00
|
|
|
if (!in_section_or_context(p.env()))
|
2014-06-18 17:36:21 +00:00
|
|
|
scope1.emplace(p);
|
|
|
|
parse_univ_params(p, ls_buffer);
|
|
|
|
expr type;
|
2014-09-23 17:00:36 +00:00
|
|
|
if (!p.curr_is_token(get_colon_tk())) {
|
2014-06-30 16:14:55 +00:00
|
|
|
buffer<expr> ps;
|
2014-06-18 17:36:21 +00:00
|
|
|
auto lenv = p.parse_binders(ps);
|
2014-09-23 17:00:36 +00:00
|
|
|
p.check_token_next(get_colon_tk(), "invalid declaration, ':' expected");
|
2014-06-18 17:36:21 +00:00
|
|
|
type = p.parse_scoped_expr(ps, lenv);
|
2014-07-14 04:41:44 +00:00
|
|
|
type = Pi(ps, type, p);
|
2014-06-18 17:36:21 +00:00
|
|
|
} else {
|
|
|
|
p.next();
|
|
|
|
type = p.parse_expr();
|
|
|
|
}
|
2014-06-30 23:52:20 +00:00
|
|
|
p.parse_close_binder_info(bi);
|
2014-06-18 17:36:21 +00:00
|
|
|
level_param_names ls;
|
2014-08-23 22:44:28 +00:00
|
|
|
if (in_section_or_context(p.env())) {
|
2014-06-18 17:36:21 +00:00
|
|
|
ls = to_level_param_names(collect_univ_params(type));
|
|
|
|
} else {
|
2014-06-18 20:55:48 +00:00
|
|
|
update_univ_parameters(ls_buffer, collect_univ_params(type), p);
|
2014-06-18 17:36:21 +00:00
|
|
|
ls = to_list(ls_buffer.begin(), ls_buffer.end());
|
|
|
|
}
|
2014-07-06 23:46:34 +00:00
|
|
|
level_param_names new_ls;
|
2014-07-14 04:04:01 +00:00
|
|
|
list<expr> ctx = locals_to_context(type, p);
|
|
|
|
std::tie(type, new_ls) = p.elaborate_type(type, ctx);
|
2014-07-06 23:46:34 +00:00
|
|
|
update_section_local_levels(p, new_ls);
|
|
|
|
return declare_var(p, p.env(), n, append(ls, new_ls), type, is_axiom, bi, pos);
|
2014-06-18 17:36:21 +00:00
|
|
|
}
|
|
|
|
environment variable_cmd(parser & p) {
|
2014-06-23 00:51:00 +00:00
|
|
|
return variable_cmd_core(p, false);
|
2014-06-18 17:36:21 +00:00
|
|
|
}
|
|
|
|
environment axiom_cmd(parser & p) {
|
2014-06-23 00:51:00 +00:00
|
|
|
return variable_cmd_core(p, true);
|
2014-06-18 17:36:21 +00:00
|
|
|
}
|
|
|
|
|
2014-07-04 21:25:44 +00:00
|
|
|
struct decl_modifiers {
|
2014-09-28 19:20:42 +00:00
|
|
|
bool m_is_instance;
|
|
|
|
bool m_is_coercion;
|
|
|
|
bool m_is_reducible;
|
|
|
|
optional<unsigned> m_priority;
|
|
|
|
decl_modifiers():m_priority() {
|
2014-09-03 22:01:13 +00:00
|
|
|
m_is_instance = false;
|
|
|
|
m_is_coercion = false;
|
2014-09-19 20:30:08 +00:00
|
|
|
m_is_reducible = false;
|
2014-07-04 21:25:44 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
void parse(parser & p) {
|
|
|
|
while (true) {
|
2014-09-28 19:20:42 +00:00
|
|
|
auto pos = p.pos();
|
2014-09-23 17:00:36 +00:00
|
|
|
if (p.curr_is_token(get_instance_tk())) {
|
2014-07-04 21:25:44 +00:00
|
|
|
m_is_instance = true;
|
|
|
|
p.next();
|
2014-09-23 17:00:36 +00:00
|
|
|
} else if (p.curr_is_token(get_coercion_tk())) {
|
2014-07-08 00:48:20 +00:00
|
|
|
m_is_coercion = true;
|
|
|
|
p.next();
|
2014-09-23 17:00:36 +00:00
|
|
|
} else if (p.curr_is_token(get_reducible_tk())) {
|
2014-09-19 20:30:08 +00:00
|
|
|
m_is_reducible = true;
|
|
|
|
p.next();
|
2014-09-28 19:20:42 +00:00
|
|
|
} else if (auto it = parse_instance_priority(p)) {
|
|
|
|
m_priority = *it;
|
|
|
|
if (!m_is_instance)
|
|
|
|
throw parser_error("invalid '[priority]' occurrence, declaration must be marked as an '[instance]'", pos);
|
2014-07-04 21:25:44 +00:00
|
|
|
} else {
|
|
|
|
break;
|
|
|
|
}
|
2014-06-18 17:36:21 +00:00
|
|
|
}
|
|
|
|
}
|
2014-07-04 21:25:44 +00:00
|
|
|
};
|
2014-06-18 17:36:21 +00:00
|
|
|
|
2014-08-18 00:03:54 +00:00
|
|
|
static void check_end_of_theorem(parser const & p) {
|
|
|
|
if (!p.curr_is_command_like())
|
|
|
|
throw parser_error("':=', '.', command, script, or end-of-file expected", p.pos());
|
|
|
|
}
|
|
|
|
|
2014-09-07 19:28:58 +00:00
|
|
|
static void erase_local_binder_info(buffer<expr> & ps) {
|
|
|
|
for (expr & p : ps)
|
|
|
|
p = update_local(p, binder_info());
|
|
|
|
}
|
|
|
|
|
2014-09-19 22:04:52 +00:00
|
|
|
environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, bool is_private, bool is_protected) {
|
|
|
|
lean_assert(!(is_theorem && !is_opaque));
|
|
|
|
lean_assert(!(is_private && is_protected));
|
2014-08-15 00:44:07 +00:00
|
|
|
auto n_pos = p.pos();
|
2014-08-17 19:14:42 +00:00
|
|
|
unsigned start_line = n_pos.first;
|
2014-08-15 00:44:07 +00:00
|
|
|
name n = p.check_id_next("invalid declaration, identifier expected");
|
2014-07-06 04:49:32 +00:00
|
|
|
decl_modifiers modifiers;
|
2014-06-18 17:36:21 +00:00
|
|
|
name real_n; // real name for this declaration
|
|
|
|
buffer<name> ls_buffer;
|
|
|
|
expr type, value;
|
|
|
|
level_param_names ls;
|
|
|
|
{
|
2014-07-06 04:49:32 +00:00
|
|
|
// Parse universe parameters
|
2014-06-18 17:36:21 +00:00
|
|
|
parser::local_scope scope1(p);
|
|
|
|
parse_univ_params(p, ls_buffer);
|
2014-07-06 04:49:32 +00:00
|
|
|
|
|
|
|
// Parse modifiers
|
|
|
|
modifiers.parse(p);
|
|
|
|
|
2014-09-23 17:00:36 +00:00
|
|
|
if (p.curr_is_token(get_assign_tk())) {
|
2014-06-25 15:39:14 +00:00
|
|
|
auto pos = p.pos();
|
|
|
|
p.next();
|
|
|
|
type = p.save_pos(mk_expr_placeholder(), pos);
|
|
|
|
value = p.parse_expr();
|
2014-09-23 17:00:36 +00:00
|
|
|
} else if (p.curr_is_token(get_colon_tk())) {
|
2014-06-25 15:39:14 +00:00
|
|
|
p.next();
|
2014-07-08 21:38:57 +00:00
|
|
|
auto pos = p.pos();
|
2014-07-06 23:46:34 +00:00
|
|
|
type = p.parse_expr();
|
2014-09-23 17:00:36 +00:00
|
|
|
if (is_theorem && !p.curr_is_token(get_assign_tk())) {
|
2014-08-18 00:03:54 +00:00
|
|
|
check_end_of_theorem(p);
|
2014-07-08 21:38:57 +00:00
|
|
|
value = mk_expr_placeholder();
|
|
|
|
} else {
|
2014-09-23 17:00:36 +00:00
|
|
|
p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
|
2014-07-08 21:38:57 +00:00
|
|
|
value = p.save_pos(p.parse_expr(), pos);
|
|
|
|
}
|
2014-06-25 15:39:14 +00:00
|
|
|
} else {
|
2014-06-30 16:14:55 +00:00
|
|
|
buffer<expr> ps;
|
2014-06-18 17:36:21 +00:00
|
|
|
optional<local_environment> lenv;
|
2014-07-06 23:46:34 +00:00
|
|
|
lenv = p.parse_binders(ps);
|
2014-07-14 04:41:44 +00:00
|
|
|
auto pos = p.pos();
|
2014-09-23 17:00:36 +00:00
|
|
|
if (p.curr_is_token(get_colon_tk())) {
|
2014-07-06 23:46:34 +00:00
|
|
|
p.next();
|
|
|
|
type = p.parse_scoped_expr(ps, *lenv);
|
2014-09-23 17:00:36 +00:00
|
|
|
if (is_theorem && !p.curr_is_token(get_assign_tk())) {
|
2014-08-18 00:03:54 +00:00
|
|
|
check_end_of_theorem(p);
|
2014-07-08 21:38:57 +00:00
|
|
|
value = p.save_pos(mk_expr_placeholder(), pos);
|
|
|
|
} else {
|
2014-09-23 17:00:36 +00:00
|
|
|
p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
|
2014-07-08 21:38:57 +00:00
|
|
|
value = p.parse_scoped_expr(ps, *lenv);
|
|
|
|
}
|
2014-07-06 23:46:34 +00:00
|
|
|
} else {
|
|
|
|
type = p.save_pos(mk_expr_placeholder(), p.pos());
|
2014-09-23 17:00:36 +00:00
|
|
|
p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
|
2014-07-08 21:38:57 +00:00
|
|
|
value = p.parse_scoped_expr(ps, *lenv);
|
2014-06-18 17:36:21 +00:00
|
|
|
}
|
2014-07-14 04:41:44 +00:00
|
|
|
type = Pi(ps, type, p);
|
2014-09-07 19:28:58 +00:00
|
|
|
erase_local_binder_info(ps);
|
2014-07-14 04:41:44 +00:00
|
|
|
value = Fun(ps, value, p);
|
2014-06-18 17:36:21 +00:00
|
|
|
}
|
2014-08-01 01:35:57 +00:00
|
|
|
|
2014-06-18 20:55:48 +00:00
|
|
|
update_univ_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p);
|
2014-06-18 17:36:21 +00:00
|
|
|
ls = to_list(ls_buffer.begin(), ls_buffer.end());
|
|
|
|
}
|
2014-08-17 19:14:42 +00:00
|
|
|
unsigned end_line = p.pos().first;
|
2014-08-01 01:35:57 +00:00
|
|
|
|
|
|
|
if (p.used_sorry())
|
|
|
|
p.declare_sorry();
|
|
|
|
environment env = p.env();
|
|
|
|
|
2014-09-19 21:30:02 +00:00
|
|
|
if (is_private) {
|
2014-08-01 01:35:57 +00:00
|
|
|
auto env_n = add_private_name(env, n, optional<unsigned>(hash(p.pos().first, p.pos().second)));
|
|
|
|
env = env_n.first;
|
|
|
|
real_n = env_n.second;
|
|
|
|
} else {
|
|
|
|
name const & ns = get_namespace(env);
|
|
|
|
real_n = ns + n;
|
|
|
|
}
|
|
|
|
|
2014-08-23 22:44:28 +00:00
|
|
|
if (in_section_or_context(env)) {
|
2014-06-30 16:14:55 +00:00
|
|
|
buffer<expr> section_ps;
|
2014-06-18 17:36:21 +00:00
|
|
|
collect_section_locals(type, value, p, section_ps);
|
2014-07-14 05:27:36 +00:00
|
|
|
type = Pi_as_is(section_ps, type, p);
|
2014-09-07 19:28:58 +00:00
|
|
|
buffer<expr> section_value_ps;
|
|
|
|
section_value_ps.append(section_ps);
|
|
|
|
erase_local_binder_info(section_value_ps);
|
|
|
|
value = Fun_as_is(section_value_ps, value, p);
|
2014-06-18 20:55:48 +00:00
|
|
|
levels section_ls = collect_section_levels(ls, p);
|
2014-07-25 18:10:45 +00:00
|
|
|
for (expr & p : section_ps)
|
|
|
|
p = mk_explicit(p);
|
2014-07-19 08:55:34 +00:00
|
|
|
expr ref = mk_implicit(mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_ps));
|
2014-06-18 17:36:21 +00:00
|
|
|
p.add_local_expr(n, ref);
|
|
|
|
}
|
2014-08-10 18:04:16 +00:00
|
|
|
expr pre_type = type;
|
|
|
|
expr pre_value = value;
|
2014-07-06 23:46:34 +00:00
|
|
|
level_param_names new_ls;
|
2014-08-10 18:04:16 +00:00
|
|
|
bool found_cached = false;
|
2014-08-17 19:14:42 +00:00
|
|
|
if (p.are_info_lines_valid(start_line, end_line)) {
|
|
|
|
// we only use the cache if the information associated with the line is valid
|
|
|
|
if (auto it = p.find_cached_definition(real_n, pre_type, pre_value)) {
|
|
|
|
optional<certified_declaration> cd;
|
|
|
|
try {
|
|
|
|
level_param_names c_ls; expr c_type, c_value;
|
|
|
|
std::tie(c_ls, c_type, c_value) = *it;
|
|
|
|
if (is_theorem)
|
|
|
|
cd = check(env, mk_theorem(real_n, c_ls, c_type, c_value));
|
|
|
|
else
|
2014-09-19 20:44:44 +00:00
|
|
|
cd = check(env, mk_definition(env, real_n, c_ls, c_type, c_value, is_opaque));
|
2014-09-19 21:30:02 +00:00
|
|
|
if (!is_private)
|
2014-08-23 19:39:59 +00:00
|
|
|
p.add_decl_index(real_n, n_pos, p.get_cmd_token(), c_type);
|
2014-08-17 19:14:42 +00:00
|
|
|
env = module::add(env, *cd);
|
|
|
|
found_cached = true;
|
|
|
|
} catch (exception&) {}
|
|
|
|
}
|
2014-08-10 18:04:16 +00:00
|
|
|
}
|
|
|
|
|
|
|
|
if (!found_cached) {
|
|
|
|
if (is_theorem) {
|
2014-08-26 04:26:17 +00:00
|
|
|
auto type_pos = p.pos_of(type);
|
2014-09-05 08:12:08 +00:00
|
|
|
bool clear_pre_info = false; // we don't want to clear pre_info data until we process the proof.
|
|
|
|
std::tie(type, new_ls) = p.elaborate_type(type, list<expr>(), clear_pre_info);
|
2014-08-26 16:01:17 +00:00
|
|
|
check_no_metavar(env, real_n, type, true);
|
2014-08-26 04:26:17 +00:00
|
|
|
ls = append(ls, new_ls);
|
|
|
|
expr type_as_is = p.save_pos(mk_as_is(type), type_pos);
|
2014-08-17 19:14:42 +00:00
|
|
|
if (!p.collecting_info() && p.num_threads() > 1) {
|
2014-08-10 18:04:16 +00:00
|
|
|
// add as axiom, and create a task to prove the theorem
|
2014-08-26 04:26:17 +00:00
|
|
|
p.add_delayed_theorem(env, real_n, ls, type_as_is, value);
|
|
|
|
env = module::add(env, check(env, mk_axiom(real_n, ls, type)));
|
2014-08-10 18:04:16 +00:00
|
|
|
} else {
|
2014-09-19 20:44:44 +00:00
|
|
|
std::tie(type, value, new_ls) = p.elaborate_definition(n, type_as_is, value, is_opaque);
|
2014-08-10 18:04:16 +00:00
|
|
|
new_ls = append(ls, new_ls);
|
|
|
|
env = module::add(env, check(env, mk_theorem(real_n, new_ls, type, value)));
|
|
|
|
p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value);
|
|
|
|
}
|
2014-07-12 21:50:57 +00:00
|
|
|
} else {
|
2014-09-19 20:44:44 +00:00
|
|
|
std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, is_opaque);
|
2014-08-10 18:04:16 +00:00
|
|
|
new_ls = append(ls, new_ls);
|
2014-09-19 20:44:44 +00:00
|
|
|
env = module::add(env, check(env, mk_definition(env, real_n, new_ls, type, value, is_opaque)));
|
2014-08-10 18:04:16 +00:00
|
|
|
p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value);
|
2014-07-12 21:50:57 +00:00
|
|
|
}
|
2014-09-19 21:30:02 +00:00
|
|
|
if (!is_private)
|
2014-08-23 19:39:59 +00:00
|
|
|
p.add_decl_index(real_n, n_pos, p.get_cmd_token(), type);
|
2014-06-18 17:36:21 +00:00
|
|
|
}
|
2014-08-10 18:04:16 +00:00
|
|
|
|
2014-07-14 04:41:44 +00:00
|
|
|
if (real_n != n)
|
2014-07-28 04:01:59 +00:00
|
|
|
env = add_expr_alias_rec(env, n, real_n);
|
2014-09-28 19:20:42 +00:00
|
|
|
if (modifiers.m_is_instance) {
|
|
|
|
bool persistent = true;
|
|
|
|
if (modifiers.m_priority) {
|
2014-09-29 19:33:15 +00:00
|
|
|
#if defined(__GNUC__) && !defined(__CLANG__)
|
2014-09-28 19:32:47 +00:00
|
|
|
#pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
|
|
|
|
#endif
|
2014-09-28 19:20:42 +00:00
|
|
|
env = add_instance(env, real_n, *modifiers.m_priority, persistent);
|
|
|
|
} else {
|
|
|
|
env = add_instance(env, real_n, persistent);
|
|
|
|
}
|
|
|
|
}
|
2014-07-08 00:48:20 +00:00
|
|
|
if (modifiers.m_is_coercion)
|
|
|
|
env = add_coercion(env, real_n, p.ios());
|
2014-09-19 22:04:52 +00:00
|
|
|
if (is_protected)
|
2014-09-03 22:01:13 +00:00
|
|
|
env = add_protected(env, real_n);
|
2014-09-19 20:30:08 +00:00
|
|
|
if (modifiers.m_is_reducible)
|
|
|
|
env = set_reducible(env, real_n, reducible_status::On);
|
2014-06-18 17:36:21 +00:00
|
|
|
return env;
|
|
|
|
}
|
|
|
|
environment definition_cmd(parser & p) {
|
2014-09-19 22:04:52 +00:00
|
|
|
return definition_cmd_core(p, false, false, false, false);
|
2014-09-19 20:44:44 +00:00
|
|
|
}
|
|
|
|
environment opaque_definition_cmd(parser & p) {
|
2014-09-23 17:00:36 +00:00
|
|
|
p.check_token_next(get_definition_tk(), "invalid 'opaque' definition, 'definition' expected");
|
2014-09-19 22:04:52 +00:00
|
|
|
return definition_cmd_core(p, false, true, false, false);
|
2014-06-18 17:36:21 +00:00
|
|
|
}
|
|
|
|
environment theorem_cmd(parser & p) {
|
2014-09-19 22:04:52 +00:00
|
|
|
return definition_cmd_core(p, true, true, false, false);
|
2014-09-19 21:30:02 +00:00
|
|
|
}
|
|
|
|
environment private_definition_cmd(parser & p) {
|
|
|
|
bool is_theorem = false;
|
2014-10-02 14:56:01 +00:00
|
|
|
bool is_opaque = false;
|
|
|
|
if (p.curr_is_token_or_id(get_opaque_tk())) {
|
|
|
|
is_opaque = true;
|
|
|
|
p.next();
|
|
|
|
p.check_token_next(get_definition_tk(), "invalid 'private' definition, 'definition' expected");
|
|
|
|
} else if (p.curr_is_token_or_id(get_definition_tk())) {
|
2014-09-19 21:30:02 +00:00
|
|
|
p.next();
|
2014-09-23 17:00:36 +00:00
|
|
|
} else if (p.curr_is_token_or_id(get_theorem_tk())) {
|
2014-09-19 21:30:02 +00:00
|
|
|
p.next();
|
|
|
|
is_theorem = true;
|
2014-10-02 14:56:01 +00:00
|
|
|
is_opaque = true;
|
2014-09-19 21:30:02 +00:00
|
|
|
} else {
|
|
|
|
throw parser_error("invalid 'private' definition/theorem, 'definition' or 'theorem' expected", p.pos());
|
|
|
|
}
|
2014-10-02 14:56:01 +00:00
|
|
|
return definition_cmd_core(p, is_theorem, is_opaque, true, false);
|
2014-09-19 22:04:52 +00:00
|
|
|
}
|
|
|
|
environment protected_definition_cmd(parser & p) {
|
|
|
|
bool is_theorem = false;
|
|
|
|
bool is_opaque = false;
|
2014-09-23 17:00:36 +00:00
|
|
|
if (p.curr_is_token_or_id(get_opaque_tk())) {
|
2014-09-19 22:04:52 +00:00
|
|
|
is_opaque = true;
|
|
|
|
p.next();
|
2014-09-23 17:00:36 +00:00
|
|
|
p.check_token_next(get_definition_tk(), "invalid 'protected' definition, 'definition' expected");
|
|
|
|
} else if (p.curr_is_token_or_id(get_definition_tk())) {
|
2014-09-19 22:04:52 +00:00
|
|
|
p.next();
|
2014-09-23 17:00:36 +00:00
|
|
|
} else if (p.curr_is_token_or_id(get_theorem_tk())) {
|
2014-09-19 22:04:52 +00:00
|
|
|
p.next();
|
|
|
|
is_theorem = true;
|
|
|
|
is_opaque = true;
|
|
|
|
} else {
|
|
|
|
throw parser_error("invalid 'protected' definition/theorem, 'definition' or 'theorem' expected", p.pos());
|
|
|
|
}
|
|
|
|
return definition_cmd_core(p, is_theorem, is_opaque, false, true);
|
2014-06-18 17:36:21 +00:00
|
|
|
}
|
|
|
|
|
2014-06-23 00:51:00 +00:00
|
|
|
static environment variables_cmd(parser & p) {
|
2014-06-18 17:36:21 +00:00
|
|
|
auto pos = p.pos();
|
|
|
|
environment env = p.env();
|
2014-07-17 19:47:33 +00:00
|
|
|
while (true) {
|
|
|
|
optional<binder_info> bi = parse_binder_info(p);
|
|
|
|
buffer<name> ids;
|
2014-09-23 17:00:36 +00:00
|
|
|
while (!p.curr_is_token(get_colon_tk())) {
|
2014-07-17 19:47:33 +00:00
|
|
|
name id = p.check_id_next("invalid parameters declaration, identifier expected");
|
|
|
|
ids.push_back(id);
|
|
|
|
}
|
|
|
|
p.next();
|
|
|
|
optional<parser::local_scope> scope1;
|
2014-08-23 22:44:28 +00:00
|
|
|
if (!in_section_or_context(p.env()))
|
2014-07-17 19:47:33 +00:00
|
|
|
scope1.emplace(p);
|
|
|
|
expr type = p.parse_expr();
|
|
|
|
p.parse_close_binder_info(bi);
|
|
|
|
level_param_names ls = to_level_param_names(collect_univ_params(type));
|
|
|
|
list<expr> ctx = locals_to_context(type, p);
|
2014-08-12 22:00:32 +00:00
|
|
|
for (auto id : ids) {
|
|
|
|
// Hack: to make sure we get different universe parameters for each parameter.
|
|
|
|
// Alternative: elaborate once and copy types replacing universes in new_ls.
|
|
|
|
level_param_names new_ls;
|
|
|
|
expr new_type;
|
|
|
|
std::tie(new_type, new_ls) = p.elaborate_type(type, ctx);
|
|
|
|
update_section_local_levels(p, new_ls);
|
|
|
|
new_ls = append(ls, new_ls);
|
|
|
|
env = declare_var(p, env, id, new_ls, new_type, false, bi, pos);
|
|
|
|
}
|
2014-09-23 17:00:36 +00:00
|
|
|
if (!p.curr_is_token(get_lparen_tk()) && !p.curr_is_token(get_lcurly_tk()) &&
|
|
|
|
!p.curr_is_token(get_ldcurly_tk()) && !p.curr_is_token(get_lbracket_tk()))
|
2014-07-17 19:47:33 +00:00
|
|
|
break;
|
|
|
|
}
|
2014-06-18 17:36:21 +00:00
|
|
|
return env;
|
|
|
|
}
|
2014-06-23 00:51:00 +00:00
|
|
|
|
2014-06-18 17:36:21 +00:00
|
|
|
void register_decl_cmds(cmd_table & r) {
|
|
|
|
add_cmd(r, cmd_info("universe", "declare a global universe level", universe_cmd));
|
|
|
|
add_cmd(r, cmd_info("variable", "declare a new parameter", variable_cmd));
|
|
|
|
add_cmd(r, cmd_info("axiom", "declare a new axiom", axiom_cmd));
|
|
|
|
add_cmd(r, cmd_info("definition", "add new definition", definition_cmd));
|
2014-09-19 20:44:44 +00:00
|
|
|
add_cmd(r, cmd_info("opaque", "add new opaque definition", opaque_definition_cmd));
|
2014-09-19 21:30:02 +00:00
|
|
|
add_cmd(r, cmd_info("private", "add new private definition/theorem", private_definition_cmd));
|
2014-09-19 22:04:52 +00:00
|
|
|
add_cmd(r, cmd_info("protected", "add new protected definition/theorem", protected_definition_cmd));
|
2014-06-18 17:36:21 +00:00
|
|
|
add_cmd(r, cmd_info("theorem", "add new theorem", theorem_cmd));
|
|
|
|
add_cmd(r, cmd_info("variables", "declare new parameters", variables_cmd));
|
|
|
|
}
|
|
|
|
}
|