    -----------------------------------------------------------------------------
    -- |
    -- Module    : Documentation.SBV.Examples.BitPrecise.PrefixSum
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- The PrefixSum algorithm over power-lists and proof of
    -- the Ladner-Fischer implementation.
    -- See <http://dl.acm.org/citation.cfm?id=197356>
    -- and <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>.
    -----------------------------------------------------------------------------

    {-# LANGUAGE Rank2Types          #-}
    {-# LANGUAGE ScopedTypeVariables #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Documentation.SBV.Examples.BitPrecise.PrefixSum where

    import Data.SBV

    -- $setup
    -- >>> -- For doctest purposes only:
    -- >>> import Data.SBV

    ----------------------------------------------------------------------
    -- * Formalizing power-lists
    ----------------------------------------------------------------------

    -- | A poor man's representation of powerlists and
    -- basic operations on them: <http://dl.acm.org/citation.cfm?id=197356>
    -- We merely represent power-lists by ordinary lists.
    type PowerList a = [a]

    -- | The tie operator, concatenation.
    tiePL :: PowerList a -> PowerList a -> PowerList a
    tiePL :: forall a. PowerList a -> PowerList a -> PowerList a
    tiePL = [a] -> [a] -> [a]
    forall a. PowerList a -> PowerList a -> PowerList a
    (++)

    -- | The zip operator, zips the power-lists of the same size, returns
    -- a powerlist of double the size.
    zipPL :: PowerList a -> PowerList a -> PowerList a
    zipPL :: forall a. PowerList a -> PowerList a -> PowerList a
    zipPL []     []     = []
    zipPL (a
    x:[a]
    xs) (a
    y:[a]
    ys) = a
    x a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : a
    y a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a] -> [a] -> [a]
    forall a. PowerList a -> PowerList a -> PowerList a
    zipPL [a]
    xs [a]
    ys
    zipPL [a]
    _      [a]
    _      = [Char] -> [a]
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "zipPL: nonsimilar powerlists received"

    -- | Inverse of zipping.
    unzipPL :: PowerList a -> (PowerList a, PowerList a)
    unzipPL :: forall a. PowerList a -> (PowerList a, PowerList a)
    unzipPL = [(a, a)] -> ([a], [a])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([(a, a)] -> ([a], [a])) -> ([a] -> [(a, a)]) -> [a] -> ([a], [a])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [a] -> [(a, a)]
    forall {b}. [b] -> [(b, b)]
    chunk2
      where chunk2 :: [b] -> [(b, b)]
    chunk2 []       = []
            chunk2 (b
    x:b
    y:[b]
    xs) = (b
    x,b
    y) (b, b) -> [(b, b)] -> [(b, b)]
    forall a. a -> [a] -> [a]
    : [b] -> [(b, b)]
    chunk2 [b]
    xs
            chunk2 [b]
    _        = [Char] -> [(b, b)]
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "unzipPL: malformed powerlist"

    ----------------------------------------------------------------------
    -- * Reference prefix-sum implementation
    ----------------------------------------------------------------------

    -- | Reference prefix sum (@ps@) is simply Haskell's @scanl1@ function.
    ps :: (a, a -> a -> a) -> PowerList a -> PowerList a
    ps :: forall a. (a, a -> a -> a) -> PowerList a -> PowerList a
    ps (a
    _, a -> a -> a
    f) = (a -> a -> a) -> [a] -> [a]
    forall a. (a -> a -> a) -> [a] -> [a]
    scanl1 a -> a -> a
    f

    ----------------------------------------------------------------------
    -- * The Ladner-Fischer parallel version
    ----------------------------------------------------------------------

    -- | The Ladner-Fischer (@lf@) implementation of prefix-sum. See <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>
    -- or pg. 16 of <http://dl.acm.org/citation.cfm?id=197356>
    lf :: (a, a -> a -> a) -> PowerList a -> PowerList a
    lf :: forall a. (a, a -> a -> a) -> PowerList a -> PowerList a
    lf (a, a -> a -> a)
    _ []         = [Char] -> [a]
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "lf: malformed (empty) powerlist"
    lf (a, a -> a -> a)
    _ [a
    x]        = [a
    x]
    lf (a
    zero, a -> a -> a
    f) [a]
    pl = [a] -> [a] -> [a]
    forall a. PowerList a -> PowerList a -> PowerList a
    zipPL ((a -> a -> a) -> [a] -> [a] -> [a]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith a -> a -> a
    f ([a] -> [a]
    rsh [a]
    lfpq) [a]
    p) [a]
    lfpq
       where ([a]
    p, [a]
    q) = [a] -> ([a], [a])
    forall a. PowerList a -> (PowerList a, PowerList a)
    unzipPL [a]
    pl
             pq :: [a]
    pq     = (a -> a -> a) -> [a] -> [a] -> [a]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith a -> a -> a
    f [a]
    p [a]
    q
             lfpq :: [a]
    lfpq   = (a, a -> a -> a) -> [a] -> [a]
    forall a. (a, a -> a -> a) -> PowerList a -> PowerList a
    lf (a
    zero, a -> a -> a
    f) [a]
    pq
             rsh :: [a] -> [a]
    rsh [a]
    xs = a
    zero a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a] -> [a]
    forall a. HasCallStack => [a] -> [a]
    init [a]
    xs

    ----------------------------------------------------------------------
    -- * Sample proofs for concrete operators
    ----------------------------------------------------------------------

    -- | Correctness theorem, for a powerlist of given size, an associative operator, and its left-unit element.
    flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool
    flIsCorrect :: Int
    -> (forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a))
    -> Symbolic SBool
    flIsCorrect Int
    n forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a)
    zf = do
            PowerList SWord32
    args :: PowerList SWord32 <- Int -> Symbolic (PowerList SWord32)
    forall a. SymVal a => Int -> Symbolic [SBV a]
    mkFreeVars Int
    n
            SBool -> Symbolic SBool
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> Symbolic SBool) -> SBool -> Symbolic SBool
    forall a b. (a -> b) -> a -> b
    $ (SWord32, SWord32 -> SWord32 -> SWord32)
    -> PowerList SWord32 -> PowerList SWord32
    forall a. (a, a -> a -> a) -> PowerList a -> PowerList a
    ps (SWord32, SWord32 -> SWord32 -> SWord32)
    forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a)
    zf PowerList SWord32
    args PowerList SWord32 -> PowerList SWord32 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== (SWord32, SWord32 -> SWord32 -> SWord32)
    -> PowerList SWord32 -> PowerList SWord32
    forall a. (a, a -> a -> a) -> PowerList a -> PowerList a
    lf (SWord32, SWord32 -> SWord32 -> SWord32)
    forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a)
    zf PowerList SWord32
    args

    -- | Proves Ladner-Fischer is equivalent to reference specification for addition.
    -- @0@ is the left-unit element, and we use a power-list of size @8@. We have:
    --
    -- >>> thm1
    -- Q.E.D.
    thm1 :: IO ThmResult
    thm1 :: IO ThmResult
    thm1 = Symbolic SBool -> IO ThmResult
    forall a. Provable a => a -> IO ThmResult
    prove (Symbolic SBool -> IO ThmResult) -> Symbolic SBool -> IO ThmResult
    forall a b. (a -> b) -> a -> b
    $ Int
    -> (forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a))
    -> Symbolic SBool
    flIsCorrect  Int
    8 (a
    0, a -> a -> a
    forall a. Num a => a -> a -> a
    (+))

    -- | Proves Ladner-Fischer is equivalent to reference specification for the function @max@.
    -- @0@ is the left-unit element, and we use a power-list of size @16@. We have:
    --
    -- >>> thm2
    -- Q.E.D.
    thm2 :: IO ThmResult
    thm2 :: IO ThmResult
    thm2 = Symbolic SBool -> IO ThmResult
    forall a. Provable a => a -> IO ThmResult
    prove (Symbolic SBool -> IO ThmResult) -> Symbolic SBool -> IO ThmResult
    forall a b. (a -> b) -> a -> b
    $ Int
    -> (forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a))
    -> Symbolic SBool
    flIsCorrect Int
    16 (a
    0, a -> a -> a
    forall a. OrdSymbolic a => a -> a -> a
    smax)