From 92aa4b3d4ab5edc16ff46e0d6487a2f87250dc87 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Wed, 27 Mar 2024 11:18:37 -0300
Subject: [PATCH 01/11] Refactor float combinators to extract unsafe terms

---
 src/term/transform/float_combinators.rs       | 344 ++++++------------
 .../compile_file__redex_order.hvm.snap        |  10 +-
 ...ompile_file_o_all__adt_option_and.hvm.snap |   6 +-
 .../compile_file_o_all__and.hvm.snap          |   4 +-
 ...compile_file_o_all__black_box_ref.hvm.snap |   5 +-
 .../compile_file_o_all__ex2.hvm.snap          |   4 +-
 .../compile_file_o_all__expr.hvm.snap         |  10 +-
 ...mpile_file_o_all__list_merge_sort.hvm.snap |  28 +-
 ..._file_o_all__num_pattern_with_var.hvm.snap |   4 +-
 ...ll__recursive_combinator_inactive.hvm.snap |   4 +-
 ...le_o_all__repeated_name_trucation.hvm.snap |   4 +-
 ...e_o_all__scrutinee_reconstruction.hvm.snap |   8 +-
 .../compile_file_o_all__weekday.hvm.snap      |  12 +-
 13 files changed, 139 insertions(+), 304 deletions(-)

diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs
index 9c0cfb85..195cdc71 100644
--- a/src/term/transform/float_combinators.rs
+++ b/src/term/transform/float_combinators.rs
@@ -1,277 +1,149 @@
 use crate::term::{Book, Definition, Name, Rule, Term};
-use std::{
-  collections::{BTreeMap, BTreeSet},
-  ops::BitAnd,
-};
+use std::collections::BTreeMap;
+
+type Combinators = BTreeMap<Name, Definition>;
 
-/// Replaces closed Terms (i.e. without free variables) with a Ref to the extracted term
-/// Precondition: Vars must have been sanitized
 impl Book {
   pub fn float_combinators(&mut self) {
     let mut combinators = Combinators::new();
 
+    let slf = self.clone();
     for (def_name, def) in self.defs.iter_mut() {
+      let mut name_gen = 0;
+
       if self.entrypoint.as_ref().is_some_and(|m| m == def_name) {
         continue;
       }
 
       let builtin = def.builtin;
       let rule = def.rule_mut();
-      rule.body.float_combinators(def_name, builtin, &mut combinators);
+      rule.body.float_combinators(&mut combinators, &mut name_gen, &slf, def_name.clone(), builtin);
     }
 
-    // Definitions are not inserted to the book as they are defined to appease the borrow checker.
-    // Since we are mut borrowing the rules we can't borrow the book to insert at the same time.
     self.defs.extend(combinators);
   }
 }
 
-type Combinators = BTreeMap<Name, Definition>;
-
-#[derive(Debug)]
-struct TermInfo<'d> {
-  // Number of times a Term has been detached from the current Term
-  counter: u32,
-  def_name: Name,
-
-  builtin: bool,
-  needed_names: BTreeSet<Name>,
-  combinators: &'d mut Combinators,
-}
-
-impl<'d> TermInfo<'d> {
-  fn new(def_name: Name, builtin: bool, combinators: &'d mut Combinators) -> Self {
-    Self { counter: 0, def_name, builtin, needed_names: BTreeSet::new(), combinators }
-  }
-  fn request_name(&mut self, name: &Name) {
-    self.needed_names.insert(name.clone());
-  }
-
-  fn provide(&mut self, name: Option<&Name>) {
-    if let Some(name) = name {
-      self.needed_names.remove(name);
-    }
-  }
-
-  fn has_no_free_vars(&self) -> bool {
-    self.needed_names.is_empty()
-  }
-
-  fn replace_scope(&mut self, new_scope: BTreeSet<Name>) -> BTreeSet<Name> {
-    std::mem::replace(&mut self.needed_names, new_scope)
-  }
-
-  fn merge_scope(&mut self, target: BTreeSet<Name>) {
-    self.needed_names.extend(target);
-  }
-
-  fn detach_term(&mut self, term: &mut Term) {
-    let comb_name = Name::new(format!("{}$C{}", self.def_name, self.counter));
-    self.counter += 1;
-
-    let comb_var = Term::Ref { nam: comb_name.clone() };
-    let extracted_term = std::mem::replace(term, comb_var);
-
-    let rules = vec![Rule { body: extracted_term, pats: Vec::new() }];
-    let rule = Definition { name: comb_name.clone(), rules, builtin: self.builtin };
-    self.combinators.insert(comb_name, rule);
-  }
-}
-
-#[derive(Debug)]
-enum Detach {
-  /// Can be detached freely
-  Combinator,
-  /// Can not be detached
-  Unscoped { lams: BTreeSet<Name>, vars: BTreeSet<Name> },
-  /// Should be detached to make the program not hang
-  Recursive,
-}
-
-impl Detach {
-  fn can_detach(&self) -> bool {
-    !matches!(self, Detach::Unscoped { .. })
-  }
-
-  fn unscoped_lam(nam: Name) -> Self {
-    Detach::Unscoped { lams: [nam].into(), vars: Default::default() }
-  }
-
-  fn unscoped_var(nam: Name) -> Self {
-    Detach::Unscoped { lams: Default::default(), vars: [nam].into() }
-  }
-}
-
-impl BitAnd for Detach {
-  type Output = Detach;
-
-  fn bitand(self, rhs: Self) -> Self::Output {
-    match (self, rhs) {
-      (Detach::Combinator, Detach::Combinator) => Detach::Combinator,
-
-      (Detach::Combinator, unscoped @ Detach::Unscoped { .. }) => unscoped,
-      (unscoped @ Detach::Unscoped { .. }, Detach::Combinator) => unscoped,
-
-      // Merge two unscoped terms into one, removing entries of each matching `Lam` and `Var`.
-      // If all unscoped pairs are found and removed this way, the term can be treated as a Combinator.
-      (Detach::Unscoped { mut lams, mut vars }, Detach::Unscoped { lams: rhs_lams, vars: rhs_vars }) => {
-        lams.extend(rhs_lams);
-        vars.extend(rhs_vars);
-
-        let res_lams: BTreeSet<_> = lams.difference(&vars).cloned().collect();
-        let res_vars: BTreeSet<_> = vars.difference(&lams).cloned().collect();
-
-        if res_lams.is_empty() && res_vars.is_empty() {
-          Detach::Combinator
-        } else {
-          Detach::Unscoped { lams: res_lams, vars: res_vars }
-        }
-      }
-
-      (Detach::Combinator, Detach::Recursive) => Detach::Recursive,
-      (Detach::Recursive, Detach::Combinator) => Detach::Recursive,
-      (Detach::Recursive, Detach::Recursive) => Detach::Recursive,
-
-      // TODO: Is this the best way to best deal with a term that is both unscoped and recursive?
-      (unscoped @ Detach::Unscoped { .. }, Detach::Recursive) => unscoped,
-      (Detach::Recursive, unscoped @ Detach::Unscoped { .. }) => unscoped,
-    }
-  }
-}
-
 impl Term {
-  pub fn float_combinators(&mut self, def_name: &Name, builtin: bool, combinators: &mut Combinators) {
-    self.go_float(0, &mut TermInfo::new(def_name.clone(), builtin, combinators));
-  }
-
-  fn go_float(&mut self, depth: usize, term_info: &mut TermInfo) -> Detach {
-    Term::recursive_call(move || match self {
-      Term::Lam { .. } | Term::Chn { .. } if self.is_id() => Detach::Combinator,
-
-      Term::Lam { .. } => self.float_lam(depth, term_info),
-      Term::Chn { .. } => self.float_lam(depth, term_info),
-      Term::App { .. } => self.float_app(depth, term_info),
-      Term::Mat { .. } => self.float_mat(depth, term_info),
-
-      Term::Var { nam } => {
-        term_info.request_name(nam);
-        Detach::Combinator
-      }
-
-      Term::Lnk { nam } => Detach::unscoped_var(nam.clone()),
-
-      Term::Ref { nam: def_name } if def_name == &term_info.def_name => Detach::Recursive,
-
-      _ => {
-        let mut detach = Detach::Combinator;
-        for (child, binds) in self.children_mut_with_binds() {
-          detach = detach & child.go_float(depth + 1, term_info);
-          for bind in binds {
-            term_info.provide(bind.as_ref());
-          }
+  fn float_combinators(
+    &mut self,
+    combinators: &mut Combinators,
+    name_gen: &mut usize,
+    book: &Book,
+    def_name: Name,
+    builtin: bool,
+  ) {
+    Term::recursive_call(move || {
+      for term in self.children_mut() {
+        if term.is_constant() || term.is_safe(book) || term.has_unscoped_diff() {
+          continue;
+        }
+
+        term.float_combinators(combinators, name_gen, book, def_name.clone(), builtin);
+
+        match term {
+          Term::App { .. } => {
+            if term.free_vars().is_empty() && !term.has_unscoped_diff() {
+              float_combinator(&def_name, name_gen, term, builtin, combinators);
+            }
+          }
+
+          Term::Sup { els, .. } => els
+            .iter_mut()
+            .for_each(|e| e.float_combinators(combinators, name_gen, book, def_name.clone(), builtin)),
+
+          term if term.is_combinator() => float_combinator(&def_name, name_gen, term, builtin, combinators),
+
+          _ => term.float_combinators(combinators, name_gen, book, def_name.clone(), builtin),
         }
-        detach
       }
     })
   }
+}
 
-  fn float_lam(&mut self, depth: usize, term_info: &mut TermInfo) -> Detach {
-    let (nam, bod, unscoped): (Option<&Name>, &mut Term, bool) = match self {
-      Term::Lam { nam, bod, .. } => (nam.as_ref(), bod, false),
-      Term::Chn { nam, bod, .. } => (nam.as_ref(), bod, true),
-      _ => unreachable!(),
-    };
+fn float_combinator(
+  def_name: &Name,
+  name_gen: &mut usize,
+  term: &mut Term,
+  builtin: bool,
+  combinators: &mut BTreeMap<Name, Definition>,
+) {
+  let comb_name = Name::new(format!("{}$C{}", def_name, *name_gen));
+  *name_gen += 1;
 
-    let parent_scope = term_info.replace_scope(BTreeSet::new());
+  let comb_var = Term::Ref { nam: comb_name.clone() };
+  let extracted_term = std::mem::replace(term, comb_var);
 
-    let mut detach = bod.go_float(depth + 1, term_info);
+  let rules = vec![Rule { body: extracted_term, pats: Vec::new() }];
+  let rule = Definition { name: comb_name.clone(), rules, builtin };
+  combinators.insert(comb_name, rule);
+}
 
-    if unscoped {
-      detach = detach & Detach::unscoped_lam(nam.cloned().unwrap());
-    } else {
-      term_info.provide(nam);
-    }
+impl Term {
+  pub fn is_safe(&self, book: &Book) -> bool {
+    Term::recursive_call(move || match self {
+      // A number or an eraser is safe.
+      Term::Num { .. } | Term::Era => true,
 
-    if depth != 0 && detach.can_detach() && term_info.has_no_free_vars() {
-      term_info.detach_term(self);
-    }
+      // A tuple or superposition with only constant elements is safe.
+      Term::Tup { els } | Term::Sup { els, .. } => els.iter().all(Term::is_constant),
 
-    term_info.merge_scope(parent_scope);
+      // A constant lambda sequence is safe.
+      Term::Lam { bod: box Term::Var { .. }, .. } => self.is_constant_lambda(),
 
-    detach
-  }
+      // A lambda with a safe body is safe.
+      Term::Lam { bod, .. } => bod.is_safe(book),
 
-  fn float_app(&mut self, depth: usize, term_info: &mut TermInfo) -> Detach {
-    let Term::App { fun, arg, .. } = self else { unreachable!() };
-
-    let parent_scope = term_info.replace_scope(BTreeSet::new());
-
-    let fun_detach = fun.go_float(depth + 1, term_info);
-    let fun_scope = term_info.replace_scope(BTreeSet::new());
-
-    let arg_detach = arg.go_float(depth + 1, term_info);
-    let arg_scope = term_info.replace_scope(parent_scope);
-
-    let detach = match fun_detach {
-      // If the fun scope is not empty, we know the recursive ref is not in a active position,
-      // Because if it was an application, it would be already extracted
-      //
-      // e.g.: {recursive_ref some_var}
-      Detach::Recursive if !fun_scope.is_empty() => arg_detach,
-
-      Detach::Recursive if arg_scope.is_empty() && arg_detach.can_detach() => {
-        term_info.detach_term(self);
-        Detach::Combinator
+      // A ref to a function with a safe body is safe if the function is in the book and its body is safe.
+      Term::Ref { nam } => {
+        if let Some(definition) = book.defs.get(nam) {
+          definition.rule().body.is_safe(book)
+        } else {
+          false
+        }
       }
 
-      // If the only term that is possible to detach is just a Term::Ref,
-      // there is no benefit to it, so that case is skipped
-      Detach::Recursive if !matches!(fun, box Term::Ref { .. }) => {
-        term_info.detach_term(fun);
-        arg_detach
-      }
-
-      _ => fun_detach & arg_detach,
-    };
-
-    term_info.merge_scope(fun_scope);
-    term_info.merge_scope(arg_scope);
-
-    detach
+      // TODO?: Any term that, when fully expanded, becomes a supercombinator is safe.
+      // _ => self.is_supercombinator(),
+      _ => false,
+    })
   }
 
-  fn float_mat(&mut self, depth: usize, term_info: &mut TermInfo) -> Detach {
-    let Term::Mat { args, rules } = self else { unreachable!() };
-
-    let mut detach = Detach::Combinator;
-    for arg in args {
-      detach = detach & arg.go_float(depth + 1, term_info);
-    }
-    let parent_scope = term_info.replace_scope(BTreeSet::new());
-
-    for rule in rules.iter_mut() {
-      for pat in &rule.pats {
-        debug_assert!(pat.is_native_num_match());
-      }
-
-      let arm_detach = match rule.body.go_float(depth + 1, term_info) {
-        // If the recursive ref reached here, it is not in a active position
-        Detach::Recursive => Detach::Combinator,
-        detach => detach,
-      };
-
-      detach = detach & arm_detach;
-    }
-
-    term_info.merge_scope(parent_scope);
-    detach
-  }
-
-  // We don't want to detach id function, since that's not a net gain in performance or space
-  fn is_id(&self) -> bool {
+  pub fn is_constant(&self) -> bool {
     match self {
-      Term::Lam { nam: Some(lam_nam), bod: box Term::Var { nam: var_nam }, .. } => lam_nam == var_nam,
+      Term::Num { .. } => true,
+      Term::Era => true,
+      Term::Tup { els } | Term::Sup { els, .. } => els.iter().all(Term::is_constant),
+      Term::Lam { .. } => self.is_constant_lambda(),
       _ => false,
     }
   }
+
+  /// Checks if the term is a lambda sequence with the body being a variable in the scope or a reference.
+  fn is_constant_lambda(&self) -> bool {
+    let mut current = self;
+    let mut scope = Vec::new();
+
+    while let Term::Lam { nam, bod, .. } = current {
+      if let Some(nam) = nam {
+        scope.push(nam);
+      }
+      current = bod;
+    }
+
+    match current {
+      Term::Var { nam } if scope.contains(&nam) => true,
+      Term::Ref { .. } => true,
+      other => other.is_constant(),
+    }
+  }
+
+  fn is_combinator(&self) -> bool {
+    matches!(self, Term::Lam { .. } if self.free_vars().is_empty())
+  }
+
+  fn has_unscoped_diff(&self) -> bool {
+    let (declared, used) = self.unscoped_vars();
+    declared.difference(&used).count() != 0
+  }
 }
diff --git a/tests/snapshots/compile_file__redex_order.hvm.snap b/tests/snapshots/compile_file__redex_order.hvm.snap
index ce82b4cb..2f393c36 100644
--- a/tests/snapshots/compile_file__redex_order.hvm.snap
+++ b/tests/snapshots/compile_file__redex_order.hvm.snap
@@ -14,9 +14,13 @@ input_file: tests/golden_tests/compile_file/redex_order.hvm
   & @c ~ (a d)
 
 @foo2 = a
-  & @a ~ (b a)
-  & @b ~ (c b)
-  & @c ~ (#0 c)
+  & @a ~ (@foo2$C1 a)
+
+@foo2$C0 = a
+  & @c ~ (#0 a)
+
+@foo2$C1 = a
+  & @b ~ (@foo2$C0 a)
 
 @main = a
   & @foo ~ (@foo2 a)
diff --git a/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap b/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap
index e9703407..66c2ef0c 100644
--- a/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__adt_option_and.hvm.snap
@@ -4,13 +4,11 @@ input_file: tests/golden_tests/compile_file_o_all/adt_option_and.hvm
 ---
 @None = {2 * {2 a a}}
 
-@Option.and = ({2 @Option.and$C2 {2 @Option.and$C1_$_Option.and$C3 a}} a)
+@Option.and = ({2 @Option.and$C1 {2 (* @None) a}} a)
 
 @Option.and$C0 = {2 a (b {2 {2 [b a] c} {2 * c}})}
 
-@Option.and$C1_$_Option.and$C3 = (* @None)
-
-@Option.and$C2 = {2 a ({2 @Option.and$C0 {2 @Option.and$C1_$_Option.and$C3 (a b)}} b)}
+@Option.and$C1 = {2 a ({2 @Option.and$C0 {2 (* @None) (a b)}} b)}
 
 @Some = (a {2 {2 a b} {2 * b}})
 
diff --git a/tests/snapshots/compile_file_o_all__and.hvm.snap b/tests/snapshots/compile_file_o_all__and.hvm.snap
index 580ab4e1..7a8f1147 100644
--- a/tests/snapshots/compile_file_o_all__and.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__and.hvm.snap
@@ -2,9 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/and.hvm
 ---
-@and = (a ({2 (b b) {2 @and$C0 (a c)}} c))
-
-@and$C0 = (* @false)
+@and = (a ({2 (b b) {2 (* @false) (a c)}} c))
 
 @false = {2 * {2 a a}}
 
diff --git a/tests/snapshots/compile_file_o_all__black_box_ref.hvm.snap b/tests/snapshots/compile_file_o_all__black_box_ref.hvm.snap
index 65f8c5b3..afbbc9ed 100644
--- a/tests/snapshots/compile_file_o_all__black_box_ref.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__black_box_ref.hvm.snap
@@ -2,5 +2,8 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/black_box_ref.hvm
 ---
+@def_that_uses_black_box$C0 = a
+  & @HVM.black_box ~ (#6 a)
+
 @main = a
-  & @HVM.black_box ~ (#6 <* #7 a>)
+  & @def_that_uses_black_box$C0 ~ <* #7 a>
diff --git a/tests/snapshots/compile_file_o_all__ex2.hvm.snap b/tests/snapshots/compile_file_o_all__ex2.hvm.snap
index e4a0baa4..6ad5b791 100644
--- a/tests/snapshots/compile_file_o_all__ex2.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__ex2.hvm.snap
@@ -2,9 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/ex2.hvm
 ---
-@E = (* @E$C0)
-
-@E$C0 = (* (a a))
+@E = (* (* (a a)))
 
 @I = (a (* ((a b) (* b))))
 
diff --git a/tests/snapshots/compile_file_o_all__expr.hvm.snap b/tests/snapshots/compile_file_o_all__expr.hvm.snap
index 6c0623ee..e9cb0e70 100644
--- a/tests/snapshots/compile_file_o_all__expr.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__expr.hvm.snap
@@ -8,19 +8,13 @@ input_file: tests/golden_tests/compile_file_o_all/expr.hvm
 
 @Let = (a (b (c {2 * {2 * {2 * {2 * {2 * {2 {2 a {2 b {2 c d}}} {2 * {2 * {2 * d}}}}}}}}})))
 
-@Mul = {4 * @Mul$C1}
-
-@Mul$C0 = {4 a {4 * a}}
-
-@Mul$C1 = {4 * @Mul$C0}
+@Mul = {4 * {4 * {4 a {4 * a}}}}
 
 @Num = (a {2 * {2 {2 a b} {2 * {2 * {2 * {2 * {2 * {2 * {2 * b}}}}}}}}})
 
 @Op2 = (a (b (c {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 {2 a {2 b {2 c d}}} d}}}}}}}}})))
 
-@Sub = {4 * @Sub$C0}
-
-@Sub$C0 = {4 a {4 * {4 * a}}}
+@Sub = {4 * {4 a {4 * {4 * a}}}}
 
 @Var = (a {2 {2 a b} {2 * {2 * {2 * {2 * {2 * {2 * {2 * {2 * b}}}}}}}}})
 
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 80fa2b09..e453ba2c 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
@@ -4,25 +4,15 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
 ---
 @Cons = (a (b {4 {4 a {4 b c}} {4 * c}}))
 
-@If$C0 = (a (* a))
+@Map = ({4 @Map$C0 {4 (* @Nil) a}} a)
 
-@If$C1 = (* (a a))
+@Map$C0 = {4 a {4 {4 @Map$C0 {4 (* @Nil) (b c)}} ({3 (a d) b} {4 {4 d {4 c e}} {4 * e}})}}
 
-@Map = ({4 @Map$C0 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 a}} a)
+@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)))}}
 
-@Map$C0 = {4 a {4 {4 @Map$C0 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 (b c)}} ({3 (a d) b} {4 {4 d {4 c e}} {4 * e}})}}
+@Merge$C1 = {4 a {4 b (c ({4 @Merge$C0 {4 (* @Cons) (c (a (b d)))}} d))}}
 
-@Map$C1_$_MergePair$C4_$_Unpack$C3 = (* @Nil)
-
-@Merge$C0 = {4 {5 a {5 b c}} {4 {7 d {4 @Merge$C0 {4 @Merge$C1 (e (f (g h)))}}} ({9 (i (a {2 @If$C0 {2 @If$C1 ({4 {4 j {4 k l}} {4 * l}} ({4 {4 c {4 h m}} {4 * m}} n))}})) {9 o e}} ({11 i {11 j f}} ({13 {4 @Merge$C2 {4 @Merge$C3 (o ({4 {4 b {4 d p}} {4 * p}} k))}} g} n)))}}
-
-@Merge$C1 = (* @Cons)
-
-@Merge$C2 = {4 a {4 b (c ({4 @Merge$C0 {4 @Merge$C1 (c (a (b d)))}} d))}}
-
-@Merge$C3 = (* (a a))
-
-@MergePair$C0 = {4 a {4 {4 @MergePair$C3 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 (b c)}} ({15 d b} ({4 @Merge$C2 {4 @Merge$C3 (d (a e))}} {4 {4 e {4 c f}} {4 * f}}))}}
+@MergePair$C0 = {4 a {4 {4 @MergePair$C3 {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 = (a {4 {4 a {4 @Nil b}} {4 * b}})
 
@@ -34,13 +24,11 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
 
 @Pure = (a {4 {4 a {4 @Nil b}} {4 * b}})
 
-@Unpack = (a ({4 @Unpack$C2 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 (a b)}} b))
+@Unpack = (a ({4 @Unpack$C1 {4 (* @Nil) (a b)}} b))
 
-@Unpack$C0 = {4 a {4 {4 @MergePair$C3 {4 @Map$C1_$_MergePair$C4_$_Unpack$C3 (b {4 @Unpack$C0 {4 @Unpack$C1 (c (d e))}})}} ({17 c {15 f b}} ({4 @Merge$C2 {4 @Merge$C3 (f (a d))}} e))}}
+@Unpack$C0 = {4 a {4 {4 @MergePair$C3 {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$C1 = (* (a a))
-
-@Unpack$C2 = {4 a {4 {4 @Unpack$C0 {4 @Unpack$C1 (b (a c))}} (b c)}}
+@Unpack$C1 = {4 a {4 {4 @Unpack$C0 {4 (* (b b)) (c (a d))}} (c d)}}
 
 @main = (a (b c))
   & @Unpack ~ (a (d c))
diff --git a/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap b/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap
index 4ed72aa2..1acbbb86 100644
--- a/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__num_pattern_with_var.hvm.snap
@@ -2,9 +2,9 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/num_pattern_with_var.hvm
 ---
-@Foo = ({2 (* #0) {2 @Foo$C1 a}} a)
+@Foo = ({2 (* #0) {2 @Foo$C0 a}} a)
 
-@Foo$C1 = (?<#0 (a a) b> b)
+@Foo$C0 = (?<#0 (a a) b> b)
 
 @main = a
   & @Foo ~ (@true (#3 a))
diff --git a/tests/snapshots/compile_file_o_all__recursive_combinator_inactive.hvm.snap b/tests/snapshots/compile_file_o_all__recursive_combinator_inactive.hvm.snap
index 21f2c33c..2cf847f3 100644
--- a/tests/snapshots/compile_file_o_all__recursive_combinator_inactive.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__recursive_combinator_inactive.hvm.snap
@@ -2,9 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/recursive_combinator_inactive.hvm
 ---
-@Foo = (?<{3 @Foo @Foo} @Foo$C0 a> a)
-
-@Foo$C0 = (a (* a))
+@Foo = (?<{3 @Foo @Foo} (a (* a)) b> b)
 
 @main = a
   & @Foo ~ (#0 a)
diff --git a/tests/snapshots/compile_file_o_all__repeated_name_trucation.hvm.snap b/tests/snapshots/compile_file_o_all__repeated_name_trucation.hvm.snap
index 7e52424c..ecf60eb0 100644
--- a/tests/snapshots/compile_file_o_all__repeated_name_trucation.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__repeated_name_trucation.hvm.snap
@@ -28,9 +28,7 @@ For let expressions where the variable is non-linear (used more than once), you
 See here for more info: https://github.com/HigherOrderCO/hvm-lang/blob/main/docs/lazy-definitions.md.
 
 
-@long_name_that_truncates = (* @long_name_that_truncates$C0)
-
-@long_name_that_truncates$C0 = (* @long_name_that_truncates)
+@long_name_that_truncates = (* (* @long_name_that_truncates))
 
 @main = a
   & @long_name_that_truncates ~ ((b b) a)
diff --git a/tests/snapshots/compile_file_o_all__scrutinee_reconstruction.hvm.snap b/tests/snapshots/compile_file_o_all__scrutinee_reconstruction.hvm.snap
index 683416cc..503904de 100644
--- a/tests/snapshots/compile_file_o_all__scrutinee_reconstruction.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__scrutinee_reconstruction.hvm.snap
@@ -4,13 +4,7 @@ input_file: tests/golden_tests/compile_file_o_all/scrutinee_reconstruction.hvm
 ---
 @None = {2 * {2 a a}}
 
-@Option.or = ({3 {2 @Option.or$C1 {2 @Option.or$C2 (a b)}} a} b)
-
-@Option.or$C0 = (a (* a))
-
-@Option.or$C1 = {2 * @Option.or$C0}
-
-@Option.or$C2 = (* (a a))
+@Option.or = ({3 {2 {2 * (a (* a))} {2 (* (b b)) (c d)}} c} d)
 
 @Some = (a {2 {2 a b} {2 * b}})
 
diff --git a/tests/snapshots/compile_file_o_all__weekday.hvm.snap b/tests/snapshots/compile_file_o_all__weekday.hvm.snap
index a141dfab..ea12e94c 100644
--- a/tests/snapshots/compile_file_o_all__weekday.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__weekday.hvm.snap
@@ -2,17 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/weekday.hvm
 ---
-@Saturday = {2 * @Saturday$C4}
-
-@Saturday$C0 = {2 a {2 * a}}
-
-@Saturday$C1 = {2 * @Saturday$C0}
-
-@Saturday$C2 = {2 * @Saturday$C1}
-
-@Saturday$C3 = {2 * @Saturday$C2}
-
-@Saturday$C4 = {2 * @Saturday$C3}
+@Saturday = {2 * {2 * {2 * {2 * {2 * {2 a {2 * a}}}}}}}
 
 @main = a
   & (b b) ~ (@Saturday a)

From b4a79fee1b705921937f58dfe557e3ae409ff6d1 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Wed, 27 Mar 2024 11:22:12 -0300
Subject: [PATCH 02/11] Add deref loop test and remove unnecessary clone

---
 src/term/transform/float_combinators.rs        | 18 +++++++++---------
 tests/golden_tests/desugar_file/deref_loop.hvm | 10 ++++++++++
 .../desugar_file__deref_loop.hvm.snap          | 15 +++++++++++++++
 3 files changed, 34 insertions(+), 9 deletions(-)
 create mode 100644 tests/golden_tests/desugar_file/deref_loop.hvm
 create mode 100644 tests/snapshots/desugar_file__deref_loop.hvm.snap

diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs
index 195cdc71..06ca1f6b 100644
--- a/src/term/transform/float_combinators.rs
+++ b/src/term/transform/float_combinators.rs
@@ -17,7 +17,7 @@ impl Book {
 
       let builtin = def.builtin;
       let rule = def.rule_mut();
-      rule.body.float_combinators(&mut combinators, &mut name_gen, &slf, def_name.clone(), builtin);
+      rule.body.float_combinators(&mut combinators, &mut name_gen, &slf, def_name, builtin);
     }
 
     self.defs.extend(combinators);
@@ -30,7 +30,7 @@ impl Term {
     combinators: &mut Combinators,
     name_gen: &mut usize,
     book: &Book,
-    def_name: Name,
+    def_name: &Name,
     builtin: bool,
   ) {
     Term::recursive_call(move || {
@@ -39,22 +39,22 @@ impl Term {
           continue;
         }
 
-        term.float_combinators(combinators, name_gen, book, def_name.clone(), builtin);
+        term.float_combinators(combinators, name_gen, book, def_name, builtin);
 
         match term {
           Term::App { .. } => {
             if term.free_vars().is_empty() && !term.has_unscoped_diff() {
-              float_combinator(&def_name, name_gen, term, builtin, combinators);
+              float_combinator(def_name, name_gen, term, builtin, combinators);
             }
           }
 
-          Term::Sup { els, .. } => els
-            .iter_mut()
-            .for_each(|e| e.float_combinators(combinators, name_gen, book, def_name.clone(), builtin)),
+          Term::Sup { els, .. } => {
+            els.iter_mut().for_each(|e| e.float_combinators(combinators, name_gen, book, def_name, builtin))
+          }
 
-          term if term.is_combinator() => float_combinator(&def_name, name_gen, term, builtin, combinators),
+          term if term.is_combinator() => float_combinator(def_name, name_gen, term, builtin, combinators),
 
-          _ => term.float_combinators(combinators, name_gen, book, def_name.clone(), builtin),
+          _ => term.float_combinators(combinators, name_gen, book, def_name, builtin),
         }
       }
     })
diff --git a/tests/golden_tests/desugar_file/deref_loop.hvm b/tests/golden_tests/desugar_file/deref_loop.hvm
new file mode 100644
index 00000000..3e08367b
--- /dev/null
+++ b/tests/golden_tests/desugar_file/deref_loop.hvm
@@ -0,0 +1,10 @@
+data nat = (succ pred) | zero
+
+foo = @x match x {
+  succ: x.pred
+  zero: (bar 0)
+}
+
+bar = (foo 1)
+
+main = (foo 0)
diff --git a/tests/snapshots/desugar_file__deref_loop.hvm.snap b/tests/snapshots/desugar_file__deref_loop.hvm.snap
new file mode 100644
index 00000000..1d5b81f3
--- /dev/null
+++ b/tests/snapshots/desugar_file__deref_loop.hvm.snap
@@ -0,0 +1,15 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/desugar_file/deref_loop.hvm
+---
+(foo) = λa #nat (a #nat λb b foo$C0)
+
+(bar) = (foo 1)
+
+(main) = (foo 0)
+
+(succ) = λa #nat λb #nat λ* #nat (b a)
+
+(zero) = #nat λ* #nat λb b
+
+(foo$C0) = (bar 0)

From bcbcdc5442ca8b14bab581bf55416e5a32afd713 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Wed, 27 Mar 2024 15:51:59 -0300
Subject: [PATCH 03/11] Refactor float combinators and add combinators test

---
 src/term/transform/float_combinators.rs       | 82 +++++++++++--------
 tests/golden_tests.rs                         |  3 +-
 .../golden_tests/desugar_file/combinators.hvm | 17 ++++
 3 files changed, 65 insertions(+), 37 deletions(-)
 create mode 100644 tests/golden_tests/desugar_file/combinators.hvm

diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs
index 06ca1f6b..bcd8f82c 100644
--- a/src/term/transform/float_combinators.rs
+++ b/src/term/transform/float_combinators.rs
@@ -1,11 +1,24 @@
+use indexmap::IndexSet;
+
 use crate::term::{Book, Definition, Name, Rule, Term};
 use std::collections::BTreeMap;
 
 type Combinators = BTreeMap<Name, Definition>;
 
 impl Book {
+  /// Extracts unsafe terms into new definitions.
+  ///
+  /// Precondition: Variables must have been sanitized.
+  ///
+  /// The term is floated if it:
+  /// - Is an Application without free variables.
+  /// - Is a Superposition.
+  /// - Is a combinator.
+  /// The term is not floated if it:
+  /// - Is safe or has unscoped variables.
   pub fn float_combinators(&mut self) {
     let mut combinators = Combinators::new();
+    let mut safe_defs = IndexSet::new();
 
     let slf = self.clone();
     for (def_name, def) in self.defs.iter_mut() {
@@ -17,7 +30,7 @@ impl Book {
 
       let builtin = def.builtin;
       let rule = def.rule_mut();
-      rule.body.float_combinators(&mut combinators, &mut name_gen, &slf, def_name, builtin);
+      rule.body.float_combinators(&mut combinators, &mut name_gen, &slf, def_name, builtin, &mut safe_defs);
     }
 
     self.defs.extend(combinators);
@@ -32,35 +45,42 @@ impl Term {
     book: &Book,
     def_name: &Name,
     builtin: bool,
+    safe_defs: &mut IndexSet<Name>,
   ) {
     Term::recursive_call(move || {
       for term in self.children_mut() {
-        if term.is_constant() || term.is_safe(book) || term.has_unscoped_diff() {
+        // Don't float if it's safe or has unscoped variables.
+        if term.is_safe(book, safe_defs) || term.has_unscoped_diff() {
           continue;
         }
 
-        term.float_combinators(combinators, name_gen, book, def_name, builtin);
+        // Recusively float the children terms.
+        term.float_combinators(combinators, name_gen, book, def_name, builtin, safe_defs);
 
         match term {
+          // If it is an Application without free variables like '(bar 0)', float into a new definition.
           Term::App { .. } => {
             if term.free_vars().is_empty() && !term.has_unscoped_diff() {
               float_combinator(def_name, name_gen, term, builtin, combinators);
             }
           }
 
-          Term::Sup { els, .. } => {
-            els.iter_mut().for_each(|e| e.float_combinators(combinators, name_gen, book, def_name, builtin))
-          }
+          // If it is a Superposition, float every child element.
+          Term::Sup { els, .. } => els
+            .iter_mut()
+            .for_each(|e| e.float_combinators(combinators, name_gen, book, def_name, builtin, safe_defs)),
 
+          // If it is a combinator, float into a new definition.
           term if term.is_combinator() => float_combinator(def_name, name_gen, term, builtin, combinators),
 
-          _ => term.float_combinators(combinators, name_gen, book, def_name, builtin),
+          _ => continue,
         }
       }
     })
   }
 }
 
+/// Inserts a new definition for the given term in the combinators map.
 fn float_combinator(
   def_name: &Name,
   name_gen: &mut usize,
@@ -80,27 +100,26 @@ fn float_combinator(
 }
 
 impl Term {
-  pub fn is_safe(&self, book: &Book) -> bool {
+  /// A term can be considered safe if it is:
+  /// - A Number or an Eraser.
+  /// - A Tuple or Superposition where all elements are constants.
+  /// - A constant Lambda, e.g a nullary constructor.
+  /// - A Reference with safe body.
+  pub fn is_safe(&self, book: &Book, safe_defs: &mut IndexSet<Name>) -> bool {
     Term::recursive_call(move || match self {
-      // A number or an eraser is safe.
       Term::Num { .. } | Term::Era => true,
 
-      // A tuple or superposition with only constant elements is safe.
-      Term::Tup { els } | Term::Sup { els, .. } => els.iter().all(Term::is_constant),
+      Term::Tup { els } | Term::Sup { els, .. } => els.iter().all(|e| Term::is_safe(e, book, safe_defs)),
 
-      // A constant lambda sequence is safe.
-      Term::Lam { bod: box Term::Var { .. }, .. } => self.is_constant_lambda(),
+      Term::Lam { .. } => self.is_constant_lambda(book, safe_defs),
 
-      // A lambda with a safe body is safe.
-      Term::Lam { bod, .. } => bod.is_safe(book),
-
-      // A ref to a function with a safe body is safe if the function is in the book and its body is safe.
       Term::Ref { nam } => {
-        if let Some(definition) = book.defs.get(nam) {
-          definition.rule().body.is_safe(book)
-        } else {
-          false
-        }
+        !safe_defs.insert(nam.clone())
+          || if let Some(definition) = book.defs.get(nam) {
+            definition.rule().body.is_safe(book, safe_defs)
+          } else {
+            false
+          }
       }
 
       // TODO?: Any term that, when fully expanded, becomes a supercombinator is safe.
@@ -109,18 +128,8 @@ impl Term {
     })
   }
 
-  pub fn is_constant(&self) -> bool {
-    match self {
-      Term::Num { .. } => true,
-      Term::Era => true,
-      Term::Tup { els } | Term::Sup { els, .. } => els.iter().all(Term::is_constant),
-      Term::Lam { .. } => self.is_constant_lambda(),
-      _ => false,
-    }
-  }
-
   /// Checks if the term is a lambda sequence with the body being a variable in the scope or a reference.
-  fn is_constant_lambda(&self) -> bool {
+  fn is_constant_lambda(&self, book: &Book, safe_defs: &mut IndexSet<Name>) -> bool {
     let mut current = self;
     let mut scope = Vec::new();
 
@@ -134,15 +143,16 @@ impl Term {
     match current {
       Term::Var { nam } if scope.contains(&nam) => true,
       Term::Ref { .. } => true,
-      other => other.is_constant(),
+      term => term.is_safe(book, safe_defs),
     }
   }
 
-  fn is_combinator(&self) -> bool {
+  /// A term is a combinator if it is a lambda abstraction without free variables.
+  pub fn is_combinator(&self) -> bool {
     matches!(self, Term::Lam { .. } if self.free_vars().is_empty())
   }
 
-  fn has_unscoped_diff(&self) -> bool {
+  pub fn has_unscoped_diff(&self) -> bool {
     let (declared, used) = self.unscoped_vars();
     declared.difference(&used).count() != 0
   }
diff --git a/tests/golden_tests.rs b/tests/golden_tests.rs
index 09609cc7..df4ea2ca 100644
--- a/tests/golden_tests.rs
+++ b/tests/golden_tests.rs
@@ -276,7 +276,8 @@ fn encode_pattern_match() {
 #[test]
 fn desugar_file() {
   run_golden_test_dir(function_name!(), &|code, path| {
-    let diagnostics_cfg = DiagnosticsConfig::new(Severity::Error, true);
+    let mut diagnostics_cfg = DiagnosticsConfig::new(Severity::Error, true);
+    diagnostics_cfg.unused_definition = Severity::Allow;
     let mut book = do_parse_book(code, path)?;
     desugar_book(&mut book, CompileOpts::light(), diagnostics_cfg, None)?;
     Ok(book.to_string())
diff --git a/tests/golden_tests/desugar_file/combinators.hvm b/tests/golden_tests/desugar_file/combinators.hvm
new file mode 100644
index 00000000..50f80b58
--- /dev/null
+++ b/tests/golden_tests/desugar_file/combinators.hvm
@@ -0,0 +1,17 @@
+(foo) = λa λb λc (foo a)
+
+(bar) = λa λb (a bar b)
+
+(List.ignore list ignore) =
+  match list {
+    (List.cons): (List.ignore list.tail (List.ignore))
+    (List.nil): 0
+  }
+
+(baz) = {0 1 2 3 λa a foo}
+
+(qux) = {0 qux}
+
+(list) = [0 list]
+
+(Main) = list

From ec24ae2a80ffe1bdfeb516898d2482e5d6594df8 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Wed, 27 Mar 2024 16:41:30 -0300
Subject: [PATCH 04/11] Update float combinators doc and combinators test

---
 cspell.json                                   |  2 +
 src/term/transform/float_combinators.rs       | 55 ++++++++++---------
 .../golden_tests/desugar_file/combinators.hvm |  4 ++
 .../desugar_file__combinators.hvm.snap        | 35 ++++++++++++
 4 files changed, 69 insertions(+), 27 deletions(-)
 create mode 100644 tests/snapshots/desugar_file__combinators.hvm.snap

diff --git a/cspell.json b/cspell.json
index 3ee82f47..42bdc6ae 100644
--- a/cspell.json
+++ b/cspell.json
@@ -45,6 +45,7 @@
     "namegen",
     "nams",
     "nats",
+    "nullary",
     "numop",
     "nums",
     "oper",
@@ -54,6 +55,7 @@
     "peekable",
     "postcondition",
     "readback",
+    "recursively",
     "redex",
     "redexes",
     "resugar",
diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs
index bcd8f82c..33f17900 100644
--- a/src/term/transform/float_combinators.rs
+++ b/src/term/transform/float_combinators.rs
@@ -10,15 +10,13 @@ impl Book {
   ///
   /// Precondition: Variables must have been sanitized.
   ///
-  /// The term is floated if it:
-  /// - Is an Application without free variables.
-  /// - Is a Superposition.
-  /// - Is a combinator.
-  /// The term is not floated if it:
-  /// - Is safe or has unscoped variables.
+  /// The floating algorithm follows these rules:
+  /// - Don't extract safe terms or terms that contains unscoped variables.
+  /// - Extract if it is a closed Application
+  /// - Extract if it is a combinator
+  /// - Float every element of a Superposition
   pub fn float_combinators(&mut self) {
     let mut combinators = Combinators::new();
-    let mut safe_defs = IndexSet::new();
 
     let slf = self.clone();
     for (def_name, def) in self.defs.iter_mut() {
@@ -30,7 +28,8 @@ impl Book {
 
       let builtin = def.builtin;
       let rule = def.rule_mut();
-      rule.body.float_combinators(&mut combinators, &mut name_gen, &slf, def_name, builtin, &mut safe_defs);
+      let mut seen = IndexSet::new();
+      rule.body.float_combinators(&mut combinators, &mut name_gen, &slf, def_name, builtin, &mut seen);
     }
 
     self.defs.extend(combinators);
@@ -45,17 +44,17 @@ impl Term {
     book: &Book,
     def_name: &Name,
     builtin: bool,
-    safe_defs: &mut IndexSet<Name>,
+    seen: &mut IndexSet<Name>,
   ) {
     Term::recursive_call(move || {
       for term in self.children_mut() {
         // Don't float if it's safe or has unscoped variables.
-        if term.is_safe(book, safe_defs) || term.has_unscoped_diff() {
+        if term.is_safe(book, seen) || term.has_unscoped_diff() {
           continue;
         }
 
         // Recusively float the children terms.
-        term.float_combinators(combinators, name_gen, book, def_name, builtin, safe_defs);
+        term.float_combinators(combinators, name_gen, book, def_name, builtin, seen);
 
         match term {
           // If it is an Application without free variables like '(bar 0)', float into a new definition.
@@ -68,7 +67,7 @@ impl Term {
           // If it is a Superposition, float every child element.
           Term::Sup { els, .. } => els
             .iter_mut()
-            .for_each(|e| e.float_combinators(combinators, name_gen, book, def_name, builtin, safe_defs)),
+            .for_each(|e| e.float_combinators(combinators, name_gen, book, def_name, builtin, seen)),
 
           // If it is a combinator, float into a new definition.
           term if term.is_combinator() => float_combinator(def_name, name_gen, term, builtin, combinators),
@@ -102,34 +101,36 @@ fn float_combinator(
 impl Term {
   /// A term can be considered safe if it is:
   /// - A Number or an Eraser.
-  /// - A Tuple or Superposition where all elements are constants.
-  /// - A constant Lambda, e.g a nullary constructor.
+  /// - A Tuple or Superposition where all elements are safe.
+  /// - A constant Lambda, e.g. a nullary constructor.
   /// - A Reference with safe body.
-  pub fn is_safe(&self, book: &Book, safe_defs: &mut IndexSet<Name>) -> bool {
+  pub fn is_safe(&self, book: &Book, seen: &mut IndexSet<Name>) -> bool {
     Term::recursive_call(move || match self {
       Term::Num { .. } | Term::Era => true,
 
-      Term::Tup { els } | Term::Sup { els, .. } => els.iter().all(|e| Term::is_safe(e, book, safe_defs)),
+      Term::Tup { els } | Term::Sup { els, .. } => els.iter().all(|e| Term::is_safe(e, book, seen)),
 
-      Term::Lam { .. } => self.is_constant_lambda(book, safe_defs),
+      Term::Lam { .. } => self.is_constant_lambda(book, seen),
 
       Term::Ref { nam } => {
-        !safe_defs.insert(nam.clone())
-          || if let Some(definition) = book.defs.get(nam) {
-            definition.rule().body.is_safe(book, safe_defs)
-          } else {
-            false
-          }
+        if seen.contains(nam) {
+          return false;
+        }
+
+        seen.insert(nam.clone());
+        if let Some(definition) = book.defs.get(nam) {
+          definition.rule().body.is_safe(book, seen)
+        } else {
+          false
+        }
       }
 
-      // TODO?: Any term that, when fully expanded, becomes a supercombinator is safe.
-      // _ => self.is_supercombinator(),
       _ => false,
     })
   }
 
   /// Checks if the term is a lambda sequence with the body being a variable in the scope or a reference.
-  fn is_constant_lambda(&self, book: &Book, safe_defs: &mut IndexSet<Name>) -> bool {
+  fn is_constant_lambda(&self, book: &Book, seen: &mut IndexSet<Name>) -> bool {
     let mut current = self;
     let mut scope = Vec::new();
 
@@ -143,7 +144,7 @@ impl Term {
     match current {
       Term::Var { nam } if scope.contains(&nam) => true,
       Term::Ref { .. } => true,
-      term => term.is_safe(book, safe_defs),
+      term => term.is_safe(book, seen),
     }
   }
 
diff --git a/tests/golden_tests/desugar_file/combinators.hvm b/tests/golden_tests/desugar_file/combinators.hvm
index 50f80b58..cf4e398a 100644
--- a/tests/golden_tests/desugar_file/combinators.hvm
+++ b/tests/golden_tests/desugar_file/combinators.hvm
@@ -12,6 +12,10 @@
 
 (qux) = {0 qux}
 
+(tup) = (tup, 1, 0)
+
 (list) = [0 list]
 
+(A x) = let {a b} = A; (a b x)
+
 (Main) = list
diff --git a/tests/snapshots/desugar_file__combinators.hvm.snap b/tests/snapshots/desugar_file__combinators.hvm.snap
new file mode 100644
index 00000000..7a075339
--- /dev/null
+++ b/tests/snapshots/desugar_file__combinators.hvm.snap
@@ -0,0 +1,35 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/desugar_file/combinators.hvm
+---
+(foo) = λa λ* λ* (foo a)
+
+(bar) = λa λb (a bar b)
+
+(List.ignore) = λa λ* #List (a List.ignore$C1 0)
+
+(baz) = {0 1 2 3 λa a foo}
+
+(qux) = {0 qux}
+
+(tup) = (tup, 1, 0)
+
+(list) = (list$C0 list$C2)
+
+(A) = λa let {b c} = A; (b c a)
+
+(Main) = list
+
+(List.cons) = λa λb #List λc #List λ* #List (c a b)
+
+(List.nil) = #List λ* #List λb b
+
+(List.ignore$C0) = #List λd (List.ignore d List.ignore)
+
+(List.ignore$C1) = #List λ* List.ignore$C0
+
+(list$C0) = (List.cons 0)
+
+(list$C1) = (List.cons list)
+
+(list$C2) = (list$C1 List.nil)

From bbc714635efcb80a34f45b61cf5ab38e239d1ce2 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Wed, 27 Mar 2024 16:44:03 -0300
Subject: [PATCH 05/11] Fix typo

---
 src/term/transform/float_combinators.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs
index 33f17900..ec22f876 100644
--- a/src/term/transform/float_combinators.rs
+++ b/src/term/transform/float_combinators.rs
@@ -53,7 +53,7 @@ impl Term {
           continue;
         }
 
-        // Recusively float the children terms.
+        // Recursively float the children terms.
         term.float_combinators(combinators, name_gen, book, def_name, builtin, seen);
 
         match term {

From bd8fb66b8cd2898c81610f814637f9bee2ffa7f9 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Thu, 28 Mar 2024 09:10:10 -0300
Subject: [PATCH 06/11] Refactor float combinators

---
 src/term/transform/float_combinators.rs       | 53 ++++++++-----------
 ...mpile_file_o_all__list_merge_sort.hvm.snap |  8 ++-
 .../desugar_file__combinators.hvm.snap        |  4 +-
 .../snapshots/mutual_recursion__len.hvm.snap  |  4 +-
 4 files changed, 27 insertions(+), 42 deletions(-)

diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs
index ec22f876..2119b485 100644
--- a/src/term/transform/float_combinators.rs
+++ b/src/term/transform/float_combinators.rs
@@ -13,7 +13,7 @@ impl Book {
   /// The floating algorithm follows these rules:
   /// - Don't extract safe terms or terms that contains unscoped variables.
   /// - Extract if it is a closed Application
-  /// - Extract if it is a combinator
+  /// - Extract if it is a supercombinator
   /// - Float every element of a Superposition
   pub fn float_combinators(&mut self) {
     let mut combinators = Combinators::new();
@@ -46,36 +46,19 @@ impl Term {
     builtin: bool,
     seen: &mut IndexSet<Name>,
   ) {
-    Term::recursive_call(move || {
-      for term in self.children_mut() {
-        // Don't float if it's safe or has unscoped variables.
-        if term.is_safe(book, seen) || term.has_unscoped_diff() {
-          continue;
-        }
+    for term in self.children_mut() {
+      // Recursively float the children terms.
+      term.float_combinators(combinators, name_gen, book, def_name, builtin, seen);
 
-        // Recursively float the children terms.
-        term.float_combinators(combinators, name_gen, book, def_name, builtin, seen);
-
-        match term {
-          // If it is an Application without free variables like '(bar 0)', float into a new definition.
-          Term::App { .. } => {
-            if term.free_vars().is_empty() && !term.has_unscoped_diff() {
-              float_combinator(def_name, name_gen, term, builtin, combinators);
-            }
-          }
-
-          // If it is a Superposition, float every child element.
-          Term::Sup { els, .. } => els
-            .iter_mut()
-            .for_each(|e| e.float_combinators(combinators, name_gen, book, def_name, builtin, seen)),
-
-          // If it is a combinator, float into a new definition.
-          term if term.is_combinator() => float_combinator(def_name, name_gen, term, builtin, combinators),
-
-          _ => continue,
-        }
+      // Don't float if it has unscoped variables.
+      if term.has_unscoped_diff() {
+        return;
       }
-    })
+
+      if term.is_combinator() && !term.is_safe(book, seen) {
+        float_combinator(def_name, name_gen, term, builtin, combinators);
+      }
+    }
   }
 }
 
@@ -148,8 +131,8 @@ impl Term {
     }
   }
 
-  /// A term is a combinator if it is a lambda abstraction without free variables.
-  pub fn is_combinator(&self) -> bool {
+  /// A term is a supercombinator if it is a lambda abstraction without free variables.
+  pub fn is_supercombinator(&self) -> bool {
     matches!(self, Term::Lam { .. } if self.free_vars().is_empty())
   }
 
@@ -157,4 +140,12 @@ impl Term {
     let (declared, used) = self.unscoped_vars();
     declared.difference(&used).count() != 0
   }
+
+  fn is_combinator(&self) -> bool {
+    self.is_supercombinator() || self.is_closed_app()
+  }
+
+  fn is_closed_app(&self) -> bool {
+    matches!(self, Term::App { .. }) && self.free_vars().is_empty() && !self.has_unscoped_diff()
+  }
 }
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 e453ba2c..c61d593c 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
@@ -12,13 +12,11 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
 
 @Merge$C1 = {4 a {4 b (c ({4 @Merge$C0 {4 (* @Cons) (c (a (b d)))}} d))}}
 
-@MergePair$C0 = {4 a {4 {4 @MergePair$C3 {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$C0 = {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 = (a {4 {4 a {4 @Nil b}} {4 * b}})
 
-@MergePair$C2 = (* @MergePair$C1)
-
-@MergePair$C3 = {4 a {4 {4 @MergePair$C0 {4 @MergePair$C2 (b (a c))}} (b c)}}
+@MergePair$C2 = {4 a {4 {4 @MergePair$C0 {4 (* @MergePair$C1) (b (a c))}} (b c)}}
 
 @Nil = {4 * {4 a a}}
 
@@ -26,7 +24,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$C3 {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$C1 {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/desugar_file__combinators.hvm.snap b/tests/snapshots/desugar_file__combinators.hvm.snap
index 7a075339..b84eb396 100644
--- a/tests/snapshots/desugar_file__combinators.hvm.snap
+++ b/tests/snapshots/desugar_file__combinators.hvm.snap
@@ -6,7 +6,7 @@ input_file: tests/golden_tests/desugar_file/combinators.hvm
 
 (bar) = λa λb (a bar b)
 
-(List.ignore) = λa λ* #List (a List.ignore$C1 0)
+(List.ignore) = λa λ* #List (a #List λ* List.ignore$C0 0)
 
 (baz) = {0 1 2 3 λa a foo}
 
@@ -26,8 +26,6 @@ input_file: tests/golden_tests/desugar_file/combinators.hvm
 
 (List.ignore$C0) = #List λd (List.ignore d List.ignore)
 
-(List.ignore$C1) = #List λ* List.ignore$C0
-
 (list$C0) = (List.cons 0)
 
 (list$C1) = (List.cons list)
diff --git a/tests/snapshots/mutual_recursion__len.hvm.snap b/tests/snapshots/mutual_recursion__len.hvm.snap
index ed86bff9..ca3b7dac 100644
--- a/tests/snapshots/mutual_recursion__len.hvm.snap
+++ b/tests/snapshots/mutual_recursion__len.hvm.snap
@@ -2,14 +2,12 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/mutual_recursion/len.hvm
 ---
-@Len = ({2 @Len$C1 {2 #0 a}} a)
+@Len = ({2 {2 * @Len$C0} {2 #0 a}} a)
 
 @Len$C0 = {2 a b}
   & #1 ~ <+ c b>
   & @Len ~ (a c)
 
-@Len$C1 = {2 * @Len$C0}
-
 @List.cons = (a (b {2 {2 a {2 b c}} {2 * c}}))
 
 @List.nil = {2 * {2 a a}}

From 1f273c4fc406ed33ec4e146c641e9dae3c732e71 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Thu, 28 Mar 2024 15:34:42 -0300
Subject: [PATCH 07/11] Refactor float combinator logic and implement float
 iterator

---
 src/term/mod.rs                               |  1 +
 src/term/transform/float_combinators.rs       | 64 ++++++++++++++-----
 .../golden_tests/desugar_file/combinators.hvm |  4 +-
 ...pile_file__match_num_all_patterns.hvm.snap |  6 +-
 ...le_file__unscoped_supercombinator.hvm.snap |  2 +-
 ...mpile_file_o_all__list_merge_sort.hvm.snap |  6 +-
 ...ll__recursive_combinator_inactive.hvm.snap |  4 +-
 .../desugar_file__combinators.hvm.snap        | 16 +++--
 8 files changed, 73 insertions(+), 30 deletions(-)

diff --git a/src/term/mod.rs b/src/term/mod.rs
index 83bb70d2..f3f4fcd2 100644
--- a/src/term/mod.rs
+++ b/src/term/mod.rs
@@ -231,6 +231,7 @@ pub struct Name(GlobalString);
 /// A macro for creating iterators that can have statically known
 /// different types. Useful for iterating over tree children, where
 /// each tree node variant yields a different iterator type.
+#[macro_export]
 macro_rules! multi_iterator {
   ($Iter:ident { $($Variant:ident),* $(,)? }) => {
     #[derive(Debug, Clone)]
diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs
index 2119b485..47b0f86c 100644
--- a/src/term/transform/float_combinators.rs
+++ b/src/term/transform/float_combinators.rs
@@ -1,6 +1,9 @@
 use indexmap::IndexSet;
 
-use crate::term::{Book, Definition, Name, Rule, Term};
+use crate::{
+  multi_iterator,
+  term::{Book, Definition, Name, Rule, Term},
+};
 use std::collections::BTreeMap;
 
 type Combinators = BTreeMap<Name, Definition>;
@@ -46,13 +49,13 @@ impl Term {
     builtin: bool,
     seen: &mut IndexSet<Name>,
   ) {
-    for term in self.children_mut() {
+    for term in self.float_children_mut() {
       // Recursively float the children terms.
       term.float_combinators(combinators, name_gen, book, def_name, builtin, seen);
 
       // Don't float if it has unscoped variables.
       if term.has_unscoped_diff() {
-        return;
+        continue;
       }
 
       if term.is_combinator() && !term.is_safe(book, seen) {
@@ -85,7 +88,7 @@ impl Term {
   /// A term can be considered safe if it is:
   /// - A Number or an Eraser.
   /// - A Tuple or Superposition where all elements are safe.
-  /// - A constant Lambda, e.g. a nullary constructor.
+  /// - A safe Lambda, e.g. a nullary constructor or a lambda with safe body.
   /// - A Reference with safe body.
   pub fn is_safe(&self, book: &Book, seen: &mut IndexSet<Name>) -> bool {
     Term::recursive_call(move || match self {
@@ -93,7 +96,7 @@ impl Term {
 
       Term::Tup { els } | Term::Sup { els, .. } => els.iter().all(|e| Term::is_safe(e, book, seen)),
 
-      Term::Lam { .. } => self.is_constant_lambda(book, seen),
+      Term::Lam { .. } => self.is_safe_lambda(book, seen),
 
       Term::Ref { nam } => {
         if seen.contains(nam) {
@@ -113,7 +116,7 @@ impl Term {
   }
 
   /// Checks if the term is a lambda sequence with the body being a variable in the scope or a reference.
-  fn is_constant_lambda(&self, book: &Book, seen: &mut IndexSet<Name>) -> bool {
+  fn is_safe_lambda(&self, book: &Book, seen: &mut IndexSet<Name>) -> bool {
     let mut current = self;
     let mut scope = Vec::new();
 
@@ -131,21 +134,52 @@ impl Term {
     }
   }
 
-  /// A term is a supercombinator if it is a lambda abstraction without free variables.
-  pub fn is_supercombinator(&self) -> bool {
-    matches!(self, Term::Lam { .. } if self.free_vars().is_empty())
-  }
-
   pub fn has_unscoped_diff(&self) -> bool {
     let (declared, used) = self.unscoped_vars();
-    declared.difference(&used).count() != 0
+
+    declared.difference(&used).count() != 0 || used.difference(&declared).count() != 0
   }
 
   fn is_combinator(&self) -> bool {
-    self.is_supercombinator() || self.is_closed_app()
+    self.is_closed()
   }
 
-  fn is_closed_app(&self) -> bool {
-    matches!(self, Term::App { .. }) && self.free_vars().is_empty() && !self.has_unscoped_diff()
+  pub fn is_closed(&self) -> bool {
+    self.free_vars().is_empty() && !self.has_unscoped_diff() && !matches!(self, Term::Ref { .. })
+  }
+}
+
+impl Term {
+  pub fn float_children_mut(&mut self) -> impl DoubleEndedIterator<Item = &mut Term> {
+    multi_iterator!(FloatIter { Zero, One, Two, Vec, Mat, App });
+    match self {
+      Term::App { fun, arg, .. } => {
+        let mut args = vec![arg.as_mut()];
+        let mut app = fun.as_mut();
+        while let Term::App { fun, arg, .. } = app {
+          args.push(arg);
+          app = fun;
+        }
+        args.push(app);
+        FloatIter::App(args)
+      }
+      Term::Mat { args, rules } => {
+        FloatIter::Mat(args.iter_mut().chain(rules.iter_mut().map(|r| &mut r.body)))
+      }
+      Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => FloatIter::Vec(els),
+      Term::Let { val: fst, nxt: snd, .. }
+      | Term::Use { val: fst, nxt: snd, .. }
+      | Term::Dup { val: fst, nxt: snd, .. }
+      | Term::Opx { fst, snd, .. } => FloatIter::Two([fst.as_mut(), snd.as_mut()]),
+      Term::Lam { bod, .. } | Term::Chn { bod, .. } => FloatIter::One([bod.as_mut()]),
+      Term::Var { .. }
+      | Term::Lnk { .. }
+      | Term::Num { .. }
+      | Term::Nat { .. }
+      | Term::Str { .. }
+      | Term::Ref { .. }
+      | Term::Era
+      | Term::Err => FloatIter::Zero([]),
+    }
   }
 }
diff --git a/tests/golden_tests/desugar_file/combinators.hvm b/tests/golden_tests/desugar_file/combinators.hvm
index cf4e398a..05d8f9ea 100644
--- a/tests/golden_tests/desugar_file/combinators.hvm
+++ b/tests/golden_tests/desugar_file/combinators.hvm
@@ -16,6 +16,8 @@
 
 (list) = [0 list]
 
-(A x) = let {a b} = A; (a b x)
+(A x) = (let {a b} = A; @c (a b c) x)
+
+(B x) = (let (a, b) = B; @c (a b c) x)
 
 (Main) = list
diff --git a/tests/snapshots/compile_file__match_num_all_patterns.hvm.snap b/tests/snapshots/compile_file__match_num_all_patterns.hvm.snap
index b3d3b2d3..dc8212d0 100644
--- a/tests/snapshots/compile_file__match_num_all_patterns.hvm.snap
+++ b/tests/snapshots/compile_file__match_num_all_patterns.hvm.snap
@@ -30,10 +30,12 @@ In definition 'zero_var_succ':
 
 @succ_var = (?<#0 (a a) b> b)
 
-@succ_var_zero = (?<a @succ_var_zero$C0 b> b)
+@succ_var_zero = (?<@succ_var_zero$C0 @succ_var_zero$C1 a> a)
+
+@succ_var_zero$C0 = a
   & #0 ~ <+ #1 a>
 
-@succ_var_zero$C0 = (<+ #2 a> a)
+@succ_var_zero$C1 = (<+ #2 a> a)
 
 @succ_zero = (?<#0 (a a) b> b)
 
diff --git a/tests/snapshots/compile_file__unscoped_supercombinator.hvm.snap b/tests/snapshots/compile_file__unscoped_supercombinator.hvm.snap
index 7f81e847..ef64214b 100644
--- a/tests/snapshots/compile_file__unscoped_supercombinator.hvm.snap
+++ b/tests/snapshots/compile_file__unscoped_supercombinator.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/unscoped_supercombinator.hvm
 ---
-@Foo = ((@Foo$C0 (@Foo$C1 a)) a)
+@Foo = ((@Foo$C1 (@Foo$C0 a)) a)
 
 @Foo$C0 = (a ((a b) b))
 
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 c61d593c..e6537b16 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
@@ -12,11 +12,11 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
 
 @Merge$C1 = {4 a {4 b (c ({4 @Merge$C0 {4 (* @Cons) (c (a (b d)))}} d))}}
 
-@MergePair$C0 = {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$C0 = (a {4 {4 a {4 @Nil b}} {4 * b}})
 
-@MergePair$C1 = (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$C2 = {4 a {4 {4 @MergePair$C0 {4 (* @MergePair$C1) (b (a c))}} (b c)}}
+@MergePair$C2 = {4 a {4 {4 @MergePair$C1 {4 (* @MergePair$C0) (b (a c))}} (b c)}}
 
 @Nil = {4 * {4 a a}}
 
diff --git a/tests/snapshots/compile_file_o_all__recursive_combinator_inactive.hvm.snap b/tests/snapshots/compile_file_o_all__recursive_combinator_inactive.hvm.snap
index 2cf847f3..c601a8f6 100644
--- a/tests/snapshots/compile_file_o_all__recursive_combinator_inactive.hvm.snap
+++ b/tests/snapshots/compile_file_o_all__recursive_combinator_inactive.hvm.snap
@@ -2,7 +2,9 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/recursive_combinator_inactive.hvm
 ---
-@Foo = (?<{3 @Foo @Foo} (a (* a)) b> b)
+@Foo = (?<@Foo$C0 (a (* a)) b> b)
+
+@Foo$C0 = {3 @Foo @Foo}
 
 @main = a
   & @Foo ~ (#0 a)
diff --git a/tests/snapshots/desugar_file__combinators.hvm.snap b/tests/snapshots/desugar_file__combinators.hvm.snap
index b84eb396..22559c08 100644
--- a/tests/snapshots/desugar_file__combinators.hvm.snap
+++ b/tests/snapshots/desugar_file__combinators.hvm.snap
@@ -14,9 +14,11 @@ input_file: tests/golden_tests/desugar_file/combinators.hvm
 
 (tup) = (tup, 1, 0)
 
-(list) = (list$C0 list$C2)
+(list) = (List.cons 0 list$C0)
 
-(A) = λa let {b c} = A; (b c a)
+(A) = λa (A$C0 a)
+
+(B) = λa (B$C0 a)
 
 (Main) = list
 
@@ -24,10 +26,10 @@ input_file: tests/golden_tests/desugar_file/combinators.hvm
 
 (List.nil) = #List λ* #List λb b
 
+(A$C0) = let {b c} = A; λd (b c d)
+
+(B$C0) = let (c, d) = B; λe (c d e)
+
 (List.ignore$C0) = #List λd (List.ignore d List.ignore)
 
-(list$C0) = (List.cons 0)
-
-(list$C1) = (List.cons list)
-
-(list$C2) = (list$C1 List.nil)
+(list$C0) = (List.cons list List.nil)

From ab2e081d0378c521b1f809023e575354210f3745 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Thu, 28 Mar 2024 15:39:16 -0300
Subject: [PATCH 08/11] Remove unnecessary condition

---
 src/term/transform/float_combinators.rs | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs
index 47b0f86c..5595a1a1 100644
--- a/src/term/transform/float_combinators.rs
+++ b/src/term/transform/float_combinators.rs
@@ -53,11 +53,6 @@ impl Term {
       // Recursively float the children terms.
       term.float_combinators(combinators, name_gen, book, def_name, builtin, seen);
 
-      // Don't float if it has unscoped variables.
-      if term.has_unscoped_diff() {
-        continue;
-      }
-
       if term.is_combinator() && !term.is_safe(book, seen) {
         float_combinator(def_name, name_gen, term, builtin, combinators);
       }

From c695bbcf2cb7d9bcb278b05223bd301d6a72f19d Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Thu, 28 Mar 2024 16:59:03 -0300
Subject: [PATCH 09/11] Update float children lambda case and docs

---
 src/term/transform/float_combinators.rs        | 18 ++++++------------
 ...ompile_file_o_all__list_merge_sort.hvm.snap |  4 ++--
 .../desugar_file__combinators.hvm.snap         |  4 ++--
 tests/snapshots/mutual_recursion__len.hvm.snap |  4 ++--
 4 files changed, 12 insertions(+), 18 deletions(-)

diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs
index 5595a1a1..8f723b69 100644
--- a/src/term/transform/float_combinators.rs
+++ b/src/term/transform/float_combinators.rs
@@ -14,10 +14,8 @@ impl Book {
   /// Precondition: Variables must have been sanitized.
   ///
   /// The floating algorithm follows these rules:
-  /// - Don't extract safe terms or terms that contains unscoped variables.
-  /// - Extract if it is a closed Application
-  /// - Extract if it is a supercombinator
-  /// - Float every element of a Superposition
+  /// - Recusively float every child term.
+  /// - Extract if it is a combinator and not is a safe term.
   pub fn float_combinators(&mut self) {
     let mut combinators = Combinators::new();
 
@@ -71,8 +69,8 @@ fn float_combinator(
   let comb_name = Name::new(format!("{}$C{}", def_name, *name_gen));
   *name_gen += 1;
 
-  let comb_var = Term::Ref { nam: comb_name.clone() };
-  let extracted_term = std::mem::replace(term, comb_var);
+  let comb_ref = Term::Ref { nam: comb_name.clone() };
+  let extracted_term = std::mem::replace(term, comb_ref);
 
   let rules = vec![Rule { body: extracted_term, pats: Vec::new() }];
   let rule = Definition { name: comb_name.clone(), rules, builtin };
@@ -136,17 +134,13 @@ impl Term {
   }
 
   fn is_combinator(&self) -> bool {
-    self.is_closed()
-  }
-
-  pub fn is_closed(&self) -> bool {
     self.free_vars().is_empty() && !self.has_unscoped_diff() && !matches!(self, Term::Ref { .. })
   }
 }
 
 impl Term {
   pub fn float_children_mut(&mut self) -> impl DoubleEndedIterator<Item = &mut Term> {
-    multi_iterator!(FloatIter { Zero, One, Two, Vec, Mat, App });
+    multi_iterator!(FloatIter { Zero, Two, Vec, Mat, App });
     match self {
       Term::App { fun, arg, .. } => {
         let mut args = vec![arg.as_mut()];
@@ -166,7 +160,7 @@ impl Term {
       | Term::Use { val: fst, nxt: snd, .. }
       | Term::Dup { val: fst, nxt: snd, .. }
       | Term::Opx { fst, snd, .. } => FloatIter::Two([fst.as_mut(), snd.as_mut()]),
-      Term::Lam { bod, .. } | Term::Chn { bod, .. } => FloatIter::One([bod.as_mut()]),
+      Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.float_children_mut(),
       Term::Var { .. }
       | Term::Lnk { .. }
       | Term::Num { .. }
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 e6537b16..00e5a684 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
@@ -12,11 +12,11 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
 
 @Merge$C1 = {4 a {4 b (c ({4 @Merge$C0 {4 (* @Cons) (c (a (b d)))}} d))}}
 
-@MergePair$C0 = (a {4 {4 a {4 @Nil b}} {4 * b}})
+@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$C2 = {4 a {4 {4 @MergePair$C1 {4 (* @MergePair$C0) (b (a c))}} (b c)}}
+@MergePair$C2 = {4 a {4 {4 @MergePair$C1 {4 @MergePair$C0 (b (a c))}} (b c)}}
 
 @Nil = {4 * {4 a a}}
 
diff --git a/tests/snapshots/desugar_file__combinators.hvm.snap b/tests/snapshots/desugar_file__combinators.hvm.snap
index 22559c08..446098bb 100644
--- a/tests/snapshots/desugar_file__combinators.hvm.snap
+++ b/tests/snapshots/desugar_file__combinators.hvm.snap
@@ -6,7 +6,7 @@ input_file: tests/golden_tests/desugar_file/combinators.hvm
 
 (bar) = λa λb (a bar b)
 
-(List.ignore) = λa λ* #List (a #List λ* List.ignore$C0 0)
+(List.ignore) = λa λ* #List (a List.ignore$C0 0)
 
 (baz) = {0 1 2 3 λa a foo}
 
@@ -30,6 +30,6 @@ input_file: tests/golden_tests/desugar_file/combinators.hvm
 
 (B$C0) = let (c, d) = B; λe (c d e)
 
-(List.ignore$C0) = #List λd (List.ignore d List.ignore)
+(List.ignore$C0) = #List λ* #List λd (List.ignore d List.ignore)
 
 (list$C0) = (List.cons list List.nil)
diff --git a/tests/snapshots/mutual_recursion__len.hvm.snap b/tests/snapshots/mutual_recursion__len.hvm.snap
index ca3b7dac..80481c36 100644
--- a/tests/snapshots/mutual_recursion__len.hvm.snap
+++ b/tests/snapshots/mutual_recursion__len.hvm.snap
@@ -2,9 +2,9 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/mutual_recursion/len.hvm
 ---
-@Len = ({2 {2 * @Len$C0} {2 #0 a}} a)
+@Len = ({2 @Len$C0 {2 #0 a}} a)
 
-@Len$C0 = {2 a b}
+@Len$C0 = {2 * {2 a b}}
   & #1 ~ <+ c b>
   & @Len ~ (a c)
 

From 37fdd38d7b6459de1bb5b3a72d15b47451e0750c Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Thu, 28 Mar 2024 17:02:38 -0300
Subject: [PATCH 10/11] Fix typo

---
 src/term/transform/float_combinators.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs
index 8f723b69..24a05680 100644
--- a/src/term/transform/float_combinators.rs
+++ b/src/term/transform/float_combinators.rs
@@ -14,7 +14,7 @@ impl Book {
   /// Precondition: Variables must have been sanitized.
   ///
   /// The floating algorithm follows these rules:
-  /// - Recusively float every child term.
+  /// - Recursively float every child term.
   /// - Extract if it is a combinator and not is a safe term.
   pub fn float_combinators(&mut self) {
     let mut combinators = Combinators::new();

From 30d7888d23a6273447e6e814a405c254c6cf1914 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Thu, 28 Mar 2024 19:10:49 -0300
Subject: [PATCH 11/11] Update combinators test and improve docs

---
 src/term/transform/float_combinators.rs            | 3 ++-
 tests/golden_tests/desugar_file/combinators.hvm    | 6 ++++--
 tests/snapshots/desugar_file__combinators.hvm.snap | 4 ++++
 3 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/term/transform/float_combinators.rs b/src/term/transform/float_combinators.rs
index 24a05680..3a3aae3d 100644
--- a/src/term/transform/float_combinators.rs
+++ b/src/term/transform/float_combinators.rs
@@ -15,7 +15,8 @@ impl Book {
   ///
   /// The floating algorithm follows these rules:
   /// - Recursively float every child term.
-  /// - Extract if it is a combinator and not is a safe term.
+  /// - Extract if it is a combinator and is not a safe term.
+  /// See [`Term::is_safe`] for what is considered safe here.
   pub fn float_combinators(&mut self) {
     let mut combinators = Combinators::new();
 
diff --git a/tests/golden_tests/desugar_file/combinators.hvm b/tests/golden_tests/desugar_file/combinators.hvm
index 05d8f9ea..bbbc458d 100644
--- a/tests/golden_tests/desugar_file/combinators.hvm
+++ b/tests/golden_tests/desugar_file/combinators.hvm
@@ -12,12 +12,14 @@
 
 (qux) = {0 qux}
 
+(clax) = (λx x λa λb λc λd (clax d))
+
 (tup) = (tup, 1, 0)
 
 (list) = [0 list]
 
-(A x) = (let {a b} = A; @c (a b c) x)
+(A x) = (let {a b} = A; λc (a b c) x)
 
-(B x) = (let (a, b) = B; @c (a b c) x)
+(B x) = (let (a, b) = B; λc (a b c) x)
 
 (Main) = list
diff --git a/tests/snapshots/desugar_file__combinators.hvm.snap b/tests/snapshots/desugar_file__combinators.hvm.snap
index 446098bb..062a8a5f 100644
--- a/tests/snapshots/desugar_file__combinators.hvm.snap
+++ b/tests/snapshots/desugar_file__combinators.hvm.snap
@@ -12,6 +12,8 @@ input_file: tests/golden_tests/desugar_file/combinators.hvm
 
 (qux) = {0 qux}
 
+(clax) = (λa a clax$C0)
+
 (tup) = (tup, 1, 0)
 
 (list) = (List.cons 0 list$C0)
@@ -32,4 +34,6 @@ input_file: tests/golden_tests/desugar_file/combinators.hvm
 
 (List.ignore$C0) = #List λ* #List λd (List.ignore d List.ignore)
 
+(clax$C0) = λ* λ* λ* λe (clax e)
+
 (list$C0) = (List.cons list List.nil)