feat(frontends/lean): add inductive_cmd
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
461689f758
commit
bdab979e09
18 changed files with 520 additions and 32 deletions
|
|
@ -24,7 +24,7 @@
|
|||
(define-generic-mode
|
||||
'lean-mode ;; name of the mode to create
|
||||
'("--") ;; comments start with
|
||||
'("import" "abbreviation" "definition" "parameter" "parameters" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "section" "set_option" "add_rewrite") ;; some keywords
|
||||
'("import" "abbreviation" "definition" "parameter" "parameters" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "section" "set_option" "add_rewrite") ;; some keywords
|
||||
'(("\\_<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face)
|
||||
("\\_<\\(calc\\|have\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face)
|
||||
("\"[^\"]*\"" . 'font-lock-string-face)
|
||||
|
|
|
|||
|
|
@ -2,6 +2,6 @@ add_library(lean_frontend register_module.cpp token_table.cpp
|
|||
scanner.cpp parse_table.cpp parser_config.cpp parser.cpp
|
||||
parser_pos_provider.cpp builtin_cmds.cpp builtin_tactic_cmds.cpp
|
||||
builtin_exprs.cpp interactive.cpp notation_cmd.cpp calc.cpp
|
||||
decl_cmds.cpp util.cpp)
|
||||
decl_cmds.cpp util.cpp inductive_cmd.cpp)
|
||||
|
||||
target_link_libraries(lean_frontend ${LEAN_LIBS})
|
||||
|
|
|
|||
|
|
@ -16,6 +16,7 @@ Author: Leonardo de Moura
|
|||
#include "frontends/lean/parser.h"
|
||||
#include "frontends/lean/calc.h"
|
||||
#include "frontends/lean/notation_cmd.h"
|
||||
#include "frontends/lean/inductive_cmd.h"
|
||||
#include "frontends/lean/decl_cmds.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -217,6 +218,7 @@ cmd_table init_cmd_table() {
|
|||
add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd));
|
||||
add_cmd(r, cmd_info("#setline", "modify the current line number, it only affects error/report messages", set_line_cmd));
|
||||
register_decl_cmds(r);
|
||||
register_inductive_cmd(r);
|
||||
register_notation_cmds(r);
|
||||
register_calc_cmds(r);
|
||||
return r;
|
||||
|
|
|
|||
|
|
@ -38,7 +38,7 @@ environment universe_cmd(parser & p) {
|
|||
return env;
|
||||
}
|
||||
|
||||
void parse_univ_params(parser & p, buffer<name> & ps) {
|
||||
bool parse_univ_params(parser & p, buffer<name> & ps) {
|
||||
if (p.curr_is_token(g_llevel_curly)) {
|
||||
p.next();
|
||||
while (!p.curr_is_token(g_rcurly)) {
|
||||
|
|
@ -47,10 +47,13 @@ void parse_univ_params(parser & p, buffer<name> & ps) {
|
|||
ps.push_back(l);
|
||||
}
|
||||
p.next();
|
||||
return true;
|
||||
} else{
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
void update_parameters(buffer<name> & ls_buffer, name_set const & found, parser const & p) {
|
||||
void update_univ_parameters(buffer<name> & ls_buffer, name_set const & found, parser const & p) {
|
||||
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)
|
||||
|
|
@ -107,7 +110,7 @@ environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi)
|
|||
if (in_section(p.env())) {
|
||||
ls = to_level_param_names(collect_univ_params(type));
|
||||
} else {
|
||||
update_parameters(ls_buffer, collect_univ_params(type), p);
|
||||
update_univ_parameters(ls_buffer, collect_univ_params(type), p);
|
||||
ls = to_list(ls_buffer.begin(), ls_buffer.end());
|
||||
}
|
||||
type = p.elaborate(type, ls);
|
||||
|
|
@ -132,10 +135,9 @@ environment cast_variable_cmd(parser & p) {
|
|||
return variable_cmd_core(p, false, mk_cast_binder_info());
|
||||
}
|
||||
|
||||
// Collect local (section) constants occurring in type and value, sort them, and store in section_ps
|
||||
void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer<parameter> & section_ps) {
|
||||
name_set ls = collect_locals(type, collect_locals(value));
|
||||
ls.for_each([&](name const & n) {
|
||||
// Sort local_names by order of occurrence in the section, and copy the associated parameters to section_ps
|
||||
void mk_section_params(name_set const & local_names, parser const & p, buffer<parameter> & section_ps) {
|
||||
local_names.for_each([&](name const & n) {
|
||||
section_ps.push_back(*p.get_local(n));
|
||||
});
|
||||
std::sort(section_ps.begin(), section_ps.end(), [&](parameter const & p1, parameter const & p2) {
|
||||
|
|
@ -143,6 +145,12 @@ void collect_section_locals(expr const & type, expr const & value, parser const
|
|||
});
|
||||
}
|
||||
|
||||
// Collect local (section) constants occurring in type and value, sort them, and store in section_ps
|
||||
void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer<parameter> & section_ps) {
|
||||
name_set ls = collect_locals(type, collect_locals(value));
|
||||
return mk_section_params(ls, p, section_ps);
|
||||
}
|
||||
|
||||
static void parse_modifiers(parser & p, bool & is_private, bool & is_opaque) {
|
||||
while (true) {
|
||||
if (p.curr_is_token(g_private)) {
|
||||
|
|
@ -157,6 +165,18 @@ static void parse_modifiers(parser & p, bool & is_private, bool & is_opaque) {
|
|||
}
|
||||
}
|
||||
|
||||
// Return the levels in \c ls that are defined in the section
|
||||
levels collect_section_levels(level_param_names const & ls, parser & p) {
|
||||
buffer<level> section_ls_buffer;
|
||||
for (name const & l : ls) {
|
||||
if (p.get_local_level_index(l))
|
||||
section_ls_buffer.push_back(mk_param_univ(l));
|
||||
else
|
||||
break;
|
||||
}
|
||||
return to_list(section_ls_buffer.begin(), section_ls_buffer.end());
|
||||
}
|
||||
|
||||
environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
|
||||
bool is_private = false;
|
||||
parse_modifiers(p, is_private, is_opaque);
|
||||
|
|
@ -202,7 +222,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
|
|||
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
|
||||
value = p.parse_expr();
|
||||
}
|
||||
update_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p);
|
||||
update_univ_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p);
|
||||
ls = to_list(ls_buffer.begin(), ls_buffer.end());
|
||||
}
|
||||
if (in_section(env)) {
|
||||
|
|
@ -210,14 +230,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
|
|||
collect_section_locals(type, value, p, section_ps);
|
||||
type = p.pi_abstract(section_ps, type);
|
||||
value = p.lambda_abstract(section_ps, value);
|
||||
buffer<level> section_ls_buffer;
|
||||
for (name const & l : ls) {
|
||||
if (p.get_local_level_index(l))
|
||||
section_ls_buffer.push_back(mk_param_univ(l));
|
||||
else
|
||||
break;
|
||||
}
|
||||
levels section_ls = to_list(section_ls_buffer.begin(), section_ls_buffer.end());
|
||||
levels section_ls = collect_section_levels(ls, p);
|
||||
buffer<expr> section_args;
|
||||
for (auto const & p : section_ps)
|
||||
section_args.push_back(p.m_local);
|
||||
|
|
|
|||
|
|
@ -7,11 +7,29 @@ Author: Leonardo de Moura
|
|||
#pragma once
|
||||
#include "util/buffer.h"
|
||||
#include "kernel/expr.h"
|
||||
#include "frontends/lean/parameter.h"
|
||||
#include "frontends/lean/cmd_table.h"
|
||||
namespace lean {
|
||||
class parser;
|
||||
void parse_univ_params(parser & p, buffer<name> & ps);
|
||||
void update_parameters(buffer<name> & ls_buffer, name_set const & found, parser const & p);
|
||||
void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer<parameter> & section_ps);
|
||||
/**
|
||||
\brief Parse (optional) universe parameters <tt>'.{' l_1 ... l_k '}'</tt>
|
||||
Store the result in \c ps.
|
||||
Return true when levels were provided.
|
||||
*/
|
||||
bool parse_univ_params(parser & p, buffer<name> & ps);
|
||||
/**
|
||||
\brief Add universe levels from \c found_ls to \c ls_buffer (only the levels that do not already occur in \c ls_buffer are added).
|
||||
Then sort \c ls_buffer (using the order in which the universe levels were declared).
|
||||
*/
|
||||
void update_univ_parameters(buffer<name> & ls_buffer, name_set const & found_ls, parser const & p);
|
||||
/**
|
||||
\brief Copy the parameters associated with the local names in \c local_names to \c section_ps.
|
||||
Then sort \c section_ps (using the order in which they were declared).
|
||||
*/
|
||||
void mk_section_params(name_set const & local_names, parser const & p, buffer<parameter> & section_ps);
|
||||
/**
|
||||
\brief Return the levels in \c ls that are defined in the section.
|
||||
*/
|
||||
levels collect_section_levels(level_param_names const & ls, parser & p);
|
||||
void register_decl_cmds(cmd_table & r);
|
||||
}
|
||||
|
|
|
|||
343
src/frontends/lean/inductive_cmd.cpp
Normal file
343
src/frontends/lean/inductive_cmd.cpp
Normal file
|
|
@ -0,0 +1,343 @@
|
|||
/*
|
||||
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 "util/sstream.h"
|
||||
#include "util/name_map.h"
|
||||
#include "kernel/replace_fn.h"
|
||||
#include "kernel/type_checker.h"
|
||||
#include "kernel/instantiate.h"
|
||||
#include "kernel/inductive/inductive.h"
|
||||
#include "library/scoped_ext.h"
|
||||
#include "library/locals.h"
|
||||
#include "library/placeholder.h"
|
||||
#include "library/aliases.h"
|
||||
#include "frontends/lean/decl_cmds.h"
|
||||
#include "frontends/lean/util.h"
|
||||
#include "frontends/lean/parser.h"
|
||||
|
||||
namespace lean {
|
||||
static name g_assign(":=");
|
||||
static name g_with("with");
|
||||
static name g_colon(":");
|
||||
static name g_bar("|");
|
||||
|
||||
using inductive::intro_rule;
|
||||
using inductive::inductive_decl;
|
||||
using inductive::inductive_decl_name;
|
||||
using inductive::inductive_decl_type;
|
||||
using inductive::inductive_decl_intros;
|
||||
using inductive::intro_rule_name;
|
||||
using inductive::intro_rule_type;
|
||||
|
||||
// Mark all parameters as implicit
|
||||
static void make_implicit(buffer<parameter> & ps) {
|
||||
for (parameter & p : ps)
|
||||
p.m_bi = mk_implicit_binder_info();
|
||||
}
|
||||
|
||||
// Make sure that every inductive datatype (in decls) occurring in \c type has
|
||||
// the universe levels \c lvl_params and section parameters \c section_params
|
||||
static expr fix_inductive_occs(expr const & type, buffer<inductive_decl> const & decls,
|
||||
buffer<name> const & lvl_params, buffer<parameter> const & section_params) {
|
||||
return replace(type, [&](expr const & e, unsigned) {
|
||||
if (!is_constant(e))
|
||||
return none_expr();
|
||||
if (!std::any_of(decls.begin(), decls.end(),
|
||||
[&](inductive_decl const & d) { return const_name(e) == inductive_decl_name(d); }))
|
||||
return none_expr();
|
||||
// found target
|
||||
levels ls = const_levels(e);
|
||||
unsigned n = length(ls);
|
||||
if (n < lvl_params.size()) {
|
||||
unsigned i = lvl_params.size() - n;
|
||||
while (i > 0) {
|
||||
--i;
|
||||
ls = cons(mk_param_univ(lvl_params[i]), ls);
|
||||
}
|
||||
}
|
||||
expr r = update_constant(e, ls);
|
||||
for (unsigned i = 0; i < section_params.size(); i++)
|
||||
r = mk_app(r, section_params[i].m_local);
|
||||
return some_expr(r);
|
||||
});
|
||||
}
|
||||
|
||||
static level mk_result_level(bool impredicative, buffer<level> const & ls) {
|
||||
if (ls.empty()) {
|
||||
return impredicative ? mk_level_one() : mk_level_zero();
|
||||
} else {
|
||||
level r = ls[0];
|
||||
for (unsigned i = 1; i < ls.size(); i++)
|
||||
r = mk_max(r, ls[i]);
|
||||
return impredicative ? mk_max(r, mk_level_one()) : r;
|
||||
}
|
||||
}
|
||||
|
||||
static expr update_result_sort(expr const & t, level const & l) {
|
||||
if (is_pi(t)) {
|
||||
return update_binding(t, binding_domain(t), update_result_sort(binding_body(t), l));
|
||||
} else if (is_sort(t)) {
|
||||
return update_sort(t, l);
|
||||
} else {
|
||||
lean_unreachable();
|
||||
}
|
||||
}
|
||||
|
||||
static name g_tmp_prefix = name::mk_internal_unique_name();
|
||||
static void set_result_universes(buffer<inductive_decl> & decls, level_param_names const & lvls, unsigned num_params, parser & p) {
|
||||
if (std::all_of(decls.begin(), decls.end(), [](inductive_decl const & d) {
|
||||
return !has_placeholder(inductive_decl_type(d));
|
||||
}))
|
||||
return; // nothing to be done
|
||||
// We can't infer the type of intro rule arguments because we did declare the inductive datatypes.
|
||||
// So, we use the following trick, we create a "draft" environment where the inductive datatypes
|
||||
// are asserted as variable declarations, and keep doing that until we reach a "fix" point.
|
||||
unsigned num_rounds = 0;
|
||||
while (true) {
|
||||
if (num_rounds > 2*decls.size() + 1) {
|
||||
// TODO(Leo): this is test is a hack to avoid non-termination.
|
||||
// We should use a better termination condition
|
||||
throw exception("failed to compute resultant universe level for inductive datatypes, "
|
||||
"provide explicit universe levels");
|
||||
}
|
||||
num_rounds++;
|
||||
bool progress = false;
|
||||
environment env = p.env();
|
||||
bool impredicative = env.impredicative();
|
||||
// first assert inductive types that do not have placeholders
|
||||
for (auto const & d : decls) {
|
||||
expr type = inductive_decl_type(d);
|
||||
if (!has_placeholder(type))
|
||||
env = env.add(check(env, mk_var_decl(inductive_decl_name(d), lvls, inductive_decl_type(d))));
|
||||
}
|
||||
type_checker tc(env);
|
||||
name_generator ngen(g_tmp_prefix);
|
||||
// try to update resultant universe levels
|
||||
for (auto & d : decls) {
|
||||
expr d_t = inductive_decl_type(d);
|
||||
while (is_pi(d_t)) {
|
||||
d_t = binding_body(d_t);
|
||||
}
|
||||
if (!is_sort(d_t))
|
||||
throw exception(sstream() << "invalid inductive datatype '" << inductive_decl_name(d) << "', "
|
||||
"resultant type is not a sort");
|
||||
level r_lvl = sort_level(d_t);
|
||||
if (impredicative && is_zero(r_lvl))
|
||||
continue;
|
||||
buffer<level> lvls;
|
||||
for (intro_rule const & ir : inductive_decl_intros(d)) {
|
||||
expr t = intro_rule_type(ir);
|
||||
unsigned i = 0;
|
||||
while (is_pi(t)) {
|
||||
if (i >= num_params) {
|
||||
try {
|
||||
expr s = tc.ensure_sort(tc.infer(binding_domain(t)));
|
||||
level lvl = sort_level(s);
|
||||
if (std::find(lvls.begin(), lvls.end(), lvl) == lvls.end())
|
||||
lvls.push_back(lvl);
|
||||
} catch (...) {
|
||||
}
|
||||
}
|
||||
t = instantiate(binding_body(t), mk_local(ngen.next(), binding_name(t), binding_domain(t)));
|
||||
i++;
|
||||
}
|
||||
}
|
||||
level m_lvl = normalize(mk_result_level(impredicative, lvls));
|
||||
if (is_placeholder(r_lvl) || !(is_geq(r_lvl, m_lvl))) {
|
||||
progress = true;
|
||||
// update result level
|
||||
expr new_type = update_result_sort(inductive_decl_type(d), m_lvl);
|
||||
d = inductive_decl(inductive_decl_name(d), new_type, inductive_decl_intros(d));
|
||||
}
|
||||
}
|
||||
if (!progress)
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
static environment create_alias(environment const & env, name const & full_id, name const & id, levels const & section_leves,
|
||||
buffer<parameter> const & section_params, parser & p) {
|
||||
if (in_section(env)) {
|
||||
expr r = mark_explicit(mk_constant(full_id, section_leves));
|
||||
for (unsigned i = 0; i < section_params.size(); i++)
|
||||
r = mk_app(r, section_params[i].m_local);
|
||||
p.add_local_expr(id, r);
|
||||
return env;
|
||||
} else if (full_id != id) {
|
||||
return add_alias(env, id, mk_constant(full_id));
|
||||
} else {
|
||||
return env;
|
||||
}
|
||||
}
|
||||
|
||||
environment inductive_cmd(parser & p) {
|
||||
parser::no_undef_id_error_scope err_scope(p);
|
||||
environment env = p.env();
|
||||
name const & ns = get_namespace(env);
|
||||
bool first = true;
|
||||
buffer<name> ls_buffer;
|
||||
name_map<name> id_to_short_id;
|
||||
unsigned num_params = 0;
|
||||
bool explicit_levels = false;
|
||||
buffer<inductive_decl> decls;
|
||||
while (true) {
|
||||
parser::local_scope l_scope(p);
|
||||
auto id_pos = p.pos();
|
||||
name id = p.check_id_next("invalid inductive declaration, identifier expected");
|
||||
check_atomic(id);
|
||||
name full_id = ns + id;
|
||||
id_to_short_id.insert(full_id, id);
|
||||
buffer<name> curr_ls_buffer;
|
||||
expr type;
|
||||
optional<parser::param_universe_scope> pu_scope;
|
||||
if (parse_univ_params(p, curr_ls_buffer)) {
|
||||
if (first) {
|
||||
explicit_levels = true;
|
||||
ls_buffer.append(curr_ls_buffer);
|
||||
} else if (!explicit_levels) {
|
||||
throw parser_error("invalid mutually recursive declaration, "
|
||||
"explicit universe levels were not provided for previous inductive types in this declaration",
|
||||
id_pos);
|
||||
} else if (curr_ls_buffer.size() != ls_buffer.size()) {
|
||||
throw parser_error("invalid mutually recursive declaration, "
|
||||
"all inductive types must have the same number of universe paramaters", id_pos);
|
||||
} else {
|
||||
for (unsigned i = 0; i < ls_buffer.size(); i++) {
|
||||
if (curr_ls_buffer[i] != ls_buffer[i])
|
||||
throw parser_error("invalid mutually recursive inductive declaration, "
|
||||
"all inductive types must have the same universe paramaters", id_pos);
|
||||
}
|
||||
}
|
||||
} else {
|
||||
if (first) {
|
||||
explicit_levels = false;
|
||||
} else if (explicit_levels) {
|
||||
throw parser_error("invalid mutually recursive declaration, "
|
||||
"explicit universe levels were provided for previous inductive types in this declaration",
|
||||
id_pos);
|
||||
}
|
||||
// initialize param_universe_scope, we are using implicit universe levels
|
||||
pu_scope.emplace(p);
|
||||
}
|
||||
buffer<parameter> ps;
|
||||
local_environment lenv = env;
|
||||
auto params_pos = p.pos();
|
||||
if (!p.curr_is_token(g_colon)) {
|
||||
lenv = p.parse_binders(ps);
|
||||
p.check_token_next(g_colon, "invalid inductive declaration, ':' expected");
|
||||
{
|
||||
parser::placeholder_universe_scope place_scope(p);
|
||||
type = p.parse_scoped_expr(ps, lenv);
|
||||
}
|
||||
type = p.pi_abstract(ps, type);
|
||||
} else {
|
||||
p.next();
|
||||
parser::placeholder_universe_scope place_scope(p);
|
||||
type = p.parse_scoped_expr(ps, lenv);
|
||||
}
|
||||
// check if number of parameters
|
||||
if (first) {
|
||||
num_params = ps.size();
|
||||
} else {
|
||||
// mutually recursive declaration checks
|
||||
if (num_params != ps.size()) {
|
||||
throw parser_error("invalid mutually recursive inductive declaration, "
|
||||
"all inductive types must have the same number of arguments",
|
||||
params_pos);
|
||||
}
|
||||
}
|
||||
make_implicit(ps); // parameters are implicit for introduction rules
|
||||
// parse introduction rules
|
||||
p.check_token_next(g_assign, "invalid inductive declaration, ':=' expected");
|
||||
buffer<intro_rule> intros;
|
||||
while (p.curr_is_token(g_bar)) {
|
||||
p.next();
|
||||
name intro_id = p.check_id_next("invalid introduction rule, identifier expected");
|
||||
check_atomic(intro_id);
|
||||
name full_intro_id = ns + intro_id;
|
||||
id_to_short_id.insert(full_intro_id, intro_id);
|
||||
p.check_token_next(g_colon, "invalid introduction rule, ':' expected");
|
||||
expr intro_type = p.parse_scoped_expr(ps, lenv);
|
||||
intro_type = p.pi_abstract(ps, intro_type);
|
||||
intros.push_back(intro_rule(full_intro_id, intro_type));
|
||||
}
|
||||
decls.push_back(inductive_decl(full_id, type, to_list(intros.begin(), intros.end())));
|
||||
if (!p.curr_is_token(g_with))
|
||||
break;
|
||||
p.next();
|
||||
first = false;
|
||||
}
|
||||
// Collect (section) locals occurring in inductive_decls, and abstract them
|
||||
// using these additional parameters.
|
||||
name_set used_levels;
|
||||
name_set section_locals;
|
||||
for (inductive_decl const & d : decls) {
|
||||
used_levels = collect_univ_params(inductive_decl_type(d), used_levels);
|
||||
section_locals = collect_locals(inductive_decl_type(d), section_locals);
|
||||
for (auto const & ir : inductive_decl_intros(d)) {
|
||||
used_levels = collect_univ_params(intro_rule_type(ir), used_levels);
|
||||
section_locals = collect_locals(intro_rule_type(ir), section_locals);
|
||||
}
|
||||
}
|
||||
update_univ_parameters(ls_buffer, used_levels, p);
|
||||
buffer<parameter> section_params;
|
||||
mk_section_params(section_locals, p, section_params);
|
||||
// First, add section_params to inductive types type.
|
||||
// We don't update the introduction rules in the first pass, because
|
||||
// we will mark all section_params as implicit for them.
|
||||
for (inductive_decl & d : decls) {
|
||||
d = inductive_decl(inductive_decl_name(d),
|
||||
p.pi_abstract(section_params, inductive_decl_type(d)),
|
||||
inductive_decl_intros(d));
|
||||
}
|
||||
make_implicit(section_params);
|
||||
// Add section_params to introduction rules type, and also "fix"
|
||||
// occurrences of inductive types.
|
||||
for (inductive_decl & d : decls) {
|
||||
buffer<intro_rule> new_irs;
|
||||
for (auto const & ir : inductive_decl_intros(d)) {
|
||||
expr type = intro_rule_type(ir);
|
||||
type = fix_inductive_occs(type, decls, ls_buffer, section_params);
|
||||
type = p.pi_abstract(section_params, type);
|
||||
new_irs.push_back(intro_rule(intro_rule_name(ir), type));
|
||||
}
|
||||
d = inductive_decl(inductive_decl_name(d),
|
||||
inductive_decl_type(d),
|
||||
to_list(new_irs.begin(), new_irs.end()));
|
||||
}
|
||||
num_params += section_params.size();
|
||||
level_param_names ls = to_list(ls_buffer.begin(), ls_buffer.end());
|
||||
|
||||
// Check if introduction rules do not have placeholders
|
||||
for (inductive_decl const & d : decls) {
|
||||
for (auto const & ir : inductive_decl_intros(d)) {
|
||||
if (has_placeholder(intro_rule_type(ir)))
|
||||
throw exception(sstream() << "invalid inductive datatype '" << inductive_decl_name(d) << "', "
|
||||
<< "introduction rule '" << intro_rule_name(ir) << "' has placeholders");
|
||||
}
|
||||
}
|
||||
// "Fix" the inductive type resultant type universe level, if it was not explicitly provided.
|
||||
set_result_universes(decls, ls, num_params, p);
|
||||
env = module::add_inductive(env, ls, num_params, to_list(decls.begin(), decls.end()));
|
||||
// Create aliases/local refs
|
||||
levels section_levels = collect_section_levels(ls, p);
|
||||
for (inductive_decl const & d : decls) {
|
||||
name const & n = inductive_decl_name(d);
|
||||
env = create_alias(env, n, *id_to_short_id.find(n), section_levels, section_params, p);
|
||||
env = create_alias(env, n.append_after("_rec"), id_to_short_id.find(n)->append_after("_rec"), section_levels, section_params, p);
|
||||
for (intro_rule const & ir : inductive_decl_intros(d)) {
|
||||
name const & n = intro_rule_name(ir);
|
||||
env = create_alias(env, n, *id_to_short_id.find(n), section_levels, section_params, p);
|
||||
}
|
||||
}
|
||||
return env;
|
||||
}
|
||||
void register_inductive_cmd(cmd_table & r) {
|
||||
add_cmd(r, cmd_info("inductive", "declare an inductive datatype", inductive_cmd));
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
11
src/frontends/lean/inductive_cmd.h
Normal file
11
src/frontends/lean/inductive_cmd.h
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "frontends/lean/cmd_table.h"
|
||||
namespace lean {
|
||||
void register_inductive_cmd(cmd_table & r);
|
||||
}
|
||||
|
|
@ -24,6 +24,7 @@ Author: Leonardo de Moura
|
|||
#include "library/placeholder.h"
|
||||
#include "library/deep_copy.h"
|
||||
#include "library/module.h"
|
||||
#include "library/scoped_ext.h"
|
||||
#include "library/error_handling/error_handling.h"
|
||||
#include "frontends/lean/parser.h"
|
||||
#include "frontends/lean/notation_cmd.h"
|
||||
|
|
@ -58,6 +59,13 @@ parser::param_universe_scope::~param_universe_scope() {
|
|||
m_p.m_type_use_placeholder = m_old;
|
||||
}
|
||||
|
||||
parser::placeholder_universe_scope::placeholder_universe_scope(parser & p):m_p(p), m_old(m_p.m_type_use_placeholder) {
|
||||
m_p.m_type_use_placeholder = true;
|
||||
}
|
||||
parser::placeholder_universe_scope::~placeholder_universe_scope() {
|
||||
m_p.m_type_use_placeholder = m_old;
|
||||
}
|
||||
|
||||
parser::no_undef_id_error_scope::no_undef_id_error_scope(parser & p):m_p(p), m_old(m_p.m_no_undef_id_error) {
|
||||
m_p.m_no_undef_id_error = true;
|
||||
}
|
||||
|
|
@ -817,7 +825,7 @@ expr parser::parse_id() {
|
|||
r = mk_choice(new_as.size(), new_as.data());
|
||||
}
|
||||
if (m_no_undef_id_error)
|
||||
r = mk_constant(id, ls);
|
||||
r = mk_constant(get_namespace(m_env) + id, ls);
|
||||
if (!r)
|
||||
throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
|
||||
return *r;
|
||||
|
|
|
|||
|
|
@ -18,21 +18,13 @@ Author: Leonardo de Moura
|
|||
#include "library/io_state.h"
|
||||
#include "library/io_state_stream.h"
|
||||
#include "library/kernel_bindings.h"
|
||||
#include "frontends/lean/parameter.h"
|
||||
#include "frontends/lean/scanner.h"
|
||||
#include "frontends/lean/local_decls.h"
|
||||
#include "frontends/lean/parser_config.h"
|
||||
#include "frontends/lean/parser_pos_provider.h"
|
||||
|
||||
namespace lean {
|
||||
struct parameter {
|
||||
pos_info m_pos;
|
||||
expr m_local;
|
||||
binder_info m_bi;
|
||||
parameter(pos_info const & p, expr const & l, binder_info const & bi):
|
||||
m_pos(p), m_local(l), m_bi(bi) {}
|
||||
parameter():m_pos(0, 0) {}
|
||||
};
|
||||
|
||||
/** \brief Exception used to track parsing erros, it does not leak outside of this class. */
|
||||
struct parser_error : public exception {
|
||||
pos_info m_pos;
|
||||
|
|
@ -248,6 +240,8 @@ public:
|
|||
The new parameter is automatically added to \c m_local_level_decls.
|
||||
*/
|
||||
struct param_universe_scope { parser & m_p; bool m_old; param_universe_scope(parser &); ~param_universe_scope(); };
|
||||
/** \brief Switch back to <tt>Type.{_}</tt>, see \c param_universe_scope */
|
||||
struct placeholder_universe_scope { parser & m_p; bool m_old; placeholder_universe_scope(parser &); ~placeholder_universe_scope(); };
|
||||
expr mk_Type();
|
||||
|
||||
/** \brief Use tactic \c t for "synthesizing" the placeholder \c e. */
|
||||
|
|
|
|||
|
|
@ -56,7 +56,7 @@ token_table init_token_table() {
|
|||
std::pair<char const *, unsigned> builtin[] =
|
||||
{{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"by", 0},
|
||||
{"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
|
||||
{"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec},
|
||||
{"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec}, {"|", 0}, {"with", 0},
|
||||
{"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0},
|
||||
{"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0},
|
||||
{"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
|
||||
|
|
|
|||
6
tests/lean/run/ind0.lean
Normal file
6
tests/lean/run/ind0.lean
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
inductive nat : Type :=
|
||||
| zero : nat
|
||||
| succ : nat → nat
|
||||
|
||||
check nat
|
||||
check nat_rec.{1}
|
||||
7
tests/lean/run/ind1.lean
Normal file
7
tests/lean/run/ind1.lean
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
inductive list (A : Type) : Type :=
|
||||
| nil : list A
|
||||
| cons : A → list A → list A
|
||||
|
||||
check list.{1}
|
||||
check cons.{1}
|
||||
check list_rec.{1 1}
|
||||
12
tests/lean/run/ind2.lean
Normal file
12
tests/lean/run/ind2.lean
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
inductive nat : Type :=
|
||||
| zero : nat
|
||||
| succ : nat → nat
|
||||
|
||||
inductive vector (A : Type) : nat → Type :=
|
||||
| vnil : vector A zero
|
||||
| vcons : Π {n : nat}, A → vector A n → vector A (succ n)
|
||||
|
||||
check vector.{1}
|
||||
check vnil.{1}
|
||||
check vcons.{1}
|
||||
check vector_rec.{1 1}
|
||||
21
tests/lean/run/ind3.lean
Normal file
21
tests/lean/run/ind3.lean
Normal file
|
|
@ -0,0 +1,21 @@
|
|||
inductive tree (A : Type) : Type :=
|
||||
| node : A → forest A → tree A
|
||||
with forest {A : Type} : Type :=
|
||||
| nil : forest A
|
||||
| cons : tree A → forest A → forest A
|
||||
|
||||
check tree.{1}
|
||||
check forest.{1}
|
||||
check tree_rec.{1 1}
|
||||
check forest_rec.{1 1}
|
||||
|
||||
print "==============="
|
||||
|
||||
inductive group : Type :=
|
||||
| mk_group : Π (carrier : Type) (mul : carrier → carrier → carrier) (one : carrier), group
|
||||
|
||||
check group.{1}
|
||||
check group.{2}
|
||||
check group_rec.{1 1}
|
||||
|
||||
|
||||
23
tests/lean/run/ind4.lean
Normal file
23
tests/lean/run/ind4.lean
Normal file
|
|
@ -0,0 +1,23 @@
|
|||
section
|
||||
parameter A : Type
|
||||
inductive list : Type :=
|
||||
| nil : list
|
||||
| cons : A → list → list
|
||||
end
|
||||
|
||||
check list.{1}
|
||||
check cons.{1}
|
||||
|
||||
section
|
||||
parameter A : Type
|
||||
inductive tree : Type :=
|
||||
| node : A → forest → tree
|
||||
with forest : Type :=
|
||||
| fnil : forest
|
||||
| fcons : tree → forest → forest
|
||||
check tree
|
||||
check forest
|
||||
end
|
||||
|
||||
check tree.{1}
|
||||
check forest.{1}
|
||||
9
tests/lean/run/ind5.lean
Normal file
9
tests/lean/run/ind5.lean
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
definition [inline] Bool : Type.{1} := Type.{0}
|
||||
|
||||
inductive or (A B : Bool) : Bool :=
|
||||
| or_intro_left : A → or A B
|
||||
| or_intro_right : B → or A B
|
||||
|
||||
check or
|
||||
check or_intro_left
|
||||
check or_rec
|
||||
10
tests/lean/run/ind6.lean
Normal file
10
tests/lean/run/ind6.lean
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
inductive tree.{u} (A : Type.{u}) : Type.{max u 1} :=
|
||||
| node : A → forest.{u} A → tree.{u} A
|
||||
with forest.{u} {A : Type.{u}} : Type.{max u 1} :=
|
||||
| nil : forest.{u} A
|
||||
| cons : tree.{u} A → forest.{u} A → forest.{u} A
|
||||
|
||||
check tree.{1}
|
||||
check forest.{1}
|
||||
check tree_rec.{1 1}
|
||||
check forest_rec.{1 1}
|
||||
11
tests/lean/run/ind7.lean
Normal file
11
tests/lean/run/ind7.lean
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
namespace list
|
||||
inductive list (A : Type) : Type :=
|
||||
| nil : list A
|
||||
| cons : A → list A → list A
|
||||
|
||||
check list.{1}
|
||||
check cons.{1}
|
||||
check list_rec.{1 1}
|
||||
end
|
||||
|
||||
check list.list.{1}
|
||||
Loading…
Reference in a new issue