decl_lang/
subsume.rs

1//! The subsumption judgment ⊑ (§3.17) — the runtime needs it for `match`
2//! arm selection over bound records and generic value-argument checks.
3use crate::ast::Expr;
4use crate::semantics::*;
5use num_traits::ToPrimitive;
6use std::collections::HashMap;
7use std::rc::Rc;
8
9pub fn subsumes(env: &Rc<Env>, a: &RT, b: &RT) -> bool {
10    let mut assume: HashMap<usize, Vec<usize>> = HashMap::new();
11    sub(env, a, b, &mut assume)
12}
13
14fn sub(env: &Rc<Env>, a: &RT, b: &RT, assume: &mut HashMap<usize, Vec<usize>>) -> bool {
15    if Rc::ptr_eq(a, b) {
16        return true;
17    }
18    let (ia, ib) = (Rc::as_ptr(a) as usize, Rc::as_ptr(b) as usize);
19    if is_rec(a) && is_rec(b) && assume.get(&ia).map(|s| s.contains(&ib)).unwrap_or(false) {
20        return true;
21    }
22    if let RTk::Union(arms) = &a.k {
23        return arms.iter().all(|x| sub(env, x, b, assume));
24    }
25    if let RTk::Union(arms) = &b.k {
26        return arms.iter().any(|x| sub(env, a, x, assume));
27    }
28    if let RTk::IsectN(arms) = &a.k {
29        return arms.iter().any(|x| sub(env, x, b, assume));
30    }
31    if let RTk::IsectN(arms) = &b.k {
32        return arms.iter().all(|x| sub(env, a, x, assume));
33    }
34    if let RTk::Pred {
35        base: bb,
36        preds: bp,
37    } = &b.k
38    {
39        return match &a.k {
40            RTk::Pred {
41                base: ab,
42                preds: ap,
43            } => sub(env, ab, bb, assume) && bp.iter().all(|p| ap.iter().any(|q| pred_eq(p, q))),
44            RTk::Lit(v) => lit_satisfies(env, v, bb, bp),
45            _ => false,
46        };
47    }
48    if let RTk::Pred { base, .. } = &a.k {
49        return sub(env, base, b, assume);
50    }
51    match &b.k {
52        RTk::Prim(bn) => match &a.k {
53            RTk::Prim(an) => an == bn,
54            RTk::Lit(v) => lit_kind(v) == bn,
55            RTk::Range { base, .. } => base == bn,
56            RTk::Pattern { .. } => bn == "string",
57            _ => false,
58        },
59        RTk::Lit(bv) => matches!(&a.k, RTk::Lit(av) if lit_eq(av, bv)),
60        RTk::Range { lo, hi, excl, base } => match &a.k {
61            RTk::Lit(v) => lit_kind(v) == base && in_range(v, lo, hi, *excl),
62            RTk::Range {
63                lo: alo,
64                hi: ahi,
65                excl: aexcl,
66                base: abase,
67            } => {
68                if abase != base {
69                    return false;
70                }
71                let a_hi = if *aexcl { dec(ahi) } else { ahi.clone() };
72                let b_hi = if *excl { dec(hi) } else { hi.clone() };
73                num_ge(alo, lo) && num_le(&a_hi, &b_hi)
74            }
75            _ => false,
76        },
77        RTk::Pattern { src, re } => match &a.k {
78            RTk::Lit(Value::Str(s)) => re.is_match(s),
79            RTk::Pattern { src: asrc, .. } => asrc == src,
80            _ => false,
81        },
82        RTk::Arr { elem, lo, hi } => match &a.k {
83            RTk::Arr {
84                elem: ae,
85                lo: alo,
86                hi: ahi,
87            } => {
88                sub(env, ae, elem, assume)
89                    && alo.unwrap_or(0) >= lo.unwrap_or(0)
90                    && ahi.unwrap_or(i64::MAX) <= hi.unwrap_or(i64::MAX)
91            }
92            _ => false,
93        },
94        RTk::Map { key, val } => match &a.k {
95            RTk::Map { key: ak, val: av } => sub(env, ak, key, assume) && sub(env, av, val, assume),
96            _ => false,
97        },
98        RTk::Quantity(d) => matches!(&a.k, RTk::Quantity(ad) if ad == d),
99        RTk::Ref(t) => matches!(&a.k, RTk::Ref(at) if sub(env, at, t, assume)),
100        RTk::Func { params, ret } => match &a.k {
101            RTk::Func {
102                params: ap,
103                ret: ar,
104            } => {
105                ap.len() == params.len()
106                    && params
107                        .iter()
108                        .zip(ap)
109                        .all(|(bp, ap)| sub(env, bp, ap, assume))
110                    && sub(env, ar, ret, assume)
111            }
112            _ => false,
113        },
114        RTk::Rec(br) => {
115            let RTk::Rec(ar) = &a.k else { return false };
116            assume.entry(ia).or_default().push(ib);
117            let bm = br.members.borrow().clone();
118            let am = ar.members.borrow().clone();
119            for m in &bm {
120                if m.hidden {
121                    continue; // not part of the value: ⊑ never compares it (D34)
122                }
123                let sm = am.iter().find(|x| x.name == m.name);
124                let m_types: Vec<RT> = m
125                    .conj
126                    .clone()
127                    .unwrap_or_else(|| m.ty.iter().cloned().collect());
128                let s_types: Vec<RT> = sm
129                    .map(|s| {
130                        s.conj
131                            .clone()
132                            .unwrap_or_else(|| s.ty.iter().cloned().collect())
133                    })
134                    .unwrap_or_default();
135                let mut type_ok = || {
136                    m_types.is_empty()
137                        || s_types.is_empty()
138                        || m_types
139                            .iter()
140                            .all(|mt| s_types.iter().any(|st| sub(env, st, mt, assume)))
141                };
142                let ok = match m.kind {
143                    MKind::Req => sm.map(|s| s.kind != MKind::Opt).unwrap_or(false) && type_ok(),
144                    MKind::Opt | MKind::Dflt => sm.is_none() || type_ok(),
145                    MKind::Der => sm.is_some() && type_ok(),
146                };
147                if !ok {
148                    if let Some(v) = assume.get_mut(&ia) {
149                        v.retain(|x| *x != ib);
150                    }
151                    return false;
152                }
153            }
154            true
155        }
156        RTk::Any => true,
157        _ => false,
158    }
159}
160
161fn lit_kind(v: &Value) -> &'static str {
162    match v {
163        Value::Int(_) => "int",
164        Value::Float(_) => "float",
165        Value::Str(_) => "string",
166        Value::Bool(_) => "bool",
167        Value::Null => "null",
168        _ => "unknown",
169    }
170}
171fn lit_eq(a: &Value, b: &Value) -> bool {
172    match (a, b) {
173        (Value::Int(x), Value::Int(y)) => x == y,
174        (Value::Float(x), Value::Float(y)) => x == y,
175        (Value::Str(x), Value::Str(y)) => x == y,
176        (Value::Bool(x), Value::Bool(y)) => x == y,
177        (Value::Null, Value::Null) => true,
178        _ => false,
179    }
180}
181fn dec(v: &Value) -> Value {
182    match v {
183        Value::Int(i) => Value::Int(i - 1),
184        Value::Float(f) => Value::Float(f - 1.0),
185        other => other.clone(),
186    }
187}
188fn num_ge(a: &Value, b: &Value) -> bool {
189    match (a, b) {
190        (Value::Int(x), Value::Int(y)) => x >= y,
191        (Value::Float(x), Value::Float(y)) => x >= y,
192        (Value::Int(x), Value::Float(y)) => x.to_f64().map(|f| f >= *y).unwrap_or(false),
193        (Value::Float(x), Value::Int(y)) => y.to_f64().map(|f| *x >= f).unwrap_or(false),
194        _ => false,
195    }
196}
197fn num_le(a: &Value, b: &Value) -> bool {
198    num_ge(b, a)
199}
200fn in_range(v: &Value, lo: &Value, hi: &Value, excl: bool) -> bool {
201    let h = if excl { dec(hi) } else { hi.clone() };
202    num_ge(v, lo) && num_le(v, &h)
203}
204fn pred_eq(a: &Rc<Expr>, b: &Rc<Expr>) -> bool {
205    match (&**a, &**b) {
206        (Expr::Name(x), Expr::Name(y)) => x == y,
207        (Expr::Call { fun: fa, args: aa }, Expr::Call { fun: fb, args: ab }) => {
208            pred_eq(fa, fb)
209                && aa.len() == ab.len()
210                && aa.iter().zip(ab).all(
211                    |(x, y)| matches!((&**x, &**y), (Expr::Lit(p), Expr::Lit(q)) if lit_eq(p, q)),
212                )
213        }
214        _ => false,
215    }
216}
217fn lit_satisfies(env: &Rc<Env>, v: &Value, base: &RT, preds: &[Rc<Expr>]) -> bool {
218    let eng = crate::engine::Engine::bare(env.clone());
219    let sc = Scope::new("", None);
220    if !subsumes(env, &ty(RTk::Lit(v.clone())), base) {
221        return false;
222    }
223    for p in preds {
224        let ok = eng
225            .ev(p, &sc)
226            .and_then(|f| eng.call(&f, vec![v.clone()], &sc));
227        if !matches!(ok, Ok(Value::Bool(true))) {
228            return false;
229        }
230    }
231    true
232}
233
234// ---------------- structural emptiness (§3.17; the checker's E4011/E4012) ----------------
235/// JavaScript `>`: strings compare lexically, a string against a number is NaN (false)
236fn js_gt(a: &Value, b: &Value) -> bool {
237    match (a, b) {
238        (Value::Str(x), Value::Str(y)) => x > y,
239        (Value::Str(_), _) | (_, Value::Str(_)) => false,
240        _ => num_ge(a, b) && !value_eq(a, b),
241    }
242}
243
244pub fn structurally_empty(env: &Rc<Env>, t: &RT) -> bool {
245    match &t.k {
246        RTk::Range { lo, hi, excl, .. } => {
247            let h = if *excl && !matches!(hi, Value::Str(_)) {
248                dec(hi)
249            } else {
250                hi.clone()
251            };
252            js_gt(lo, &h)
253        }
254        RTk::Arr { lo, hi, .. } => matches!((lo, hi), (Some(l), Some(h)) if l > h),
255        RTk::IsectN(arms) => {
256            for i in 0..arms.len() {
257                for j in i + 1..arms.len() {
258                    if disjoint(env, &arms[i], &arms[j]) {
259                        return true;
260                    }
261                }
262            }
263            arms.iter().any(|a| structurally_empty(env, a))
264        }
265        RTk::Union(arms) => arms.iter().all(|a| structurally_empty(env, a)),
266        _ => false,
267    }
268}
269
270fn kind_of(t: &RT) -> Option<String> {
271    Some(match &t.k {
272        RTk::Prim(n) => n.clone(),
273        RTk::Lit(v) => lit_kind(v).to_string(),
274        RTk::Range { base, .. } => base.clone(),
275        RTk::Pattern { .. } => "string".into(),
276        RTk::Arr { .. } => "array".into(),
277        RTk::Rec(_) | RTk::Map { .. } | RTk::Quantity(_) => "object".into(),
278        _ => return None,
279    })
280}
281
282fn disjoint(env: &Rc<Env>, a: &RT, b: &RT) -> bool {
283    let (ka, kb) = (kind_of(a), kind_of(b));
284    if let (Some(x), Some(y)) = (&ka, &kb) {
285        if x != y {
286            return true;
287        }
288    }
289    match (&a.k, &b.k) {
290        (
291            RTk::Range {
292                lo: alo,
293                hi: ahi,
294                excl: aexcl,
295                base: abase,
296            },
297            RTk::Range {
298                lo: blo,
299                hi: bhi,
300                excl: bexcl,
301                base: bbase,
302            },
303        ) if abase == bbase => {
304            let a_hi = if *aexcl { dec(ahi) } else { ahi.clone() };
305            let b_hi = if *bexcl { dec(bhi) } else { bhi.clone() };
306            js_gt(alo, &b_hi) || js_gt(blo, &a_hi)
307        }
308        (RTk::Lit(x), RTk::Lit(y)) => !lit_eq(x, y),
309        (RTk::Lit(v), RTk::Range { lo, hi, excl, base }) => {
310            !(lit_kind(v) == base && in_range(v, lo, hi, *excl))
311        }
312        (RTk::Range { .. }, RTk::Lit(_)) => disjoint(env, b, a),
313        _ => false,
314    }
315}
decl_lang/subsume.rs

decl_lang/
subsume.rs
