Repository: HigherOrderCO/Bend
File: src/term/transform/encode_pattern_matching.rs (Rust)

Code before:

  // Add the lambdas to get the matched variables
  let arg_decl = new_args.chain(old_args);
  let term = arg_decl.rev().fold(term, |term, arg| Term::named_lam(arg, term));

  add_case_to_book(book, crnt_name.clone(), term);
}

fn make_num_pattern_matching_case(
  book: &mut Book,
  def_type: &[Type],
  def_id: DefId,
  crnt_name: &Name,
  crnt_rules: Vec<usize>,
  match_path: Vec<Pattern>,
) {
  use MatchNum::*;

  fn filter_rules(def_rules: &[Rule], crnt_rules: &[usize], arg_idx: usize, Name(ctr): &Name) -> Vec<usize> {
    crnt_rules
      .iter()
      .copied()
      .filter(|&rule_idx| match &def_rules[rule_idx].pats[arg_idx] {
        Pattern::Var(_) => false,
        Pattern::Ctr(_nam, _) => false,
        Pattern::Num(Succ(_)) => ctr == "+",
        Pattern::Num(Zero) => ctr == "0",
        Pattern::Tup(..) => false,
      })
      .collect()
  }

  let make_next_fn_name = |crnt_name, ctr_name: &Name| Name(format!("{crnt_name}$P{ctr_name}"));

  for (next_ctr, next_ctr_args) in vec![(Name::new("0"), vec![]), (Name::new("+"), vec![Name::new("p")])] {
    let def = &book.defs[&def_id];
    let crnt_name = make_next_fn_name(crnt_name, &next_ctr);
    let crnt_rules = filter_rules(&def.rules, &crnt_rules, match_path.len(), &next_ctr);
    let new_vars =
      Pattern::Ctr(next_ctr.clone(), vec![Pattern::Var(Some(Name::new(""))); next_ctr_args.len()]);
    let mut match_path = match_path.clone();
    match_path.push(new_vars);
    make_pattern_matching_case(book, def_type, def_id, &crnt_name, crnt_rules, match_path);
  }

  let term = Term::Var { nam: Name::new("x").clone() };
  let zero_id = book.def_names.def_id(&make_next_fn_name(crnt_name, &Name::new("0"))).unwrap();
  let succ_id = book.def_names.def_id(&make_next_fn_name(crnt_name, &Name::new("+"))).unwrap();

  let term = Term::Match {
    scrutinee: Box::new(term),

Review comment (suggestion):
Is there any case where the constructor name will not be `"+"`? If not, we can just have this return true always

Code after:
  });

  // Add the lambdas to get the matched variables
  let arg_decl = new_args.chain(old_args);
  let term = arg_decl.rev().fold(term, |term, arg| Term::named_lam(arg, term));

  add_case_to_book(book, crnt_name.clone(), term);
}

fn make_num_pattern_matching_case(
  book: &mut Book,
  def_type: &[Type],
  def_id: DefId,
  crnt_name: &Name,
  crnt_rules: Vec<usize>,
  match_path: Vec<Pattern>,
) {
  use MatchNum::*;

  fn filter_rules(def_rules: &[Rule], crnt_rules: &[usize], arg_idx: usize, num: &MatchNum) -> Vec<usize> {
    crnt_rules
      .iter()
      .copied()
      .filter(|&rule_idx| match (&def_rules[rule_idx].pats[arg_idx], num) {
        (Pattern::Num(Zero), Zero) => true,
        (Pattern::Num(Succ(..)), Succ(..)) => true,
        _ => false,
      })
      .collect()
  }

  let make_next_fn_name = |ctr_name: &MatchNum| Name(format!("{crnt_name}$P{ctr_name}"));

  let arms = [Zero, Succ(Some(Name::new("pred$")))];

  let arms = arms
    .into_iter()
    .map(|next_ctr| {
      let def = &book.defs[&def_id];
      let crnt_name = make_next_fn_name(&next_ctr);
      let crnt_rules = filter_rules(&def.rules, &crnt_rules, match_path.len(), &next_ctr);
      let new_vars = Pattern::Num(next_ctr.clone());
      let mut match_path = match_path.clone();
      match_path.push(new_vars);

      make_pattern_matching_case(book, def_type, def_id, &crnt_name, crnt_rules, match_path);

      let mut body = Term::Ref { def_id: book.def_names.def_id(&crnt_name).unwrap() };

      if let Succ(nam) = &next_ctr {
        body = Term::App {