-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.BitPrecise.MergeSort
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Symbolic implementation of merge-sort and its correctness.
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.BitPrecise.MergeSort where

import Data.SBV
import Data.SBV.Tools.CodeGen

-----------------------------------------------------------------------------
-- * Implementing Merge-Sort
-----------------------------------------------------------------------------
-- | Element type of lists we'd like to sort. For simplicity, we'll just
-- use 'SWord8' here, but we can pick any symbolic type.
type E = SWord8

-- | Merging two given sorted lists, preserving the order.
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)

-- | Simple merge-sort implementation. We simply divide the input list
-- in two two halves so long as it has at least two elements, sort
-- each half on its own, and then merge.
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

-----------------------------------------------------------------------------
-- * Proving correctness
-- ${props}
-----------------------------------------------------------------------------
{- $props
There are two main parts to proving that a sorting algorithm is correct:

       * Prove that the output is non-decreasing
 
       * Prove that the output is a permutation of the input
-}

-- | Check whether a given sequence is non-decreasing.
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)

-- | Check whether two given sequences are permutations. We simply check that each sequence
-- is a subset of the other, when considered as a set. The check is slightly complicated
-- for the need to account for possibly duplicated elements.
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'
        -- Go and mark off an instance of 'x' in the list, if possible. We keep track
        -- of unmarked elements by associating a boolean bit. Note that we have to
        -- keep the lists equal size for the recursive result to merge properly.
        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'))

-- | Asserting correctness of merge-sort for a list of the given size. Note that we can
-- only check correctness for fixed-size lists. Also, the proof will get more and more
-- complicated for the backend SMT solver as the list size increases. A value around
-- 5 or 6 should be fairly easy to prove. For instance, we have:
--
-- >>> correctness 5
-- Q.E.D.
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

-----------------------------------------------------------------------------
-- * Generating C code
-----------------------------------------------------------------------------

-- | Generate C code for merge-sorting an array of size @n@. Again, we're restricted
-- to fixed size inputs. While the output is not how one would code merge sort in C
-- by hand, it's a faithful rendering of all the operations merge-sort would do as
-- described by its Haskell counterpart.
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)