bend/fun/check/
check_untyped.rs

1use crate::{
2  diagnostics::Diagnostics,
3  fun::{Ctx, FanKind, Pattern, Tag, Term},
4  maybe_grow,
5};
6
7impl Ctx<'_> {
8  /// Checks that terms that cannot be typed are only used inside untyped functions.
9  pub fn check_untyped_terms(&mut self) -> Result<(), Diagnostics> {
10    for def in self.book.defs.values() {
11      if def.check {
12        for rule in def.rules.iter() {
13          if let Err(e) = rule.body.check_untyped_terms() {
14            self.info.add_function_error(e, def.name.clone(), def.source.clone());
15          }
16        }
17      }
18    }
19    self.info.fatal(())
20  }
21}
22
23impl Term {
24  fn check_untyped_terms(&self) -> Result<(), String> {
25    maybe_grow(|| {
26      match self {
27        Term::Lam { tag: Tag::Static, pat, .. } => pat.check_untyped_patterns()?,
28        Term::Lam { tag: _, .. } => {
29          return Err("Tagged lambda in type-checked function".to_string());
30        }
31        Term::Link { nam } => {
32          return Err(format!("Unscoped variable '${nam}' in type-checked function"));
33        }
34        Term::App { tag: Tag::Static, .. } => {}
35        Term::App { tag: _, .. } => {
36          return Err("Tagged application in type-checked function".to_string());
37        }
38        Term::Fan { fan: FanKind::Dup, .. } => {
39          return Err("Superposition term in type-checked function".to_string());
40        }
41        Term::Fan { fan: FanKind::Tup, tag: Tag::Static, .. } => {}
42        Term::Fan { fan: FanKind::Tup, tag: _, .. } => {
43          return Err("Tagged tuple in type-checked function".to_string());
44        }
45        Term::Let { pat, .. } => {
46          pat.check_untyped_patterns()?;
47        }
48        _ => {}
49      }
50      for child in self.children() {
51        child.check_untyped_terms()?;
52      }
53      Ok(())
54    })
55  }
56}
57
58impl Pattern {
59  fn check_untyped_patterns(&self) -> Result<(), String> {
60    maybe_grow(|| {
61      match self {
62        Pattern::Chn(x) => {
63          return Err(format!("Unscoped variable bind '${x}' in type-checked function"));
64        }
65        Pattern::Fan(FanKind::Dup, Tag::Auto, _) => {}
66        Pattern::Fan(FanKind::Dup, _, _) => {
67          return Err("Tagged duplication in type-checked function".to_string());
68        }
69        Pattern::Fan(FanKind::Tup, Tag::Static, _) => {}
70        Pattern::Fan(FanKind::Tup, _, _) => {
71          return Err("Tagged tuple elimination in type-checked function".to_string());
72        }
73        _ => {}
74      }
75      for pat in self.children() {
76        pat.check_untyped_patterns()?;
77      }
78      Ok(())
79    })
80  }
81}
bend/fun/check/check_untyped.rs

bend/fun/check/
check_untyped.rs
