From 148a0e2e0371435785290a1489714d6f0520b769 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Thu, 14 Mar 2024 15:47:13 -0300
Subject: [PATCH 1/2] Change to use substitutions instead of creating let terms

---
 src/term/transform/simplify_matches.rs        | 63 ++++++++++++-------
 ...mpile_file_o_all__list_merge_sort.hvm.snap |  2 +-
 ..._file_o_all__num_pattern_with_var.hvm.snap |  5 +-
 .../desugar_file__used_once_names.hvm.snap    |  2 +-
 ...encode_pattern_match__adt_tup_era.hvm.snap |  4 +-
 .../encode_pattern_match__concat.hvm.snap     |  4 +-
 .../encode_pattern_match__concat_def.hvm.snap |  4 +-
 ...de_pattern_match__flatten_era_pat.hvm.snap | 12 ++--
 ...de_pattern_match__list_merge_sort.hvm.snap | 20 +++---
 ...de_pattern_match__match_many_args.hvm.snap | 12 ++--
 ...n_match__match_num_adt_tup_parser.hvm.snap |  8 +--
 ...ncode_pattern_match__match_syntax.hvm.snap |  4 +-
 ...ode_pattern_match__nested_let_tup.hvm.snap |  4 +-
 ...ttern_match__non_matching_fst_arg.hvm.snap |  6 +-
 .../encode_pattern_match__var_only.hvm.snap   |  6 +-
 .../simplify_matches__already_flat.hvm.snap   |  4 +-
 .../simplify_matches__bits_dec.hvm.snap       |  2 +-
 ...mplify_matches__double_unwrap_box.hvm.snap |  2 +-
 ...lify_matches__double_unwrap_maybe.hvm.snap |  2 +-
 .../simplify_matches__match_str.hvm.snap      |  2 +-
 .../simplify_matches__nested.hvm.snap         |  2 +-
 .../simplify_matches__nested2.hvm.snap        |  2 +-
 .../simplify_matches__nested_0ary.hvm.snap    |  2 +-
 ...plify_matches__redundant_with_era.hvm.snap |  2 +-
 24 files changed, 94 insertions(+), 82 deletions(-)

diff --git a/src/term/transform/simplify_matches.rs b/src/term/transform/simplify_matches.rs
index 33910a965..87b2639fc 100644
--- a/src/term/transform/simplify_matches.rs
+++ b/src/term/transform/simplify_matches.rs
@@ -30,8 +30,9 @@ impl Ctx<'_> {
 
 impl Definition {
   pub fn simplify_matches(&mut self, ctrs: &Constructors, adts: &Adts) -> Result<(), SimplifyMatchErr> {
+    let name_gen = &mut 0;
     for rule in self.rules.iter_mut() {
-      rule.body.simplify_matches(ctrs, adts)?;
+      rule.body.simplify_matches(ctrs, adts, name_gen)?;
     }
     Ok(())
   }
@@ -43,20 +44,25 @@ impl Term {
   /// simple (non-nested) patterns, and one rule for each constructor.
   ///
   /// See `[simplify_match_expression]` for more information.
-  pub fn simplify_matches(&mut self, ctrs: &Constructors, adts: &Adts) -> Result<(), SimplifyMatchErr> {
+  pub fn simplify_matches(
+    &mut self,
+    ctrs: &Constructors,
+    adts: &Adts,
+    name_gen: &mut usize,
+  ) -> Result<(), SimplifyMatchErr> {
     Term::recursive_call(move || {
       match self {
         Term::Mat { args, rules } => {
           let extracted = extract_args(args);
           let args = std::mem::take(args);
           let rules = std::mem::take(rules);
-          let term = simplify_match_expression(args, rules, ctrs, adts)?;
+          let term = simplify_match_expression(args, rules, ctrs, adts, name_gen)?;
           *self = bind_extracted_args(extracted, term);
         }
 
         _ => {
           for child in self.children_mut() {
-            child.simplify_matches(ctrs, adts)?;
+            child.simplify_matches(ctrs, adts, name_gen)?;
           }
         }
       }
@@ -92,16 +98,17 @@ fn simplify_match_expression(
   rules: Vec<Rule>,
   ctrs: &Constructors,
   adts: &Adts,
+  name_gen: &mut usize,
 ) -> Result<Term, SimplifyMatchErr> {
   let fst_row_irrefutable = rules[0].pats.iter().all(|p| p.is_wildcard());
   let fst_col_type = infer_match_arg_type(&rules, 0, ctrs)?;
 
   if fst_row_irrefutable {
-    irrefutable_fst_row_rule(args, rules, ctrs, adts)
+    irrefutable_fst_row_rule(args, rules, ctrs, adts, name_gen)
   } else if fst_col_type == Type::Any {
-    var_rule(args, rules, ctrs, adts)
+    var_rule(args, rules, ctrs, adts, name_gen)
   } else {
-    switch_rule(args, rules, fst_col_type, ctrs, adts)
+    switch_rule(args, rules, fst_col_type, ctrs, adts, name_gen)
   }
 }
 
@@ -113,17 +120,19 @@ fn irrefutable_fst_row_rule(
   mut rules: Vec<Rule>,
   ctrs: &Constructors,
   adts: &Adts,
+  name_gen: &mut usize,
 ) -> Result<Term, SimplifyMatchErr> {
   rules.truncate(1);
 
   let Rule { pats, body: mut term } = rules.pop().unwrap();
-  term.simplify_matches(ctrs, adts)?;
+  term.simplify_matches(ctrs, adts, name_gen)?;
+
+  for (pat, arg) in pats.iter().zip(args.iter()) {
+    for bind in pat.binds().flatten() {
+      term.subst(bind, arg);
+    }
+  }
 
-  let term = pats.into_iter().zip(args).fold(term, |term, (pat, arg)| Term::Let {
-    pat,
-    val: Box::new(arg),
-    nxt: Box::new(term),
-  });
   Ok(term)
 }
 
@@ -137,13 +146,17 @@ fn var_rule(
   rules: Vec<Rule>,
   ctrs: &Constructors,
   adts: &Adts,
+  name_gen: &mut usize,
 ) -> Result<Term, SimplifyMatchErr> {
   let mut new_rules = vec![];
   for mut rule in rules {
     let rest = rule.pats.split_off(1);
 
-    let body =
-      Term::Let { pat: rule.pats.pop().unwrap(), val: Box::new(args[0].clone()), nxt: Box::new(rule.body) };
+    let pat = rule.pats.pop().unwrap();
+    let mut body = rule.body;
+    if let Pattern::Var(Some(nam)) = &pat {
+      body.subst(nam, &args[0]);
+    }
 
     let new_rule = Rule { pats: rest, body };
     new_rules.push(new_rule);
@@ -151,7 +164,7 @@ fn var_rule(
 
   let rest = args.split_off(1);
   let mut term = Term::Mat { args: rest, rules: new_rules };
-  term.simplify_matches(ctrs, adts)?;
+  term.simplify_matches(ctrs, adts, name_gen)?;
   Ok(term)
 }
 
@@ -206,6 +219,7 @@ fn switch_rule(
   typ: Type,
   ctrs: &Constructors,
   adts: &Adts,
+  name_gen: &mut usize,
 ) -> Result<Term, SimplifyMatchErr> {
   let mut new_rules = vec![];
 
@@ -253,10 +267,10 @@ fn switch_rule(
   for ctr in adt_ctrs {
     // Create the matched constructor and the name of the bound variables.
     let Term::Var { nam: arg_nam } = &args[0] else { unreachable!() };
-    let nested_fields = switch_rule_nested_fields(arg_nam, &ctr);
+    let nested_fields = switch_rule_nested_fields(arg_nam, &ctr, name_gen);
     let matched_ctr = switch_rule_matched_ctr(ctr.clone(), &nested_fields);
     let mut body = switch_rule_submatch(&args, &rules, &matched_ctr, &nested_fields)?;
-    body.simplify_matches(ctrs, adts)?;
+    body.simplify_matches(ctrs, adts, name_gen)?;
     let pats = vec![matched_ctr];
     new_rules.push(Rule { pats, body });
   }
@@ -265,13 +279,14 @@ fn switch_rule(
   Ok(term)
 }
 
-fn switch_rule_nested_fields(arg_nam: &Name, ctr: &Pattern) -> Vec<Option<Name>> {
+fn switch_rule_nested_fields(arg_nam: &Name, ctr: &Pattern, name_gen: &mut usize) -> Vec<Option<Name>> {
   let mut nested_fields = vec![];
   let old_vars = ctr.binds();
   for old_var in old_vars {
+    *name_gen += 1;
     let new_nam = if let Some(field) = old_var {
       // Name of constructor field
-      Name::new(format!("{arg_nam}%{field}"))
+      Name::new(format!("{arg_nam}%{field}%{name_gen}"))
     } else {
       // Name of var pattern
       arg_nam.clone()
@@ -347,13 +362,15 @@ fn switch_rule_submatch_arm(rule: &Rule, ctr: &Pattern, nested_fields: &[Option<
     //     x%field0 ...: let var = (Ctr x%field0 ...); Body;
     //   ... };
     // ... }
+    let mut body = rule.body.clone();
+    if let Pattern::Var(Some(nam)) = &rule.pats[0] {
+      body.subst(nam, &ctr.to_term());
+    }
+
     let nested_var_pats = nested_fields.iter().cloned().map(Pattern::Var);
     let old_pats = rule.pats[1 ..].iter().cloned();
     let pats = nested_var_pats.chain(old_pats).collect_vec();
 
-    let body =
-      Term::Let { pat: rule.pats[0].clone(), val: Box::new(ctr.to_term()), nxt: Box::new(rule.body.clone()) };
-
     Some(Rule { pats, body })
   } else {
     // Non-matching constructor. Don't include in submatch expression.
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 6c3946472..7b4b25121 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
@@ -7,7 +7,7 @@ input_file: tests/golden_tests/compile_file_o_all/list_merge_sort.hvm
 @If$C1 = (* (a a))
 @Map = ({4 @Map$C0 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 a}} a)
 @Map$C0 = {4 a {4 {4 @Map$C0 {4 @Unpack$C3_$_MergePair$C4_$_Map$C1 (b c)}} ({5 (a d) b} {4 {4 d {4 c e}} {4 * e}})}}
-@Merge$C0 = {4 {9 a {9 b c}} {4 {7 d {4 @Merge$C0 {4 @Merge$C1 (e (f (g h)))}}} ({15 (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))}})) {15 o e}} ({13 i {13 j f}} ({11 {4 @Merge$C2 {4 @Merge$C3 (o ({4 {4 b {4 d p}} {4 * p}} k))}} g} n)))}}
+@Merge$C0 = {4 {7 a {7 b c}} {4 {9 d {4 @Merge$C0 {4 @Merge$C1 (e (f (g h)))}}} ({11 (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))}})) {11 o e}} ({13 i {13 j f}} ({15 {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))
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 66198c5c3..6dcae01fa 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,8 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file_o_all/num_pattern_with_var.hvm
 ---
-@Foo = ({2 (* #0) {2 @Foo$C3 a}} a)
-@Foo$C2 = (a (* a))
-@Foo$C3 = (?<((* #0) @Foo$C2) (* a)> a)
+@Foo = ({2 (* #0) {2 @Foo$C1 a}} a)
+@Foo$C1 = (?<(#0 (a a)) b> b)
 @main = a
 & @Foo ~ (@true (#3 a))
 @true = {2 * {2 a a}}
diff --git a/tests/snapshots/desugar_file__used_once_names.hvm.snap b/tests/snapshots/desugar_file__used_once_names.hvm.snap
index 3ba67acbe..8db53571c 100644
--- a/tests/snapshots/desugar_file__used_once_names.hvm.snap
+++ b/tests/snapshots/desugar_file__used_once_names.hvm.snap
@@ -2,6 +2,6 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/desugar_file/used_once_names.hvm
 ---
-(foo) = λa λb λc let {d d_2} = c; (a b (d d_2))
+(foo) = λa λb λc let {c c_2} = c; (a b (c c_2))
 
 (main) = (foo 2 3 λa a)
diff --git a/tests/snapshots/encode_pattern_match__adt_tup_era.hvm.snap b/tests/snapshots/encode_pattern_match__adt_tup_era.hvm.snap
index e069a47bf..5284d3eb1 100644
--- a/tests/snapshots/encode_pattern_match__adt_tup_era.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__adt_tup_era.hvm.snap
@@ -3,14 +3,14 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/adt_tup_era.hvm
 ---
 TaggedScott:
-(Foo) = λa #Tuple (a #Tuple λb #Tuple λc (#Tuple (b #Tuple λd #Tuple λ* λ* d) c))
+(Foo) = λa #Tuple (a #Tuple λb #Tuple λ* #Tuple (b #Tuple λd #Tuple λ* d))
 
 (Main) = (Foo (Pair 1 5))
 
 (Pair) = λa λb #Tuple λc #Tuple (c a b)
 
 Scott:
-(Foo) = λa (a λb λc (b λd λ* λ* d c))
+(Foo) = λa (a λb λ* (b λd λ* d))
 
 (Main) = (Foo (Pair 1 5))
 
diff --git a/tests/snapshots/encode_pattern_match__concat.hvm.snap b/tests/snapshots/encode_pattern_match__concat.hvm.snap
index 671f8e692..65f1cc338 100644
--- a/tests/snapshots/encode_pattern_match__concat.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__concat.hvm.snap
@@ -3,7 +3,7 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/concat.hvm
 ---
 TaggedScott:
-(String.concat) = λa λb (#String (a #String λc #String λd λe (String.cons c (String.concat d e)) λh h) b)
+(String.concat) = λa λb (#String (a #String λc #String λd λe (String.cons c (String.concat d e)) λf f) b)
 
 (main) = (String.concat (String.cons 97 (String.cons 98 String.nil)) (String.cons 99 (String.cons 100 String.nil)))
 
@@ -12,7 +12,7 @@ TaggedScott:
 (String.nil) = #String λ* #String λb b
 
 Scott:
-(String.concat) = λa λb (a λc λd λe (String.cons c (String.concat d e)) λh h b)
+(String.concat) = λa λb (a λc λd λe (String.cons c (String.concat d e)) λf f b)
 
 (main) = (String.concat (String.cons 97 (String.cons 98 String.nil)) (String.cons 99 (String.cons 100 String.nil)))
 
diff --git a/tests/snapshots/encode_pattern_match__concat_def.hvm.snap b/tests/snapshots/encode_pattern_match__concat_def.hvm.snap
index bb5ef90ea..48e855176 100644
--- a/tests/snapshots/encode_pattern_match__concat_def.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__concat_def.hvm.snap
@@ -3,7 +3,7 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/concat_def.hvm
 ---
 TaggedScott:
-(concat) = λa λb (#String (a #String λc #String λd λe (String.cons c (concat d e)) λi i) b)
+(concat) = λa λb (#String (a #String λc #String λd λe (String.cons c (concat d e)) λf f) b)
 
 (main) = (concat (String.cons 97 (String.cons 98 String.nil)) (String.cons 99 (String.cons 100 String.nil)))
 
@@ -12,7 +12,7 @@ TaggedScott:
 (String.nil) = #String λ* #String λb b
 
 Scott:
-(concat) = λa λb (a λc λd λe (String.cons c (concat d e)) λi i b)
+(concat) = λa λb (a λc λd λe (String.cons c (concat d e)) λf f b)
 
 (main) = (concat (String.cons 97 (String.cons 98 String.nil)) (String.cons 99 (String.cons 100 String.nil)))
 
diff --git a/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap b/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap
index 992385330..8f341af14 100644
--- a/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap
@@ -3,19 +3,19 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/flatten_era_pat.hvm
 ---
 TaggedScott:
-(Fn1) = λa λb (let (c, d) = a; λe (let (f, *) = d; λ* λ* f c e) b)
+(Fn1) = λa λ* let (*, d) = a; let (e, *) = d; e
 
-(Fn2) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, *) = e; λ* λ* g f d) b)
+(Fn2) = λa let (*, c) = a; let (*, e) = c; let (f, *) = e; f
 
-(Fn3) = λa λb (let (c, d) = a; λe (match c { 0: λ* λ* 0; 1+: λi λ* λ* i } d e) b)
+(Fn3) = λa λ* let (c, *) = a; match c { 0: 0; 1+: λf f }
 
 (main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0)
 
 Scott:
-(Fn1) = λa λb (let (c, d) = a; λe (let (f, *) = d; λ* λ* f c e) b)
+(Fn1) = λa λ* let (*, d) = a; let (e, *) = d; e
 
-(Fn2) = λa let (b, c) = a; (let (d, e) = c; λf (let (g, *) = e; λ* λ* g f d) b)
+(Fn2) = λa let (*, c) = a; let (*, e) = c; let (f, *) = e; f
 
-(Fn3) = λa λb (let (c, d) = a; λe (match c { 0: λ* λ* 0; 1+: λi λ* λ* i } d e) b)
+(Fn3) = λa λ* let (c, *) = a; match c { 0: 0; 1+: λf f }
 
 (main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0)
diff --git a/tests/snapshots/encode_pattern_match__list_merge_sort.hvm.snap b/tests/snapshots/encode_pattern_match__list_merge_sort.hvm.snap
index e2ead7b63..eb5dc0ba4 100644
--- a/tests/snapshots/encode_pattern_match__list_merge_sort.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__list_merge_sort.hvm.snap
@@ -3,19 +3,19 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/list_merge_sort.hvm
 ---
 TaggedScott:
-(If) = λa λb λc (#Bool (a λd λ* d λ* λj j) b c)
+(If) = λa λb λc (#Bool (a λd λ* d λ* λh h) b c)
 
 (Pure) = λa (Cons a Nil)
 
-(Map) = λa λb (#List_ (a #List_ λc #List_ λd λe let {f f_2} = e; (Cons (f c) (Map d f_2)) λ* Nil) b)
+(Map) = λa λb (#List_ (a #List_ λc #List_ λd λe let {e e_2} = e; (Cons (e c) (Map d e_2)) λ* Nil) b)
 
 (MergeSort) = λa λb (Unpack a (Map b Pure))
 
-(Unpack) = λa λb (#List_ (b #List_ λc #List_ λd λe (#List_ (d #List_ λf #List_ λg λh λi let {o o_2} = h; (Unpack o (MergePair o_2 (Cons i (Cons f g)))) λ* λq q) e c) λ* Nil) a)
+(Unpack) = λa λb (#List_ (b #List_ λc #List_ λd λe (#List_ (d #List_ λf #List_ λg λh let {h h_2} = h; λi (Unpack h (MergePair h_2 (Cons i (Cons f g)))) λ* λk k) e c) λ* Nil) a)
 
-(MergePair) = λa λb (#List_ (b #List_ λc #List_ λd λe (#List_ (d #List_ λf #List_ λg λh λi let {m m_2} = h; (Cons (Merge m i f) (MergePair m_2 g)) λ* λo (Cons o Nil)) e c) λ* Nil) a)
+(MergePair) = λa λb (#List_ (b #List_ λc #List_ λd λe (#List_ (d #List_ λf #List_ λg λh let {h h_2} = h; λi (Cons (Merge h i f) (MergePair h_2 g)) λ* λk (Cons k Nil)) e c) λ* Nil) a)
 
-(Merge) = λa λb λc (#List_ (b #List_ λd #List_ λe λf λg (#List_ (g #List_ λh #List_ λi λj λk λl let {m m_2} = i; let {n n_2 n_3} = h; let {o o_2} = l; let {p p_2 p_3} = k; let {q q_2 q_3} = j; (If (q p n) (Cons p_2 (Merge q_2 o (Cons n_2 m))) (Cons n_3 (Merge q_3 (Cons p_3 o_2) m_2))) λ* λu λv (Cons u v)) f d e) λ* λcb cb) a c)
+(Merge) = λa λb λc (#List_ (b #List_ λd #List_ λe λf λg (#List_ (g #List_ λh let {h h_2 h_3} = h; #List_ λi let {i i_2} = i; λj let {j j_2 j_3} = j; λk let {k k_2 k_3} = k; λl let {l l_2} = l; (If (j k h) (Cons k_2 (Merge j_2 l (Cons h_2 i))) (Cons h_3 (Merge j_3 (Cons k_3 l_2) i_2))) λ* λp λq (Cons p q)) f d e) λ* λt t) a c)
 
 (Nil) = #List_ λ* #List_ λb b
 
@@ -26,19 +26,19 @@ TaggedScott:
 (True) = #Bool λa #Bool λ* a
 
 Scott:
-(If) = λa λb λc (a λd λ* d λ* λj j b c)
+(If) = λa λb λc (a λd λ* d λ* λh h b c)
 
 (Pure) = λa (Cons a Nil)
 
-(Map) = λa λb (a λc λd λe let {f f_2} = e; (Cons (f c) (Map d f_2)) λ* Nil b)
+(Map) = λa λb (a λc λd λe let {e e_2} = e; (Cons (e c) (Map d e_2)) λ* Nil b)
 
 (MergeSort) = λa λb (Unpack a (Map b Pure))
 
-(Unpack) = λa λb (b λc λd λe (d λf λg λh λi let {o o_2} = h; (Unpack o (MergePair o_2 (Cons i (Cons f g)))) λ* λq q e c) λ* Nil a)
+(Unpack) = λa λb (b λc λd λe (d λf λg λh let {h h_2} = h; λi (Unpack h (MergePair h_2 (Cons i (Cons f g)))) λ* λk k e c) λ* Nil a)
 
-(MergePair) = λa λb (b λc λd λe (d λf λg λh λi let {m m_2} = h; (Cons (Merge m i f) (MergePair m_2 g)) λ* λo (Cons o Nil) e c) λ* Nil a)
+(MergePair) = λa λb (b λc λd λe (d λf λg λh let {h h_2} = h; λi (Cons (Merge h i f) (MergePair h_2 g)) λ* λk (Cons k Nil) e c) λ* Nil a)
 
-(Merge) = λa λb λc (b λd λe λf λg (g λh λi λj λk λl let {m m_2} = i; let {n n_2 n_3} = h; let {o o_2} = l; let {p p_2 p_3} = k; let {q q_2 q_3} = j; (If (q p n) (Cons p_2 (Merge q_2 o (Cons n_2 m))) (Cons n_3 (Merge q_3 (Cons p_3 o_2) m_2))) λ* λu λv (Cons u v) f d e) λ* λcb cb a c)
+(Merge) = λa λb λc (b λd λe λf λg (g λh let {h h_2 h_3} = h; λi let {i i_2} = i; λj let {j j_2 j_3} = j; λk let {k k_2 k_3} = k; λl let {l l_2} = l; (If (j k h) (Cons k_2 (Merge j_2 l (Cons h_2 i))) (Cons h_3 (Merge j_3 (Cons k_3 l_2) i_2))) λ* λp λq (Cons p q) f d e) λ* λt t a c)
 
 (Nil) = λ* λb b
 
diff --git a/tests/snapshots/encode_pattern_match__match_many_args.hvm.snap b/tests/snapshots/encode_pattern_match__match_many_args.hvm.snap
index 2b2d07822..848922354 100644
--- a/tests/snapshots/encode_pattern_match__match_many_args.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__match_many_args.hvm.snap
@@ -3,11 +3,11 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/match_many_args.hvm
 ---
 TaggedScott:
-(tail_tail) = λa #L (a #L λb #L λc (#L (c #L λ* #L λe λ* e λ* N) b) N)
+(tail_tail) = λa #L (a #L λ* #L λc #L (c #L λ* #L λe e N) N)
 
-(or) = λa λb (#Option (b #Option λc λ* c λf f) a)
+(or) = λa λb (#Option (b #Option λc λ* c λe e) a)
 
-(or2) = λa λb (#Option (a #Option λc λ* c λf f) b)
+(or2) = λa λb (#Option (a #Option λc λ* c λe e) b)
 
 (map) = λa λb (#Option (b #Option λc λd (d c) λ* None) a)
 
@@ -28,11 +28,11 @@ TaggedScott:
 (C) = λa λb #L λc #L λ* #L (c a b)
 
 Scott:
-(tail_tail) = λa (a λb λc (c λ* λe λ* e λ* N b) N)
+(tail_tail) = λa (a λ* λc (c λ* λe e N) N)
 
-(or) = λa λb (b λc λ* c λf f a)
+(or) = λa λb (b λc λ* c λe e a)
 
-(or2) = λa λb (a λc λ* c λf f b)
+(or2) = λa λb (a λc λ* c λe e b)
 
 (map) = λa λb (b λc λd (d c) λ* None a)
 
diff --git a/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap b/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap
index 1ec133c10..66659352b 100644
--- a/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__match_num_adt_tup_parser.hvm.snap
@@ -3,9 +3,9 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/match_num_adt_tup_parser.hvm
 ---
 TaggedScott:
-(Parse) = λa λb (#String (b #String λc #String λd λe (match (- c 40) { 0: λf λg (Ok (40, g, f)); 1+: λk match k { 0: λl λm (Ok (41, m, l)); 1+: λq match (- q 18446744073709551584) { 0: λr λs (Ok (0, s, r)); 1+: λw λy λz (Err ((String.cons (+ w 11) z), y)) } } } e d) λeb (Err (String.nil, eb))) a)
+(Parse) = λa λb (#String (b #String λc #String λd λe (match (- c 40) { 0: λf λg (Ok (40, g, f)); 1+: λi match i { 0: λj λk (Ok (41, k, j)); 1+: λm match (- m 18446744073709551584) { 0: λn λo (Ok (0, o, n)); 1+: λq λs λt (Err ((String.cons (+ q 11) t), s)) } } } e d) λu (Err (String.nil, u))) a)
 
-(main) = #Result ((Parse * (String.cons 40 (String.cons 43 String.nil))) #Result λd let (e, f, g) = d; (e, (Parse g f)) #Result λk (Err k))
+(main) = #Result ((Parse * (String.cons 40 (String.cons 43 String.nil))) #Result λd let (e, f, g) = d; (e, (Parse g f)) #Result λh (Err h))
 
 (String.cons) = λa λb #String λc #String λ* #String (c a b)
 
@@ -16,9 +16,9 @@ TaggedScott:
 (Ok) = λa #Result λb #Result λ* #Result (b a)
 
 Scott:
-(Parse) = λa λb (b λc λd λe (match (- c 40) { 0: λf λg (Ok (40, g, f)); 1+: λk match k { 0: λl λm (Ok (41, m, l)); 1+: λq match (- q 18446744073709551584) { 0: λr λs (Ok (0, s, r)); 1+: λw λy λz (Err ((String.cons (+ w 11) z), y)) } } } e d) λeb (Err (String.nil, eb)) a)
+(Parse) = λa λb (b λc λd λe (match (- c 40) { 0: λf λg (Ok (40, g, f)); 1+: λi match i { 0: λj λk (Ok (41, k, j)); 1+: λm match (- m 18446744073709551584) { 0: λn λo (Ok (0, o, n)); 1+: λq λs λt (Err ((String.cons (+ q 11) t), s)) } } } e d) λu (Err (String.nil, u)) a)
 
-(main) = (Parse * (String.cons 40 (String.cons 43 String.nil)) λd let (e, f, g) = d; (e, (Parse g f)) λk (Err k))
+(main) = (Parse * (String.cons 40 (String.cons 43 String.nil)) λd let (e, f, g) = d; (e, (Parse g f)) λh (Err h))
 
 (String.cons) = λa λb λc λ* (c a b)
 
diff --git a/tests/snapshots/encode_pattern_match__match_syntax.hvm.snap b/tests/snapshots/encode_pattern_match__match_syntax.hvm.snap
index 0a19946e9..19fb245e1 100644
--- a/tests/snapshots/encode_pattern_match__match_syntax.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__match_syntax.hvm.snap
@@ -3,14 +3,14 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/match_syntax.hvm
 ---
 TaggedScott:
-(head) = λa #List_ (a #List_ λc #List_ λ* c Nil)
+(head) = λa #List_ (a #List_ λb #List_ λ* b Nil)
 
 (Nil) = #List_ λ* #List_ λb b
 
 (Cons) = λa λb #List_ λc #List_ λ* #List_ (c a b)
 
 Scott:
-(head) = λa (a λc λ* c Nil)
+(head) = λa (a λb λ* b Nil)
 
 (Nil) = λ* λb b
 
diff --git a/tests/snapshots/encode_pattern_match__nested_let_tup.hvm.snap b/tests/snapshots/encode_pattern_match__nested_let_tup.hvm.snap
index ce13f20ac..4e4f17b96 100644
--- a/tests/snapshots/encode_pattern_match__nested_let_tup.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__nested_let_tup.hvm.snap
@@ -3,7 +3,7 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/nested_let_tup.hvm
 ---
 TaggedScott:
-(main) = let (k, l) = let (b, c) = (10, ((1, ((2, 3), 4)), 3)); (let (d, *) = c; λ* d b); (let (m, *) = l; λ* let (s, *) = m; s k)
+(main) = let (*, h) = let (*, c) = (10, ((1, ((2, 3), 4)), 3)); let (d, *) = c; d; let (i, *) = h; let (k, *) = i; k
 
 Scott:
-(main) = let (k, l) = let (b, c) = (10, ((1, ((2, 3), 4)), 3)); (let (d, *) = c; λ* d b); (let (m, *) = l; λ* let (s, *) = m; s k)
+(main) = let (*, h) = let (*, c) = (10, ((1, ((2, 3), 4)), 3)); let (d, *) = c; d; let (i, *) = h; let (k, *) = i; k
diff --git a/tests/snapshots/encode_pattern_match__non_matching_fst_arg.hvm.snap b/tests/snapshots/encode_pattern_match__non_matching_fst_arg.hvm.snap
index c17a1a7d7..4c1bb6e48 100644
--- a/tests/snapshots/encode_pattern_match__non_matching_fst_arg.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__non_matching_fst_arg.hvm.snap
@@ -3,17 +3,15 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/non_matching_fst_arg.hvm
 ---
 TaggedScott:
-(Foo) = λa λb (#bool (b λc let {e e_2} = c; (Foo e e_2) λf f) a)
+(Foo) = λa λb (#bool (b λc let {c c_2} = c; (Foo c c_2) λe e) a)
 
 (false) = #bool λ* #bool λb b
 
 (true) = #bool λa #bool λ* a
 
 Scott:
-(Foo) = λa λb (b λc let {e e_2} = c; (Foo e e_2) λf f a)
+(Foo) = λa λb (b λc let {c c_2} = c; (Foo c c_2) λe e a)
 
 (false) = λ* λb b
 
 (true) = λa λ* a
-
-
diff --git a/tests/snapshots/encode_pattern_match__var_only.hvm.snap b/tests/snapshots/encode_pattern_match__var_only.hvm.snap
index 48311a45b..4751aae26 100644
--- a/tests/snapshots/encode_pattern_match__var_only.hvm.snap
+++ b/tests/snapshots/encode_pattern_match__var_only.hvm.snap
@@ -3,7 +3,7 @@ source: tests/golden_tests.rs
 input_file: tests/golden_tests/encode_pattern_match/var_only.hvm
 ---
 TaggedScott:
-(Foo) = λa λ* λe (e a)
+(Foo) = λa λ* λc (c a)
 
 (main) = λ* Foo
 
@@ -12,12 +12,10 @@ TaggedScott:
 (False) = #Bool λa #Bool λ* a
 
 Scott:
-(Foo) = λa λ* λe (e a)
+(Foo) = λa λ* λc (c a)
 
 (main) = λ* Foo
 
 (True) = λ* λb b
 
 (False) = λa λ* a
-
-
diff --git a/tests/snapshots/simplify_matches__already_flat.hvm.snap b/tests/snapshots/simplify_matches__already_flat.hvm.snap
index c0aa8b533..46a8bf659 100644
--- a/tests/snapshots/simplify_matches__already_flat.hvm.snap
+++ b/tests/snapshots/simplify_matches__already_flat.hvm.snap
@@ -4,13 +4,13 @@ input_file: tests/golden_tests/simplify_matches/already_flat.hvm
 ---
 (Rule1) = λa a
 
-(Rule2) = λ* λc c
+(Rule2) = λ* λb b
 
 (Rule3) = λa λb λc λd (a b c d)
 
 (Rule4) = λa match a { (CtrA): λc c; (CtrB d): d }
 
-(Rule5) = λa λb (match a { (CtrA1 c): λd (c d); (CtrA2 g h): λi (g h i); (CtrA3 m): λn (match n { (CtrB0): λo (CtrA3 o); (CtrB1 s): λt (CtrA3 t s); (CtrB2 x): λy (CtrA3 y (CtrB2 x)); (CtrB3 db): λeb (eb db) } m) } b)
+(Rule5) = λa λb (match a { (CtrA1 c): λd (c d); (CtrA2 e f): λg (e f g); (CtrA3 h): λi (match i { (CtrB0): λj (CtrA3 j); (CtrB1 l): λm (CtrA3 m l); (CtrB2 n): λo (CtrA3 o (CtrB2 n)); (CtrB3 p): λq (q p) } h) } b)
 
 (Rule6) = λa a
 
diff --git a/tests/snapshots/simplify_matches__bits_dec.hvm.snap b/tests/snapshots/simplify_matches__bits_dec.hvm.snap
index 62f716ff4..8b024f424 100644
--- a/tests/snapshots/simplify_matches__bits_dec.hvm.snap
+++ b/tests/snapshots/simplify_matches__bits_dec.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/bits_dec.hvm
 ---
-(Data.Bits.dec) = λa match a { (Data.Bits.e): Data.Bits.e; (Data.Bits.o c): match c { (Data.Bits.e): Data.Bits.e; (Data.Bits.o e): (Data.Bits.i (Data.Bits.dec e)); (Data.Bits.i g): (Data.Bits.i (Data.Bits.dec g)) }; (Data.Bits.i i): match i { (Data.Bits.e): (Data.Bits.o Data.Bits.e); (Data.Bits.o k): (Data.Bits.o k); (Data.Bits.i m): (Data.Bits.o m) } }
+(Data.Bits.dec) = λa match a { (Data.Bits.e): Data.Bits.e; (Data.Bits.o c): match c { (Data.Bits.e): Data.Bits.e; (Data.Bits.o e): (Data.Bits.i (Data.Bits.dec e)); (Data.Bits.i f): (Data.Bits.i (Data.Bits.dec f)) }; (Data.Bits.i g): match g { (Data.Bits.e): (Data.Bits.o Data.Bits.e); (Data.Bits.o i): (Data.Bits.o i); (Data.Bits.i j): (Data.Bits.o j) } }
 
 (Data.Bits.i) = λa #Data.Bits λ* #Data.Bits λ* #Data.Bits λd #Data.Bits (d a)
 
diff --git a/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap b/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap
index 2acd10427..8162ac24b 100644
--- a/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap
+++ b/tests/snapshots/simplify_matches__double_unwrap_box.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/double_unwrap_box.hvm
 ---
-(DoubleUnbox) = λa λb (match a { (Box c): λd (match c { (Box e): λ* e } d) } b)
+(DoubleUnbox) = λa λ* match a { (Box c): match c { (Box d): d } }
 
 (Main) = (DoubleUnbox (Box (Box 0)) 5)
 
diff --git a/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap b/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap
index 07040aa2d..bbaa9329f 100644
--- a/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap
+++ b/tests/snapshots/simplify_matches__double_unwrap_maybe.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/double_unwrap_maybe.hvm
 ---
-(DoubleUnwrap) = λa λb (match a { (Some c): λd (match c { (Some e): λ* e; (None): λh h } d); (None): λl l } b)
+(DoubleUnwrap) = λa λb (match a { (Some c): λd (match c { (Some e): λ* e; (None): λg g } d); (None): λi i } b)
 
 (Main) = (DoubleUnwrap (Some None) 5)
 
diff --git a/tests/snapshots/simplify_matches__match_str.hvm.snap b/tests/snapshots/simplify_matches__match_str.hvm.snap
index a88f78f14..12f4c553b 100644
--- a/tests/snapshots/simplify_matches__match_str.hvm.snap
+++ b/tests/snapshots/simplify_matches__match_str.hvm.snap
@@ -2,6 +2,6 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/match_str.hvm
 ---
-(is_as) = λa match a { (String.cons b c): (match b { 65: λd (match d { (String.cons f g): λh (match f { 115: λ* λj (match j { (String.cons * *): λ* 0; (String.nil): λ* 2 } *); *: λ* λ* 0 } h g); (String.nil): λ* 0 } *); 97: λhb (match hb { (String.cons jb kb): λlb (match jb { 115: λ* λnb (match nb { (String.cons * *): λ* 0; (String.nil): λ* 2 } *); *: λ* λ* 0 } lb kb); (String.nil): λ* 0 } *); *: λ* 0 } c); (String.nil): 1 }
+(is_as) = λa match a { (String.cons b c): (match b { 65: λd match d { (String.cons f g): (match f { 115: λh match h { (String.cons * *): 0; (String.nil): 2 }; *: λ* 0 } g); (String.nil): 0 }; 97: λp match p { (String.cons r s): (match r { 115: λt match t { (String.cons * *): 0; (String.nil): 2 }; *: λ* 0 } s); (String.nil): 0 }; *: λ* 0 } c); (String.nil): 1 }
 
 (main) = *
diff --git a/tests/snapshots/simplify_matches__nested.hvm.snap b/tests/snapshots/simplify_matches__nested.hvm.snap
index 7d1350cd0..05498d595 100644
--- a/tests/snapshots/simplify_matches__nested.hvm.snap
+++ b/tests/snapshots/simplify_matches__nested.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/nested.hvm
 ---
-(Rule) = λa match a { (CtrA b c): (match c { (CtrB1 d): λe (e d); (CtrB2 h i): λj (match h { (CtrC): λk λl (k l) } j i) } b); (CtrB p): p }
+(Rule) = λa match a { (CtrA b c): (match c { (CtrB1 d): λe (e d); (CtrB2 f g): λh (match f { (CtrC): λi λj (i j) } h g) } b); (CtrB l): l }
 
 (CtrC) = #Baz λa a
 
diff --git a/tests/snapshots/simplify_matches__nested2.hvm.snap b/tests/snapshots/simplify_matches__nested2.hvm.snap
index c7cf32d3d..3ca3b9d15 100644
--- a/tests/snapshots/simplify_matches__nested2.hvm.snap
+++ b/tests/snapshots/simplify_matches__nested2.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/nested2.hvm
 ---
-(Foo) = λa λb (match b { (List.cons c d): λe (match d { (List.cons f g): λh λi (h i f g); (List.nil): λn λo (n (List.cons o List.nil)) } e c); (List.nil): λu (u List.nil) } a)
+(Foo) = λa λb (match b { (List.cons c d): λe (match d { (List.cons f g): λh λi (h i f g); (List.nil): λj λk (j (List.cons k List.nil)) } e c); (List.nil): λm (m List.nil) } a)
 
 (List.nil) = #List λ* #List λb b
 
diff --git a/tests/snapshots/simplify_matches__nested_0ary.hvm.snap b/tests/snapshots/simplify_matches__nested_0ary.hvm.snap
index 461b17c92..724e58121 100644
--- a/tests/snapshots/simplify_matches__nested_0ary.hvm.snap
+++ b/tests/snapshots/simplify_matches__nested_0ary.hvm.snap
@@ -2,7 +2,7 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/nested_0ary.hvm
 ---
-(Unpack) = λa λb (match b { (Cons c d): λe (match d { (Cons f g): λh λi (h (Cons i (Cons f g))); (Nil): λ* λq q } e c); (Nil): λ* Nil } a)
+(Unpack) = λa λb (match b { (Cons c d): λe (match d { (Cons f g): λh λi (h (Cons i (Cons f g))); (Nil): λ* λk k } e c); (Nil): λ* Nil } a)
 
 (Nil) = #list λ* #list λb b
 
diff --git a/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap b/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap
index fc5b56eef..e7c9c75b2 100644
--- a/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap
+++ b/tests/snapshots/simplify_matches__redundant_with_era.hvm.snap
@@ -2,6 +2,6 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/simplify_matches/redundant_with_era.hvm
 ---
-(Fn2) = λa λb (match a { 0: λc (match c { (e, f): λg (match f { (*, i): λ* λ* i } g e) } *); 1+m: λn (match n { (o, p): λq (match p { (*, s): λ* λ* s } q o) } m) } b)
+(Fn2) = λa λb (match a { 0: λc match c { (*, f): match f { (*, h): h } }; 1+*: λj match j { (*, l): match l { (*, n): n } } } b)
 
 (main) = *

From 87c5cd05e670c19f0e2758a9023cd0cb3c924da8 Mon Sep 17 00:00:00 2001
From: imaqtkatt <eduarda.so@proton.me>
Date: Fri, 15 Mar 2024 10:08:47 -0300
Subject: [PATCH 2/2] Update simplify matches comments

---
 src/term/transform/simplify_matches.rs | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

diff --git a/src/term/transform/simplify_matches.rs b/src/term/transform/simplify_matches.rs
index 87b2639fc..880f2b88c 100644
--- a/src/term/transform/simplify_matches.rs
+++ b/src/term/transform/simplify_matches.rs
@@ -18,9 +18,10 @@ pub enum SimplifyMatchErr {
 impl Ctx<'_> {
   pub fn simplify_matches(&mut self) -> Result<(), Diagnostics> {
     self.info.start_pass();
+    let name_gen = &mut 0;
 
     for (def_name, def) in self.book.defs.iter_mut() {
-      let res = def.simplify_matches(&self.book.ctrs, &self.book.adts);
+      let res = def.simplify_matches(&self.book.ctrs, &self.book.adts, name_gen);
       self.info.take_rule_err(res, def_name.clone());
     }
 
@@ -29,8 +30,12 @@ impl Ctx<'_> {
 }
 
 impl Definition {
-  pub fn simplify_matches(&mut self, ctrs: &Constructors, adts: &Adts) -> Result<(), SimplifyMatchErr> {
-    let name_gen = &mut 0;
+  pub fn simplify_matches(
+    &mut self,
+    ctrs: &Constructors,
+    adts: &Adts,
+    name_gen: &mut usize,
+  ) -> Result<(), SimplifyMatchErr> {
     for rule in self.rules.iter_mut() {
       rule.body.simplify_matches(ctrs, adts, name_gen)?;
     }
@@ -43,6 +48,9 @@ impl Term {
   /// arbitrary patterns into matches on a single value, with only
   /// simple (non-nested) patterns, and one rule for each constructor.
   ///
+  /// The `name_gen` is used to generate fresh variable names for
+  /// substitution to avoid name clashes.
+  ///
   /// See `[simplify_match_expression]` for more information.
   pub fn simplify_matches(
     &mut self,
@@ -354,14 +362,8 @@ fn switch_rule_submatch_arm(rule: &Rule, ctr: &Pattern, nested_fields: &[Option<
     let body = rule.body.clone();
     Some(Rule { pats, body })
   } else if rule.pats[0].is_wildcard() {
-    // Var, reconstruct the value matched in the expression above.
-    // match x ... {var ...: Body; ...}
-    // becomes
-    // match x {
-    //   (Ctr x%field0 ...): match x1 ... {
-    //     x%field0 ...: let var = (Ctr x%field0 ...); Body;
-    //   ... };
-    // ... }
+    // Use `subst` to replace the pattern variable in the body
+    // of the rule with the term that represents the matched constructor.
     let mut body = rule.body.clone();
     if let Pattern::Var(Some(nam)) = &rule.pats[0] {
       body.subst(nam, &ctr.to_term());