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

use crate::{
  fun::{Book, Definition, Name, Num, Pattern, Rule, Term},
  AdtEncoding,
};

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![];
    let mut tags = vec![];

    for (adt_name, adt) in self.adts.iter() {
      for (ctr_idx, (ctr_name, fields)) in adt.ctrs.iter().enumerate() {
        let ctrs: Vec<_> = adt.ctrs.keys().cloned().collect();

        let body = match adt_encoding {
          AdtEncoding::Scott => encode_ctr_scott(fields.iter().map(|f| &f.nam), ctrs, ctr_name),
          AdtEncoding::NumScott => {
            let tag = make_tag(adt_name == ctr_name, ctr_name);
            let body = encode_ctr_num_scott(fields.iter().map(|f| &f.nam), &tag);
            let tag_def = make_tag_def(ctr_idx, &tag, adt);
            tags.push((tag, tag_def));
            body
          }
        };

        let rules = vec![Rule { pats: vec![], body }];
        let def = Definition { name: ctr_name.clone(), rules, builtin: adt.builtin };
        defs.push((ctr_name.clone(), def));
      }
    }
    self.defs.extend(defs);
    self.defs.extend(tags);
  }
}

fn make_tag(is_object: bool, ctr_name: &Name) -> Name {
  if is_object {
    Name::new(format!("{ctr_name}/tag"))
  } else {
    let (typ, ctr) = ctr_name.rsplit_once('/').expect("To split at '/'");
    Name::new(format!("{typ}/{ctr}/tag"))
  }
}

fn encode_ctr_scott<'a>(
  ctr_args: impl DoubleEndedIterator<Item = &'a Name> + Clone,
  ctrs: Vec<Name>,
  ctr_name: &Name,
) -> Term {
  let ctr = Term::Var { nam: ctr_name.clone() };
  let app = Term::call(ctr, ctr_args.clone().cloned().map(|nam| Term::Var { nam }));
  let lam = Term::rfold_lams(app, ctrs.into_iter().map(Some));
  Term::rfold_lams(lam, ctr_args.cloned().map(Some))
}

fn encode_ctr_num_scott<'a>(ctr_args: impl DoubleEndedIterator<Item = &'a Name> + Clone, tag: &str) -> Term {
  let nam = Name::new("%x");
  // λa1 .. λan λx (x TAG a1 .. an)
  let term = Term::Var { nam: nam.clone() };
  let tag = Term::r#ref(tag);
  let term = Term::app(term, tag);
  let term = Term::call(term, ctr_args.clone().cloned().map(|nam| Term::Var { nam }));
  let term = Term::lam(Pattern::Var(Some(nam)), term);
  Term::rfold_lams(term, ctr_args.cloned().map(Some))
}

fn make_tag_def(ctr_idx: usize, tag: &Name, adt: &crate::fun::Adt) -> Definition {
  let tag_rule = vec![Rule { pats: vec![], body: Term::Num { val: Num::U24(ctr_idx as u32) } }];
  Definition { name: tag.clone(), rules: tag_rule, builtin: adt.builtin }
}