[sc-332] Don't extract num matches into separate defs

src/term/check/exhaustiveness.rs

@@ -1,5 +1,5 @@
-use super::type_check::{DefinitionTypes, Type};
-use crate::term::{Adt, Book, MatchNum, Name, Pattern, Rule};
+use super::type_check::DefinitionTypes;
+use crate::term::{Adt, Book, MatchNum, Name, Pattern, Rule, Type};
 use std::collections::BTreeMap;
 
 impl Book {
@@ -10,7 +10,8 @@ impl Book {
       let def_name = self.def_names.name(def_id).unwrap();
       let types = &def_types[def_id];
       let rules_to_check = Vec::from_iter(0 .. def.rules.len());
-      check_pattern(&mut vec![], &self.adts, &def.rules, types, rules_to_check, def_name)?;
+      check_pattern(&mut vec![], &self.adts, &def.rules, types, rules_to_check, def_name)
+        .map_err(|e| format!("In definition '{}': {}", self.def_names.name(&def.def_id).unwrap(), e))?;
     }
     Ok(())
   }
@@ -72,10 +73,7 @@ fn check_pattern(
     for (ctr, matching_rules) in rules_matching_ctrs {
       if matching_rules.is_empty() {
         let missing = get_missing_pattern(match_path, ctr, &types[1 ..], adts);
-        return Err(format!(
-          "Non-exhaustive pattern at definition '{}'. Hint: ({} {}) not covered.",
-          def_name, def_name, missing
-        ));
+        return Err(format!("Non-exhaustive pattern. Hint: ({} {}) not covered.", def_name, missing));
       } else {
         let mut match_path = match_path.to_vec();
         match_path.push(ctr);

src/term/check/has_main.rs

@@ -8,7 +8,15 @@ impl Book {
     ) {
       (None, None) => Err("File has no 'main' definition".to_string()),
       (Some(_), Some(_)) => Err("File has both 'Main' and 'main' definitions".to_string()),
-      (None, Some(main)) | (Some(main), None) => Ok(main),
+      (None, Some(main)) | (Some(main), None) => {
+        if self.defs[&main].rules.len() > 1 {
+          Err("Main definition can't have more than one rule".to_string())
+        } else if !self.defs[&main].rules[0].pats.is_empty() {
+          Err("Main definition can't have any arguments".to_string())
+        } else {
+          Ok(main)
+        }
+      }
     }
   }
 }

src/term/check/shared_names.rs

@@ -9,19 +9,19 @@ impl Book {
 
     for adt_name in self.adts.keys() {
       if !checked.insert(adt_name) {
-        return Err(format!("Duplicated name '{adt_name}'"));
+        return Err(format!("Duplicated top-level name '{adt_name}'"));
       }
     }
 
     for ctr_name in self.ctrs.keys() {
       if !checked.insert(ctr_name) {
-        return Err(format!("Duplicated name '{ctr_name}'"));
+        return Err(format!("Duplicated top-level name '{ctr_name}'"));
       }
     }
 
     for def_name in self.def_names.names() {
       if !checked.insert(def_name) {
-        return Err(format!("Duplicated name '{def_name}'"));
+        return Err(format!("Duplicated top-level name '{def_name}'"));
       }
     }
 

src/term/check/type_check.rs

@@ -1,15 +1,7 @@
-use crate::term::{Book, DefId, Definition, Name, Pattern};
+use crate::term::{Book, DefId, Definition, Name, Pattern, Type};
 use core::fmt;
 use std::collections::HashMap;
 
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum Type {
-  Any,
-  Tup,
-  Num,
-  Adt(Name),
-}
-
 pub type DefinitionTypes = HashMap<DefId, Vec<Type>>;
 
 impl Book {
@@ -19,7 +11,9 @@ impl Book {
   pub fn infer_def_types(&self) -> Result<DefinitionTypes, String> {
     let mut def_types = HashMap::new();
     for (def_id, def) in &self.defs {
-      let def_type = def.infer_type(&self.ctrs)?;
+      let def_type = def
+        .infer_type(&self.ctrs)
+        .map_err(|e| format!("In definition '{}': {}", self.def_names.name(def_id).unwrap(), e))?;
       def_types.insert(*def_id, def_type);
     }
     Ok(def_types)
@@ -44,20 +38,7 @@ pub fn infer_arg_type<'a>(
 ) -> Result<Type, String> {
   let mut arg_type = Type::Any;
   for pat in pats {
-    let pat_type = match pat {
-      Pattern::Var(_) => Type::Any,
-      Pattern::Ctr(ctr_nam, _) => {
-        if let Some(adt_nam) = ctrs.get(ctr_nam) {
-          Type::Adt(adt_nam.clone())
-        } else {
-          return Err(format!("Unknown constructor '{ctr_nam}'"));
-        }
-      }
-      Pattern::Tup(..) => Type::Tup,
-      Pattern::Num(..) => Type::Num,
-      Pattern::List(..) => unreachable!(),
-    };
-    unify(pat_type, &mut arg_type)?
+    unify(pat.to_type(ctrs)?, &mut arg_type)?;
   }
   Ok(arg_type)
 }

src/term/check/unbound_pats.rs

@@ -9,7 +9,7 @@ impl Book {
       let def_name = self.def_names.name(&def.def_id).unwrap();
       for rule in &def.rules {
         for pat in &rule.pats {
-          pat.check_unbounds(&is_ctr, def_name)?;
+          pat.check_unbounds(&is_ctr).map_err(|e| format!("In definition '{}': {}", def_name, e))?;
         }
       }
     }
@@ -18,10 +18,10 @@ impl Book {
 }
 
 impl Pattern {
-  pub fn check_unbounds(&self, is_ctr: &impl Fn(&Name) -> bool, def_name: &Name) -> Result<(), String> {
+  pub fn check_unbounds(&self, is_ctr: &impl Fn(&Name) -> bool) -> Result<(), String> {
     let unbounds = self.unbound_pats(is_ctr);
     if let Some(unbound) = unbounds.iter().next() {
-      Err(format!("Unbound constructor '{unbound}' in definition '{def_name}'"))
+      Err(format!("Unbound constructor '{unbound}'"))
     } else {
       Ok(())
     }
@@ -50,18 +50,18 @@ impl Pattern {
 }
 
 impl Term {
-  pub fn check_unbound_pats(&self, is_ctr: &impl Fn(&Name) -> bool, def_name: &Name) -> Result<(), String> {
+  pub fn check_unbound_pats(&self, is_ctr: &impl Fn(&Name) -> bool) -> Result<(), String> {
     match self {
       Term::Let { pat, val, nxt } => {
-        pat.check_unbounds(is_ctr, def_name)?;
-        val.check_unbound_pats(is_ctr, def_name)?;
-        nxt.check_unbound_pats(is_ctr, def_name)?;
+        pat.check_unbounds(is_ctr)?;
+        val.check_unbound_pats(is_ctr)?;
+        nxt.check_unbound_pats(is_ctr)?;
       }
       Term::Match { scrutinee, arms } => {
-        scrutinee.check_unbound_pats(is_ctr, def_name)?;
+        scrutinee.check_unbound_pats(is_ctr)?;
         for (pat, body) in arms {
-          pat.check_unbounds(is_ctr, def_name)?;
-          body.check_unbound_pats(is_ctr, def_name)?;
+          pat.check_unbounds(is_ctr)?;
+          body.check_unbound_pats(is_ctr)?;
         }
       }
       Term::App { fun: fst, arg: snd, .. }
@@ -69,10 +69,10 @@ impl Term {
       | Term::Dup { val: fst, nxt: snd, .. }
       | Term::Sup { fst, snd, .. }
       | Term::Opx { fst, snd, .. } => {
-        fst.check_unbound_pats(is_ctr, def_name)?;
-        snd.check_unbound_pats(is_ctr, def_name)?;
+        fst.check_unbound_pats(is_ctr)?;
+        snd.check_unbound_pats(is_ctr)?;
       }
-      Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.check_unbound_pats(is_ctr, def_name)?,
+      Term::Lam { bod, .. } | Term::Chn { bod, .. } => bod.check_unbound_pats(is_ctr)?,
       Term::List { .. } => unreachable!(),
       Term::Var { .. }
       | Term::Lnk { .. }

src/term/check/unbound_vars.rs

@@ -5,10 +5,12 @@ use std::collections::HashMap;
 impl Book {
   /// Checks that there are no unbound variables in all definitions.
   pub fn check_unbound_vars(&self) -> Result<(), String> {
-    for (def_id, def) in &self.defs {
+    for def in self.defs.values() {
       def.assert_no_pattern_matching_rules();
-      let def_name = self.def_names.name(def_id).unwrap();
-      def.rules[0].body.check_unbound_vars(def_name)?;
+      def.rules[0]
+        .body
+        .check_unbound_vars()
+        .map_err(|e| format!("In definition '{}': {}", self.def_names.name(&def.def_id).unwrap(), e))?;
     }
     Ok(())
   }
@@ -17,14 +19,14 @@ impl Book {
 impl Term {
   /// Checks that all variables are bound.
   /// Precondition: References have been resolved.
-  pub fn check_unbound_vars(&self, def_name: &Name) -> Result<(), String> {
+  pub fn check_unbound_vars(&self) -> Result<(), String> {
     let mut globals = HashMap::new();
-    check_uses(self, &mut HashMap::new(), &mut globals, def_name)?;
+    check_uses(self, &mut HashMap::new(), &mut globals)?;
 
     // Check global vars
     for (nam, (declared, used)) in globals.into_iter() {
       if used && !declared {
-        return Err(format!("Unbound unscoped variable '${nam}' in definition '{def_name}'"));
+        return Err(format!("Unbound unscoped variable '${nam}'"));
       }
     }
     Ok(())
@@ -37,59 +39,58 @@ pub fn check_uses<'a>(
   term: &'a Term,
   scope: &mut HashMap<&'a Name, Val>,
   globals: &mut HashMap<&'a Name, (bool, bool)>,
-  def_name: &Name,
 ) -> Result<(), String> {
   // TODO: Don't stop at the first error
   match term {
     Term::Lam { nam, bod, .. } => {
       push_scope(nam.as_ref(), scope);
-      check_uses(bod, scope, globals, def_name)?;
+      check_uses(bod, scope, globals)?;
       pop_scope(nam.as_ref(), scope);
     }
     Term::Var { nam } => {
       if !scope.contains_key(nam) {
-        return Err(format!("Unbound variable '{nam}' in definition '{def_name}'"));
+        return Err(format!("Unbound variable '{nam}'"));
       }
     }
     Term::Chn { nam, bod, .. } => {
       globals.entry(nam).or_default().0 = true;
-      check_uses(bod, scope, globals, def_name)?;
+      check_uses(bod, scope, globals)?;
     }
     Term::Lnk { nam } => {
       globals.entry(nam).or_default().1 = true;
     }
     Term::Let { pat: Pattern::Var(nam), val, nxt } => {
-      check_uses(val, scope, globals, def_name)?;
+      check_uses(val, scope, globals)?;
       push_scope(nam.as_ref(), scope);
-      check_uses(nxt, scope, globals, def_name)?;
+      check_uses(nxt, scope, globals)?;
       pop_scope(nam.as_ref(), scope);
     }
     Term::Dup { fst, snd, val, nxt, .. }
     | Term::Let { pat: Pattern::Tup(box Pattern::Var(fst), box Pattern::Var(snd)), val, nxt } => {
-      check_uses(val, scope, globals, def_name)?;
+      check_uses(val, scope, globals)?;
       push_scope(fst.as_ref(), scope);
       push_scope(snd.as_ref(), scope);
-      check_uses(nxt, scope, globals, def_name)?;
+      check_uses(nxt, scope, globals)?;
       pop_scope(fst.as_ref(), scope);
       pop_scope(snd.as_ref(), scope);
     }
     Term::Let { .. } => unreachable!(),
     Term::App { fun, arg, .. } => {
-      check_uses(fun, scope, globals, def_name)?;
-      check_uses(arg, scope, globals, def_name)?;
+      check_uses(fun, scope, globals)?;
+      check_uses(arg, scope, globals)?;
     }
     Term::Tup { fst, snd } | Term::Sup { fst, snd, .. } | Term::Opx { fst, snd, .. } => {
-      check_uses(fst, scope, globals, def_name)?;
-      check_uses(snd, scope, globals, def_name)?;
+      check_uses(fst, scope, globals)?;
+      check_uses(snd, scope, globals)?;
     }
     Term::Match { scrutinee, arms } => {
-      check_uses(scrutinee, scope, globals, def_name)?;
+      check_uses(scrutinee, scope, globals)?;
       for (pat, term) in arms {
         if let Pattern::Num(MatchNum::Succ(Some(nam))) = pat {
           push_scope(nam.as_ref(), scope);
         }
 
-        check_uses(term, scope, globals, def_name)?;
+        check_uses(term, scope, globals)?;
 
         if let Pattern::Num(MatchNum::Succ(Some(nam))) = pat {
           pop_scope(nam.as_ref(), scope);

src/term/display.rs

@@ -108,7 +108,7 @@ impl fmt::Display for Pattern {
       }
       Pattern::Num(num) => write!(f, "{num}"),
       Pattern::Tup(fst, snd) => write!(f, "({}, {})", fst, snd,),
-      Pattern::List(pats) => write!(f, "[{}]", DisplayJoin(|| pats.iter().map(|p| display!("{p}")), ", "))
+      Pattern::List(pats) => write!(f, "[{}]", DisplayJoin(|| pats.iter().map(|p| display!("{p}")), ", ")),
     }
   }
 }

src/term/mod.rs

@@ -14,6 +14,8 @@ pub mod transform;
 pub use net_to_term::{net_to_term, ReadbackError};
 pub use term_to_net::{book_to_nets, term_to_compat_net};
 
+use self::transform::encode_lists;
+
 /// The representation of a program.
 #[derive(Debug, Clone, Default)]
 pub struct Book {
@@ -168,7 +170,16 @@ pub enum Op {
   NOT,
 }
 
-/// A user defined  datatype
+/// Pattern types.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum Type {
+  Any,
+  Tup,
+  Num,
+  Adt(Name),
+}
+
+/// A user defined datatype
 #[derive(Debug, Clone, Default)]
 pub struct Adt {
   pub ctrs: IndexMap<Name, Vec<Name>>,
@@ -546,6 +557,23 @@ impl Pattern {
       }
     }
   }
+
+  pub fn to_type(&self, ctrs: &HashMap<Name, Name>) -> Result<Type, String> {
+    let typ = match self {
+      Pattern::Var(_) => Type::Any,
+      Pattern::Ctr(ctr_nam, _) => {
+        if let Some(adt_nam) = ctrs.get(ctr_nam) {
+          Type::Adt(adt_nam.clone())
+        } else {
+          return Err(format!("Unknown constructor '{ctr_nam}'"));
+        }
+      }
+      Pattern::Tup(..) => Type::Tup,
+      Pattern::Num(..) => Type::Num,
+      Pattern::List(..) => Type::Adt(Name::new(encode_lists::LIST)),
+    };
+    Ok(typ)
+  }
 }
 
 impl Rule {

src/term/parser/parser.rs

@@ -357,8 +357,8 @@ where
     .then_ignore(just(Token::Equals))
 }
 
-/// This rule always emits an error when it parses successfully 
-/// It is used to report a parsing error that would be unclear otherwise 
+/// This rule always emits an error when it parses successfully
+/// It is used to report a parsing error that would be unclear otherwise
 fn rule_body_missing_paren<'a, I>()
 -> impl Parser<'a, I, ((Name, Vec<Pattern>), Term), extra::Err<Rich<'a, Token>>>
 where

src/term/term_to_net.rs

@@ -258,7 +258,7 @@ impl<'a> EncodeTermState<'a> {
         self.inet.link(Port(node, 1), Port(node, 2));
         Some(Port(node, 0))
       }
-      Term::Str { .. } => unreachable!(), // Removed in desugar str
+      Term::Str { .. } => unreachable!(),  // Removed in desugar str
       Term::List { .. } => unreachable!(), // Removed in desugar list
       // core: & fst ~ <op snd ret>
       Term::Opx { op, fst, snd } => {

src/term/transform/desugar_match_expressions.rs

@@ -0,0 +1,306 @@
+use crate::term::{
+  display::DisplayJoin, Book, DefId, DefNames, Definition, MatchNum, Name, Op, Pattern, Rule, Tag, Term, Type,
+};
+use indexmap::IndexSet;
+use itertools::Itertools;
+use std::collections::{BTreeMap, HashMap, HashSet};
+
+impl Book {
+  /// Extracts any match terms into pattern matching functions.
+  /// Creates rules with potentially nested patterns, so the flattening pass needs to be called after.
+  pub fn extract_matches(&mut self) -> Result<(), String> {
+    let book = &mut MatchesBook::new(&mut self.def_names);
+
+    for (def_id, def) in &mut self.defs {
+      let def_name = book.def_names.name(def_id).cloned().unwrap();
+      for rule in def.rules.iter_mut() {
+        rule.body.extract_matches(&def_name, &self.ctrs, book, &mut 0).map_err(|err| err.to_string())?;
+      }
+    }
+
+    self.defs.append(&mut book.new_defs);
+    Ok(())
+  }
+}
+
+struct MatchesBook<'book> {
+  def_names: &'book mut DefNames,
+  new_defs: BTreeMap<DefId, Definition>,
+}
+
+impl<'book> MatchesBook<'book> {
+  fn new(def_names: &'book mut DefNames) -> Self {
+    Self { def_names, new_defs: BTreeMap::<DefId, Definition>::new() }
+  }
+}
+
+#[derive(Debug)]
+pub enum MatchError {
+  Empty,
+  Infer(String),
+  Repeated(Name),
+  Missing(HashSet<Name>),
+  LetPat(Box<MatchError>),
+}
+
+impl std::error::Error for MatchError {}
+
+impl std::fmt::Display for MatchError {
+  fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+    fn ctrs_plural_or_sing(n: usize) -> &'static str {
+      if n > 1 { "constructors" } else { "a constructor" }
+    }
+
+    match self {
+      MatchError::Empty => write!(f, "Empty match block found"),
+      MatchError::Infer(err) => write!(f, "{err}"),
+      MatchError::Repeated(bind) => write!(f, "Repeated var name in a match block: {}", bind),
+      MatchError::Missing(names) => {
+        let constructor = ctrs_plural_or_sing(names.len());
+        let missing = DisplayJoin(|| names.iter(), ", ");
+        write!(f, "Missing {constructor} in a match block: {missing}")
+      }
+      MatchError::LetPat(err) => {
+        let let_err = err.to_string().replace("match block", "let bind");
+        write!(f, "{let_err}")?;
+
+        if matches!(err.as_ref(), MatchError::Missing(_)) {
+          write!(f, "\nConsider using a match block instead")?;
+        }
+
+        Ok(())
+      }
+    }
+  }
+}
+
+impl Term {
+  fn extract_matches(
+    &mut self,
+    def_name: &Name,
+    ctrs: &HashMap<Name, Name>,
+    book: &mut MatchesBook,
+    match_count: &mut usize,
+  ) -> Result<(), MatchError> {
+    match self {
+      Term::Match { scrutinee: box Term::Var { nam }, arms } => {
+        if arms.is_empty() {
+          return Err(MatchError::Empty);
+        }
+
+        for (_, term) in arms.iter_mut() {
+          term.extract_matches(def_name, ctrs, book, match_count)?;
+        }
+
+        let matched_type = infer_match_type(arms.iter().map(|(x, _)| x), ctrs)?;
+        match matched_type {
+          // This match is useless, will always go with the first rule.
+          // TODO: Throw a warning in this case
+          Type::Any => {
+            // Inside the match we renamed the variable, so we need to restore the name before the match to remove it.
+            let fst_arm = &mut arms[0];
+            let Pattern::Var(var) = &fst_arm.0 else { unreachable!() };
+            let body = &mut fst_arm.1;
+            if let Some(var) = var {
+              body.subst(var, &Term::Var { nam: nam.clone() });
+            }
+            *self = std::mem::take(body);
+          }
+          // Matching on nums is a primitive operation, we can leave it as is.
+          // Not extracting into a separate definition allows us to create very specific inets with the MATCH node.
+          Type::Num => normalize_num_match(self)?,
+          // TODO: It would be nice to also not extract tuple matches,
+          // but if they have nested patterns it gets more complicated.
+          // For now, we use `let (a, b) = x` to get the specific desired inet.
+          _ => {
+            *match_count += 1;
+            let nam = std::mem::take(nam);
+            let arms = std::mem::take(arms);
+            *self = match_to_def(nam, &arms, def_name, book, *match_count);
+          }
+        }
+      }
+
+      Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
+        bod.extract_matches(def_name, ctrs, book, match_count)?;
+      }
+      Term::App { fun: fst, arg: snd, .. }
+      | Term::Let { pat: Pattern::Var(_), val: fst, nxt: snd }
+      | Term::Dup { val: fst, nxt: snd, .. }
+      | Term::Tup { fst, snd }
+      | Term::Sup { fst, snd, .. }
+      | Term::Opx { fst, snd, .. } => {
+        fst.extract_matches(def_name, ctrs, book, match_count)?;
+        snd.extract_matches(def_name, ctrs, book, match_count)?;
+      }
+      Term::Var { .. }
+      | Term::Lnk { .. }
+      | Term::Num { .. }
+      | Term::Str { .. }
+      | Term::Ref { .. }
+      | Term::Era => {}
+
+      Term::List { .. } => unreachable!(),
+      Term::Match { .. } => unreachable!("Scrutinee of match expression should have been extracted already"),
+      Term::Let { pat, .. } => {
+        unreachable!("Destructor let expression should have been desugared already. {pat}")
+      }
+    }
+
+    Ok(())
+  }
+}
+
+/// Transforms a match into a new definition with every arm of `arms` as a rule.
+/// The result is the new def applied to the scrutinee followed by the free vars of the arms.
+fn match_to_def(
+  scrutinee: Name,
+  arms: &[(Pattern, Term)],
+  def_name: &Name,
+  book: &mut MatchesBook,
+  match_count: usize,
+) -> Term {
+  let free_vars: IndexSet<Name> = arms
+    .iter()
+    .flat_map(|(pat, term)| term.free_vars().into_keys().filter(|k| !pat.names().contains(k)))
+    .collect();
+
+  let mut rules: Vec<Rule> =
+    arms.iter().map(|(pat, term)| Rule { pats: vec![pat.clone()], body: term.clone() }).collect();
+
+  // Extend the rules with the free variables
+  for rule in &mut rules {
+    for var in &free_vars {
+      rule.pats.push(Pattern::Var(Some(var.clone())));
+    }
+  }
+
+  let new_name = make_def_name(def_name, &Name::new("match"), match_count);
+  let def_id = book.def_names.insert(new_name);
+  let def = Definition { def_id, generated: true, rules };
+  book.new_defs.insert(def_id, def);
+
+  let scrutinee_app = Term::App {
+    tag: Tag::Static,
+    fun: Box::new(Term::Ref { def_id }),
+    arg: Box::new(Term::Var { nam: scrutinee }),
+  };
+
+  free_vars.into_iter().fold(scrutinee_app, |acc, nam| Term::App {
+    tag: Tag::Static,
+    fun: Box::new(acc),
+    arg: Box::new(Term::Var { nam }),
+  })
+}
+
+fn make_def_name(def_name: &Name, ctr: &Name, i: usize) -> Name {
+  Name(format!("{def_name}${ctr}${i}"))
+}
+
+/// Finds the expected type of the matched argument.
+/// Errors on incompatible types.
+/// Short-circuits if the first pattern is Type::Any.
+fn infer_match_type<'a>(
+  pats: impl Iterator<Item = &'a Pattern>,
+  ctrs: &HashMap<Name, Name>,
+) -> Result<Type, MatchError> {
+  let mut match_type = None;
+  for pat in pats {
+    let new_type = pat.to_type(ctrs).map_err(MatchError::Infer)?;
+    match (new_type, &mut match_type) {
+      (new, None) => match_type = Some(new),
+      // TODO: Should we throw a type inference error in this case?
+      // Since anything else will be sort of the wrong type (expected Var).
+      (_, Some(Type::Any)) => (),
+      (Type::Any, Some(_)) => (),
+      (Type::Tup, Some(Type::Tup)) => (),
+      (Type::Num, Some(Type::Num)) => (),
+      (Type::Adt(nam_new), Some(Type::Adt(nam_old))) if &nam_new == nam_old => (),
+      (new, Some(old)) => {
+        return Err(MatchError::Infer(format!("Type mismatch. Found '{}' expected {}.", new, old)));
+      }
+    };
+  }
+  Ok(match_type.unwrap())
+}
+
+/// Transforms a match on Num with any possible patterns into 'match x {0: ...; +: @x-1 ...}'.
+fn normalize_num_match(term: &mut Term) -> Result<(), MatchError> {
+  let Term::Match { scrutinee: _, arms } = term else { unreachable!() };
+
+  let mut zero_arm = None;
+  for (pat, body) in arms.iter_mut() {
+    match pat {
+      Pattern::Num(MatchNum::Zero) => {
+        zero_arm = Some((Pattern::Num(MatchNum::Zero), std::mem::take(body)));
+        break;
+      }
+      Pattern::Var(var) => {
+        if let Some(var) = var {
+          body.subst(var, &Term::Num { val: 0 });
+        }
+        zero_arm = Some((Pattern::Num(MatchNum::Zero), std::mem::take(body)));
+        break;
+      }
+      Pattern::Num(_) => (),
+      _ => unreachable!(),
+    }
+  }
+
+  let mut succ_arm = None;
+  for (pat, body) in arms.iter_mut() {
+    match pat {
+      // Var already detached.
+      // match x {0: ...; +: ...}
+      Pattern::Num(MatchNum::Succ(None)) => {
+        let body = std::mem::take(body);
+        succ_arm = Some((Pattern::Num(MatchNum::Succ(None)), body));
+        break;
+      }
+      // Need to detach var.
+      // match x {0: ...; +: @x-1 ...}
+      Pattern::Num(MatchNum::Succ(Some(var))) => {
+        let body = Term::Lam { tag: Tag::Static, nam: var.clone(), bod: Box::new(std::mem::take(body)) };
+        succ_arm = Some((Pattern::Num(MatchNum::Succ(None)), body));
+        break;
+      }
+      // Need to detach and increment again.
+      // match x {0: ...; +: @x-1 let x = (+ x-1 1); ...}
+      Pattern::Var(Some(var)) => {
+        let body = Term::Lam {
+          tag: Tag::Static,
+          nam: Some(Name::new("%pred")),
+          bod: Box::new(Term::Let {
+            pat: Pattern::Var(Some(var.clone())),
+            val: Box::new(Term::Opx {
+              op: Op::ADD,
+              fst: Box::new(Term::Var { nam: Name::new("%pred") }),
+              snd: Box::new(Term::Num { val: 1 }),
+            }),
+            nxt: Box::new(std::mem::take(body)),
+          }),
+        };
+        succ_arm = Some((Pattern::Num(MatchNum::Succ(None)), body));
+        break;
+      }
+      // Var unused, so no need to increment
+      // match x {0: ...; +: @* ...}
+      Pattern::Var(None) => {
+        let body = Term::Lam { tag: Tag::Static, nam: None, bod: Box::new(std::mem::take(body)) };
+        succ_arm = Some((Pattern::Num(MatchNum::Succ(None)), body));
+        break;
+      }
+      Pattern::Num(_) => (),
+      _ => unreachable!(),
+    }
+  }
+
+  let Some(zero_arm) = zero_arm else {
+    return Err(MatchError::Missing(HashSet::from_iter([Name::new("0")])));
+  };
+  let Some(succ_arm) = succ_arm else {
+    return Err(MatchError::Missing(HashSet::from_iter([Name::new("0")])));
+  };
+  *arms = vec![zero_arm, succ_arm];
+  Ok(())
+}

src/term/transform/encode_lists.rs

@@ -2,11 +2,11 @@ use indexmap::IndexMap;
 
 use crate::term::{Adt, Book, Name, Pattern, Tag, Term};
 
-const LIST: &str = "List";
-const LCONS: &str = "LCons";
-const LNIL: &str = "LNil";
-const HEAD: &str = "head";
-const TAIL: &str = "tail";
+pub const LIST: &str = "List";
+pub const LCONS: &str = "LCons";
+pub const LNIL: &str = "LNil";
+pub const HEAD: &str = "head";
+pub const TAIL: &str = "tail";
 
 impl Book {
   pub fn encode_lists(&mut self) -> Result<(), String> {
@@ -52,7 +52,7 @@ impl Term {
       Term::List { els } => {
         let lnil = Term::Var { nam: Name::new(LNIL) };
 
-        *self = els.into_iter().rfold(lnil, |acc, nxt| {
+        *self = els.iter_mut().rfold(lnil, |acc, nxt| {
           nxt.encode_lists();
           let lcons_app = Term::App {
             tag: Tag::Static,
@@ -104,7 +104,7 @@ impl Pattern {
       Pattern::List(pats) => {
         let lnil = Pattern::Var(Some(Name::new(LNIL)));
 
-        *self = pats.into_iter().rfold(lnil, |acc, nxt| {
+        *self = pats.iter_mut().rfold(lnil, |acc, nxt| {
           nxt.encode_lists();
           Pattern::Ctr(Name::new(LCONS), vec![nxt.clone(), acc])
         });

src/term/transform/encode_pattern_matching.rs

@@ -1,6 +1,5 @@
 use crate::term::{
-  check::type_check::{DefinitionTypes, Type},
-  Book, DefId, MatchNum, Name, Pattern, Rule, Tag, Term,
+  check::type_check::DefinitionTypes, Book, DefId, MatchNum, Name, Pattern, Rule, Tag, Term, Type,
 };
 
 impl Book {
@@ -33,7 +32,7 @@ fn make_non_pattern_matching_def(book: &mut Book, def_id: DefId) {
   def.rules = vec![rule];
 }
 
-/// For function that do pattern match,
+/// For functions that do pattern match,
 ///  we break them into a tree of small matching functions
 ///  with the original rule bodies at the end.
 fn make_pattern_matching_def(book: &mut Book, def_id: DefId, def_type: &[Type]) {
@@ -93,6 +92,7 @@ fn make_rule_body(mut body: Term, pats: &[Pattern]) -> Term {
   body
 }
 
+/// Builds the encoding for the patterns in a pattern matching function.
 fn make_pattern_matching_case(
   book: &mut Book,
   def_type: &[Type],

src/term/transform/extract_matches.rs

@@ -1,209 +0,0 @@
-use crate::term::{
-  check::type_check::{infer_arg_type, Type},
-  display::DisplayJoin,
-  Adt, Book, DefId, DefNames, Definition, Name, Pattern, Rule, Tag, Term,
-};
-use indexmap::IndexSet;
-use itertools::Itertools;
-use std::collections::{BTreeMap, HashMap, HashSet};
-
-impl Book {
-  /// Extracts any match terms into pattern matching functions.
-  /// Creates rules with potentially nested patterns, so the flattening pass needs to be called after.
-  pub fn extract_matches(&mut self) -> Result<(), String> {
-    let book = &mut MatchesBook::new(&mut self.def_names);
-
-    for (def_id, def) in &mut self.defs {
-      let def_name = book.def_names.name(def_id).cloned().unwrap();
-      for rule in def.rules.iter_mut() {
-        rule.body.extract_matches(&def_name, book, &mut 0).map_err(|err| err.to_string())?;
-      }
-    }
-
-    self.defs.append(&mut book.new_defs);
-    Ok(())
-  }
-}
-
-struct MatchesBook<'book> {
-  def_names: &'book mut DefNames,
-  new_defs: BTreeMap<DefId, Definition>,
-}
-
-impl<'book> MatchesBook<'book> {
-  fn new(def_names: &'book mut DefNames) -> Self {
-    Self { def_names, new_defs: BTreeMap::<DefId, Definition>::new() }
-  }
-}
-
-#[derive(Debug)]
-pub enum MatchError {
-  Empty,
-  Infer(String),
-  Repeated(Name),
-  Missing(HashSet<Name>),
-  LetPat(Box<MatchError>),
-}
-
-impl std::error::Error for MatchError {}
-
-impl std::fmt::Display for MatchError {
-  fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-    fn ctrs_plural_or_sing(n: usize) -> &'static str {
-      if n > 1 { "constructors" } else { "a constructor" }
-    }
-
-    match self {
-      MatchError::Empty => write!(f, "Empty match block found"),
-      MatchError::Infer(err) => write!(f, "{err}"),
-      MatchError::Repeated(bind) => write!(f, "Repeated var name in a match block: {}", bind),
-      MatchError::Missing(names) => {
-        let constructor = ctrs_plural_or_sing(names.len());
-        let missing = DisplayJoin(|| names.iter(), ", ");
-        write!(f, "Missing {constructor} in a match block: {missing}")
-      }
-      MatchError::LetPat(err) => {
-        let let_err = err.to_string().replace("match block", "let bind");
-        write!(f, "{let_err}")?;
-
-        if matches!(err.as_ref(), MatchError::Missing(_)) {
-          write!(f, "\nConsider using a match block instead")?;
-        }
-
-        Ok(())
-      }
-    }
-  }
-}
-
-impl Term {
-  pub fn check_matches<'book>(
-    pats: &[Pattern],
-    adts: &'book BTreeMap<Name, Adt>,
-    ctrs: &'book HashMap<Name, Name>,
-  ) -> Result<&'book Adt, MatchError> {
-    let pat_type = infer_arg_type(pats.iter(), ctrs).map_err(MatchError::Infer)?;
-    let Type::Adt(nam) = pat_type else { unreachable!() };
-    let Adt { ctrs } = &adts[&nam];
-
-    let mut missing: HashSet<_> = ctrs.keys().cloned().collect();
-
-    for rule in pats {
-      let Pattern::Ctr(nam, args) = rule else { unreachable!() };
-
-      let mut binds = HashSet::new();
-      for arg in args {
-        for bind in arg.names() {
-          if !binds.insert(bind) {
-            return Err(MatchError::Repeated(bind.clone()));
-          }
-        }
-      }
-      missing.remove(nam);
-    }
-
-    if !missing.is_empty() {
-      return Err(MatchError::Missing(missing));
-    }
-
-    Ok(&adts[&nam])
-  }
-
-  fn extract_matches(
-    &mut self,
-    def_name: &Name,
-    book: &mut MatchesBook,
-    match_count: &mut usize,
-  ) -> Result<(), MatchError> {
-    match self {
-      Term::Match { scrutinee: box Term::Var { nam }, arms } => {
-        if arms.is_empty() {
-          return Err(MatchError::Empty);
-        }
-
-        for (_, term) in arms.iter_mut() {
-          term.extract_matches(def_name, book, match_count)?;
-        }
-
-        *match_count += 1;
-
-        let nam = std::mem::take(nam);
-        let arms = std::mem::take(arms);
-        *self = match_to_def(nam, &arms, def_name, book, *match_count);
-      }
-
-      Term::Lam { bod, .. } | Term::Chn { bod, .. } => {
-        bod.extract_matches(def_name, book, match_count)?;
-      }
-      Term::App { fun: fst, arg: snd, .. }
-      | Term::Let { pat: Pattern::Var(_), val: fst, nxt: snd }
-      | Term::Dup { val: fst, nxt: snd, .. }
-      | Term::Tup { fst, snd }
-      | Term::Sup { fst, snd, .. }
-      | Term::Opx { fst, snd, .. } => {
-        fst.extract_matches(def_name, book, match_count)?;
-        snd.extract_matches(def_name, book, match_count)?;
-      }
-      Term::Var { .. }
-      | Term::Lnk { .. }
-      | Term::Num { .. }
-      | Term::Str { .. }
-      | Term::Ref { .. }
-      | Term::Era => {}
-
-      Term::Match { .. } => unreachable!("Scrutinee of match expression should have been extracted already"),
-      Term::Let { pat, .. } => {
-        unreachable!("Destructor let expression should have been desugared already. {pat}")
-      }
-      Term::List { .. } => unreachable!("Should have been desugared already"),
-    }
-
-    Ok(())
-  }
-}
-
-/// Transforms a match into a new definition with every arm of `arms` as a rule.
-/// The result is the new def applied to the scrutinee followed by the free vars of the arms.
-fn match_to_def(
-  scrutinee: Name,
-  arms: &[(Pattern, Term)],
-  def_name: &Name,
-  book: &mut MatchesBook,
-  match_count: usize,
-) -> Term {
-  let free_vars: IndexSet<Name> = arms
-    .iter()
-    .flat_map(|(pat, term)| term.free_vars().into_keys().filter(|k| !pat.names().contains(k)))
-    .collect();
-
-  let mut rules: Vec<Rule> =
-    arms.iter().map(|(pat, term)| Rule { pats: vec![pat.clone()], body: term.clone() }).collect();
-
-  // Extend the rules with the free variables
-  for rule in &mut rules {
-    for var in &free_vars {
-      rule.pats.push(Pattern::Var(Some(var.clone())));
-    }
-  }
-
-  let new_name = make_def_name(def_name, &Name::new("match"), match_count);
-  let def_id = book.def_names.insert(new_name);
-  let def = Definition { def_id, generated: true, rules };
-  book.new_defs.insert(def_id, def);
-
-  let scrutinee_app = Term::App {
-    tag: Tag::Static,
-    fun: Box::new(Term::Ref { def_id }),
-    arg: Box::new(Term::Var { nam: scrutinee }),
-  };
-
-  free_vars.into_iter().fold(scrutinee_app, |acc, nam| Term::App {
-    tag: Tag::Static,
-    fun: Box::new(acc),
-    arg: Box::new(Term::Var { nam }),
-  })
-}
-
-fn make_def_name(def_name: &Name, ctr: &Name, i: usize) -> Name {
-  Name(format!("{def_name}${ctr}${i}"))
-}

src/term/transform/flatten.rs

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

src/term/transform/mod.rs

@@ -1,13 +1,13 @@
 pub mod definition_pruning;
 pub mod desugar_implicit_match_binds;
 pub mod desugar_let_destructors;
+pub mod desugar_match_expressions;
 pub mod detach_supercombinators;
 pub mod encode_adts;
 pub mod encode_lists;
 pub mod encode_pattern_matching;
 pub mod encode_strs;
 pub mod eta_reduction;
-pub mod extract_matches;
 pub mod flatten;
 pub mod linearize;
 pub mod resolve_ctrs_in_pats;

src/term/transform/simplify_main_ref.rs

@@ -2,7 +2,7 @@ use crate::term::{Book, DefId, Term};
 
 impl Book {
   /// When main is simply directly calling another function, we substitute the ref with a copy of its body.
-  /// 
+  ///
   /// This is performed because Hvm-Core produces inconsistent outputs in the parallel mode when such pattern is present
   pub fn simplify_main_ref(&mut self, main: DefId) {
     while let Term::Ref { def_id } = &self.defs.get(&main).unwrap().rules[0].body {

tests/golden_tests.rs

@@ -79,7 +79,7 @@ fn run_golden_test_dir(test_name: &str, run: &dyn Fn(&str) -> Result<String, Str
 fn compile_term() {
   run_golden_test_dir(function_name!(), &|code| {
     let mut term = do_parse_term(code)?;
-    term.check_unbound_vars(&hvml::term::Name::new(""))?;
+    term.check_unbound_vars()?;
     term.make_var_names_unique();
     term.linearize_vars();
     let compat_net = term_to_compat_net(&term, &mut Default::default());

tests/golden_tests/compile_file/extracted_match_pred.hvm

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

tests/golden_tests/compile_file_o0/match_num_all_patterns.hvm

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

tests/golden_tests/compile_file_o0/match_num_unscoped_lambda.hvm

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

tests/snapshots/compile_file__bad_parens_making_erased_let.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/bad_parens_making_erased_let.hvm
 ---
-Unbound variable 'two' in definition 'main'
+In definition 'main': Unbound variable 'two'

tests/snapshots/compile_file__cyclic_dup.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/cyclic_dup.hvm
 ---
-Unbound variable 'y1' in definition 'main'
+In definition 'main': Unbound variable 'y1'

tests/snapshots/compile_file__extracted_match_pred.hvm.snap

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

tests/snapshots/compile_file__let_adt_non_exhaustive.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/let_adt_non_exhaustive.hvm
 ---
-Non-exhaustive pattern at definition 'main$match$1'. Hint: (main$match$1 None) not covered.
+In definition 'main$match$1': Non-exhaustive pattern. Hint: (main$match$1 None) not covered.

tests/snapshots/compile_file__match_adt_non_exhaustive.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/match_adt_non_exhaustive.hvm
 ---
-Non-exhaustive pattern at definition 'main$match$1$F0'. Hint: (main$match$1$F0 Some) not covered.
+In definition 'main$match$1$F0': Non-exhaustive pattern. Hint: (main$match$1$F0 Some) not covered.

tests/snapshots/compile_file__match_num_explicit_bind.hvm.snap

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

tests/snapshots/compile_file__non_exhaustive_and.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/non_exhaustive_and.hvm
 ---
-Non-exhaustive pattern at definition 'Bool.and'. Hint: (Bool.and F T) not covered.
+In definition 'Bool.and': Non-exhaustive pattern. Hint: (Bool.and F T) not covered.

tests/snapshots/compile_file__non_exhaustive_different_types.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/non_exhaustive_different_types.hvm
 ---
-Non-exhaustive pattern at definition 'foo'. Hint: (foo f1 f2 t3 f4) not covered.
+In definition 'foo': Non-exhaustive pattern. Hint: (foo f1 f2 t3 f4) not covered.

tests/snapshots/compile_file__non_exhaustive_pattern.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/non_exhaustive_pattern.hvm
 ---
-Non-exhaustive pattern at definition 'Foo'. Hint: (Foo A A A A) not covered.
+In definition 'Foo': Non-exhaustive pattern. Hint: (Foo A A A A) not covered.

tests/snapshots/compile_file__non_exhaustive_tree.hvm.snap

@@ -2,4 +2,4 @@
 source: tests/golden_tests.rs
 input_file: tests/golden_tests/compile_file/non_exhaustive_tree.hvm
 ---
-Non-exhaustive pattern at definition 'Warp'. Hint: (Warp _ Both Leaf) not covered.
+In definition 'Warp': Non-exhaustive pattern. Hint: (Warp _ Both Leaf) not covered.

tests/snapshots/compile_file_o0__match_num_all_patterns.hvm.snap

@@ -0,0 +1,20 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/compile_file_o0/match_num_all_patterns.hvm
+---
+@B = (?<(#0 (a a)) b> b)
+@D = (<+ #1 <- #1 a>> a)
+@E = (<+ #1 <- #1 a>> a)
+@F = (<+ #2 a> a)
+@main = #0
+@succ_var = (?<(#0 (a a)) b> b)
+@succ_var_z = (?<(#1 @F) a> a)
+@succ_zero = (?<(#0 (a a)) b> b)
+@succ_zero_ = (?<(#0 (a a)) b> b)
+@var_succ = (a a)
+@var_zero = (a a)
+@zero_succ = (?<(#0 (a a)) b> b)
+@zero_succ_ = (?<(#0 (a a)) b> b)
+@zero_var = (?<(#0 @D) a> a)
+@zero_var_s = (?<(#0 @E) a> a)
+

tests/snapshots/compile_file_o0__match_num_unscoped_lambda.hvm.snap

@@ -0,0 +1,8 @@
+---
+source: tests/golden_tests.rs
+input_file: tests/golden_tests/compile_file_o0/match_num_unscoped_lambda.hvm
+---
+@lambda_in = (?<((a a) (b (c b))) (c d)> d)
+@lambda_out = (?<(a (b b)) c> (a c))
+@main = *
+

tests/snapshots/encode_pattern_match__var_only.hvm.snap

@@ -4,10 +4,8 @@ input_file: tests/golden_tests/encode_pattern_match/var_only.hvm
 ---
 (Foo) = λa λb λf (f a)
 
-(main) = λx (main$match$1 x)
+(main) = λx Foo
 
 (False) = #Bool λFalse #Bool λTrue False
 
 (True) = #Bool λFalse #Bool λTrue True
-
-(main$match$1) = λfalse Foo