[sc-301] Some small improvements on mathing code

src/term/mod.rs

@@ -298,9 +298,9 @@ impl Term {
     Term::Str { val: STRINGS.get(str) }
   }
 
-  pub fn native_num_match(arg: Term, zero: Term, succ: Term) -> Term {
+  pub fn native_num_match(arg: Term, zero: Term, succ: Term, succ_var: Option<Option<Name>>) -> Term {
     let zero = Rule { pats: vec![Pattern::Num(NumCtr::Num(0))], body: zero };
-    let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, None))], body: succ };
+    let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, succ_var))], body: succ };
     Term::Mat { args: vec![arg], rules: vec![zero, succ] }
   }
 
@@ -695,16 +695,7 @@ impl Pattern {
   }
 
   pub fn is_native_num_match(&self) -> bool {
-    if let Pattern::Num(ctr) = self {
-      match ctr {
-        NumCtr::Num(0) => true,
-        NumCtr::Num(_) => false,
-        NumCtr::Succ(1, None) => true,
-        NumCtr::Succ(_, _) => false,
-      }
-    } else {
-      false
-    }
+    matches!(self, Pattern::Num(NumCtr::Num(0) | NumCtr::Succ(1, _)))
   }
 
   /// True if this pattern has no nested subpatterns.
@@ -758,9 +749,7 @@ impl Pattern {
     match (self, other) {
       (Pattern::Ctr(a, _), Pattern::Ctr(b, _)) if a == b => true,
       (Pattern::Num(NumCtr::Num(a)), Pattern::Num(NumCtr::Num(b))) if a == b => true,
-      (Pattern::Num(NumCtr::Num(_)), Pattern::Num(NumCtr::Num(_))) => false,
       (Pattern::Num(NumCtr::Succ(a, _)), Pattern::Num(NumCtr::Succ(b, _))) if a == b => true,
-      (Pattern::Num(NumCtr::Succ(_, _)), Pattern::Num(NumCtr::Succ(_, _))) => false,
       (Pattern::Tup(_, _), Pattern::Tup(_, _)) => true,
       (Pattern::Lst(_), Pattern::Lst(_)) => true,
       (Pattern::Var(_), Pattern::Var(_)) => true,

src/term/net_to_term.rs

@@ -1,7 +1,6 @@
-use super::Rule;
 use crate::{
   net::{INet, NodeId, NodeKind::*, Port, SlotId, ROOT},
-  term::{num_to_name, term_to_net::Labels, Book, Name, NumCtr, Op, Pattern, Tag, Term},
+  term::{num_to_name, term_to_net::Labels, Book, Name, Op, Pattern, Tag, Term},
 };
 use std::collections::{BTreeSet, HashMap, HashSet};
 
@@ -103,16 +102,16 @@ impl<'a> Reader<'a> {
           if *sel_kind != (Con { lab: None }) {
             // TODO: Is there any case where we expect a different node type here on readback?
             self.error(ReadbackError::InvalidNumericMatch);
-            Term::new_native_match(scrutinee, Term::Era, None, Term::Era)
+            Term::native_num_match(scrutinee, Term::Era, Term::Era, None)
           } else {
             let zero_term = self.read_term(self.net.enter_port(Port(sel_node, 1)));
             let succ_term = self.read_term(self.net.enter_port(Port(sel_node, 2)));
 
             match succ_term {
-              Term::Lam { nam, bod, .. } => Term::new_native_match(scrutinee, zero_term, nam, *bod),
+              Term::Lam { nam, bod, .. } => Term::native_num_match(scrutinee, zero_term, *bod, Some(nam)),
               _ => {
                 self.error(ReadbackError::InvalidNumericMatch);
-                Term::new_native_match(scrutinee, zero_term, None, succ_term)
+                Term::native_num_match(scrutinee, zero_term, succ_term, None)
               }
             }
           }
@@ -392,46 +391,6 @@ impl Term {
       Term::Var { .. } | Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Err => {}
     }
   }
-
-  /// Creates a new [`Term::Match`] from the given terms.
-  /// If `scrutinee` is not a `Term::Var`, creates a let binding containing the match in its body
-  fn new_native_match(arg: Self, zero_term: Self, mut succ_label: Option<Name>, mut succ_term: Self) -> Self {
-    let zero = Rule { pats: vec![Pattern::Num(NumCtr::Num(0))], body: zero_term };
-
-    if let Term::Var { nam } = &arg {
-      if let Some(label) = &succ_label {
-        let new_label = Name::new(format!("{}-1", nam));
-        succ_term.subst(label, &Term::Var { nam: new_label.clone() });
-        succ_label = Some(new_label);
-      }
-
-      let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, Some(succ_label)))], body: succ_term };
-      Term::Mat { args: vec![arg], rules: vec![zero, succ] }
-    } else {
-      match succ_label {
-        Some(succ) => {
-          let match_bind = succ.clone();
-
-          let new_label = Name::new(format!("{}-1", succ));
-          succ_term.subst(&succ, &Term::Var { nam: new_label.clone() });
-          succ_label = Some(new_label);
-
-          let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, Some(succ_label)))], body: succ_term };
-
-          Term::Let {
-            pat: Pattern::Var(Some(match_bind.clone())),
-            val: Box::new(arg),
-            nxt: Box::new(Term::Mat { args: vec![Term::Var { nam: match_bind }], rules: vec![zero, succ] }),
-          }
-        }
-        None => {
-          let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, None))], body: succ_term };
-
-          Term::Mat { args: vec![arg], rules: vec![zero, succ] }
-        }
-      }
-    }
-  }
 }
 
 #[derive(Default)]

src/term/transform/encode_pattern_matching.rs

@@ -134,6 +134,7 @@ fn encode_num(arg: Term, mut rules: Vec<Rule>) -> Term {
           Term::sub_num(arg.unwrap(), *val),
           rule.body,
           go(rules, last_rule, Some(*val), None),
+          None,
         )
       }
       // Middle match
@@ -147,6 +148,7 @@ fn encode_num(arg: Term, mut rules: Vec<Rule>) -> Term {
             Term::sub_num(Term::Var { nam: pred_nam }, val.wrapping_sub(prev_num).wrapping_sub(1)),
             rule.body,
             go(rules, last_rule, Some(*val), None),
+            None,
           ),
         )
       }

src/term/transform/eta_reduction.rs

@@ -37,34 +37,34 @@ impl Term {
           _ => {}
         }
       }
-      Term::Lam { bod, .. } => bod.eta_reduction(),
-      Term::Let { pat: _, val, nxt } | Term::Dup { tag: _, fst: _, snd: _, val, nxt } => {
-        val.eta_reduction();
-        nxt.eta_reduction();
-      }
-      Term::App { fun: fst, arg: snd, .. }
-      | Term::Tup { fst, snd }
-      | Term::Sup { fst, snd, .. }
-      | Term::Opx { op: _, fst, snd } => {
-        fst.eta_reduction();
-        snd.eta_reduction();
-      }
+      Term::Lam { tag: _, nam: None, bod } => bod.eta_reduction(),
+
       Term::Mat { args, rules } => {
         for arg in args {
           arg.eta_reduction();
         }
         for rule in rules {
-          for pat in &rule.pats {
-            debug_assert!(pat.is_native_num_match());
-          }
           rule.body.eta_reduction();
         }
       }
+      Term::Lst { els } => {
+        for el in els {
+          el.eta_reduction();
+        }
+      }
+      Term::Let { val: fst, nxt: snd, .. }
+      | Term::Dup { val: fst, nxt: snd, .. }
+      | Term::App { fun: fst, arg: snd, .. }
+      | Term::Tup { fst, snd }
+      | Term::Sup { fst, snd, .. }
+      | Term::Opx { fst, snd, .. } => {
+        fst.eta_reduction();
+        snd.eta_reduction();
+      }
       Term::Lnk { .. }
       | Term::Var { .. }
       | Term::Num { .. }
       | Term::Str { .. }
-      | Term::Lst { .. }
       | Term::Ref { .. }
       | Term::Era
       | Term::Err => {}

tests/snapshots/readback_lnet__invalid_mat_mat.hvm.snap

@@ -5,4 +5,4 @@ input_file: tests/golden_tests/readback_lnet/invalid_mat_mat.hvm
 Readback Warning:
 Invalid Numeric Match (4 occurrences)
 
-λa match match <Invalid> { 0: 3; 1+: 4 } { 0: <Invalid>; 1+: <Invalid> }
+λa match match <Invalid> { 0: 3; 1+*: 4 } { 0: <Invalid>; 1+: <Invalid> }

tests/snapshots/readback_lnet__match.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/readback_lnet/match.hvm
 ---
-let b = 1; match b { 0: λa a; 1+b-1: b-1 }
+match 1 { 0: λa a; 1+b: b }

tests/snapshots/run_file__linearize_match.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/linearize_match.hvm
 ---
-λa match a { 0: λb b; 1+a-1: λd (+ a-1 d) }
+λa match a { 0: λb b; 1+c: λd (+ c d) }

tests/snapshots/run_file__match_mult_linearization.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_file/match_mult_linearization.hvm
 ---
-λa match a { 0: λb λc λd (+ (+ b c) d); 1+a-1: λf λg λh (+ (+ (+ a-1 f) g) h) }
+λa match a { 0: λb λc λd (+ (+ b c) d); 1+e: λf λg λh (+ (+ (+ e f) g) h) }

tests/snapshots/run_lazy__linearize_match.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_lazy/linearize_match.hvm
 ---
-λa match a { 0: λb b; 1+a-1: λd (+ a-1 d) }
+λa match a { 0: λb b; 1+c: λd (+ c d) }

tests/snapshots/run_lazy__match_mult_linearization.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/run_lazy/match_mult_linearization.hvm
 ---
-λa match a { 0: λb λc λd (+ (+ b c) d); 1+a-1: λf λg λh (+ (+ (+ a-1 f) g) h) }
+λa match a { 0: λb λc λd (+ (+ b c) d); 1+e: λf λg λh (+ (+ (+ e f) g) h) }