omnist/ops/
subschema.rs

1//! Subschema compatibility and equivalence. Ported from
2//! `~/dev/omnist/omnist/ops/subschema.py`.
3//!
4//! Implements the paper's Algorithm 4 (SubschemaSA) restricted to omnist's
5//! counting cardinality languages; [`equivalent`] is bidirectional
6//! inclusion.
7//!
8//! Algorithm 4 assumes its precondition MakeUsefulSA (useless-state removal,
9//! `super::prune`) has already run: the coinductive cycle rule below only
10//! coincides with true (finite-document) language inclusion once every
11//! A-side record is known satisfiable. Rather than requiring callers to
12//! pre-prune, [`compatible_with`] computes `a`'s satisfiable set once up
13//! front and consults it directly -- an unsatisfiable A-side record is
14//! vacuously a subschema of anything (it emits no documents at all), and an
15//! optional A-field whose type is unsatisfiable is skipped (it can never
16//! actually be emitted, so it imposes no obligation on B).
17
18use indexmap::{IndexMap, IndexSet};
19
20use crate::schema::{FieldType, Record, Scalar, ScalarKind, Schema};
21
22use super::prune::satisfiable_set;
23
24/// True if every document `a` accepts is also accepted by `b` (`a` is a
25/// subschema / `b` is backward-compatible).
26pub fn compatible_with(a: &Schema, b: &Schema) -> bool {
27    let sat_a = satisfiable_set(a);
28    let mut memo: IndexMap<(String, String), bool> = IndexMap::new();
29    sub(
30        a,
31        &FieldType::Ref(a.root().clone()),
32        b,
33        &FieldType::Ref(b.root().clone()),
34        &sat_a,
35        &mut memo,
36    )
37}
38
39/// True if both schemas accept exactly the same documents.
40pub fn equivalent(a: &Schema, b: &Schema) -> bool {
41    compatible_with(a, b) && compatible_with(b, a)
42}
43
44/// The memo key is `(a-ref-name, b-ref-name)`, guarding only the ref/ref
45/// case -- the only one that can cycle. Scalar comparisons never recurse,
46/// so they need no memoization to terminate.
47fn sub(
48    sa: &Schema,
49    ta: &FieldType,
50    sb: &Schema,
51    tb: &FieldType,
52    sat_a: &IndexSet<String>,
53    memo: &mut IndexMap<(String, String), bool>,
54) -> bool {
55    match (ta, tb) {
56        (FieldType::Ref(ra), _) if !sat_a.contains(&ra.name) => true,
57        // `any` on the B (super-schema) side absorbs every A-side value --
58        // always sound, regardless of what `ta` is. Checked before the
59        // `ta == Any` arm below, mirroring Python's `if isinstance(db,
60        // AnyType): True` running before its `elif isinstance(da, AnyType)`.
61        (_, FieldType::Any) => true,
62        // Only `any` holds `any`; `ta` is `any` and `tb` isn't -> never a
63        // subschema relation.
64        (FieldType::Any, _) => false,
65        (FieldType::Scalar(a), FieldType::Scalar(b)) => scalar_sub(*a, *b),
66        (FieldType::Ref(ra), FieldType::Ref(rb)) => {
67            let key = (ra.name.clone(), rb.name.clone());
68            if let Some(&v) = memo.get(&key) {
69                return v;
70            }
71            // Coinductive assumption while descending, mirroring the Python
72            // reference: a cycle that never disagrees is compatible.
73            memo.insert(key.clone(), true);
74            let reca = sa
75                .env()
76                .get(&ra.name)
77                .expect("Schema's own invariant: every Ref resolves within its env");
78            let recb = sb
79                .env()
80                .get(&rb.name)
81                .expect("Schema's own invariant: every Ref resolves within its env");
82            let result = record_sub(sa, reca, sb, recb, sat_a, memo);
83            memo.insert(key, result);
84            result
85        }
86        // A value type vs. an object type (or vice versa) is never
87        // compatible.
88        _ => false,
89    }
90}
91
92fn record_sub(
93    sa: &Schema,
94    a: &Record,
95    sb: &Schema,
96    b: &Record,
97    sat_a: &IndexSet<String>,
98    memo: &mut IndexMap<(String, String), bool>,
99) -> bool {
100    // Every label A may emit must be allowed by B, with a cardinality range
101    // B's covers and a type B accepts.
102    for fa in a.fields() {
103        if fa.max == Some(0) {
104            continue; // A never emits this label
105        }
106        if fa.min == 0
107            && let FieldType::Ref(r) = &fa.ty
108            && !sat_a.contains(&r.name)
109        {
110            continue; // A never actually emits this label either
111        }
112        let Some(fb) = b.field(&fa.label) else {
113            return false; // B is closed and has no such field
114        };
115        if !(fb.min <= fa.min && le(fa.max, fb.max)) {
116            return false; // [fa.min,fa.max] not a subset of B's range
117        }
118        if !sub(sa, &fa.ty, sb, &fb.ty, sat_a, memo) {
119            return false;
120        }
121    }
122    // Every label B *requires* must be guaranteed by A.
123    for fb in b.fields() {
124        if fb.min >= 1 {
125            match a.field(&fb.label) {
126                None => return false,
127                Some(fa) if fa.min < fb.min => return false,
128                _ => {}
129            }
130        }
131    }
132    true
133}
134
135/// `x <= y`, treating `None` as `+infinity` (unbounded max).
136fn le(x: Option<usize>, y: Option<usize>) -> bool {
137    match y {
138        None => true,
139        Some(y) => match x {
140            None => false,
141            Some(x) => x <= y,
142        },
143    }
144}
145
146fn scalar_sub(a: Scalar, b: Scalar) -> bool {
147    if a.is_nullable() && !b.is_nullable() {
148        return false;
149    }
150    if a.kind() == b.kind() {
151        return true;
152    }
153    a.kind() == ScalarKind::Integer && b.kind() == ScalarKind::Number
154}
omnist/ops/subschema.rs

omnist/ops/
subschema.rs
