[sc-383] Implement flattening with Era pats

src/term/transform/flatten.rs

@@ -88,7 +88,6 @@ fn split_group(rules: &[(Name, Rule)], def_names: &mut DefNames) -> HashMap<Name
         let old_rule = make_old_rule(&rule.pats, new_split_def_id);
 
         let mut new_group = vec![(name.clone(), old_rule)];
-        //let mut new_group = vec![];
 
         for (j, (_, other)) in rules.iter().enumerate().skip(i) {
           let (compatible, same_shape) = matches_together(&rule.pats, &other.pats);
@@ -151,7 +150,9 @@ fn make_old_rule(pats: &[Pattern], new_split_def_id: DefId) -> Rule {
         let snd = Pattern::Var(Some(snd));
         new_pats.push(Pattern::Tup(Box::new(fst), Box::new(snd)));
       }
-      Pattern::Var(None) => todo!(),
+      Pattern::Var(None) => {
+        new_pats.push(Pattern::Var(None));
+      }
       Pattern::Var(Some(nam)) => {
         new_pats.push(Pattern::Var(Some(nam.clone())));
         new_body_args.push(Term::Var { nam: nam.clone() });
@@ -213,7 +214,8 @@ fn make_split_rule(old_rule: &Rule, other_rule: &Rule, def_names: &DefNames) ->
         let new_ctr = Term::Tup { fst: Box::new(fst_arg), snd: Box::new(snd_arg) };
         new_body.subst(other_arg, &new_ctr);
       }
-      (Pattern::Var(..), _) => new_pats.push(other_arg.clone()),
+      (Pattern::Var(Some(_)), _) => new_pats.push(other_arg.clone()),
+      (Pattern::Var(None), _) => (),
       // Unreachable cases, we only call this function if we know the two patterns match together
       (Pattern::Ctr(..) | Pattern::Tup(..), Pattern::Ctr(..) | Pattern::Num(..) | Pattern::Tup(..)) => {
         unreachable!()

tests/golden_tests/encode_pattern_match/flatten_era_pat.hvm

@@ -0,0 +1,9 @@
+// To check that flattening works with Era patterns.
+(Fn1 (*,(a,*)) *) = a
+
+(Fn2 (*,(*,(a,*)))) = a
+
+(Fn3 (0,*) *) = 0
+(Fn3 (+a,*) *) = a
+
+main = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0)

tests/snapshots/encode_pattern_match__flatten_era_pat.hvm.snap

@@ -0,0 +1,57 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/encode_pattern_match/flatten_era_pat.hvm
+---
+(Fn1) = λx (Fn1$P x)
+
+(Fn2) = λx (Fn2$P x)
+
+(Fn3) = λx (Fn3$P x)
+
+(main) = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0)
+
+(Fn1$F0) = λx (Fn1$F0$P x)
+
+(Fn2$F0) = λx (Fn2$F0$P x)
+
+(Fn2$F0$F0) = λx (Fn2$F0$F0$P x)
+
+(Fn3$F0) = λx match x { 0: Fn3$F0$P0; +: Fn3$F0$P+ }
+
+(Fn1$R0) = λ%0 let (x$0, x$1) = %0; λ* (Fn1$F0 x$0 x$1)
+
+(Fn1$P) = λy0 (Fn1$R0 y0)
+
+(Fn2$R0) = λ%0 let (x$0, x$1) = %0; (Fn2$F0 x$0 x$1)
+
+(Fn2$P) = λy0 (Fn2$R0 y0)
+
+(Fn3$R0) = λ%0 let (x$0, x$1) = %0; λ* (Fn3$F0 x$0 x$1)
+
+(Fn3$P) = λy0 (Fn3$R0 y0)
+
+(Fn1$F0$R0) = λ* λ%0 let (a, *) = %0; a
+
+(Fn1$F0$P$P) = λy0 λx0 (Fn1$F0$R0 * y0)
+
+(Fn1$F0$P) = λy0 λx (Fn1$F0$P$P x y0)
+
+(Fn2$F0$R0) = λ* λ%0 let (x$0, x$1) = %0; (Fn2$F0$F0 x$0 x$1)
+
+(Fn2$F0$P$P) = λy0 λx0 (Fn2$F0$R0 * y0)
+
+(Fn2$F0$P) = λy0 λx (Fn2$F0$P$P x y0)
+
+(Fn2$F0$F0$R0) = λ* λ%0 let (a, *) = %0; a
+
+(Fn2$F0$F0$P$P) = λy0 λx0 (Fn2$F0$F0$R0 * y0)
+
+(Fn2$F0$F0$P) = λy0 λx (Fn2$F0$F0$P$P x y0)
+
+(Fn3$F0$R0) = λ* 0
+
+(Fn3$F0$R1) = λa λ* a
+
+(Fn3$F0$P0) = Fn3$F0$R0
+
+(Fn3$F0$P+) = λy0 (Fn3$F0$R1 y0)