--
-- Copyright (c) 2009-2011, ERICSSON AB
-- All rights reserved.
--
-- Redistribution and use in source and binary forms, with or without
-- modification, are permitted provided that the following conditions are met:
--
--     * Redistributions of source code must retain the above copyright notice,
--       this list of conditions and the following disclaimer.
--     * Redistributions in binary form must reproduce the above copyright
--       notice, this list of conditions and the following disclaimer in the
--       documentation and/or other materials provided with the distribution.
--     * Neither the name of the ERICSSON AB nor the names of its contributors
--       may be used to endorse or promote products derived from this software
--       without specific prior written permission.
--
-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
-- AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
-- IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-- DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
-- FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
-- DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
-- SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
-- CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
-- OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-- OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
--

-- | General operations on sets

module Feldspar.Lattice where



import Data.Lens.Common



-- | Lattice types
class Eq a => Lattice a
  where
    bot       :: a
    top       :: a
    -- | Join
    (\/)      :: a -> a -> a
    -- | Meet
    (/\)      :: a -> a -> a

empty :: Lattice a => a
empty = bot

universal :: Lattice a => a
universal = top

instance Lattice ()
  where
    bot       = ()
    top       = ()
    () \/ ()  = ()
    () /\ ()  = ()

-- | Lattice product
instance (Lattice a, Lattice b) => Lattice (a,b)
  where
    bot = (bot,bot)
    top = (top,top)
    (a1,a2) \/ (b1,b2) = (a1 \/ b1, a2 \/ b2)
    (a1,a2) /\ (b1,b2) = (a1 /\ b1, a2 /\ b2)

-- | Three-way product
instance (Lattice a, Lattice b, Lattice c) => Lattice (a,b,c)
  where
    bot = (bot,bot,bot)
    top = (top,top,top)
    (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 (Lattice a, Lattice b, Lattice c, Lattice d) => Lattice (a,b,c,d)
  where
    bot = (bot,bot,bot,bot)
    top = (top,top,top,top)
    (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)

-- | Five-way product
instance (Lattice a, Lattice b, Lattice c, Lattice d, Lattice e) => Lattice (a,b,c,d,e)
  where
    bot = (bot,bot,bot,bot,bot)
    top = (top,top,top,top,top)
    (a1,a2,a3,a4,a5) \/ (b1,b2,b3,b4,b5) = (a1 \/ b1, a2 \/ b2, a3 \/ b3, a4 \/ b4, a5 \/ b5)
    (a1,a2,a3,a4,a5) /\ (b1,b2,b3,b4,b5) = (a1 /\ b1, a2 /\ b2, a3 /\ b3, a4 /\ b4, a5 /\ b5)

-- | Six-way product
instance (Lattice a, Lattice b, Lattice c, Lattice d, Lattice e, Lattice f) => Lattice (a,b,c,d,e,f)
  where
    bot = (bot,bot,bot,bot,bot,bot)
    top = (top,top,top,top,top,top)
    (a1,a2,a3,a4,a5,a6) \/ (b1,b2,b3,b4,b5,b6) = (a1 \/ b1, a2 \/ b2, a3 \/ b3, a4 \/ b4, a5 \/ b5, a6 \/ b6)
    (a1,a2,a3,a4,a5,a6) /\ (b1,b2,b3,b4,b5,b6) = (a1 /\ b1, a2 /\ b2, a3 /\ b3, a4 /\ b4, a5 /\ b5, a6 /\ b6)

-- | Seven-way product
instance (Lattice a, Lattice b, Lattice c, Lattice d, Lattice e, Lattice f, Lattice g) => Lattice (a,b,c,d,e,f,g)
  where
    bot = (bot,bot,bot,bot,bot,bot,bot)
    top = (top,top,top,top,top,top,top)
    (a1,a2,a3,a4,a5,a6,a7) \/ (b1,b2,b3,b4,b5,b6,b7) = (a1 \/ b1, a2 \/ b2, a3 \/ b3, a4 \/ b4, a5 \/ b5, a6 \/ b6, a7 \/ b7)
    (a1,a2,a3,a4,a5,a6,a7) /\ (b1,b2,b3,b4,b5,b6,b7) = (a1 /\ b1, a2 /\ b2, a3 /\ b3, a4 /\ b4, a5 /\ b5, a6 /\ b6, a7 /\ b7)

-- | Accumulated join
unions :: Lattice a => [a] -> a
unions = foldr (\/) bot

-- | Accumulated meet
intersections :: Lattice a => [a] -> a
intersections = foldr (/\) top



-- * Computing fixed points

-- | Generalization of 'fixedPoint' to functions whose argument and result
-- contain (i.e has a lens to) a common lattice
lensedFixedPoint :: Lattice lat =>
    Lens a lat -> Lens b lat -> (a -> b) -> (a -> b)
lensedFixedPoint aLens bLens f a
    | aLat == bLat = (bLens ^= aLat) b
    | otherwise    = lensedFixedPoint aLens bLens f a'
  where
    aLat = a ^! aLens
    b    = f a
    bLat = (b ^! bLens) \/ aLat
    a'   = (aLens ^= bLat) a

-- | Generalization of 'indexedFixedPoint' to functions whose argument and
-- result contain (i.e has a lens to) a common lattice
lensedIndexedFixedPoint :: Lattice lat =>
    Lens a lat -> Lens b lat -> (Int -> a -> b) -> (a -> (b,Int))
lensedIndexedFixedPoint aLens bLens f = go 0
  where
    go i a
        | aLat == bLat = ((bLens ^= aLat) b, i)
        | otherwise    = go (i+1) a'
      where
        aLat = a ^! aLens
        b    = f i a
        bLat = (b ^! bLens) \/ aLat
        a'   = (aLens ^= bLat) a

-- | Take the fixed point of a function. The second argument is an initial
--  element. A sensible default for the initial element is 'bot'.
--
-- The function is not required to be monotonic. It is made monotonic internally
-- by always taking the union of the result and the previous value.
fixedPoint :: Lattice a => (a -> a) -> a -> a
fixedPoint = lensedFixedPoint (iso id id) (iso id id)

-- | Much like 'fixedPoint' but keeps track of the number of iterations
--   in the fixed point iteration. Useful for defining widening operators.
indexedFixedPoint :: Lattice a => (Int -> a -> a) -> a -> (a,Int)
indexedFixedPoint = lensedIndexedFixedPoint (iso id id) (iso id id)

-- | 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 'top' when the number of
--   iterations goes over the specified value.
cutOffAt :: Lattice a => Int -> Widening a
cutOffAt n f i a | i >= n    = top
                 | otherwise = f i a

-- | A bounded version of 'lensedFixedPoint'. It will always do at least one
-- iteration regardless of the provided bound (in order to return something of
-- the right type).
boundedLensedFixedPoint :: Lattice lat =>
    Int -> Lens a lat -> Lens b lat -> (a -> b) -> (a -> (b,Int))
boundedLensedFixedPoint n aLens bLens f = go 0
  where
    go i a
        | aLat == bLat = ((bLens ^= aLat) b, i)
        | i >= n-1     = ((bLens ^= top) b, i)
        | otherwise    = go (i+1) a'
      where
        aLat = a ^! aLens
        b    = f a
        bLat = (b ^! bLens) \/ aLat
        a'   = (aLens ^= bLat) a
  -- Note: This function achieves a similar effect to
  -- `indexedFixedPoint (cutOffAt n ...)`. The difference is that it works for
  -- lensed fixed points. It would be possible to define a version of `cutOffAt`
  -- that works for lensed fixed points, but such an operator would be less
  -- efficient since it would have to apply the argument function in the base
  -- case as well as the recursive case (in order to return something of the
  -- right type). This means that there would always be one extra unnecessary
  -- iteration. In particular, it would not be possible to get a meaningful
  -- result from performing a single iteration. To only perform a single
  -- iteration, the cut-off function would have to "fail" immediately, which
  -- means that the whole fixed point iteration would also "fail". (A
  -- single-iteration fixed point is an important special case as it avoids
  -- exponential blowup when performing several nested iterations.)