max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/compiler/util): add support for trivial structures at mk_runtime_type

Browse source
This commit is contained in:
Leonardo de Moura 2019-09-11 13:41:41 -07:00
parent 1062dcbbea
commit 3e6736b374
1 changed files with 42 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

49
src/library/compiler/util.cpp
View file

@ -462,6 +462,7 @@ expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e) {
try {
type_checker tc(st, lctx);
e = tc.whnf(e);
if (is_constant(e)) {
name const & c = const_name(e);
if (is_runtime_scalar_type(c)) {
@ -472,17 +473,51 @@ expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e) {
return e;
} else if (optional<unsigned> nbytes = is_enum_type(st.env(), c)) {
return *to_uint_type(*nbytes);
} else {
return mk_enf_object_type();
}
} else if (is_app_of(e, get_decidable_name())) {
}
if (is_app_of(e, get_decidable_name())) {
/* Recall that `decidable A` and `bool` have the same runtime representation. */
return *to_uint_type(1);
} else if (is_sort(e) || tc.is_prop(e)) {
return mk_enf_neutral_type();
} else {
return mk_enf_object_type();
}
if (is_sort(e) || tc.is_prop(e)) {
return mk_enf_neutral_type();
}
/* If `e` is a trivial structure such as `Subtype`, then convert the only relevant
field to a runtime type. */
if (is_app(e)) {
expr const & fn = get_app_fn(e);
if (is_constant(fn) && is_inductive(st.env(), const_name(fn))) {
name const & I_name = const_name(fn);
environment const & env = st.env();
if (optional<unsigned> fidx = has_trivial_structure(env, I_name)) {
/* Retrieve field `fidx` type */
inductive_val I_val = env.get(I_name).to_inductive_val();
name K = head(I_val.get_cnstrs());
unsigned nparams = I_val.get_nparams();
buffer<expr> e_args;
get_app_args(e, e_args);
lean_assert(nparams <= e_args.size());
expr k_app = mk_app(mk_constant(K, const_levels(fn)), nparams, e_args.data());
expr type = tc.whnf(tc.infer(k_app));
local_ctx aux_lctx = lctx;
unsigned idx = 0;
while (is_pi(type)) {
if (idx == *fidx) {
return mk_runtime_type(st, aux_lctx, binding_domain(type));
}
expr local = aux_lctx.mk_local_decl(st.ngen(), binding_name(type), binding_domain(type), binding_info(type));
type = instantiate(binding_body(type), local);
type = type_checker(st, aux_lctx).whnf(type);
idx++;
}
}
}
}
return mk_enf_object_type();
} catch (kernel_exception &) {
return mk_enf_object_type();
}