Merge pull request #247 from HigherOrderCO/feature/sc-540/use-hvm-cor…

…e-eta-reduction-pass [sc-540] Use hvm-core eta-reduction pass
HigherOrderCO · Apr 1, 2024 · 1a6281a · 1a6281a
2 parents b382830 + 3126eba
commit 1a6281a
Show file tree

Hide file tree

Showing 14 changed files with 35 additions and 74 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/src/lib.rs b/src/lib.rs
@@ -46,9 +46,15 @@ pub fn compile_book(
 
   let mut core_book = nets_to_hvmc(nets, &mut diagnostics)?;
 
+  if opts.eta {
+    core_book.values_mut().for_each(Net::eta_reduce);
+  }
   if opts.pre_reduce {
     core_book.pre_reduce(&|x| x == book.hvmc_entrypoint(), None, 100_000);
   }
+  if opts.eta {
+    core_book.values_mut().for_each(Net::eta_reduce);
+  }
   if opts.prune {
     prune_defs(&mut core_book, book.hvmc_entrypoint().to_string());
   }
@@ -101,9 +107,6 @@ pub fn desugar_book(
   ctx.check_unbound_vars()?;
 
   // Optimizing passes
-  if opts.eta {
-    ctx.book.eta_reduction();
-  }
   if opts.float_combinators {
     ctx.book.float_combinators();
   }

diff --git a/src/term/transform/eta_reduction.rs b/src/term/transform/eta_reduction.rs
diff --git a/src/term/transform/mod.rs b/src/term/transform/mod.rs
@@ -5,7 +5,6 @@ pub mod definition_pruning;
 pub mod desugar_match_defs;
 pub mod encode_adts;
 pub mod encode_match_terms;
-pub mod eta_reduction;
 pub mod fix_match_defs;
 pub mod fix_match_terms;
 pub mod float_combinators;

diff --git a/tests/golden_tests/cli/desugar_eta.args b/tests/golden_tests/cli/desugar_eta.args
diff --git a/tests/golden_tests/cli/desugar_eta.hvm b/tests/golden_tests/cli/desugar_eta.hvm
diff --git a/tests/golden_tests/compile_file_o_all/eta_chain.hvm b/tests/golden_tests/compile_file_o_all/eta_chain.hvm
@@ -2,4 +2,4 @@ Baz a b c = (+ a (+ b c))
 Bar a b = (Baz a b)
 Foo a = (Bar a)
 
-main = λa (Foo a)
+main = λa (Foo a)
diff --git a/tests/golden_tests/compile_file_o_all/unapplied_eta.hvm b/tests/golden_tests/compile_file_o_all/unapplied_eta.hvm
@@ -1,2 +1,2 @@
 Id = λa a
-main = λa (Id a)
+main = λa (Id a)
diff --git a/tests/snapshots/cli__desugar_eta.hvm.snap b/tests/snapshots/cli__desugar_eta.hvm.snap
diff --git a/tests/snapshots/compile_file_o_all__eta_chain.hvm.snap b/tests/snapshots/compile_file_o_all__eta_chain.hvm.snap
@@ -2,4 +2,11 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/eta_chain.hvm
 ---
-@main = (<+ a b> (<+ c a> (c b)))
+@Bar = @Baz
+
+@Baz = (<+ a b> (<+ c a> (c b)))
+
+@Foo = @Bar
+
+@main = a
+  & @Foo ~ a
diff --git a/tests/snapshots/compile_file_o_all__ex2.hvm.snap b/tests/snapshots/compile_file_o_all__ex2.hvm.snap
@@ -8,7 +8,9 @@ input_file: tests/golden_tests/compile_file_o_all/ex2.hvm
 
 @c2 = ({3 (a b) (c a)} (c b))
 
-@decO = ((@decO (@low (@E a))) (* ((a b) (* b))))
+@decI = @low
+
+@decO = ((@decO (@decI (@E a))) (* ((a b) (* b))))
 
 @low = ((@lowO (@lowI (@E a))) a)
 
@@ -24,4 +26,4 @@ input_file: tests/golden_tests/compile_file_o_all/ex2.hvm
 
 @runI = ((@lowO (@lowI (@E (@runO (@runI (@E a)))))) a)
 
-@runO = ((@decO (@low (@E (@lowO (@lowI (@E (@runO (@runI (@E a))))))))) a)
+@runO = ((@decO (@decI (@E (@lowO (@lowI (@E (@runO (@runI (@E a))))))))) a)
diff --git a/tests/snapshots/compile_file_o_all__extracted_match_pred.hvm.snap b/tests/snapshots/compile_file_o_all__extracted_match_pred.hvm.snap
@@ -5,4 +5,8 @@ input_file: tests/golden_tests/compile_file_o_all/extracted_match_pred.hvm
 @main = a
   & @val ~ (#1 a)
 
-@val = (?<#0 @val a> a)
+@val = (?<#0 @val$C0 a> a)
+
+@val$C0 = @valS
+
+@valS = @val
diff --git a/tests/snapshots/compile_file_o_all__list_merge_sort.hvm.snap b/tests/snapshots/compile_file_o_all__list_merge_sort.hvm.snap
@@ -8,13 +8,15 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
 
 @Map$C0 = {4 a {4 {4 @Map$C0 {4 (* @Nil) (b c)}} ({3 (a d) b} {4 {4 d {4 c e}} {4 * e}})}}
 
-@Merge$C0 = {4 {5 a {5 b c}} {4 {7 d {4 @Merge$C0 {4 (* @Cons) (e (f (g h)))}}} ({9 (i (a {2 (j (* j)) {2 (* (k k)) ({4 {4 l {4 m n}} {4 * n}} ({4 {4 c {4 h o}} {4 * o}} p))}})) {9 q e}} ({11 i {11 l f}} ({13 {4 @Merge$C1 {4 (* (r r)) (q ({4 {4 b {4 d s}} {4 * s}} m))}} g} p)))}}
+@Merge$C0 = (* @Cons)
 
-@Merge$C1 = {4 a {4 b (c ({4 @Merge$C0 {4 (* @Cons) (c (a (b d)))}} d))}}
+@Merge$C1 = {4 {5 a {5 b c}} {4 {7 d {4 @Merge$C1 {4 @Merge$C0 (e (f (g h)))}}} ({9 (i (a {2 (j (* j)) {2 (* (k k)) ({4 {4 l {4 m n}} {4 * n}} ({4 {4 c {4 h o}} {4 * o}} p))}})) {9 q e}} ({11 i {11 l f}} ({13 {4 @Merge$C2 {4 (* (r r)) (q ({4 {4 b {4 d s}} {4 * s}} m))}} g} p)))}}
+
+@Merge$C2 = {4 a {4 b (c ({4 @Merge$C1 {4 @Merge$C0 (c (a (b d)))}} d))}}
 
 @MergePair$C0 = (* (a {4 {4 a {4 @Nil b}} {4 * b}}))
 
-@MergePair$C1 = {4 a {4 {4 @MergePair$C2 {4 (* @Nil) (b c)}} ({15 d b} ({4 @Merge$C1 {4 (* (e e)) (d (a f))}} {4 {4 f {4 c g}} {4 * g}}))}}
+@MergePair$C1 = {4 a {4 {4 @MergePair$C2 {4 (* @Nil) (b c)}} ({15 d b} ({4 @Merge$C2 {4 (* (e e)) (d (a f))}} {4 {4 f {4 c g}} {4 * g}}))}}
 
 @MergePair$C2 = {4 a {4 {4 @MergePair$C1 {4 @MergePair$C0 (b (a c))}} (b c)}}
 
@@ -24,7 +26,7 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
 
 @Unpack = (a ({4 @Unpack$C1 {4 (* @Nil) (a b)}} b))
 
-@Unpack$C0 = {4 a {4 {4 @MergePair$C2 {4 (* @Nil) (b {4 @Unpack$C0 {4 (* (c c)) (d (e f))}})}} ({17 d {15 g b}} ({4 @Merge$C1 {4 (* (h h)) (g (a e))}} f))}}
+@Unpack$C0 = {4 a {4 {4 @MergePair$C2 {4 (* @Nil) (b {4 @Unpack$C0 {4 (* (c c)) (d (e f))}})}} ({17 d {15 g b}} ({4 @Merge$C2 {4 (* (h h)) (g (a e))}} f))}}
 
 @Unpack$C1 = {4 a {4 {4 @Unpack$C0 {4 (* (b b)) (c (a d))}} (c d)}}
 

diff --git a/tests/snapshots/compile_file_o_all__unapplied_eta.hvm.snap b/tests/snapshots/compile_file_o_all__unapplied_eta.hvm.snap
@@ -2,4 +2,5 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/unapplied_eta.hvm
 ---
-@main = (a a)
+@main = a
+  & (c c) ~ a