{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.BitPrecise.MergeSort where
import Data.SBV
import Data.SBV.Tools.CodeGen
type E = SWord8
merge :: [E] -> [E] -> [E]
merge :: [E] -> [E] -> [E]
merge [] ys :: [E]
ys = [E]
ys
merge xs :: [E]
xs [] = [E]
xs
merge xs :: [E]
xs@(x :: E
x:xr :: [E]
xr) ys :: [E]
ys@(y :: E
y:yr :: [E]
yr) = SBool -> [E] -> [E] -> [E]
forall a. Mergeable a => SBool -> a -> a -> a
ite (E
x E -> E -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< E
y) (E
x E -> [E] -> [E]
forall a. a -> [a] -> [a]
: [E] -> [E] -> [E]
merge [E]
xr [E]
ys) (E
y E -> [E] -> [E]
forall a. a -> [a] -> [a]
: [E] -> [E] -> [E]
merge [E]
xs [E]
yr)
mergeSort :: [E] -> [E]
mergeSort :: [E] -> [E]
mergeSort [] = []
mergeSort [x :: E
x] = [E
x]
mergeSort xs :: [E]
xs = [E] -> [E] -> [E]
merge ([E] -> [E]
mergeSort [E]
th) ([E] -> [E]
mergeSort [E]
bh)
where (th :: [E]
th, bh :: [E]
bh) = Int -> [E] -> ([E], [E])
forall a. Int -> [a] -> ([a], [a])
splitAt ([E] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [E]
xs Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` 2) [E]
xs
nonDecreasing :: [E] -> SBool
nonDecreasing :: [E] -> SBool
nonDecreasing [] = SBool
sTrue
nonDecreasing [_] = SBool
sTrue
nonDecreasing (a :: E
a:b :: E
b:xs :: [E]
xs) = E
a E -> E -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= E
b SBool -> SBool -> SBool
.&& [E] -> SBool
nonDecreasing (E
bE -> [E] -> [E]
forall a. a -> [a] -> [a]
:[E]
xs)
isPermutationOf :: [E] -> [E] -> SBool
isPermutationOf :: [E] -> [E] -> SBool
isPermutationOf as :: [E]
as bs :: [E]
bs = [E] -> [(E, SBool)] -> SBool
forall a.
(Mergeable a, EqSymbolic a) =>
[a] -> [(a, SBool)] -> SBool
go [E]
as ([E] -> [SBool] -> [(E, SBool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [E]
bs (SBool -> [SBool]
forall a. a -> [a]
repeat SBool
sTrue)) SBool -> SBool -> SBool
.&& [E] -> [(E, SBool)] -> SBool
forall a.
(Mergeable a, EqSymbolic a) =>
[a] -> [(a, SBool)] -> SBool
go [E]
bs ([E] -> [SBool] -> [(E, SBool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [E]
as (SBool -> [SBool]
forall a. a -> [a]
repeat SBool
sTrue))
where go :: [a] -> [(a, SBool)] -> SBool
go [] _ = SBool
sTrue
go (x :: a
x:xs :: [a]
xs) ys :: [(a, SBool)]
ys = let (found :: SBool
found, ys' :: [(a, SBool)]
ys') = a -> [(a, SBool)] -> (SBool, [(a, SBool)])
forall a.
(Mergeable a, EqSymbolic a) =>
a -> [(a, SBool)] -> (SBool, [(a, SBool)])
mark a
x [(a, SBool)]
ys in SBool
found SBool -> SBool -> SBool
.&& [a] -> [(a, SBool)] -> SBool
go [a]
xs [(a, SBool)]
ys'
mark :: a -> [(a, SBool)] -> (SBool, [(a, SBool)])
mark _ [] = (SBool
sFalse, [])
mark x :: a
x ((y :: a
y,v :: SBool
v):ys :: [(a, SBool)]
ys) = SBool
-> (SBool, [(a, SBool)])
-> (SBool, [(a, SBool)])
-> (SBool, [(a, SBool)])
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBool
v SBool -> SBool -> SBool
.&& a
x a -> a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== a
y)
(SBool
sTrue, (a
y, SBool -> SBool
sNot SBool
v)(a, SBool) -> [(a, SBool)] -> [(a, SBool)]
forall a. a -> [a] -> [a]
:[(a, SBool)]
ys)
(let (r :: SBool
r, ys' :: [(a, SBool)]
ys') = a -> [(a, SBool)] -> (SBool, [(a, SBool)])
mark a
x [(a, SBool)]
ys in (SBool
r, (a
y,SBool
v)(a, SBool) -> [(a, SBool)] -> [(a, SBool)]
forall a. a -> [a] -> [a]
:[(a, SBool)]
ys'))
correctness :: Int -> IO ThmResult
correctness :: Int -> IO ThmResult
correctness n :: Int
n = SymbolicT IO SBool -> IO ThmResult
forall a. Provable a => a -> IO ThmResult
prove (SymbolicT IO SBool -> IO ThmResult)
-> SymbolicT IO SBool -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ do [E]
xs <- Int -> Symbolic [E]
forall a. SymVal a => Int -> Symbolic [SBV a]
mkFreeVars Int
n
let ys :: [E]
ys = [E] -> [E]
mergeSort [E]
xs
SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ [E] -> SBool
nonDecreasing [E]
ys SBool -> SBool -> SBool
.&& [E] -> [E] -> SBool
isPermutationOf [E]
xs [E]
ys
codeGen :: Int -> IO ()
codeGen :: Int -> IO ()
codeGen n :: Int
n = Maybe FilePath -> FilePath -> SBVCodeGen () -> IO ()
forall a. Maybe FilePath -> FilePath -> SBVCodeGen a -> IO a
compileToC (FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just ("mergeSort" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
n)) "mergeSort" (SBVCodeGen () -> IO ()) -> SBVCodeGen () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
[E]
xs <- Int -> FilePath -> SBVCodeGen [E]
forall a. SymVal a => Int -> FilePath -> SBVCodeGen [SBV a]
cgInputArr Int
n "xs"
FilePath -> [E] -> SBVCodeGen ()
forall a. SymVal a => FilePath -> [SBV a] -> SBVCodeGen ()
cgOutputArr "ys" ([E] -> [E]
mergeSort [E]
xs)