From 33c77afc297a8a8a8fed7161f8a19ef8cb58fde0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Jul 2014 19:04:57 -0700 Subject: [PATCH] feat(frontends/lean/structure): add 'structure' command skeleton Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 2 + src/emacs/lean-mode.el | 2 +- src/frontends/lean/CMakeLists.txt | 3 +- src/frontends/lean/builtin_cmds.cpp | 2 + src/frontends/lean/inductive_cmd.cpp | 30 +-- src/frontends/lean/parser.cpp | 11 +- src/frontends/lean/parser.h | 9 +- src/frontends/lean/structure_cmd.cpp | 298 +++++++++++++++++++++++++++ src/frontends/lean/structure_cmd.h | 11 + src/frontends/lean/token_table.cpp | 4 +- src/frontends/lean/util.cpp | 26 +++ src/frontends/lean/util.h | 4 + src/kernel/record/CMakeLists.txt | 2 + src/kernel/record/record.cpp | 54 +++++ src/kernel/record/record.h | 56 +++++ 15 files changed, 473 insertions(+), 41 deletions(-) create mode 100644 src/frontends/lean/structure_cmd.cpp create mode 100644 src/frontends/lean/structure_cmd.h create mode 100644 src/kernel/record/CMakeLists.txt create mode 100644 src/kernel/record/record.cpp create mode 100644 src/kernel/record/record.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0da367f8f0..2b624fc113 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -241,6 +241,8 @@ add_subdirectory(kernel) set(LEAN_LIBS ${LEAN_LIBS} kernel) add_subdirectory(kernel/inductive) set(LEAN_LIBS ${LEAN_LIBS} inductive) +add_subdirectory(kernel/record) +set(LEAN_LIBS ${LEAN_LIBS} record) add_subdirectory(library) set(LEAN_LIBS ${LEAN_LIBS} library) # add_subdirectory(library/rewriter) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index c82f298bc8..df7a56d4d8 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -30,7 +30,7 @@ (define-generic-mode 'lean-mode ;; name of the mode to create '("--") ;; comments start with - '("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "renaming" "inline" "hiding" "exposing" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "private" "using" "namespace" "builtin" "including" "class" "instance" "section" "set_option" "add_rewrite") ;; some keywords + '("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "renaming" "inline" "hiding" "exposing" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "private" "using" "namespace" "builtin" "including" "class" "instance" "section" "set_option" "add_rewrite" "extends") ;; some keywords '(("\\_<\\(bool\\|int\\|nat\\|real\\|Prop\\|Type\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face) ("\\_<\\(calc\\|have\\|obtains\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face) ("\"[^\"]*\"" . 'font-lock-string-face) diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index c2469bcff5..27f3622fd9 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -4,6 +4,7 @@ parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp interactive.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp proof_qed_ext.cpp -class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp) +class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp +structure_cmd.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index dfad4c52e5..fbb8fd90a2 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -21,6 +21,7 @@ Author: Leonardo de Moura #include "frontends/lean/calc.h" #include "frontends/lean/notation_cmd.h" #include "frontends/lean/inductive_cmd.h" +#include "frontends/lean/structure_cmd.h" #include "frontends/lean/proof_qed_ext.h" #include "frontends/lean/decl_cmds.h" #include "frontends/lean/class.h" @@ -302,6 +303,7 @@ cmd_table init_cmd_table() { 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_structure_cmd(r); register_notation_cmds(r); register_calc_cmds(r); register_proof_qed_cmds(r); diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 8b22746b24..2e815b8655 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -39,17 +39,6 @@ using inductive::inductive_decl_intros; using inductive::intro_rule_name; using inductive::intro_rule_type; -/** \brief Return true if \c u occurs in \c l */ -bool occurs(level const & u, level const & l) { - bool found = false; - for_each(l, [&](level const & l) { - if (found) return false; - if (l == u) { found = true; return false; } - return true; - }); - return found; -} - inductive_decl update_inductive_decl(inductive_decl const & d, expr const & t) { return inductive_decl(inductive_decl_name(d), t, inductive_decl_intros(d)); } @@ -479,23 +468,6 @@ struct inductive_cmd_fn { } } - /** \brief Create the resultant universe level using the levels computed during introduction rule elaboration */ - level mk_result_level(buffer const & r_lvls) { - bool impredicative = m_env.impredicative(); - if (r_lvls.empty()) { - return impredicative ? mk_level_one() : mk_level_zero(); - } else { - level r = r_lvls[0]; - for (unsigned i = 1; i < r_lvls.size(); i++) - r = mk_max(r, r_lvls[i]); - r = normalize(r); - if (is_not_zero(r)) - return normalize(r); - else - return impredicative ? normalize(mk_max(r, mk_level_one())) : normalize(r); - } - } - /** \brief Update the resultant universe level of the inductive datatypes using the inferred universe \c r_lvl */ void update_resultant_universe(buffer & decls, level const & r_lvl) { for (inductive_decl & d : decls) { @@ -570,7 +542,7 @@ struct inductive_cmd_fn { elaborate_intro_rules(decls, r_lvls); include_extra_univ_levels(decls, num_univ_params); if (m_infer_result_universe) { - level r_lvl = mk_result_level(r_lvls); + level r_lvl = mk_result_level(m_env, r_lvls); update_resultant_universe(decls, r_lvl); } level_param_names ls = to_list(m_levels.begin(), m_levels.end()); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 0d7b83d66e..9133984c2c 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -641,14 +641,14 @@ void parser::parse_binder_block(buffer & r, binder_info const & bi) { } } -void parser::parse_binders_core(buffer & r) { +void parser::parse_binders_core(buffer & r, buffer * nentries) { while (true) { if (curr_is_identifier()) { parse_binder_block(r, binder_info()); } else { optional bi = parse_optional_binder_info(); if (bi) { - if (!parse_local_notation_decl()) + if (!parse_local_notation_decl(nentries)) parse_binder_block(r, *bi); parse_close_binder_info(bi); } else { @@ -658,22 +658,23 @@ void parser::parse_binders_core(buffer & r) { } } -local_environment parser::parse_binders(buffer & r) { +local_environment parser::parse_binders(buffer & r, buffer * nentries) { flet save(m_env, m_env); // save environment local_expr_decls::mk_scope scope(m_local_decls); unsigned old_sz = r.size(); - parse_binders_core(r); + parse_binders_core(r, nentries); if (old_sz == r.size()) throw_invalid_open_binder(pos()); return local_environment(m_env); } -bool parser::parse_local_notation_decl() { +bool parser::parse_local_notation_decl(buffer * nentries) { if (curr_is_notation_decl(*this)) { buffer new_tokens; auto ne = ::lean::parse_notation(*this, false, new_tokens); for (auto const & te : new_tokens) m_env = add_token(m_env, te); + if (nentries) nentries->push_back(ne); m_env = add_notation(m_env, ne); return true; } else { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index d7ab996db2..851b81595b 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -119,7 +119,9 @@ class parser { expr parse_string_expr(); expr parse_binder_core(binder_info const & bi); void parse_binder_block(buffer & r, binder_info const & bi); - void parse_binders_core(buffer & r); + void parse_binders_core(buffer & r, buffer * nentries); + local_environment parse_binders(buffer & r, buffer * nentries); + bool parse_local_notation_decl(buffer * entries); friend environment section_cmd(parser & p); friend environment end_scoped_cmd(parser & p); @@ -209,12 +211,13 @@ public: unsigned parse_small_nat(); double parse_double(); - bool parse_local_notation_decl(); + bool parse_local_notation_decl() { return parse_local_notation_decl(nullptr); } level parse_level(unsigned rbp = 0); expr parse_binder(); - local_environment parse_binders(buffer & r); + local_environment parse_binders(buffer & r) { return parse_binders(r, nullptr); } + local_environment parse_binders(buffer & r, buffer & nentries) { return parse_binders(r, &nentries); } optional parse_optional_binder_info(); binder_info parse_binder_info(); void parse_close_binder_info(optional const & bi); diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp new file mode 100644 index 0000000000..951a1e936d --- /dev/null +++ b/src/frontends/lean/structure_cmd.cpp @@ -0,0 +1,298 @@ +/* +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 +#include +#include +#include +#include "kernel/type_checker.h" +#include "kernel/instantiate.h" +#include "kernel/replace_fn.h" +#include "kernel/record/record.h" +#include "library/scoped_ext.h" +#include "library/placeholder.h" +#include "library/locals.h" +#include "library/opaque_hints.h" +#include "frontends/lean/parser.h" +#include "frontends/lean/util.h" +#include "frontends/lean/decl_cmds.h" + +namespace lean { +static name g_assign(":="); +static name g_colon(":"); +static name g_dcolon("::"); +static name g_comma(","); +static name g_lparen("("); +static name g_rparen(")"); +static name g_arrow("->"); +static name g_extends("extends"); +static name g_renaming("renaming"); + +static name g_tmp_prefix = name::mk_internal_unique_name(); + +struct structure_cmd_fn { + typedef std::unique_ptr type_checker_ptr; + typedef std::vector> rename_vector; + parser & m_p; + environment m_env; + name_generator m_ngen; + name m_namespace; + name m_name; + buffer m_level_names; + name m_mk; + buffer m_univ_params; + buffer m_params; + expr m_type; + buffer m_parents; + buffer m_fields; + buffer m_nentries; + std::vector m_renames; + level m_u; // temporary auxiliary global universe used for inferring the result universe + bool m_infer_result_universe; + bool m_using_explicit_levels; + + structure_cmd_fn(parser & p):m_p(p), m_env(p.env()), m_ngen(p.mk_ngen()), m_namespace(get_namespace(m_env)) { + name u_name(g_tmp_prefix, "u"); + m_env = m_env.add_universe(u_name); + m_u = mk_global_univ(u_name); + m_infer_result_universe = false; + m_using_explicit_levels = false; + } + + void parse_decl_name() { + m_name = m_p.check_atomic_id_next("invalid 'structure', identifier expected"); + m_name = m_namespace + m_name; + buffer ls_buffer; + if (parse_univ_params(m_p, ls_buffer)) { + m_infer_result_universe = false; + m_level_names.append(ls_buffer); + } else { + m_infer_result_universe = true; + } + } + + void parse_params() { + if (!m_p.curr_is_token(g_extends) && !m_p.curr_is_token(g_assign)) + m_p.parse_binders(m_params); + for (expr const & l : m_params) + m_p.add_local(l); + } + + void parse_extends() { + if (m_p.curr_is_token(g_extends)) { + m_p.next(); + while (true) { + m_parents.push_back(m_p.parse_expr()); + m_renames.push_back(rename_vector()); + if (m_p.curr_is_token(g_renaming)) { + m_p.next(); + rename_vector & v = m_renames.back(); + while (!m_p.curr_is_token(g_comma)) { + name from = m_p.check_id_next("invalid 'renaming', identifier expected"); + m_p.check_token_next(g_arrow, "invalid 'renaming', '->' expected"); + name to = m_p.check_id_next("invalid 'renaming', identifier expected"); + v.emplace_back(from, to); + } + } + if (!m_p.curr_is_token(g_comma)) + break; + m_p.next(); + } + } + } + + void parse_result_type() { + auto pos = m_p.pos(); + if (m_p.curr_is_token(g_colon)) { + m_p.next(); + m_type = m_p.parse_expr(); + if (!is_sort(m_type)) + throw parser_error("invalid 'structure', 'Type' expected", pos); + } else { + m_type = m_p.save_pos(mk_sort(mk_level_placeholder()), pos); + } + } + + /** \brief Include in m_level_names any section level referenced m_type and m_fields */ + void include_section_levels() { + if (!in_section(m_env)) + return; + name_set all_lvl_params; + all_lvl_params = collect_univ_params(m_type); + for (expr const & f : m_fields) + all_lvl_params = collect_univ_params(mlocal_type(f), all_lvl_params); + buffer section_lvls; + all_lvl_params.for_each([&](name const & l) { + if (std::find(m_level_names.begin(), m_level_names.end(), l) == m_level_names.end()) + section_lvls.push_back(l); + }); + std::sort(section_lvls.begin(), section_lvls.end(), [&](name const & n1, name const & n2) { + return m_p.get_local_level_index(n1) < m_p.get_local_level_index(n2); + }); + buffer new_levels; + new_levels.append(section_lvls); + new_levels.append(m_level_names); + m_level_names.clear(); + m_level_names.append(new_levels); + } + + /** \brief Collect section local parameters used in m_params and m_fields */ + void collect_section_locals(expr_struct_set & ls) { + collect_locals(m_type, ls); + expr tmp = Pi(m_fields, Prop, m_p); // temp expr just for collecting section parameters occurring in the fields. + collect_locals(tmp, ls); + } + + /** \brief Include the used section parameters as additional arguments. + The section parameters are stored in section_params + */ + void abstract_section_locals(buffer & section_params) { + if (!in_section(m_env)) + return; + expr_struct_set section_locals; + collect_section_locals(section_locals); + if (section_locals.empty()) + return; + sort_section_params(section_locals, m_p, section_params); + m_type = Pi_as_is(section_params, m_type, m_p); + } + + /** \brief Return the universe level of the given type, if it is not a sort, then raise an exception. */ + level get_result_sort(expr d_type) { + while (is_pi(d_type)) + d_type = binding_body(d_type); + lean_assert(is_sort(d_type)); + return sort_level(d_type); + } + + /** \brief Update the result sort of the given type */ + expr update_result_sort(expr 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(); + } + } + + void elaborate_type() { + level l = get_result_sort(m_type); + if (is_placeholder(l)) { + if (m_using_explicit_levels) + throw parser_error("resultant universe must be provided, when using explicit universe levels", m_p.pos()); + m_type = update_result_sort(m_type, m_u); + m_infer_result_universe = true; + } + level_param_names ls; + std::tie(m_type, ls) = m_p.elaborate_at(m_env, m_type); + to_buffer(ls, m_level_names); + } + + void add_tmp_record_decl() { + m_env = m_env.add(check(m_env, mk_var_decl(m_name, to_list(m_level_names.begin(), m_level_names.end()), m_type))); + } + + levels to_levels(buffer const & lvl_names) { + buffer ls; + for (name const & n : lvl_names) ls.push_back(mk_param_univ(n)); + return to_list(ls.begin(), ls.end()); + } + + expr elaborate_intro(buffer & params) { + expr t = m_type; + while (is_pi(t)) { + expr p = mk_local(binding_name(t), binding_domain(t), binding_info(t)); + t = instantiate(binding_body(t), p); + params.push_back(p); + } + levels lvls = to_levels(m_level_names); + expr intro_type = mk_app(mk_constant(m_name, lvls), params); + intro_type = Pi(m_fields, intro_type, m_p); + intro_type = Pi_as_is(params, intro_type, m_p); + level_param_names new_ls; + std::tie(intro_type, new_ls) = m_p.elaborate_at(m_env, intro_type); + for (name const & l : new_ls) + m_level_names.push_back(l); + if (!empty(new_ls)) { + // replace mk_constant(m_name, lvls) with mk_constant(m_name, new_lvls) + levels new_lvls = to_levels(m_level_names); + intro_type = replace(intro_type, [&](expr const & e) { + if (is_constant(e) && const_name(e) == m_name) { + return some_expr(mk_constant(m_name, new_lvls)); + } else { + return none_expr(); + } + }); + } + return intro_type; + } + + /** \brief Traverse the introduction rule type and collect the universes where non-parameters reside in \c r_lvls. + This information is used to compute the resultant universe level for the inductive datatype declaration. + */ + void accumulate_levels(expr intro_type, unsigned num_params, buffer & r_lvls) { + auto tc = mk_type_checker_with_hints(m_env, m_p.mk_ngen(), false); + unsigned i = 0; + while (is_pi(intro_type)) { + if (i >= num_params) { + expr s = tc->ensure_type(binding_domain(intro_type)); + level l = sort_level(s); + if (l == m_u) { + // ignore, this is the auxiliary level + } else if (occurs(m_u, l)) { + throw exception("failed to infer record resultant universe, provide the universe levels explicitly"); + } else if (std::find(r_lvls.begin(), r_lvls.end(), l) == r_lvls.end()) { + r_lvls.push_back(l); + } + } + intro_type = instantiate(binding_body(intro_type), + mk_local(m_p.mk_fresh_name(), binding_name(intro_type), binding_domain(intro_type), binding_info(intro_type))); + i++; + } + } + + environment operator()() { + parser::local_scope scope(m_p); + parse_decl_name(); + parse_params(); + parse_extends(); + // TODO(Leo): process extends + parse_result_type(); + m_p.check_token_next(g_assign, "invalid 'structure', ':=' expected"); + m_mk = m_p.check_atomic_id_next("invalid 'structure', identifier expected"); + m_p.check_token_next(g_dcolon, "invalid 'structure', '::' expected"); + m_p.parse_binders(m_fields, m_nentries); + m_type = Pi(m_params, m_type, m_p); + include_section_levels(); + buffer section_params; + abstract_section_locals(section_params); + elaborate_type(); + add_tmp_record_decl(); + buffer all_params; + expr intro_type = elaborate_intro(all_params); + if (m_infer_result_universe) { + buffer r_lvls; + unsigned num_params = all_params.size(); + accumulate_levels(intro_type, num_params, r_lvls); + level r_lvl = mk_result_level(m_env, r_lvls); + m_type = update_result_sort(m_type, r_lvl); + } + m_env = record::add_record(m_p.env(), to_list(m_level_names.begin(), m_level_names.end()), m_name, m_type, + m_mk, intro_type); + // TODO(Leo): create aliases, declare notation, create to_parent methods. + return m_env; + } +}; + +environment structure_cmd(parser & p) { + return structure_cmd_fn(p)(); +} + +void register_structure_cmd(cmd_table & r) { + add_cmd(r, cmd_info("structure", "declare a new structure/record type", structure_cmd)); +} +} diff --git a/src/frontends/lean/structure_cmd.h b/src/frontends/lean/structure_cmd.h new file mode 100644 index 0000000000..55b82d31f5 --- /dev/null +++ b/src/frontends/lean/structure_cmd.h @@ -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_structure_cmd(cmd_table & r); +} diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index d00c50b3e8..385662c422 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -68,14 +68,14 @@ token_table init_token_table() { {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"obtain", 0}, {"by", 0}, {"then", 0}, {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec}, {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type'", g_max_prec}, - {"|", 0}, {"!", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, + {"|", 0}, {"!", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}}; char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion", "variables", "[private]", "[inline]", "[fact]", "[instance]", "[class]", "[module]", "[coercion]", "abbreviation", "opaque_hint", "evaluate", "check", "print", "end", "namespace", "section", "import", - "abbreviation", "inductive", "record", "structure", "module", "universe", + "abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe", "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "exit", "set_option", "using", "calc_subst", "calc_refl", "calc_trans", "tactic_hint", "add_proof_qed", "set_proof_qed", "#setline", "class", "instance", nullptr}; diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index f9e4bf6de2..42cf0c8092 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -100,4 +100,30 @@ expr Fun_as_is(buffer const & locals, expr const & e, parser & p) { expr Pi_as_is(buffer const & locals, expr const & e, parser & p) { return p.rec_save_pos(mk_binding_as_is(locals.size(), locals.data(), e), p.pos_of(e)); } + +level mk_result_level(environment const & env, buffer const & r_lvls) { + bool impredicative = env.impredicative(); + if (r_lvls.empty()) { + return impredicative ? mk_level_one() : mk_level_zero(); + } else { + level r = r_lvls[0]; + for (unsigned i = 1; i < r_lvls.size(); i++) + r = mk_max(r, r_lvls[i]); + r = normalize(r); + if (is_not_zero(r)) + return normalize(r); + else + return impredicative ? normalize(mk_max(r, mk_level_one())) : normalize(r); + } +} + +bool occurs(level const & u, level const & l) { + bool found = false; + for_each(l, [&](level const & l) { + if (found) return false; + if (l == u) { found = true; return false; } + return true; + }); + return found; +} } diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index c2ed2428b0..a5aa5381f3 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -28,4 +28,8 @@ expr Pi(buffer const & locals, expr const & e, parser & p); expr Fun_as_is(buffer const & locals, expr const & e, parser & p); /** \brief Similar to Pi(locals, e, p), but the types are marked as 'as-is' (i.e., they are not processed by the elaborator. */ expr Pi_as_is(buffer const & locals, expr const & e, parser & p); +/** \brief Create the resultant universe level using the levels computed during introduction rule elaboration */ +level mk_result_level(environment const & env, buffer const & r_lvls); +/** \brief Return true if \c u occurs in \c l */ +bool occurs(level const & u, level const & l); } diff --git a/src/kernel/record/CMakeLists.txt b/src/kernel/record/CMakeLists.txt new file mode 100644 index 0000000000..c64a45e472 --- /dev/null +++ b/src/kernel/record/CMakeLists.txt @@ -0,0 +1,2 @@ +add_library(record record.cpp) +target_link_libraries(record ${LEAN_LIBS}) diff --git a/src/kernel/record/record.cpp b/src/kernel/record/record.cpp new file mode 100644 index 0000000000..850cafa46e --- /dev/null +++ b/src/kernel/record/record.cpp @@ -0,0 +1,54 @@ +/* +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 +#include "kernel/type_checker.h" +#include "kernel/record/record.h" + +namespace lean { namespace record { +static name g_tmp_prefix = name::mk_internal_unique_name(); + +/** \brief Environment extension used to store record information */ +struct record_env_ext : public environment_extension { + struct record_info { + list m_fields; + }; + + // mapping from introduction rule name to computation rule data + rb_map m_record_info; + record_env_ext() {} +}; + +/** \brief Helper functional object for processing record declarations. */ +struct add_record_fn { + typedef std::unique_ptr type_checker_ptr; + environment m_env; + name_generator m_ngen; + type_checker_ptr m_tc; + level_param_names const & m_level_params; + name const & m_record_name; + expr const & m_record_type; + name const & m_intro_name; + expr const & m_intro_type; + add_record_fn(environment const & env, level_param_names const & level_params, name const & rec_name, expr const & rec_type, + name const & intro_name, expr const & intro_type): + m_env(env), m_ngen(g_tmp_prefix), m_tc(new type_checker(m_env)), + m_level_params(level_params), m_record_name(rec_name), m_record_type(rec_type), + m_intro_name(intro_name), m_intro_type(intro_type) {} + + environment operator()() { + // TODO(Leo): + std::cout << m_record_name << " : " << m_record_type << "\n"; + std::cout << " >> " << m_intro_name << " : " << m_intro_type << "\n"; + return m_env; + } +}; + +environment add_record(environment const & env, level_param_names const & level_params, name const & rec_name, expr const & rec_type, + name const & intro_name, expr const & intro_type) { + return add_record_fn(env, level_params, rec_name, rec_type, intro_name, intro_type)(); +} +}} diff --git a/src/kernel/record/record.h b/src/kernel/record/record.h new file mode 100644 index 0000000000..4e2f5b5ad1 --- /dev/null +++ b/src/kernel/record/record.h @@ -0,0 +1,56 @@ +/* +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 +#include +#include "util/list.h" +#include "util/optional.h" +#include "kernel/environment.h" + +namespace lean { namespace record { +typedef std::pair field; +inline name const & field_name(field const & f) { return f.first; } +inline expr const & field_type(field const & f) { return f.second; } + +/** \brief Declare a record type. */ +environment add_record(environment const & env, + level_param_names const & level_params, + name const & rec_name, + expr const & rec_type, + name const & intro_name, + expr const & intro_type); + +/** \brief Normalizer extension for applying record computational rules. */ +class record_normalizer_extension : public normalizer_extension { +public: + virtual optional operator()(expr const & e, extension_context & ctx) const; + virtual bool may_reduce_later(expr const & e, extension_context & ctx) const; +}; + +/** \brief If \c n is the name of a record in the environment \c env, then return the + list of all fields. Return none otherwise +*/ +optional> is_record(environment const & env, name const & n); + +/** \brief If \c n is the name of a record's field in \c env, then return the name of the record type + associated with it. +*/ +optional is_field(environment const & env, name const & n); + +/** \brief If \c n is the name of an introduction rule for a record in \c env, then return the name of the record type + associated with it. +*/ +optional is_intro_rule(environment const & env, name const & n); + +/** \brief If \c n is the name of an elimination rule for a record in \c env, then return the name of the record type + associated with it. +*/ +optional is_elim_rule(environment const & env, name const & n); + +/** \brief Given the eliminator \c n, this function return the position of major premise */ +optional get_elim_major_idx(environment const & env, name const & n); +}}