selection: normal: implement absorbtion (#389)

Summary:
Pull Request resolved: #389

ghstack-source-id: 293656201

implement the absorbtion normalization rules

Reviewed By: mariusae

Differential Revision: D77597600

fbshipit-source-id: 5e20504f18017f9fdbd02a0dd2ff8d66593c28e8

Author: shayne-fletcher

ndslice/src/selection/mod.rs

@@ -359,7 +359,9 @@ pub fn structurally_equal(a: &Selection, b: &Selection) -> bool {
 /// structure. It is designed to improve over time as additional
 /// rewrites (e.g., flattening, simplification) are introduced.
 pub fn normalize(sel: &Selection) -> NormalizedSelection {
-    let rule = normal::FlatteningRules.then(normal::IdentityRules);
+    let rule = normal::FlatteningRules
+        .then(normal::IdentityRules)
+        .then(normal::AbsorbtionRules);
     sel.fold::<normal::NormalizedSelection>()
         .rewrite_bottom_up(&rule)
 }

ndslice/src/selection/normal.rs

@@ -272,6 +272,42 @@ impl RewriteRule for FlatteningRules {
     }
 }
 
+/// A normalization rule that applies absorption laws for unions and
+/// intersections.
+///
+/// A union containing `True` always evaluates to `True`, and an
+/// intersection containing `False` always evaluates to `False`.
+#[derive(Default)]
+pub struct AbsorbtionRules;
+
+impl RewriteRule for AbsorbtionRules {
+    // Absorption rewrites:
+    //
+    // - Union(..., True, ...) → True
+    // - Intersection(..., False, ...) → False
+    fn rewrite(&self, node: NormalizedSelection) -> NormalizedSelection {
+        use NormalizedSelection::*;
+
+        match node {
+            Union(set) => {
+                if set.contains(&True) {
+                    True // Union(..., True, ...) → True
+                } else {
+                    Union(set)
+                }
+            }
+            Intersection(set) => {
+                if set.contains(&False) {
+                    False // Intersection(..., False, ...) → False
+                } else {
+                    Intersection(set)
+                }
+            }
+            other => other,
+        }
+    }
+}
+
 impl NormalizedSelection {
     pub fn rewrite_bottom_up(self, rule: &impl RewriteRule) -> Self {
         let mapped = self.trav(|child| child.rewrite_bottom_up(rule));
@@ -396,3 +432,31 @@ mod tests {
         }
     }
 }
+
+#[test]
+fn test_absorbtion_rules() {
+    use NormalizedSelection::*;
+
+    // Union(True, Any(True)) should absorb to True
+    let union_case = {
+        let mut set = BTreeSet::new();
+        set.insert(True);
+        set.insert(Any(Box::new(True)));
+        Union(set)
+    };
+
+    let rule = AbsorbtionRules;
+    let result = rule.rewrite(union_case);
+    assert_eq!(result, True);
+
+    // Intersection(False, All(True)) should absorb to False
+    let intersection_case = {
+        let mut set = BTreeSet::new();
+        set.insert(False);
+        set.insert(All(Box::new(True)));
+        Intersection(set)
+    };
+
+    let result = rule.rewrite(intersection_case);
+    assert_eq!(result, False);
+}