-----------------------------------------------------------------------------
-- |
-- 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 :: PowerList a -> PowerList a -> PowerList a
tiePL = PowerList a -> PowerList a -> PowerList a
forall a. [a] -> [a] -> [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 :: PowerList a -> PowerList a -> PowerList a
zipPL []     []     = []
zipPL (a
x:PowerList a
xs) (a
y:PowerList a
ys) = a
x a -> PowerList a -> PowerList a
forall a. a -> [a] -> [a]
: a
y a -> PowerList a -> PowerList a
forall a. a -> [a] -> [a]
: PowerList a -> PowerList a -> PowerList a
forall a. [a] -> [a] -> [a]
zipPL PowerList a
xs PowerList a
ys
zipPL PowerList a
_      PowerList a
_      = [Char] -> PowerList a
forall a. HasCallStack => [Char] -> a
error [Char]
"zipPL: nonsimilar powerlists received"

-- | Inverse of zipping.
unzipPL :: PowerList a -> (PowerList a, PowerList a)
unzipPL :: PowerList a -> (PowerList a, PowerList a)
unzipPL = [(a, a)] -> (PowerList a, PowerList a)
forall a b. [(a, b)] -> ([a], [b])
unzip ([(a, a)] -> (PowerList a, PowerList a))
-> (PowerList a -> [(a, a)])
-> PowerList a
-> (PowerList a, PowerList a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PowerList 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 :: (a, a -> a -> a) -> PowerList a -> PowerList a
ps (a
_, a -> a -> a
f) = (a -> a -> a) -> PowerList a -> PowerList 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 :: (a, a -> a -> a) -> PowerList a -> PowerList a
lf (a, a -> a -> a)
_ []         = [Char] -> PowerList 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) PowerList a
pl = PowerList a -> PowerList a -> PowerList a
forall a. [a] -> [a] -> [a]
zipPL ((a -> a -> a) -> PowerList a -> PowerList a -> PowerList a
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> a
f (PowerList a -> PowerList a
rsh PowerList a
lfpq) PowerList a
p) PowerList a
lfpq
   where (PowerList a
p, PowerList a
q) = PowerList a -> (PowerList a, PowerList a)
forall a. PowerList a -> (PowerList a, PowerList a)
unzipPL PowerList a
pl
         pq :: PowerList a
pq     = (a -> a -> a) -> PowerList a -> PowerList a -> PowerList a
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> a
f PowerList a
p PowerList a
q
         lfpq :: PowerList a
lfpq   = (a, a -> a -> a) -> PowerList a -> PowerList a
forall a. (a, a -> a -> a) -> PowerList a -> PowerList a
lf (a
zero, a -> a -> a
f) PowerList a
pq
         rsh :: PowerList a -> PowerList a
rsh PowerList a
xs = a
zero a -> PowerList a -> PowerList a
forall a. a -> [a] -> [a]
: PowerList a -> PowerList a
forall a. [a] -> [a]
init PowerList 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]
mkForallVars Int
n
        SBool -> Symbolic SBool
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)