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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112

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

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, adt_encoding: AdtEncoding) {
    for def in self.defs.values_mut() {
      for rule in &mut def.rules {
        rule.body.encode_matches(adt_encoding);
      }
    }
  }
}

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

      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, adt_encoding);
      } 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>, adt_encoding: AdtEncoding) -> Term {
  match adt_encoding {
    AdtEncoding::Scott => {
      let arms = rules.into_iter().map(|rule| Term::rfold_lams(rule.2, rule.1.into_iter()));
      Term::call(arg, arms)
    }
    AdtEncoding::NumScott => {
      fn make_switches(arms: &mut [Term]) -> Term {
        maybe_grow(|| match arms {
          [] => Term::Err,
          [arm] => Term::lam(Pattern::Var(None), std::mem::take(arm)),
          [arm, rest @ ..] => Term::lam(Pattern::Var(Some(Name::new("%tag"))), Term::Swt {
            arg: Box::new(Term::Var { nam: Name::new("%tag") }),
            bnd: None,
            with: vec![],
            pred: None,
            arms: vec![std::mem::take(arm), make_switches(rest)],
          }),
        })
      }
      let mut arms =
        rules.into_iter().map(|rule| Term::rfold_lams(rule.2, rule.1.into_iter())).collect::<Vec<_>>();
      let term = if arms.len() == 1 {
        // λx (x λtag switch tag {0: Ctr0; _: * })
        let arm = arms.pop().unwrap();
        let term = Term::Swt {
          arg: Box::new(Term::Var { nam: Name::new("%tag") }),
          bnd: None,
          with: vec![],
          pred: None,
          arms: vec![arm, Term::Era],
        };
        Term::lam(Pattern::Var(Some(Name::new("%tag"))), term)
      } else {
        // λx (x λtag switch tag {0: Ctr0; _: switch tag-1 { ... } })
        make_switches(arms.as_mut_slice())
      };
      Term::call(arg, [term])
    }
  }
}

/// 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)
    }
  })
}