diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean index 64096c3609..5c706c7af7 100644 --- a/library/init/datatypes.lean +++ b/library/init/datatypes.lean @@ -397,7 +397,7 @@ attribute [instance] definition nat_has_sizeof : has_sizeof nat := has_sizeof.mk (λ a, a) -attribute [simp, defeq] +attribute [simp, defeq, simp.sizeof] definition sizeof_nat_eq (a : nat) : sizeof a = a := rfl @@ -405,7 +405,7 @@ attribute [instance] definition prod_has_sizeof (A B : Type) [has_sizeof A] [has_sizeof B] : has_sizeof (prod A B) := has_sizeof.mk (λ p, prod.cases_on p (λ a b, sizeof a + sizeof b + 1)) -attribute [simp, defeq] +attribute [simp, defeq, simp.sizeof] definition sizeof_prod_eq {A B : Type} [has_sizeof A] [has_sizeof B] (a : A) (b : B) : sizeof (prod.mk a b) = sizeof a + sizeof b + 1 := rfl @@ -413,11 +413,11 @@ attribute [instance] definition sum_has_sizeof (A B : Type) [has_sizeof A] [has_sizeof B] : has_sizeof (sum A B) := has_sizeof.mk (λ s, sum.cases_on s (λ a, sizeof a + 1) (λ b, sizeof b + 1)) -attribute [simp, defeq] +attribute [simp, defeq, simp.sizeof] definition sizeof_sum_eq_left {A B : Type} [has_sizeof A] [has_sizeof B] (a : A) : sizeof (@sum.inl A B a) = sizeof a + 1 := rfl -attribute [simp, defeq] +attribute [simp, defeq, simp.sizeof] definition sizeof_sum_eq_right {A B : Type} [has_sizeof A] [has_sizeof B] (b : B) : sizeof (@sum.inr A B b) = sizeof b + 1 := rfl @@ -425,7 +425,7 @@ attribute [instance] definition sigma_has_sizeof (A : Type) (B : A → Type) [has_sizeof A] [∀ a, has_sizeof (B a)] : has_sizeof (sigma B) := has_sizeof.mk (λ p, sigma.cases_on p (λ a b, sizeof a + sizeof b + 1)) -attribute [simp, defeq] +attribute [simp, defeq, simp.sizeof] definition sizeof_sigma_eq {A : Type} {B : A → Type} [has_sizeof A] [∀ a, has_sizeof (B a)] (a : A) (b : B a) : sizeof (@sigma.mk A B a b) = sizeof a + sizeof b + 1 := rfl @@ -433,7 +433,7 @@ attribute [instance] definition unit_has_sizeof : has_sizeof unit := has_sizeof.mk (λ u, 1) -attribute [simp, defeq] +attribute [simp, defeq, simp.sizeof] definition sizeof_unit_eq (u : unit) : sizeof u = 1 := rfl @@ -441,7 +441,7 @@ attribute [instance] definition poly_unit_has_sizeof : has_sizeof poly_unit := has_sizeof.mk (λ u, 1) -attribute [simp, defeq] +attribute [simp, defeq, simp.sizeof] definition sizeof_poly_unit_eq (u : poly_unit) : sizeof u = 1 := rfl @@ -449,7 +449,7 @@ attribute [instance] definition bool_has_sizeof : has_sizeof bool := has_sizeof.mk (λ u, 1) -attribute [simp, defeq] +attribute [simp, defeq, simp.sizeof] definition sizeof_bool_eq (b : bool) : sizeof b = 1 := rfl @@ -457,7 +457,7 @@ attribute [instance] definition pos_num_has_sizeof : has_sizeof pos_num := has_sizeof.mk (λ p, nat.of_pos_num p) -attribute [simp, defeq] +attribute [simp, defeq, simp.sizeof] definition sizeof_pos_num_eq (p : pos_num) : sizeof p = nat.of_pos_num p := rfl @@ -465,7 +465,7 @@ attribute [instance] definition num_has_sizeof : has_sizeof num := has_sizeof.mk (λ p, nat.of_num p) -attribute [simp, defeq] +attribute [simp, defeq, simp.sizeof] definition sizeof_num_eq (n : num) : sizeof n = nat.of_num n := rfl @@ -473,11 +473,11 @@ attribute [instance] definition option_has_sizeof (A : Type) [has_sizeof A] : has_sizeof (option A) := has_sizeof.mk (λ o, option.cases_on o 1 (λ a, sizeof a + 1)) -attribute [simp, defeq] +attribute [simp, defeq, simp.sizeof] definition sizeof_option_none_eq (A : Type) [has_sizeof A] : sizeof (@none A) = 1 := rfl -attribute [simp, defeq] +attribute [simp, defeq, simp.sizeof] definition sizeof_option_some_eq {A : Type} [has_sizeof A] (a : A) : sizeof (some a) = sizeof a + 1 := rfl @@ -485,10 +485,10 @@ attribute [instance] definition list_has_sizeof (A : Type) [has_sizeof A] : has_sizeof (list A) := has_sizeof.mk (λ l, list.rec_on l 1 (λ a t ih, sizeof a + ih + 1)) -attribute [simp, defeq] +attribute [simp, defeq, simp.sizeof] definition sizeof_list_nil_eq (A : Type) [has_sizeof A] : sizeof (@list.nil A) = 1 := rfl -attribute [simp, defeq] +attribute [simp, defeq, simp.sizeof] definition sizeof_list_cons_eq {A : Type} [has_sizeof A] (a : A) (l : list A) : sizeof (list.cons a l) = sizeof a + sizeof l + 1 := rfl diff --git a/library/init/logic.lean b/library/init/logic.lean index 062f457e51..0d440689a7 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -52,7 +52,6 @@ assume Hna : ¬a, absurd Ha Hna theorem false.elim {c : Prop} (H : false) : c := false.rec c H - /- eq -/ -- proof irrelevance is built in diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 0de5f9546b..e750754343 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -28,12 +28,7 @@ Authors: Daniel Selsam, Leonardo de Moura #include "library/trace.h" #include "library/app_builder.h" #include "library/type_context.h" -#include "library/constructions/rec_on.h" -#include "library/constructions/induction_on.h" -#include "library/constructions/cases_on.h" -#include "library/constructions/brec_on.h" -#include "library/constructions/no_confusion.h" -#include "library/inductive_compiler/compiler.h" +#include "library/inductive_compiler/add_decl.h" #include "frontends/lean/decl_cmds.h" #include "frontends/lean/decl_util.h" #include "frontends/lean/util.h" @@ -295,6 +290,8 @@ class inductive_cmd_fn { convert_params_to_kernel(elab, elab_params, new_params); + level result_level; + bool first = true; for (expr const & ind : inds) { expr new_ind_type = mlocal_type(ind); if (is_placeholder(new_ind_type)) @@ -306,6 +303,14 @@ class inductive_cmd_fn { new_ind_type = update_result_sort(new_ind_type, m_u); m_infer_result_universe = true; } + if (first) { + result_level = l; + first = false; + } else { + if (!is_placeholder(l) && result_level != l) { + throw_error("mutually inductive types must live in the same universe"); + } + } new_inds.push_back(update_mlocal(ind, elab.elaborate(replace_locals(new_ind_type, params_no_inds, new_params)))); } @@ -359,14 +364,17 @@ class inductive_cmd_fn { new_params.push_back(all_exprs[i]); } - // TODO(dhs): I don't think we actually need to keep replacing all the locals, as long as the names are the same - m_env = m_env.remove_universe(tmp_global_univ_name()); + // We replace the inds appearing in the types of introduction rules with constants + buffer c_inds; + for (expr const & ind : inds) { + c_inds.push_back(mk_app(mk_constant(mlocal_name(ind), param_names_to_levels(to_list(m_lp_names))), new_params)); + } + unsigned offset = offsets[0] + offsets[1]; for (unsigned i = 2; i < offsets.size(); ++i) { new_intro_rules.emplace_back(); - unsigned offset = offsets[0] + offsets[1]; for (unsigned j = 0; j < offsets[i]; ++j) { - expr new_ir = replace_locals(all_exprs[offset+j], offsets[1], all_exprs.data() + offsets[0], new_inds.data()); + expr new_ir = replace_locals(all_exprs[offset+j], offsets[1], all_exprs.data() + offsets[0], c_inds.data()); if (m_infer_result_universe) new_ir = update_mlocal(new_ir, replace_u(mlocal_type(new_ir), resultant_level)); new_intro_rules.back().push_back(new_ir); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index c059faca33..31987620f4 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -316,6 +316,7 @@ void pretty_fn::set_options_core(options const & _o) { m_private_names = get_pp_private_names(o); m_purify_metavars = get_pp_purify_metavars(o); m_purify_locals = get_pp_purify_locals(o); + m_locals_full_names = get_pp_locals_full_names(o); m_beta = get_pp_beta(o); m_numerals = get_pp_numerals(o); m_strings = get_pp_strings(o); @@ -706,7 +707,10 @@ auto pretty_fn::pp_meta(expr const & e) -> result { auto pretty_fn::pp_local(expr const & e) -> result { name n = sanitize_if_fresh(local_pp_name(e)); - return result(format(n)); + if (m_locals_full_names) + return result(format("<") + format(n + mlocal_name(e)) + format(">")); + else + return format(n); } bool pretty_fn::has_implicit_args(expr const & f) { diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index e9c66bbdee..053b8ccc01 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -65,6 +65,7 @@ private: bool m_private_names; bool m_purify_metavars; bool m_purify_locals; + bool m_locals_full_names; bool m_beta; bool m_numerals; bool m_strings; diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 2b9fa9b44e..35951ecac4 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -44,6 +44,7 @@ Author: Leonardo de Moura #include "library/constructions/cases_on.h" #include "library/constructions/projection.h" #include "library/constructions/no_confusion.h" +#include "library/inductive_compiler/add_decl.h" #include "frontends/lean/elaborator_exception.h" #include "frontends/lean/parser.h" #include "frontends/lean/util.h" @@ -718,6 +719,7 @@ struct structure_cmd_fn { add_alias(m_mk); add_rec_alias(rec_name); m_env = m_attrs.apply(m_env, m_p.ios(), m_name); + m_env = add_structure_declaration_aux(m_env, m_p.get_options(), m_level_names, m_params, mk_local(m_name, mk_structure_type()), mk_local(m_mk, mk_intro_type())); } void save_def_info(name const & n) { diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 7145a0c06f..2152171036 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -13,7 +13,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp attribute_manager.cpp error_handling.cpp unification_hint.cpp local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp - inductive.cpp mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp + mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp aux_definition.cpp inverse.cpp library_system.cpp # Legacy -- The following files will be eventually deleted diff --git a/src/library/constants.cpp b/src/library/constants.cpp index d3c0eec155..aa315e4633 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -87,6 +87,9 @@ name const * g_has_lt = nullptr; name const * g_has_neg = nullptr; name const * g_has_one = nullptr; name const * g_has_one_one = nullptr; +name const * g_has_sizeof = nullptr; +name const * g_has_sizeof_mk = nullptr; +name const * g_has_sizeof_sizeof = nullptr; name const * g_has_sub = nullptr; name const * g_has_to_string = nullptr; name const * g_has_zero = nullptr; @@ -294,6 +297,7 @@ name const * g_ring = nullptr; name const * g_select = nullptr; name const * g_semiring = nullptr; name const * g_sigma = nullptr; +name const * g_sigma_cases_on = nullptr; name const * g_sigma_mk = nullptr; name const * g_sigma_pr1 = nullptr; name const * g_sigma_pr2 = nullptr; @@ -303,6 +307,7 @@ name const * g_simplifier_congr_bin_op = nullptr; name const * g_simplifier_congr_bin_arg1 = nullptr; name const * g_simplifier_congr_bin_arg2 = nullptr; name const * g_simplifier_congr_bin_args = nullptr; +name const * g_sizeof = nullptr; name const * g_smt_array = nullptr; name const * g_smt_select = nullptr; name const * g_smt_store = nullptr; @@ -319,6 +324,10 @@ name const * g_subsingleton_helim = nullptr; name const * g_subtype_tag = nullptr; name const * g_subtype_elt_of = nullptr; name const * g_subtype_rec = nullptr; +name const * g_sum = nullptr; +name const * g_sum_cases_on = nullptr; +name const * g_sum_inl = nullptr; +name const * g_sum_inr = nullptr; name const * g_tactic = nullptr; name const * g_tactic_try = nullptr; name const * g_tactic_constructor = nullptr; @@ -334,6 +343,7 @@ name const * g_unification_hint_mk = nullptr; name const * g_unification_constraint = nullptr; name const * g_unification_constraint_mk = nullptr; name const * g_unit = nullptr; +name const * g_unit_cases_on = nullptr; name const * g_unit_star = nullptr; name const * g_user_attribute = nullptr; name const * g_weak_order = nullptr; @@ -428,6 +438,9 @@ void initialize_constants() { g_has_neg = new name{"has_neg"}; g_has_one = new name{"has_one"}; g_has_one_one = new name{"has_one", "one"}; + g_has_sizeof = new name{"has_sizeof"}; + g_has_sizeof_mk = new name{"has_sizeof", "mk"}; + g_has_sizeof_sizeof = new name{"has_sizeof", "sizeof"}; g_has_sub = new name{"has_sub"}; g_has_to_string = new name{"has_to_string"}; g_has_zero = new name{"has_zero"}; @@ -635,6 +648,7 @@ void initialize_constants() { g_select = new name{"select"}; g_semiring = new name{"semiring"}; g_sigma = new name{"sigma"}; + g_sigma_cases_on = new name{"sigma", "cases_on"}; g_sigma_mk = new name{"sigma", "mk"}; g_sigma_pr1 = new name{"sigma", "pr1"}; g_sigma_pr2 = new name{"sigma", "pr2"}; @@ -644,6 +658,7 @@ void initialize_constants() { g_simplifier_congr_bin_arg1 = new name{"simplifier", "congr_bin_arg1"}; g_simplifier_congr_bin_arg2 = new name{"simplifier", "congr_bin_arg2"}; g_simplifier_congr_bin_args = new name{"simplifier", "congr_bin_args"}; + g_sizeof = new name{"sizeof"}; g_smt_array = new name{"smt", "array"}; g_smt_select = new name{"smt", "select"}; g_smt_store = new name{"smt", "store"}; @@ -660,6 +675,10 @@ void initialize_constants() { g_subtype_tag = new name{"subtype", "tag"}; g_subtype_elt_of = new name{"subtype", "elt_of"}; g_subtype_rec = new name{"subtype", "rec"}; + g_sum = new name{"sum"}; + g_sum_cases_on = new name{"sum", "cases_on"}; + g_sum_inl = new name{"sum", "inl"}; + g_sum_inr = new name{"sum", "inr"}; g_tactic = new name{"tactic"}; g_tactic_try = new name{"tactic", "try"}; g_tactic_constructor = new name{"tactic", "constructor"}; @@ -675,6 +694,7 @@ void initialize_constants() { g_unification_constraint = new name{"unification_constraint"}; g_unification_constraint_mk = new name{"unification_constraint", "mk"}; g_unit = new name{"unit"}; + g_unit_cases_on = new name{"unit", "cases_on"}; g_unit_star = new name{"unit", "star"}; g_user_attribute = new name{"user_attribute"}; g_weak_order = new name{"weak_order"}; @@ -770,6 +790,9 @@ void finalize_constants() { delete g_has_neg; delete g_has_one; delete g_has_one_one; + delete g_has_sizeof; + delete g_has_sizeof_mk; + delete g_has_sizeof_sizeof; delete g_has_sub; delete g_has_to_string; delete g_has_zero; @@ -977,6 +1000,7 @@ void finalize_constants() { delete g_select; delete g_semiring; delete g_sigma; + delete g_sigma_cases_on; delete g_sigma_mk; delete g_sigma_pr1; delete g_sigma_pr2; @@ -986,6 +1010,7 @@ void finalize_constants() { delete g_simplifier_congr_bin_arg1; delete g_simplifier_congr_bin_arg2; delete g_simplifier_congr_bin_args; + delete g_sizeof; delete g_smt_array; delete g_smt_select; delete g_smt_store; @@ -1002,6 +1027,10 @@ void finalize_constants() { delete g_subtype_tag; delete g_subtype_elt_of; delete g_subtype_rec; + delete g_sum; + delete g_sum_cases_on; + delete g_sum_inl; + delete g_sum_inr; delete g_tactic; delete g_tactic_try; delete g_tactic_constructor; @@ -1017,6 +1046,7 @@ void finalize_constants() { delete g_unification_constraint; delete g_unification_constraint_mk; delete g_unit; + delete g_unit_cases_on; delete g_unit_star; delete g_user_attribute; delete g_weak_order; @@ -1111,6 +1141,9 @@ name const & get_has_lt_name() { return *g_has_lt; } name const & get_has_neg_name() { return *g_has_neg; } name const & get_has_one_name() { return *g_has_one; } name const & get_has_one_one_name() { return *g_has_one_one; } +name const & get_has_sizeof_name() { return *g_has_sizeof; } +name const & get_has_sizeof_mk_name() { return *g_has_sizeof_mk; } +name const & get_has_sizeof_sizeof_name() { return *g_has_sizeof_sizeof; } name const & get_has_sub_name() { return *g_has_sub; } name const & get_has_to_string_name() { return *g_has_to_string; } name const & get_has_zero_name() { return *g_has_zero; } @@ -1318,6 +1351,7 @@ name const & get_ring_name() { return *g_ring; } name const & get_select_name() { return *g_select; } name const & get_semiring_name() { return *g_semiring; } name const & get_sigma_name() { return *g_sigma; } +name const & get_sigma_cases_on_name() { return *g_sigma_cases_on; } name const & get_sigma_mk_name() { return *g_sigma_mk; } name const & get_sigma_pr1_name() { return *g_sigma_pr1; } name const & get_sigma_pr2_name() { return *g_sigma_pr2; } @@ -1327,6 +1361,7 @@ name const & get_simplifier_congr_bin_op_name() { return *g_simplifier_congr_bin name const & get_simplifier_congr_bin_arg1_name() { return *g_simplifier_congr_bin_arg1; } name const & get_simplifier_congr_bin_arg2_name() { return *g_simplifier_congr_bin_arg2; } name const & get_simplifier_congr_bin_args_name() { return *g_simplifier_congr_bin_args; } +name const & get_sizeof_name() { return *g_sizeof; } name const & get_smt_array_name() { return *g_smt_array; } name const & get_smt_select_name() { return *g_smt_select; } name const & get_smt_store_name() { return *g_smt_store; } @@ -1343,6 +1378,10 @@ name const & get_subsingleton_helim_name() { return *g_subsingleton_helim; } name const & get_subtype_tag_name() { return *g_subtype_tag; } name const & get_subtype_elt_of_name() { return *g_subtype_elt_of; } name const & get_subtype_rec_name() { return *g_subtype_rec; } +name const & get_sum_name() { return *g_sum; } +name const & get_sum_cases_on_name() { return *g_sum_cases_on; } +name const & get_sum_inl_name() { return *g_sum_inl; } +name const & get_sum_inr_name() { return *g_sum_inr; } name const & get_tactic_name() { return *g_tactic; } name const & get_tactic_try_name() { return *g_tactic_try; } name const & get_tactic_constructor_name() { return *g_tactic_constructor; } @@ -1358,6 +1397,7 @@ name const & get_unification_hint_mk_name() { return *g_unification_hint_mk; } name const & get_unification_constraint_name() { return *g_unification_constraint; } name const & get_unification_constraint_mk_name() { return *g_unification_constraint_mk; } name const & get_unit_name() { return *g_unit; } +name const & get_unit_cases_on_name() { return *g_unit_cases_on; } name const & get_unit_star_name() { return *g_unit_star; } name const & get_user_attribute_name() { return *g_user_attribute; } name const & get_weak_order_name() { return *g_weak_order; } diff --git a/src/library/constants.h b/src/library/constants.h index 59b5a17f9d..61ebb2aa30 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -89,6 +89,9 @@ name const & get_has_lt_name(); name const & get_has_neg_name(); name const & get_has_one_name(); name const & get_has_one_one_name(); +name const & get_has_sizeof_name(); +name const & get_has_sizeof_mk_name(); +name const & get_has_sizeof_sizeof_name(); name const & get_has_sub_name(); name const & get_has_to_string_name(); name const & get_has_zero_name(); @@ -296,6 +299,7 @@ name const & get_ring_name(); name const & get_select_name(); name const & get_semiring_name(); name const & get_sigma_name(); +name const & get_sigma_cases_on_name(); name const & get_sigma_mk_name(); name const & get_sigma_pr1_name(); name const & get_sigma_pr2_name(); @@ -305,6 +309,7 @@ name const & get_simplifier_congr_bin_op_name(); name const & get_simplifier_congr_bin_arg1_name(); name const & get_simplifier_congr_bin_arg2_name(); name const & get_simplifier_congr_bin_args_name(); +name const & get_sizeof_name(); name const & get_smt_array_name(); name const & get_smt_select_name(); name const & get_smt_store_name(); @@ -321,6 +326,10 @@ name const & get_subsingleton_helim_name(); name const & get_subtype_tag_name(); name const & get_subtype_elt_of_name(); name const & get_subtype_rec_name(); +name const & get_sum_name(); +name const & get_sum_cases_on_name(); +name const & get_sum_inl_name(); +name const & get_sum_inr_name(); name const & get_tactic_name(); name const & get_tactic_try_name(); name const & get_tactic_constructor_name(); @@ -336,6 +345,7 @@ name const & get_unification_hint_mk_name(); name const & get_unification_constraint_name(); name const & get_unification_constraint_mk_name(); name const & get_unit_name(); +name const & get_unit_cases_on_name(); name const & get_unit_star_name(); name const & get_user_attribute_name(); name const & get_weak_order_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 5f32628974..543dec2154 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -82,6 +82,9 @@ has_lt has_neg has_one has_one.one +has_sizeof +has_sizeof.mk +has_sizeof.sizeof has_sub has_to_string has_zero @@ -289,6 +292,7 @@ ring select semiring sigma +sigma.cases_on sigma.mk sigma.pr1 sigma.pr2 @@ -298,6 +302,7 @@ simplifier.congr_bin_op simplifier.congr_bin_arg1 simplifier.congr_bin_arg2 simplifier.congr_bin_args +sizeof smt.array smt.select smt.store @@ -314,6 +319,10 @@ subsingleton.helim subtype.tag subtype.elt_of subtype.rec +sum +sum.cases_on +sum.inl +sum.inr tactic tactic.try tactic.constructor @@ -329,6 +338,7 @@ unification_hint.mk unification_constraint unification_constraint.mk unit +unit.cases_on unit.star user_attribute weak_order diff --git a/src/library/constructions/CMakeLists.txt b/src/library/constructions/CMakeLists.txt index 0cd5d6bce6..b84c1e8f40 100644 --- a/src/library/constructions/CMakeLists.txt +++ b/src/library/constructions/CMakeLists.txt @@ -1,2 +1,2 @@ add_library(constructions OBJECT rec_on.cpp induction_on.cpp cases_on.cpp - no_confusion.cpp projection.cpp brec_on.cpp init_module.cpp) + no_confusion.cpp projection.cpp brec_on.cpp init_module.cpp has_sizeof.cpp) diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp index 42d0f1b42b..cb6b6f0a3c 100644 --- a/src/library/constructions/brec_on.cpp +++ b/src/library/constructions/brec_on.cpp @@ -41,7 +41,7 @@ static optional is_typeformer_app(buffer const & typeformer_name static environment mk_below(environment const & env, name const & n, bool ibelow) { if (!is_recursive_datatype(env, n)) return env; - if (is_inductive_predicate(env, n)) + if (is_inductive_predicate(env, n) || !can_elim_to_type(env, n)) return env; inductive::inductive_decls decls = *inductive::is_inductive_decl(env, n); type_checker tc(env); @@ -161,7 +161,7 @@ environment mk_ibelow(environment const & env, name const & n) { static environment mk_brec_on(environment const & env, name const & n, bool ind) { if (!is_recursive_datatype(env, n)) return env; - if (is_inductive_predicate(env, n)) + if (is_inductive_predicate(env, n) || !can_elim_to_type(env, n)) return env; inductive::inductive_decls decls = *inductive::is_inductive_decl(env, n); type_checker tc(env); diff --git a/src/library/constructions/has_sizeof.cpp b/src/library/constructions/has_sizeof.cpp new file mode 100644 index 0000000000..54a516b62d --- /dev/null +++ b/src/library/constructions/has_sizeof.cpp @@ -0,0 +1,319 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#include +#include "util/sstream.h" +#include "util/fresh_name.h" +#include "kernel/environment.h" +#include "kernel/type_checker.h" +#include "kernel/instantiate.h" +#include "kernel/abstract.h" +#include "kernel/find_fn.h" +#include "kernel/inductive/inductive.h" +#include "library/attribute_manager.h" +#include "library/type_context.h" +#include "library/protected.h" +#include "library/local_context.h" +#include "library/app_builder.h" +#include "library/util.h" +#include "library/class.h" +#include "library/trace.h" +#include "library/module.h" +#include "library/constants.h" +#include "library/tactic/simplifier/simp_lemmas.h" +#include "library/constructions/has_sizeof.h" + +namespace lean { + +static name * g_simp_sizeof = nullptr; + +static basic_attribute const & get_simp_sizeof_attribute() { + return static_cast(get_system_attribute(*g_simp_sizeof)); +} + +environment set_simp_sizeof(environment const & env, name const & n) { + return get_simp_sizeof_attribute().set(env, get_dummy_ios(), n, LEAN_DEFAULT_PRIORITY, true); +} + +name mk_has_sizeof_name(name const & ind_name) { + return ind_name + "has_sizeof_inst"; +} + +name mk_sizeof_spec_name(name const & ir_name) { + return ir_name + "sizeof_spec"; +} + +// TODO(dhs): Put these in one place and stop copying them +static expr mk_local_for(expr const & b) { return mk_local(mk_fresh_name(), binding_name(b), binding_domain(b), binding_info(b)); } +static expr mk_local_pp(name const & n, expr const & ty) { return mk_local(mk_fresh_name(), n, ty, binder_info()); } + +class mk_has_sizeof_fn { + environment m_env; + type_context m_tctx; + name m_ind_name; + + optional mk_has_sizeof(expr const & type) { + level l = get_level(m_tctx, type); + expr inst_type = mk_app(mk_constant(get_has_sizeof_name(), {l}), type); + return m_tctx.mk_class_instance(inst_type); + } + + optional build_has_sizeof_argument_type(expr const & param) { + expr ty = m_tctx.relaxed_whnf(m_tctx.infer(param)); + buffer locals; + while (is_pi(ty)) { + expr local = mk_local_for(ty); + locals.push_back(local); + ty = m_tctx.relaxed_whnf(instantiate(binding_body(ty), local)); + } + if (!is_sort(ty)) + return none_expr(); + level l = sort_level(ty); + return some_expr(Pi(locals, mk_app(mk_constant(get_has_sizeof_name(), {l}), + mk_app(param, locals)))); + } + + optional is_recursive_arg(expr const & arg_ty, buffer & arg_args) { + expr it = m_tctx.relaxed_whnf(arg_ty); + while (is_pi(it)) { + expr arg_arg = mk_local_for(it); + arg_args.push_back(arg_arg); + it = m_tctx.relaxed_whnf(instantiate(binding_body(it), arg_arg)); + } + expr fn = get_app_fn(it); + if (is_constant(fn) && const_name(fn) == m_ind_name) + return some_expr(it); + else + return none_expr(); + } + + void define_instance() { + auto odecls = inductive::is_inductive_decl(m_env, m_ind_name); + if (!odecls) + throw exception(sstream() << "'" << m_ind_name << "' not an inductive datatype\n"); + + if (is_inductive_predicate(m_env, m_ind_name) || !can_elim_to_type(m_env, m_ind_name)) + return; + + inductive::inductive_decls decls = *odecls; + lean_assert(length(std::get<2>(decls)) == 1); + + level_param_names lp_names = std::get<0>(decls); + unsigned num_params = std::get<1>(decls); + + inductive::inductive_decl decl = head(std::get<2>(decls)); + expr const & ind_type = inductive::inductive_decl_type(decl); + buffer intro_rules; + to_buffer(inductive::inductive_decl_intros(decl), intro_rules); + + levels lvls = param_names_to_levels(lp_names); + + name has_sizeof_name = mk_has_sizeof_name(m_ind_name); + + type_context::tmp_locals locals(m_tctx); + + buffer params; + buffer param_insts; + buffer indices; + { + expr ty = m_tctx.relaxed_whnf(ind_type); + + // 1. Create locals for the parameters of the inductive type + for (unsigned param_idx = 0; param_idx < num_params; ++param_idx) { + expr param = locals.push_local_from_binding(ty); + params.push_back(param); + ty = m_tctx.relaxed_whnf(instantiate(binding_body(ty), param)); + } + + // 2. Add extra [has_sizeof] locals for parameters returning sorts + for (expr const & param : params) { + if (auto inst_arg_type = build_has_sizeof_argument_type(param)) { + expr param_inst = locals.push_local(local_pp_name(param).append_after("_inst"), *inst_arg_type, mk_inst_implicit_binder_info()); + param_insts.push_back(param_inst); + } + } + + // 3. Collect indices + while (is_pi(ty)) { + expr index = locals.push_local_from_binding(ty); + indices.push_back(index); + ty = m_tctx.relaxed_whnf(instantiate(binding_body(ty), index)); + } + } + + expr c_ind = mk_app(mk_constant(m_ind_name, lvls), params); + + // Create a new type context so that the [has_sizeof] instances are available for type class resolution + m_tctx = type_context(m_env, options(), m_tctx.lctx()); + + expr motive; + { + expr x = mk_local_pp("x", mk_app(c_ind, indices)); + motive = m_tctx.mk_lambda(indices, Fun(x, mk_constant(get_nat_name()))); + } + + buffer minor_premises; + for (inductive::intro_rule const & ir : intro_rules) { + expr ir_ty = m_tctx.relaxed_whnf(inductive::intro_rule_type(ir)); + expr result = mk_nat_one(); + buffer locals; + buffer > rec_arg_args; + + // Skip the params + for (unsigned param_idx = 0; param_idx < num_params; ++param_idx) { + ir_ty = m_tctx.relaxed_whnf(instantiate(binding_body(ir_ty), params[param_idx])); + } + + while (is_pi(ir_ty)) { + expr local = mk_local_for(ir_ty); + locals.push_back(local); + expr arg_ty = binding_domain(ir_ty); + + buffer arg_args; + if (is_recursive_arg(arg_ty, arg_args)) { + rec_arg_args.push_back(arg_args); + } else if (auto inst = mk_has_sizeof(arg_ty)) { + level l = get_level(m_tctx, arg_ty); + result = mk_nat_add(result, mk_app(mk_constant(get_sizeof_name(), {l}), arg_ty, *inst, local)); + } + ir_ty = m_tctx.relaxed_whnf(instantiate(binding_body(ir_ty), local)); + } + + // Introduce locals for the recursive arguments of type nat + for (buffer const & arg_args : rec_arg_args) { + expr local = mk_local_pp("IH", Pi(arg_args, mk_constant(get_nat_name()))); + locals.push_back(local); + if (arg_args.empty()) + result = mk_nat_add(result, local); + } + minor_premises.push_back(Fun(locals, result)); + } + + expr recursor_application = + mk_app( + mk_app( + mk_app( + mk_app(mk_constant(inductive::get_elim_name(m_ind_name), levels(mk_level_one(), lvls)), + params), + motive), + minor_premises), + indices); + + expr has_sizeof_type = m_tctx.mk_pi(indices, + mk_app(mk_constant(get_has_sizeof_name(), {get_datatype_level(ind_type)}), + mk_app(c_ind, indices))); + + expr has_sizeof_val = m_tctx.mk_lambda(indices, + mk_app( + mk_app(mk_constant(get_has_sizeof_mk_name(), {get_datatype_level(ind_type)}), + mk_app(c_ind, indices)), + recursor_application)); + + buffer used_param_insts; + for (expr const & param_inst : param_insts) { + if (find(has_sizeof_val, [&](expr const & e, unsigned) { return e == param_inst; })) { + used_param_insts.push_back(param_inst); + } + } + + has_sizeof_type = m_tctx.mk_pi(params, m_tctx.mk_pi(used_param_insts, has_sizeof_type)); + has_sizeof_val = m_tctx.mk_lambda(params, m_tctx.mk_lambda(used_param_insts, has_sizeof_val)); + + lean_trace(name({"constructions", "has_sizeof"}), tout() + << has_sizeof_name << " : " << has_sizeof_type << "\n";); + + m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, has_sizeof_name, lp_names, has_sizeof_type, has_sizeof_val, true))); + m_env = add_instance(m_env, has_sizeof_name, LEAN_DEFAULT_PRIORITY, true); + m_env = add_protected(m_env, has_sizeof_name); + + // TODO(dhs): switch back to `set_env` once the bug is fixed + // m_tctx.set_env(m_env); + m_tctx = type_context(m_env, options(), m_tctx.lctx()); + expr c_has_sizeof = mk_app(mk_app(mk_constant(has_sizeof_name, lvls), params), used_param_insts); + + // Defeq simp lemmas + for (inductive::intro_rule const & ir : intro_rules) { + expr ir_ty = m_tctx.relaxed_whnf(inductive::intro_rule_type(ir)); + expr c_ir = mk_app(mk_constant(inductive::intro_rule_name(ir), lvls), params); + expr rhs = mk_nat_one(); + buffer locals; + + // Skip the params + for (unsigned param_idx = 0; param_idx < num_params; ++param_idx) { + ir_ty = m_tctx.relaxed_whnf(instantiate(binding_body(ir_ty), params[param_idx])); + } + + while (is_pi(ir_ty)) { + expr local = mk_local_for(ir_ty); + locals.push_back(local); + expr arg_ty = binding_domain(ir_ty); + + buffer arg_args; + if (auto ind_app = is_recursive_arg(arg_ty, arg_args)) { + if (arg_args.empty()) { + buffer ind_app_args; + get_app_args(*ind_app, ind_app_args); + expr new_val = mk_app(mk_constant(get_sizeof_name(), {get_datatype_level(ind_type)}), + {mk_app(c_ind, ind_app_args.size() - num_params, ind_app_args.data() + num_params), + mk_app(c_has_sizeof, ind_app_args.size() - num_params, ind_app_args.data() + num_params), + local}); + rhs = mk_nat_add(rhs, new_val); + } + } else if (auto inst = mk_has_sizeof(arg_ty)) { + level l = get_level(m_tctx, arg_ty); + rhs = mk_nat_add(rhs, mk_app(mk_constant(get_sizeof_name(), {l}), arg_ty, *inst, local)); + } + ir_ty = m_tctx.relaxed_whnf(instantiate(binding_body(ir_ty), local)); + } + + expr lhs = mk_app(m_tctx, get_sizeof_name(), {mk_app(c_ir, locals)}); + expr dsimp_rule_type = m_tctx.mk_pi(params, m_tctx.mk_pi(used_param_insts, Pi(locals, mk_eq(m_tctx, lhs, rhs)))); + expr dsimp_rule_val = m_tctx.mk_lambda(params, m_tctx.mk_lambda(used_param_insts, Fun(locals, mk_eq_refl(m_tctx, lhs)))); + name dsimp_rule_name = mk_sizeof_spec_name(inductive::intro_rule_name(ir)); + + m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, dsimp_rule_name, lp_names, dsimp_rule_type, dsimp_rule_val, true))); + m_env = set_simp_sizeof(m_env, dsimp_rule_name); + m_env = add_protected(m_env, dsimp_rule_name); + m_tctx.set_env(m_env); + } + } + +public: + mk_has_sizeof_fn(environment const & env, name const & ind_name): + m_env(env), m_tctx(env), m_ind_name(ind_name) {} + + environment operator()() { + if (m_env.find(get_has_sizeof_name())) + define_instance(); + return m_env; + } +}; + +name simp_sizeof_attribute_name() { + return *g_simp_sizeof; +} + +simp_lemmas get_sizeof_simp_lemmas(type_context & tctx) { + buffer simp_attrs, congr_attrs; + simp_attrs.push_back(simp_sizeof_attribute_name()); + return get_simp_lemmas(tctx, simp_attrs, congr_attrs); +} + +void initialize_has_sizeof() { + g_simp_sizeof = new name{"simp", "sizeof"}; + register_system_attribute(basic_attribute::with_check(*g_simp_sizeof, "simplification lemma", on_add_simp_lemma)); + + register_trace_class(name({"constructions", "has_sizeof"})); +} + +void finalize_has_sizeof() { + delete g_simp_sizeof; +} + +environment mk_has_sizeof(environment const & env, name const & ind_name) { + return mk_has_sizeof_fn(env, ind_name)(); +} +} diff --git a/src/library/constructions/has_sizeof.h b/src/library/constructions/has_sizeof.h new file mode 100644 index 0000000000..826259ef73 --- /dev/null +++ b/src/library/constructions/has_sizeof.h @@ -0,0 +1,24 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#pragma once +#include "kernel/environment.h" +#include "library/tactic/simplifier/simp_lemmas.h" + +namespace lean { +/** \brief Given an inductive datatype \c n in \c env, add + n.has_sizeof instance to the environment. */ +environment mk_has_sizeof(environment const & env, name const & ind_name); + +name mk_has_sizeof_name(name const & ind_name); +name mk_sizeof_spec_name(name const & ir_name); +name simp_sizeof_attribute_name(); +simp_lemmas get_sizeof_simp_lemmas(type_context & tctx); +environment set_simp_sizeof(environment const & env, name const & n); + +void initialize_has_sizeof(); +void finalize_has_sizeof(); +} diff --git a/src/library/constructions/init_module.cpp b/src/library/constructions/init_module.cpp index 028d878b14..45d704f1f3 100644 --- a/src/library/constructions/init_module.cpp +++ b/src/library/constructions/init_module.cpp @@ -5,13 +5,16 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "library/constructions/projection.h" +#include "library/constructions/has_sizeof.h" namespace lean{ void initialize_constructions_module() { initialize_def_projection(); + initialize_has_sizeof(); } void finalize_constructions_module() { + finalize_has_sizeof(); finalize_def_projection(); } } diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index 396e041c01..568d9b3881 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -29,8 +29,8 @@ optional mk_no_confusion_type(environment const & env, name const & optional decls = inductive::is_inductive_decl(env, n); if (!decls) throw exception(sstream() << "error in 'no_confusion' generation, '" << n << "' is not an inductive datatype"); - if (is_inductive_predicate(env, n)) - return optional(); // type is a proposition + if (is_inductive_predicate(env, n) || !can_elim_to_type(env, n)) + return optional(); bool impredicative = env.impredicative(); unsigned nparams = std::get<1>(*decls); declaration ind_decl = env.get(n); @@ -45,8 +45,6 @@ optional mk_no_confusion_type(environment const & env, name const & rlvl = plvl; else rlvl = mk_max(plvl, ind_lvl); - if (length(ilvls) != ind_decl.get_num_univ_params()) - return optional(); // type does not have only a restricted eliminator // All inductive datatype parameters and indices are arguments buffer args; ind_type = to_telescope(ind_type, args, some(mk_implicit_binder_info())); diff --git a/src/library/inductive.cpp b/src/library/inductive.cpp deleted file mode 100644 index 9a8eed05f0..0000000000 --- a/src/library/inductive.cpp +++ /dev/null @@ -1,42 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Daniel Selsam -*/ -#include "kernel/environment.h" -#include "library/inductive.h" - -namespace lean { - -bool is_inductive(environment const & /* env */, name const & /* ind_name */) { - throw exception("TODO(dhs): implement"); -} - -list get_intro_rule_names(environment const & /* env */, name const & /* ind_name */) { - throw exception("TODO(dhs): implement"); -} - -optional is_intro_rule_name(environment const & /* env */, name const & /* ir_name */) { - throw exception("TODO(dhs): implement"); -} - -/* For basic inductive types, we can prove this lemma using .no_confusion. - - For non-basic inductive types, we first create a function .cidx that maps - each element of \e ind_type to a natural number depending only on its constructor. - We then prove the lemma forall c1 c2, cidx c1 != cidx c2 -> c1 != c2 and - use it to prove the desired theorem. -*/ -expr prove_intro_rules_disjoint(environment const & /* env */, name const & /* ir_name1 */, name const & /* ir_name2 */) { - throw exception("TODO(dhs): implement"); -} - -unsigned get_inductive_num_params(environment const & /* env */, name const & /* ind_name */) { - throw exception("TODO(dhs): implement"); -} - -void initialize_library_inductive() {} -void finalize_library_inductive() {} - -} diff --git a/src/library/inductive.h b/src/library/inductive.h deleted file mode 100644 index 646ff97ee3..0000000000 --- a/src/library/inductive.h +++ /dev/null @@ -1,69 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Daniel Selsam -*/ -#pragma once -#include "kernel/environment.h" - -/* This file presents a unified interface to all (user-facing) inductive types, - which include the basic inductive types understood by the kernel, as well as - mutual inductive types and nested inductive types that are compiled to basic - inductive types behind the scenes. - - For every inductive type \e ind_name with intro rule \e ir_name recognized - by this module, the following are guaranteed to be in the environment: - - 1. .cases_on - 2. .size_of - 3. .has_size_of [instance] - 4. ..size_of_spec - 5. ..injective - - Suppose has parameters (A : Type) and has non-recursive arguments X - and recursive arguments Y1 ... Yn. - - Then .size_of_spec is a proof of: - - forall C A x y1 ... yn, - let k := size_of ( A x y1 ... yn) in - (k > size_of y1 -> ... -> k > size_of yn -> C) -> C - - - and .injective is a proof of: - - forall C A x y x' y', - A x y = A x' y' -> (x = x' -> y = y' -> C) -> C -*/ - -namespace lean { - -/* \brief Returns true if \e ind_name is the name of a (user-facing) inductive type, - whether it is basic, mutual, or nested. */ -bool is_inductive(environment const & env, name const & ind_name); - -/* \brief Returns the names of the introduction rules for the inductive type \e ind_name. */ -list get_intro_rule_names(environment const & env, name const & ind_name); - -/* \brief Returns the name of the inductive type if \e ir_name is indeed an introduction rule. */ -optional is_intro_rule_name(environment const & env, name const & ir_name); - -/* \brief Given the names of two introduction rules for the same inductive type, returns a - proof that they are disjoint. - - \example For an inductive type \e I with parameters (A : Type) and two introduction rules - c1 : X1 -> I and c2 : X2 -> I, returns a proof of the following theorem: - - forall (A : Type), forall (x1 : X1) (x2 : X2), @c1 A x1 = @c2 A x2 -> false. - - \remark When there are indices, the equality will need to be heterogenous. -*/ -expr prove_intro_rules_disjoint(environment const & env, name const & ir_name1, name const & ir_name2); - -/* \brief Returns the number of parameters for the given inductive type \e ind_name. */ -unsigned get_inductive_num_params(environment const & env, name const & ind_name); - -void initialize_library_inductive(); -void finalize_library_inductive(); -} diff --git a/src/library/inductive_compiler/CMakeLists.txt b/src/library/inductive_compiler/CMakeLists.txt index c67a2bf285..743d9b3f36 100644 --- a/src/library/inductive_compiler/CMakeLists.txt +++ b/src/library/inductive_compiler/CMakeLists.txt @@ -1,4 +1,10 @@ add_library(inductive_compiler OBJECT init_module.cpp compiler.cpp + add_decl.cpp + ginductive.cpp + basic.cpp + mutual.cpp + nested.cpp + util.cpp ) diff --git a/src/library/inductive_compiler/add_decl.cpp b/src/library/inductive_compiler/add_decl.cpp new file mode 100644 index 0000000000..2445b3b972 --- /dev/null +++ b/src/library/inductive_compiler/add_decl.cpp @@ -0,0 +1,42 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#include "library/inductive_compiler/ginductive.h" +#include "library/inductive_compiler/add_decl.h" +#include "library/inductive_compiler/compiler.h" +#include "library/constructions/has_sizeof.h" +#include "library/constants.h" + +namespace lean { +environment add_inductive_declaration(environment const & old_env, options const & opts, + name_map implicit_infer_map, + buffer const & lp_names, buffer const & params, + buffer const & inds, buffer > const & intro_rules) { + ginductive_decl decl(lp_names, params, inds, intro_rules); + environment env = add_inner_inductive_declaration(old_env, opts, implicit_infer_map, decl); + return env; +} + +environment add_structure_declaration_aux(environment const & env, options const & opts, + buffer const & lp_names, buffer const & params, + expr const & ind, expr const & intro_rule) { + buffer inds; + inds.push_back(ind); + + buffer > intro_rules; + intro_rules.emplace_back(); + intro_rules.back().push_back(intro_rule); + + ginductive_decl decl(lp_names, params, inds, intro_rules); + + environment new_env = env; + if (mlocal_name(ind) != get_has_sizeof_name()) + mk_has_sizeof(env, mlocal_name(ind)); + + return register_ginductive_decl(new_env, decl); +} + +} diff --git a/src/library/inductive_compiler/add_decl.h b/src/library/inductive_compiler/add_decl.h new file mode 100644 index 0000000000..240aecbb17 --- /dev/null +++ b/src/library/inductive_compiler/add_decl.h @@ -0,0 +1,22 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#pragma once +#include "kernel/environment.h" +#include "library/util.h" + +namespace lean { + +environment add_inductive_declaration(environment const & env, options const & opts, + name_map implicit_infer_map, + buffer const & lp_names, buffer const & params, + buffer const & inds, buffer > const & intro_rules); + +environment add_structure_declaration_aux(environment const & env, options const & opts, + buffer const & lp_names, buffer const & params, + expr const & ind, expr const & intro_rule); + +} diff --git a/src/library/inductive_compiler/basic.cpp b/src/library/inductive_compiler/basic.cpp new file mode 100644 index 0000000000..2d207fe23f --- /dev/null +++ b/src/library/inductive_compiler/basic.cpp @@ -0,0 +1,191 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#include "kernel/inductive/inductive.h" +#include "kernel/abstract.h" +#include "util/sexpr/option_declarations.h" +#include "library/locals.h" +#include "library/trace.h" +#include "library/module.h" +#include "library/attribute_manager.h" +#include "library/inductive_compiler/compiler.h" +#include "library/inductive_compiler/basic.h" +#include "library/inductive_compiler/util.h" +#include "library/constructions/rec_on.h" +#include "library/constructions/induction_on.h" +#include "library/constructions/cases_on.h" +#include "library/constructions/brec_on.h" +#include "library/constructions/no_confusion.h" +#include "library/constructions/has_sizeof.h" + +#ifndef LEAN_DEFAULT_XINDUCTIVE_REC_ON +#define LEAN_DEFAULT_XINDUCTIVE_REC_ON true +#endif + +#ifndef LEAN_DEFAULT_XINDUCTIVE_CASES_ON +#define LEAN_DEFAULT_XINDUCTIVE_CASES_ON true +#endif + +#ifndef LEAN_DEFAULT_XINDUCTIVE_NO_CONFUSION +#define LEAN_DEFAULT_XINDUCTIVE_NO_CONFUSION true +#endif + +#ifndef LEAN_DEFAULT_XINDUCTIVE_BREC_ON +#define LEAN_DEFAULT_XINDUCTIVE_BREC_ON true +#endif + +namespace lean { + +static name * g_inductive_rec_on = nullptr; +static name * g_inductive_cases_on = nullptr; +static name * g_inductive_no_confusion = nullptr; +static name * g_inductive_brec_on = nullptr; + +static bool get_inductive_rec_on(options const & opts) { + return opts.get_bool(*g_inductive_rec_on, LEAN_DEFAULT_XINDUCTIVE_REC_ON); +} + +static bool get_inductive_cases_on(options const & opts) { + return opts.get_bool(*g_inductive_cases_on, LEAN_DEFAULT_XINDUCTIVE_CASES_ON); +} + +static bool get_inductive_brec_on(options const & opts) { + return opts.get_bool(*g_inductive_brec_on, LEAN_DEFAULT_XINDUCTIVE_BREC_ON); +} + +static bool get_inductive_no_confusion(options const & opts) { + return opts.get_bool(*g_inductive_no_confusion, LEAN_DEFAULT_XINDUCTIVE_NO_CONFUSION); +} + +using inductive::inductive_decl; +using inductive::intro_rule; +using inductive::mk_intro_rule; + +class add_basic_inductive_decl_fn { + environment m_env; + options const & m_opts; + name_map const & m_implicit_infer_map; + ginductive_decl const & m_decl; + + void mk_basic_aux_decls() { + name ind_name = mlocal_name(m_decl.get_inds()[0]); + + bool has_unit = has_poly_unit_decls(m_env); + bool has_eq = has_eq_decls(m_env); + bool has_heq = has_heq_decls(m_env); + bool has_prod = has_prod_decls(m_env); + bool has_lift = has_lift_decls(m_env); + + bool gen_rec_on = get_inductive_rec_on(m_opts); + bool gen_brec_on = get_inductive_brec_on(m_opts); + bool gen_cases_on = get_inductive_cases_on(m_opts); + bool gen_no_confusion = get_inductive_no_confusion(m_opts); + + if (gen_rec_on) + m_env = mk_rec_on(m_env, ind_name); + + if (gen_rec_on && m_env.impredicative()) + m_env = mk_induction_on(m_env, ind_name); + + if (has_unit) { + if (gen_cases_on) + m_env = mk_cases_on(m_env, ind_name); + + if (gen_cases_on && gen_no_confusion && has_eq + && ((m_env.prop_proof_irrel() && has_heq) || (!m_env.prop_proof_irrel() && has_lift))) { + m_env = mk_no_confusion(m_env, ind_name); + } + + if (gen_brec_on && has_prod) { + m_env = mk_below(m_env, ind_name); + if (m_env.impredicative()) { + m_env = mk_ibelow(m_env, ind_name); + } + } + } + + if (gen_brec_on && has_unit && has_prod) { + m_env = mk_brec_on(m_env, ind_name); + if (m_env.impredicative()) { + m_env = mk_binduction_on(m_env, ind_name); + } + } + + m_env = mk_has_sizeof(m_env, ind_name); + } + + void send_to_kernel() { + buffer const & lp_names = m_decl.get_lp_names(); + buffer const & params = m_decl.get_params(); + expr const & ind = m_decl.get_inds()[0]; + buffer const & intro_rules = m_decl.get_intro_rules()[0]; + + expr new_ind_type = Pi(params, mlocal_type(ind)); + lean_assert(!has_local(new_ind_type)); + + lean_trace(name({"inductive_compiler", "basic", "ind"}), tout() << mlocal_name(ind) << "\n";); + + buffer new_intro_rules; + for (expr const & ir : intro_rules) { + implicit_infer_kind k = get_implicit_infer_kind(m_implicit_infer_map, mlocal_name(ir)); + expr new_ir_type = infer_implicit_params(Pi(params, mlocal_type(ir)), params.size(), k); + lean_assert(!has_local(new_ir_type)); + new_intro_rules.push_back(mk_intro_rule(mlocal_name(ir), new_ir_type)); + lean_trace(name({"inductive_compiler", "basic", "irs"}), tout() << mlocal_name(ir) << " : " << new_ir_type << "\n";); + } + inductive_decl kdecl(mlocal_name(ind), new_ind_type, to_list(new_intro_rules)); + m_env = module::add_inductive(m_env, to_list(lp_names), params.size(), list(kdecl)); + } + +public: + add_basic_inductive_decl_fn(environment const & env, options const & opts, name_map implicit_infer_map, + ginductive_decl const & decl): + m_env(env), m_opts(opts), m_implicit_infer_map(implicit_infer_map), m_decl(decl) {} + + environment operator()() { + send_to_kernel(); + mk_basic_aux_decls(); + return m_env; + } +}; + +environment add_basic_inductive_decl(environment const & env, options const & opts, name_map implicit_infer_map, + ginductive_decl const & decl) { + return add_basic_inductive_decl_fn(env, opts, implicit_infer_map, decl)(); +} + +void initialize_inductive_compiler_basic() { + register_trace_class(name({"inductive_compiler", "basic"})); + register_trace_class(name({"inductive_compiler", "basic", "ind"})); + register_trace_class(name({"inductive_compiler", "basic", "irs"})); + + g_inductive_rec_on = new name{"inductive", "rec_on"}; + g_inductive_cases_on = new name{"inductive", "cases_on"}; + g_inductive_brec_on = new name{"inductive", "brec_on"}; + g_inductive_no_confusion = new name{"inductive", "no_confusion"}; + + register_bool_option(*g_inductive_rec_on, LEAN_DEFAULT_XINDUCTIVE_REC_ON, + "(inductive) automatically generate the auxiliary declarations C.rec_on and C.induction_on for each inductive datatype C"); + + register_bool_option(*g_inductive_brec_on, LEAN_DEFAULT_XINDUCTIVE_BREC_ON, + "(inductive) automatically generate the auxiliary declaration C.brec_on for each inductive datatype C"); + + register_bool_option(*g_inductive_cases_on, LEAN_DEFAULT_XINDUCTIVE_CASES_ON, + "(inductive) automatically generate the auxiliary declaration C.cases_on for each inductive datatype C" + "(remark: if cases_on is disabled, then the auxiliary declaration C.no_confusion is also disabled"); + + register_bool_option(*g_inductive_no_confusion, LEAN_DEFAULT_XINDUCTIVE_NO_CONFUSION, + "(inductive) automatically generate the auxiliary declaration C.no_confusion for each inductive datatype C"); +} + +void finalize_inductive_compiler_basic() { + delete g_inductive_rec_on; + delete g_inductive_cases_on; + delete g_inductive_brec_on; + delete g_inductive_no_confusion; +} + +} diff --git a/src/library/inductive_compiler/basic.h b/src/library/inductive_compiler/basic.h new file mode 100644 index 0000000000..8bd60d1064 --- /dev/null +++ b/src/library/inductive_compiler/basic.h @@ -0,0 +1,20 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#pragma once +#include "kernel/environment.h" +#include "frontends/lean/type_util.h" +#include "library/inductive_compiler/ginductive.h" + +namespace lean { + +environment add_basic_inductive_decl(environment const & env, options const & opts, name_map implicit_infer_map, + ginductive_decl const & decl); + +void initialize_inductive_compiler_basic(); +void finalize_inductive_compiler_basic(); + +} diff --git a/src/library/inductive_compiler/compiler.cpp b/src/library/inductive_compiler/compiler.cpp index f410830403..3543933da4 100644 --- a/src/library/inductive_compiler/compiler.cpp +++ b/src/library/inductive_compiler/compiler.cpp @@ -11,154 +11,27 @@ Author: Daniel Selsam #include "library/module.h" #include "library/attribute_manager.h" #include "library/inductive_compiler/compiler.h" -#include "library/constructions/rec_on.h" -#include "library/constructions/induction_on.h" -#include "library/constructions/cases_on.h" -#include "library/constructions/brec_on.h" -#include "library/constructions/no_confusion.h" - -#ifndef LEAN_DEFAULT_XINDUCTIVE_REC_ON -#define LEAN_DEFAULT_XINDUCTIVE_REC_ON true -#endif - -#ifndef LEAN_DEFAULT_XINDUCTIVE_CASES_ON -#define LEAN_DEFAULT_XINDUCTIVE_CASES_ON true -#endif - -#ifndef LEAN_DEFAULT_XINDUCTIVE_NO_CONFUSION -#define LEAN_DEFAULT_XINDUCTIVE_NO_CONFUSION true -#endif - -#ifndef LEAN_DEFAULT_XINDUCTIVE_BREC_ON -#define LEAN_DEFAULT_XINDUCTIVE_BREC_ON true -#endif +#include "library/inductive_compiler/basic.h" +#include "library/inductive_compiler/mutual.h" +#include "library/inductive_compiler/nested.h" namespace lean { -static name * g_inductive_rec_on = nullptr; -static name * g_inductive_cases_on = nullptr; -static name * g_inductive_no_confusion = nullptr; -static name * g_inductive_brec_on = nullptr; - -static bool get_inductive_rec_on(options const & opts) { - return opts.get_bool(*g_inductive_rec_on, LEAN_DEFAULT_XINDUCTIVE_REC_ON); -} - -static bool get_inductive_cases_on(options const & opts) { - return opts.get_bool(*g_inductive_cases_on, LEAN_DEFAULT_XINDUCTIVE_CASES_ON); -} - -static bool get_inductive_brec_on(options const & opts) { - return opts.get_bool(*g_inductive_brec_on, LEAN_DEFAULT_XINDUCTIVE_BREC_ON); -} - -static bool get_inductive_no_confusion(options const & opts) { - return opts.get_bool(*g_inductive_no_confusion, LEAN_DEFAULT_XINDUCTIVE_NO_CONFUSION); -} - -using inductive::inductive_decl; -using inductive::intro_rule; -using inductive::mk_intro_rule; - -environment tmp_add_kernel_inductive(environment const & env, name_map implicit_infer_map, - buffer const & lp_names, - buffer const & params, expr const & ind, buffer const & intro_rules) { - expr new_ind_type = Pi(params, mlocal_type(ind)); - expr c_ind = mk_app(mk_constant(mlocal_name(ind), param_names_to_levels(to_list(lp_names))), params); - - buffer new_intro_rules; - for (expr const & ir : intro_rules) { - expr new_ir_type = Pi(params, replace_local(mlocal_type(ir), ind, c_ind)); - implicit_infer_kind k = *implicit_infer_map.find(mlocal_name(ir)); - new_intro_rules.push_back(mk_intro_rule(mlocal_name(ir), infer_implicit_params(new_ir_type, params.size(), k))); +environment add_inner_inductive_declaration(environment const & env, options const & opts, + name_map implicit_infer_map, + ginductive_decl const & decl) { + lean_assert(decl.get_inds().size() == decl.get_intro_rules().size()); + if (optional new_env = add_nested_inductive_decl(env, opts, implicit_infer_map, decl)) { + return register_ginductive_decl(*new_env, decl); + } else if (decl.is_mutual()) { + return register_ginductive_decl(add_mutual_inductive_decl(env, opts, implicit_infer_map, decl), decl); + } else { + lean_assert(!decl.is_mutual()); + return register_ginductive_decl(add_basic_inductive_decl(env, opts, implicit_infer_map, decl), decl); } - inductive_decl decl(mlocal_name(ind), new_ind_type, to_list(new_intro_rules)); - return module::add_inductive(env, to_list(lp_names), params.size(), list(decl)); } -environment mk_basic_aux_decls(environment env, options const & opts, name const & ind_name) { - bool has_unit = has_poly_unit_decls(env); - bool has_eq = has_eq_decls(env); - bool has_heq = has_heq_decls(env); - bool has_prod = has_prod_decls(env); - bool has_lift = has_lift_decls(env); - - bool gen_rec_on = get_inductive_rec_on(opts); - bool gen_brec_on = get_inductive_brec_on(opts); - bool gen_cases_on = get_inductive_cases_on(opts); - bool gen_no_confusion = get_inductive_no_confusion(opts); - - if (gen_rec_on) - env = mk_rec_on(env, ind_name); - - if (gen_rec_on && env.impredicative()) - env = mk_induction_on(env, ind_name); - - if (has_unit) { - if (gen_cases_on) - env = mk_cases_on(env, ind_name); - - if (gen_cases_on && gen_no_confusion && has_eq - && ((env.prop_proof_irrel() && has_heq) || (!env.prop_proof_irrel() && has_lift))) { - env = mk_no_confusion(env, ind_name); - } - - if (gen_brec_on && has_prod) { - env = mk_below(env, ind_name); - if (env.impredicative()) { - env = mk_ibelow(env, ind_name); - } - } - } - - if (gen_brec_on && has_unit && has_prod) { - env = mk_brec_on(env, ind_name); - if (env.impredicative()) { - env = mk_binduction_on(env, ind_name); - } - } - return env; -} - -environment add_inductive_declaration(environment const & old_env, options const & opts, - name_map implicit_infer_map, - buffer const & lp_names, buffer const & params, - buffer const & inds, buffer > const & intro_rules) { - // TODO(dhs): mutual and nested inductive types - lean_assert(inds.size() == 1); - lean_assert(intro_rules.size() == 1); - - environment env = tmp_add_kernel_inductive(old_env, implicit_infer_map, lp_names, params, inds[0], intro_rules[0]); - env = mk_basic_aux_decls(env, opts, mlocal_name(inds[0])); - return env; -} - - -void initialize_inductive_compiler() { - g_inductive_rec_on = new name{"inductive", "rec_on"}; - g_inductive_cases_on = new name{"inductive", "cases_on"}; - g_inductive_brec_on = new name{"inductive", "brec_on"}; - g_inductive_no_confusion = new name{"inductive", "no_confusion"}; - - register_bool_option(*g_inductive_rec_on, LEAN_DEFAULT_XINDUCTIVE_REC_ON, - "(inductive) automatically generate the auxiliary declarations C.rec_on and C.induction_on for each inductive datatype C"); - - register_bool_option(*g_inductive_brec_on, LEAN_DEFAULT_XINDUCTIVE_BREC_ON, - "(inductive) automatically generate the auxiliary declaration C.brec_on for each inductive datatype C"); - - register_bool_option(*g_inductive_cases_on, LEAN_DEFAULT_XINDUCTIVE_CASES_ON, - "(inductive) automatically generate the auxiliary declaration C.cases_on for each inductive datatype C" - "(remark: if cases_on is disabled, then the auxiliary declaration C.no_confusion is also disabled"); - - register_bool_option(*g_inductive_no_confusion, LEAN_DEFAULT_XINDUCTIVE_NO_CONFUSION, - "(inductive) automatically generate the auxiliary declaration C.no_confusion for each inductive datatype C"); -} - -void finalize_inductive_compiler() { - delete g_inductive_rec_on; - delete g_inductive_cases_on; - delete g_inductive_brec_on; - delete g_inductive_no_confusion; -} +void initialize_inductive_compiler() {} +void finalize_inductive_compiler() {} } diff --git a/src/library/inductive_compiler/compiler.h b/src/library/inductive_compiler/compiler.h index b995ccade3..1f8f274e42 100644 --- a/src/library/inductive_compiler/compiler.h +++ b/src/library/inductive_compiler/compiler.h @@ -8,13 +8,13 @@ Author: Daniel Selsam #include "kernel/environment.h" #include "frontends/lean/type_util.h" #include "library/util.h" +#include "library/inductive_compiler/ginductive.h" namespace lean { -environment add_inductive_declaration(environment const & env, options const & opts, - name_map implicit_infer_map, - buffer const & lp_names, buffer const & params, - buffer const & inds, buffer > const & intro_rules); +environment add_inner_inductive_declaration(environment const & env, options const & opts, + name_map implicit_infer_map, + ginductive_decl const & decl); void initialize_inductive_compiler(); void finalize_inductive_compiler(); diff --git a/src/library/inductive_compiler/ginductive.cpp b/src/library/inductive_compiler/ginductive.cpp new file mode 100644 index 0000000000..6c911f9562 --- /dev/null +++ b/src/library/inductive_compiler/ginductive.cpp @@ -0,0 +1,197 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#include +#include +#include "util/serializer.h" +#include "kernel/environment.h" +#include "library/inductive_compiler/ginductive.h" +#include "library/module.h" +#include "library/kernel_serializer.h" + +namespace lean { + +struct ginductive_entry { + unsigned m_num_params; + list m_inds; + list > m_intro_rules; +}; + +serializer & operator<<(serializer & s, ginductive_entry const & entry); +ginductive_decl read_ginductive_decl(deserializer & d); +inline deserializer & operator>>(deserializer & d, ginductive_entry & entry); + +serializer & operator<<(serializer & s, ginductive_entry const & entry) { + s << entry.m_num_params; + write_list(s, entry.m_inds); + for (list const & irs : reverse(entry.m_intro_rules)) + write_list(s, irs); + return s; +} + +ginductive_entry read_ginductive_entry(deserializer & d) { + ginductive_entry entry; + d >> entry.m_num_params; + entry.m_inds = read_list(d, read_name); + + unsigned num_inds = length(entry.m_inds); + for (unsigned i = 0; i < num_inds; ++i) { + entry.m_intro_rules = list >(read_list(d, read_name), entry.m_intro_rules); + } + return entry; +} + +inline deserializer & operator>>(deserializer & d, ginductive_entry & entry) { + entry = read_ginductive_entry(d); + return d; +} + +static name * g_ginductive_extension = nullptr; +static std::string * g_ginductive_key = nullptr; + +struct ginductive_env_ext : public environment_extension { + name_map > m_ind_to_irs; + name_map > m_ind_to_mut_inds; + name_map m_ir_to_ind; + name_map m_num_params; + + ginductive_env_ext() {} + + void register_ginductive_entry(ginductive_entry const & entry) { + buffer > intro_rules; + to_buffer(entry.m_intro_rules, intro_rules); + + unsigned ind_idx = 0; + for (name const & ind : entry.m_inds) { + m_num_params.insert(ind, entry.m_num_params); + m_ind_to_irs.insert(ind, intro_rules[ind_idx]); + m_ind_to_mut_inds.insert(ind, entry.m_inds); + for (name const & ir : intro_rules[ind_idx]) { + m_ir_to_ind.insert(ir, ind); + } + } + } + + bool is_ginductive(name const & ind_name) const { + return m_ind_to_irs.contains(ind_name); + } + + optional > get_intro_rules(name const & ind_name) const { + list const * ir_names = m_ind_to_irs.find(ind_name); + if (ir_names) + return optional >(*ir_names); + else + return optional >(); + } + + optional is_intro_rule(name const & ir_name) const { + name const * ind_name = m_ir_to_ind.find(ir_name); + if (ind_name) + return optional(*ind_name); + else + return optional(); + } + + unsigned get_num_params(name const & ind_name) const { + unsigned const * num_params = m_num_params.find(ind_name); + lean_assert(num_params); + return *num_params; + } + + list get_mut_ind_names(name const & ind_name) const { + list const * mut_ind_names = m_ind_to_mut_inds.find(ind_name); + lean_assert(mut_ind_names); + return *mut_ind_names; + } +}; + +struct ginductive_env_ext_reg { + unsigned m_ext_id; + ginductive_env_ext_reg() { m_ext_id = environment::register_extension(std::make_shared()); } +}; + +static ginductive_env_ext_reg * g_ext = nullptr; + +static ginductive_env_ext const & get_extension(environment const & env) { + return static_cast(env.get_extension(g_ext->m_ext_id)); +} + +static environment update(environment const & env, ginductive_env_ext const & ext) { + return env.update(g_ext->m_ext_id, std::make_shared(ext)); +} + +environment register_ginductive_decl(environment const & env, ginductive_decl const & decl) { + ginductive_env_ext ext(get_extension(env)); + + ginductive_entry entry; + entry.m_num_params = decl.get_num_params(); + + buffer inds; + for (expr const & ind : decl.get_inds()) { + inds.push_back(mlocal_name(ind)); + } + entry.m_inds = to_list(inds); + + buffer > intro_rules; + for (buffer const & irs : decl.get_intro_rules()) { + buffer ir_names; + for (expr const & ir : irs) + ir_names.push_back(mlocal_name(ir)); + intro_rules.push_back(to_list(ir_names)); + } + entry.m_intro_rules = to_list(intro_rules); + + ext.register_ginductive_entry(entry); + environment new_env = update(env, ext); + return module::add(new_env, *g_ginductive_key, [=](environment const &, serializer & s) { s << entry; }); +} + +bool is_ginductive(environment const & env, name const & ind_name) { + return get_extension(env).is_ginductive(ind_name); +} + +optional > get_ginductive_intro_rules(environment const & env, name const & ind_name) { + return get_extension(env).get_intro_rules(ind_name); +} + +optional is_ginductive_intro_rule(environment const & env, name const & ir_name) { + return get_extension(env).is_intro_rule(ir_name); +} + +unsigned get_ginductive_num_params(environment const & env, name const & ind_name) { + return get_extension(env).get_num_params(ind_name); +} + +list get_mut_ind_names(environment const & env, name const & ind_name) { + return get_extension(env).get_mut_ind_names(ind_name); +} + +static void ginductive_reader(deserializer & d, shared_environment & senv, + std::function &, + std::function &) { + ginductive_entry entry; + d >> entry; + senv.update([=](environment const & env) -> environment { + ginductive_env_ext ext = get_extension(env); + ext.register_ginductive_entry(entry); + return update(env, ext); + }); +} + +void initialize_inductive_compiler_ginductive() { + g_ginductive_extension = new name("ginductive_extension"); + g_ginductive_key = new std::string("gind"); + g_ext = new ginductive_env_ext_reg(); + + register_module_object_reader(*g_ginductive_key, ginductive_reader); +} + +void finalize_inductive_compiler_ginductive() { + delete g_ginductive_extension; + delete g_ginductive_key; + delete g_ext; +} +} diff --git a/src/library/inductive_compiler/ginductive.h b/src/library/inductive_compiler/ginductive.h new file mode 100644 index 0000000000..368fa678fc --- /dev/null +++ b/src/library/inductive_compiler/ginductive.h @@ -0,0 +1,98 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#pragma once +#include "kernel/environment.h" +#include "kernel/find_fn.h" + +namespace lean { + +class ginductive_decl { + buffer m_lp_names; + buffer m_params; + buffer m_inds; + buffer > m_intro_rules; +public: + ginductive_decl() {} + ginductive_decl(buffer const & lp_names, buffer const & params): + m_lp_names(lp_names), m_params(params) {} + ginductive_decl(buffer const & lp_names, buffer const & params, + buffer const & inds, buffer > const & intro_rules): + m_lp_names(lp_names), m_params(params), m_inds(inds), m_intro_rules(intro_rules) {} + + bool is_mutual() const { return m_inds.size() > 1; } + unsigned get_num_params() const { return m_params.size(); } + unsigned get_num_inds() const { return m_inds.size(); } + unsigned get_num_intro_rules(unsigned ind_idx) const { return m_intro_rules[ind_idx].size(); } + levels get_levels() const { return param_names_to_levels(to_list(m_lp_names)); } + + expr const & get_param(unsigned i) const { return m_params[i]; } + expr const & get_ind(unsigned i) const { return m_inds[i]; } + expr const & get_intro_rule(unsigned ind_idx, unsigned ir_idx) const { return m_intro_rules[ind_idx][ir_idx]; } + buffer const & get_intro_rules(unsigned ind_idx) const { return m_intro_rules[ind_idx]; } + + buffer const & get_lp_names() const { return m_lp_names; } + buffer const & get_params() const { return m_params; } + buffer const & get_inds() const { return m_inds; } + buffer > const & get_intro_rules() const { return m_intro_rules; } + + buffer & get_lp_names() { return m_lp_names; } + buffer & get_params() { return m_params; } + buffer & get_inds() { return m_inds; } + buffer > & get_intro_rules() { return m_intro_rules; } + + expr get_c_ind(unsigned ind_idx) const { + return mk_constant(mlocal_name(m_inds[ind_idx]), get_levels()); + } + + expr get_c_ind_params(unsigned ind_idx) const { + return mk_app(mk_constant(mlocal_name(m_inds[ind_idx]), get_levels()), m_params); + } + + expr get_c_ir(unsigned ind_idx, unsigned ir_idx) const { + return mk_constant(mlocal_name(m_intro_rules[ind_idx][ir_idx]), get_levels()); + } + + expr get_c_ir_params(unsigned ind_idx, unsigned ir_idx) const { + return mk_app(mk_constant(mlocal_name(m_intro_rules[ind_idx][ir_idx]), get_levels()), m_params); + } + + void args_to_indices(buffer const & args, buffer & indices) const { + for (unsigned i = get_num_params(); i < args.size(); ++i) + indices.push_back(args[i]); + } + + bool is_ind(expr const & e) const { + return is_constant(e) + && std::any_of(m_inds.begin(), m_inds.end(), [&](expr const & ind) { + return const_name(e) == mlocal_name(ind); + }); + } + + bool has_ind_occ(expr const & t) const { + return static_cast(find(t, [&](expr const & e, unsigned) { return is_ind(e); })); + } +}; + +environment register_ginductive_decl(environment const & env, ginductive_decl const & decl); + +bool is_ginductive(environment const & env, name const & ind_name); + +/* \brief Returns the names of the introduction rules for the inductive type \e ind_name. */ +optional > get_ginductive_intro_rules(environment const & env, name const & ind_name); + +/* \brief Returns the name of the inductive type if \e ir_name is indeed an introduction rule. */ +optional is_ginductive_intro_rule(environment const & env, name const & ir_name); + +/* \brief Returns the number of parameters for the given inductive type \e ind_name. */ +unsigned get_ginductive_num_params(environment const & env, name const & ind_name); + +/* \brief Returns the names of all types that are mutually inductive with \e ind_name */ +list get_mut_ind_names(environment const & env, name const & ind_name); + +void initialize_inductive_compiler_ginductive(); +void finalize_inductive_compiler_ginductive(); +} diff --git a/src/library/inductive_compiler/init_module.cpp b/src/library/inductive_compiler/init_module.cpp index 98a97919cb..e4203e4752 100644 --- a/src/library/inductive_compiler/init_module.cpp +++ b/src/library/inductive_compiler/init_module.cpp @@ -5,15 +5,27 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Daniel Selsam */ #include "library/inductive_compiler/init_module.h" +#include "library/inductive_compiler/ginductive.h" #include "library/inductive_compiler/compiler.h" +#include "library/inductive_compiler/basic.h" +#include "library/inductive_compiler/mutual.h" +#include "library/inductive_compiler/nested.h" namespace lean { void initialize_inductive_compiler_module() { initialize_inductive_compiler(); + initialize_inductive_compiler_ginductive(); + initialize_inductive_compiler_basic(); + initialize_inductive_compiler_mutual(); + initialize_inductive_compiler_nested(); } void finalize_inductive_compiler_module() { + finalize_inductive_compiler_nested(); + finalize_inductive_compiler_mutual(); + finalize_inductive_compiler_basic(); + finalize_inductive_compiler_ginductive(); finalize_inductive_compiler(); } diff --git a/src/library/inductive_compiler/mutual.cpp b/src/library/inductive_compiler/mutual.cpp new file mode 100644 index 0000000000..5bca72d777 --- /dev/null +++ b/src/library/inductive_compiler/mutual.cpp @@ -0,0 +1,812 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#include "kernel/inductive/inductive.h" +#include "kernel/abstract.h" +#include "kernel/instantiate.h" +#include "kernel/type_checker.h" +#include "kernel/find_fn.h" +#include "util/sexpr/option_declarations.h" +#include "library/locals.h" +#include "library/app_builder.h" +#include "library/constants.h" +#include "library/class.h" +#include "library/module.h" +#include "library/trace.h" +#include "library/protected.h" +#include "library/type_context.h" +#include "library/attribute_manager.h" +#include "library/constructions/has_sizeof.h" +#include "library/inductive_compiler/compiler.h" +#include "library/inductive_compiler/basic.h" +#include "library/inductive_compiler/mutual.h" +#include "library/inductive_compiler/util.h" + +namespace lean { + +static unsigned g_next_mutual_id = 0; +static name * g_mutual_prefix = nullptr; + +class add_mutual_inductive_decl_fn { + environment m_env; + options const & m_opts; + name_map m_implicit_infer_map; + ginductive_decl const & m_mut_decl; + ginductive_decl m_basic_decl; + name m_prefix; + + type_context m_tctx; + + buffer m_index_types; + expr m_full_index_type; + buffer m_makers; + buffer m_putters; + + buffer m_ind_ir_locals; + buffer m_ind_ir_cs; + + // For the recursor + level m_elim_level; + expr poly_unit() const { return mk_constant(get_poly_unit_name(), {m_elim_level}); } + expr poly_unit_star() const { return mk_constant(get_poly_unit_star_name(), {m_elim_level}); } + + expr mk_local_for(expr const & b) { return mk_local(mk_fresh_name(), binding_name(b), binding_domain(b), binding_info(b)); } + expr mk_local_pp(name const & n, expr const & ty) { return mk_local(mk_fresh_name(), n, ty, binder_info()); } + + expr to_sigma_type(expr const & _ty) { + expr ty = m_tctx.whnf(_ty); + if (!is_pi(ty)) + return mk_constant(get_unit_name()); + expr l = mk_local_for(ty); + expr dom = binding_domain(ty); + expr rest = Fun(l, to_sigma_type(instantiate(binding_body(ty), l))); + return mk_app(m_tctx, get_sigma_name(), {dom, rest}); + } + + expr mk_sum(expr const & A, expr const & B) { + return mk_app(m_tctx, get_sum_name(), A, B); + } + + expr mk_sum(unsigned num_args, expr const * args) { + expr sum = args[num_args-1]; + for (unsigned i = num_args - 2; i + 1 > 0; --i) { + sum = mk_sum(args[i], sum); + } + return sum; + } + + bool dep_elim() { return inductive::has_dep_elim(m_env, mlocal_name(m_basic_decl.get_ind(0))); } + + void compute_index_types() { + for (expr const & ind : m_mut_decl.get_inds()) { + m_index_types.push_back(to_sigma_type(mlocal_type(ind))); + lean_trace(name({"inductive_compiler", "mutual", "index_types"}), tout() << mlocal_name(ind) << " ==> " << m_index_types.back() << "\n";); + } + m_full_index_type = mk_sum(m_index_types.size(), m_index_types.data()); + lean_trace(name({"inductive_compiler", "mutual", "full_index_type"}), tout() << m_full_index_type << "\n";); + } + + // Returns the maker, and the sigma type that is being "made" + pair to_maker_core(expr const & _ty) { + expr ty = m_tctx.whnf(_ty); + buffer locals; + while (is_pi(ty)) { + expr l = mk_local_for(ty); + ty = m_tctx.whnf(instantiate(binding_body(ty), l)); + locals.push_back(l); + } + expr maker = mk_constant(get_unit_star_name()); + expr stype = mk_constant(get_unit_name()); + + for (int i = locals.size() - 1; i >= 0; --i) { + expr const & l = locals[i]; + expr A = mlocal_type(l); + level l1 = get_level(m_tctx, A); + level l2 = get_level(m_tctx, stype); + stype = Fun(l, stype); + maker = mk_app(mk_constant(get_sigma_mk_name(), {l1, l2}), A, stype, l, maker); + stype = mk_app(m_tctx, get_sigma_name(), {A, stype}); + } + return mk_pair(Fun(locals, maker), stype); + } + + expr to_maker(expr const & ty) { + return to_maker_core(ty).first; + } + + expr args_to_sigma_type(expr const & ty) { + return to_maker_core(ty).second; + } + + void compute_makers() { + for (expr const & ind : m_mut_decl.get_inds()) { + m_makers.push_back(to_maker(mlocal_type(ind))); + lean_trace(name({"inductive_compiler", "mutual", "makers"}), tout() << mlocal_name(ind) << " ==> " << m_makers.back() << "\n";); + } + } + + expr mk_put_rest(unsigned i) { + expr l = mk_local_pp("rest", mk_sum(m_index_types.size() - i, m_index_types.data() + i)); + expr putter = l; + for (unsigned j = i; j > 0; --j) { + putter = mk_app(m_tctx, get_sum_inr_name(), m_index_types[j-1], mk_sum(m_index_types.size() - j, m_index_types.data() + j), putter); + } + return Fun(l, putter); + } + + expr to_putter(unsigned ind_idx) { + unsigned num_inds = m_index_types.size(); + expr l = mk_local_pp(name("idx"), m_index_types[ind_idx]); + + expr putter; + if (ind_idx == num_inds - 1) { + putter = mk_app(m_tctx, get_sum_inr_name(), m_index_types[ind_idx - 1], m_index_types[ind_idx], l); + ind_idx--; + } else { + putter = mk_app(m_tctx, get_sum_inl_name(), m_index_types[ind_idx], mk_sum(num_inds - ind_idx - 1, m_index_types.data() + ind_idx + 1), l); + } + for (unsigned i = ind_idx; i > 0; --i) { + putter = mk_app(m_tctx, get_sum_inr_name(), m_index_types[i - 1], mk_sum(num_inds - i, m_index_types.data() + i), putter); + } + return Fun(l, putter); + } + + void compute_putters() { + for (unsigned i = 0; i < m_mut_decl.get_inds().size(); ++i) { + m_putters.push_back(to_putter(i)); + lean_trace(name({"inductive_compiler", "mutual", "putters"}), tout() << mlocal_name(m_mut_decl.get_ind(i)) << " ==> " << m_putters.back() << "\n";); + } + } + + name mk_prefix() { + return m_prefix; + } + + void compute_new_ind() { + expr ind = mk_local(mk_prefix(), mk_arrow(m_full_index_type, get_ind_result_type(m_tctx, m_mut_decl.get_ind(0)))); + lean_trace(name({"inductive_compiler", "mutual", "basic_ind"}), tout() << mlocal_name(ind) << " : " << mlocal_type(ind) << "\n";); + m_basic_decl.get_inds().push_back(ind); + } + + expr mk_basic_ind(unsigned ind_idx, buffer const & indices) { + return mk_app(m_basic_decl.get_c_ind_params(0), mk_app(m_putters[ind_idx], mk_app(m_makers[ind_idx], indices))); + } + + expr mk_basic_ind_from_args(unsigned ind_idx, buffer const & args) { + return mk_app(m_basic_decl.get_c_ind_params(0), + mk_app(m_putters[ind_idx], + mk_app(m_makers[ind_idx], args.size() - m_basic_decl.get_num_params(), args.data() + m_basic_decl.get_num_params()))); + } + + optional translate_ind_app(expr const & app) { + buffer args; + expr fn = get_app_args(app, args); + for (unsigned ind_idx = 0; ind_idx < m_mut_decl.get_inds().size(); ++ind_idx) { + expr c_ind = m_mut_decl.get_c_ind_params(ind_idx); + if (args.size() >= m_mut_decl.get_num_params() && mk_app(fn, m_mut_decl.get_num_params(), args.data()) == c_ind) + return some_expr(mk_basic_ind_from_args(ind_idx, args)); + } + return none_expr(); + } + + expr translate_ir_arg(expr const & arg_type) { + expr ty = m_tctx.whnf(arg_type); + buffer locals; + while (is_pi(ty)) { + expr l = mk_local_for(ty); + locals.push_back(l); + ty = instantiate(binding_body(ty), l); + ty = m_tctx.whnf(ty); + } + return Pi(locals, translate_all_ind_apps(ty)); + } + + expr translate_all_ind_apps(expr const & e) { + // We might have a nested occurrence of foo in the return type of an introduction rule! + // Example: + // inductive foo : Type -> Type + // | mk : foo (foo poly_unit) + // We cannot use replace since we need to translate bottom-up + buffer args; + expr fn = get_app_args(e, args); + for (expr & arg : args) + arg = translate_all_ind_apps(arg); + + expr new_e = copy_tag(e, mk_app(fn, args)); + if (auto res = translate_ind_app(new_e)) + return *res; + else + return new_e; + } + + expr translate_ir(expr const & ir) { + name ir_name = mk_prefix() + mlocal_name(ir); + buffer locals; + expr ty = m_tctx.whnf(mlocal_type(ir)); + while (is_pi(ty)) { + expr l = mk_local_pp(binding_name(ty), translate_ir_arg(binding_domain(ty))); + locals.push_back(l); + ty = instantiate(binding_body(ty), l); + ty = m_tctx.whnf(ty); + } + expr result_type = translate_all_ind_apps(ty); + return mk_local(ir_name, Pi(locals, result_type)); + } + + void compute_new_intro_rules() { + m_basic_decl.get_intro_rules().emplace_back(); + for (unsigned ind_idx = 0; ind_idx < m_mut_decl.get_inds().size(); ++ind_idx) { + buffer const & irs = m_mut_decl.get_intro_rules(ind_idx); + for (unsigned ir_idx = 0; ir_idx < irs.size(); ++ir_idx) { + expr const & ir = irs[ir_idx]; + expr new_ir = translate_ir(ir); + m_basic_decl.get_intro_rules().back().push_back(new_ir); + lean_trace(name({"inductive_compiler", "mutual", "basic_irs"}), tout() << mlocal_name(new_ir) << " : " << mlocal_type(new_ir) << "\n";); + } + } + } + + void define_ind_types() { + for (unsigned ind_idx = 0; ind_idx < m_mut_decl.get_inds().size(); ++ind_idx) { + expr const & ind = m_mut_decl.get_ind(ind_idx); + buffer locals; + expr ty = m_tctx.whnf(mlocal_type(ind)); + while (is_pi(ty)) { + expr l = mk_local_for(ty); + locals.push_back(l); + ty = m_tctx.whnf(instantiate(binding_body(ty), l)); + } + expr new_ind_val = Fun(locals, mk_basic_ind(ind_idx, locals)); + expr new_ind_type = mlocal_type(ind); + + new_ind_val = Fun(m_mut_decl.get_params(), new_ind_val); + new_ind_type = Pi(m_mut_decl.get_params(), new_ind_type); + + lean_trace(name({"inductive_compiler", "mutual", "new_inds"}), tout() + << mlocal_name(ind) << " : " << new_ind_type << " :=\n " << new_ind_val << "\n";); + lean_assert(!has_local(new_ind_type)); + lean_assert(!has_local(new_ind_val)); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, mlocal_name(ind), to_list(m_mut_decl.get_lp_names()), new_ind_type, new_ind_val, true))); + m_env = set_reducible(m_env, mlocal_name(ind), reducible_status::Irreducible, true); + m_tctx.set_env(m_env); + } + } + + optional is_recursive_arg(name const & ind_name, expr const & arg_ty, buffer & arg_args) { + expr it = m_tctx.whnf(arg_ty); + while (is_pi(it)) { + expr arg_arg = mk_local_for(it); + arg_args.push_back(arg_arg); + it = m_tctx.whnf(instantiate(binding_body(it), arg_arg)); + } + expr fn = get_app_fn(it); + if (is_constant(fn) && const_name(fn) == ind_name) + return some_expr(it); + else + return none_expr(); + } + + void define_sizeofs() { + unsigned num_params = m_mut_decl.get_num_params(); + name basic_sizeof_name = mk_has_sizeof_name(mlocal_name(m_basic_decl.get_ind(0))); + optional opt_d = m_env.find(basic_sizeof_name); + if (!opt_d) return; + declaration const & d = *opt_d; + expr ty = m_tctx.whnf(d.get_type()); + + for (expr const & param : m_mut_decl.get_params()) { + ty = m_tctx.whnf(instantiate(binding_body(ty), param)); + } + + buffer param_insts; + while (is_pi(ty) && binding_info(ty).is_inst_implicit()) { + expr param_inst = m_tctx.push_local(binding_name(ty).append_after("_inst"), binding_domain(ty), mk_inst_implicit_binder_info()); + param_insts.push_back(param_inst); + ty = m_tctx.whnf(instantiate(binding_body(ty), param_inst)); + } + + type_context tctx_synth(m_env, m_tctx.get_options(), m_tctx.lctx(), transparency_mode::Semireducible); + + for (unsigned ind_idx = 0; ind_idx < m_mut_decl.get_inds().size(); ++ind_idx) { + expr const & ind = m_mut_decl.get_ind(ind_idx); + name has_sizeof_name = mk_has_sizeof_name(mlocal_name(ind)); + expr c_has_sizeof = mk_app(mk_app(mk_constant(has_sizeof_name, m_mut_decl.get_levels()), m_mut_decl.get_params()), param_insts); + expr c_ind = mk_app(mk_constant(mlocal_name(ind), m_mut_decl.get_levels()), m_mut_decl.get_params()); + + ty = mlocal_type(ind); + buffer indices; + while (is_pi(ty)) { + expr index = mk_local_for(ty); + indices.push_back(index); + ty = m_tctx.whnf(instantiate(binding_body(ty), index)); + } + + expr has_sizeof_type = Pi(m_mut_decl.get_params(), + tctx_synth.mk_pi(param_insts, + Pi(indices, + mk_app(m_tctx, get_has_sizeof_name(), mk_app(c_ind, indices))))); + + expr c_sizeof = mk_app(mk_app(mk_constant(basic_sizeof_name, m_mut_decl.get_levels()), m_mut_decl.get_params()), param_insts); + + expr has_sizeof_val = Fun(m_mut_decl.get_params(), + m_tctx.mk_lambda(param_insts, + Fun(indices, mk_app(c_sizeof, mk_app(m_putters[ind_idx], mk_app(m_makers[ind_idx], indices)))))); + + lean_trace(name({"inductive_compiler", "mutual", "has_sizeof"}), tout() + << has_sizeof_name << " : " << has_sizeof_type << " :=\n " << has_sizeof_val << "\n";); + lean_assert(!has_local(has_sizeof_type)); + lean_assert(!has_local(has_sizeof_val)); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, has_sizeof_name, to_list(m_mut_decl.get_lp_names()), has_sizeof_type, has_sizeof_val, true))); + m_env = add_instance(m_env, has_sizeof_name, LEAN_DEFAULT_PRIORITY, true); + m_env = add_protected(m_env, has_sizeof_name); + m_tctx.set_env(m_env); + tctx_synth.set_env(m_env); + } + + for (unsigned ind_idx = 0; ind_idx < m_mut_decl.get_inds().size(); ++ind_idx) { + expr const & ind = m_mut_decl.get_ind(ind_idx); + name has_sizeof_name = mk_has_sizeof_name(mlocal_name(ind)); + expr c_has_sizeof = mk_app(mk_app(mk_constant(has_sizeof_name, m_mut_decl.get_levels()), m_mut_decl.get_params()), param_insts); + expr c_ind = mk_app(mk_constant(mlocal_name(ind), m_mut_decl.get_levels()), m_mut_decl.get_params()); + + for (expr const & ir : m_mut_decl.get_intro_rules(ind_idx)) { + expr c_ir = mk_app(mk_constant(mlocal_name(ir), m_mut_decl.get_levels()), m_mut_decl.get_params()); + expr ir_ty = tctx_synth.whnf(m_tctx.infer(c_ir)); + + expr rhs = mk_nat_one(); + buffer locals; + + while (is_pi(ir_ty)) { + expr local = mk_local_for(ir_ty); + locals.push_back(local); + expr arg_ty = binding_domain(ir_ty); + + buffer arg_args; + if (auto ind_app = is_recursive_arg(mlocal_name(ind), arg_ty, arg_args)) { + if (arg_args.empty()) { + buffer ind_app_args; + get_app_args(*ind_app, ind_app_args); + expr new_val = mk_app(mk_constant(get_sizeof_name(), {get_datatype_level(mlocal_type(ind))}), + {mk_app(c_ind, ind_app_args.size() - num_params, ind_app_args.data() + num_params), + mk_app(c_has_sizeof, ind_app_args.size() - num_params, ind_app_args.data() + num_params), + local}); + rhs = mk_nat_add(rhs, new_val); + } + } else { + level l = get_level(m_tctx, arg_ty); + rhs = mk_nat_add(rhs, mk_app(tctx_synth, get_sizeof_name(), local)); + } + ir_ty = m_tctx.whnf(instantiate(binding_body(ir_ty), local)); + } + + expr lhs = mk_app(tctx_synth, get_sizeof_name(), {mk_app(c_ir, locals)}); + expr dsimp_rule_type = Pi(m_mut_decl.get_params(), m_tctx.mk_pi(param_insts, Pi(locals, mk_eq(m_tctx, lhs, rhs)))); + expr dsimp_rule_val = Fun(m_mut_decl.get_params(), m_tctx.mk_lambda(param_insts, Fun(locals, mk_eq_refl(m_tctx, lhs)))); + name dsimp_rule_name = mk_sizeof_spec_name(mlocal_name(ir)); + + assert_def_eq(m_env, tctx_synth.infer(dsimp_rule_val), dsimp_rule_type); + + lean_trace(name({"inductive_compiler", "mutual", "sizeof"}), tout() + << dsimp_rule_name << " : " << dsimp_rule_type << " :=\n "<< dsimp_rule_val << "\n";); + + m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, dsimp_rule_name, to_list(m_mut_decl.get_lp_names()), dsimp_rule_type, dsimp_rule_val, true))); + m_env = set_simp_sizeof(m_env, dsimp_rule_name); + m_env = add_protected(m_env, dsimp_rule_name); + + tctx_synth.set_env(m_env); + m_tctx.set_env(m_env); + } + } + } + + void define_intro_rules() { + unsigned basic_ir_idx = 0; + for (unsigned ind_idx = 0; ind_idx < m_mut_decl.get_inds().size(); ++ind_idx) { + buffer const & irs = m_mut_decl.get_intro_rules(ind_idx); + for (expr const & ir : irs) { + expr new_ir_val = Fun(m_mut_decl.get_params(), mk_app(mk_constant(mlocal_name(m_basic_decl.get_intro_rule(0, basic_ir_idx)), + m_mut_decl.get_levels()), + m_mut_decl.get_params())); + expr new_ir_type = Pi(m_mut_decl.get_params(), mlocal_type(ir)); + implicit_infer_kind k = get_implicit_infer_kind(m_implicit_infer_map, mlocal_name(ir)); + new_ir_type = infer_implicit_params(new_ir_type, m_mut_decl.get_params().size(), k); + lean_assert(!has_local(new_ir_type)); + lean_assert(!has_local(new_ir_val)); + lean_trace(name({"inductive_compiler", "mutual", "ir"}), tout() << mlocal_name(ir) << " : " << new_ir_type << "\n";); + + m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, mlocal_name(ir), to_list(m_mut_decl.get_lp_names()), new_ir_type, new_ir_val, true))); + m_env = set_reducible(m_env, mlocal_name(ir), reducible_status::Irreducible, true); + m_tctx.set_env(m_env); + basic_ir_idx++; + } + } + } + + expr mk_sigma(list const & rev_unpacked_sigma_args, expr const & idx) { + buffer rev_sigma_args; + to_buffer(rev_unpacked_sigma_args, rev_sigma_args); + expr sigma = idx; + expr stype = m_tctx.infer(sigma); + for (expr const & sarg : rev_sigma_args) { + expr A = mlocal_type(sarg); + level l1 = get_level(m_tctx, A); + level l2 = get_level(m_tctx, stype); + stype = Fun(sarg, stype); + sigma = mk_app(mk_constant(get_sigma_mk_name(), {l1, l2}), A, stype, sarg, sigma); + stype = mk_app(m_tctx, get_sigma_name(), {A, stype}); + } + return sigma; + } + + expr unpack_sigma_and_apply_C_core(unsigned ind_idx, expr const & ty, list const & rev_unpacked_sigma_args, + expr const & idx, expr const & C) { + if (!is_pi(ty)) { + buffer indices; + to_buffer(reverse(rev_unpacked_sigma_args), indices); + + expr u = mk_local_pp("u", mk_constant(get_unit_name())); + expr x_u = mk_local_pp("x_u", mk_app(m_basic_decl.get_c_ind_params(0), mk_app(m_putters[ind_idx], mk_sigma(rev_unpacked_sigma_args, u)))); + expr unit_C = dep_elim() ? Fun(u, Pi(x_u, mk_sort(m_elim_level))) : Fun(u, mk_sort(m_elim_level)); + level motive_level = get_level(m_tctx, dep_elim() ? Pi(u, Pi(x_u, mk_sort(m_elim_level))) : Pi(u, mk_sort(m_elim_level))); + expr unit_major_premise = idx; + + expr x_star = mk_local_pp("x", mk_app(m_basic_decl.get_c_ind_params(0), mk_app(m_putters[ind_idx], mk_sigma(rev_unpacked_sigma_args, mk_constant(get_unit_star_name()))))); + expr unit_minor_premise = dep_elim() ? Fun(x_star, mk_app(mk_app(C, indices), x_star)) : mk_app(C, indices); + + return mk_app(mk_constant(get_unit_cases_on_name(), {motive_level}), unit_C, unit_major_premise, unit_minor_premise); + } + + expr A = binding_domain(ty); + expr a = mk_local_for(ty); + expr B = args_to_sigma_type(instantiate(binding_body(ty), a)); + expr A_to_B = Fun(a, B); + + expr motive; + level motive_level; + { + expr idx = mk_local_pp("idx", args_to_sigma_type(ty)); + if (dep_elim()) { + expr x = mk_local_pp("x", mk_app(m_basic_decl.get_c_ind_params(0), + mk_app(m_putters[ind_idx], mk_sigma(rev_unpacked_sigma_args, idx)))); + motive = Fun(idx, Pi(x, mk_sort(m_elim_level))); + motive_level = get_level(m_tctx, Pi(x, mk_sort(m_elim_level))); + } else { + motive = Fun(idx, mk_sort(m_elim_level)); + motive_level = get_level(m_tctx, mk_sort(m_elim_level)); + } + } + + expr major_premise = idx; + + expr minor_premise; + { + expr b = mk_local_pp("b", mk_app(A_to_B, a)); + expr rest = unpack_sigma_and_apply_C_core(ind_idx, + instantiate(binding_body(ty), a), + list(a, rev_unpacked_sigma_args), + b, + C); + minor_premise = Fun({a, b}, rest); + } + levels lvls = {motive_level, get_level(m_tctx, A), get_level(m_tctx, B)}; + return mk_app(mk_constant(get_sigma_cases_on_name(), lvls), {A, A_to_B, motive, major_premise, minor_premise}); + } + + expr unpack_sigma_and_apply_C(unsigned ind_idx, expr const & idx, expr const & C) { + expr const & ind = m_mut_decl.get_ind(ind_idx); + list rev_unpacked_sigma_args; + return unpack_sigma_and_apply_C_core(ind_idx, mlocal_type(ind), rev_unpacked_sigma_args, idx, C); + } + + expr construct_inner_C_core(expr const & C, expr const & index, unsigned i, unsigned ind_idx) { + expr A = m_index_types[i]; + expr B = mk_sum(m_index_types.size() - (i+1), m_index_types.data() + (i+1)); + + expr motive; + level motive_level; + { + expr c = mk_local_pp("c", mk_sum(A, B)); + if (dep_elim()) { + expr x = mk_local_pp("x", mk_app(m_basic_decl.get_c_ind_params(0), mk_app(mk_put_rest(i), c))); + motive = Fun(c, Pi(x, mk_sort(m_elim_level))); + motive_level = get_level(m_tctx, Pi(x, mk_sort(m_elim_level))); + } else { + motive = Fun(c, mk_sort(m_elim_level)); + motive_level = get_level(m_tctx, mk_sort(m_elim_level)); + } + lean_trace(name({"inductive_compiler", "mutual", "rec"}), tout() << "inner C motive: " << motive << "\n";); + } + bool found_target = false; + expr case1; + { + expr idx = mk_local_pp("idx", A); + if (i == ind_idx) { + found_target = true; + case1 = Fun(idx, unpack_sigma_and_apply_C(ind_idx, idx, C)); + } else { + if (dep_elim()) { + expr x = mk_local_pp("x", mk_app(m_basic_decl.get_c_ind_params(0), mk_app(m_putters[i], idx))); + case1 = Fun({idx, x}, poly_unit()); + } else { + case1 = Fun(idx, poly_unit()); + } + } + lean_trace(name({"inductive_compiler", "mutual", "rec"}), tout() << "inner C case1: " << case1 << "\n";); + } + + expr case2; + { + expr idx = mk_local_pp("idx", B); + if (found_target) { + // case2 absorbs everything else + if (dep_elim()) { + expr x = mk_local_pp("x", mk_app(m_basic_decl.get_c_ind_params(0), mk_app(mk_put_rest(ind_idx+1), idx))); + case2 = Fun({idx, x}, poly_unit()); + } else { + case2 = Fun(idx, poly_unit()); + } + } else if (i + 1 == ind_idx && ind_idx + 1 == m_mut_decl.get_inds().size()) { + // case2 is the end, and has the payload + case2 = Fun(idx, unpack_sigma_and_apply_C(ind_idx, idx, C)); + } else { + // case2 is a recursive call + case2 = Fun(idx, construct_inner_C_core(C, idx, i+1, ind_idx)); + } + lean_trace(name({"inductive_compiler", "mutual", "rec"}), tout() << "inner C case2: " << case2 << "\n";); + } + level l1 = get_level(m_tctx, A); + level l2 = get_level(m_tctx, B); + return mk_app(mk_constant(get_sum_cases_on_name(), {motive_level, l1, l2}), {A, B, motive, index, case1, case2}); + } + + expr construct_inner_C(expr const & C, unsigned ind_idx) { +/* (λ (i : I), @sum.cases_on I₁ + I₂ + (λ (c : I₁ ⊎ I₂), @foo_vector c -> Type) + i + (λ (i : I₁) (x : @foo_vector (put₁ i)), poly_unit) + (λ (n : I₂) (x : @foo_vector (put₂ n)), C n x)) */ + expr index = mk_local_pp("idx", m_full_index_type); + return Fun(index, construct_inner_C_core(C, index, 0, ind_idx)); + } + + expr introduce_locals_for_rec_args(unsigned ind_idx, expr & C, buffer & minor_premises, buffer & indices, expr & major_premise) { + expr const & ind = m_mut_decl.get_ind(ind_idx); + { + buffer C_args; + expr ind_ty = m_tctx.whnf(mlocal_type(ind)); + while (is_pi(ind_ty)) { + expr C_arg = mk_local_for(ind_ty); + C_args.push_back(C_arg); + ind_ty = m_tctx.whnf(instantiate(binding_body(ind_ty), C_arg)); + } + expr C_type; + if (dep_elim()) { + C_type = Pi(C_args, mk_arrow(mk_app(m_mut_decl.get_c_ind_params(ind_idx), C_args), mk_sort(m_elim_level))); + } else { + C_type = Pi(C_args, mk_sort(m_elim_level)); + } + C = mk_local_pp("C", C_type); + lean_trace(name({"inductive_compiler", "mutual", "rec"}), tout() << "C_type: " << C_type << "\n";); + } + + for (unsigned ir_idx = 0; ir_idx < m_mut_decl.get_intro_rules(ind_idx).size(); ++ir_idx) { + expr const & ir = m_mut_decl.get_intro_rule(ind_idx, ir_idx); + buffer ir_args; + buffer rec_args; + expr ir_ty = m_tctx.whnf(mlocal_type(ir)); + while (is_pi(ir_ty)) { + expr minor_premise_arg = mk_local_for(ir_ty); + ir_args.push_back(minor_premise_arg); + + buffer ir_arg_args; + expr ir_arg = binding_domain(ir_ty); + while (is_pi(ir_arg)) { + expr ir_arg_arg = mk_local_for(ir_arg); + ir_arg_args.push_back(ir_arg_arg); + ir_arg = instantiate(binding_body(ir_arg), ir_arg_arg); + } + + buffer inner_args, inner_indices; + expr arg_fn = get_app_args(ir_arg, inner_args); + m_mut_decl.args_to_indices(inner_args, inner_indices); + + if (arg_fn == m_mut_decl.get_c_ind(ind_idx)) { + expr rec_arg_type; + if (dep_elim()) { + rec_arg_type = Pi(ir_arg_args, mk_app(mk_app(C, inner_indices), mk_app(minor_premise_arg, ir_arg_args))); + } else { + rec_arg_type = Pi(ir_arg_args, mk_app(C, inner_indices)); + } + expr rec_arg = mk_local_pp("x", rec_arg_type); + rec_args.push_back(rec_arg); + } + ir_ty = m_tctx.whnf(instantiate(binding_body(ir_ty), minor_premise_arg)); + } + buffer result_args, result_indices; + get_app_args(ir_ty, result_args); + m_mut_decl.args_to_indices(result_args, result_indices); + + expr minor_premise_type; + if (dep_elim()) { + minor_premise_type = Pi(ir_args, Pi(rec_args, mk_app(mk_app(C, result_indices), mk_app(m_mut_decl.get_c_ir_params(ind_idx, ir_idx), ir_args)))); + } else { + minor_premise_type = Pi(ir_args, Pi(rec_args, mk_app(C, result_indices))); + } + expr minor_premise = mk_local_pp("mp", minor_premise_type); + minor_premises.push_back(minor_premise); + lean_trace(name({"inductive_compiler", "mutual", "rec"}), tout() << "mp_type: " << minor_premise_type << "\n";); + } + + { + expr ind_ty = m_tctx.whnf(mlocal_type(ind)); + while (is_pi(ind_ty)) { + expr index = mk_local_for(ind_ty); + indices.push_back(index); + ind_ty = m_tctx.whnf(instantiate(binding_body(ind_ty), index)); + } + expr major_premise_type = mk_app(m_mut_decl.get_c_ind_params(ind_idx), indices); + major_premise = mk_local_pp("x", major_premise_type); + lean_trace(name({"inductive_compiler", "mutual", "rec"}), tout() << "major premise type: " << major_premise_type << "\n";); + } + + expr rec_type = dep_elim() ? mk_app(mk_app(C, indices), major_premise) : mk_app(C, indices); + lean_trace(name({"inductive_compiler", "mutual", "rec"}), tout() << "rec_type: " << rec_type << "\n";); + return rec_type; + } + + void define_recursor(name const & rec_name, level_param_names const & rec_lp_names, unsigned ind_idx) { + expr const & ind = m_mut_decl.get_ind(ind_idx); + + expr C; + buffer minor_premises, indices; + expr major_premise; + expr rec_type = introduce_locals_for_rec_args(ind_idx, C, minor_premises, indices, major_premise); + + expr inner_C = construct_inner_C(C, ind_idx); + lean_trace(name({"inductive_compiler", "mutual", "rec"}), tout() << "inner C: " << inner_C << "\n";); + + buffer inner_minor_premises; + for (unsigned i = 0; i < m_mut_decl.get_inds().size(); ++i) { + buffer const & irs = m_mut_decl.get_intro_rules(i); + for (unsigned ir_idx = 0; ir_idx < irs.size(); ++ir_idx) { + expr const & ir = irs[ir_idx]; + buffer locals; + buffer rec_args; + buffer return_args; + buffer return_rec_args; + expr ir_type = mlocal_type(ir); + while (is_pi(ir_type)) { + expr l = mk_local_for(ir_type); + locals.push_back(l); + + buffer ir_arg_args; + expr ir_arg = binding_domain(ir_type); + + while (is_pi(ir_arg)) { + expr ir_arg_arg = mk_local_for(ir_arg); + ir_arg_args.push_back(ir_arg_arg); + ir_arg = instantiate(binding_body(ir_arg), ir_arg_arg); + } + + buffer inner_args, inner_indices; + expr arg_fn = get_app_args(ir_arg, inner_args); + m_mut_decl.args_to_indices(inner_args, inner_indices); + + ir_type = m_tctx.whnf(instantiate(binding_body(ir_type), l)); + return_args.push_back(l); + if (m_mut_decl.is_ind(arg_fn)) { + expr C_term = dep_elim() ? mk_app(mk_app(C, inner_indices), mk_app(l, ir_arg_args)) : mk_app(C, inner_indices); + expr rec_arg_type = Pi(ir_arg_args, (arg_fn == m_mut_decl.get_c_ind(ind_idx)) ? C_term : poly_unit()); + expr l2 = mk_local_pp("x", rec_arg_type); + rec_args.push_back(l2); + // We only pass recursive arguments of the inductive type in question to the minor premise + if (arg_fn == m_mut_decl.get_c_ind(ind_idx)) { + return_rec_args.push_back(l2); + } + } + } + locals.append(rec_args); + expr return_value; + if (i == ind_idx) { + return_value = mk_app(mk_app(minor_premises[ir_idx], return_args), return_rec_args); + } else { + return_value = poly_unit_star(); + } + expr inner_minor_premise = Fun(locals, return_value); + lean_trace(name({"inductive_compiler", "mutual", "rec"}), tout() << "inner minor premise: " << inner_minor_premise << "\n";); + inner_minor_premises.push_back(inner_minor_premise); + } + } + + expr inner_index = mk_app(m_putters[ind_idx], mk_app(m_makers[ind_idx], indices)); + lean_trace(name({"inductive_compiler", "mutual", "rec"}), tout() << "inner index: " << inner_index << "\n";); + expr inner_major_premise = major_premise; + expr rec_val = mk_app(mk_app(mk_app(mk_app(mk_app(mk_constant(rec_name, param_names_to_levels(rec_lp_names)), m_mut_decl.get_params()), inner_C), + inner_minor_premises), inner_index), inner_major_premise); + + rec_type = Pi(m_mut_decl.get_params(), Pi(C, Pi(minor_premises, Pi(indices, Pi(major_premise, rec_type))))); + rec_val = Fun(m_mut_decl.get_params(), Fun(C, Fun(minor_premises, Fun(indices, Fun(major_premise, rec_val))))); + + lean_trace(name({"inductive_compiler", "mutual", "rec"}), tout() << "rec type: " << rec_type << "\n";); + lean_trace(name({"inductive_compiler", "mutual", "rec"}), tout() << "rec val: " << rec_val << "\n";); + + lean_assert(!has_local(rec_type)); + lean_assert(!has_local(rec_val)); + m_env = module::add(m_env, check(m_env, mk_definition_inferring_trusted(m_env, inductive::get_elim_name(mlocal_name(ind)), rec_lp_names, rec_type, rec_val, true))); + } + + void define_recursors() { + name rec_name = inductive::get_elim_name(mlocal_name(m_basic_decl.get_ind(0))); + declaration rec_decl = m_env.get(rec_name); + + level_param_names rec_lp_names = rec_decl.get_univ_params(); + bool elim_to_prop = rec_decl.get_num_univ_params() == m_basic_decl.get_lp_names().size(); + m_elim_level = elim_to_prop ? mk_level_zero() : mk_param_univ(head(rec_lp_names)); + + levels rec_levels = param_names_to_levels(rec_lp_names); + expr rec_const = mk_constant(rec_name, rec_levels); + + for (unsigned i = 0; i < m_mut_decl.get_inds().size(); ++i) { + define_recursor(rec_name, rec_lp_names, i); + } + } +public: + add_mutual_inductive_decl_fn(environment const & env, options const & opts, + name_map const & implicit_infer_map, ginductive_decl const & mut_decl): + m_env(env), m_opts(opts), m_implicit_infer_map(implicit_infer_map), + m_mut_decl(mut_decl), m_basic_decl(m_mut_decl.get_lp_names(), m_mut_decl.get_params()), + m_prefix("_mut" + std::to_string(g_next_mutual_id++)), + m_tctx(env, opts) {} + + environment operator()() { + compute_index_types(); + compute_makers(); + compute_putters(); + + compute_new_ind(); + compute_new_intro_rules(); + + try { + m_env = add_inner_inductive_declaration(m_env, m_opts, m_implicit_infer_map, m_basic_decl); + } catch (exception & ex) { + throw nested_exception(sstream() << "mutually inductive types compiled to invalid basic inductive type", ex); + } + + define_ind_types(); + define_intro_rules(); + define_sizeofs(); + + define_recursors(); + return m_env; + } +}; + +environment add_mutual_inductive_decl(environment const & env, options const & opts, + name_map const & implicit_infer_map, ginductive_decl const & mut_decl) { + return add_mutual_inductive_decl_fn(env, opts, implicit_infer_map, mut_decl)(); +} + +void initialize_inductive_compiler_mutual() { + register_trace_class(name({"inductive_compiler", "mutual"})); + register_trace_class(name({"inductive_compiler", "mutual", "index_types"})); + register_trace_class(name({"inductive_compiler", "mutual", "full_index_type"})); + register_trace_class(name({"inductive_compiler", "mutual", "makers"})); + register_trace_class(name({"inductive_compiler", "mutual", "putters"})); + register_trace_class(name({"inductive_compiler", "mutual", "basic_ind"})); + register_trace_class(name({"inductive_compiler", "mutual", "basic_irs"})); + register_trace_class(name({"inductive_compiler", "mutual", "new_irs"})); + register_trace_class(name({"inductive_compiler", "mutual", "new_inds"})); + register_trace_class(name({"inductive_compiler", "mutual", "rec"})); + register_trace_class(name({"inductive_compiler", "mutual", "has_sizeof"})); + + g_mutual_prefix = new name(name::mk_internal_unique_name()); +} + +void finalize_inductive_compiler_mutual() { + delete g_mutual_prefix; +} +} diff --git a/src/library/inductive_compiler/mutual.h b/src/library/inductive_compiler/mutual.h new file mode 100644 index 0000000000..1acd68016c --- /dev/null +++ b/src/library/inductive_compiler/mutual.h @@ -0,0 +1,21 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#pragma once +#include "kernel/environment.h" +#include "frontends/lean/type_util.h" +#include "library/inductive_compiler/ginductive.h" + +namespace lean { + +environment add_mutual_inductive_decl(environment const & env, options const & opts, + name_map const & implicit_infer_map, + ginductive_decl const & mut_decl); + +void initialize_inductive_compiler_mutual(); +void finalize_inductive_compiler_mutual(); + +} diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp new file mode 100644 index 0000000000..0fc8f3cd07 --- /dev/null +++ b/src/library/inductive_compiler/nested.cpp @@ -0,0 +1,47 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#include +#include "kernel/inductive/inductive.h" +#include "kernel/abstract.h" +#include "kernel/instantiate.h" +#include "kernel/type_checker.h" +#include "kernel/find_fn.h" +#include "kernel/expr.h" +#include "kernel/replace_fn.h" +#include "util/sexpr/option_declarations.h" +#include "util/list_fn.h" +#include "util/fresh_name.h" +#include "library/locals.h" +#include "library/app_builder.h" +#include "library/constants.h" +#include "library/class.h" +#include "library/module.h" +#include "library/trace.h" +#include "library/type_context.h" +#include "library/attribute_manager.h" +#include "library/constructions/has_sizeof.h" +#include "library/inductive_compiler/compiler.h" +#include "library/inductive_compiler/basic.h" +#include "library/inductive_compiler/nested.h" +#include "library/inductive_compiler/util.h" +#include "library/tactic/simplifier/simplifier.h" +#include "library/tactic/simplifier/simp_lemmas.h" + +namespace lean { + +optional add_nested_inductive_decl(environment const & env, options const & opts, + name_map const & implicit_infer_map, ginductive_decl const & decl) { + // TODO(dhs): re-implement + return optional(); +} + +void initialize_inductive_compiler_nested() { +} + +void finalize_inductive_compiler_nested() { +} +} diff --git a/src/library/inductive_compiler/nested.h b/src/library/inductive_compiler/nested.h new file mode 100644 index 0000000000..f307685a8b --- /dev/null +++ b/src/library/inductive_compiler/nested.h @@ -0,0 +1,21 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#pragma once +#include "kernel/environment.h" +#include "frontends/lean/type_util.h" +#include "library/inductive_compiler/ginductive.h" + +namespace lean { + +optional add_nested_inductive_decl(environment const & env, options const & opts, + name_map const & implicit_infer_map, + ginductive_decl const & decl); + +void initialize_inductive_compiler_nested(); +void finalize_inductive_compiler_nested(); + +} diff --git a/src/library/inductive_compiler/util.cpp b/src/library/inductive_compiler/util.cpp new file mode 100644 index 0000000000..c226598458 --- /dev/null +++ b/src/library/inductive_compiler/util.cpp @@ -0,0 +1,49 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#include "kernel/inductive/inductive.h" +#include "kernel/abstract.h" +#include "kernel/instantiate.h" +#include "kernel/type_checker.h" +#include "util/sexpr/option_declarations.h" +#include "library/locals.h" +#include "library/module.h" +#include "library/attribute_manager.h" +#include "library/inductive_compiler/util.h" + +namespace lean { + +implicit_infer_kind get_implicit_infer_kind(name_map const & implicit_infer_map, name const & n) { + if (auto it = implicit_infer_map.find(n)) + return *it; + else + return implicit_infer_kind::Implicit; +} + +expr get_ind_result_type(type_context & tctx, expr const & ind) { + expr ind_type = tctx.relaxed_whnf(mlocal_type(ind)); + type_context::tmp_locals locals(tctx); + while (is_pi(ind_type)) { + ind_type = instantiate(binding_body(ind_type), locals.push_local_from_binding(ind_type)); + ind_type = tctx.relaxed_whnf(ind_type); + } + lean_assert(is_sort(ind_type)); + return ind_type; +} + +void assert_def_eq(environment const & env, expr const & e1, expr const & e2) { + type_checker checker(env); + try { + lean_assert(checker.is_def_eq(e1, e2)); + } catch (exception ex) { + // TODO(dhs): this is only for debugging + // We prefer to enter GDB than to throw an exception + lean_assert(false); + throw ex; + } +} + +} diff --git a/src/library/inductive_compiler/util.h b/src/library/inductive_compiler/util.h new file mode 100644 index 0000000000..23894b467a --- /dev/null +++ b/src/library/inductive_compiler/util.h @@ -0,0 +1,18 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Daniel Selsam +*/ +#pragma once +#include "kernel/environment.h" +#include "library/util.h" +#include "library/type_context.h" + +namespace lean { + +implicit_infer_kind get_implicit_infer_kind(name_map const & implicit_infer_map, name const & n); +expr get_ind_result_type(type_context & tctx, expr const & ind); +void assert_def_eq(environment const & env, expr const & e1, expr const & e2); + +} diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 01c1e88be9..1089ed580e 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -45,7 +45,6 @@ Author: Leonardo de Moura #include "library/delayed_abstraction.h" #include "library/app_builder.h" #include "library/fun_info.h" -#include "library/inductive.h" #include "library/mpq_macro.h" #include "library/arith_instance_manager.h" #include "library/inverse.h" @@ -125,7 +124,6 @@ void initialize_library_module() { initialize_unification_hint(); initialize_type_context(); initialize_delayed_abstraction(); - initialize_library_inductive(); initialize_mpq_macro(); initialize_arith_instance_manager(); initialize_inverse(); @@ -135,7 +133,6 @@ void finalize_library_module() { finalize_inverse(); finalize_arith_instance_manager(); finalize_mpq_macro(); - finalize_library_inductive(); finalize_delayed_abstraction(); finalize_type_context(); finalize_unification_hint(); diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index ea83a92bbd..8ca1633ced 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -51,6 +51,10 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_PP_PURIFY_LOCALS true #endif +#ifndef LEAN_DEFAULT_PP_LOCALS_FULL_NAMES +#define LEAN_DEFAULT_PP_LOCALS_FULL_NAMES false +#endif + #ifndef LEAN_DEFAULT_PP_BETA #define LEAN_DEFAULT_PP_BETA true #endif @@ -104,6 +108,7 @@ static name * g_pp_full_names = nullptr; static name * g_pp_private_names = nullptr; static name * g_pp_purify_metavars = nullptr; static name * g_pp_purify_locals = nullptr; +static name * g_pp_locals_full_names = nullptr; static name * g_pp_beta = nullptr; static name * g_pp_numerals = nullptr; static name * g_pp_strings = nullptr; @@ -128,6 +133,7 @@ void initialize_pp_options() { g_pp_private_names = new name{"pp", "private_names"}; g_pp_purify_metavars = new name{"pp", "purify_metavars"}; g_pp_purify_locals = new name{"pp", "purify_locals"}; + g_pp_locals_full_names = new name{"pp", "locals_full_names"}; g_pp_beta = new name{"pp", "beta"}; g_pp_numerals = new name{"pp", "numerals"}; g_pp_strings = new name{"pp", "strings"}; @@ -163,6 +169,8 @@ void initialize_pp_options() { register_bool_option(*g_pp_purify_locals, LEAN_DEFAULT_PP_PURIFY_LOCALS, "(pretty printer) rename local names to avoid name capture, " "before pretty printing"); + register_bool_option(*g_pp_locals_full_names, LEAN_DEFAULT_PP_LOCALS_FULL_NAMES, + "(pretty printer) show full names of locals"); register_bool_option(*g_pp_beta, LEAN_DEFAULT_PP_BETA, "(pretty printer) apply beta-reduction when pretty printing"); register_bool_option(*g_pp_numerals, LEAN_DEFAULT_PP_NUMERALS, @@ -213,6 +221,7 @@ void finalize_pp_options() { delete g_pp_private_names; delete g_pp_purify_metavars; delete g_pp_purify_locals; + delete g_pp_locals_full_names; delete g_pp_beta; delete g_pp_goal_compact; delete g_pp_goal_max_hyps; @@ -231,6 +240,7 @@ name const & get_pp_universes_name() { return *g_pp_universes; } name const & get_pp_notation_name() { return *g_pp_notation; } name const & get_pp_purify_metavars_name() { return *g_pp_purify_metavars; } name const & get_pp_purify_locals_name() { return *g_pp_purify_locals; } +name const & get_pp_locals_full_names_name() { return *g_pp_locals_full_names; } name const & get_pp_beta_name() { return *g_pp_beta; } name const & get_pp_preterm_name() { return *g_pp_preterm; } name const & get_pp_numerals_name() { return *g_pp_numerals; } @@ -248,6 +258,7 @@ bool get_pp_full_names(options const & opts) { return opts.get_bool(* bool get_pp_private_names(options const & opts) { return opts.get_bool(*g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); } bool get_pp_purify_metavars(options const & opts) { return opts.get_bool(*g_pp_purify_metavars, LEAN_DEFAULT_PP_PURIFY_METAVARS); } bool get_pp_purify_locals(options const & opts) { return opts.get_bool(*g_pp_purify_locals, LEAN_DEFAULT_PP_PURIFY_LOCALS); } +bool get_pp_locals_full_names(options const & opts) { return opts.get_bool(*g_pp_locals_full_names, LEAN_DEFAULT_PP_LOCALS_FULL_NAMES); } bool get_pp_beta(options const & opts) { return opts.get_bool(*g_pp_beta, LEAN_DEFAULT_PP_BETA); } bool get_pp_numerals(options const & opts) { return opts.get_bool(*g_pp_numerals, LEAN_DEFAULT_PP_NUMERALS); } bool get_pp_strings(options const & opts) { return opts.get_bool(*g_pp_strings, LEAN_DEFAULT_PP_STRINGS); } diff --git a/src/library/pp_options.h b/src/library/pp_options.h index f03dd7ca05..99f13b54a4 100644 --- a/src/library/pp_options.h +++ b/src/library/pp_options.h @@ -15,6 +15,7 @@ name const & get_pp_universes_name(); name const & get_pp_notation_name(); name const & get_pp_purify_metavars_name(); name const & get_pp_purify_locals_name(); +name const & get_pp_locals_full_names_name(); name const & get_pp_beta_name(); name const & get_pp_preterm_name(); name const & get_pp_numerals_name(); @@ -33,6 +34,7 @@ bool get_pp_private_names(options const & opts); bool get_pp_beta(options const & opts); bool get_pp_purify_metavars(options const & opts); bool get_pp_purify_locals(options const & opts); +bool get_pp_locals_full_names(options const & opts); bool get_pp_numerals(options const & opts); bool get_pp_strings(options const & opts); bool get_pp_preterm(options const & opts); diff --git a/src/library/tactic/simplifier/simp_lemmas.cpp b/src/library/tactic/simplifier/simp_lemmas.cpp index 67befdb4cc..25475111cf 100644 --- a/src/library/tactic/simplifier/simp_lemmas.cpp +++ b/src/library/tactic/simplifier/simp_lemmas.cpp @@ -114,31 +114,6 @@ simp_lemmas add_core(tmp_type_context & tmp_tctx, simp_lemmas const & s, return new_s; } -simp_lemmas add(type_context & tctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, unsigned priority) { - tmp_type_context tmp_tctx(tctx); - return add_core(tmp_tctx, s, id, list(), e, h, priority); -} - -simp_lemmas join(simp_lemmas const & s1, simp_lemmas const & s2) { - simp_lemmas new_s1 = s1; - - buffer> slemmas; - s2.for_each_simp([&](name const & eqv, simp_lemma const & r) { - slemmas.push_back({eqv, r}); - }); - for (unsigned i = slemmas.size() - 1; i + 1 > 0; --i) - new_s1.insert(slemmas[i].first, slemmas[i].second); - - buffer> clemmas; - s2.for_each_congr([&](name const & eqv, user_congr_lemma const & r) { - clemmas.push_back({eqv, r}); - }); - for (unsigned i = clemmas.size() - 1; i + 1 > 0; --i) - new_s1.insert(clemmas[i].first, clemmas[i].second); - - return new_s1; -} - static simp_lemmas add_core(tmp_type_context & tmp_tctx, simp_lemmas const & s, name const & cname, unsigned priority) { declaration const & d = tmp_tctx.tctx().env().get(cname); buffer us; @@ -152,6 +127,7 @@ static simp_lemmas add_core(tmp_type_context & tmp_tctx, simp_lemmas const & s, return add_core(tmp_tctx, s, cname, ls, e, h, priority); } + // Return true iff lhs is of the form (B (x : ?m1), ?m2) or (B (x : ?m1), ?m2 x), // where B is lambda or Pi static bool is_valid_congr_rule_binding_lhs(expr const & lhs, name_set & found_mvars) { @@ -304,6 +280,36 @@ simp_lemmas add_congr_core(tmp_type_context & tmp_tctx, simp_lemmas const & s, n return new_s; } +simp_lemmas add_poly(type_context & tctx, simp_lemmas const & s, name const & id, unsigned priority) { + tmp_type_context tmp_tctx(tctx); + return add_core(tmp_tctx, s, id, priority); +} + +simp_lemmas add(type_context & tctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, unsigned priority) { + tmp_type_context tmp_tctx(tctx); + return add_core(tmp_tctx, s, id, list(), e, h, priority); +} + +simp_lemmas join(simp_lemmas const & s1, simp_lemmas const & s2) { + simp_lemmas new_s1 = s1; + + buffer> slemmas; + s2.for_each_simp([&](name const & eqv, simp_lemma const & r) { + slemmas.push_back({eqv, r}); + }); + for (unsigned i = slemmas.size() - 1; i + 1 > 0; --i) + new_s1.insert(slemmas[i].first, slemmas[i].second); + + buffer> clemmas; + s2.for_each_congr([&](name const & eqv, user_congr_lemma const & r) { + clemmas.push_back({eqv, r}); + }); + for (unsigned i = clemmas.size() - 1; i + 1 > 0; --i) + new_s1.insert(clemmas[i].first, clemmas[i].second); + + return new_s1; +} + void validate_simp(type_context & tctx, name const & n) { simp_lemmas s; flet set_ex(g_throw_ex, true); diff --git a/src/library/tactic/simplifier/simp_lemmas.h b/src/library/tactic/simplifier/simp_lemmas.h index 034a654906..a1d1ed4598 100644 --- a/src/library/tactic/simplifier/simp_lemmas.h +++ b/src/library/tactic/simplifier/simp_lemmas.h @@ -13,14 +13,8 @@ Author: Leonardo de Moura namespace lean { -environment add_simp_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent); -environment add_congr_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent); -unsigned get_simp_lemma_priority(environment const & env, name const & n); - -bool is_simp_lemma(environment const & env, name const & n); -bool is_congr_lemma(environment const & env, name const & n); -void get_simp_lemma_names(environment const & env, buffer & r); -void get_congr_lemma_names(environment const & env, buffer & r); +void on_add_simp_lemma(environment const & env, name const & c, bool); +void on_add_congr_lemma(environment const & env, name const & c, bool); void initialize_simp_lemmas(); void finalize_simp_lemmas(); @@ -148,6 +142,7 @@ public: simp_lemmas get_simp_lemmas(type_context & tctx, buffer const & simp_attrs, buffer const & congr_attrs); +simp_lemmas add_poly(type_context & tctx, simp_lemmas const & s, name const & id, unsigned priority); simp_lemmas add(type_context & tctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, unsigned priority); simp_lemmas join(simp_lemmas const & s1, simp_lemmas const & s2); diff --git a/src/library/tactic/simplifier/simplifier.cpp b/src/library/tactic/simplifier/simplifier.cpp index a7fc537db3..d4c829b05a 100644 --- a/src/library/tactic/simplifier/simplifier.cpp +++ b/src/library/tactic/simplifier/simplifier.cpp @@ -168,7 +168,7 @@ class simplifier { optional m_curr_nary_op; - vm_obj m_prove_fn; + optional m_prove_fn; /* Logging */ unsigned m_num_steps{0}; @@ -360,25 +360,30 @@ class simplifier { list const * srs = sr->find_simp(e); if (!srs) { - lean_trace(name({"debug", "simplifier", "try_rewrite"}), tout() << "no simp lemmas for: " << e << "\n";); + lean_trace_d(name({"debug", "simplifier", "try_rewrite"}), tout() << "no simp lemmas for: " << e << "\n";); return simp_result(e); } for (simp_lemma const & lemma : *srs) { simp_result r = rewrite_binary(e, lemma); - if (r.has_proof()) + if (r.has_proof()) { + lean_trace_d(name({"simplifier", "rewrite"}), tout() << "[" << lemma.get_id() << "]: " << e << " ==> " << r.get_new() << "\n";); return r; + } } return simp_result(e); } simp_result rewrite_binary(expr const & e, simp_lemma const & sl) { tmp_type_context tmp_tctx(m_tctx, sl.get_num_umeta(), sl.get_num_emeta()); - if (!tmp_tctx.is_def_eq(e, sl.get_lhs())) + if (!tmp_tctx.is_def_eq(e, sl.get_lhs())) { + lean_trace_d(name({"debug", "simplifier", "try_rewrite"}), tout() << "fail to unify: " << sl.get_id() << "\n";); return simp_result(e); - - if (!instantiate_emetas(tmp_tctx, sl.get_num_emeta(), sl.get_emetas(), sl.get_instances())) + } + if (!instantiate_emetas(tmp_tctx, sl.get_num_emeta(), sl.get_emetas(), sl.get_instances())) { + lean_trace_d(name({"debug", "simplifier", "try_rewrite"}), tout() << "fail to instantiate emetas: " << sl.get_id() << "\n";); return simp_result(e); + } for (unsigned i = 0; i < sl.get_num_umeta(); i++) { if (!tmp_tctx.is_uassigned(i)) @@ -442,7 +447,6 @@ class simplifier { if (m_rewrite) { simp_result r_rewrite = simplify_rewrite_binary(e); if (r_rewrite.get_new() != e) { - lean_trace_d(name({"simplifier", "rewrite"}), tout() << e << " ==> " << r_rewrite.get_new() << "\n";); return r_rewrite; } } @@ -769,7 +773,7 @@ class simplifier { expr whnf_eta(expr const & e); public: - simplifier(type_context & tctx, name const & rel, simp_lemmas const & slss, vm_obj const & prove_fn): + simplifier(type_context & tctx, name const & rel, simp_lemmas const & slss, optional const & prove_fn): m_tctx(tctx), m_theory_simplifier(tctx), m_rel(rel), m_slss(slss), m_prove_fn(prove_fn), /* Options */ m_max_steps(get_simplify_max_steps(tctx.get_options())), @@ -920,11 +924,14 @@ simp_result simplifier::simplify_operator_of_app(expr const & e) { /* Proving */ optional simplifier::prove(expr const & goal) { + if (!m_prove_fn) + return none_expr(); + metavar_context mctx = m_tctx.mctx(); expr goal_mvar = mctx.mk_metavar_decl(m_tctx.lctx(), goal); lean_trace(name({"simplifier", "prove"}), tout() << "goal: " << goal_mvar << " : " << goal << "\n";); vm_obj s = to_obj(tactic_state(m_tctx.env(), m_tctx.get_options(), mctx, list(goal_mvar), goal_mvar)); - vm_obj prove_fn_result = invoke(m_prove_fn, s); + vm_obj prove_fn_result = invoke(*m_prove_fn, s); optional s_new = is_tactic_success(prove_fn_result); if (s_new) { if (!s_new->mctx().is_assigned(goal_mvar)) { @@ -1483,7 +1490,11 @@ void finalize_simplifier() { /* Entry point */ simp_result simplify(type_context & ctx, name const & rel, simp_lemmas const & simp_lemmas, vm_obj const & prove_fn, expr const & e) { - return simplifier(ctx, rel, simp_lemmas, prove_fn)(e); + return simplifier(ctx, rel, simp_lemmas, optional(prove_fn))(e); +} + +simp_result simplify(type_context & ctx, name const & rel, simp_lemmas const & simp_lemmas, expr const & e) { + return simplifier(ctx, rel, simp_lemmas, optional())(e); } } diff --git a/src/library/tactic/simplifier/simplifier.h b/src/library/tactic/simplifier/simplifier.h index 0ffb5ec357..96cf9e2b74 100644 --- a/src/library/tactic/simplifier/simplifier.h +++ b/src/library/tactic/simplifier/simplifier.h @@ -13,6 +13,7 @@ Author: Daniel Selsam namespace lean { simp_result simplify(type_context & ctx, name const & rel, simp_lemmas const & simp_lemmas, vm_obj const & prove_fn, expr const & e); +simp_result simplify(type_context & ctx, name const & rel, simp_lemmas const & simp_lemmas, expr const & e); void initialize_simplifier(); void finalize_simplifier(); diff --git a/src/library/util.cpp b/src/library/util.cpp index 452e18ac49..8823b4b430 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -200,6 +200,16 @@ bool is_inductive_predicate(environment const & env, name const & n) { return is_zero(get_datatype_level(env.get(n).get_type())); } +bool can_elim_to_type(environment const & env, name const & n) { + if (!is_standard(env)) + return true; + if (!inductive::is_inductive_decl(env, n)) + return false; // n is not inductive datatype + declaration ind_decl = env.get(n); + declaration rec_decl = env.get(inductive::get_elim_name(n)); + return rec_decl.get_num_univ_params() > ind_decl.get_num_univ_params(); +} + void get_intro_rule_names(environment const & env, name const & n, buffer & result) { if (auto decls = inductive::is_inductive_decl(env, n)) { for (inductive::inductive_decl const & decl : std::get<2>(*decls)) { @@ -504,6 +514,15 @@ expr mk_pr2(abstract_type_context & ctx, expr const & p) { return mk_app(mk_constant(get_prod_pr2_name(), const_levels(get_app_fn(AxB))), A, B, p); } +expr mk_nat_one() { + return mk_app(mk_constant(get_one_name(), {mk_level_one()}), {mk_constant(get_nat_name()), mk_constant(get_nat_has_one_name())}); +} + +expr mk_nat_add(expr const & e1, expr const & e2) { + expr nat_add = mk_app(mk_constant(get_add_name(), {mk_level_one()}), {mk_constant(get_nat_name()), mk_constant(get_nat_has_add_name())}); + return mk_app(nat_add, e1, e2); +} + expr mk_unit(level const & l, bool prop) { return prop ? mk_true() : mk_unit(l); } expr mk_unit_mk(level const & l, bool prop) { return prop ? mk_true_intro() : mk_unit_mk(l); } expr mk_prod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop) { diff --git a/src/library/util.h b/src/library/util.h index e448cd1ece..51037507b0 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -65,6 +65,9 @@ bool is_reflexive_datatype(abstract_type_context & tc, name const & n); \remark If \c env does not have Prop (i.e., Type.{0} is not impredicative), then this method always return false. */ bool is_inductive_predicate(environment const & env, name const & n); +/** \brief Return true iff \c n is an inductive type with a recursor with an extra level parameter. */ +bool can_elim_to_type(environment const & env, name const & n); + /** \brief Store in \c result the introduction rules of the given inductive datatype. \remark this procedure does nothing if \c n is not an inductive datatype. */ void get_intro_rule_names(environment const & env, name const & n, buffer & result); @@ -171,6 +174,9 @@ expr mk_pair(abstract_type_context & ctx, expr const & a, expr const & b, bool p expr mk_pr1(abstract_type_context & ctx, expr const & p, bool prop); expr mk_pr2(abstract_type_context & ctx, expr const & p, bool prop); +expr mk_nat_one(); +expr mk_nat_add(expr const & e1, expr const & e2); + bool is_ite(expr const & e, expr & c, expr & H, expr & A, expr & t, expr & f); bool is_ite(expr const & e); diff --git a/tests/lean/run/mutual_inductive.lean b/tests/lean/run/mutual_inductive.lean new file mode 100644 index 0000000000..fa28e6feb4 --- /dev/null +++ b/tests/lean/run/mutual_inductive.lean @@ -0,0 +1,201 @@ +namespace X1 + +mutual_inductive foo, bar +with foo : Type +| mk : foo +with bar : Type +| mk : bar + +check @foo +check @bar +check @foo.rec +check @bar.rec +check @foo.has_sizeof_inst +check @bar.has_sizeof_inst +check @foo.mk.sizeof_spec +check @bar.mk.sizeof_spec +end X1 + +namespace X2 + +mutual_inductive foo, bar +with foo : Type +| mk : bar -> foo +with bar : Type +| mk : foo -> bar + +check @foo +check @bar +check @foo.rec +check @bar.rec +check @foo.has_sizeof_inst +check @bar.has_sizeof_inst +check @foo.mk.sizeof_spec +check @bar.mk.sizeof_spec +end X2 + +namespace X3 + +mutual_inductive foo, bar +with foo : bool -> Type +| mk : bar -> foo tt +with bar : Type +| mk : foo tt -> bar + +check @foo +check @bar +check @foo.rec +check @bar.rec +check @foo.has_sizeof_inst +check @bar.has_sizeof_inst +check @foo.mk.sizeof_spec +check @bar.mk.sizeof_spec +end X3 + +namespace X4 + +mutual_inductive foo, bar, rig +with foo : bool -> bool -> Type +| mk : bar tt -> foo tt tt +with bar : bool -> Type +| mk : foo tt tt -> bar tt +with rig : Type +| mk : foo tt tt -> bar tt -> rig + +check @foo +check @bar +check @rig +check @foo.rec +check @bar.rec +check @rig.rec +check @foo.has_sizeof_inst +check @bar.has_sizeof_inst +check @rig.has_sizeof_inst +check @foo.mk.sizeof_spec +check @bar.mk.sizeof_spec +check @rig.mk.sizeof_spec +end X4 + +namespace X5 + +mutual_inductive foo, bar, rig +with foo : bool -> bool -> Prop +| mk : bar tt -> foo tt tt +with bar : bool -> Prop +| mk : foo tt tt -> bar tt +with rig : Prop +| mk : foo tt tt -> bar tt -> rig + +check @foo +check @bar +check @rig +check @foo.rec +check @bar.rec +check @rig.rec +end X5 + +namespace X6 + +mutual_inductive foo, bar, rig (A : Type) +with foo : bool -> bool -> Prop +| mk : A -> bar tt -> foo tt tt +with bar : bool -> Prop +| mk : A -> foo tt tt -> bar tt +with rig : Prop +| mk : A -> foo tt tt -> bar tt -> rig + +check @foo +check @bar +check @rig +check @foo.rec +check @bar.rec +check @rig.rec +end X6 + +namespace X7 + +mutual_inductive foo, bar, rig (A : Type) +with foo : Pi (b : bool), b = b -> Type +| mk : A -> bar tt ff tt -> foo tt rfl +with bar : bool -> bool -> bool -> Type +| mk : A -> foo tt rfl -> bar tt ff tt +with rig : Type +| mk : A -> foo tt rfl -> bar tt ff tt -> rig +| put : A -> foo tt rfl -> bar tt ff tt -> rig + +check @foo +check @bar +check @rig +check @foo.rec +check @bar.rec +check @rig.rec +check @foo.has_sizeof_inst +check @bar.has_sizeof_inst +check @rig.has_sizeof_inst +check @foo.mk.sizeof_spec +check @bar.mk.sizeof_spec +check @rig.mk.sizeof_spec +check @rig.put.sizeof_spec +end X7 + +namespace X8 + +mutual_inductive {l₁ l₂} foo, bar, rig (A : Type.{l₁}) (B : Type.{l₂}) +with foo : Pi (b : bool), b = b -> Type.{max l₁ l₂} +| mk : A -> B -> bar tt ff tt -> foo tt rfl +with bar : bool -> bool -> bool -> Type.{max l₁ l₂} +| mk : A -> B -> foo tt rfl -> bar tt ff tt +with rig : Type.{max l₁ l₂} +| mk : A -> B -> foo tt rfl -> bar tt ff tt -> rig + +check @foo +check @bar +check @rig +check @foo.rec +check @bar.rec +check @rig.rec +end X8 + +namespace X9 + +mutual_inductive {l₁ l₂ l₃} foo, bar, rig (A : Type.{l₁}) (B : Type.{l₂}) (a : A) +with foo : Pi (b : bool), b = b -> Type.{max l₁ l₂ l₃} +| mk : A -> B -> Pi x : A, x = a -> bar tt ff tt -> foo tt rfl +with bar : bool -> bool -> bool -> Type.{max l₁ l₂ l₃} +| mk : A -> B -> foo tt rfl -> bar tt ff tt +with rig : Type.{max l₁ l₂ l₃} +| mk : A -> B -> (Pi x : A, x = a -> foo tt rfl) -> bar tt ff tt -> rig + +check @foo +check @bar +check @rig +check @foo.rec +check @bar.rec +check @rig.rec + +end X9 + +namespace X10 + +mutual_inductive foo, bar, rig +with foo : Type -> Type +| mk : bar (foo poly_unit) -> foo (bar poly_unit) +with bar : Type -> Type +| mk : foo (bar poly_unit) -> bar (foo poly_unit) +with rig : Type -> Type +| mk : foo (bar (rig poly_unit)) -> rig (bar (foo poly_unit)) -> rig (bar (foo poly_unit)) + +check @foo +check @bar +check @rig +check @foo.rec +check @bar.rec +check @rig.rec +check @foo.has_sizeof_inst +check @bar.has_sizeof_inst +check @rig.has_sizeof_inst +check @foo.mk.sizeof_spec +check @bar.mk.sizeof_spec +check @rig.mk.sizeof_spec + +end X10