1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81

use crate::{
  fun::{Book, MatchRule, Name, Pattern, Tag, Term},
  maybe_grow,
};

impl Book {
  /// Encodes pattern matching expressions in the book into their
  /// native/core form. Must be run after [`Ctr::fix_match_terms`].
  ///
  /// 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_matches(&mut self) {
    for def in self.defs.values_mut() {
      for rule in &mut def.rules {
        rule.body.encode_matches();
      }
    }
  }
}

impl Term {
  pub fn encode_matches(&mut self) {
    maybe_grow(|| {
      for child in self.children_mut() {
        child.encode_matches()
      }

      if let Term::Mat { arg, bnd: _, with, arms: rules } = self {
        assert!(with.is_empty());
        let arg = std::mem::take(arg.as_mut());
        let rules = std::mem::take(rules);
        *self = encode_match(arg, rules);
      } else if let Term::Swt { arg, bnd: _, with, pred, arms: rules } = self {
        assert!(with.is_empty());
        let arg = std::mem::take(arg.as_mut());
        let pred = std::mem::take(pred);
        let rules = std::mem::take(rules);
        *self = encode_switch(arg, pred, rules);
      }
    })
  }
}

fn encode_match(arg: Term, rules: Vec<MatchRule>) -> Term {
  let tag = Tag::Static;
  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.clone(), Pattern::Var(nam), bod));
    arms.push(body);
  }
  Term::tagged_call(tag.clone(), arg, arms)
}

/// Convert into a sequence of native switches, decrementing by 1 each switch.
/// switch n {0: A; 1: B; _: (C n-2)} converted to
/// switch n {0: A; _: @%x match %x {0: B; _: @n-2 (C n-2)}}
fn encode_switch(arg: Term, pred: Option<Name>, mut rules: Vec<Term>) -> Term {
  // Create the cascade of switches
  let match_var = Name::new("%x");
  let (succ, nums) = rules.split_last_mut().unwrap();
  let last_arm = Term::lam(Pattern::Var(pred), std::mem::take(succ));
  nums.iter_mut().enumerate().rfold(last_arm, |term, (i, rule)| {
    let arms = vec![std::mem::take(rule), term];
    if i == 0 {
      Term::Swt { arg: Box::new(arg.clone()), bnd: None, with: vec![], pred: None, arms }
    } else {
      let swt = Term::Swt {
        arg: Box::new(Term::Var { nam: match_var.clone() }),
        bnd: None,
        with: vec![],
        pred: None,
        arms,
      };
      Term::lam(Pattern::Var(Some(match_var.clone())), swt)
    }
  })
}