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

fix: #1087

Browse source 
This commit is using the easy fix described at issue #1087.
Hopefully the performance overhead is small.

closes #1087
This commit is contained in:
Leonardo de Moura 2022-03-30 18:48:02 -07:00
parent 63b9060ce9
commit 2bd04285f8
2 changed files with 29 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/runtime/apply.cpp
View file

@ -99,6 +99,7 @@ default: return reinterpret_cast<fnn>(f)(as);
static obj* curry(obj* f, unsigned n, obj** as) { return curry(lean_closure_fun(f), n, as); }
extern "C" obj* lean_apply_n(obj*, unsigned, obj**);
extern "C" LEAN_EXPORT obj* lean_apply_1(obj* f, obj* a1) {
if (lean_is_scalar(f)) { lean_dec(a1); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 1) {
@ -157,6 +158,7 @@ if (arity == fixed + 1) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_2(obj* f, obj* a1, obj* a2) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 2) {
@ -218,6 +220,7 @@ if (arity == fixed + 2) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_3(obj* f, obj* a1, obj* a2, obj* a3) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 3) {
@ -277,6 +280,7 @@ if (arity == fixed + 3) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_4(obj* f, obj* a1, obj* a2, obj* a3, obj* a4) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 4) {
@ -334,6 +338,7 @@ if (arity == fixed + 4) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_5(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4); lean_dec(a5); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 5) {
@ -389,6 +394,7 @@ if (arity == fixed + 5) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_6(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4); lean_dec(a5); lean_dec(a6); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 6) {
@ -442,6 +448,7 @@ if (arity == fixed + 6) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_7(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* a7) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4); lean_dec(a5); lean_dec(a6); lean_dec(a7); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 7) {
@ -493,6 +500,7 @@ if (arity == fixed + 7) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_8(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* a7, obj* a8) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4); lean_dec(a5); lean_dec(a6); lean_dec(a7); lean_dec(a8); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 8) {
@ -542,6 +550,7 @@ if (arity == fixed + 8) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_9(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* a7, obj* a8, obj* a9) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4); lean_dec(a5); lean_dec(a6); lean_dec(a7); lean_dec(a8); lean_dec(a9); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 9) {
@ -589,6 +598,7 @@ if (arity == fixed + 9) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_10(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* a7, obj* a8, obj* a9, obj* a10) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4); lean_dec(a5); lean_dec(a6); lean_dec(a7); lean_dec(a8); lean_dec(a9); lean_dec(a10); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 10) {
@ -634,6 +644,7 @@ if (arity == fixed + 10) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_11(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* a7, obj* a8, obj* a9, obj* a10, obj* a11) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4); lean_dec(a5); lean_dec(a6); lean_dec(a7); lean_dec(a8); lean_dec(a9); lean_dec(a10); lean_dec(a11); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 11) {
@ -677,6 +688,7 @@ if (arity == fixed + 11) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_12(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* a7, obj* a8, obj* a9, obj* a10, obj* a11, obj* a12) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4); lean_dec(a5); lean_dec(a6); lean_dec(a7); lean_dec(a8); lean_dec(a9); lean_dec(a10); lean_dec(a11); lean_dec(a12); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 12) {
@ -718,6 +730,7 @@ if (arity == fixed + 12) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_13(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* a7, obj* a8, obj* a9, obj* a10, obj* a11, obj* a12, obj* a13) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4); lean_dec(a5); lean_dec(a6); lean_dec(a7); lean_dec(a8); lean_dec(a9); lean_dec(a10); lean_dec(a11); lean_dec(a12); lean_dec(a13); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 13) {
@ -757,6 +770,7 @@ if (arity == fixed + 13) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_14(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* a7, obj* a8, obj* a9, obj* a10, obj* a11, obj* a12, obj* a13, obj* a14) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4); lean_dec(a5); lean_dec(a6); lean_dec(a7); lean_dec(a8); lean_dec(a9); lean_dec(a10); lean_dec(a11); lean_dec(a12); lean_dec(a13); lean_dec(a14); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 14) {
@ -794,6 +808,7 @@ if (arity == fixed + 14) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_15(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* a7, obj* a8, obj* a9, obj* a10, obj* a11, obj* a12, obj* a13, obj* a14, obj* a15) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4); lean_dec(a5); lean_dec(a6); lean_dec(a7); lean_dec(a8); lean_dec(a9); lean_dec(a10); lean_dec(a11); lean_dec(a12); lean_dec(a13); lean_dec(a14); lean_dec(a15); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 15) {
@ -829,6 +844,7 @@ if (arity == fixed + 15) {
}
}
extern "C" LEAN_EXPORT obj* lean_apply_16(obj* f, obj* a1, obj* a2, obj* a3, obj* a4, obj* a5, obj* a6, obj* a7, obj* a8, obj* a9, obj* a10, obj* a11, obj* a12, obj* a13, obj* a14, obj* a15, obj* a16) {
if (lean_is_scalar(f)) { lean_dec(a1); lean_dec(a2); lean_dec(a3); lean_dec(a4); lean_dec(a5); lean_dec(a6); lean_dec(a7); lean_dec(a8); lean_dec(a9); lean_dec(a10); lean_dec(a11); lean_dec(a12); lean_dec(a13); lean_dec(a14); lean_dec(a15); lean_dec(a16); return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + 16) {
@ -863,6 +879,7 @@ if (arity == fixed + 16) {
}
extern "C" LEAN_EXPORT obj* lean_apply_m(obj* f, unsigned n, obj** as) {
lean_assert(n > 16);
if (lean_is_scalar(f)) { for (unsigned i = 0; i < n; i++) { lean_dec(as[i]); } return f; } // f is an erased proof
unsigned arity = lean_closure_arity(f);
unsigned fixed = lean_closure_num_fixed(f);
if (arity == fixed + n) {

12
tests/lean/run/proofDataConfusionBug.lean Normal file
View file

@ -0,0 +1,12 @@
def combine : PSum Unit (p → q) → PSum Unit p → PSum Unit q
| PSum.inr f, PSum.inr proof => PSum.inr $ f proof
| _, _ => PSum.inl ()
def tst : String :=
let f : PSum Unit (True → True) := .inr id
let v : PSum Unit True := .inr .intro
match combine f v with
| .inr _ => "inr"
| .inl _ => "inl"
#eval tst