-- | General operations on sets

module Feldspar.Set where



-- | A 'Set' is an *over-approximation* of a set of values. The class does not
-- care about how the set is interpreted, but it only makes sense to use
-- interpretations for which the operations are sound.
class Eq a => Set a
  where
    empty     :: a
    universal :: a
    -- | Union
    (\/)      :: a -> a -> a
    -- | Intersection
    (/\)      :: a -> a -> a

-- | Approximates all sets as @()@, which is the 'universal' set.
instance Set ()
  where
    empty     = ()
    universal = ()
    () \/ ()  = ()
    () /\ ()  = ()

-- | Set product
instance (Set a, Set b) => Set (a,b)
  where
    empty     = (empty,empty)
    universal = (universal,universal)
    (a1,a2) \/ (b1,b2) = (a1 \/ b1, a2 \/ b2)
    (a1,a2) /\ (b1,b2) = (a1 /\ b1, a2 /\ b2)

-- | Three-way product
instance (Set a, Set b, Set c) => Set (a,b,c)
  where
    empty     = (empty,empty,empty)
    universal = (universal,universal,universal)
    (a1,a2,a3) \/ (b1,b2,b3) = (a1 \/ b1, a2 \/ b2, a3 \/ b3)
    (a1,a2,a3) /\ (b1,b2,b3) = (a1 /\ b1, a2 /\ b2, a3 /\ b3)

-- | Four-way product
instance (Set a, Set b, Set c, Set d) => Set (a,b,c,d)
  where
    empty     = (empty,empty,empty,empty)
    universal = (universal,universal,universal,universal)
    (a1,a2,a3,a4) \/ (b1,b2,b3,b4) = (a1 \/ b1, a2 \/ b2, a3 \/ b3, a4 \/ b4)
    (a1,a2,a3,a4) /\ (b1,b2,b3,b4) = (a1 /\ b1, a2 /\ b2, a3 /\ b3, a4 /\ b4)

unions :: Set a => [a] -> a
unions = foldr (\/) empty

intersections :: Set a => [a] -> a
intersections = foldr (/\) universal

-- Computing fixed points

-- | Take the fixed point of a monotonic function. The second argument is
--   an initial element. A sensible default for the initial element is
--   'empty'.
fixedPoint :: Set a => (a -> a) -> a -> a
fixedPoint f a | fa == a   = fa
               | otherwise = fixedPoint f fa
  where fa = f a \/ a

-- | Much like 'fixedPoint' but keeps track of the number of iterations
--   in the fixed point iteration. Useful for defining widening operators.
indexedFixedPoint :: Set a => (Int -> a -> a) -> a -> (a,Int)
indexedFixedPoint f a = go 0 f a
  where go i f a | fa == a   = (fa,i)
                 | otherwise = go (i+1) f fa
          where fa = f i a \/ a

-- | The type of widening operators. A widening operator modifies a
--   function that is subject to fixed point analysis. A widening
--   operator introduces approximations in order to guarantee (fast)
--   termination of the fixed point analysis.
type Widening a = (Int -> a -> a) -> (Int -> a -> a)

-- | A widening operator which defaults to 'universal' when the number of
--   iterations goes over the specified value.
cutOffAt :: Set a => Int -> Widening a
cutOffAt n f i a | i >= n    = universal
                 | otherwise = f i a