Skip to content

Commit b5c13fa

Browse files
committed
improve whir recursion cycle count
1 parent 67afea2 commit b5c13fa

File tree

1 file changed

+37
-43
lines changed

1 file changed

+37
-43
lines changed

crates/rec_aggregation/recursion_program.lean_lang

Lines changed: 37 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -504,73 +504,67 @@ fn dot_product_ee_dynamic(a, b, res, n) {
504504
if n == 16 {
505505
dot_product_ee(a, b, res, 16);
506506
return;
507+
} else {
508+
if n == NUM_QUERIES_0 {
509+
dot_product_ee(a, b, res, NUM_QUERIES_0);
510+
return;
511+
} else {
512+
dot_product_ee_dynamic_helper_1(a, b, res, n);
513+
return;
514+
}
507515
}
508516

509-
dot_product_ee_dynamic_helper_1(a, b, res, n);
510-
return;
511517
}
512518

513519
fn dot_product_ee_dynamic_helper_1(a, b, res, n) {
514-
if n == NUM_QUERIES_0 {
515-
dot_product_ee(a, b, res, NUM_QUERIES_0);
516-
return;
517-
}
518-
519-
dot_product_ee_dynamic_helper_2(a, b, res, n);
520-
return;
521-
}
522-
523-
fn dot_product_ee_dynamic_helper_2(a, b, res, n) {
524520
if n == NUM_QUERIES_1 {
525521
dot_product_ee(a, b, res, NUM_QUERIES_1);
526522
return;
523+
} else {
524+
if n == NUM_QUERIES_2 {
525+
dot_product_ee(a, b, res, NUM_QUERIES_2);
526+
return;
527+
} else {
528+
dot_product_ee_dynamic_helper_3(a, b, res, n);
529+
return;
530+
}
527531
}
528-
if n == NUM_QUERIES_2 {
529-
dot_product_ee(a, b, res, NUM_QUERIES_2);
530-
return;
531-
}
532-
533-
dot_product_ee_dynamic_helper_3(a, b, res, n);
534-
return;
535532
}
536533

537534
fn dot_product_ee_dynamic_helper_3(a, b, res, n) {
538535
if n == NUM_QUERIES_3 {
539536
dot_product_ee(a, b, res, NUM_QUERIES_3);
540537
return;
538+
} else {
539+
if n == NUM_QUERIES_0 + 1 {
540+
dot_product_ee(a, b, res, NUM_QUERIES_0 + 1);
541+
return;
542+
} else {
543+
dot_product_ee_dynamic_helper_4(a, b, res, n);
544+
return;
545+
}
541546
}
542-
if n == NUM_QUERIES_0 + 1 {
543-
dot_product_ee(a, b, res, NUM_QUERIES_0 + 1);
544-
return;
545-
}
546-
547-
dot_product_ee_dynamic_helper_4(a, b, res, n);
548-
return;
549547
}
550548

551549
fn dot_product_ee_dynamic_helper_4(a, b, res, n) {
552550
if n == NUM_QUERIES_1 + 1 {
553551
dot_product_ee(a, b, res, NUM_QUERIES_1 + 1);
554552
return;
555-
}
556-
if n == NUM_QUERIES_2 + 1 {
557-
dot_product_ee(a, b, res, NUM_QUERIES_2 + 1);
558-
return;
559-
}
560-
561-
dot_product_ee_dynamic_helper_5(a, b, res, n);
562-
return;
563-
}
553+
} else {
554+
if n == NUM_QUERIES_2 + 1 {
555+
dot_product_ee(a, b, res, NUM_QUERIES_2 + 1);
556+
return;
557+
} else {
558+
if n == NUM_QUERIES_3 + 1 {
559+
dot_product_ee(a, b, res, NUM_QUERIES_3 + 1);
560+
return;
561+
}
564562

565-
fn dot_product_ee_dynamic_helper_5(a, b, res, n) {
566-
if n == NUM_QUERIES_3 + 1 {
567-
dot_product_ee(a, b, res, NUM_QUERIES_3 + 1);
568-
return;
563+
TODO_dot_product_ee_dynamic = 0;
564+
print(TODO_dot_product_ee_dynamic, n);
565+
panic();
566+
}
569567
}
570-
571-
TODO_dot_product_ee_dynamic = 0;
572-
print(TODO_dot_product_ee_dynamic, n);
573-
panic();
574568
}
575569

576570
fn poly_eq_extension(point, n, two_pow_n) -> 1 {

0 commit comments

Comments
 (0)