-----------------------------------------------------------------------------
-- |
-- 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. Note that this
-- version, while fully push-button, proves merge-sort correct for fixed number
-- of elements, i.e., not in its generality. A general proof would require
-- non-trivial applications of induction and more manual guiding. We do
-- such a proof in "Documentation.SBV.Examples.KnuckleDragger.MergeSort", which
-- shows the full-power of the theorem-proving like aspects of SBV.
-----------------------------------------------------------------------------

{-# LANGUAGE TupleSections #-}

{-# 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 []     [E]
ys           = [E]
ys
merge [E]
xs     []           = [E]
xs
merge xs :: [E]
xs@(E
x:[E]
xr) ys :: [E]
ys@(E
y:[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 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 [E
x] = [E
x]
mergeSort [E]
xs  = [E] -> [E] -> [E]
merge ([E] -> [E]
mergeSort [E]
th) ([E] -> [E]
mergeSort [E]
bh)
   where ([E]
th, [E]
bh) = Int -> [E] -> ([E], [E])
forall a. Int -> [a] -> ([a], [a])
splitAt ([E] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [E]
xs Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
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 [E
_]      = SBool
sTrue
nonDecreasing (E
a:E
b:[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 [E]
as [E]
bs = [E] -> [(E, SBool)] -> SBool
forall {a}.
(Mergeable a, EqSymbolic a) =>
[a] -> [(a, SBool)] -> SBool
go [E]
as ((E -> (E, SBool)) -> [E] -> [(E, SBool)]
forall a b. (a -> b) -> [a] -> [b]
map (, SBool
sTrue) [E]
bs) SBool -> SBool -> SBool
.&& [E] -> [(E, SBool)] -> SBool
forall {a}.
(Mergeable a, EqSymbolic a) =>
[a] -> [(a, SBool)] -> SBool
go [E]
bs ((E -> (E, SBool)) -> [E] -> [(E, SBool)]
forall a b. (a -> b) -> [a] -> [b]
map (, SBool
sTrue) [E]
as)
  where go :: [a] -> [(a, SBool)] -> SBool
go []     [(a, SBool)]
_  = SBool
sTrue
        go (a
x:[a]
xs) [(a, SBool)]
ys = let (SBool
found, [(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 a
_ []         = (SBool
sFalse, [])
        mark a
x ((a
y,SBool
v):[(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 (SBool
r, [(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 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 xs <- Int -> Symbolic [E]
forall a. SymVal a => Int -> Symbolic [SBV a]
mkFreeVars Int
n
                           let ys = [E] -> [E]
mergeSort [E]
xs
                           return $ nonDecreasing ys .&& isPermutationOf xs 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 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 (FilePath
"mergeSort" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
n)) FilePath
"mergeSort" (SBVCodeGen () -> IO ()) -> SBVCodeGen () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
                xs <- Int -> FilePath -> SBVCodeGen [E]
forall a. SymVal a => Int -> FilePath -> SBVCodeGen [SBV a]
cgInputArr Int
n FilePath
"xs"
                cgOutputArr "ys" (mergeSort xs)