[sc-517] Use kind2-like pattern matching terms, remove nested lets and adt lets

.gitignore

@@ -1 +1,2 @@
 /target
+*.snap.new

cspell.json

@@ -15,6 +15,7 @@
     "ctrs",
     "Dall",
     "datatypes",
+    "Deque",
     "desugared",
     "desugars",
     "dref",
@@ -85,6 +86,13 @@
     "walkdir",
     "wopts"
   ],
-  "files": ["**/*.rs", "**/*.md"],
+  "files": [
-  "ignoreRegExpList": ["HexValues", "/λ/g", "/-O/g"]
+    "**/*.rs",
+    "**/*.md"
+  ],
+  "ignoreRegExpList": [
+    "HexValues",
+    "/λ/g",
+    "/-O/g"
+  ]
 }

src/diagnostics.rs

@@ -16,7 +16,9 @@ pub struct Diagnostics {
 #[derive(Debug, Clone, Copy)]
 pub struct DiagnosticsConfig {
   pub verbose: bool,
-  pub match_only_vars: Severity,
+  pub irrefutable_match: Severity,
+  pub redundant_match: Severity,
+  pub unreachable_match: Severity,
   pub unused_definition: Severity,
   pub repeated_bind: Severity,
   pub mutual_recursion_cycle: Severity,
@@ -49,7 +51,9 @@ pub enum Severity {
 
 #[derive(Debug, Clone, Copy)]
 pub enum WarningType {
-  MatchOnlyVars,
+  IrrefutableMatch,
+  RedundantMatch,
+  UnreachableMatch,
   UnusedDefinition,
   RepeatedBind,
   MutualRecursionCycle,
@@ -221,7 +225,9 @@ impl From<String> for Diagnostics {
 impl DiagnosticsConfig {
   pub fn new(severity: Severity, verbose: bool) -> Self {
     Self {
-      match_only_vars: severity,
+      irrefutable_match: severity,
+      redundant_match: severity,
+      unreachable_match: severity,
       unused_definition: severity,
       repeated_bind: severity,
       mutual_recursion_cycle: severity,
@@ -231,10 +237,12 @@ impl DiagnosticsConfig {
 
   pub fn warning_severity(&self, warn: WarningType) -> Severity {
     match warn {
-      WarningType::MatchOnlyVars => self.match_only_vars,
       WarningType::UnusedDefinition => self.unused_definition,
       WarningType::RepeatedBind => self.repeated_bind,
       WarningType::MutualRecursionCycle => self.mutual_recursion_cycle,
+      WarningType::IrrefutableMatch => self.irrefutable_match,
+      WarningType::RedundantMatch => self.redundant_match,
+      WarningType::UnreachableMatch => self.unreachable_match,
     }
   }
 }
@@ -256,3 +264,9 @@ impl ToStringVerbose for &str {
     self.to_string()
   }
 }
+
+impl ToStringVerbose for String {
+  fn to_string_verbose(&self, _verbose: bool) -> String {
+    self.clone()
+  }
+}

src/lib.rs

@@ -66,55 +66,32 @@ pub fn desugar_book(
   let mut ctx = Ctx::new(book, diagnostics_cfg);
 
   ctx.check_shared_names();
+
   ctx.set_entrypoint();
+
+  ctx.book.encode_adts(opts.adt_encoding);
+
+  ctx.book.resolve_ctrs_in_pats();
+  ctx.check_unbound_ctr()?;
+  ctx.check_ctrs_arities()?;
+
   ctx.apply_args(args)?;
   ctx.book.apply_use();
 
-  ctx.book.encode_adts(opts.adt_encoding);
   ctx.book.encode_builtins();
 
-  ctx.book.resolve_ctrs_in_pats();
   ctx.resolve_refs()?;
-  ctx.check_repeated_binds();
 
-  ctx.check_match_arity()?;
+  ctx.fix_match_terms()?;
-  ctx.check_unbound_pats()?;
+  ctx.desugar_match_defs()?;
 
-  ctx.book.desugar_let_destructors();
-  ctx.book.desugar_implicit_match_binds();
-
-  ctx.check_ctrs_arities()?;
-  // Must be between [`Book::desugar_implicit_match_binds`] and [`Ctx::linearize_matches`]
   ctx.check_unbound_vars()?;
 
-  ctx.book.convert_match_def_to_term();
-
-  // TODO: We give variables fresh names before the match
-  // simplification to avoid `foo a a = a` binding to the wrong
-  // variable (it should be the second `a`). Ideally we'd like this
-  // pass to create the binds in the correct order, but to do that we
-  // have to reverse the order of the created let expressions when we
-  // have multiple consecutive var binds without a match in between,
-  // and I couldn't think of a simple way of doing that.
-  //
-  // In the paper this is not a problem because all var matches are
-  // pushed to the end, so it only needs to fix it in the irrefutable
-  // rule case. We could maybe do the opposite and do all var matches
-  // first, when it would also become easy to deal with. But this
-  // would potentially generate suboptimal lambda terms, need to think
-  // more about it.
-  //
-  // We technically still generate the let bindings in the wrong order
-  // but since lets can float between the binds it uses in its body
-  // and the places where its variable is used, this is not a problem.
-  ctx.book.make_var_names_unique();
-  ctx.simplify_matches()?;
-
   if opts.linearize_matches.enabled() {
-    ctx.book.linearize_simple_matches(opts.linearize_matches.is_extra());
+    ctx.book.linearize_matches(opts.linearize_matches.is_extra());
   }
 
-  ctx.book.encode_simple_matches(opts.adt_encoding);
+  ctx.book.encode_matches(opts.adt_encoding);
 
   // sanity check
   ctx.check_unbound_vars()?;

src/main.rs

@@ -213,8 +213,10 @@ impl OptArgs {
 #[derive(clap::ValueEnum, Clone, Debug)]
 pub enum WarningArgs {
   All,
-  UnusedDefs,
+  IrrefutableMatch,
-  MatchOnlyVars,
+  RedundantMatch,
+  UnreachableMatch,
+  UnusedDefinition,
   RepeatedBind,
   MutualRecursionCycle,
 }
@@ -250,6 +252,7 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Diagnostics> {
       let mut book = load_book(&path)?;
       check_book(&mut book)?;
     }
+
     Mode::Compile { path, comp_opts, warn_opts, lazy_mode } => {
       let diagnostics_cfg = set_warning_cfg_from_cli(
         DiagnosticsConfig::new(Severity::Warning, arg_verbose),
@@ -268,6 +271,7 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Diagnostics> {
       eprint!("{}", compile_res.diagnostics);
       println!("{}", compile_res.core_book);
     }
+
     Mode::Desugar { path, comp_opts, warn_opts, lazy_mode } => {
       let diagnostics_cfg = set_warning_cfg_from_cli(
         DiagnosticsConfig::new(Severity::Warning, arg_verbose),
@@ -286,6 +290,7 @@ fn execute_cli_mode(mut cli: Cli) -> Result<(), Diagnostics> {
       eprint!("{diagnostics}");
       println!("{book}");
     }
+
     Mode::Run {
       path,
       max_memory,
@@ -369,15 +374,19 @@ fn set_warning_cfg_from_cli(
   fn set(cfg: &mut DiagnosticsConfig, severity: Severity, cli_val: WarningArgs, lazy_mode: bool) {
     match cli_val {
       WarningArgs::All => {
+        cfg.irrefutable_match = severity;
+        cfg.redundant_match = severity;
+        cfg.unreachable_match = severity;
         cfg.unused_definition = severity;
-        cfg.match_only_vars = severity;
         cfg.repeated_bind = severity;
         if !lazy_mode {
           cfg.mutual_recursion_cycle = severity;
         }
       }
-      WarningArgs::UnusedDefs => cfg.unused_definition = severity,
+      WarningArgs::IrrefutableMatch => cfg.irrefutable_match = severity,
-      WarningArgs::MatchOnlyVars => cfg.match_only_vars = severity,
+      WarningArgs::RedundantMatch => cfg.redundant_match = severity,
+      WarningArgs::UnreachableMatch => cfg.unreachable_match = severity,
+      WarningArgs::UnusedDefinition => cfg.unused_definition = severity,
       WarningArgs::RepeatedBind => cfg.repeated_bind = severity,
       WarningArgs::MutualRecursionCycle => cfg.mutual_recursion_cycle = severity,
     }

src/term/builtins.rs

@@ -1,4 +1,4 @@
-use super::{parser::parse_book, Book, Name, NumCtr, Pattern, Term};
+use super::{parser::parse_book, Book, Name, Pattern, Term};
 
 const BUILTINS: &str = include_str!(concat!(env!("CARGO_MANIFEST_DIR"), "/src/term/builtins.hvm"));
 
@@ -38,46 +38,16 @@ impl Book {
 
 impl Term {
   fn encode_builtins(&mut self) {
-    match self {
+    Term::recursive_call(move || match self {
       Term::Lst { els } => *self = Term::encode_list(std::mem::take(els)),
       Term::Str { val } => *self = Term::encode_str(val),
       Term::Nat { val } => *self = Term::encode_nat(*val),
-      Term::Let { pat, val, nxt } => {
+      _ => {
-        pat.encode_builtins();
+        for child in self.children_mut() {
-        val.encode_builtins();
+          child.encode_builtins();
-        nxt.encode_builtins();
-      }
-      Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.encode_builtins(),
-      Term::App { fun: fst, arg: snd, .. }
-      | Term::Opx { fst, snd, .. }
-      | Term::Dup { val: fst, nxt: snd, .. } => {
-        fst.encode_builtins();
-        snd.encode_builtins();
-      }
-      Term::Sup { els, .. } | Term::Tup { els } => {
-        for el in els {
-          el.encode_builtins();
         }
       }
-      Term::Mat { args, rules } => {
+    })
-        for arg in args {
-          arg.encode_builtins();
-        }
-        for rule in rules {
-          for pat in &mut rule.pats {
-            pat.encode_builtins();
-          }
-          rule.body.encode_builtins();
-        }
-      }
-      Term::Use { .. }
-      | Term::Var { .. }
-      | Term::Lnk { .. }
-      | Term::Ref { .. }
-      | Term::Num { .. }
-      | Term::Era
-      | Term::Err => {}
-    }
   }
 
   fn encode_list(elements: Vec<Term>) -> Term {
@@ -133,7 +103,7 @@ impl Pattern {
     let lnil = Pattern::Ctr(Name::from(SNIL), vec![]);
 
     str.chars().rfold(lnil, |tail, head| {
-      let head = Pattern::Num(NumCtr::Num(head as u64));
+      let head = Pattern::Num(head as u64);
       Pattern::Ctr(Name::from(SCONS), vec![head, tail])
     })
   }

src/term/check/ctrs_arities.rs

@@ -2,7 +2,7 @@ use std::collections::HashMap;
 
 use crate::{
   diagnostics::{Diagnostics, ToStringVerbose},
-  term::{Book, Ctx, Name, Pattern, Term},
+  term::{Book, Ctx, Name, Pattern},
 };
 
 pub struct CtrArityMismatchErr {
@@ -26,8 +26,6 @@ impl Ctx<'_> {
           let res = pat.check_ctrs_arities(&arities);
           self.info.take_rule_err(res, def_name.clone());
         }
-        let res = rule.body.check_ctrs_arities(&arities);
-        self.info.take_rule_err(res, def_name.clone());
       }
     }
 
@@ -70,20 +68,6 @@ impl Pattern {
   }
 }
 
-impl Term {
-  pub fn check_ctrs_arities(&self, arities: &HashMap<Name, usize>) -> Result<(), CtrArityMismatchErr> {
-    Term::recursive_call(move || {
-      for pat in self.patterns() {
-        pat.check_ctrs_arities(arities)?;
-      }
-      for child in self.children() {
-        child.check_ctrs_arities(arities)?;
-      }
-      Ok(())
-    })
-  }
-}
-
 impl ToStringVerbose for CtrArityMismatchErr {
   fn to_string_verbose(&self, _verbose: bool) -> String {
     format!(

src/term/check/match_arity.rs

@@ -1,64 +0,0 @@
-use crate::{
-  diagnostics::{Diagnostics, ToStringVerbose},
-  term::{Ctx, Definition, Term},
-};
-
-pub struct MatchArityMismatchErr {
-  expected: usize,
-  found: usize,
-}
-
-impl Ctx<'_> {
-  /// Checks that the number of arguments in every pattern matching rule is consistent.
-  pub fn check_match_arity(&mut self) -> Result<(), Diagnostics> {
-    self.info.start_pass();
-
-    for (def_name, def) in self.book.defs.iter() {
-      let res = def.check_match_arity();
-      self.info.take_rule_err(res, def_name.clone());
-    }
-
-    self.info.fatal(())
-  }
-}
-
-impl Definition {
-  pub fn check_match_arity(&self) -> Result<(), MatchArityMismatchErr> {
-    let expected = self.arity();
-    for rule in &self.rules {
-      let found = rule.arity();
-      if found != expected {
-        return Err(MatchArityMismatchErr { found, expected });
-      }
-      rule.body.check_match_arity()?;
-    }
-    Ok(())
-  }
-}
-
-impl Term {
-  pub fn check_match_arity(&self) -> Result<(), MatchArityMismatchErr> {
-    Term::recursive_call(move || {
-      if let Term::Mat { args, rules } = self {
-        let expected = args.len();
-        for rule in rules {
-          let found = rule.pats.len();
-          if found != expected {
-            return Err(MatchArityMismatchErr { found, expected });
-          }
-        }
-      }
-
-      for child in self.children() {
-        child.check_match_arity()?;
-      }
-      Ok(())
-    })
-  }
-}
-
-impl ToStringVerbose for MatchArityMismatchErr {
-  fn to_string_verbose(&self, _verbose: bool) -> String {
-    format!("Arity mismatch in pattern matching. Expected {} patterns, found {}.", self.expected, self.found)
-  }
-}

src/term/check/mod.rs

@@ -1,8 +1,5 @@
 pub mod ctrs_arities;
-pub mod match_arity;
-pub mod repeated_bind;
 pub mod set_entrypoint;
 pub mod shared_names;
-pub mod type_check;
+pub mod unbound_ctrs;
-pub mod unbound_pats;
 pub mod unbound_vars;

src/term/check/repeated_bind.rs

@@ -1,77 +0,0 @@
-use crate::{
-  diagnostics::{ToStringVerbose, WarningType},
-  term::{Ctx, Name, Term},
-};
-use std::collections::HashSet;
-
-#[derive(Debug, Clone)]
-pub enum RepeatedBindWarn {
-  Rule(Name),
-  Match(Name),
-}
-
-impl Ctx<'_> {
-  /// Checks that there are no unbound variables in all definitions.
-  pub fn check_repeated_binds(&mut self) {
-    for (def_name, def) in &self.book.defs {
-      for rule in &def.rules {
-        let mut binds = HashSet::new();
-        for pat in &rule.pats {
-          for nam in pat.binds().flatten() {
-            if !binds.insert(nam) {
-              self.info.add_rule_warning(
-                RepeatedBindWarn::Rule(nam.clone()),
-                WarningType::RepeatedBind,
-                def_name.clone(),
-              );
-            }
-          }
-        }
-
-        let mut repeated_in_matches = Vec::new();
-        rule.body.check_repeated_binds(&mut repeated_in_matches);
-
-        for warn in repeated_in_matches {
-          self.info.add_rule_warning(warn, WarningType::RepeatedBind, def_name.clone());
-        }
-      }
-    }
-  }
-}
-
-impl Term {
-  pub fn check_repeated_binds(&self, repeated: &mut Vec<RepeatedBindWarn>) {
-    Term::recursive_call(|| match self {
-      Term::Mat { args, rules } => {
-        for arg in args {
-          arg.check_repeated_binds(repeated);
-        }
-
-        for rule in rules {
-          let mut binds = HashSet::new();
-          for pat in &rule.pats {
-            for nam in pat.binds().flatten() {
-              if !binds.insert(nam) {
-                repeated.push(RepeatedBindWarn::Match(nam.clone()));
-              }
-            }
-          }
-        }
-      }
-      _ => {
-        for child in self.children() {
-          child.check_repeated_binds(repeated);
-        }
-      }
-    })
-  }
-}
-
-impl ToStringVerbose for RepeatedBindWarn {
-  fn to_string_verbose(&self, _verbose: bool) -> String {
-    match self {
-      RepeatedBindWarn::Rule(bind) => format!("Repeated bind inside rule pattern: '{bind}'."),
-      RepeatedBindWarn::Match(bind) => format!("Repeated bind inside match arm: '{bind}'."),
-    }
-  }
-}

src/term/check/type_check.rs

@@ -1,58 +0,0 @@
-use crate::{
-  diagnostics::ToStringVerbose,
-  term::{Constructors, Name, Pattern, Rule, Type},
-};
-use indexmap::IndexMap;
-
-pub type DefinitionTypes = IndexMap<Name, Vec<Type>>;
-
-#[derive(Debug)]
-pub struct TypeMismatchErr {
-  expected: Type,
-  found: Type,
-}
-
-pub fn infer_match_arg_type(
-  rules: &[Rule],
-  arg_idx: usize,
-  ctrs: &Constructors,
-) -> Result<Type, TypeMismatchErr> {
-  infer_type(rules.iter().map(|r| &r.pats[arg_idx]), ctrs)
-}
-
-/// Infers the type of a sequence of arguments
-pub fn infer_type<'a>(
-  pats: impl IntoIterator<Item = &'a Pattern>,
-  ctrs: &Constructors,
-) -> Result<Type, TypeMismatchErr> {
-  let mut arg_type = Type::Any;
-  for pat in pats.into_iter() {
-    arg_type = unify(arg_type, pat.to_type(ctrs))?;
-  }
-  Ok(arg_type)
-}
-
-fn unify(old: Type, new: Type) -> Result<Type, TypeMismatchErr> {
-  match (old, new) {
-    (Type::Any, new) => Ok(new),
-    (old, Type::Any) => Ok(old),
-
-    (Type::Adt(old), Type::Adt(new)) if new == old => Ok(Type::Adt(old)),
-
-    (Type::Num, Type::Num) => Ok(Type::Num),
-    (Type::Num, Type::NumSucc(n)) => Ok(Type::NumSucc(n)),
-
-    (Type::NumSucc(n), Type::Num) => Ok(Type::NumSucc(n)),
-    (Type::NumSucc(a), Type::NumSucc(b)) if a == b => Ok(Type::NumSucc(a)),
-
-    (Type::Tup(a), Type::Tup(b)) if a == b => Ok(Type::Tup(a)),
-
-    (old, new) => Err(TypeMismatchErr { found: new, expected: old }),
-  }
-}
-
-impl ToStringVerbose for TypeMismatchErr {
-  fn to_string_verbose(&self, _verbose: bool) -> String {
-    format!("Type mismatch in pattern matching. Expected '{}', found '{}'.", self.expected, self.found)
-  }
-}

src/term/check/unbound_ctrs.rs

@@ -1,6 +1,6 @@
 use crate::{
   diagnostics::{Diagnostics, ToStringVerbose},
-  term::{Ctx, Name, Pattern, Term},
+  term::{Ctx, Name, Pattern},
 };
 use std::collections::HashSet;
 
@@ -8,8 +8,9 @@ use std::collections::HashSet;
 pub struct UnboundCtrErr(Name);
 
 impl Ctx<'_> {
-  /// Check if the constructors in rule patterns or match patterns are defined.
+  /// Check if the constructors in rule patterns are defined.
-  pub fn check_unbound_pats(&mut self) -> Result<(), Diagnostics> {
+  /// Match terms are not checked since unbounds there are treated as vars.
+  pub fn check_unbound_ctr(&mut self) -> Result<(), Diagnostics> {
     self.info.start_pass();
 
     let is_ctr = |nam: &Name| self.book.ctrs.contains_key(nam);
@@ -19,9 +20,6 @@ impl Ctx<'_> {
           let res = pat.check_unbounds(&is_ctr);
           self.info.take_rule_err(res, def_name.clone());
         }
-
-        let res = rule.body.check_unbound_pats(&is_ctr);
-        self.info.take_rule_err(res, def_name.clone());
       }
     }
 
@@ -51,20 +49,6 @@ impl Pattern {
   }
 }
 
-impl Term {
-  pub fn check_unbound_pats(&self, is_ctr: &impl Fn(&Name) -> bool) -> Result<(), UnboundCtrErr> {
-    Term::recursive_call(move || {
-      for pat in self.patterns() {
-        pat.check_unbounds(is_ctr)?;
-      }
-      for child in self.children() {
-        child.check_unbound_pats(is_ctr)?;
-      }
-      Ok(())
-    })
-  }
-}
-
 impl ToStringVerbose for UnboundCtrErr {
   fn to_string_verbose(&self, _verbose: bool) -> String {
     format!("Unbound constructor '{}'.", self.0)

src/term/display.rs

@@ -1,4 +1,4 @@
-use super::{Book, Definition, Name, NumCtr, Op, Pattern, Rule, Tag, Term, Type};
+use super::{Book, Definition, Name, NumCtr, Op, Pattern, Rule, Tag, Term};
 use std::{fmt, ops::Deref};
 
 /* Some aux structures for things that are not so simple to display */
@@ -50,8 +50,8 @@ impl fmt::Display for Term {
         write!(f, "{}λ${} {}", tag.display_padded(), var_as_str(nam), bod)
       }
       Term::Lnk { nam } => write!(f, "${nam}"),
-      Term::Let { pat, val, nxt } => {
+      Term::Let { nam, val, nxt } => {
-        write!(f, "let {} = {}; {}", pat, val, nxt)
+        write!(f, "let {} = {}; {}", var_as_str(nam), val, nxt)
       }
       Term::Use { nam, val, nxt } => {
         write!(f, "use {} = {}; {}", nam, val, nxt)
@@ -60,17 +60,26 @@ impl fmt::Display for Term {
       Term::App { tag, fun, arg } => {
         write!(f, "{}({} {})", tag.display_padded(), fun.display_app(tag), arg)
       }
-      Term::Mat { args, rules } => {
+      Term::Mat { arg, rules } => {
         write!(
           f,
           "match {} {{ {} }}",
-          DisplayJoin(|| args, ", "),
+          arg,
-          DisplayJoin(
+          DisplayJoin(|| rules.iter().map(|rule| display!("{}: {}", var_as_str(&rule.0), rule.2)), "; "),
-            || rules.iter().map(|rule| display!("{}: {}", DisplayJoin(|| &rule.pats, " "), rule.body)),
-            "; "
-          ),
         )
       }
+      Term::Swt { arg, rules } => {
+        write!(
+          f,
+          "switch {} {{ {} }}",
+          arg,
+          DisplayJoin(|| rules.iter().map(|rule| display!("{}: {}", rule.0, rule.1)), "; "),
+        )
+      }
+      Term::Ltp { bnd, val, nxt } => {
+        write!(f, "let ({}) = {}; {}", DisplayJoin(|| bnd.iter().map(var_as_str), ", "), val, nxt)
+      }
+      Term::Tup { els } => write!(f, "({})", DisplayJoin(|| els.iter(), ", "),),
       Term::Dup { tag, bnd, val, nxt } => {
         write!(f, "let {}{{{}}} = {}; {}", tag, DisplayJoin(|| bnd.iter().map(var_as_str), " "), val, nxt)
       }
@@ -84,7 +93,6 @@ impl fmt::Display for Term {
       Term::Opx { op, fst, snd } => {
         write!(f, "({} {} {})", op, fst, snd)
       }
-      Term::Tup { els } => write!(f, "({})", DisplayJoin(|| els.iter(), ", "),),
       Term::Lst { els } => write!(f, "[{}]", DisplayJoin(|| els.iter(), ", "),),
       Term::Err => write!(f, "<Invalid>"),
     })
@@ -145,9 +153,7 @@ impl fmt::Display for NumCtr {
   fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
     match self {
       NumCtr::Num(n) => write!(f, "{n}"),
-      NumCtr::Succ(n, None) => write!(f, "{n}+"),
+      NumCtr::Succ(_) => write!(f, "_"),
-      NumCtr::Succ(n, Some(None)) => write!(f, "{n}+*"),
-      NumCtr::Succ(n, Some(Some(nam))) => write!(f, "{n}+{nam}"),
     }
   }
 }
@@ -181,18 +187,6 @@ impl fmt::Display for Name {
   }
 }
 
-impl fmt::Display for Type {
-  fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-    match self {
-      Type::Any => write!(f, "any"),
-      Type::Tup(n) => write!(f, "tup{n}"),
-      Type::Num => write!(f, "num"),
-      Type::NumSucc(n) => write!(f, "{n}+"),
-      Type::Adt(nam) => write!(f, "{nam}"),
-    }
-  }
-}
-
 impl Term {
   fn display_app<'a>(&'a self, tag: &'a Tag) -> impl fmt::Display + 'a {
     DisplayFn(move |f| match self {

src/term/mod.rs

@@ -1,4 +1,4 @@
-use self::{check::type_check::infer_match_arg_type, parser::lexer::STRINGS};
+use self::parser::lexer::STRINGS;
 use crate::{
   diagnostics::{Diagnostics, DiagnosticsConfig},
   term::builtins::*,
@@ -7,11 +7,7 @@ use crate::{
 use indexmap::{IndexMap, IndexSet};
 use interner::global::GlobalString;
 use itertools::Itertools;
-use std::{
+use std::{borrow::Cow, collections::HashMap, ops::Deref};
-  borrow::Cow,
-  collections::{HashMap, HashSet},
-  ops::Deref,
-};
 
 pub mod builtins;
 pub mod check;
@@ -92,7 +88,7 @@ pub enum Term {
     nam: Name,
   },
   Let {
-    pat: Pattern,
+    nam: Option<Name>,
     val: Box<Term>,
     nxt: Box<Term>,
   },
@@ -106,6 +102,12 @@ pub enum Term {
     fun: Box<Term>,
     arg: Box<Term>,
   },
+  /// "let tup" tuple destructor
+  Ltp {
+    bnd: Vec<Option<Name>>,
+    val: Box<Term>,
+    nxt: Box<Term>,
+  },
   Tup {
     els: Vec<Term>,
   },
@@ -137,9 +139,15 @@ pub enum Term {
     fst: Box<Term>,
     snd: Box<Term>,
   },
+  /// Pattern matching on an ADT.
   Mat {
-    args: Vec<Term>,
+    arg: Box<Term>,
-    rules: Vec<Rule>,
+    rules: Vec<(Option<Name>, Vec<Option<Name>>, Term)>,
+  },
+  /// Native pattern matching on numbers
+  Swt {
+    arg: Box<Term>,
+    rules: Vec<(NumCtr, Term)>,
   },
   Ref {
     nam: Name,
@@ -153,16 +161,16 @@ pub enum Term {
 pub enum Pattern {
   Var(Option<Name>),
   Ctr(Name, Vec<Pattern>),
-  Num(NumCtr),
+  Num(u64),
   Tup(Vec<Pattern>),
   Lst(Vec<Pattern>),
   Str(GlobalString),
 }
 
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
 pub enum NumCtr {
   Num(u64),
-  Succ(u64, Option<Option<Name>>),
+  Succ(Option<Name>),
 }
 
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
@@ -193,21 +201,6 @@ pub enum Op {
   Shr,
 }
 
-/// Pattern types.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum Type {
-  /// Variables/wildcards.
-  Any,
-  /// A native tuple.
-  Tup(usize),
-  /// A sequence of arbitrary numbers ending in a variable.
-  Num,
-  /// A strictly incrementing sequence of numbers starting from 0, ending in a + ctr.
-  NumSucc(u64),
-  /// Adt constructors declared with the `data` syntax.
-  Adt(Name),
-}
-
 /// A user defined datatype
 #[derive(Debug, Clone, Default)]
 pub struct Adt {
@@ -273,6 +266,12 @@ impl PartialEq<str> for Name {
   }
 }
 
+impl PartialEq<&str> for Name {
+  fn eq(&self, other: &&str) -> bool {
+    self == other
+  }
+}
+
 impl PartialEq<Option<Name>> for Name {
   fn eq(&self, other: &Option<Name>) -> bool {
     if let Some(other) = other.as_ref() { self == other } else { false }
@@ -311,9 +310,10 @@ impl Clone for Term {
       Self::Var { nam } => Self::Var { nam: nam.clone() },
       Self::Chn { tag, nam, bod } => Self::Chn { tag: tag.clone(), nam: nam.clone(), bod: bod.clone() },
       Self::Lnk { nam } => Self::Lnk { nam: nam.clone() },
-      Self::Let { pat, val, nxt } => Self::Let { pat: pat.clone(), val: val.clone(), nxt: nxt.clone() },
+      Self::Let { nam, val, nxt } => Self::Let { nam: nam.clone(), val: val.clone(), nxt: nxt.clone() },
       Self::Use { nam, val, nxt } => Self::Use { nam: nam.clone(), val: val.clone(), nxt: nxt.clone() },
       Self::App { tag, fun, arg } => Self::App { tag: tag.clone(), fun: fun.clone(), arg: arg.clone() },
+      Self::Ltp { bnd, val, nxt } => Self::Ltp { bnd: bnd.clone(), val: val.clone(), nxt: nxt.clone() },
       Self::Tup { els } => Self::Tup { els: els.clone() },
       Self::Dup { tag, bnd, val, nxt } => {
         Self::Dup { tag: tag.clone(), bnd: bnd.clone(), val: val.clone(), nxt: nxt.clone() }
@@ -324,7 +324,8 @@ impl Clone for Term {
       Self::Str { val } => Self::Str { val: val.clone() },
       Self::Lst { els } => Self::Lst { els: els.clone() },
       Self::Opx { op, fst, snd } => Self::Opx { op: *op, fst: fst.clone(), snd: snd.clone() },
-      Self::Mat { args, rules } => Self::Mat { args: args.clone(), rules: rules.clone() },
+      Self::Mat { arg, rules } => Self::Mat { arg: arg.clone(), rules: rules.clone() },
+      Self::Swt { arg, rules } => Self::Swt { arg: arg.clone(), rules: rules.clone() },
       Self::Ref { nam } => Self::Ref { nam: nam.clone() },
       Self::Era => Self::Era,
       Self::Err => Self::Err,
@@ -348,12 +349,15 @@ impl Drop for Term {
             stack.push(std::mem::take(fst.as_mut()));
             stack.push(std::mem::take(snd.as_mut()));
           }
-          Term::Mat { args, rules } => {
+          Term::Mat { arg, rules } => {
-            for arg in std::mem::take(args).into_iter() {
+            stack.push(std::mem::take(arg));
-              stack.push(arg);
+            for (_ctr, _fields, body) in std::mem::take(rules).into_iter() {
+              stack.push(body);
             }
-
+          }
-            for Rule { body, .. } in std::mem::take(rules).into_iter() {
+          Term::Swt { arg, rules } => {
+            stack.push(std::mem::take(arg));
+            for (_nam, body) in std::mem::take(rules).into_iter() {
               stack.push(body);
             }
           }
@@ -432,10 +436,10 @@ impl Term {
     Term::Str { val: STRINGS.get(str) }
   }
 
-  pub fn native_num_match(arg: Term, zero: Term, succ: Term, succ_var: Option<Option<Name>>) -> Term {
+  pub fn switch(arg: Term, zero: Term, succ: Term, succ_var: Option<Name>) -> Term {
-    let zero = Rule { pats: vec![Pattern::Num(NumCtr::Num(0))], body: zero };
+    let zero = (NumCtr::Num(0), zero);
-    let succ = Rule { pats: vec![Pattern::Num(NumCtr::Succ(1, succ_var))], body: succ };
+    let succ = (NumCtr::Succ(succ_var), succ);
-    Term::Mat { args: vec![arg], rules: vec![zero, succ] }
+    Term::Swt { arg: Box::new(arg), rules: vec![zero, succ] }
   }
 
   pub fn sub_num(arg: Term, val: u64) -> Term {
@@ -456,13 +460,19 @@ impl Term {
 
   /* Iterators */
   pub fn children(&self) -> impl DoubleEndedIterator<Item = &Term> + Clone {
-    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat });
+    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt });
     match self {
-      Term::Mat { args, rules } => ChildrenIter::Mat(args.iter().chain(rules.iter().map(|r| &r.body))),
+      Term::Mat { arg, rules } => {
+        ChildrenIter::Mat([arg.as_ref()].into_iter().chain(rules.iter().map(|r| &r.2)))
+      }
+      Term::Swt { arg, rules } => {
+        ChildrenIter::Swt([arg.as_ref()].into_iter().chain(rules.iter().map(|r| &r.1)))
+      }
       Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => ChildrenIter::Vec(els),
       Term::Let { val: fst, nxt: snd, .. }
       | Term::Use { val: fst, nxt: snd, .. }
       | Term::App { fun: fst, arg: snd, .. }
+      | Term::Ltp { val: fst, nxt: snd, .. }
       | Term::Dup { val: fst, nxt: snd, .. }
       | Term::Opx { fst, snd, .. } => ChildrenIter::Two([fst.as_ref(), snd.as_ref()]),
       Term::Lam { bod, .. } | Term::Chn { bod, .. } => ChildrenIter::One([bod.as_ref()]),
@@ -478,15 +488,19 @@ impl Term {
   }
 
   pub fn children_mut(&mut self) -> impl DoubleEndedIterator<Item = &mut Term> {
-    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat });
+    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt });
     match self {
-      Term::Mat { args, rules } => {
+      Term::Mat { arg, rules } => {
-        ChildrenIter::Mat(args.iter_mut().chain(rules.iter_mut().map(|r| &mut r.body)))
+        ChildrenIter::Mat([arg.as_mut()].into_iter().chain(rules.iter_mut().map(|r| &mut r.2)))
+      }
+      Term::Swt { arg, rules } => {
+        ChildrenIter::Swt([arg.as_mut()].into_iter().chain(rules.iter_mut().map(|r| &mut r.1)))
       }
       Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => ChildrenIter::Vec(els),
       Term::Let { val: fst, nxt: snd, .. }
       | Term::Use { val: fst, nxt: snd, .. }
       | Term::App { fun: fst, arg: snd, .. }
+      | Term::Ltp { val: fst, nxt: snd, .. }
       | Term::Dup { val: fst, nxt: snd, .. }
       | Term::Opx { fst, snd, .. } => ChildrenIter::Two([fst.as_mut(), snd.as_mut()]),
       Term::Lam { bod, .. } | Term::Chn { bod, .. } => ChildrenIter::One([bod.as_mut()]),
@@ -511,23 +525,30 @@ impl Term {
     &self,
   ) -> impl DoubleEndedIterator<Item = (&Term, impl DoubleEndedIterator<Item = &Option<Name>> + Clone)> + Clone
   {
-    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat });
+    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt });
-    multi_iterator!(BindsIter { Zero, One, Dup, Pat, Rule });
+    multi_iterator!(BindsIter { Zero, One, Dup, Mat });
     match self {
-      Term::Mat { args, rules } => ChildrenIter::Mat(
+      Term::Mat { arg, rules } => ChildrenIter::Mat(
-        args
+        [(arg.as_ref(), BindsIter::Zero([]))]
-          .iter()
+          .into_iter()
-          .map(|arg| (arg, BindsIter::Zero([])))
+          .chain(rules.iter().map(|r| (&r.2, BindsIter::Mat(r.1.iter())))),
-          .chain(rules.iter().map(|r| (&r.body, BindsIter::Rule(r.pats.iter().flat_map(|p| p.binds()))))),
       ),
+      Term::Swt { arg, rules } => {
+        ChildrenIter::Swt([(arg.as_ref(), BindsIter::Zero([]))].into_iter().chain(rules.iter().map(|r| {
+          match &r.0 {
+            NumCtr::Num(_) => (&r.1, BindsIter::Zero([])),
+            NumCtr::Succ(nam) => (&r.1, BindsIter::One([nam])),
+          }
+        })))
+      }
       Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => {
         ChildrenIter::Vec(els.iter().map(|el| (el, BindsIter::Zero([]))))
       }
-      Term::Let { pat, val, nxt, .. } => {
+      Term::Let { nam, val, nxt, .. } => {
-        ChildrenIter::Two([(val.as_ref(), BindsIter::Zero([])), (nxt.as_ref(), BindsIter::Pat(pat.binds()))])
+        ChildrenIter::Two([(val.as_ref(), BindsIter::Zero([])), (nxt.as_ref(), BindsIter::One([nam]))])
       }
-      Term::Use { .. } => ChildrenIter::Zero([]),
+      Term::Use { .. } => todo!(),
-      Term::Dup { bnd, val, nxt, .. } => {
+      Term::Ltp { bnd, val, nxt, .. } | Term::Dup { bnd, val, nxt, .. } => {
         ChildrenIter::Two([(val.as_ref(), BindsIter::Zero([])), (nxt.as_ref(), BindsIter::Dup(bnd))])
       }
       Term::App { fun: fst, arg: snd, .. } | Term::Opx { fst, snd, .. } => {
@@ -550,22 +571,28 @@ impl Term {
     &mut self,
   ) -> impl DoubleEndedIterator<Item = (&mut Term, impl DoubleEndedIterator<Item = &Option<Name>> + Clone)>
   {
-    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat });
+    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt });
-    multi_iterator!(BindsIter { Zero, One, Dup, Pat, Rule });
+    multi_iterator!(BindsIter { Zero, One, Dup, Mat });
     match self {
-      Term::Mat { args, rules } => {
+      Term::Mat { arg, rules } => ChildrenIter::Mat(
-        ChildrenIter::Mat(args.iter_mut().map(|arg| (arg, BindsIter::Zero([]))).chain(
+        [(arg.as_mut(), BindsIter::Zero([]))]
-          rules.iter_mut().map(|r| (&mut r.body, BindsIter::Rule(r.pats.iter().flat_map(|p| p.binds())))),
+          .into_iter()
-        ))
+          .chain(rules.iter_mut().map(|r| (&mut r.2, BindsIter::Mat(r.1.iter())))),
-      }
+      ),
+      Term::Swt { arg, rules } => ChildrenIter::Swt([(arg.as_mut(), BindsIter::Zero([]))].into_iter().chain(
+        rules.iter_mut().map(|r| match &r.0 {
+          NumCtr::Num(_) => (&mut r.1, BindsIter::Zero([])),
+          NumCtr::Succ(nam) => (&mut r.1, BindsIter::One([nam])),
+        }),
+      )),
       Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => {
         ChildrenIter::Vec(els.iter_mut().map(|el| (el, BindsIter::Zero([]))))
       }
-      Term::Let { pat, val, nxt, .. } => {
+      Term::Let { nam, val, nxt, .. } => {
-        ChildrenIter::Two([(val.as_mut(), BindsIter::Zero([])), (nxt.as_mut(), BindsIter::Pat(pat.binds()))])
+        ChildrenIter::Two([(val.as_mut(), BindsIter::Zero([])), (nxt.as_mut(), BindsIter::One([&*nam]))])
       }
-      Term::Use { .. } => ChildrenIter::Zero([]),
+      Term::Use { .. } => todo!(),
-      Term::Dup { bnd, val, nxt, .. } => {
+      Term::Ltp { bnd, val, nxt, .. } | Term::Dup { bnd, val, nxt, .. } => {
         ChildrenIter::Two([(val.as_mut(), BindsIter::Zero([])), (nxt.as_mut(), BindsIter::Dup(bnd.iter()))])
       }
       Term::App { fun: fst, arg: snd, .. } | Term::Opx { fst, snd, .. } => {
@@ -587,25 +614,28 @@ impl Term {
   pub fn children_mut_with_binds_mut(
     &mut self,
   ) -> impl DoubleEndedIterator<Item = (&mut Term, impl DoubleEndedIterator<Item = &mut Option<Name>>)> {
-    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat });
+    multi_iterator!(ChildrenIter { Zero, One, Two, Vec, Mat, Swt });
-    multi_iterator!(BindsIter { Zero, One, Dup, Pat, Rule });
+    multi_iterator!(BindsIter { Zero, One, Dup, Mat });
     match self {
-      Term::Mat { args, rules } => ChildrenIter::Mat(
+      Term::Mat { arg, rules } => ChildrenIter::Mat(
-        args.iter_mut().map(|arg| (arg, BindsIter::Zero([]))).chain(
+        [(arg.as_mut(), BindsIter::Zero([]))]
-          rules
+          .into_iter()
-            .iter_mut()
+          .chain(rules.iter_mut().map(|r| (&mut r.2, BindsIter::Mat(r.1.iter_mut())))),
-            .map(|r| (&mut r.body, BindsIter::Rule(r.pats.iter_mut().flat_map(|p| p.binds_mut())))),
-        ),
       ),
+      Term::Swt { arg, rules } => ChildrenIter::Swt([(arg.as_mut(), BindsIter::Zero([]))].into_iter().chain(
+        rules.iter_mut().map(|r| match &mut r.0 {
+          NumCtr::Num(_) => (&mut r.1, BindsIter::Zero([])),
+          NumCtr::Succ(nam) => (&mut r.1, BindsIter::One([nam])),
+        }),
+      )),
       Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => {
         ChildrenIter::Vec(els.iter_mut().map(|el| (el, BindsIter::Zero([]))))
       }
-      Term::Let { pat, val, nxt, .. } => ChildrenIter::Two([
+      Term::Use { .. } => todo!(),
-        (val.as_mut(), BindsIter::Zero([])),
+      Term::Let { nam, val, nxt, .. } => {
-        (nxt.as_mut(), BindsIter::Pat(pat.binds_mut())),
+        ChildrenIter::Two([(val.as_mut(), BindsIter::Zero([])), (nxt.as_mut(), BindsIter::One([nam]))])
-      ]),
+      }
-      Term::Use { .. } => ChildrenIter::Zero([]),
+      Term::Ltp { bnd, val, nxt, .. } | Term::Dup { bnd, val, nxt, .. } => {
-      Term::Dup { bnd, val, nxt, .. } => {
         ChildrenIter::Two([(val.as_mut(), BindsIter::Zero([])), (nxt.as_mut(), BindsIter::Dup(bnd))])
       }
       Term::App { fun: fst, arg: snd, .. } | Term::Opx { fst, snd, .. } => {
@@ -624,56 +654,6 @@ impl Term {
     }
   }
 
-  pub fn patterns(&self) -> impl DoubleEndedIterator<Item = &Pattern> + Clone {
-    multi_iterator!(PatternsIter { Zero, Let, Mat });
-    match self {
-      Term::Mat { rules, .. } => PatternsIter::Mat(rules.iter().flat_map(|r| r.pats.iter())),
-      Term::Let { pat, .. } => PatternsIter::Let([pat]),
-      Term::Tup { .. }
-      | Term::Sup { .. }
-      | Term::Lst { .. }
-      | Term::Dup { .. }
-      | Term::Use { .. }
-      | Term::App { .. }
-      | Term::Opx { .. }
-      | Term::Lam { .. }
-      | Term::Chn { .. }
-      | Term::Var { .. }
-      | Term::Lnk { .. }
-      | Term::Num { .. }
-      | Term::Nat { .. }
-      | Term::Str { .. }
-      | Term::Ref { .. }
-      | Term::Era
-      | Term::Err => PatternsIter::Zero([]),
-    }
-  }
-
-  pub fn patterns_mut(&mut self) -> impl DoubleEndedIterator<Item = &mut Pattern> {
-    multi_iterator!(PatternsIter { Zero, Let, Mat });
-    match self {
-      Term::Mat { rules, .. } => PatternsIter::Mat(rules.iter_mut().flat_map(|r| r.pats.iter_mut())),
-      Term::Let { pat, .. } => PatternsIter::Let([pat]),
-      Term::Tup { .. }
-      | Term::Sup { .. }
-      | Term::Lst { .. }
-      | Term::Dup { .. }
-      | Term::Use { .. }
-      | Term::App { .. }
-      | Term::Opx { .. }
-      | Term::Lam { .. }
-      | Term::Chn { .. }
-      | Term::Var { .. }
-      | Term::Lnk { .. }
-      | Term::Num { .. }
-      | Term::Nat { .. }
-      | Term::Str { .. }
-      | Term::Ref { .. }
-      | Term::Era
-      | Term::Err => PatternsIter::Zero([]),
-    }
-  }
-
   /* Common checks and transformations */
   pub fn recursive_call<R, F>(f: F) -> R
   where
@@ -683,8 +663,12 @@ impl Term {
   }
 
   /// Substitute the occurrences of a variable in a term with the given term.
+  ///
   /// Caution: can cause invalid shadowing of variables if used incorrectly.
-  /// Ex: Using subst to beta-reduce (@a @b a b) converting it into (@b b).
+  /// Ex: Using subst to beta-reduce `(@a @b a b)` converting it into `@b b`.
+  ///
+  /// Expects var bind information to be properly stored in match expressions,
+  /// so it must run AFTER `fix_match_terms`.
   pub fn subst(&mut self, from: &Name, to: &Term) {
     Term::recursive_call(move || match self {
       Term::Var { nam } if nam == from => *self = to.clone(),
@@ -765,108 +749,12 @@ impl Term {
     go(self, &mut decls, &mut uses);
     (decls, uses)
   }
-
-  pub fn is_simple_match(&self, ctrs: &Constructors, adts: &Adts) -> bool {
-    // A match term
-    let Term::Mat { args, rules } = self else {
-      return false;
-    };
-    // With 1 argument
-    if args.len() != 1 {
-      return false;
-    }
-    // The argument is a variable
-    if !matches!(args[0], Term::Var { .. }) {
-      return false;
-    }
-    // Each arm only has 1 pattern for the 1 argument
-    if rules.iter().any(|r| r.pats.len() != 1) {
-      return false;
-    }
-    // The match is over a valid type
-    let Ok(typ) = infer_match_arg_type(rules, 0, ctrs) else {
-      return false;
-    };
-    // The match has one arm for each constructor, matching the constructors in adt declaration order
-    match typ {
-      Type::Any => {
-        if rules.len() != 1 {
-          return false;
-        }
-        if !matches!(rules[0].pats.as_slice(), [Pattern::Var(_)]) {
-          return false;
-        }
-      }
-      Type::Tup(_) => {
-        if rules.len() != 1 {
-          return false;
-        }
-        let Pattern::Tup(args) = &rules[0].pats[0] else { return false };
-        if args.iter().any(|p| !matches!(p, Pattern::Var(_))) {
-          return false;
-        }
-      }
-      Type::Num => {
-        let mut nums = HashSet::new();
-        for rule in rules {
-          if let Pattern::Num(NumCtr::Num(n)) = &rule.pats[0] {
-            if nums.contains(n) {
-              return false;
-            }
-            nums.insert(*n);
-          }
-        }
-      }
-      Type::NumSucc(n) => {
-        if rules.len() as u64 != n + 1 {
-          return false;
-        }
-        for (i, _) in rules.iter().enumerate() {
-          if i as u64 == n {
-            let Pattern::Num(NumCtr::Succ(n_pat, Some(_))) = &rules[i].pats[0] else { return false };
-            if n != *n_pat {
-              return false;
-            }
-          } else {
-            let Pattern::Num(NumCtr::Num(i_pat)) = &rules[i].pats[0] else { return false };
-            if i as u64 != *i_pat {
-              return false;
-            }
-          }
-        }
-      }
-      Type::Adt(adt) => {
-        let ctrs = &adts[&adt].ctrs;
-        if rules.len() != ctrs.len() {
-          return false;
-        }
-        for (rule, (ctr, args)) in rules.iter().zip(ctrs.iter()) {
-          if let Pattern::Ctr(rule_ctr, rule_args) = &rule.pats[0] {
-            if ctr != rule_ctr {
-              return false;
-            }
-            if rule_args.len() != args.len() {
-              return false;
-            }
-            if rule_args.iter().any(|arg| !matches!(arg, Pattern::Var(_))) {
-              return false;
-            }
-          } else {
-            return false;
-          }
-        }
-      }
-    }
-
-    true
-  }
 }
 
 impl Pattern {
   pub fn binds(&self) -> impl DoubleEndedIterator<Item = &Option<Name>> + Clone {
     self.iter().filter_map(|pat| match pat {
       Pattern::Var(nam) => Some(nam),
-      Pattern::Num(NumCtr::Succ(_, nam)) => nam.as_ref(),
       _ => None,
     })
   }
@@ -877,7 +765,7 @@ impl Pattern {
     let mut to_visit = vec![self];
     while let Some(pat) = to_visit.pop() {
       match pat {
-        Pattern::Var(nam) | Pattern::Num(NumCtr::Succ(_, Some(nam))) => binds.push(nam),
+        Pattern::Var(nam) => binds.push(nam),
         _ => to_visit.extend(pat.children_mut().rev()),
       }
     }
@@ -914,90 +802,21 @@ impl Pattern {
     els.into_iter()
   }
 
-  pub fn ctr_name(&self) -> Option<Name> {
-    match self {
-      Pattern::Var(_) => None,
-      Pattern::Ctr(nam, _) => Some(nam.clone()),
-      Pattern::Num(NumCtr::Num(num)) => Some(Name::new(format!("{num}"))),
-      Pattern::Num(NumCtr::Succ(num, _)) => Some(Name::new(format!("{num}+"))),
-      Pattern::Tup(pats) => Some(Name::new(format!("({})", ",".repeat(pats.len())))),
-      Pattern::Lst(_) => todo!(),
-      Pattern::Str(_) => todo!(),
-    }
-  }
-
   pub fn is_wildcard(&self) -> bool {
     matches!(self, Pattern::Var(_))
   }
 
-  pub fn is_native_num_match(&self) -> bool {
-    matches!(self, Pattern::Num(NumCtr::Num(0) | NumCtr::Succ(1, _)))
-  }
-
-  /// True if this pattern has no nested subpatterns.
-  pub fn is_simple(&self) -> bool {
-    match self {
-      Pattern::Var(_) => true,
-      Pattern::Ctr(_, args) | Pattern::Tup(args) => args.iter().all(|arg| matches!(arg, Pattern::Var(_))),
-      Pattern::Num(_) => true,
-      Pattern::Lst(_) | Pattern::Str(_) => todo!(),
-    }
-  }
-
-  pub fn to_type(&self, ctrs: &Constructors) -> Type {
-    match self {
-      Pattern::Var(_) => Type::Any,
-      Pattern::Ctr(ctr_nam, _) => {
-        let adt_nam = ctrs.get(ctr_nam).expect("Unknown constructor '{ctr_nam}'");
-        Type::Adt(adt_nam.clone())
-      }
-      Pattern::Tup(args) => Type::Tup(args.len()),
-      Pattern::Num(NumCtr::Num(_)) => Type::Num,
-      Pattern::Num(NumCtr::Succ(n, _)) => Type::NumSucc(*n),
-      Pattern::Lst(..) => Type::Adt(builtins::LIST.into()),
-      Pattern::Str(..) => Type::Adt(builtins::STRING.into()),
-    }
-  }
-
   pub fn to_term(&self) -> Term {
     match self {
       Pattern::Var(nam) => Term::var_or_era(nam.clone()),
       Pattern::Ctr(ctr, args) => {
         Term::call(Term::Ref { nam: ctr.clone() }, args.iter().map(|arg| arg.to_term()))
       }
-      Pattern::Num(NumCtr::Num(val)) => Term::Num { val: *val },
+      Pattern::Num(val) => Term::Num { val: *val },
-      // Succ constructor with no variable is not a valid term, only a compiler intermediate for a MAT inet node.
-      Pattern::Num(NumCtr::Succ(_, None)) => unreachable!(),
-      Pattern::Num(NumCtr::Succ(val, Some(Some(nam)))) => Term::add_num(Term::Var { nam: nam.clone() }, *val),
-      Pattern::Num(NumCtr::Succ(_, Some(None))) => Term::Era,
       Pattern::Tup(args) => Term::Tup { els: args.iter().map(|p| p.to_term()).collect() },
       Pattern::Lst(_) | Pattern::Str(_) => todo!(),
     }
   }
-
-  /// True if both patterns are equal (match the same expressions) without considering nested patterns.
-  pub fn simple_equals(&self, other: &Pattern) -> bool {
-    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::Succ(a, _)), Pattern::Num(NumCtr::Succ(b, _))) if a == b => true,
-      (Pattern::Tup(a), Pattern::Tup(b)) if a.len() == b.len() => true,
-      (Pattern::Lst(_), Pattern::Lst(_)) => true,
-      (Pattern::Var(_), Pattern::Var(_)) => true,
-      _ => false,
-    }
-  }
-
-  /// True if this pattern matches a subset of the other pattern, without considering nested patterns.
-  /// That is, when something matches the ctr of self if it also matches other.
-  pub fn simple_subset_of(&self, other: &Pattern) -> bool {
-    self.simple_equals(other) || matches!(other, Pattern::Var(_))
-  }
-
-  /// True if the two pattern will match some common expressions.
-  pub fn shares_simple_matches_with(&self, other: &Pattern) -> bool {
-    self.simple_equals(other) || matches!(self, Pattern::Var(_)) || matches!(other, Pattern::Var(_))
-  }
 }
 
 impl Rule {
@@ -1030,43 +849,6 @@ impl Definition {
   }
 }
 
-impl Type {
-  /// Return the constructors for a given type as patterns.
-  pub fn ctrs(&self, adts: &Adts) -> Vec<Pattern> {
-    match self {
-      Type::Any => vec![Pattern::Var(None)],
-      Type::Tup(len) => {
-        vec![Pattern::Tup((0 .. *len).map(|i| Pattern::Var(Some(Name::new(format!("%x{i}"))))).collect())]
-      }
-      Type::NumSucc(n) => {
-        let mut ctrs = (0 .. *n).map(|n| Pattern::Num(NumCtr::Num(n))).collect::<Vec<_>>();
-        ctrs.push(Pattern::Num(NumCtr::Succ(*n, Some(Some("%pred".into())))));
-        ctrs
-      }
-      Type::Num => unreachable!(),
-      Type::Adt(adt) => {
-        // TODO: Should return just a ref to ctrs and not clone.
-        adts[adt]
-          .ctrs
-          .iter()
-          .map(|(nam, args)| {
-            Pattern::Ctr(nam.clone(), args.iter().map(|x| Pattern::Var(Some(x.clone()))).collect())
-          })
-          .collect()
-      }
-    }
-  }
-
-  /// True if the type is an ADT or a builtin equivalent of an ADT (like tups and numbers)
-  pub fn is_ctr_type(&self) -> bool {
-    matches!(self, Type::Adt(_) | Type::Num | Type::Tup(_))
-  }
-
-  pub fn is_var_type(&self) -> bool {
-    matches!(self, Type::Any)
-  }
-}
-
 impl Name {
   pub fn new<'a, V: Into<Cow<'a, str>>>(value: V) -> Name {
     Name(STRINGS.get(value))

src/term/net_to_term.rs

@@ -1,7 +1,7 @@
 use crate::{
   diagnostics::{DiagnosticOrigin, Diagnostics, Severity},
   net::{INet, NodeId, NodeKind::*, Port, SlotId, ROOT},
-  term::{num_to_name, term_to_net::Labels, Book, Name, Op, Pattern, Tag, Term},
+  term::{num_to_name, term_to_net::Labels, Book, Name, Op, Tag, Term},
 };
 use std::collections::{BTreeSet, HashMap, HashSet};
 
@@ -59,6 +59,7 @@ pub struct Reader<'a> {
   net: &'a INet,
   labels: &'a Labels,
   dup_paths: Option<HashMap<u32, Vec<SlotId>>>,
+  /// Store for floating/unscoped terms, like dups and let tups.
   scope: Scope,
   seen_fans: Scope,
   seen: HashSet<Port>,
@@ -102,7 +103,7 @@ impl Reader<'_> {
         Mat => match next.slot() {
           2 => {
             // Read the matched expression
-            let scrutinee = self.read_term(self.net.enter_port(Port(node, 0)));
+            let mut arg = self.read_term(self.net.enter_port(Port(node, 0)));
 
             // Read the pattern matching node
             let sel_node = self.net.enter_port(Port(node, 1)).node();
@@ -112,20 +113,38 @@ impl Reader<'_> {
             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::native_num_match(scrutinee, Term::Era, Term::Era, None)
+              Term::switch(arg, Term::Era, Term::Era, None)
             } else {
               let zero_term = self.read_term(self.net.enter_port(Port(sel_node, 1)));
               let mut succ_term = self.read_term(self.net.enter_port(Port(sel_node, 2)));
 
               match &mut succ_term {
                 Term::Lam { nam, bod, .. } => {
+                  // Extract non-var args so we can refer to the pred.
+                  let (arg, bind) = if let Term::Var { nam } = &mut arg {
+                    (std::mem::replace(nam, Name::from("")), None)
+                  } else {
+                    (self.namegen.unique(), Some(arg))
+                  };
+
                   let nam = std::mem::take(nam);
-                  let bod = std::mem::take(bod);
+                  let mut bod = std::mem::take(bod);
-                  Term::native_num_match(scrutinee, zero_term, *bod, Some(nam))
+
+                  // Rename the pred variable to indicate it's arg-1.
+                  if let Some(nam) = &nam {
+                    bod.subst(nam, &Term::Var { nam: Name::new(format!("{arg}-1")) });
+                  }
+
+                  let swt = Term::switch(Term::Var { nam: arg.clone() }, zero_term, *bod, nam);
+                  if let Some(bind) = bind {
+                    Term::Let { nam: Some(arg), val: Box::new(bind), nxt: Box::new(swt) }
+                  } else {
+                    swt
+                  }
                 }
                 _ => {
                   self.error(ReadbackError::InvalidNumericMatch);
-                  Term::native_num_match(scrutinee, zero_term, succ_term, None)
+                  Term::switch(arg, zero_term, succ_term, None)
                 }
               }
             }
@@ -322,48 +341,27 @@ impl Term {
   /// This has the effect of inserting the split at the lowest common ancestor
   /// of all of the uses of `fst` and `snd`.
   fn insert_split(&mut self, split: &mut Split, threshold: usize) -> Option<usize> {
-    let n = match self {
+    Term::recursive_call(move || {
-      Term::Var { nam } => usize::from(split.fst.as_ref() == Some(nam) || split.snd.as_ref() == Some(nam)),
+      let mut n = match self {
-      Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.insert_split(split, threshold)?,
+        Term::Var { nam } => usize::from(split.fst.as_ref() == Some(nam) || split.snd.as_ref() == Some(nam)),
-      Term::Let { val: fst, nxt: snd, .. }
+        _ => 0,
-      | Term::App { fun: fst, arg: snd, .. }
-      | Term::Dup { val: fst, nxt: snd, .. }
-      | Term::Opx { fst, snd, .. } => {
-        fst.insert_split(split, threshold)? + snd.insert_split(split, threshold)?
-      }
-      Term::Use { .. } => unreachable!(),
-      Term::Sup { els, .. } | Term::Tup { els } => {
-        let mut n = 0;
-        for el in els {
-          n += el.insert_split(split, threshold)?;
-        }
-        n
-      }
-      Term::Mat { args, rules } => {
-        debug_assert_eq!(args.len(), 1);
-        let mut n = args[0].insert_split(split, threshold)?;
-        for rule in rules {
-          n += rule.body.insert_split(split, threshold)?;
-        }
-        n
-      }
-      Term::Nat { .. } | Term::Lst { .. } => unreachable!(),
-      Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Ref { .. } | Term::Era | Term::Err => 0,
-    };
-
-    if n >= threshold {
-      let Split { tag, fst, snd, val } = std::mem::take(split);
-      let nxt = Box::new(std::mem::take(self));
-      *self = match tag {
-        None => {
-          Term::Let { pat: Pattern::Tup(vec![Pattern::Var(fst), Pattern::Var(snd)]), val: Box::new(val), nxt }
-        }
-        Some(tag) => Term::Dup { tag, bnd: vec![fst, snd], val: Box::new(val), nxt },
       };
-      None
+      for child in self.children_mut() {
-    } else {
+        n += child.insert_split(split, threshold)?;
-      Some(n)
+      }
-    }
+
+      if n >= threshold {
+        let Split { tag, fst, snd, val } = std::mem::take(split);
+        let nxt = Box::new(std::mem::take(self));
+        *self = match tag {
+          None => Term::Ltp { bnd: vec![fst, snd], val: Box::new(val), nxt },
+          Some(tag) => Term::Dup { tag, bnd: vec![fst, snd], val: Box::new(val), nxt },
+        };
+        None
+      } else {
+        Some(n)
+      }
+    })
   }
 
   pub fn fix_names(&mut self, id_counter: &mut u64, book: &Book) {
@@ -376,11 +374,7 @@ impl Term {
       }
     }
 
-    match self {
+    Term::recursive_call(move || match self {
-      Term::Lam { nam, bod, .. } => {
-        fix_name(nam, id_counter, bod);
-        bod.fix_names(id_counter, book);
-      }
       Term::Ref { nam: def_name } => {
         if def_name.is_generated() {
           let def = book.defs.get(def_name).unwrap();
@@ -389,39 +383,15 @@ impl Term {
           *self = term;
         }
       }
-      Term::Dup { bnd, val, nxt, .. } => {
+      _ => {
-        val.fix_names(id_counter, book);
+        for (child, bnd) in self.children_mut_with_binds_mut() {
-        for bnd in bnd {
+          for bnd in bnd {
-          fix_name(bnd, id_counter, nxt);
+            fix_name(bnd, id_counter, child);
-        }
+            child.fix_names(id_counter, book);
-        nxt.fix_names(id_counter, book);
-      }
-      Term::Chn { bod, .. } => bod.fix_names(id_counter, book),
-      Term::App { fun: fst, arg: snd, .. } | Term::Opx { op: _, fst, snd } => {
-        fst.fix_names(id_counter, book);
-        snd.fix_names(id_counter, book);
-      }
-      Term::Sup { els, .. } | Term::Tup { els } => {
-        for el in els {
-          el.fix_names(id_counter, book);
-        }
-      }
-      Term::Mat { args, rules } => {
-        for arg in args {
-          arg.fix_names(id_counter, book);
-        }
-
-        for rule in rules {
-          for nam in rule.pats.iter_mut().flat_map(|p| p.binds_mut()) {
-            fix_name(nam, id_counter, &mut rule.body);
           }
-
-          rule.body.fix_names(id_counter, book);
         }
       }
-      Term::Let { .. } | Term::Use { .. } | Term::Nat { .. } | Term::Lst { .. } => unreachable!(),
+    })
-      Term::Var { .. } | Term::Lnk { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era | Term::Err => {}
-    }
   }
 }
 

src/term/parser/lexer.rs

@@ -26,6 +26,9 @@ pub enum Token {
   #[token("match")]
   Match,
 
+  #[token("switch")]
+  Switch,
+
   #[token("=")]
   Equals,
 
@@ -270,6 +273,7 @@ impl fmt::Display for Token {
       Self::Let => write!(f, "let"),
       Self::Use => write!(f, "use"),
       Self::Match => write!(f, "match"),
+      Self::Switch => write!(f, "switch"),
       Self::Equals => write!(f, "="),
       Self::Num(num) => write!(f, "{num}"),
       Self::Str(s) => write!(f, "\"{s}\""),

src/term/parser/parser.rs

@@ -1,6 +1,6 @@
 use crate::term::{
   parser::lexer::{LexingError, Token},
-  Adt, Book, Definition, Name, NumCtr, Op, Pattern, Rule, Tag, Term,
+  Adt, Book, Definition, Name, NumCtr, Op, Pattern, Rule, Tag, Term, LNIL, SNIL,
 };
 use chumsky::{
   error::{Error, RichReason},
@@ -198,24 +198,27 @@ where
   I: ValueInput<'a, Token = Token, Span = SimpleSpan>,
 {
   let var = name().map(|name| Term::Var { nam: name }).boxed();
-  let global_var = just(Token::Dollar).ignore_then(name()).map(|name| Term::Lnk { nam: name }).boxed();
+  let unscoped_var = just(Token::Dollar).ignore_then(name()).map(|name| Term::Lnk { nam: name }).boxed();
 
-  let number = select!(Token::Num(num) => Term::Num{val: num}).or(
+  let number = select!(Token::Num(num) => num).or(
     select!(Token::Error(LexingError::InvalidNumberLiteral) => ()).validate(|_, span, emit| {
       emit.emit(Rich::custom(span, "found invalid number literal expected number"));
-      Term::Num { val: 0 }
+      0
     }),
   );
 
-  let nat = just(Token::Hash).ignore_then(select!(Token::Num(num) => Term::Nat { val: num }).or(
+  let nat: chumsky::Boxed<I, Term, extra::Err<Rich<_>>> = just(Token::Hash)
-    select!(Token::Error(LexingError::InvalidNumberLiteral) => ()).validate(|_, span, emit| {
+    .ignore_then(select!(Token::Num(num) => Term::Nat { val: num }).or(
-      emit.emit(Rich::custom(span, "found invalid nat literal expected number"));
+      select!(Token::Error(LexingError::InvalidNumberLiteral) => ()).validate(|_, span, emit| {
-      Term::Nat { val: 0 }
+        emit.emit(Rich::custom(span, "found invalid nat literal expected number"));
-    }),
+        Term::Nat { val: 0 }
-  ));
+      }),
+    ))
+    .boxed();
+
+  let num_term = number.map(|val| Term::Num { val });
 
   let term_sep = just(Token::Semicolon).or_not();
-  let list_sep = just(Token::Comma).or_not();
 
   recursive(|term| {
     // *
@@ -230,7 +233,7 @@ where
       .boxed();
 
     // #tag? λ$x body
-    let global_lam = tag(Tag::Static)
+    let unscoped_lam = tag(Tag::Static)
       .then_ignore(just(Token::Lambda))
       .then(just(Token::Dollar).ignore_then(name_or_era()))
       .then(term.clone())
@@ -240,7 +243,7 @@ where
     // #tag {fst snd}
     let sup = tag(Tag::Auto)
       .then_ignore(just(Token::LBracket))
-      .then(term.clone().separated_by(list_sep.clone()).at_least(2).collect())
+      .then(term.clone().separated_by(just(Token::Comma).or_not()).at_least(2).collect())
       .then_ignore(just(Token::RBracket))
       .map(|(tag, els)| Term::Sup { tag, els })
       .boxed();
@@ -249,7 +252,7 @@ where
     let dup = just(Token::Let)
       .ignore_then(tag(Tag::Auto))
       .then_ignore(just(Token::LBracket))
-      .then(name_or_era().separated_by(list_sep.clone()).at_least(2).collect())
+      .then(name_or_era().separated_by(just(Token::Comma).or_not()).at_least(2).collect())
       .then_ignore(just(Token::RBracket))
       .then_ignore(just(Token::Equals))
       .then(term.clone())
@@ -258,20 +261,14 @@ where
       .map(|(((tag, bnd), val), next)| Term::Dup { tag, bnd, val: Box::new(val), nxt: Box::new(next) })
       .boxed();
 
-    // let a = ...
+    // let nam = term; term
-    // let (a, b) = ...
     let let_ = just(Token::Let)
-      .ignore_then(pattern().validate(|pat, span, emit| {
+      .ignore_then(name_or_era())
-        if matches!(&pat, Pattern::Num(..)) {
-          emit.emit(Rich::custom(span, "Numbers not supported in let."));
-        }
-        pat
-      }))
       .then_ignore(just(Token::Equals))
       .then(term.clone())
       .then_ignore(term_sep.clone())
       .then(term.clone())
-      .map(|((pat, val), nxt)| Term::Let { pat, val: Box::new(val), nxt: Box::new(nxt) })
+      .map(|((nam, val), nxt)| Term::Let { nam, val: Box::new(val), nxt: Box::new(nxt) })
       .boxed();
 
     // use a = val ';'? nxt
@@ -284,42 +281,69 @@ where
       .map(|((nam, val), nxt)| Term::Use { nam, val: Box::new(val), nxt: Box::new(nxt) })
       .boxed();
 
-    let match_arg = name().then_ignore(just(Token::Equals)).or_not().then(term.clone());
+    // (name '=')? term
-    let match_args =
+    let match_arg = name().then_ignore(just(Token::Equals)).or_not().then(term.clone()).boxed();
-      match_arg.separated_by(list_sep.clone()).at_least(1).allow_trailing().collect::<Vec<_>>();
 
-    // '|'? pat+: term
+    let lnil = just(Token::LBrace)
+      .ignore_then(just(Token::RBrace))
+      .ignored()
+      .map(|_| Some(Name::from(LNIL)))
+      .labelled("List.nil");
+    let snil =
+      select!(Token::Str(s) if s.is_empty() => ()).map(|_| Some(Name::from(SNIL))).labelled("String.nil");
+    let match_pat = choice((name_or_era(), lnil, snil));
+
+    // '|'? name: term
     let match_rule = just(Token::Or)
       .or_not()
-      .ignore_then(pattern().repeated().at_least(1).collect::<Vec<_>>())
+      .ignore_then(match_pat)
+      .labelled("<Match pattern>")
       .then_ignore(just(Token::Colon))
       .then(term.clone())
-      .map(|(pats, body)| Rule { pats, body });
+      .map(|(nam, body)| (nam, vec![], body));
     let match_rules = match_rule.separated_by(term_sep.clone()).at_least(1).allow_trailing().collect();
 
     // match ((scrutinee | <name> = value),?)+ { pat+: term;... }
     let match_ = just(Token::Match)
-      .ignore_then(match_args)
+      .ignore_then(match_arg.clone())
       .then_ignore(just(Token::LBracket))
       .then(match_rules)
       .then_ignore(just(Token::RBracket))
-      .map(|(args, rules)| {
+      .map(|((bind, arg), rules)| {
-        let mut args_no_bind = vec![];
+        if let Some(bind) = bind {
-        let mut binds = vec![];
+          Term::Let {
-        for (bind, arg) in args {
+            nam: Some(bind.clone()),
-          if let Some(bind) = bind {
+            val: Box::new(arg),
-            args_no_bind.push(Term::Var { nam: bind.clone() });
+            nxt: Box::new(Term::Mat { arg: Box::new(Term::Var { nam: bind }), rules }),
-            binds.push((bind, arg));
-          } else {
-            args_no_bind.push(arg);
           }
+        } else {
+          Term::Mat { arg: Box::new(arg), rules }
+        }
+      })
+      .boxed();
+
+    let switch_ctr = choice((number.map(NumCtr::Num), soft_keyword("_").map(|_| NumCtr::Succ(None))))
+      .labelled("<Switch pattern>");
+
+    let switch_rule =
+      just(Token::Or).or_not().ignore_then(switch_ctr).then_ignore(just(Token::Colon)).then(term.clone());
+    let switch_rules = switch_rule.separated_by(term_sep.clone()).at_least(1).allow_trailing().collect();
+
+    let switch = just(Token::Switch)
+      .ignore_then(match_arg)
+      .then_ignore(just(Token::LBracket))
+      .then(switch_rules)
+      .then_ignore(just(Token::RBracket))
+      .map(|((bind, arg), rules)| {
+        if let Some(bind) = bind {
+          Term::Let {
+            nam: Some(bind.clone()),
+            val: Box::new(arg),
+            nxt: Box::new(Term::Swt { arg: Box::new(Term::Var { nam: bind }), rules }),
+          }
+        } else {
+          Term::Swt { arg: Box::new(arg), rules }
         }
-        let mat = Term::Mat { args: args_no_bind, rules };
-        binds.into_iter().rfold(mat, |acc, (bind, arg)| Term::Let {
-          pat: Pattern::Var(Some(bind)),
-          val: Box::new(arg),
-          nxt: Box::new(acc),
-        })
       })
       .boxed();
 
@@ -351,6 +375,18 @@ where
       .map(|els| Term::Tup { els })
       .boxed();
 
+    // let (x, ..n) = term; term
+    let let_tup = just(Token::Let)
+      .ignore_then(just(Token::LParen))
+      .ignore_then(name_or_era().separated_by(just(Token::Comma)).at_least(2).collect())
+      .then_ignore(just(Token::RParen))
+      .then_ignore(just(Token::Equals))
+      .then(term.clone())
+      .then_ignore(term_sep.clone())
+      .then(term.clone())
+      .map(|((bnd, val), next)| Term::Ltp { bnd, val: Box::new(val), nxt: Box::new(next) })
+      .boxed();
+
     let str = select!(Token::Str(s) => Term::Str { val: s }).boxed();
     let chr = select!(Token::Char(c) => Term::Num { val: c }).boxed();
 
@@ -363,16 +399,32 @@ where
       .boxed();
 
     choice((
-      // OBS: `num_op` has to be before app, idk why?
+      num_op,
-      // OBS: `app` has to be before `tup` to not overflow on huge app terms
+      app,
-      // TODO: What happens on huge `tup` and other terms?
+      tup,
-      num_op, app, tup, global_var, var, number, nat, list, str, chr, sup, global_lam, lam, dup, let_, use_,
+      unscoped_var,
-      match_, era,
+      var,
+      nat,
+      num_term,
+      list,
+      str,
+      chr,
+      sup,
+      unscoped_lam,
+      lam,
+      dup,
+      use_,
+      let_tup,
+      let_,
+      match_,
+      switch,
+      era,
     ))
+    .labelled("term")
   })
 }
 
-fn pattern<'a, I>() -> impl Parser<'a, I, Pattern, extra::Err<Rich<'a, Token>>>
+fn rule_pattern<'a, I>() -> impl Parser<'a, I, Pattern, extra::Err<Rich<'a, Token>>>
 where
   I: ValueInput<'a, Token = Token, Span = SimpleSpan>,
 {
@@ -407,28 +459,22 @@ where
       n
     });
 
-    let num = num_val.map(|n| Pattern::Num(NumCtr::Num(n))).labelled("<Num>");
+    let num = num_val.map(Pattern::Num).labelled("<Num>");
 
-    let succ = num_val
+    let chr = select!(Token::Char(c) => Pattern::Num(c)).labelled("<Char>").boxed();
-      .then_ignore(just(Token::Add))
-      .then(name_or_era().or_not())
-      .map(|(num, nam)| Pattern::Num(NumCtr::Succ(num, nam)))
-      .labelled("<Num>+")
-      .boxed();
-
-    let chr = select!(Token::Char(c) => Pattern::Num(NumCtr::Num(c))).labelled("<Char>").boxed();
 
     let str = select!(Token::Str(s) => Pattern::Str(s)).labelled("<String>").boxed();
 
-    choice((succ, num, chr, str, var, ctr, list, tup))
+    choice((num, chr, str, var, ctr, list, tup))
   })
+  .labelled("<Rule pattern>")
 }
 
-fn rule_pattern<'a, I>() -> impl Parser<'a, I, (Name, Vec<Pattern>), extra::Err<Rich<'a, Token>>>
+fn rule_lhs<'a, I>() -> impl Parser<'a, I, (Name, Vec<Pattern>), extra::Err<Rich<'a, Token>>>
 where
   I: ValueInput<'a, Token = Token, Span = SimpleSpan>,
 {
-  let lhs = tl_name().then(pattern().repeated().collect()).boxed();
+  let lhs = tl_name().then(rule_pattern().repeated().collect()).boxed();
 
   let just_lhs = lhs.clone().then_ignore(just(Token::Equals).map_err(|err: Rich<'a, Token>| {
     Error::<I>::expected_found(
@@ -455,7 +501,7 @@ fn rule<'a, I>() -> impl Parser<'a, I, TopLevel, extra::Err<Rich<'a, Token>>>
 where
   I: ValueInput<'a, Token = Token, Span = SimpleSpan>,
 {
-  rule_pattern().then(term()).map(move |((name, pats), body)| TopLevel::Rule((name, Rule { pats, body })))
+  rule_lhs().then(term()).map(move |((name, pats), body)| TopLevel::Rule((name, Rule { pats, body })))
 }
 
 fn datatype<'a, I>() -> impl Parser<'a, I, TopLevel, extra::Err<Rich<'a, Token>>>

src/term/term_to_net.rs

@@ -4,7 +4,7 @@ use crate::{
     NodeKind::{self, *},
     Port, ROOT,
   },
-  term::{Book, Name, NumCtr, Op, Pattern, Tag, Term},
+  term::{Book, Name, NumCtr, Op, Tag, Term},
 };
 use std::collections::{hash_map::Entry, HashMap};
 
@@ -111,30 +111,31 @@ impl EncodeTermState<'_> {
 
           Some(Port(app, 2))
         }
-        // core: & cond ~  (zero succ) ret
+        Term::Mat { .. } => unreachable!("Should've been desugared already"),
-        Term::Mat { args, rules } => {
+        // core: & arg ~ ?<(zero succ) ret>
-          // At this point should be only simple num matches.
+        Term::Swt { arg, rules } => {
-          let arg = args.iter().next().unwrap();
+          // At this point should be only num matches of 0 and succ.
-          debug_assert!(matches!(rules[0].pats[..], [Pattern::Num(NumCtr::Num(0))]));
+          debug_assert!(rules.len() == 2);
-          debug_assert!(matches!(rules[1].pats[..], [Pattern::Num(NumCtr::Succ(1, None))]));
+          debug_assert!(matches!(rules[0].0, NumCtr::Num(0)));
+          debug_assert!(matches!(rules[1].0, NumCtr::Succ(None)));
 
-          let if_ = self.inet.new_node(Mat);
+          let mat = self.inet.new_node(Mat);
 
-          let cond = self.encode_term(arg, Port(if_, 0));
+          let arg = self.encode_term(arg, Port(mat, 0));
-          self.link_local(Port(if_, 0), cond);
+          self.link_local(Port(mat, 0), arg);
 
-          let zero = &rules[0].body;
+          let zero = &rules[0].1;
-          let succ = &rules[1].body;
+          let succ = &rules[1].1;
 
           let sel = self.inet.new_node(Con { lab: None });
-          self.inet.link(Port(sel, 0), Port(if_, 1));
+          self.inet.link(Port(sel, 0), Port(mat, 1));
           let zero = self.encode_term(zero, Port(sel, 1));
           self.link_local(Port(sel, 1), zero);
 
           let succ = self.encode_term(succ, Port(sel, 2));
           self.link_local(Port(sel, 2), succ);
 
-          Some(Port(if_, 2))
+          Some(Port(mat, 2))
         }
         // A dup becomes a dup node too. Ports for dups of size 2:
         // - 0: points to the value projected.
@@ -189,24 +190,23 @@ impl EncodeTermState<'_> {
           self.inet.link(up, Port(node, 0));
           Some(Port(node, 0))
         }
-        Term::Let { pat: Pattern::Tup(args), val, nxt } => {
+        Term::Ltp { bnd, val, nxt } => {
-          let nams = args.iter().map(|arg| if let Pattern::Var(nam) = arg { nam } else { unreachable!() });
+          let (main, aux) = self.make_node_list(Tup, bnd.len());
-          let (main, aux) = self.make_node_list(Tup, args.len());
 
           let val = self.encode_term(val, main);
           self.link_local(main, val);
 
-          for (nam, aux) in nams.clone().zip(aux.iter()) {
+          for (nam, aux) in bnd.iter().zip(aux.iter()) {
             self.push_scope(nam, *aux);
           }
           let nxt = self.encode_term(nxt, up);
-          for (nam, aux) in nams.rev().zip(aux.iter().rev()) {
+          for (nam, aux) in bnd.iter().rev().zip(aux.iter().rev()) {
             self.pop_scope(nam, *aux);
           }
 
           nxt
         }
-        Term::Let { pat: Pattern::Var(None), val, nxt } => {
+        Term::Let { nam: None, val, nxt } => {
           let nod = self.inet.new_node(Era);
           let val = self.encode_term(val, Port(nod, 0));
 

src/term/transform/apply_args.rs

@@ -1,10 +1,8 @@
 use crate::{
-  diagnostics::{Diagnostics, ToStringVerbose},
+  diagnostics::Diagnostics,
-  term::{Ctx, Pattern, Term},
+  term::{Ctx, Pattern, Rule, Term},
 };
 
-struct PatternArgError(Pattern);
-
 impl Ctx<'_> {
   /// Applies the arguments to the program being run by applying them to the main function.
   ///
@@ -22,26 +20,35 @@ impl Ctx<'_> {
     if let Some(entrypoint) = &self.book.entrypoint {
       let main_def = &mut self.book.defs[entrypoint];
 
-      for pat in &main_def.rules[0].pats {
+      // Since we fatal error, no need to exit early
-        if !matches!(pat, Pattern::Var(Some(..))) {
+      let n_rules = main_def.rules.len();
-          self.info.add_rule_error(PatternArgError(pat.clone()), entrypoint.clone());
+      if n_rules != 1 {
+        self.info.add_rule_error(
+          format!("Expected the entrypoint function to have only one rule, found {n_rules}."),
+          entrypoint.clone(),
+        );
+      }
+
+      let mut main_body = std::mem::take(&mut main_def.rules[0].body);
+
+      for pat in main_def.rules[0].pats.iter().rev() {
+        if let Pattern::Var(var) = pat {
+          main_body = Term::lam(var.clone(), main_body);
+        } else {
+          self.info.add_rule_error(
+            format!("Expected the entrypoint function to only have variable patterns, found '{pat}'."),
+            entrypoint.clone(),
+          );
         }
       }
 
       if let Some(args) = args {
-        main_def.convert_match_def_to_term();
+        main_body = Term::call(main_body, args);
-        let main_body = &mut self.book.defs[entrypoint].rule_mut().body;
-
-        *main_body = Term::call(main_body.clone(), args);
       }
+
+      main_def.rules = vec![Rule { pats: vec![], body: main_body }];
     }
 
     self.info.fatal(())
   }
 }
-
-impl ToStringVerbose for PatternArgError {
-  fn to_string_verbose(&self, _verbose: bool) -> String {
-    format!("Expected the entrypoint to only have variable pattern, found '{}'.", self.0)
-  }
-}

src/term/transform/desugar_implicit_match_binds.rs

@@ -1,97 +0,0 @@
-use crate::term::{Adts, Book, Constructors, Name, NumCtr, Pattern, Term};
-
-impl Book {
-  /// Converts implicit match binds into explicit ones, using the
-  /// field names specified in the ADT declaration or the default
-  /// names for builtin constructors.
-  ///
-  /// Example:
-  /// ```hvm
-  /// data MyList = (Cons h t) | Nil
-  /// match x y {
-  ///   0 Nil: (A)
-  ///   0 Cons: (B y.h y.t)
-  ///   1+ Nil: (C x-1)
-  ///   1+p (Cons x xs): (D p x xs)
-  /// }
-  /// ```
-  /// becomes
-  /// ```hvm
-  /// match x y {
-  ///   0 Nil: (A)
-  ///   0 (Cons y.h y.t): (B y.h y.t)
-  ///   1+x-1 Nil: (C x-1)
-  ///   1+p (Cons x xs): (D p x xs)
-  /// }
-  /// ```
-  pub fn desugar_implicit_match_binds(&mut self) {
-    for def in self.defs.values_mut() {
-      for rule in &mut def.rules {
-        rule.body.desugar_implicit_match_binds(&self.ctrs, &self.adts);
-      }
-    }
-  }
-}
-
-impl Term {
-  pub fn desugar_implicit_match_binds(&mut self, ctrs: &Constructors, adts: &Adts) {
-    Term::recursive_call(move || {
-      for child in self.children_mut() {
-        child.desugar_implicit_match_binds(ctrs, adts);
-      }
-
-      if let Term::Mat { args, rules } = self {
-        // Make all the matched terms variables
-        let mut match_args = vec![];
-        for arg in args.iter_mut() {
-          if let Term::Var { nam } = arg {
-            match_args.push((nam.clone(), None))
-          } else {
-            let nam = Name::new(format!("%matched_{}", match_args.len()));
-            let arg = std::mem::replace(arg, Term::Var { nam: nam.clone() });
-            match_args.push((nam, Some(arg)));
-          }
-        }
-
-        // Make implicit match binds explicit
-        for rule in rules.iter_mut() {
-          for ((nam, _), pat) in match_args.iter().zip(rule.pats.iter_mut()) {
-            match pat {
-              Pattern::Var(_) => (),
-              Pattern::Ctr(ctr_nam, pat_args) => {
-                let adt = &adts[ctrs.get(ctr_nam).unwrap()];
-                let ctr_args = adt.ctrs.get(ctr_nam).unwrap();
-                if pat_args.is_empty() && !ctr_args.is_empty() {
-                  // Implicit ctr args
-                  *pat_args = ctr_args
-                    .iter()
-                    .map(|field| Pattern::Var(Some(Name::new(format!("{nam}.{field}")))))
-                    .collect();
-                }
-              }
-              Pattern::Num(NumCtr::Num(_)) => (),
-              Pattern::Num(NumCtr::Succ(_, Some(_))) => (),
-              Pattern::Num(NumCtr::Succ(n, p @ None)) => {
-                // Implicit num arg
-                *p = Some(Some(Name::new(format!("{nam}-{n}"))));
-              }
-              Pattern::Tup(..) => (),
-              Pattern::Lst(..) => (),
-              Pattern::Str(..) => (),
-            }
-          }
-        }
-
-        // Add the binds to the extracted term vars.
-        *self = match_args.into_iter().rfold(std::mem::take(self), |nxt, (nam, val)| {
-          if let Some(val) = val {
-            // Non-Var term that was extracted.
-            Term::Let { pat: Pattern::Var(Some(nam)), val: Box::new(val), nxt: Box::new(nxt) }
-          } else {
-            nxt
-          }
-        });
-      }
-    })
-  }
-}

src/term/transform/desugar_let_destructors.rs

@@ -1,41 +0,0 @@
-use crate::term::{Book, Name, Pattern, Rule, Term};
-
-impl Book {
-  /// Convert let destructor expressions like `let (a, b) = X` into the equivalent match expression.
-  pub fn desugar_let_destructors(&mut self) {
-    for def in self.defs.values_mut() {
-      for rule in &mut def.rules {
-        rule.body.desugar_let_destructors();
-      }
-    }
-  }
-}
-
-impl Term {
-  pub fn desugar_let_destructors(&mut self) {
-    Term::recursive_call(move || {
-      for child in self.children_mut() {
-        child.desugar_let_destructors();
-      }
-
-      if let Term::Let { pat, val, nxt } = self
-        && !pat.is_wildcard()
-      {
-        let pat = std::mem::replace(pat, Pattern::Var(None));
-        let val = std::mem::take(val);
-        let nxt = std::mem::take(nxt);
-
-        let rules = vec![Rule { pats: vec![pat], body: *nxt }];
-
-        *self = if let Term::Var { .. } = val.as_ref() {
-          Term::Mat { args: vec![*val], rules }
-        } else {
-          let nam = Name::from("%matched");
-          let pat = Pattern::Var(Some(nam.clone()));
-          let args = vec![Term::Var { nam }];
-          Term::Let { pat, val, nxt: Box::new(Term::Mat { args, rules }) }
-        };
-      }
-    })
-  }
-}

src/term/transform/desugar_match_defs.rs

@@ -0,0 +1,522 @@
+use std::collections::{BTreeSet, HashSet};
+
+use crate::{
+  diagnostics::{Diagnostics, ToStringVerbose, WarningType},
+  term::{builtins, Adts, Constructors, Ctx, Definition, Name, NumCtr, Pattern, Rule, Term},
+};
+
+pub enum DesugarMatchDefErr {
+  AdtNotExhaustive { adt: Name, ctr: Name },
+  NumMissingDefault,
+  TypeMismatch { expected: Type, found: Type, pat: Pattern },
+  RepeatedBind { bind: Name },
+}
+
+impl Ctx<'_> {
+  pub fn desugar_match_defs(&mut self) -> Result<(), Diagnostics> {
+    self.info.start_pass();
+
+    for (def_name, def) in self.book.defs.iter_mut() {
+      let errs = def.desugar_match_def(&self.book.ctrs, &self.book.adts);
+      for err in errs {
+        match err {
+          DesugarMatchDefErr::AdtNotExhaustive { .. }
+          | DesugarMatchDefErr::NumMissingDefault
+          | DesugarMatchDefErr::TypeMismatch { .. } => self.info.add_rule_error(err, def_name.clone()),
+          DesugarMatchDefErr::RepeatedBind { .. } => {
+            self.info.add_rule_warning(err, WarningType::RepeatedBind, def_name.clone())
+          }
+        }
+      }
+    }
+
+    self.info.fatal(())
+  }
+}
+
+impl Definition {
+  pub fn desugar_match_def(&mut self, ctrs: &Constructors, adts: &Adts) -> Vec<DesugarMatchDefErr> {
+    let mut errs = vec![];
+
+    let repeated_bind_errs = fix_repeated_binds(&mut self.rules);
+    errs.extend(repeated_bind_errs);
+
+    let args = (0 .. self.arity()).map(|i| Name::new(format!("%arg{i}"))).collect::<Vec<_>>();
+    let rules = std::mem::take(&mut self.rules);
+    match simplify_rule_match(args.clone(), rules, ctrs, adts) {
+      Ok(body) => {
+        let body = args.into_iter().rfold(body, |body, arg| Term::lam(Some(arg), body));
+        self.rules = vec![Rule { pats: vec![], body }];
+      }
+      Err(e) => errs.push(e),
+    }
+    errs
+  }
+}
+
+/// When a rule has repeated bind, the only one that is actually useful is the last one.
+///
+/// Example: In `(Foo x x x x) = x`, the function should return the fourth argument.
+///
+/// To avoid having to deal with this, we can just erase any repeated binds.
+/// ```hvm
+/// (Foo a (Succ a) (Cons a)) = (a a)
+/// // After this transformation, becomes:
+/// (Foo * (Succ *) (Cons a)) = (a a)
+/// ```
+fn fix_repeated_binds(rules: &mut [Rule]) -> Vec<DesugarMatchDefErr> {
+  let mut errs = vec![];
+  for rule in rules {
+    let mut binds = HashSet::new();
+    rule.pats.iter_mut().flat_map(|p| p.binds_mut()).rev().for_each(|nam| {
+      if binds.contains(nam) {
+        // Repeated bind, not reachable and can be erased.
+        if let Some(nam) = nam {
+          errs.push(DesugarMatchDefErr::RepeatedBind { bind: nam.clone() });
+        }
+        *nam = None;
+        // TODO: Send a repeated bind warning
+      } else {
+        binds.insert(&*nam);
+      }
+    });
+  }
+  errs
+}
+
+/// Creates the match tree for a given pattern matching function definition.
+/// For each constructor, a match case is created.
+///
+/// The match cases follow the same order as the order the constructors are in
+/// the ADT declaration.
+///
+/// If there are constructors of different types for the same arg, returns a type error.
+///
+/// If no patterns match one of the constructors, returns a non-exhaustive match error.
+///
+/// ===========================================================================
+///
+
+///
+/// Any nested subpatterns are extracted and moved into a nested match
+/// expression, together with the remaining match arguments.
+fn simplify_rule_match(
+  args: Vec<Name>,
+  mut rules: Vec<Rule>,
+  ctrs: &Constructors,
+  adts: &Adts,
+) -> Result<Term, DesugarMatchDefErr> {
+  if args.is_empty() {
+    Ok(std::mem::take(&mut rules[0].body))
+  } else if rules[0].pats.iter().all(|p| p.is_wildcard()) {
+    Ok(irrefutable_fst_row_rule(args, std::mem::take(&mut rules[0])))
+  } else {
+    let typ = Type::infer_from_def_arg(&rules, 0, ctrs)?;
+    match typ {
+      Type::Any => var_rule(args, rules, ctrs, adts),
+      Type::Tup(tup_len) => tup_rule(args, rules, tup_len, ctrs, adts),
+      Type::Num => num_rule(args, rules, ctrs, adts),
+      Type::Adt(adt_name) => switch_rule(args, rules, adt_name, ctrs, adts),
+    }
+  }
+}
+
+/// Irrefutable first row rule.
+/// Short-circuits the encoding in case the first rule always matches.
+/// This is useful to avoid unnecessary pattern matching.
+fn irrefutable_fst_row_rule(args: Vec<Name>, rule: Rule) -> Term {
+  let mut term = rule.body;
+  for (arg, pat) in args.into_iter().zip(rule.pats.into_iter()) {
+    let Pattern::Var(var) = pat else { unreachable!() };
+    if let Some(var) = var {
+      term.subst(&var, &Term::Var { nam: arg });
+    }
+  }
+  term
+}
+
+/// Var rule.
+/// `case x0 ... xN { var p1 ... pN: (Body var p1 ... pN) }`
+/// becomes
+/// `case x1 ... xN { p1 ... pN: use var = x0; (Body var p1 ... pN) }`
+fn var_rule(
+  mut args: Vec<Name>,
+  rules: Vec<Rule>,
+  ctrs: &Constructors,
+  adts: &Adts,
+) -> Result<Term, DesugarMatchDefErr> {
+  let arg = args[0].clone();
+  let new_args = args.split_off(1);
+
+  let mut new_rules = vec![];
+  for mut rule in rules {
+    let new_pats = rule.pats.split_off(1);
+    let pat = rule.pats.pop().unwrap();
+
+    if let Pattern::Var(Some(nam)) = &pat {
+      rule.body.subst(nam, &Term::Var { nam: arg.clone() });
+    }
+
+    let new_rule = Rule { pats: new_pats, body: rule.body };
+    new_rules.push(new_rule);
+  }
+
+  simplify_rule_match(new_args, new_rules, ctrs, adts)
+}
+
+/// Tuple rule.
+/// ```hvm
+/// case x0 ... xN {
+///   (p0_0, ... p0_M) p1 ... pN:
+///     (Body p0_0 ... p0_M p1 ... pN)
+/// }
+/// ```
+/// becomes
+/// ```hvm
+/// let (x0.0, ... x0.M) = x0;
+/// case x0.0 ... x0.M x1 ... xN {
+///   p0_0 ... p0_M p1 ... pN:
+///     (Body p0_0 ... p0_M p1 ... pN)
+/// }
+/// ```
+fn tup_rule(
+  mut args: Vec<Name>,
+  rules: Vec<Rule>,
+  tup_len: usize,
+  ctrs: &Constructors,
+  adts: &Adts,
+) -> Result<Term, DesugarMatchDefErr> {
+  let arg = args[0].clone();
+  let old_args = args.split_off(1);
+  let new_args = (0 .. tup_len).map(|i| Name::new(format!("{arg}.{i}")));
+
+  let mut new_rules = vec![];
+  for mut rule in rules {
+    let pat = rule.pats[0].clone();
+    let old_pats = rule.pats.split_off(1);
+
+    // Extract subpats from the tuple pattern
+    let mut new_pats = match pat {
+      Pattern::Tup(sub_pats) => sub_pats,
+      Pattern::Var(var) => {
+        if let Some(var) = var {
+          // Rebuild the tuple if it was a var pattern
+          let tup = Term::Tup { els: new_args.clone().map(|nam| Term::Var { nam }).collect() };
+          rule.body.subst(&var, &tup);
+        }
+        new_args.clone().map(|nam| Pattern::Var(Some(nam))).collect()
+      }
+      _ => unreachable!(),
+    };
+    new_pats.extend(old_pats);
+
+    let new_rule = Rule { pats: new_pats, body: rule.body };
+    new_rules.push(new_rule);
+  }
+
+  let bnd = new_args.clone().map(Some).collect();
+  let args = new_args.chain(old_args).collect();
+  let nxt = simplify_rule_match(args, new_rules, ctrs, adts)?;
+  let term = Term::Ltp { bnd, val: Box::new(Term::Var { nam: arg }), nxt: Box::new(nxt) };
+
+  Ok(term)
+}
+
+fn num_rule(
+  mut args: Vec<Name>,
+  rules: Vec<Rule>,
+  ctrs: &Constructors,
+  adts: &Adts,
+) -> Result<Term, DesugarMatchDefErr> {
+  // Number match must always have a default case
+  if !rules.iter().any(|r| r.pats[0].is_wildcard()) {
+    return Err(DesugarMatchDefErr::NumMissingDefault);
+  }
+
+  let arg = args[0].clone();
+  let args = args.split_off(1);
+
+  let match_var = Name::new(format!("{arg}%matched"));
+  let pred_var = Name::new(format!("{arg}%matched-1"));
+
+  // Since numbers have infinite (2^60) constructors, they require special treatment.
+  // We first iterate over each present number then get the default.
+  let nums = rules
+    .iter()
+    .filter_map(|r| if let Pattern::Num(n) = r.pats[0] { Some(n) } else { None })
+    .collect::<BTreeSet<_>>()
+    .into_iter()
+    .collect::<Vec<_>>();
+
+  // Number cases
+  let mut bodies = vec![];
+  for num in nums.iter() {
+    let mut new_rules = vec![];
+    for rule in rules.iter() {
+      match &rule.pats[0] {
+        Pattern::Num(n) if n == num => {
+          let body = rule.body.clone();
+          let rule = Rule { pats: rule.pats[1 ..].to_vec(), body };
+          new_rules.push(rule);
+        }
+        Pattern::Var(var) => {
+          let mut body = rule.body.clone();
+          if let Some(var) = var {
+            body.subst(var, &Term::Num { val: *num });
+          }
+          let rule = Rule { pats: rule.pats[1 ..].to_vec(), body };
+          new_rules.push(rule);
+        }
+        _ => (),
+      }
+    }
+    let body = simplify_rule_match(args.clone(), new_rules, ctrs, adts)?;
+    bodies.push(body);
+  }
+
+  // Default case
+  let mut new_rules = vec![];
+  for rule in rules {
+    if let Pattern::Var(var) = &rule.pats[0] {
+      let mut body = rule.body.clone();
+      if let Some(var) = var {
+        let last_num = *nums.last().unwrap();
+        let var_recovered = Term::add_num(Term::Var { nam: pred_var.clone() }, 1 + last_num);
+        body.subst(var, &var_recovered);
+      }
+      let rule = Rule { pats: rule.pats[1 ..].to_vec(), body };
+      new_rules.push(rule);
+    }
+  }
+  let default_body = simplify_rule_match(args, new_rules, ctrs, adts)?;
+
+  let term = bodies.into_iter().enumerate().rfold(default_body, |term, (i, body)| {
+    let zero = (NumCtr::Num(0), body);
+    let succ = (NumCtr::Succ(Some(pred_var.clone())), term);
+    let mut swt = Term::Swt { arg: Box::new(Term::Var { nam: match_var.clone() }), rules: vec![zero, succ] };
+
+    let val = if i > 0 {
+      // let %matched = (%matched-1 +1 +num_i-1 - num_i)
+      //  switch %matched { 0: body_i; _: acc }
+      // nums[i] >= nums[i-1]+1, so we do a sub here.
+      Term::sub_num(Term::Var { nam: pred_var.clone() }, nums[i] - 1 - nums[i - 1])
+    } else {
+      // let %matched = (arg -num_0);
+      //  switch %matched { 0: body_0; _: acc}
+      Term::sub_num(Term::Var { nam: arg.clone() }, nums[i])
+    };
+
+    if let Term::Var { .. } = &val {
+      // No need to create a let expression if it's just a rename.
+      // We know that the bound value is a uniquely named var, so we can subst.
+      swt.subst(&match_var, &val);
+      swt
+    } else {
+      Term::Let { nam: Some(match_var.clone()), val: Box::new(val), nxt: Box::new(swt) }
+    }
+  });
+
+  Ok(term)
+}
+
+/// When the first column has constructors, create a branch on the constructors
+/// of the first arg.
+///
+/// The extracted nested patterns and remaining args are handled recursively in
+/// a nested expression for each match arm.
+///
+/// If we imagine a complex match expression representing what's left of the
+/// encoding of a pattern matching function:
+/// ```hvm
+/// data MyType = (CtrA ctrA_field0 ... ctrA_fieldA) | (CtrB ctrB_field0 ... ctrB_fieldB) | CtrC | ...
+///
+/// case x0 ... xN {
+///   (CtrA p0_0_0 ... p0_A) p0_1 ... p0_N : (Body0 p0_0_0 ... p0_0_A p0_1 ... p0_N)
+///   ...
+///   varI pI_1 ... pI_N: (BodyI varI pI_1 ... pI_N)
+///   ...
+///   (CtrB pJ_0_0 ... pJ_0_B) pJ_1 ... pJ_N: (BodyJ pJ_0_0 ... pJ_0_B pJ_1 ... pJ_N)
+///   ...
+///   (CtrC) pK_1 ... pK_N: (BodyK p_1 ... pK_N)
+///   ...
+/// }
+/// ```
+/// is converted into
+/// ```hvm
+/// match x0 {
+///   CtrA: case x.ctrA_field0 ... x.ctrA_fieldA x1 ... xN {
+///     p0_0_0 ... p0_0_B p0_1 ... p0_N :
+///       (Body0 p0_0_0 ... p0_0_B )
+///     x.ctrA_field0 ... x.ctrA_fieldA pI_1 ... pI_N:
+///       use varI = (CtrA x.ctrA_field0 ... x.ctrA_fieldN); (BodyI varI pI_1 ... pI_N)
+///     ...
+///   }
+///   CtrB: case x.ctrB_field0 ... x.ctrB_fieldB x1 ... xN {
+///     x.ctrB_field0 ... x.ctrB_fieldB pI_1 ... pI_N:
+///       use varI = (CtrB x.ctrB_field0 ... x.ctrB_fieldB); (BodyI varI pI_1 ... pI_N)
+///     pJ_0_0 ... pJ_0_B pJ_1 ... pJ_N :
+///       (BodyJ pJ_0_0 ... pJ_0_B pJ_1 ... pJ_N)
+///     ...
+///   }
+///   CtrC: case * x1 ... xN {
+///     * pI_1 ... pI_N:
+///       use varI = CtrC; (BodyI varI pI_1 ... pI_N)
+///     * pK_1 ... pK_N:
+///       (BodyK p_1 ... pK_N)
+///     ...
+///   }
+///   ...
+/// }
+/// ```
+/// Where `case` represents a call of the [`simplify_rule_match`] function.
+fn switch_rule(
+  mut args: Vec<Name>,
+  rules: Vec<Rule>,
+  adt_name: Name,
+  ctrs: &Constructors,
+  adts: &Adts,
+) -> Result<Term, DesugarMatchDefErr> {
+  let arg = args[0].clone();
+  let old_args = args.split_off(1);
+
+  let mut new_arms = vec![];
+  for (ctr, fields) in &adts[&adt_name].ctrs {
+    let new_args = fields.iter().map(|f| Name::new(format!("{arg}.{f}")));
+    let args = new_args.clone().chain(old_args.clone()).collect();
+
+    let mut new_rules = vec![];
+    for rule in &rules {
+      let old_pats = rule.pats[1 ..].to_vec();
+      match &rule.pats[0] {
+        // Same ctr, extract subpats.
+        // (Ctr pat0_0 ... pat0_m) pat1 ... patN: body
+        // becomes
+        // pat0_0 ... pat0_m pat1 ... patN: body
+        Pattern::Ctr(found_ctr, new_pats) if ctr == found_ctr => {
+          let pats = new_pats.iter().cloned().chain(old_pats).collect();
+          let body = rule.body.clone();
+          let rule = Rule { pats, body };
+          new_rules.push(rule);
+        }
+        // Var, match and rebuild the constructor.
+        // var pat1 ... patN: body
+        // becomes
+        // arg0.field0 ... arg0.fieldM pat1 ... patN:
+        //   use var = (Ctr arg0.field0 ... arg0.fieldM); body
+        Pattern::Var(var) => {
+          let new_pats = new_args.clone().map(|n| Pattern::Var(Some(n)));
+          let pats = new_pats.chain(old_pats.clone()).collect();
+          let mut body = rule.body.clone();
+          let reconstructed_var =
+            Term::call(Term::Ref { nam: ctr.clone() }, new_args.clone().map(|nam| Term::Var { nam }));
+          if let Some(var) = var {
+            body.subst(var, &reconstructed_var);
+          }
+          let rule = Rule { pats, body };
+          new_rules.push(rule);
+        }
+        _ => (),
+      }
+    }
+
+    if new_rules.is_empty() {
+      return Err(DesugarMatchDefErr::AdtNotExhaustive { adt: adt_name, ctr: ctr.clone() });
+    }
+
+    let body = simplify_rule_match(args, new_rules, ctrs, adts)?;
+    new_arms.push((Some(ctr.clone()), new_args.map(Some).collect(), body));
+  }
+  let term = Term::Mat { arg: Box::new(Term::Var { nam: arg }), rules: new_arms };
+  Ok(term)
+}
+
+/// Pattern types.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum Type {
+  /// Variables/wildcards.
+  Any,
+  /// A native tuple.
+  Tup(usize),
+  /// A sequence of arbitrary numbers ending in a variable.
+  Num,
+  /// Adt constructors declared with the `data` syntax.
+  Adt(Name),
+}
+
+impl Type {
+  // Infers the type of a column of a pattern matrix, from the rules of a function def.
+  fn infer_from_def_arg(
+    rules: &[Rule],
+    arg_idx: usize,
+    ctrs: &Constructors,
+  ) -> Result<Type, DesugarMatchDefErr> {
+    let pats = rules.iter().map(|r| &r.pats[arg_idx]);
+    let mut arg_type = Type::Any;
+    for pat in pats {
+      arg_type = match (arg_type, pat.to_type(ctrs)) {
+        (Type::Any, found) => found,
+        (expected, Type::Any) => expected,
+
+        (Type::Adt(expected), Type::Adt(found)) if found == expected => Type::Adt(expected),
+
+        (Type::Num, Type::Num) => Type::Num,
+
+        (Type::Tup(a), Type::Tup(b)) if a == b => Type::Tup(a),
+
+        (expected, found) => {
+          return Err(DesugarMatchDefErr::TypeMismatch { expected, found, pat: pat.clone() });
+        }
+      };
+    }
+    Ok(arg_type)
+  }
+}
+
+impl Pattern {
+  fn to_type(&self, ctrs: &Constructors) -> Type {
+    match self {
+      Pattern::Var(_) => Type::Any,
+      Pattern::Ctr(ctr_nam, _) => {
+        let adt_nam = ctrs.get(ctr_nam).expect("Unknown constructor '{ctr_nam}'");
+        Type::Adt(adt_nam.clone())
+      }
+      Pattern::Tup(args) => Type::Tup(args.len()),
+      Pattern::Num(_) => Type::Num,
+      Pattern::Lst(..) => Type::Adt(builtins::LIST.into()),
+      Pattern::Str(..) => Type::Adt(builtins::STRING.into()),
+    }
+  }
+}
+
+impl std::fmt::Display for Type {
+  fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+    match self {
+      Type::Any => write!(f, "any"),
+      Type::Tup(n) => write!(f, "{n}-tuple"),
+      Type::Num => write!(f, "number"),
+      Type::Adt(nam) => write!(f, "{nam}"),
+    }
+  }
+}
+
+impl ToStringVerbose for DesugarMatchDefErr {
+  fn to_string_verbose(&self, _verbose: bool) -> String {
+    match self {
+      DesugarMatchDefErr::AdtNotExhaustive { adt, ctr } => {
+        format!("Non-exhaustive pattern matching rule. Constructor '{ctr}' of type '{adt}' not covered")
+      }
+      DesugarMatchDefErr::TypeMismatch { expected, found, pat } => {
+        format!(
+          "Type mismatch in pattern matching rule. Expected a constructor of type '{}', found '{}' with type '{}'.",
+          expected, pat, found
+        )
+      }
+      DesugarMatchDefErr::NumMissingDefault => {
+        "Non-exhaustive pattern matching rule. Default case of number type not covered.".to_string()
+      }
+      DesugarMatchDefErr::RepeatedBind { bind } => {
+        format!("Repeated bind in pattern matching rule: '{bind}'.")
+      }
+    }
+  }
+}

src/term/transform/encode_adts.rs

@@ -1,6 +1,7 @@
 use crate::term::{AdtEncoding, Book, Definition, Name, Rule, Tag, Term};
 
 impl Book {
+  /// Defines a function for each constructor in each ADT in the book.
   pub fn encode_adts(&mut self, adt_encoding: AdtEncoding) {
     let mut defs = vec![];
     for (adt_name, adt) in &self.adts {

src/term/transform/encode_match_terms.rs

@@ -1,96 +1,103 @@
-use crate::term::{
+use crate::term::{AdtEncoding, Book, Constructors, Name, NumCtr, Tag, Term};
-  check::type_check::infer_match_arg_type, AdtEncoding, Adts, Book, Constructors, Name, NumCtr, Pattern,
-  Rule, Tag, Term, Type,
-};
 
 impl Book {
-  /// Encodes simple pattern matching expressions in the book into
+  /// Encodes pattern matching expressions in the book into their
-  /// their native/core form.
+  /// native/core form. Must be run after [`Ctr::fix_match_terms`].
-  /// See [`super::simplify_matches::simplify_match_expression`] for
-  /// the meaning of "simple" used here.
   ///
   /// ADT matches are encoded based on `adt_encoding`.
   ///
   /// Num matches are encoded as a sequence of native num matches (on 0 and 1+).
   ///
   /// Var and pair matches become a let expression.
-  pub fn encode_simple_matches(&mut self, adt_encoding: AdtEncoding) {
+  pub fn encode_matches(&mut self, adt_encoding: AdtEncoding) {
     for def in self.defs.values_mut() {
       for rule in &mut def.rules {
-        rule.body.encode_simple_matches(&self.ctrs, &self.adts, adt_encoding);
+        rule.body.encode_matches(&self.ctrs, adt_encoding);
       }
     }
   }
 }
 
 impl Term {
-  pub fn encode_simple_matches(&mut self, ctrs: &Constructors, adts: &Adts, adt_encoding: AdtEncoding) {
+  pub fn encode_matches(&mut self, ctrs: &Constructors, adt_encoding: AdtEncoding) {
     Term::recursive_call(move || {
       for child in self.children_mut() {
-        child.encode_simple_matches(ctrs, adts, adt_encoding)
+        child.encode_matches(ctrs, adt_encoding)
       }
 
-      if let Term::Mat { .. } = self {
+      if let Term::Mat { arg, rules } = self {
-        debug_assert!(self.is_simple_match(ctrs, adts), "{self}");
+        let arg = std::mem::take(arg.as_mut());
-        let Term::Mat { args, rules } = self else { unreachable!() };
-        let arg = std::mem::take(&mut args[0]);
         let rules = std::mem::take(rules);
         *self = encode_match(arg, rules, ctrs, adt_encoding);
+      } else if let Term::Swt { arg, rules } = self {
+        let arg = std::mem::take(arg.as_mut());
+        let rules = std::mem::take(rules);
+        *self = encode_switch(arg, rules);
       }
     })
   }
 }
 
-fn encode_match(arg: Term, rules: Vec<Rule>, ctrs: &Constructors, adt_encoding: AdtEncoding) -> Term {
+fn encode_match(
-  let typ = infer_match_arg_type(&rules, 0, ctrs).unwrap();
+  arg: Term,
-  match typ {
+  rules: Vec<(Option<Name>, Vec<Option<Name>>, Term)>,
-    Type::Any | Type::Tup(_) => {
+  ctrs: &Constructors,
-      let fst_rule = rules.into_iter().next().unwrap();
+  adt_encoding: AdtEncoding,
-      encode_var(arg, fst_rule)
+) -> Term {
-    }
+  let adt = ctrs.get(rules[0].0.as_ref().unwrap()).unwrap();
-    Type::NumSucc(_) => encode_num_succ(arg, rules),
-    Type::Num => encode_num(arg, rules),
-    // ADT Encoding depends on compiler option
-    Type::Adt(adt) => encode_adt(arg, rules, adt, adt_encoding),
-  }
-}
 
-/// Just move the match into a let term
+  // ADT Encoding depends on compiler option
-fn encode_var(arg: Term, rule: Rule) -> Term {
+  match adt_encoding {
-  Term::Let { pat: rule.pats.into_iter().next().unwrap(), val: Box::new(arg), nxt: Box::new(rule.body) }
+    // (x @field1 @field2 ... body1  @field1 body2 ...)
+    AdtEncoding::Scott => {
+      let mut arms = vec![];
+      for rule in rules {
+        let body = rule.1.iter().cloned().rfold(rule.2, |bod, nam| Term::lam(nam, bod));
+        arms.push(body);
+      }
+      Term::call(arg, arms)
+    }
+    // #adt_name(x arm[0] arm[1] ...)
+    AdtEncoding::TaggedScott => {
+      let mut arms = vec![];
+      for rule in rules.into_iter() {
+        let body =
+          rule.1.iter().cloned().rfold(rule.2, |bod, nam| Term::tagged_lam(Tag::adt_name(adt), nam, bod));
+        arms.push(body);
+      }
+      Term::tagged_call(Tag::adt_name(adt), arg, arms)
+    }
+  }
 }
 
 /// Convert into a sequence of native matches, decrementing by 1 each match.
 /// match n {0: A; 1: B; 2+: (C n-2)} converted to
 /// match n {0: A; 1+: @%x match %x {0: B; 1+: @n-2 (C n-2)}}
-fn encode_num_succ(arg: Term, mut rules: Vec<Rule>) -> Term {
+fn encode_switch(arg: Term, mut rules: Vec<(NumCtr, Term)>) -> Term {
   let last_rule = rules.pop().unwrap();
 
   let match_var = Name::from("%x");
 
   // @n-2 (C n-2)
-  let Pattern::Num(NumCtr::Succ(_, Some(last_var))) = last_rule.pats.into_iter().next().unwrap() else {
+  let NumCtr::Succ(last_var) = last_rule.0 else { unreachable!() };
-    unreachable!()
+  let last_arm = Term::lam(last_var, last_rule.1);
-  };
-  let last_arm = Term::lam(last_var, last_rule.body);
 
   rules.into_iter().rfold(last_arm, |term, rule| {
-    let rules = vec![Rule { pats: vec![Pattern::Num(NumCtr::Num(0))], body: rule.body }, Rule {
+    let zero = (NumCtr::Num(0), rule.1);
-      pats: vec![Pattern::Num(NumCtr::Succ(1, None))],
+    let one = (NumCtr::Succ(None), term);
-      body: term,
+    let rules = vec![zero, one];
-    }];
 
-    let Pattern::Num(NumCtr::Num(num)) = rule.pats.into_iter().next().unwrap() else { unreachable!() };
+    let NumCtr::Num(num) = rule.0 else { unreachable!() };
     if num == 0 {
-      Term::Mat { args: vec![arg.clone()], rules }
+      Term::Swt { arg: Box::new(arg.clone()), rules }
     } else {
-      let mat = Term::Mat { args: vec![Term::Var { nam: match_var.clone() }], rules };
+      let swt = Term::Swt { arg: Box::new(Term::Var { nam: match_var.clone() }), rules };
-      Term::named_lam(match_var.clone(), mat)
+      Term::named_lam(match_var.clone(), swt)
     }
   })
 }
 
-/// Convert into a sequence of native matches on (- n num_case)
+/* /// Convert into a sequence of native matches on (- n num_case)
 /// match n {a: A; b: B; n: (C n)} converted to
 /// match (- n a) {0: A; 1+: @%p match (- %p b-a-1) { 0: B; 1+: @%p let n = (+ %p b+1); (C n)}}
 fn encode_num(arg: Term, mut rules: Vec<Rule>) -> Term {
@@ -109,7 +116,7 @@ fn encode_num(arg: Term, mut rules: Vec<Rule>) -> Term {
       // match (- n a) {0: A; 1+: ...}
       (None, Some(rule)) => {
         let Pattern::Num(NumCtr::Num(val)) = &rule.pats[0] else { unreachable!() };
-        Term::native_num_match(
+        Term::switch(
           Term::sub_num(arg.unwrap(), *val),
           rule.body,
           go(rules, last_rule, Some(*val), None),
@@ -123,7 +130,7 @@ fn encode_num(arg: Term, mut rules: Vec<Rule>) -> Term {
         let pred_nam = Name::from("%p");
         Term::named_lam(
           pred_nam.clone(),
-          Term::native_num_match(
+          Term::switch(
             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),
@@ -147,29 +154,4 @@ fn encode_num(arg: Term, mut rules: Vec<Rule>) -> Term {
   let last_rule = rules.pop().unwrap();
   go(rules.into_iter(), last_rule, None, Some(arg))
 }
-
+ */
-fn encode_adt(arg: Term, rules: Vec<Rule>, adt: Name, adt_encoding: AdtEncoding) -> Term {
-  match adt_encoding {
-    // (x @field1 @field2 ... body1  @field1 body2 ...)
-    AdtEncoding::Scott => {
-      let mut arms = vec![];
-      for rule in rules {
-        let body = rule.pats[0].binds().cloned().rfold(rule.body, |bod, nam| Term::lam(nam, bod));
-        arms.push(body);
-      }
-      Term::call(arg, arms)
-    }
-    // #adt_name(x arm[0] arm[1] ...)
-    AdtEncoding::TaggedScott => {
-      let mut arms = vec![];
-      for rule in rules.into_iter() {
-        let body = rule.pats[0]
-          .binds()
-          .cloned()
-          .rfold(rule.body, |bod, nam| Term::tagged_lam(Tag::adt_name(&adt), nam, bod));
-        arms.push(body);
-      }
-      Term::tagged_call(Tag::adt_name(&adt), arg, arms)
-    }
-  }
-}

src/term/transform/fix_match_terms.rs

@@ -0,0 +1,278 @@
+use crate::{
+  diagnostics::{Diagnostics, ToStringVerbose, WarningType},
+  term::{Adts, Constructors, Ctx, Name, NumCtr, Term},
+};
+use std::collections::HashMap;
+
+enum FixMatchErr {
+  AdtMismatch { expected: Name, found: Name, ctr: Name },
+  NonExhaustiveMatch { typ: Name, missing: Name },
+  NumMismatch { expected: NumCtr, found: NumCtr },
+  IrrefutableMatch { var: Option<Name> },
+  UnreachableMatchArms { var: Option<Name> },
+  ExtraSwitchArms,
+  RedundantArm { ctr: Name },
+}
+
+impl Ctx<'_> {
+  /// Convert all match and switch expressions to a normalized form.
+  /// * For matches, resolve the constructors and create the name of the field variables.
+  /// * For switches, resolve the succ case ("_") and create the name of the pred variable.
+  /// * If the match arg is not a variable, it is separated into a let expression and bound to "%matched"
+  /// * Check for redundant arms and non-exhaustive matches.
+  ///
+  /// Example:
+  /// For the program
+  /// ```hvm
+  /// data MyList = (Cons h t) | Nil
+  /// match x {
+  ///   Cons: (A x.h x.t)
+  ///   Nil: switch (Foo y) { 0: B; 1: C; _: D }
+  /// }
+  /// ```
+  /// The following AST transformations will be made:
+  /// * The binds `x.h` and `x.t` will be generated and stored in the match term.
+  /// * `(Foo y)`` will be put in a let expression, bound to the variable `%matched`;
+  /// * The bind `%matched-2` will be generated and stored in the switch term.
+  /// * If either was missing one of the match cases (a number or a constructor), we'd get an error.
+  /// * If either included one of the cases more than once (including wildcard patterns), we'd get a warning.
+  /// ```hvm
+  /// match x {
+  ///   Cons: (A x.h x.t)
+  ///   Nil: let %matched = (Foo y); switch %matched { 0: B; 1: C; _: D }
+  /// }
+  /// ```
+  pub fn fix_match_terms(&mut self) -> Result<(), Diagnostics> {
+    self.info.start_pass();
+
+    for def in self.book.defs.values_mut() {
+      for rule in def.rules.iter_mut() {
+        let errs = rule.body.fix_match_terms(&self.book.ctrs, &self.book.adts);
+
+        for err in errs {
+          match err {
+            FixMatchErr::ExtraSwitchArms { .. }
+            | FixMatchErr::AdtMismatch { .. }
+            | FixMatchErr::NumMismatch { .. }
+            | FixMatchErr::NonExhaustiveMatch { .. } => self.info.add_rule_error(err, def.name.clone()),
+
+            FixMatchErr::IrrefutableMatch { .. } => {
+              self.info.add_rule_warning(err, WarningType::IrrefutableMatch, def.name.clone())
+            }
+            FixMatchErr::UnreachableMatchArms { .. } => {
+              self.info.add_rule_warning(err, WarningType::UnreachableMatch, def.name.clone())
+            }
+            FixMatchErr::RedundantArm { .. } => {
+              self.info.add_rule_warning(err, WarningType::RedundantMatch, def.name.clone())
+            }
+          }
+        }
+      }
+    }
+
+    self.info.fatal(())
+  }
+}
+
+impl Term {
+  fn fix_match_terms(&mut self, ctrs: &Constructors, adts: &Adts) -> Vec<FixMatchErr> {
+    Term::recursive_call(move || {
+      let mut errs = Vec::new();
+
+      for child in self.children_mut() {
+        let mut e = child.fix_match_terms(ctrs, adts);
+        errs.append(&mut e);
+      }
+
+      if let Term::Mat { .. } = self {
+        self.fix_match(&mut errs, ctrs, adts);
+      } else if let Term::Swt { .. } = self {
+        self.fix_switch(&mut errs);
+      }
+
+      errs
+    })
+  }
+
+  fn fix_match(&mut self, errs: &mut Vec<FixMatchErr>, ctrs: &Constructors, adts: &Adts) {
+    let Term::Mat { arg, rules } = self else { unreachable!() };
+
+    let (arg_nam, arg) = extract_match_arg(arg);
+
+    // Normalize arms
+    if let Some(ctr_nam) = &rules[0].0
+      && let Some(adt_nam) = ctrs.get(ctr_nam)
+    {
+      let adt_ctrs = &adts[adt_nam].ctrs;
+
+      // For each arm, decide to which arm of the fixed match they map to.
+      let mut bodies = HashMap::<&Name, Option<Term>>::from_iter(adt_ctrs.iter().map(|(ctr, _)| (ctr, None)));
+      for rule_idx in 0 .. rules.len() {
+        if let Some(ctr_nam) = &rules[rule_idx].0
+          && let Some(found_adt) = ctrs.get(ctr_nam)
+        {
+          // Ctr arm
+          if found_adt == adt_nam {
+            let body = bodies.get_mut(ctr_nam).unwrap();
+            if body.is_none() {
+              // Use this rule for this constructor
+              *body = Some(rules[rule_idx].2.clone());
+            } else {
+              errs.push(FixMatchErr::RedundantArm { ctr: ctr_nam.clone() });
+            }
+          } else {
+            errs.push(FixMatchErr::AdtMismatch {
+              expected: adt_nam.clone(),
+              found: found_adt.clone(),
+              ctr: ctr_nam.clone(),
+            })
+          }
+        } else {
+          // Var arm
+          if rule_idx != rules.len() - 1 {
+            errs.push(FixMatchErr::UnreachableMatchArms { var: rules[rule_idx].0.clone() });
+            rules.truncate(rule_idx + 1);
+          }
+          // Use this rule for all remaining constructors
+          for (ctr, body) in bodies.iter_mut() {
+            if body.is_none() {
+              let mut new_body = rules[rule_idx].2.clone();
+              if let Some(var) = &rules[rule_idx].0 {
+                new_body.subst(var, &rebuild_ctr(&arg_nam, ctr, &adts[adt_nam].ctrs[&**ctr]));
+              }
+              *body = Some(new_body);
+            }
+          }
+
+          break;
+        }
+      }
+
+      // Build the match arms, with all constructors
+      let mut new_rules = vec![];
+      for (ctr, fields) in adt_ctrs.iter() {
+        let fields = fields.iter().map(|f| Some(match_field(&arg_nam, f))).collect::<Vec<_>>();
+        let body = if let Some(Some(body)) = bodies.remove(ctr) {
+          body
+        } else {
+          errs.push(FixMatchErr::NonExhaustiveMatch { typ: adt_nam.clone(), missing: ctr.clone() });
+          Term::Err
+        };
+        new_rules.push((Some(ctr.clone()), fields, body));
+      }
+      *rules = new_rules;
+    } else {
+      errs.push(FixMatchErr::IrrefutableMatch { var: rules[0].0.clone() });
+
+      let match_var = rules[0].0.take();
+      *self = std::mem::take(&mut rules[0].2);
+      if let Some(var) = match_var {
+        self.subst(&var, &Term::Var { nam: arg_nam.clone() });
+      }
+    }
+
+    *self = apply_arg(std::mem::take(self), arg_nam, arg);
+  }
+
+  /// For switches, the only necessary change is to add the implicit pred bind to the AST.
+  ///
+  /// Check that all numbers are in order and no cases are skipped.
+  /// Also check that we have a default case at the end, binding the pred.
+  fn fix_switch(&mut self, errs: &mut Vec<FixMatchErr>) {
+    let Term::Swt { arg, rules } = self else { unreachable!() };
+
+    let (arg_nam, arg) = extract_match_arg(arg);
+
+    let mut has_num = false;
+    let len = rules.len();
+    for i in 0 .. len {
+      let ctr = &mut rules[i].0;
+      match ctr {
+        NumCtr::Num(n) if i as u64 == *n => {
+          has_num = true;
+        }
+        NumCtr::Num(n) => {
+          errs.push(FixMatchErr::NumMismatch { expected: NumCtr::Num(i as u64), found: NumCtr::Num(*n) });
+          break;
+        }
+        NumCtr::Succ(pred) => {
+          if !has_num {
+            errs.push(FixMatchErr::NumMismatch {
+              expected: NumCtr::Num(i as u64),
+              found: NumCtr::Succ(pred.clone()),
+            });
+            break;
+          }
+          *pred = Some(Name::new(format!("{arg_nam}-{i}")));
+          if i != len - 1 {
+            errs.push(FixMatchErr::ExtraSwitchArms);
+            rules.truncate(i + 1);
+            break;
+          }
+        }
+      }
+    }
+
+    *self = apply_arg(std::mem::take(self), arg_nam, arg);
+  }
+}
+
+fn extract_match_arg(arg: &mut Term) -> (Name, Option<Term>) {
+  if let Term::Var { nam } = arg {
+    (nam.clone(), None)
+  } else {
+    let nam = Name::from("%matched");
+    let arg = std::mem::replace(arg, Term::Var { nam: nam.clone() });
+    (nam, Some(arg))
+  }
+}
+
+fn apply_arg(term: Term, arg_nam: Name, arg: Option<Term>) -> Term {
+  if let Some(arg) = arg {
+    Term::Let { nam: Some(arg_nam), val: Box::new(arg), nxt: Box::new(term) }
+  } else {
+    term
+  }
+}
+
+fn match_field(arg: &Name, field: &Name) -> Name {
+  Name::new(format!("{arg}.{field}"))
+}
+
+fn rebuild_ctr(arg: &Name, ctr: &Name, fields: &[Name]) -> Term {
+  let ctr = Term::Ref { nam: ctr.clone() };
+  let fields = fields.iter().map(|f| Term::Var { nam: match_field(arg, f) });
+  Term::call(ctr, fields)
+}
+
+impl ToStringVerbose for FixMatchErr {
+  fn to_string_verbose(&self, _verbose: bool) -> String {
+    match self {
+      FixMatchErr::AdtMismatch { expected, found, ctr } => format!(
+        "Type mismatch in 'match' expression: Expected a constructor of type '{expected}', found '{ctr}' of type '{found}'"
+      ),
+      FixMatchErr::NonExhaustiveMatch { typ, missing } => {
+        format!("Non-exhaustive 'match' expression of type '{typ}'. Case '{missing}' not covered.")
+      }
+      FixMatchErr::NumMismatch { expected, found } => {
+        format!(
+          "Malformed 'switch' expression. Expected case '{expected}', found '{found}'. Switch expressions must go from 0 to the desired value without skipping any cases and ending with the default case."
+        )
+      }
+      FixMatchErr::IrrefutableMatch { var } => format!(
+        "Irrefutable 'match' expression. All cases after '{}' will be ignored. If this is not a mistake, consider using a 'let' expression instead.",
+        var.as_ref().unwrap_or(&Name::new("*"))
+      ),
+      FixMatchErr::UnreachableMatchArms { var } => format!(
+        "Unreachable arms in 'match' expression. All cases after '{}' will be ignored.",
+        var.as_ref().unwrap_or(&Name::new("*"))
+      ),
+      FixMatchErr::ExtraSwitchArms => {
+        "Extra arms in 'switch' expression. No rules should come after the default.".to_string()
+      }
+      FixMatchErr::RedundantArm { ctr } => {
+        format!("Redundant arm in 'match' expression. Case '{ctr}' appears more than once.")
+      }
+    }
+  }
+}

src/term/transform/float_combinators.rs

@@ -141,7 +141,7 @@ impl Term {
 
 impl Term {
   pub fn float_children_mut(&mut self) -> impl DoubleEndedIterator<Item = &mut Term> {
-    multi_iterator!(FloatIter { Zero, Two, Vec, Mat, App });
+    multi_iterator!(FloatIter { Zero, Two, Vec, Mat, App, Swt });
     match self {
       Term::App { fun, arg, .. } => {
         let mut args = vec![arg.as_mut()];
@@ -153,11 +153,15 @@ impl Term {
         args.push(app);
         FloatIter::App(args)
       }
-      Term::Mat { args, rules } => {
+      Term::Mat { arg, rules } => {
-        FloatIter::Mat(args.iter_mut().chain(rules.iter_mut().map(|r| &mut r.body)))
+        FloatIter::Mat([arg.as_mut()].into_iter().chain(rules.iter_mut().map(|r| &mut r.2)))
+      }
+      Term::Swt { arg, rules } => {
+        FloatIter::Swt([arg.as_mut()].into_iter().chain(rules.iter_mut().map(|r| &mut r.1)))
       }
       Term::Tup { els } | Term::Sup { els, .. } | Term::Lst { els } => FloatIter::Vec(els),
-      Term::Let { val: fst, nxt: snd, .. }
+      Term::Ltp { val: fst, nxt: snd, .. }
+      | 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()]),

src/term/transform/inline.rs

@@ -53,9 +53,9 @@ impl Term {
         Term::Chn { .. } | Term::Lnk { .. } => false,
         Term::Let { .. } => false,
         Term::App { .. } => false,
-        Term::Dup { .. } => false,
+        Term::Dup { .. } | Term::Ltp { .. } => false,
         Term::Opx { .. } => false,
-        Term::Mat { .. } => false,
+        Term::Mat { .. } | Term::Swt { .. } => false,
         Term::Ref { .. } => false,
 
         Term::Nat { .. } | Term::Str { .. } | Term::Lst { .. } | Term::Use { .. } => unreachable!(),

src/term/transform/linearize_matches.rs

@@ -1,26 +1,25 @@
-use crate::term::{Book, Name, Term};
+use crate::term::{Book, Name, NumCtr, Term};
-use itertools::Itertools;
 use std::collections::{BTreeMap, BTreeSet};
 
 impl Book {
   /// Linearizes the variables between match cases, transforming them into combinators when possible.
-  pub fn linearize_simple_matches(&mut self, lift_all_vars: bool) {
+  pub fn linearize_matches(&mut self, lift_all_vars: bool) {
     for def in self.defs.values_mut() {
       for rule in def.rules.iter_mut() {
-        rule.body.linearize_simple_matches(lift_all_vars);
+        rule.body.linearize_matches(lift_all_vars);
       }
     }
   }
 }
 
 impl Term {
-  fn linearize_simple_matches(&mut self, lift_all_vars: bool) {
+  fn linearize_matches(&mut self, lift_all_vars: bool) {
     Term::recursive_call(move || {
       for child in self.children_mut() {
-        child.linearize_simple_matches(lift_all_vars);
+        child.linearize_matches(lift_all_vars);
       }
 
-      if let Term::Mat { .. } = self {
+      if matches!(self, Term::Mat { .. } | Term::Swt { .. }) {
         lift_match_vars(self, lift_all_vars);
       }
     })
@@ -33,43 +32,71 @@ impl Term {
 /// If `lift_all_vars`, acts on all variables found in the arms,
 /// Otherwise, only lift vars that are used on more than one arm.
 ///
-/// Obs: This does not interact unscoped variables
+/// Obs: This does not modify unscoped variables
 pub fn lift_match_vars(match_term: &mut Term, lift_all_vars: bool) -> &mut Term {
-  let Term::Mat { args: _, rules } = match_term else { unreachable!() };
+  // Collect match arms with binds
-
+  let arms: Vec<_> = match match_term {
-  let free = rules.iter().flat_map(|rule| {
+    Term::Mat { arg: _, rules } => {
-    rule
+      rules.iter().map(|(_, binds, body)| (binds.iter().flatten().cloned().collect(), body)).collect()
-      .body
+    }
-      .free_vars()
+    Term::Swt { arg: _, rules } => rules
-      .into_iter()
+      .iter()
-      .filter(|(name, _)| !rule.pats.iter().any(|p| p.binds().flatten().contains(name)))
+      .map(|(ctr, body)| match ctr {
-  });
+        NumCtr::Num(_) => (vec![], body),
-
+        NumCtr::Succ(None) => (vec![], body),
-  // Collect the vars.
+        NumCtr::Succ(Some(var)) => (vec![var.clone()], body),
-  // We need consistent iteration order.
-  let free_vars: BTreeSet<Name> = if lift_all_vars {
-    free.map(|(name, _)| name).collect()
-  } else {
-    free
-      .fold(BTreeMap::new(), |mut acc, (name, count)| {
-        *acc.entry(name).or_insert(0) += count.min(1);
-        acc
       })
+      .collect(),
+    _ => unreachable!(),
+  };
+
+  // Collect all free vars in the match arms
+  let mut free_vars = Vec::<Vec<_>>::new();
+  for (binds, body) in arms {
+    let mut arm_free_vars = body.free_vars();
+    for bind in binds {
+      arm_free_vars.remove(&bind);
+    }
+    free_vars.push(arm_free_vars.into_keys().collect());
+  }
+
+  // Collect the vars to lift
+  // We need consistent iteration order.
+  let vars_to_lift: BTreeSet<Name> = if lift_all_vars {
+    free_vars.into_iter().flatten().collect()
+  } else {
+    // If not lifting all vars, lift only those that are used in more than one arm.
+    let mut vars_to_lift = BTreeMap::<Name, u64>::new();
+    for free_vars in free_vars {
+      for free_var in free_vars {
+        *vars_to_lift.entry(free_var).or_default() += 1;
+      }
+    }
+    vars_to_lift
       .into_iter()
-      .filter(|(_, count)| *count >= 2)
+      .filter_map(|(var, arm_count)| if arm_count >= 2 { Some(var) } else { None })
-      .map(|(name, _)| name)
       .collect()
   };
 
   // Add lambdas to the arms
-  for rule in rules {
+  match match_term {
-    let old_body = std::mem::take(&mut rule.body);
+    Term::Mat { arg: _, rules } => {
-    rule.body = free_vars.iter().cloned().rfold(old_body, |body, nam| Term::named_lam(nam, body));
+      for rule in rules {
+        let old_body = std::mem::take(&mut rule.2);
+        rule.2 = vars_to_lift.iter().cloned().rfold(old_body, |body, nam| Term::named_lam(nam, body));
+      }
+    }
+    Term::Swt { arg: _, rules } => {
+      for rule in rules {
+        let old_body = std::mem::take(&mut rule.1);
+        rule.1 = vars_to_lift.iter().cloned().rfold(old_body, |body, nam| Term::named_lam(nam, body));
+      }
+    }
+    _ => unreachable!(),
   }
 
   // Add apps to the match
-  let old_match = std::mem::take(match_term);
+  *match_term = vars_to_lift.into_iter().fold(std::mem::take(match_term), Term::arg_call);
-  *match_term = free_vars.into_iter().fold(old_match, Term::arg_call);
 
   get_match_reference(match_term)
 }
@@ -81,7 +108,7 @@ fn get_match_reference(mut match_term: &mut Term) -> &mut Term {
   loop {
     match match_term {
       Term::App { tag: _, fun, arg: _ } => match_term = fun.as_mut(),
-      Term::Mat { .. } => return match_term,
+      Term::Swt { .. } | Term::Mat { .. } => return match_term,
       _ => unreachable!(),
     }
   }

src/term/transform/linearize_vars.rs

@@ -1,4 +1,4 @@
-use crate::term::{Book, Name, Pattern, Tag, Term};
+use crate::term::{Book, Name, Tag, Term};
 use std::collections::HashMap;
 
 /// Erases variables that weren't used, dups the ones that were used more than once.
@@ -36,7 +36,7 @@ impl Term {
 
 fn term_to_affine(term: &mut Term, var_uses: &mut HashMap<Name, u64>) {
   Term::recursive_call(move || match term {
-    Term::Let { pat: Pattern::Var(Some(nam)), val, nxt } => {
+    Term::Let { nam: Some(nam), val, nxt } => {
       // TODO: This is swapping the order of how the bindings are
       // used, since it's not following the usual AST order (first
       // val, then nxt). Doesn't change behaviour, but looks strange.
@@ -51,7 +51,7 @@ fn term_to_affine(term: &mut Term, var_uses: &mut HashMap<Name, u64>) {
             let val = std::mem::take(val);
             let nxt = std::mem::take(nxt);
 
-            *term = Term::Let { pat: Pattern::Var(None), val, nxt };
+            *term = Term::Let { nam: None, val, nxt };
           } else {
             *term = std::mem::take(nxt.as_mut());
           }
@@ -69,7 +69,7 @@ fn term_to_affine(term: &mut Term, var_uses: &mut HashMap<Name, u64>) {
       }
     }
 
-    Term::Let { pat: Pattern::Var(None), val, nxt } => {
+    Term::Let { nam: None, val, nxt } => {
       term_to_affine(nxt, var_uses);
 
       if val.has_unscoped() {

src/term/transform/match_defs_to_term.rs

@@ -1,55 +0,0 @@
-use crate::term::{Book, Definition, Name, Rule, Term};
-
-impl Book {
-  /// See [`Definition::convert_match_def_to_term`].
-  pub fn convert_match_def_to_term(&mut self) {
-    for def in self.defs.values_mut() {
-      def.convert_match_def_to_term();
-    }
-  }
-}
-
-impl Definition {
-  /// Converts a pattern matching function with multiple rules and args, into a
-  /// single rule without pattern matching.
-  ///
-  /// Moves the pattern matching of the rules into a complex match expression.
-  ///
-  /// Example:
-  ///
-  /// ```hvm
-  /// if True then else = then
-  /// if False then else = else
-  /// ```
-  ///
-  /// becomes
-  ///
-  /// ```hvm
-  /// if = @%x0 @%x1 @%x2 match %x0, %x1, %x2 {
-  ///   True then else: then
-  ///   False then else: else
-  /// }
-  /// ```
-  ///
-  /// Preconditions: Rule arities must be correct.
-  pub fn convert_match_def_to_term(&mut self) {
-    let rule = def_rules_to_match(std::mem::take(&mut self.rules));
-    self.rules = vec![rule];
-  }
-}
-
-fn def_rules_to_match(rules: Vec<Rule>) -> Rule {
-  let arity = rules[0].arity();
-
-  if arity == 0 {
-    // If no args, not pattern matching function, nothings needs to be done.
-    rules.into_iter().next().unwrap()
-  } else {
-    let nams = (0 .. arity).map(|i| Name::new(format!("%x{i}")));
-
-    let args = nams.clone().map(|nam| Term::Var { nam }).collect();
-    let mat = Term::Mat { args, rules };
-    let body = nams.rfold(mat, |bod, nam| Term::named_lam(nam, bod));
-    Rule { pats: vec![], body }
-  }
-}

src/term/transform/mod.rs

@@ -2,21 +2,19 @@ pub mod apply_args;
 pub mod apply_use;
 pub mod definition_merge;
 pub mod definition_pruning;
-pub mod desugar_implicit_match_binds;
+pub mod desugar_match_defs;
-pub mod desugar_let_destructors;
 pub mod encode_adts;
-pub mod encode_pattern_matching;
+pub mod encode_match_terms;
 pub mod eta_reduction;
+pub mod fix_match_terms;
 pub mod float_combinators;
 pub mod inline;
 pub mod linearize_matches;
 pub mod linearize_vars;
-pub mod match_defs_to_term;
 pub mod resolve_ctrs_in_pats;
 pub mod resolve_refs;
 pub mod resugar_adts;
 pub mod resugar_builtins;
 pub mod simplify_main_ref;
-pub mod simplify_matches;
 pub mod simplify_ref_to_ref;
 pub mod unique_names;

src/term/transform/resolve_ctrs_in_pats.rs

@@ -1,4 +1,4 @@
-use crate::term::{Book, Name, Pattern, Term};
+use crate::term::{Book, Name, Pattern};
 
 impl Book {
   /// Resolve Constructor names inside rule patterns and match patterns,
@@ -15,7 +15,6 @@ impl Book {
         for pat in &mut rule.pats {
           pat.resolve_ctrs(&is_ctr);
         }
-        rule.body.resolve_ctrs_in_pats(&is_ctr);
       }
     }
   }
@@ -36,18 +35,3 @@ impl Pattern {
     }
   }
 }
-
-impl Term {
-  pub fn resolve_ctrs_in_pats(&mut self, is_ctr: &impl Fn(&Name) -> bool) {
-    let mut to_resolve = vec![self];
-
-    while let Some(term) = to_resolve.pop() {
-      for pat in term.patterns_mut() {
-        pat.resolve_ctrs(is_ctr);
-      }
-      for child in term.children_mut() {
-        to_resolve.push(child);
-      }
-    }
-  }
-}

src/term/transform/resugar_adts.rs

@@ -1,11 +1,13 @@
+use std::collections::VecDeque;
+
 use crate::{
   diagnostics::ToStringVerbose,
-  term::{Adt, AdtEncoding, Book, Name, Pattern, Rule, Tag, Term},
+  term::{Adt, AdtEncoding, Book, Name, Tag, Term},
 };
 
 pub enum AdtReadbackError {
-  InvalidAdt,
+  MalformedCtr(Name),
-  InvalidAdtMatch,
+  MalformedMatch(Name),
   UnexpectedTag(Tag, Tag),
 }
 
@@ -73,12 +75,13 @@ impl Term {
     let mut app = &mut *self;
     let mut current_arm = None;
 
+    // One lambda per ctr of this adt
     for ctr in &adt.ctrs {
       match app {
         Term::Lam { tag: Tag::Named(tag), nam, bod } if tag == adt_name => {
           if let Some(nam) = nam {
             if current_arm.is_some() {
-              errs.push(AdtReadbackError::InvalidAdt);
+              errs.push(AdtReadbackError::MalformedCtr(adt_name.clone()));
               return;
             }
             current_arm = Some((nam.clone(), ctr));
@@ -86,19 +89,20 @@ impl Term {
           app = bod;
         }
         _ => {
-          errs.push(AdtReadbackError::InvalidAdt);
+          errs.push(AdtReadbackError::MalformedCtr(adt_name.clone()));
           return;
         }
       }
     }
 
     let Some((arm_name, (ctr, ctr_args))) = current_arm else {
-      errs.push(AdtReadbackError::InvalidAdt);
+      errs.push(AdtReadbackError::MalformedCtr(adt_name.clone()));
       return;
     };
 
     let mut cur = &mut *app;
 
+    // One app per field of this constructor
     for _ in ctr_args.iter().rev() {
       let expected_tag = Tag::adt_name(adt_name);
 
@@ -113,7 +117,7 @@ impl Term {
           return;
         }
         _ => {
-          errs.push(AdtReadbackError::InvalidAdt);
+          errs.push(AdtReadbackError::MalformedCtr(adt_name.clone()));
           return;
         }
       }
@@ -122,7 +126,7 @@ impl Term {
     match cur {
       Term::Var { nam } if nam == &arm_name => {}
       _ => {
-        errs.push(AdtReadbackError::InvalidAdt);
+        errs.push(AdtReadbackError::MalformedCtr(adt_name.clone()));
         return;
       }
     }
@@ -140,7 +144,7 @@ impl Term {
   /// ```hvm
   /// data Option = (Some val) | None
   ///
-  /// // This match expression:
+  /// // Compiling this match expression:
   /// Option.and = @a @b match a {
   ///   Some: match b {
   ///     Some: 1
@@ -154,11 +158,11 @@ impl Term {
   ///
   /// // Which gets resugared as:
   /// λa λb (match a {
-  ///   (Some *): λc match c {
+  ///   Some: λc match c {
-  ///     (Some *): 1;
+  ///     Some: 1;
-  ///     (None)  : 2
+  ///     None: 2
   ///   };
-  ///   (None): λ* 3
+  ///   None: λ* 3
   /// } b)
   /// ```
   fn resugar_match_tagged_scott(
@@ -168,61 +172,119 @@ impl Term {
     adt: &Adt,
     errs: &mut Vec<AdtReadbackError>,
   ) {
-    let mut cur = &mut *self;
+    // TODO: This is too complex, refactor this.
-    let mut arms = Vec::new();
 
+    let mut cur = &mut *self;
+    let mut arms = VecDeque::new();
+    // Since we don't have access to the match arg when first reading
+    // the arms, we must store the position of the fields that have
+    // to be applied to the arm body.
+    let expected_tag = Tag::adt_name(adt_name);
+
+    // For each match arm, we expect an application where the arm body is the app arg.
+    // If matching a constructor with N fields, the body should start with N tagged lambdas.
     for (ctr, ctr_args) in adt.ctrs.iter().rev() {
       match cur {
         Term::App { tag: Tag::Named(tag), fun, arg } if tag == adt_name => {
-          let mut args = Vec::new();
+          // We expect a lambda for each field. If we got anything
+          // else, we have to create an eta-reducible match to get
+          // the same behaviour.
+          let mut has_all_fields = true;
+          let mut fields = Vec::new();
           let mut arm = arg.as_mut();
-
+          for _ in ctr_args.iter() {
-          for field in ctr_args {
-            let expected_tag = Tag::adt_name(adt_name);
-
             match arm {
               Term::Lam { tag, .. } if tag == &expected_tag => {
                 let Term::Lam { nam, bod, .. } = arm else { unreachable!() };
+                fields.push(nam.clone());
+                arm = bod;
+              }
 
-                args.push(nam.clone().map_or(Pattern::Var(None), |x| Pattern::Var(Some(x))));
+              Term::Lam { tag, .. } => {
-                arm = bod.as_mut();
+                errs.push(AdtReadbackError::UnexpectedTag(expected_tag.clone(), tag.clone()));
+                has_all_fields = false;
+                break;
               }
               _ => {
-                if let Term::Lam { tag, .. } = arm {
+                has_all_fields = false;
-                  errs.push(AdtReadbackError::UnexpectedTag(expected_tag.clone(), tag.clone()));
+                break;
-                }
-
-                let arg = Name::new(format!("{ctr}.{field}"));
-                args.push(Pattern::Var(Some(arg.clone())));
-                *arm = Term::tagged_app(expected_tag, std::mem::take(arm), Term::Var { nam: arg });
               }
             }
           }
 
-          arms.push((vec![Pattern::Ctr(ctr.clone(), args)], arm));
+          if has_all_fields {
+            arm.resugar_tagged_scott(book, errs);
+            arms.push_front((Some(ctr.clone()), fields, std::mem::take(arm)));
+          } else {
+            // If we didn't find lambdas for all the fields, create the eta-reducible match.
+            arg.resugar_tagged_scott(book, errs);
+            let fields = ctr_args.iter().map(|f| Name::new(format!("%{f}")));
+            let applied_arm = Term::tagged_call(
+              expected_tag.clone(),
+              std::mem::take(arg.as_mut()),
+              fields.clone().map(|f| Term::Var { nam: f }),
+            );
+            arms.push_front((Some(ctr.clone()), fields.map(Some).collect(), applied_arm));
+          }
+
           cur = &mut *fun;
         }
         _ => {
-          errs.push(AdtReadbackError::InvalidAdtMatch);
+          // Looked like a match but doesn't cover all constructors.
+          errs.push(AdtReadbackError::MalformedMatch(adt_name.clone()));
           return;
         }
       }
     }
 
-    let args = vec![std::mem::take(cur)];
+    // Resugar the argument.
-    let rules =
+    cur.resugar_tagged_scott(book, errs);
-      arms.into_iter().rev().map(|(pats, term)| Rule { pats, body: std::mem::take(term) }).collect();
-    *self = Term::Mat { args, rules };
 
-    self.resugar_tagged_scott(book, errs);
+    // If the match is on a non-var we have to extract it to get usable ctr fields.
+    // Here we get the arg name and separate the term if it's not a variable.
+    let (arg, bind) = if let Term::Var { nam } = cur {
+      (nam.clone(), None)
+    } else {
+      (Name::from("%matched"), Some(std::mem::take(cur)))
+    };
+
+    // Subst the unique readback names for the field names.
+    // ex: reading `@a(a @b@c(b c))` we create `@a match a{A: (a.field1 a.field2)}`,
+    // changing `b` to `a.field1` and `c` to `a.field2`.
+    for (ctr, fields, body) in arms.iter_mut() {
+      let mut new_fields = vec![];
+      for (field_idx, field) in fields.iter().enumerate() {
+        if let Some(old_field) = field {
+          let field_name = &adt.ctrs[ctr.as_ref().unwrap()][field_idx];
+          let new_field = Name::new(format!("{arg}.{field_name}"));
+          new_fields.push(Some(new_field.clone()));
+          body.subst(old_field, &Term::Var { nam: new_field });
+        }
+      }
+      *fields = new_fields;
+    }
+
+    let arms = arms.into_iter().collect::<Vec<_>>();
+
+    *self = if let Some(bind) = bind {
+      Term::Let {
+        nam: Some(arg.clone()),
+        val: Box::new(bind),
+        nxt: Box::new(Term::Mat { arg: Box::new(Term::Var { nam: arg }), rules: arms }),
+      }
+    } else {
+      Term::Mat { arg: Box::new(Term::Var { nam: arg }), rules: arms }
+    };
   }
 }
 
 impl ToStringVerbose for AdtReadbackError {
   fn to_string_verbose(&self, _verbose: bool) -> String {
     match self {
-      AdtReadbackError::InvalidAdt => "Invalid Adt.".to_string(),
+      AdtReadbackError::MalformedCtr(adt) => format!("Encountered malformed constructor of type '{adt}'."),
-      AdtReadbackError::InvalidAdtMatch => "Invalid Adt Match.".to_string(),
+      AdtReadbackError::MalformedMatch(adt) => {
+        format!("Encountered malformed 'match' expression of type '{adt}'")
+      }
       AdtReadbackError::UnexpectedTag(expected, found) => {
         let found = if let Tag::Static = found { "no tag".to_string() } else { format!("'{found}'") };
         format!("Unexpected tag found during Adt readback, expected '{}', but found {}.", expected, found)

src/term/transform/simplify_matches.rs

@@ -1,459 +0,0 @@
-use crate::{
-  diagnostics::{Diagnostics, ToStringVerbose, ERR_INDENT_SIZE},
-  term::{
-    check::type_check::{infer_match_arg_type, TypeMismatchErr},
-    display::{DisplayFn, DisplayJoin},
-    Adts, Constructors, Ctx, Definition, Name, NumCtr, Pattern, Rule, Term, Type,
-  },
-};
-use indexmap::IndexSet;
-use itertools::Itertools;
-
-pub enum SimplifyMatchErr {
-  NotExhaustive(Vec<Name>),
-  TypeMismatch(TypeMismatchErr),
-  MalformedNumSucc(Pattern, Pattern),
-}
-
-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, name_gen);
-      self.info.take_rule_err(res, def_name.clone());
-    }
-
-    self.info.fatal(())
-  }
-}
-
-impl Definition {
-  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)?;
-    }
-    Ok(())
-  }
-}
-
-impl Term {
-  /// Converts match expressions with multiple matched arguments and
-  /// 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,
-    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, name_gen)?;
-          *self = bind_extracted_args(extracted, term);
-        }
-
-        _ => {
-          for child in self.children_mut() {
-            child.simplify_matches(ctrs, adts, name_gen)?;
-          }
-        }
-      }
-      Ok(())
-    })
-  }
-}
-
-/// Given the values held by a match expression, separates a simple, non-nested
-/// match out of the first argument of the given match.
-///
-/// If there are constructors of different types, returns a type error.
-///
-/// If no patterns match one of the constructors, returns a non-exhaustive match error.
-///
-/// Invariant: All the match arg terms are variables.
-///
-/// ===========================================================================
-///
-/// For each constructor, a match case is created. It has only a single simple
-/// pattern with the constructor and no subpatterns.
-///
-/// The match cases follow the same order as the order the constructors are in
-/// the ADT declaration.
-///
-/// Any nested subpatterns are extracted and moved into a nested match
-/// expression, together with the remaining match arguments.
-///
-/// For Var matches, we skip creating the surrounding match term since it's
-/// redundant. (would be simply match x {x: ...})
-fn simplify_match_expression(
-  args: Vec<Term>,
-  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, name_gen)
-  } else if fst_col_type == Type::Any {
-    var_rule(args, rules, ctrs, adts, name_gen)
-  } else {
-    switch_rule(args, rules, fst_col_type, ctrs, adts, name_gen)
-  }
-}
-
-/// Irrefutable row rule.
-/// An optimization to not generate unnecessary pattern matching when we
-/// know the first case always matches.
-fn irrefutable_fst_row_rule(
-  args: Vec<Term>,
-  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, name_gen)?;
-
-  for (pat, arg) in pats.iter().zip(args.iter()) {
-    for bind in pat.binds().flatten() {
-      term.subst(bind, arg);
-    }
-  }
-
-  Ok(term)
-}
-
-/// Var rule.
-/// Could be merged with the ctr rule, but this is slightly simpler.
-/// `match x0 ... xN { var p1 ... pN: (Body var p1 ... pN) }`
-/// becomes
-/// `match x1 ... xN { p1 ... pN: let var = x0; (Body var p1 ... pN) }`
-fn var_rule(
-  mut args: Vec<Term>,
-  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 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);
-  }
-
-  let rest = args.split_off(1);
-  let mut term = Term::Mat { args: rest, rules: new_rules };
-  term.simplify_matches(ctrs, adts, name_gen)?;
-  Ok(term)
-}
-
-/// When the first column has constructors, create a branch on the constructors
-/// of the first match arg.
-///
-/// Each created match case has another nested match
-/// expression to deal with the extracted nested patterns and remaining args.
-///
-/// ```hvm
-/// match x0 ... xN {
-///   (CtrA p0_0_0 ... p0_A) p0_1 ... p0_N : (Body0 p0_0_0 ... p0_0_A p0_1 ... p0_N)
-///   ...
-///   varI pI_1 ... pI_N: (BodyI varI pI_1 ... pI_N)
-///   ...
-///   (CtrB pJ_0_0 ... pJ_0_B) pJ_1 ... pJ_N: (BodyJ pJ_0_0 ... pJ_0_B pJ_1 ... pJ_N)
-///   ...
-///   (CtrC) pK_1 ... pK_N: (BodyK p_1 ... pK_N)
-///   ...
-/// }
-/// ```
-/// is converted into
-/// ```hvm
-/// match x0 {
-///   (CtrA x0%ctrA_field0 ... x%ctrA_fieldA): match x%ctrA_field0 ... x%ctrA_fieldN x1 ... xN {
-///     p0_0_0 ... p0_0_B p0_1 ... p0_N :
-///       (Body0 p0_0_0 ... p0_0_B )
-///     x%ctrA_field0 ... x%ctrA_fieldA pI_1 ... pI_N:
-///       let varI = (CtrA x%ctrA_field0 ... x%ctrA_fieldN); (BodyI varI pI_1 ... pI_N)
-///     ...
-///   }
-///   (CtrB x%ctrB_field0 ... x%ctrB_fieldB): match x%ctrB_field0 ... x%ctrB_fieldB x1 ... xN {
-///     x%ctrB_field0 ... x%ctrB_fieldB pI_1 ... pI_N:
-///       let varI = (CtrB x%ctrB_field0 ... x%ctrB_fieldB); (BodyI varI pI_1 ... pI_N)
-///     pJ_0_0 ... pJ_0_B pJ_1 ... pJ_N :
-///       (BodyJ pJ_0_0 ... pJ_0_B pJ_1 ... pJ_N)
-///     ...
-///   }
-///   (CtrC): match * x1 ... xN {
-///     * pI_1 ... pI_N:
-///       let varI = CtrC; (BodyI varI pI_1 ... pI_N)
-///     * pK_1 ... pK_N:
-///       (BodyK p_1 ... pK_N)
-///     ...
-///   }
-///   ...
-/// }
-/// ```
-fn switch_rule(
-  mut args: Vec<Term>,
-  rules: Vec<Rule>,
-  typ: Type,
-  ctrs: &Constructors,
-  adts: &Adts,
-  name_gen: &mut usize,
-) -> Result<Term, SimplifyMatchErr> {
-  let mut new_rules = vec![];
-
-  let adt_ctrs = match typ {
-    Type::Num => {
-      // Since numbers have infinite (2^60) constructors, they require special treatment.
-      let mut ctrs = IndexSet::new();
-      for rule in &rules {
-        ctrs.insert(rule.pats[0].clone());
-        if rule.pats[0].is_wildcard() {
-          break;
-        }
-      }
-
-      Vec::from_iter(ctrs)
-    }
-    _ => typ.ctrs(adts),
-  };
-
-  // Check valid number match
-  match typ {
-    Type::Num => {
-      // Number match without + must have a default case
-      if !rules.iter().any(|r| r.pats[0].is_wildcard()) {
-        return Err(SimplifyMatchErr::NotExhaustive(vec![Name::from("+")]));
-      }
-    }
-    Type::NumSucc(exp) => {
-      // Number match with + can't have number larger than that in the +
-      // TODO: could be just a warning.
-      for rule in &rules {
-        if let Pattern::Num(NumCtr::Num(got)) = rule.pats[0]
-          && got >= exp
-        {
-          return Err(SimplifyMatchErr::MalformedNumSucc(
-            rule.pats[0].clone(),
-            Pattern::Num(NumCtr::Succ(exp, None)),
-          ));
-        }
-      }
-    }
-    _ => (),
-  }
-
-  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, 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, name_gen)?;
-    let pats = vec![matched_ctr];
-    new_rules.push(Rule { pats, body });
-  }
-  args.truncate(1);
-  let term = Term::Mat { args, rules: new_rules };
-  Ok(term)
-}
-
-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_gen}"))
-    } else {
-      // Name of var pattern
-      arg_nam.clone()
-    };
-    nested_fields.push(Some(new_nam));
-  }
-  if nested_fields.is_empty() {
-    // We say that a unit variant always has an unused wildcard nested
-    nested_fields.push(None);
-  }
-  nested_fields
-}
-
-fn switch_rule_matched_ctr(mut ctr: Pattern, nested_fields: &[Option<Name>]) -> Pattern {
-  let mut nested_fields = nested_fields.iter().cloned();
-  ctr.binds_mut().for_each(|var| *var = nested_fields.next().unwrap());
-  ctr
-}
-
-fn switch_rule_submatch(
-  args: &[Term],
-  rules: &[Rule],
-  ctr: &Pattern,
-  nested_fields: &[Option<Name>],
-) -> Result<Term, SimplifyMatchErr> {
-  // Create the nested match expression.
-  let new_args = nested_fields.iter().cloned().map(Term::var_or_era);
-  let old_args = args[1 ..].iter().cloned();
-  let args = new_args.clone().chain(old_args).collect::<Vec<_>>();
-
-  // Make the match cases of the nested submatch, filtering out the rules
-  // that don't match the current ctr.
-  let rules =
-    rules.iter().filter_map(|rule| switch_rule_submatch_arm(rule, ctr, nested_fields)).collect::<Vec<_>>();
-
-  if rules.is_empty() {
-    // TODO: Return the full pattern
-    return Err(SimplifyMatchErr::NotExhaustive(vec![ctr.ctr_name().unwrap()]));
-  }
-
-  let mat = Term::Mat { args, rules };
-  Ok(mat)
-}
-
-/// Make one of the cases of the nested submatch of a switch case.
-/// Returns None if the rule doesn't match the constructor.
-fn switch_rule_submatch_arm(rule: &Rule, ctr: &Pattern, nested_fields: &[Option<Name>]) -> Option<Rule> {
-  if rule.pats[0].simple_equals(ctr) {
-    // Same ctr, extract the patterns.
-    // match x ... {(Ctr p0_0...) ...: Body; ...}
-    // becomes
-    // match x {(Ctr x%field0 ...): match x1 ... {p0_0 ...: Body; ...}; ...}
-    let mut pats = match &rule.pats[0] {
-      // Since the variable in the succ ctr is not a nested pattern, we need this special case.
-      Pattern::Num(NumCtr::Succ(_, Some(var))) => vec![Pattern::Var(var.clone())],
-      // Similarly for the default case in a num match
-      Pattern::Var(var) => vec![Pattern::Var(var.clone())],
-      _ => rule.pats[0].children().cloned().collect::<Vec<_>>(),
-    };
-    if pats.is_empty() {
-      // We say that a unit variant always has an unused wildcard nested
-      pats.push(Pattern::Var(None));
-    }
-    pats.extend(rule.pats[1 ..].iter().cloned());
-    let body = rule.body.clone();
-    Some(Rule { pats, body })
-  } else if rule.pats[0].is_wildcard() {
-    // 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());
-    }
-
-    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();
-
-    Some(Rule { pats, body })
-  } else {
-    // Non-matching constructor. Don't include in submatch expression.
-    None
-  }
-}
-
-/// Swaps non-Var arguments in a match by vars with generated names,
-/// returning a vec with the extracted args and what they were replaced by.
-///
-/// `match Term {...}` => `match %match_arg0 {...}` + `vec![(%match_arg0, Term)])`
-fn extract_args(args: &mut [Term]) -> Vec<(Name, Term)> {
-  let mut extracted = vec![];
-
-  for (i, arg) in args.iter_mut().enumerate() {
-    if !matches!(arg, Term::Var { .. }) {
-      let nam = Name::new(format!("%match_arg{i}"));
-      let new_arg = Term::Var { nam: nam.clone() };
-      let old_arg = std::mem::replace(arg, new_arg);
-      extracted.push((nam, old_arg));
-    }
-  }
-  extracted
-}
-
-/// Binds the arguments that were extracted from a match with [`extract_args`];
-///
-/// `vec![(%match_arg0, arg)]` + `term` => `let %match_arg0 = arg; term`
-fn bind_extracted_args(extracted: Vec<(Name, Term)>, term: Term) -> Term {
-  extracted.into_iter().rfold(term, |term, (nam, val)| Term::Let {
-    pat: Pattern::Var(Some(nam)),
-    val: Box::new(val),
-    nxt: Box::new(term),
-  })
-}
-
-const PATTERN_ERROR_LIMIT: usize = 5;
-const ERROR_LIMIT_HINT: &str = "Use the --verbose option to see all cases.";
-
-impl SimplifyMatchErr {
-  pub fn display(&self, verbose: bool) -> impl std::fmt::Display + '_ {
-    let limit = if verbose { usize::MAX } else { PATTERN_ERROR_LIMIT };
-    DisplayFn(move |f| match self {
-      SimplifyMatchErr::NotExhaustive(cases) => {
-        let ident = ERR_INDENT_SIZE * 2;
-        let hints = DisplayJoin(
-          || {
-            cases
-              .iter()
-              .take(limit)
-              .map(|pat| DisplayFn(move |f| write!(f, "{:ident$}Case '{pat}' not covered.", "")))
-          },
-          "\n",
-        );
-        write!(f, "Non-exhaustive pattern matching. Hint:\n{}", hints)?;
-
-        let len = cases.len();
-        if len > limit {
-          write!(f, " ... and {} others.\n{:ident$}{}", len - limit, "", ERROR_LIMIT_HINT)?;
-        }
-
-        Ok(())
-      }
-      SimplifyMatchErr::TypeMismatch(err) => {
-        write!(f, "{}", err.to_string_verbose(verbose))
-      }
-      SimplifyMatchErr::MalformedNumSucc(got, exp) => {
-        write!(f, "Expected a sequence of incrementing numbers ending with '{exp}', found '{got}'.")
-      }
-    })
-  }
-}
-
-impl ToStringVerbose for SimplifyMatchErr {
-  fn to_string_verbose(&self, verbose: bool) -> String {
-    format!("{}", self.display(verbose))
-  }
-}
-
-impl From<TypeMismatchErr> for SimplifyMatchErr {
-  fn from(value: TypeMismatchErr) -> Self {
-    SimplifyMatchErr::TypeMismatch(value)
-  }
-}

tests/golden_tests.rs

@@ -92,6 +92,14 @@ fn run_golden_test_dir_multiple(test_name: &str, run: &[&RunFn]) {
   }
 }
 
+/* Snapshot/regression/golden tests
+
+ Each tests runs all the files in tests/golden_tests/<test name>.
+
+ The test functions decide how exactly to process the test programs
+ and what to save as a snapshot.
+*/
+
 #[test]
 fn compile_term() {
   run_golden_test_dir(function_name!(), &|code, _| {
@@ -147,6 +155,7 @@ fn linear_readback() {
     Ok(format!("{}{}", info.diagnostics, res))
   });
 }
+
 #[test]
 fn run_file() {
   run_golden_test_dir_multiple(function_name!(), &[
@@ -206,25 +215,22 @@ fn simplify_matches() {
     let diagnostics_cfg = DiagnosticsConfig::new(Severity::Error, true);
     let mut book = do_parse_book(code, path)?;
     let mut ctx = Ctx::new(&mut book, diagnostics_cfg);
+
     ctx.check_shared_names();
     ctx.set_entrypoint();
     ctx.book.encode_adts(AdtEncoding::TaggedScott);
-    ctx.book.encode_builtins();
     ctx.book.resolve_ctrs_in_pats();
-    ctx.resolve_refs()?;
+    ctx.check_unbound_ctr()?;
-    ctx.check_match_arity()?;
-    ctx.check_unbound_pats()?;
-    ctx.book.convert_match_def_to_term();
-    ctx.book.desugar_let_destructors();
-    ctx.book.desugar_implicit_match_binds();
     ctx.check_ctrs_arities()?;
+    ctx.book.encode_builtins();
+    ctx.resolve_refs()?;
+    ctx.fix_match_terms()?;
+    ctx.desugar_match_defs()?;
     ctx.check_unbound_vars()?;
-    ctx.simplify_matches()?;
+    ctx.book.linearize_matches(true);
-    ctx.book.linearize_simple_matches(true);
     ctx.check_unbound_vars()?;
-    ctx.book.make_var_names_unique();
-    ctx.book.linearize_vars();
     ctx.prune(false, AdtEncoding::TaggedScott);
+
     Ok(ctx.book.to_string())
   })
 }
@@ -242,25 +248,22 @@ fn encode_pattern_match() {
   run_golden_test_dir(function_name!(), &|code, path| {
     let mut result = String::new();
     for adt_encoding in [AdtEncoding::TaggedScott, AdtEncoding::Scott] {
-      let diagnostics_cfg = DiagnosticsConfig::new(Severity::Error, true);
+      let diagnostics_cfg = DiagnosticsConfig::new(Severity::Warning, true);
       let mut book = do_parse_book(code, path)?;
       let mut ctx = Ctx::new(&mut book, diagnostics_cfg);
       ctx.check_shared_names();
       ctx.set_entrypoint();
       ctx.book.encode_adts(adt_encoding);
-      ctx.book.encode_builtins();
       ctx.book.resolve_ctrs_in_pats();
-      ctx.resolve_refs()?;
+      ctx.check_unbound_ctr()?;
-      ctx.check_match_arity()?;
-      ctx.check_unbound_pats()?;
-      ctx.book.convert_match_def_to_term();
-      ctx.book.desugar_let_destructors();
-      ctx.book.desugar_implicit_match_binds();
       ctx.check_ctrs_arities()?;
+      ctx.book.encode_builtins();
+      ctx.resolve_refs()?;
+      ctx.fix_match_terms()?;
+      ctx.desugar_match_defs()?;
       ctx.check_unbound_vars()?;
-      ctx.simplify_matches()?;
+      ctx.book.linearize_matches(true);
-      ctx.book.linearize_simple_matches(true);
+      ctx.book.encode_matches(adt_encoding);
-      ctx.book.encode_simple_matches(adt_encoding);
       ctx.check_unbound_vars()?;
       ctx.book.make_var_names_unique();
       ctx.book.linearize_vars();

tests/golden_tests/cli/debug_u60_to_nat.hvm

@@ -1,6 +1,8 @@
 data Nat_ = (Z) | (S nat)
 
-(U60ToNat 0)   = Z
+U60ToNat n = switch n {
-(U60ToNat 1+p) = (S (U60ToNat p))
+  0: Z
+  _: (S (U60ToNat n-1))
+}
 
 (Main n) = (U60ToNat n)

tests/golden_tests/cli/desugar_linearize_matches.hvm

@@ -1 +1 @@
-main = λa λb match a { 0: b; 1+: b }
+main = λa λb switch a { 0: b; _: b }

tests/golden_tests/cli/desugar_linearize_matches_extra.hvm

@@ -1 +1 @@
-main = λa λb λc match a { 0: b; 1+: c }
+main = λa λb λc switch a { 0: b; _: c }

tests/golden_tests/compile_file/implicit_match_in_match_arg.hvm

@@ -1,4 +0,0 @@
-main x = match (match x {0: 0; 1+: x-1}) {
-  0: 0
-  1+x-2: x-2
-}

tests/golden_tests/compile_file/match_num_all_patterns.hvm

@@ -1,60 +0,0 @@
-zero_succ = @x match x {
-  0: 0
-  1+: x-1
-}
-succ_zero = @x match x {
-  1+: x-1
-  0: 0
-}
-
-var_zero = @x match x {
-  var: var
-  0: 0
-}
-
-var_succ = @x match x {
-  var: var
-  1+: x-1
-}
-
-zero_var = @x match x {
-  0: 0
-  var: (- var 1)
-}
-
-succ_var = @x match x {
-  1+: x-1
-  var: 0
-}
-
-zero_var_succ = @x match x {
-  0: 0
-  var: (- var 1)
-  1+: x-1
-}
-
-succ_var_zero = @x match x {
-  1+: (+ x-1 2)
-  var: (+ var 1)
-  0: 1
-}
-
-zero_succ_var = @x match x {
-  0: 0
-  1+: x-1
-  var: (- var 1)
-}
-
-succ_zero_var = @x match x {
-  1+: x-1
-  0: 0
-  var: (- var 1)
-}
-
-succ_zero_succ = @x match x {
-  1+: x-1
-  0: 0
-  1+a: (+ a 1)
-}
-
-main = 0

tests/golden_tests/compile_file/match_num_unscoped_lambda.hvm

@@ -1,11 +0,0 @@
-lambda_out = @x @$y match x {
-  0: $y
-  1+: x-1
-}
-
-lambda_in = @x (match x {
-  0: @x x
-  1+: @$y x-1
-} $y)
-
-main = *

tests/golden_tests/compile_file/repeated_bind_match.hvm

@@ -1,4 +0,0 @@
-main = @a match a {
- (List.cons x x): x
- (List.nil)     : *
-}

tests/golden_tests/compile_file/switch_all_patterns.hvm

@@ -0,0 +1,43 @@
+zero_succ = @x switch x {
+  0: 0
+  _: x-1
+}
+
+succ_zero = @x switch x {
+  _: x-1
+  0: 0
+}
+
+zero = @x switch x {
+  0: 0
+}
+
+succ = @x switch x {
+  _: x-1
+}
+
+succ_zero_succ = @x switch x {
+  _: x-1
+  0: 0
+  _: (+ x-1 1)
+}
+
+zero_succ_zero = @x switch x {
+  0: 0
+  _: x-1
+  0: 1
+}
+
+zero_zero_succ = @x switch x {
+  0: 0
+  0: 1
+  _: x-1
+}
+
+zero_succ_succ = @x switch x {
+  0: 0
+  _: x-1
+  _: (+ x-1 1)
+}
+
+main = 0

tests/golden_tests/compile_file/switch_in_switch_arg.hvm

@@ -0,0 +1,4 @@
+main x = switch (switch x {0: 0; _: x-1}) {
+  0: 0
+  _: x
+}

tests/golden_tests/compile_file/switch_unscoped_lambda.hvm

@@ -0,0 +1,11 @@
+lambda_out = @x @$y switch x {
+  0: $y
+  _: x-1
+}
+
+lambda_in = @x (switch x {
+  0: @x x
+  _: @$y x-1
+} $y)
+
+main = *

tests/golden_tests/compile_file_o_all/extracted_match_pred.hvm

@@ -1,5 +1,5 @@
 // We expect the inferred 'λn-1' from the match to be extracted which allows this recursive func
-val = λn (match n { 0: valZ; 1+: (valS n-1) })
+val = λn (switch n { 0: valZ; _: (valS n-1) })
   valZ = 0
   valS = λp (val p)
 main = (val 1)

tests/golden_tests/compile_file_o_all/let_adt_destructuring.hvm

@@ -1,7 +0,0 @@
-data Boxed = (Box val)
-
-// Both rules should have the same compiled net structure
-// (Unbox (Box val)) = val 
-(Unbox x) = let (Box val) = x; val
-
-main = (Unbox (Box 1))

tests/golden_tests/compile_file_o_all/let_adt_non_exhaustive.hvm

@@ -1,6 +0,0 @@
-data Maybe = (Some val) | None
-
-main = 
-  let maybe = (Some 1)
-  let (Some value) = maybe
-  value

tests/golden_tests/compile_file_o_all/linearize_match.hvm

@@ -1,4 +1,4 @@
-main = @a @b let c = (+ a a); match a {
+main = @a @b let c = (+ a a); switch a {
   0: b;
-  1+: (+ a-1 b);
+  _: (+ a-1 b);
 }

tests/golden_tests/compile_file_o_all/match_adt_non_exhaustive.hvm

@@ -2,6 +2,8 @@ data Maybe = (Some val) | None
 
 main = @maybe
   match maybe {
-    (None): 0
+    None: 0
-    (Some (None)): 0
+    Some: match maybe.val {
+      None: 0
+    }
   }

tests/golden_tests/compile_file_o_all/match_mult_linearization.hvm

@@ -1,4 +1,4 @@
-main = @a @b @c @d match a {
+main = @a @b @c @d switch a {
   0: (+ (+ b c) d);
-  1+: (+ (+ (+ a-1 b) c) d);
+  _: (+ (+ (+ a-1 b) c) d);
 }

tests/golden_tests/compile_file_o_all/match_num_explicit_bind.hvm

@@ -1,6 +1,6 @@
-pred = @n match n {
+pred = @n switch n {
   0: 0
-  1+: n-1
+  _: n-1
 }
 
 main = (pred 4)

tests/golden_tests/compile_file_o_all/nested_adt_match.hvm

@@ -1,8 +0,0 @@
-data Maybe = (Some val) | None
-
-main =
-  match (Some (Some 1)) {
-    (None): 0
-    (Some (None)): 0
-    (Some (Some v)): v
-  }

tests/golden_tests/compile_file_o_all/num_pattern_with_var.hvm

@@ -3,6 +3,6 @@ data bool = false | true
 
 (Foo false a) = 0
 (Foo true 0) = 0
-(Foo true 1+n) = n
+(Foo true n) = n
 
 Main = (Foo true 3)

tests/golden_tests/compile_file_o_all/recursive_combinator_inactive.hvm

@@ -1,4 +1,4 @@
 // `Foo` inside the term `{Foo Foo}` is not in a active position, tests that it is not unnecessarily extracted
-Foo = @a match a { 0: {Foo Foo}; 1+p: @* p }
+Foo = @a switch a { 0: {Foo Foo}; _: @* a-1 }
 
 main = (Foo 0)

tests/golden_tests/compile_file_o_all/sum_predicates.hvm

@@ -1,11 +1,11 @@
-sum_pred = @a @b match a {
+sum_pred = @a @b switch a {
-  0: match b {
+  0: switch b {
     0: 0
-    1+: b-1
+    _: b-1
   };
-  1+: match b {
+  _: switch b {
     0: a-1
-    1+: (+ a-1 b-1)
+    _: (+ a-1 b-1)
   }
 }
 

tests/golden_tests/compile_term/match.hvm

@@ -1,4 +1,4 @@
-match (+ 0 1) {
+switch (+ 0 1) {
   0: λt λf t
-  1+: λ* λt λf f // The term to hvmc function assumes the pred variable is already detached from the match
+  _: λ* λt λf f // The term to hvmc function assumes the pred variable is already detached from the match
 }

tests/golden_tests/desugar_file/combinators.hvm

@@ -4,8 +4,8 @@
 
 (List.ignore list ignore) =
   match list {
-    (List.cons): (List.ignore list.tail (List.ignore))
+    List.cons: (List.ignore list.tail (List.ignore))
-    (List.nil): 0
+    List.nil: 0
   }
 
 (baz) = {0 1 2 3 λa a foo}

tests/golden_tests/encode_pattern_match/concat.hvm

@@ -1,7 +1,7 @@
 String.concat = @a @b
   match a {
     String.nil: b;
-    (String.cons hd tl): (String.cons hd (String.concat tl b))
+    String.cons: (String.cons a.head (String.concat a.tail b))
   }
 
 main = (String.concat "ab" "cd")

tests/golden_tests/encode_pattern_match/flatten_era_pat.hvm

@@ -4,6 +4,6 @@
 (Fn2 (*,(*,(a,*)))) = a
 
 (Fn3 (0,*) *) = 0
-(Fn3 (1+a,*) *) = a
+(Fn3 (a,*) *) = a
 
 main = (Fn2 ((1, 2), (3, (4, (5, 6)))) 0)

tests/golden_tests/encode_pattern_match/list_str_encoding_undeclared_map.hvm

@@ -4,7 +4,7 @@ main = @a @b
     String.nil : 2
   };
   let b = match b {
-    (List.cons h t): 1
+    List.cons: 1
-    (List.nil) : 2
+    List.nil : 2
   };
   (a, b)

tests/golden_tests/encode_pattern_match/match_adt_unscoped_lambda.hvm

@@ -1,6 +1,6 @@
 data Maybe = None | (Some val)
 
-main = (match (Some 1) {
+main = (match x = (Some 1) {
   None: @$x *
-  (Some x): x
+  Some: x.val
 } $x)

tests/golden_tests/encode_pattern_match/match_adt_unscoped_var.hvm

@@ -1,13 +1,13 @@
 data Maybe = None | (Some val)
 
-Foo = @$x match (Some 1) {
+Foo = @$x match x = (Some 1) {
   None: $x
-  (Some x): x
+  Some: x.val
 }
 
-Bar = (match (Some 1) {
+Bar = (match x = (Some 1) {
   None: $x
-  (Some x): x
+  Some: x.val
 } @$x *)
 
 main = *

tests/golden_tests/encode_pattern_match/match_bind.hvm

@@ -1,7 +1,7 @@
 cheese =
-  match num = (+ 2 3) {
+  switch num = (+ 2 3) {
   | 0: 653323
-  | 1+: (+ num num-1)
+  | _: (+ num num-1)
   }
 
 main = cheese

tests/golden_tests/encode_pattern_match/match_many_args.hvm

@@ -1,40 +0,0 @@
-data L = (C h t) | N
-data Option = (Some val) | None
-
-tail_tail = @xs match xs {
-  (C * (C * t)): t
-  *: N
-}
-
-or = @dflt @opt match dflt opt {
-  * (Some val): val
-  dflt *: dflt
-}
-
-or2 = @opt @dflt match opt dflt {
-  (Some val) *: val
-  * dflt: dflt
-}
-
-map = @f @opt match f opt {
-  f (Some val): (f val)
-  * None: None
-}
-
-map2 = @f @opt match f opt {
-  f (Some val): (f val)
-  * val: val
-}
-
-flatten = @opt match opt {
-  (Some (Some val)): (Some val)
-  *: None
-}
-
-map_pair = @f @xs @ys match f xs ys {
-  * N *: N
-  * * N: N
-  f (C x xs) (C y ys): (C (f x y) (map_pair xs ys))
-}
-
-main = *

tests/golden_tests/encode_pattern_match/match_num_adt_tup_parser.hvm

@@ -9,7 +9,7 @@ Parse state xs = (Err (xs, state))
 main =
   let str = "(+";
   let state = *;
-  match (Parse state str) {
+  match res = (Parse state str) {
-    (Ok (val, xs, state)): (val, (Parse state xs))
+    Ok: let (val, xs, state) = res.val; (val, (Parse state xs))
     err: err
   }

tests/golden_tests/encode_pattern_match/match_num_pred.hvm

@@ -1,18 +1,21 @@
-pred 0 = 0
+pred = @n switch n {
-pred 1+x = x
+  0: 0
+  _: n-1
+}
 
-pred2 2+x = x
+pred2 n = switch n {
-pred2 * = 0
+  0: 0
+  1: 0
+  _: n-2
+}
 
 pred3 0 = 0
 pred3 1 = 0
 pred3 2 = 0
-pred3 3+x-3 = x-3
+pred3 x = (- x 3)
 
-pred4 0 = 0
+zero 0 = 1
-pred4 1 = 0
+zero 1 = 0
-pred4 2 = 0
+zero * = 0
-pred4 3 = 0
-pred4 n = (- n 4)
 
 main = *

tests/golden_tests/encode_pattern_match/nested_let_tup.hvm

@@ -1,6 +0,0 @@
-main =
-  let (a, (b, c)) =
-    let (i, (j, k)) = (10, ((1, ((2, 3), 4)), 3));
-    j;
-  let (x, y) = b;
-  x

tests/golden_tests/run_file/bitonic_sort.hvm

@@ -2,9 +2,9 @@ data Tree = (Leaf a) | (Both a b)
 data Error = Err
 
 // Atomic Swapper
-(Swap n a b) = match n {
+(Swap n a b) = switch n {
   0: (Both a b)
-  1+: (Both b a)
+  _: (Both b a)
 }
 
 // Swaps distant values in parallel; corresponds to a Red Box
@@ -29,9 +29,9 @@ data Error = Err
 (Sort s (Both a b)) = (Flow s (Both (Sort 0 a) (Sort 1 b)))
 
 // Generates a tree of depth `n`
-(Gen n x) = match n {
+(Gen n x) = switch n {
   0: (Leaf x)
-  1+: (Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 1)))
+  _: (Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 1)))
 }
 
 // Reverses a tree

tests/golden_tests/run_file/bitonic_sort_lam.hvm

@@ -2,9 +2,9 @@
 Leaf = λx      #Tree λl #Tree λn (l x)
 Node = λx0 λx1 #Tree λl #Tree λn (n x0 x1)
 
-swap = λn match n {
+swap = λn switch n {
   0: λx0 λx1 (Node x0 x1)
-  1+: λx0 λx1 (Node x1 x0)
+  _: λx0 λx1 (Node x1 x0)
 }
 
 warp = λa
@@ -41,9 +41,9 @@ sort = λa
   let a_node = λa0 λa1 λs (flow (Node (sort a0 0) (sort a1 1)) s)
   #Tree (a a_leaf a_node)
 
-gen = λn match n {
+gen = λn switch n {
   0: λx (Leaf x)
-  1+: λx (Node (gen n-1 (* x 2)) (gen n-1 (+ (* x 2) 1)))
+  _: λx (Node (gen n-1 (* x 2)) (gen n-1 (+ (* x 2) 1)))
 }
 
 rev = λa

tests/golden_tests/run_file/box.hvm

@@ -2,6 +2,6 @@ data _Box = (Box val)
 
 Box.subst (Box n) from to = (Box.subst.go n (== from n) to)
 Box.subst.go a 0   to = (Box a)
-Box.subst.go a 1+* to = to
+Box.subst.go a * to = to
 
 Main = (Box.subst (Box 4) 4 (Box 10))

tests/golden_tests/run_file/box2.hvm

@@ -1,7 +0,0 @@
-data _Box = (Box val)
-
-Box.subst (Box n) from to = (Box.subst.go n (== from n) to)
-Box.subst.go a 0   to = (Box a)
-Box.subst.go a 1+* to = to
-
-Main = (Box.subst (Box 4) 8000 (Box 10))

tests/golden_tests/run_file/def_bool_num.hvm

@@ -1,6 +1,6 @@
 data bool = true | false
 
-go true  0   = 1
+go true  0 = 1
-go false 1+* = 0
+go false _ = 0
 
 main = (go true 1)

tests/golden_tests/run_file/example.hvm

@@ -20,9 +20,9 @@
 // You can use numbers on the native match expression
 // The `+` arm binds the `scrutinee`-1 variable to the the value of the number -1
 (Num.pred) = λn 
-  match n { 
+  switch n { 
     0: 0
-    1+: n-1
+    _: n-1
   }
 
 // Write new data types like this
@@ -51,9 +51,9 @@ data Boxed = (Box val)
 // Types with only one constructor can be destructured using `let` or a single matching definition
 (Box.map (Box val) f) = (Box (f val))
 
-(Box.unbox) = λbox
+(Box.unbox) = λbox match box {
-  let (Box val) = box
+  Box: box.val
-  val
+}
 
 // Use tuples to store two values together without needing to create a new data type
 (Tuple.new fst snd) =
@@ -68,9 +68,9 @@ data Boxed = (Box val)
   snd
 
 // All files must have a main definition to be run.
-// You can execute a program in HVM with "cargo run -- --run <path to file>"
+// You can execute a program in HVM with "cargo run -- run <path to file>"
-// Other options are "--check" (the default mode) to just see if the file is well formed
+// Other options are "check" (the default mode) to just see if the file is well formed
-// and "--compile" to output hvm-core code.
+// and "compile" to output hvm-core code.
 (main) = 
   let tup = (Tuple.new None (Num.pred 5))
 

tests/golden_tests/run_file/extracted_match_pred.hvm

@@ -1,5 +1,5 @@
 // We expect the lambda 'p' from the match to be extracted which allows this recursive func
-val = λn (match n { 0: valZ; 1+: (valS n-1) })
+val = λn (switch n { 0: valZ; _: (valS n-1) })
   valZ = 0
   valS = λp (val p)
 main = (val 1)

tests/golden_tests/run_file/linearize_match.hvm

@@ -1,4 +1,4 @@
-main = @a @b let c = (+ a a); match a {
+main = @a @b let c = (+ a a); switch a {
   0: b;
-  1+: (+ a-1 b);
+  _: (+ a-1 b);
 }

tests/golden_tests/run_file/list_take.hvm

@@ -1,7 +1,7 @@
 Take_ n list =
-  match (== n 0) {
+  switch (== n 0) {
   | 0: (Take n list)
-  | 1+: []
+  | _: []
   }
 Take n (List.nil) = []
 Take n (List.cons x xs) = (List.cons x (Take_ (- n 1) xs))

tests/golden_tests/run_file/list_to_tree.hvm

@@ -3,17 +3,17 @@ List.len.go [] count = count
 List.len.go (List.cons x xs) count = (List.len.go xs (+ count 1))
 
 Take.go n list =
-  match (== n 0) {
+  switch (== n 0) {
   | 0: (Take n list)
-  | 1+: []
+  | _: []
   }
 Take n [] = []
 Take n (List.cons x xs) = (List.cons x (Take.go (- n 1) xs))
 
 Drop.go n list =
-  match (== n 0) {
+  switch (== n 0) {
   | 0: (Drop n list)
-  | 1+: list
+  | _: list
   }
 Drop n [] = []
 Drop n (List.cons x xs) = (Drop.go (- n 1) xs)

tests/golden_tests/run_file/match.hvm

@@ -1,5 +1,5 @@
 main =
-  match (+ 0 1) {
+  switch (+ 0 1) {
     0: λt λf t
-    1+: λt λf f
+    _: λt λf f
   }

tests/golden_tests/run_file/match_mult_linearization.hvm

@@ -1,4 +1,4 @@
-main = @a @b @c @d match a {
+main = @a @b @c @d switch a {
   0: (+ (+ b c) d);
-  1+: (+ (+ (+ a-1 b) c) d);
+  _: (+ (+ (+ a-1 b) c) d);
 }

tests/golden_tests/run_file/match_num_adt_tup_parser.hvm

@@ -9,7 +9,7 @@ Parse state xs = (Err (xs, state))
 main =
   let str = "(+";
   let state = *;
-  match (Parse state str) {
+  match res = (Parse state str) {
-    (Ok (val, xs, state)): (val, (Parse state xs))
+    Ok: let (val, xs, state) = res.val; (val, (Parse state xs))
     err: err
   }

tests/golden_tests/run_file/match_num_explicit_bind.hvm

@@ -1,6 +1,6 @@
-pred = @n match n {
+pred = @n switch n {
   0: 0
-  1+: n-1
+  _: n-1
 }
 
 main = (pred 4)

tests/golden_tests/run_file/match_num_num_to_char.hvm

@@ -1,4 +1,4 @@
-num_to_char n = match n {
+num_to_char n = switch n {
   0: '0'
   1: '1'
   2: '2'
@@ -9,22 +9,20 @@ num_to_char n = match n {
   7: '7'
   8: '8'
   9: '9'
-  10+: '\0'
+  _: '\0'
 }
 
-char_to_num c = match c {
+char_to_num '9' = 9
-  57: 9
+char_to_num '8' = 8
-  56: 8
+char_to_num '7' = 7
-  55: 7
+char_to_num '6' = 6
-  54: 6
+char_to_num '5' = 5
-  53: 5
+char_to_num '4' = 4
-  52: 4
+char_to_num '3' = 3
-  51: 3
+char_to_num '2' = 2
-  50: 2
+char_to_num '1' = 1
-  49: 1
+char_to_num '0' = 0
-  48: 0
+char_to_num  _  = (- 0 1)
-  c : (- 0 1)
-}
 
 map f List.nil = List.nil
 map f (List.cons x xs) = (List.cons (f x) (map f xs))

tests/golden_tests/run_file/match_num_succ_complex.hvm

@@ -1,16 +1,16 @@
-min1 *   0   = 0
+min1 * 0 = 0
-min1 0   *   = 0
+min1 0 * = 0
-min1 1+a 1+b = (+ 1 (min1 a b))
+min1 a b = (+ 1 (min1 (- a 1) (- b 1)))
 
-min2 0 * = 0
+min2 a b = switch a {
-min2 * 0 = 0
+  0: 0
-min2 1+a 1+b = (+ (min2 a b) 1)
+  _: switch b {
-
+    0: 0
-min3 1+a 1+b = (+ (min3 a b) 1)
+    _: (+ 1 (min2 a-1 b-1))
-min3 * * = 0
+  }
+}
 
 main = [
   [(min1 5 10) (min1 10 5) (min1 0 12) (min1 12 0) (min1 0 0) (min1 6 6)]
   [(min2 5 10) (min2 10 5) (min2 0 12) (min2 12 0) (min2 0 0) (min2 6 6)]
-  [(min3 5 10) (min3 10 5) (min3 0 12) (min3 12 0) (min3 0 0) (min3 6 6)]
 ]

tests/golden_tests/run_file/match_sup.hvm

@@ -1,4 +1,6 @@
-main = let k = #a{0 1}; match k {
+main =
+  let k = #a{0 1};
+  switch k {
     0: 1
-    1+p: (+ p 2)
+    _: (+ k-1 2)
-}
+  }

tests/golden_tests/run_file/merge_sort.hvm

@@ -7,9 +7,9 @@ sort (Node a b) = (merge (sort a) (sort b))
 merge (Nil) b = b
 merge (Cons x xs) (Nil) = (Cons x xs)
 merge (Cons x xs) (Cons y ys) = 
-  let t = match (< x y) {
+  let t = switch (< x y) {
     0: λaλbλcλt(t c a b)
-    1+: λaλbλcλt(t a b c)
+    _: λaλbλcλt(t a b c)
   }
 
   let t = (t (Cons x) λx(x) (Cons y))
@@ -19,9 +19,9 @@ merge (Cons x xs) (Cons y ys) =
 sum Nil = 0
 sum (Cons h t) = (+ h (sum t))
 
-range n = match n {
+range n = switch n {
   0: λx (Leaf x)
-  1+: λx (Node (range n-1 (+ (* x 2) 1)) (range n-1 (* x 2)))
+  _: λx (Node (range n-1 (+ (* x 2) 1)) (range n-1 (* x 2)))
 }
 
 main = (sum (sort (range 4 0)))

tests/golden_tests/run_file/names_hyphen.hvm

@@ -3,9 +3,9 @@ id cool-var-name = cool-var-name
 data Done_ = (Done done-var)
 
 toZero n =
-  match n {
+  switch n {
     0: (Done 1)
-    1+: (toZero n-1)
+    _: (toZero n-1)
   }
 
 main =

tests/golden_tests/run_file/nested_let_tup.hvm

@@ -1,6 +0,0 @@
-main =
-  let (a, (b, c)) =
-    let (i, (j, k)) = (10, ((1, ((2, 3), 4)), 3));
-    j;
-  let (x, y) = b;
-  x

tests/golden_tests/run_file/num_match_missing_var.hvm

@@ -1,21 +1,15 @@
 if 0 t f = f
 if 1 t f = t
 
-if2 n t f = match n {
+if2 n t f = switch n {
   0: f
-  1+: t
+  _: t
-  n: f
+  _: f
 }
 
-if3 n t f = match n {
+if3 n t f = switch n {
   0: f
-  *: t
+  _: t
-  1+: t
-}
-
-if4 n t f = match n {
-  0: f
-  1+: t
   1: t
 }
 

tests/golden_tests/run_file/num_pred.hvm

@@ -1,4 +1,6 @@
-Pred 0      = 0
+Pred n = switch n {
-Pred 1+pred = pred
+  0: 0
+  _: n-1
+}
 
 Main = (Pred 43)

tests/golden_tests/run_file/pred.hvm

@@ -1,6 +1,6 @@
-Pred = λt match t {
+Pred = λt switch t {
   0: 0
-  1+: t-1
+  _: t-1
 }
 
 main = (Pred 3)

tests/golden_tests/run_file/radix_sort_ctr.hvm

@@ -1,9 +1,9 @@
 data Map = Free | Used | (Both a b)
 data Arr = Null | (Leaf x) | (Node a b)
 
-(Swap s a b) = match s {
+(Swap s a b) = switch s {
   0: (Both a b)
-  1+: (Both b a)
+  _: (Both b a)
 }
 
 // Sort : Arr -> Arr
@@ -74,9 +74,9 @@ data Arr = Null | (Leaf x) | (Node a b)
 
 // Gen : U60 -> Arr
 (Gen n) = (Gen.go n 0)
-  (Gen.go n x) = match n {
+  (Gen.go n x) = switch n {
     0: (Leaf x)
-    1+:
+    _:
       let x = (<< x 1)
       let y = (| x 1)
       (Node (Gen.go n-1 x) (Gen.go n-1 y))

tests/golden_tests/run_file/recursive_combinator_nested.hvm

@@ -1,4 +1,7 @@
 // Tests that `({Foo @* a} 9)` is correctly extracted as a combinator, otherwise the file would hang when running
-Foo = @a match a { 0: (#a {Foo @* a} 9); 1+p: p }
+Foo = @a switch a {
+  0: (#a {Foo @* a} 9);
+  _: a-1
+}
 
 main = (Foo 0)

tests/golden_tests/run_file/recursive_match_native.hvm

@@ -1,8 +1,8 @@
 add = λa λb (+ a b)
 
-sum = λn match n {
+sum = λn switch n {
   0: 1
-  1+: (add (sum n-1) (sum n-1))
+  _: (add (sum n-1) (sum n-1))
 }
 
 main = (sum 9)

tests/golden_tests/run_file/str_inc.hvm

@@ -1,7 +1,7 @@
 (StrInc (len, buf)) = (len, #str λx (StrGo len #str (buf x)))
 
 (StrGo 0 str) = str
-(StrGo 1+x (head, tail)) = ((+ 1 head), (StrGo x tail))
+(StrGo x (head, tail)) = ((+ 1 head), (StrGo (- x 1) tail))
 
 // Old str encoding
 Hello = (11, #str λx (104, (101, (108, (108, (111, (32, (119, (111, (114, (108, (100, x))))))))))))

tests/golden_tests/run_file/str_inc_eta.hvm

@@ -1,7 +1,7 @@
 (StrInc (len, buf)) = (len, #str λx (StrGo len #str (buf x)))
 
 (StrGo 0  (head, tail)) = (head, tail)
-(StrGo 1+x (head, tail)) = ((+ 1 head), (StrGo x tail))
+(StrGo x (head, tail)) = ((+ 1 head), (StrGo (- x 1) tail))
 
 // Old str encoding
 Hello = (11, #str λx (104, (101, (108, (108, (111, (32, (119, (111, (114, (108, (100, x))))))))))))

tests/golden_tests/run_file/sum_tree.hvm

@@ -2,9 +2,9 @@ data Tree = (Leaf x) | (Node x0 x1)
 
 add = λa λb (+ a b)
 
-gen = λn match n {
+gen = λn switch n {
   0: (Leaf 1)
-  1+: (Node (gen n-1) (gen n-1))
+  _: (Node (gen n-1) (gen n-1))
 }
 
 sum = λt

tests/golden_tests/run_file/tuple_rots.hvm

@@ -2,9 +2,9 @@ MkTup8 = @a @b @c @d @e @f @g @h @MkTup8 (MkTup8 a b c d e f g h)
 
 rot = λx (x λa λb λc λd λe λf λg λh (MkTup8 b c d e f g h a))
 
-app = λn match n {
+app = λn switch n {
   0: λf λx x
-  1+: λf λx (app n-1 f (f x))
+  _: λf λx (app n-1 f (f x))
 }
 
 main = (app 100 rot (MkTup8 1 2 3 4 5 6 7 8))

tests/golden_tests/run_lazy/bitonic_sort.hvm

@@ -2,9 +2,9 @@ data Tree = (Leaf a) | (Both a b)
 data Error = Err
 
 // Atomic Swapper
-(Swap n a b) = match n {
+(Swap n a b) = switch n {
   0: (Both a b)
-  1+: (Both b a)
+  _: (Both b a)
 }
 
 // Swaps distant values in parallel; corresponds to a Red Box
@@ -29,9 +29,9 @@ data Error = Err
 (Sort s (Both a b)) = (Flow s (Both (Sort 0 a) (Sort 1 b)))
 
 // Generates a tree of depth `n`
-(Gen n x) = match n {
+(Gen n x) = switch n {
   0: (Leaf x)
-  1+: (Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 1)))
+  _: (Both (Gen n-1 (* x 2)) (Gen n-1 (+ (* x 2) 1)))
 }
 
 // Reverses a tree

tests/golden_tests/run_lazy/bitonic_sort_lam.hvm

@@ -2,9 +2,9 @@
 Leaf = λx      #Tree λl #Tree λn (l x)
 Node = λx0 λx1 #Tree λl #Tree λn (n x0 x1)
 
-swap = λn match n {
+swap = λn switch n {
   0: λx0 λx1 (Node x0 x1)
-  1+: λx0 λx1 (Node x1 x0)
+  _: λx0 λx1 (Node x1 x0)
 }
 
 warp = λa
@@ -41,9 +41,9 @@ sort = λa
   let a_node = λa0 λa1 λs (flow (Node (sort a0 0) (sort a1 1)) s)
   #Tree (a a_leaf a_node)
 
-gen = λn match n {
+gen = λn switch n {
   0: λx (Leaf x)
-  1+: λx (Node (gen n-1 (* x 2)) (gen n-1 (+ (* x 2) 1)))
+  _: λx (Node (gen n-1 (* x 2)) (gen n-1 (+ (* x 2) 1)))
 }
 
 rev = λa