From f948eecaaa34f6c1846881c95caabfaa8aa1381f Mon Sep 17 00:00:00 2001
From: Spencer Killen <sjkillen@ualberta.ca>
Date: Thu, 21 Dec 2023 23:13:11 -0700
Subject: [PATCH] a

---
 src/main.rs | 117 +++++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 101 insertions(+), 16 deletions(-)

diff --git a/src/main.rs b/src/main.rs
index 3589ed4..0c69fbc 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -74,8 +74,8 @@ impl Display for Lattice<Atom, ()> {
 
 impl<I: Incrementable + Default, Ext> Incrementable for Lattice<I, Ext> {
     fn increment(&mut self) -> IncrementResult {
-        for atom in &mut self.order {
-            if let Good = atom.increment() {
+        for element in &mut self.order {
+            if let Good = element.increment() {
                 return Good;
             }
         }
@@ -88,15 +88,16 @@ where
     Self: LatticeAbstract,
 {
     fn next_lattice(&mut self) -> IncrementResult {
-        self.increment();
-        while !self.is_lattice() {
+        loop {
             if let Overflow = self.increment() {
                 if let Overflow = self.grow() {
                     return Overflow;
                 }
             }
+            if self.is_lattice() {
+                return Good;
+            }
         }
-        return Good;
     }
     fn ge(&self, a: usize, b: usize) -> bool {
         return self.le(b, a);
@@ -140,7 +141,7 @@ where
         }
         return true;
     }
-    fn monotone<IncB, ExtB>(&self, other: &Lattice<IncB, ExtB>) -> bool
+    fn order_preserving<IncB, ExtB>(&self, other: &Lattice<IncB, ExtB>) -> bool
     where
         IncB: Incrementable + Default,
         Lattice<IncB, ExtB>: LatticeAbstract,
@@ -158,7 +159,7 @@ where
         IncB: Incrementable + Default,
         Lattice<IncB, ExtB>: LatticeAbstract,
     {
-        self.monotone(other) && other.monotone(self)
+        self.order_preserving(other) && other.order_preserving(self)
     }
 }
 
@@ -299,15 +300,24 @@ impl<'a> Operator<'a> {
     fn new(domain: &'a Lattice<Atom, ()>, image: &'a Lattice<Atom, ()>) -> Operator<'a> {
         Lattice {
             ext: Mapping { domain, image },
-            order: vec![AtomSet { included: vec![] }; image.order.len()],
+            order: vec![
+                AtomSet {
+                    included: vec![false; domain.order.len()]
+                };
+                image.order.len()
+            ],
         }
     }
     fn all_nonempty(&self) -> bool {
         self.order.iter().all(|set| set.included.iter().any(|&x| x))
     }
-    fn le_helper<I: Iterator<Item = usize> + Clone>(&self, a: I, b: I) -> bool {
+    fn le_helper<I, F>(&self, a: I, b: I, rel: F) -> bool
+    where
+        I: Iterator<Item = usize> + Clone,
+        F: Fn(&Lattice<Atom, ()>, usize, usize) -> bool,
+    {
         b.clone()
-            .all(|right| a.clone().any(|left| self.ext.domain.le(left, right)))
+            .all(|right| a.clone().any(|left| rel(&self.ext.domain, left, right)))
     }
 }
 
@@ -323,10 +333,10 @@ impl<'a> LatticeAbstract for Operator<'a> {
         let left = pick(a);
         let right = pick(b);
 
-        if !self.le_helper(left.clone(), right.clone()) {
+        if !self.le_helper(left.clone(), right.clone(), Lattice::<Atom, ()>::le) {
             return false;
         }
-        if !self.le_helper(right, left) {
+        if !self.le_helper(right, left, Lattice::<Atom, ()>::ge) {
             return false;
         }
         return true;
@@ -362,6 +372,78 @@ mod operator_tests {
 
     #[test]
     fn test_operator() {
+        let domain = &Lattice {
+            ext: (),
+            order: vec![
+                Atom { smaller: vec![] },
+                Atom {
+                    smaller: vec![true],
+                },
+                Atom {
+                    smaller: vec![true, false],
+                },
+            ],
+        };
+        let image = &Lattice {
+            ext: (),
+            order: vec![
+                Atom { smaller: vec![] },
+                Atom {
+                    smaller: vec![true],
+                },
+                Atom {
+                    smaller: vec![true, false],
+                },
+            ],
+        };
+        assert!(domain.is_lattice());
+        assert!(image.is_lattice());
+        assert!(image.equal(domain));
+        // Identity operator
+        let operator = Lattice {
+            ext: Mapping { domain, image },
+            order: vec![
+                AtomSet {
+                    included: vec![true, false, false],
+                },
+                AtomSet {
+                    included: vec![false, true, false],
+                },
+                AtomSet {
+                    included: vec![false, false, true],
+                },
+            ],
+        };
+        assert!(operator.is_lattice());
+    }
+
+    #[test]
+    fn test_order_preserving() {
+        let lattice_a = Lattice {
+            ext: (),
+            order: vec![
+                Atom { smaller: vec![] },
+                Atom {
+                    smaller: vec![true],
+                },
+                Atom {
+                    smaller: vec![true, false],
+                },
+            ],
+        };
+        let lattice_b = Lattice {
+            ext: (),
+            order: vec![
+                Atom { smaller: vec![] },
+                Atom {
+                    smaller: vec![true],
+                },
+                Atom {
+                    smaller: vec![true, false],
+                },
+            ],
+        };
+        assert!(lattice_a.order_preserving(&lattice_b));
     }
 }
 
@@ -379,12 +461,15 @@ fn main() {
             },
         ],
     };
-    loop {
-        domain.next_lattice();
+    while let Good = domain.next_lattice() {
+        if domain.order.len() != image.order.len() || !domain.order_preserving(&image) {
+            continue;
+        }
         println!("{}", domain);
         let mut operator = Operator::new(&domain, &image);
-        while let Good = operator.next_lattice() {
-            println!("{}", operator);
+        while let Good = operator.increment() {
+            // println!("ah: {}", operator);
+            // TODO doesn't work because we generate a domain larger than the image lol
         }
     }
 }