From b8a9632f5cc4e65da1f96bd24354b38bcc22d43a Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Mon, 1 Apr 2024 10:42:15 -0300
Subject: [PATCH 1/2] Use inet level eta reduction pass

---
 Cargo.lock                                    |  4 +-
 src/lib.rs                                    |  6 +--
 src/term/transform/eta_reduction.rs           | 41 -------------------
 src/term/transform/mod.rs                     |  3 --
 tests/golden_tests/cli/desugar_eta.args       |  3 --
 tests/golden_tests/cli/desugar_eta.hvm        |  4 --
 .../compile_file_o_all/eta_chain.hvm          |  5 ---
 .../compile_file_o_all/unapplied_eta.hvm      |  2 -
 tests/snapshots/cli__desugar_eta.hvm.snap     |  9 ----
 .../compile_file_o_all__ex2.hvm.snap          |  6 ++-
 ..._file_o_all__extracted_match_pred.hvm.snap |  6 ++-
 ...mpile_file_o_all__list_merge_sort.hvm.snap | 10 +++--
 12 files changed, 20 insertions(+), 79 deletions(-)
 delete mode 100644 src/term/transform/eta_reduction.rs
 delete mode 100644 tests/golden_tests/cli/desugar_eta.args
 delete mode 100644 tests/golden_tests/cli/desugar_eta.hvm
 delete mode 100644 tests/golden_tests/compile_file_o_all/eta_chain.hvm
 delete mode 100644 tests/golden_tests/compile_file_o_all/unapplied_eta.hvm
 delete mode 100644 tests/snapshots/cli__desugar_eta.hvm.snap

diff --git a/Cargo.lock b/Cargo.lock
index 72e17dd85..77adc4fe8 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -409,9 +409,9 @@ checksum = "5ee073c9e4cd00e28217186dbe12796d692868f432bf2e97ee73bed0c56dfa01"
 
 [[package]]
 name = "syn"
-version = "2.0.55"
+version = "2.0.57"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "002a1b3dbf967edfafc32655d0f377ab0bb7b994aa1d32c8cc7e9b8bf3ebb8f0"
+checksum = "11a6ae1e52eb25aab8f3fb9fca13be982a373b8f1157ca14b897a825ba4a2d35"
 dependencies = [
  "proc-macro2",
  "quote",
diff --git a/src/lib.rs b/src/lib.rs
index 0766e2a46..cd5205a78 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -46,6 +46,9 @@ 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);
   }
@@ -101,9 +104,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
deleted file mode 100644
index bb7b32fc5..000000000
--- a/src/term/transform/eta_reduction.rs
+++ /dev/null
@@ -1,41 +0,0 @@
-use crate::term::*;
-
-impl Book {
-  /// Applies eta-reduction to all generated definitions, converting occurrences of `@x (f x)` into just `f`.
-  /// Assumes that variables are linear (used exactly once).
-  pub fn eta_reduction(&mut self) {
-    for def in self.defs.values_mut() {
-      def.rule_mut().body.eta_reduction();
-    }
-  }
-}
-
-impl Term {
-  /// Eta-reduces a term and any subterms.
-  /// Expects variables to be linear.
-  pub fn eta_reduction(&mut self) {
-    Term::recursive_call(move || {
-      for child in self.children_mut() {
-        child.eta_reduction()
-      }
-      match self {
-        Term::Lam {
-          tag: lam_tag,
-          nam: lam_var,
-          bod: box Term::App { tag: arg_tag, fun, arg: box Term::Var { nam: var_nam } },
-        } if lam_var == var_nam && lam_tag == arg_tag => {
-          *self = std::mem::take(fun.as_mut());
-        }
-        Term::Chn {
-          tag: chn_tag,
-          nam: chn_var,
-          bod: box Term::App { tag: arg_tag, fun, arg: box Term::Lnk { nam: var_nam } },
-        } if chn_var == var_nam && chn_tag == arg_tag => {
-          *self = std::mem::take(fun.as_mut());
-        }
-
-        _ => {}
-      }
-    })
-  }
-}
diff --git a/src/term/transform/mod.rs b/src/term/transform/mod.rs
index 5d363f373..f4737d8e9 100644
--- a/src/term/transform/mod.rs
+++ b/src/term/transform/mod.rs
@@ -5,9 +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;
 pub mod inline;
 pub mod linearize_matches;
diff --git a/tests/golden_tests/cli/desugar_eta.args b/tests/golden_tests/cli/desugar_eta.args
deleted file mode 100644
index b7547139e..000000000
--- a/tests/golden_tests/cli/desugar_eta.args
+++ /dev/null
@@ -1,3 +0,0 @@
-desugar
-tests/golden_tests/cli/desugar_eta.hvm
--Oeta
diff --git a/tests/golden_tests/cli/desugar_eta.hvm b/tests/golden_tests/cli/desugar_eta.hvm
deleted file mode 100644
index 93e6d7a1b..000000000
--- a/tests/golden_tests/cli/desugar_eta.hvm
+++ /dev/null
@@ -1,4 +0,0 @@
-id x = x
-id2 x = (id x)
-
-main = (id2 42)
diff --git a/tests/golden_tests/compile_file_o_all/eta_chain.hvm b/tests/golden_tests/compile_file_o_all/eta_chain.hvm
deleted file mode 100644
index 63f824788..000000000
--- a/tests/golden_tests/compile_file_o_all/eta_chain.hvm
+++ /dev/null
@@ -1,5 +0,0 @@
-Baz a b c = (+ a (+ b c))
-Bar a b = (Baz a b)
-Foo a = (Bar a)
-
-main = λa (Foo a)
\ No newline at end of file
diff --git a/tests/golden_tests/compile_file_o_all/unapplied_eta.hvm b/tests/golden_tests/compile_file_o_all/unapplied_eta.hvm
deleted file mode 100644
index dc663882b..000000000
--- a/tests/golden_tests/compile_file_o_all/unapplied_eta.hvm
+++ /dev/null
@@ -1,2 +0,0 @@
-Id = λa a
-main = λa (Id a)
\ No newline at end of file
diff --git a/tests/snapshots/cli__desugar_eta.hvm.snap b/tests/snapshots/cli__desugar_eta.hvm.snap
deleted file mode 100644
index f45582f9b..000000000
--- a/tests/snapshots/cli__desugar_eta.hvm.snap
+++ /dev/null
@@ -1,9 +0,0 @@
----
-source: tests/golden_tests.rs
-input_file: tests/golden_tests/cli/desugar_eta.hvm
----
-(id) = λa a
-
-(id2) = id
-
-(main) = (id2 42)
diff --git a/tests/snapshots/compile_file_o_all__ex2.hvm.snap b/tests/snapshots/compile_file_o_all__ex2.hvm.snap
index 6ad5b7910..8bf2b84bb 100644
--- 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
index 948303fb7..96614f20b 100644
--- 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
index 00e5a6845..303ce49cb 100644
--- 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)}}
 

From 3126eba2ba1b07502e24177db0f997578830f365 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Mon, 1 Apr 2024 11:20:40 -0300
Subject: [PATCH 2/2] Readd oall eta tests

---
 src/lib.rs                                               | 3 +++
 src/term/transform/mod.rs                                | 2 ++
 tests/golden_tests/compile_file_o_all/eta_chain.hvm      | 5 +++++
 tests/golden_tests/compile_file_o_all/unapplied_eta.hvm  | 2 ++
 tests/snapshots/compile_file_o_all__eta_chain.hvm.snap   | 9 ++++++++-
 .../snapshots/compile_file_o_all__unapplied_eta.hvm.snap | 3 ++-
 6 files changed, 22 insertions(+), 2 deletions(-)
 create mode 100644 tests/golden_tests/compile_file_o_all/eta_chain.hvm
 create mode 100644 tests/golden_tests/compile_file_o_all/unapplied_eta.hvm

diff --git a/src/lib.rs b/src/lib.rs
index cd5205a78..a2062c81f 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -52,6 +52,9 @@ pub fn compile_book(
   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());
   }
diff --git a/src/term/transform/mod.rs b/src/term/transform/mod.rs
index f4737d8e9..9e125e17a 100644
--- a/src/term/transform/mod.rs
+++ b/src/term/transform/mod.rs
@@ -5,6 +5,8 @@ pub mod definition_pruning;
 pub mod desugar_match_defs;
 pub mod encode_adts;
 pub mod encode_match_terms;
+pub mod fix_match_defs;
+pub mod fix_match_terms;
 pub mod float_combinators;
 pub mod inline;
 pub mod linearize_matches;
diff --git a/tests/golden_tests/compile_file_o_all/eta_chain.hvm b/tests/golden_tests/compile_file_o_all/eta_chain.hvm
new file mode 100644
index 000000000..d8cd9c0f8
--- /dev/null
+++ b/tests/golden_tests/compile_file_o_all/eta_chain.hvm
@@ -0,0 +1,5 @@
+Baz a b c = (+ a (+ b c))
+Bar a b = (Baz a b)
+Foo a = (Bar 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
new file mode 100644
index 000000000..728eb962d
--- /dev/null
+++ b/tests/golden_tests/compile_file_o_all/unapplied_eta.hvm
@@ -0,0 +1,2 @@
+Id = λa a
+main = λa (Id a)
diff --git a/tests/snapshots/compile_file_o_all__eta_chain.hvm.snap b/tests/snapshots/compile_file_o_all__eta_chain.hvm.snap
index 3ae33e837..cc403c5dc 100644
--- 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__unapplied_eta.hvm.snap b/tests/snapshots/compile_file_o_all__unapplied_eta.hvm.snap
index 6ae3dd0cc..c21b26302 100644
--- 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