-----------------------------------------------------------------------------
-- |
-- 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 = 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 forall a. a -> [a] -> [a]
: a
y forall a. a -> [a] -> [a]
: forall a. PowerList a -> PowerList a -> PowerList a
zipPL [a]
xs [a]
ys
zipPL [a]
_      [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 = forall a b. [(a, b)] -> ([a], [b])
unzip forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {b}. [b] -> [(b, b)]
chunk2
  where chunk2 :: [b] -> [(b, b)]
chunk2 []       = []
        chunk2 (b
x:b
y:[b]
xs) = (b
x,b
y) forall a. a -> [a] -> [a]
: [b] -> [(b, b)]
chunk2 [b]
xs
        chunk2 [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) = 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)
_ []         = 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 = forall a. PowerList a -> PowerList a -> PowerList a
zipPL (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) = forall a. PowerList a -> (PowerList a, PowerList a)
unzipPL [a]
pl
         pq :: [a]
pq     = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> a
f [a]
p [a]
q
         lfpq :: [a]
lfpq   = 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 forall a. a -> [a] -> [a]
: forall a. [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 <- forall a. SymVal a => Int -> Symbolic [SBV a]
mkForallVars Int
n
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a, a -> a -> a) -> PowerList a -> PowerList a
ps forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a)
zf PowerList SWord32
args forall a. EqSymbolic a => a -> a -> SBool
.== forall a. (a, a -> a -> a) -> PowerList a -> PowerList a
lf 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 = forall a. Provable a => a -> IO ThmResult
prove 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, 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 = forall a. Provable a => a -> IO ThmResult
prove 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, forall a. OrdSymbolic a => a -> a -> a
smax)