bynk_check/
narrowing.rs

1//! Which `is` tests an expression proves. #1654 (runtime-semantics track S5,
2//! Decision A): the one structural rule the resolver, the checker and the
3//! emitter all read, so their views of an `is` binding's scope cannot drift.
4//!
5//! An `e is P` test with bindings brings those bindings into scope wherever the
6//! test is **known to have matched**. Given a Boolean expression and whether it
7//! evaluated to `true` or `false`, [`matched_is_tests`] returns the `is` tests
8//! that must then have matched:
9//!
10//! | expression    | when true                     | when false                    |
11//! |---------------|-------------------------------|-------------------------------|
12//! | `e is P`      | the test                      | —                             |
13//! | `a && b`      | `a` when true, `b` when true  | — (either may have failed)    |
14//! | `a \|\| b`    | — (either may have held)      | `a` when false, `b` when false |
15//! | `!e`          | `e` when false                | `e` when true                 |
16//! | `a implies b` | — (`!a \|\| b`)               | `a` when true, `b` when false |
17//! | `(e)`         | `e`                           | `e`                           |
18//!
19//! The consumers apply it at these scopes:
20//! - an `if`'s then-branch: its condition when true;
21//! - an `if`'s else-branch: its condition when false (`if !(o is Some(v))
22//!   { … } else { v }`, type-system §2.3.6);
23//! - the right operand of `&&` and `implies`: the left operand when true, since
24//!   the right is evaluated only then.
25//!
26//! The right operand of `||` (the left operand when false) is not scoped in
27//! this slice: nothing lowers it with bindings yet, and a scope the checker
28//! accepts must be one the emitter lowers.
29
30use bynk_syntax::ast::{BinOp, Expr, ExprKind, UnaryOp};
31
32/// The `is` tests (`ExprKind::Is` nodes) that `expr` proves matched when it
33/// evaluates to `when_true`, in source order.
34pub fn matched_is_tests(expr: &Expr, when_true: bool) -> Vec<&Expr> {
35    let mut out = Vec::new();
36    collect(expr, when_true, &mut out);
37    out
38}
39
40fn collect<'e>(expr: &'e Expr, when_true: bool, out: &mut Vec<&'e Expr>) {
41    match (&expr.kind, when_true) {
42        (ExprKind::Is { .. }, true) => out.push(expr),
43        (ExprKind::Paren(inner), _) => collect(inner, when_true, out),
44        (ExprKind::UnaryOp(UnaryOp::Not, inner), _) => collect(inner, !when_true, out),
45        (ExprKind::BinOp(BinOp::And, a, b), true) | (ExprKind::BinOp(BinOp::Or, a, b), false) => {
46            collect(a, when_true, out);
47            collect(b, when_true, out);
48        }
49        (ExprKind::BinOp(BinOp::Implies, a, b), false) => {
50            collect(a, true, out);
51            collect(b, false, out);
52        }
53        _ => {}
54    }
55}
56
57#[cfg(test)]
58mod tests {
59    use super::matched_is_tests;
60    use bynk_syntax::{lexer, parser};
61
62    /// The `is` tests' receiver names `cond` proves when `when_true`.
63    fn proved(cond: &str, when_true: bool) -> Vec<String> {
64        let src = format!(
65            "commons m\n\nfn f(a: Option[Int], b: Option[Int], c: Bool) -> Bool {{ {cond} }}\n"
66        );
67        let tokens = lexer::tokenize(&src).expect("lex");
68        let unit = parser::parse_unit(&tokens, &src).expect("parse");
69        let bynk_syntax::ast::SourceUnit::Commons(commons) = unit else {
70            panic!("commons")
71        };
72        let bynk_syntax::ast::CommonsItem::Fn(f) = &commons.items[0] else {
73            panic!("fn")
74        };
75        matched_is_tests(&f.body.tail, when_true)
76            .into_iter()
77            .map(|e| match &e.kind {
78                bynk_syntax::ast::ExprKind::Is { value, .. } => match &value.kind {
79                    bynk_syntax::ast::ExprKind::Ident(id) => id.name.clone(),
80                    _ => "?".to_string(),
81                },
82                _ => unreachable!(),
83            })
84            .collect()
85    }
86
87    #[test]
88    fn a_test_proves_itself_only_when_true() {
89        assert_eq!(proved("a is Some(x)", true), ["a"]);
90        assert!(proved("a is Some(x)", false).is_empty());
91        assert_eq!(proved("(a is Some(x))", true), ["a"]);
92    }
93
94    #[test]
95    fn and_proves_both_when_true_and_nothing_when_false() {
96        assert_eq!(proved("a is Some(x) && b is Some(y)", true), ["a", "b"]);
97        assert!(proved("a is Some(x) && b is Some(y)", false).is_empty());
98    }
99
100    #[test]
101    fn or_proves_nothing_when_true_and_both_negations_when_false() {
102        assert!(proved("a is Some(x) || b is Some(y)", true).is_empty());
103        assert_eq!(
104            proved("!(a is Some(x)) || !(b is Some(y))", false),
105            ["a", "b"]
106        );
107    }
108
109    #[test]
110    fn not_flips_the_polarity() {
111        assert!(proved("!(a is Some(x))", true).is_empty());
112        assert_eq!(proved("!(a is Some(x))", false), ["a"]);
113        assert_eq!(proved("!!(a is Some(x))", true), ["a"]);
114        // `!(a && b)` false means `a && b` true.
115        assert_eq!(proved("!(a is Some(x) && b is Some(y))", false), ["a", "b"]);
116        // `!(a && b)` true proves nothing.
117        assert!(proved("!(a is Some(x) && b is Some(y))", true).is_empty());
118    }
119
120    #[test]
121    fn implies_proves_its_antecedent_and_negated_consequent_when_false() {
122        assert!(proved("a is Some(x) implies c", true).is_empty());
123        assert_eq!(
124            proved("a is Some(x) implies !(b is Some(y))", false),
125            ["a", "b"]
126        );
127    }
128}
bynk_check/narrowing.rs

bynk_check/
narrowing.rs
