-----------------------------------------------------------------------------
-- |
-- 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 <https://www.cs.utexas.edu/~misra/psp.dir/powerlist.pdf>
-- and <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>.
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.BitPrecise.PrefixSum where

import Data.SBV

#ifndef HADDOCK
-- $setup
-- >>> -- For doctest purposes only:
-- >>> import Data.SBV
#endif

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

-- | A poor man's representation of powerlists and
-- basic operations on them: <https://www.cs.utexas.edu/~misra/psp.dir/powerlist.pdf>.
-- 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.
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
        args :: PowerList SWord32 <- Int -> Symbolic (PowerList SWord32)
forall a. SymVal a => Int -> Symbolic [SBV a]
mkFreeVars Int
n
        return $ ps zf args .== lf zf 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)