[sc-339] Improve eta-reduction to not apply on all functions

src/term/mod.rs

@@ -41,6 +41,7 @@ pub struct DefNames {
 #[derive(Debug, Clone)]
 pub struct Definition {
   pub def_id: DefId,
+  pub generated: bool,
   pub rules: Vec<Rule>,
 }
 
@@ -220,9 +221,9 @@ impl Book {
     Default::default()
   }
 
-  pub fn insert_def(&mut self, name: Name, rules: Vec<Rule>) -> DefId {
+  pub fn insert_def(&mut self, name: Name, is_generated: bool, rules: Vec<Rule>) -> DefId {
     let def_id = self.def_names.insert(name);
-    let def = Definition { def_id, rules };
+    let def = Definition { def_id, generated: is_generated, rules };
     self.defs.insert(def_id, def);
     def_id
   }

src/term/parser/parser.rs

@@ -357,7 +357,7 @@ where
           if let Some(def_id) = book.def_names.def_id(&nam) {
             book.defs.get_mut(&def_id).unwrap().rules.push(rule);
           } else {
-            book.insert_def(nam, vec![rule]);
+            book.insert_def(nam, false, vec![rule]);
           }
         }
         TopLevel::Adt((nam, adt)) => {

src/term/transform/definition_pruning.rs

@@ -12,18 +12,15 @@ impl Book {
     // to mark as used all constructors in case of the user
     // manually encode a constructor with tagged lambdas
     for ctr in self.ctrs.keys() {
-      let Definition { def_id, rules } = self.defs.get(&self.def_names.name_to_id[ctr]).unwrap();
-      used.insert(*def_id);
-      for rule in rules {
-        rule.body.find_used_definitions(&mut used, &self.defs);
-      }
+      let def = self.defs.get(&self.def_names.name_to_id[ctr]).unwrap();
+      used.insert(def.def_id);
+      def.assert_no_pattern_matching_rules();
+      def.rules[0].body.find_used_definitions(&mut used, &self.defs);
     }
 
-    let Definition { def_id, rules } = self.defs.get(&main).unwrap();
-    used.insert(*def_id);
-    for rule in rules {
-      rule.body.find_used_definitions(&mut used, &self.defs);
-    }
+    let def = self.defs.get(&main).unwrap();
+    used.insert(def.def_id);
+    def.rules[0].body.find_used_definitions(&mut used, &self.defs);
 
     let ids = HashSet::from_iter(self.def_names.def_ids().copied());
     let unused = ids.difference(&used);

src/term/transform/detach_supercombinators.rs

@@ -9,9 +9,8 @@ impl Book {
     let mut combinators = Combinators::new();
 
     for def in self.defs.values_mut() {
-      for rule in def.rules.iter_mut() {
-        rule.body.detach_combinators(def.def_id, &mut self.def_names, &mut combinators);
-      }
+      def.assert_no_pattern_matching_rules();
+      def.rules[0].body.detach_combinators(def.def_id, &mut self.def_names, &mut combinators);
     }
 
     // Definitions are not inserted to the book as they are defined to appease the borrow checker.
@@ -68,7 +67,7 @@ impl<'d> TermInfo<'d> {
     let extracted_term = std::mem::replace(term, comb_var);
 
     let rules = vec![Rule { body: extracted_term, pats: Vec::new() }];
-    let rule = Definition { def_id: comb_id, rules };
+    let rule = Definition { def_id: comb_id, rules, generated: false };
     self.combinators.insert(comb_id, rule);
   }
 }

src/term/transform/encode_adts.rs

@@ -14,7 +14,7 @@ impl Book {
       }
     }
     for (name, rules) in defs {
-      self.insert_def(name, rules);
+      self.insert_def(name, true, rules);
     }
   }
 }

src/term/transform/encode_pattern_matching.rs

@@ -12,7 +12,7 @@ impl Book {
       if is_matching_def {
         make_pattern_matching_def(self, def_id, def_type);
       } else {
-        // For functions with only one rule that doesnt pattern match,
+        // For functions with only one rule that doesn't pattern match,
         // we just move the variables from arg to body.
         make_non_pattern_matching_def(self, def_id);
       }
@@ -50,7 +50,8 @@ fn make_pattern_matching_def(book: &mut Book, def_id: DefId, def_type: &[Type])
   }
   for (rule_idx, body) in rule_bodies.into_iter().enumerate() {
     let rule_name = make_rule_name(&def_name, rule_idx);
-    book.insert_def(rule_name, vec![Rule { pats: vec![], body }]);
+    let is_generated = false;
+    book.insert_def(rule_name, is_generated, vec![Rule { pats: vec![], body }]);
   }
 
   // Generate scott-encoded pattern matching
@@ -454,7 +455,7 @@ fn add_case_to_book(book: &mut Book, nam: Name, body: Term) {
   if let Some(def_id) = book.def_names.def_id(&nam) {
     book.defs.get_mut(&def_id).unwrap().rules = vec![Rule { pats: vec![], body }];
   } else {
-    book.insert_def(nam, vec![Rule { pats: vec![], body }]);
+    book.insert_def(nam, true, vec![Rule { pats: vec![], body }]);
   }
 }
 

src/term/transform/eta_reduction.rs

@@ -1,12 +1,14 @@
 use crate::term::*;
 
 impl Book {
-  /// Applies eta-reduction to all definitions, converting occurences of `@x (f x)` into just `f`.
+  /// 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() {
-      for rule in def.rules.iter_mut() {
-        rule.body.eta_reduction();
+      def.assert_no_pattern_matching_rules();
+      if def.generated {
+        let rule = &mut def.rules[0].body;
+        rule.eta_reduction();
       }
     }
   }

src/term/transform/extract_matches.rs

@@ -187,7 +187,7 @@ fn match_to_def(
 
   let new_name = make_def_name(def_name, &Name::new("match"), match_count);
   let def_id = book.def_names.insert(new_name);
-  let def = Definition { def_id, rules };
+  let def = Definition { def_id, generated: true, rules };
   book.new_defs.insert(def_id, def);
 
   let scrutinee_app = Term::App {

src/term/transform/flatten.rs

@@ -24,7 +24,7 @@ fn flatten_def(def: &Definition, def_names: &mut DefNames) -> Vec<Definition> {
     .into_iter()
     .map(|(name, rules)| {
       let def_id = def_names.def_id(&name).unwrap();
-      Definition { def_id, rules }
+      Definition { def_id , generated: def.generated, rules }
     })
     .collect()
 }

src/term/transform/linearize.rs

@@ -17,9 +17,8 @@ use std::collections::{hash_map::Entry, HashMap};
 impl Book {
   pub fn linearize_vars(&mut self) {
     for def in self.defs.values_mut() {
-      for rule in def.rules.iter_mut() {
-        rule.body.linearize_vars();
-      }
+      def.assert_no_pattern_matching_rules();
+      def.rules[0].body.linearize_vars();
     }
   }
 }

src/term/transform/unique_names.rs

@@ -9,9 +9,8 @@ impl Book {
   /// Precondition: Definition references have been resolved, no unbound variables.
   pub fn make_var_names_unique(&mut self) {
     for def in self.defs.values_mut() {
-      for rule in def.rules.iter_mut() {
-        rule.body.make_var_names_unique()
-      }
+      def.assert_no_pattern_matching_rules();
+      def.rules[0].body.make_var_names_unique()
     }
   }
 }

tests/golden_tests/compile_file/long_name.hvm

@@ -1,2 +1,2 @@
 (WowThis_is_a_very_long_name_no_way_ItFits) = λa a
-main = λa (WowThis_is_a_very_long_name_no_way_ItFits *)
+main = λa (WowThis_is_a_very_long_name_no_way_ItFits *)

tests/golden_tests/compile_file/eta.hvm → tests/golden_tests/compile_file/unapplied_eta.hvm

@@ -1,2 +1,2 @@
-Id = λb b
+Id = λa a
 main = λa (Id a)

tests/snapshots/compile_file__adt_option_and.hvm.snap

@@ -2,15 +2,15 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/adt_option_and.hvm
 ---
-@6 = ({2 @D {2 @C a}} a)
 @8 = (* @None)
 @9 = {4 a (b {2 {4 [b a] c} {2 * c}})}
 @C = (* @None)
 @D = {4 a ({2 @9 {2 @8 (a b)}} b)}
 @None = {2 * {2 a a}}
+@Option.and = ({2 @D {2 @C (a b)}} (a b))
 @Some = (a {2 {4 a b} {2 * b}})
 @main = a
-& @6 ~ (b (c a))
+& @Option.and ~ (b (c a))
 & @Some ~ (#3 c)
 & @Some ~ (#1 b)
 

tests/snapshots/compile_file__and.hvm.snap

@@ -4,9 +4,9 @@ input_file: tests/golden_tests/compile_file/and.hvm
 ---
 @6 = (a a)
 @8 = (* @false)
-@9 = (a ({2 @6 {2 @8 (a b)}} b))
+@and = (a ({2 @6 {2 @8 (a b)}} b))
 @false = {2 * {2 a a}}
 @main = a
-& @9 ~ (@true (@false a))
+& @and ~ (@true (@false a))
 @true = {2 a {2 * a}}
 

tests/snapshots/compile_file__ex2.hvm.snap

@@ -6,14 +6,14 @@ input_file: tests/golden_tests/compile_file/ex2.hvm
 @F = (* (a a))
 @I = (a (* ((a b) (* b))))
 @c2 = ({3 (a b) (c a)} (c b))
-@decO = ((@decO (@low (@E a))) (* ((a b) (* b))))
-@low = ((@lowO (@lowI (@E a))) a)
+@decI = ((@lowO (@lowI (@E a))) a)
+@decO = ((@decO (@decI (@E a))) (* ((a b) (* b))))
 @lowI = (a (((* ((a b) (* b))) c) (* (* c))))
 @lowO = (a ((((a b) (* (* b))) c) (* (* c))))
 @main = a
 & @run ~ (b a)
 & @c2 ~ (@I (@E b))
 @run = ((@runO (@runI (@E a))) a)
 @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)
 

tests/snapshots/compile_file__extracted_match_pred.hvm.snap

@@ -2,8 +2,9 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/extracted_match_pred.hvm
 ---
-@5 = (?<(@valZ @5) a> a)
+@7 = (?<(@valZ @7) a> a)
 @main = a
-& @5 ~ (#1 a)
+& @val ~ (#1 a)
+@val = (?<(@valZ @7) a> a)
 @valZ = #0
 

tests/snapshots/compile_file__fst.hvm.snap

@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/fst.hvm
 ---
-@3 = ([a *] a)
+@Fst = ([a *] a)
 @main = a
-& @3 ~ ([#4 #8] a)
+& @Fst ~ ([#4 #8] a)
 

tests/snapshots/compile_file__fst_fst.hvm.snap

@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/fst_fst.hvm
 ---
-@5 = ([a *] ([b *] [a b]))
+@FstFst = ([a *] ([b *] [a b]))
 @main = a
-& @5 ~ ([#3 #9] ([#4 #12] a))
+& @FstFst ~ ([#3 #9] ([#4 #12] a))
 

tests/snapshots/compile_file__let_adt_destructuring.hvm.snap

@@ -2,10 +2,10 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/let_adt_destructuring.hvm
 ---
-@4 = ({2 @6 a} a)
 @6 = {4 a a}
 @Box = (a {2 {4 a b} b})
+@Unbox = ({2 @6 a} a)
 @main = a
-& @4 ~ (b a)
+& @Unbox ~ (b a)
 & @Box ~ (#1 b)
 

tests/snapshots/compile_file__linearize_match.hvm.snap

@@ -2,7 +2,9 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/linearize_match.hvm
 ---
+@2 = (?<(@3 @4) a> a)
 @3 = (a a)
 @4 = (<+ a b> (a b))
-@main = (?<(@3 @4) a> a)
+@main = (a (b c))
+& @2 ~ (a (b c))
 

tests/snapshots/compile_file__list_merge_sort.hvm.snap

@@ -11,7 +11,7 @@ input_file: tests/golden_tests/compile_file/list_merge_sort.hvm
 @Pure = (a {4 {8 a {6 @Nil b}} {4 * b}})
 @Q = {8 a {6 {4 @i {4 @j (b (a c))}} (b c)}}
 @R = (* @Nil)
-@S = (a ({4 @Q {4 @R (a b)}} b))
+@Unpack = (a ({4 @Q {4 @R (a b)}} b))
 @V = {8 a {6 {4 @o {4 @p (b (a c))}} (b c)}}
 @W = (* @Nil)
 @b = {8 {15 a {17 b c}} {6 {19 {4 @b {4 @c (d (e (f g)))}} h} ({5 d {7 i (j (c {2 @F {2 @G ({4 {8 k {6 l m}} {4 * m}} ({4 {8 a {6 g n}} {4 * n}} o))}}))}} ({9 e {11 k j}} ({13 f {4 @d {4 @e (i ({4 {8 b {6 h p}} {4 * p}} l))}}} o)))}}
@@ -21,10 +21,10 @@ input_file: tests/golden_tests/compile_file/list_merge_sort.hvm
 @i = {8 a {6 {4 @V {4 @W (b {4 @i {4 @j (c (d e))}})}} ({21 {23 b f} c} ({4 @d {4 @e (f (a d))}} e))}}
 @j = (* (a a))
 @main = (a (b c))
-& @S ~ (a (d c))
+& @Unpack ~ (a (d c))
 & @Map ~ (b (@Pure d))
 @o = {8 a {6 {4 @V {4 @W (b c)}} ({23 b d} ({4 @d {4 @e (d (a e))}} {4 {8 e {6 c f}} {4 * f}}))}}
-@p = (* @t)
+@p = (* @u)
 @s = (a (b {4 {8 a {6 b c}} {4 * c}}))
-@t = (a {4 {8 a {6 @Nil b}} {4 * b}})
+@u = (a {4 {8 a {6 @Nil b}} {4 * b}})
 

tests/snapshots/compile_file__match_mult_linearization.hvm.snap

@@ -2,7 +2,9 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/match_mult_linearization.hvm
 ---
+@2 = (?<(@3 @4) a> a)
 @3 = (<+ a <+ b c>> (a (b c)))
 @4 = (<+ a <+ b <+ c d>>> (a (b (c d))))
-@main = (?<(@3 @4) a> a)
+@main = (a (b (c (d e))))
+& @2 ~ (a (b (c (d e))))
 

tests/snapshots/compile_file__match_num_explicit_bind.hvm.snap

@@ -2,9 +2,9 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/match_num_explicit_bind.hvm
 ---
-@3 = (?<(@4 @5) a> a)
 @4 = #0
 @5 = (a a)
 @main = a
-& @3 ~ (#4 a)
+& @pred ~ (#4 a)
+@pred = (?<(@4 @5) a> a)
 

tests/snapshots/compile_file__match_tup.hvm.snap

@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/match_tup.hvm
 ---
-@3 = ([<+ a b> a] b)
+@Sum = ([<+ a b> a] b)
 @main = a
-& @3 ~ ([#7 #3] a)
+& @Sum ~ ([#7 #3] a)
 

tests/snapshots/compile_file__scrutinee_reconstruction.hvm.snap

@@ -6,7 +6,7 @@ input_file: tests/golden_tests/compile_file/scrutinee_reconstruction.hvm
 @8 = {4 * @A}
 @A = (a (* a))
 @None = {2 * {2 a a}}
-@Option.or = ({3 a {2 @8 {2 @7 (a b)}}} b)
+@Option.or = ({3 a {2 @8 {2 @7 (a (b c))}}} (b c))
 @Some = (a {2 {4 a b} {2 * b}})
 @main = a
 & @Option.or ~ (b (@None a))

tests/snapshots/compile_file__snd.hvm.snap

@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/snd.hvm
 ---
-@4 = ([* a] a)
 @main = a
-& @4 ~ ([#0 #42] a)
+& @snd ~ ([#0 #42] a)
+@snd = ([* a] a)
 

tests/snapshots/compile_file__sum_predicates.hvm.snap

@@ -2,13 +2,13 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/sum_predicates.hvm
 ---
-@3 = (?<(@6 @7) a> a)
-@5 = (?<(@3 @F) a> a)
 @6 = #0
 @7 = (a a)
 @A = (a a)
 @B = (a (<+ a b> b))
+@E = (?<(@6 @7) a> a)
 @F = (a (?<(@A @B) (a b)> b))
 @main = a
-& @5 ~ (#8 (#5 a))
+& @sum_pred ~ (#8 (#5 a))
+@sum_pred = (?<(@E @F) (a b)> (a b))