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

fix(library/compiler/compiler): make sure that the type of functions that return closures match their arity

Browse source 
Before this commit, we could have a LLNF function `f` of arity 0 and
type `_obj -> _obj`. Now, this kind of function has type `_obj`.
This commit is contained in:
Leonardo de Moura 2019-01-25 15:40:25 -08:00
parent dd30cac8aa
commit 274aeed30f
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/library/compiler/compiler.cpp
View file

@ -76,11 +76,22 @@ static environment cache_stage1(environment env, comp_decls const & ds) {
return env;
}
static expr ensure_arity(expr const & t, unsigned arity) {
if (arity == 0) {
if (is_pi(t)) return mk_enf_object_type(); // closure
else return t;
}
lean_assert(is_pi(t));
return ensure_arity(binding_body(t), arity-1);
}
static environment cache_stage2(environment env, comp_decls const & ds) {
for (comp_decl const & d : ds) {
name n = d.fst();
expr v = d.snd();
expr t = ll_infer_type(env, v);
unsigned arity = get_num_nested_lambdas(v);
v = ensure_arity(t, arity);
lean_trace(name({"compiler", "stage2"}), tout() << n << " : " << t << "\n";);
env = register_stage2_decl(env, n, t, v);
}