content: module Data.Abstract.Widening where
  
  import Data.Abstract.Stable
  import Data.Order
  
  -- | ▽ has to be an upper bound operator, i.e. x ⊑ x ▽ y and y ⊑ x ▽ y.
  -- Furthermore, iterating ▽ on an ascending chain has to stabilize:
  -- Let x1, x2, ... xn be an infinite ascending chain, then x1, x1 ▽
  -- x2, (x1 ▽ x2) ▽ x3, ... (similar to left fold) has a limit:
  --
  --            ... finite
  --          ▽
  --        /   \
  --       ▽     \
  --     /   \    \
  --    ▽     \    \
  --  /   \    \    \
  -- x1 ⊑ x2 ⊑ x3 ⊑ x4 ⊑ ... infinite
  --
  -- Furthermore, we allow our widening operators to maintain some state
  -- between each iteration.
  type Widening a = a -> a -> (Stable,a)
  
  -- | For a preorder with no infinite ascending chains, (⊔) is a
  -- trivial widening operator.
  finite :: Complete a => Widening a
  finite a b = let x = a ⊔ b in (if x ⊑ a then Stable else Unstable,x)
  {-# INLINE finite #-}
  
  toJoin :: Widening a -> (a -> a -> a)
  toJoin w a b = snd (w a b)
  {-# INLINE toJoin #-}
  
  toJoin1 :: (Widening a -> Widening b) -> (a -> a -> a) -> (b -> b -> b)
  toJoin1 f g a a' = snd (f (\b b' -> (Unstable,g b b')) a a')
  {-# INLINE toJoin1 #-}
  
  toJoin2 :: (Widening a -> Widening b -> Widening c) -> (a -> a -> a) -> (b -> b -> b) -> (c -> c -> c)
  toJoin2 f g h c c' = snd (f (\a a' -> (Unstable,g a a')) (\b b' -> (Unstable,h b b')) c c')
  {-# INLINE toJoin2 #-}
  
  -- | Widening operator that joins until the given limit is
  -- reached. Then it calls the fallback widening operator.
  bounded :: Complete a => a -> Widening a -> Widening a
  bounded limit w a b
    | b ⊑ limit = let b' = a ⊔ b
                  in (if b' ⊑ b then Stable else Unstable,b')
    | otherwise = a `w` b
  {-# INLINE bounded #-}
  
  (**) :: Widening a -> Widening b -> Widening (a,b)
  (**) wa wb (a1,b1) (a2,b2) =
      let (s1,a') = wa a1 a2
          (s2,b') = wb b1 b2
      in (s1 ⊔ s2, (a',b'))
  {-# INLINE (**) #-}
  