michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/definitional): add some helper functions

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-12 12:24:22 -08:00
parent 463e70332d
commit b4c37d180b
3 changed files with 23 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/library/definitional/induction_on.cpp
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "kernel/type_checker.h"
#include "library/module.h"
#include "library/protected.h"
#include "library/definitional/util.h"
namespace lean {
environment mk_induction_on(environment const & env, name const & n) {
@ -35,10 +36,10 @@ environment mk_induction_on(environment const & env, name const & n) {
new_env = module::add(new_env, cdecl);
} else {
level_param_names induction_on_univs = tail(rec_on_decl.get_univ_params());
level_param_names from = to_list(head(rec_on_decl.get_univ_params()));
levels to = to_list(mk_level_zero());
expr induction_on_type = instantiate_univ_params(rec_on_decl.get_type(), from, to);
expr induction_on_value = instantiate_univ_params(rec_on_decl.get_value(), from, to);
name from = head(rec_on_decl.get_univ_params());
level to = mk_level_zero();
expr induction_on_type = instantiate_univ_param(rec_on_decl.get_type(), from, to);
expr induction_on_value = instantiate_univ_param(rec_on_decl.get_value(), from, to);
certified_declaration cdecl = check(new_env,
mk_definition(new_env, induction_on_name, induction_on_univs,
induction_on_type, induction_on_value,

16
src/library/definitional/util.cpp
View file

@ -63,16 +63,22 @@ bool is_recursive_datatype(environment const & env, name const & n) {
return false;
}
level get_datatype_level(expr ind_type) {
while (is_pi(ind_type))
ind_type = binding_body(ind_type);
return sort_level(ind_type);
}
bool is_inductive_predicate(environment const & env, name const & n) {
if (!env.impredicative())
return false; // environment does not have Prop
if (!inductive::is_inductive_decl(env, n))
return false; // n is not inductive datatype
expr type = env.get(n).get_type();
while (is_pi(type)) {
type = binding_body(type);
}
return is_sort(type) && is_zero(sort_level(type));
return is_zero(get_datatype_level(env.get(n).get_type()));
}
expr instantiate_univ_param (expr const & e, name const & p, level const & l) {
return instantiate_univ_params(e, to_list(p), to_list(l));
}
expr to_telescope(name_generator & ngen, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo) {

7
src/library/definitional/util.h
View file

@ -35,4 +35,11 @@ bool is_inductive_predicate(environment const & env, name const & n);
*/
expr to_telescope(name_generator & ngen, expr type, buffer<expr> & telescope,
optional<binder_info> const & binfo = optional<binder_info>());
/** \brief Return the universe where inductive datatype resides
\pre \c ind_type is of the form <tt>Pi (a_1 : A_1) (a_2 : A_2[a_1]) ..., Type.{lvl}</tt>
*/
level get_datatype_level(expr ind_type);
expr instantiate_univ_param (expr const & e, name const & p, level const & l);
}