From 858538a3294a01e57b216300ace81b492b667fb5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 12 Nov 2014 13:31:31 -0800 Subject: [PATCH] refactor(library/definitional): add new to_telescope procedure, and remove code duplication in no_confusion.cpp --- src/library/definitional/no_confusion.cpp | 33 ++++------------------- src/library/definitional/util.cpp | 15 +++++++++++ src/library/definitional/util.h | 3 +++ 3 files changed, 23 insertions(+), 28 deletions(-) diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp index c4a35fbea..7a8c67537 100644 --- a/src/library/definitional/no_confusion.cpp +++ b/src/library/definitional/no_confusion.cpp @@ -39,11 +39,7 @@ optional mk_no_confusion_type(environment const & env, name const & name heq_name("heq"); // All inductive datatype parameters and indices are arguments buffer args; - while (is_pi(ind_type)) { - expr arg = mk_local(ngen.next(), binding_name(ind_type), binding_domain(ind_type), mk_implicit_binder_info()); - args.push_back(arg); - ind_type = instantiate(binding_body(ind_type), arg); - } + ind_type = to_telescope(ngen, ind_type, args, some(mk_implicit_binder_info())); if (!is_sort(ind_type) || args.size() < nparams) throw_corrupted(n); lean_assert(!(env.impredicative() && is_zero(sort_level(ind_type)))); @@ -79,24 +75,14 @@ optional mk_no_confusion_type(environment const & env, name const & buffer outer_cases_on_args; unsigned idx1 = 0; while (is_pi(t1)) { - expr minor1 = tc.whnf(binding_domain(t1)).first; buffer minor1_args; - while (is_pi(minor1)) { - expr arg = mk_local(ngen.next(), binding_name(minor1), binding_domain(minor1), binding_info(minor1)); - minor1_args.push_back(arg); - minor1 = tc.whnf(instantiate(binding_body(minor1), arg)).first; - } + expr minor1 = to_telescope(tc, binding_domain(t1), minor1_args); expr curr_t2 = t2; buffer inner_cases_on_args; unsigned idx2 = 0; while (is_pi(curr_t2)) { - expr minor2 = tc.whnf(binding_domain(curr_t2)).first; buffer minor2_args; - while (is_pi(minor2)) { - expr arg = mk_local(ngen.next(), binding_name(minor2), binding_domain(minor2), binding_info(minor2)); - minor2_args.push_back(arg); - minor2 = tc.whnf(instantiate(binding_body(minor2), arg)).first; - } + expr minor2 = to_telescope(tc, binding_domain(curr_t2), minor2_args); if (idx1 != idx2) { // infeasible case, constructors do not match inner_cases_on_args.push_back(Fun(minor2_args, P)); @@ -158,11 +144,7 @@ environment mk_no_confusion(environment const & env, name const & n) { name heq_refl_name{"heq", "refl"}; buffer args; expr type = no_confusion_type_type; - while (is_pi(type)) { - expr arg = mk_local(ngen.next(), binding_name(type), binding_domain(type), mk_implicit_binder_info()); - args.push_back(arg); - type = instantiate(binding_body(type), arg); - } + type = to_telescope(ngen, type, args, some(mk_implicit_binder_info())); lean_assert(args.size() >= nparams + 3); unsigned nindices = args.size() - nparams - 3; // 3 is for P v1 v2 expr range = mk_app(mk_constant(no_confusion_type_decl.get_name(), ls), args); @@ -205,13 +187,8 @@ environment mk_no_confusion(environment const & env, name const & n) { expr cot = tc.infer(cases_on).first; while (is_pi(cot)) { - expr minor = tc.whnf(binding_domain(cot)).first; buffer minor_args; - while (is_pi(minor)) { - expr arg = mk_local(ngen.next(), binding_name(minor), binding_domain(minor), binding_info(minor)); - minor_args.push_back(arg); - minor = tc.whnf(instantiate(binding_body(minor), arg)).first; - } + expr minor = to_telescope(tc, binding_domain(cot), minor_args); lean_assert(!minor_args.empty()); expr H = minor_args.back(); expr Ht = mlocal_type(H); diff --git a/src/library/definitional/util.cpp b/src/library/definitional/util.cpp index 5d4b02c09..5d853f0f4 100644 --- a/src/library/definitional/util.cpp +++ b/src/library/definitional/util.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/find_fn.h" #include "kernel/instantiate.h" +#include "kernel/type_checker.h" #include "kernel/inductive/inductive.h" namespace lean { @@ -93,4 +94,18 @@ expr to_telescope(name_generator & ngen, expr type, buffer & telescope, op } return type; } + +expr to_telescope(type_checker & tc, expr type, buffer & telescope, optional const & binfo) { + type = tc.whnf(type).first; + while (is_pi(type)) { + expr local; + if (binfo) + local = mk_local(tc.mk_fresh_name(), binding_name(type), binding_domain(type), *binfo); + else + local = mk_local(tc.mk_fresh_name(), binding_name(type), binding_domain(type), binder_info(type)); + telescope.push_back(local); + type = tc.whnf(instantiate(binding_body(type), local)).first; + } + return type; +} } diff --git a/src/library/definitional/util.h b/src/library/definitional/util.h index a9dea4555..f54e4ac40 100644 --- a/src/library/definitional/util.h +++ b/src/library/definitional/util.h @@ -35,6 +35,9 @@ bool is_inductive_predicate(environment const & env, name const & n); */ expr to_telescope(name_generator & ngen, expr type, buffer & telescope, optional const & binfo = optional()); +/** \brief Similar to previous method, but puts \c type in whnf */ +expr to_telescope(type_checker & tc, expr type, buffer & telescope, + optional const & binfo = optional()); /** \brief Return the universe where inductive datatype resides \pre \c ind_type is of the form Pi (a_1 : A_1) (a_2 : A_2[a_1]) ..., Type.{lvl}