Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Add merge-sort example

  • Loading branch information...
commit b42ec29120ac0142c5793e526fd974182d87c1e1 1 parent b9b7870
@LeventErkok authored
View
95 Data/SBV/Examples/BitPrecise/MergeSort.hs
@@ -0,0 +1,95 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module : Data.SBV.Examples.BitPrecise.MergeSort
+-- Copyright : (c) Levent Erkok
+-- License : BSD3
+-- Maintainer : erkokl@gmail.com
+-- Stability : experimental
+-- Portability : portable
+--
+-- Symbolic implementation of merge-sort and its correctness.
+-----------------------------------------------------------------------------
+
+module Data.SBV.Examples.BitPrecise.MergeSort where
+
+import Data.SBV
+
+-----------------------------------------------------------------------------
+-- * 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 [] ys = ys
+merge xs [] = xs
+merge xs@(x:xr) ys@(y:yr) = ite (x .< y) (x : merge xr ys) (y : merge xs 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 [] = []
+mergeSort [x] = [x]
+mergeSort xs = merge (mergeSort th) (mergeSort bh)
+ where (th, bh) = splitAt (length xs `div` 2) 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 [] = true
+nonDecreasing [_] = true
+nonDecreasing (a:b:xs) = a .<= b &&& nonDecreasing (b: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 as bs = go as (zip bs (repeat true)) &&& go bs (zip as (repeat true))
+ where go [] _ = true
+ go (x:xs) ys = let (found, ys') = mark x ys in found &&& go xs 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 _ [] = (false, [])
+ mark x ((y,v):ys) = ite (v &&& x .== y)
+ (true, (y, bnot v):ys)
+ (let (r, ys') = mark x ys in (r, (y,v):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 'n' 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 n = prove $ do xs <- mkFreeVars n
+ let ys = mergeSort 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 it's Haskell counterpart.
+codeGen :: Int -> IO ()
+codeGen n = compileToC (Just ("mergeSort" ++ show n)) "mergeSort" $ do
+ xs <- cgInputArr n "xs"
+ cgOutputArr "ys" (mergeSort xs)
View
4 RELEASENOTES
@@ -6,7 +6,7 @@ Latest Hackage released version: 1.3
======================================================================
Version 1.4, Not yet released
- Library
+ Library:
* Fix minor bug in the default implementation of select when the
indexer is an SInteger. Since SInteger is unbounded, we cannot
use the bit-walking trick on non-base non-mergeable types as we
@@ -16,6 +16,8 @@ Version 1.4, Not yet released
would've caused a call to "error" anyhow, so there's no soundness
concern.)
* Increase haddock coverage metrics
+ Examples:
+ * Add merge-sort example: Data.SBV.Examples.BitPrecise.MergeSort
======================================================================
Version 1.3, 2012-02-25
View
152 SBVUnitTest/GoldFiles/merge.gold
@@ -0,0 +1,152 @@
+== BEGIN: "Makefile" ================
+# Makefile for merge. Automatically generated by SBV. Do not edit!
+
+# include any user-defined .mk file in the current directory.
+-include *.mk
+
+CC=gcc
+CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
+
+all: merge_driver
+
+merge.o: merge.c merge.h
+ ${CC} ${CCFLAGS} -c $< -o $@
+
+merge_driver.o: merge_driver.c
+ ${CC} ${CCFLAGS} -c $< -o $@
+
+merge_driver: merge.o merge_driver.o
+ ${CC} ${CCFLAGS} $^ -o $@
+
+clean:
+ rm -f *.o
+
+veryclean: clean
+ rm -f merge_driver
+== END: "Makefile" ==================
+== BEGIN: "merge.h" ================
+/* Header file for merge. Automatically generated by SBV. Do not edit! */
+
+#ifndef __merge__HEADER_INCLUDED__
+#define __merge__HEADER_INCLUDED__
+
+#include <inttypes.h>
+#include <stdint.h>
+#include <stdbool.h>
+
+/* The boolean type */
+typedef bool SBool;
+
+/* Unsigned bit-vectors */
+typedef uint8_t SWord8 ;
+typedef uint16_t SWord16;
+typedef uint32_t SWord32;
+typedef uint64_t SWord64;
+
+/* Signed bit-vectors */
+typedef int8_t SInt8 ;
+typedef int16_t SInt16;
+typedef int32_t SInt32;
+typedef int64_t SInt64;
+
+/* Entry point prototype: */
+void merge(const SWord8 *xs, SWord8 *ys);
+
+#endif /* __merge__HEADER_INCLUDED__ */
+== END: "merge.h" ==================
+== BEGIN: "merge_driver.c" ================
+/* Example driver program for merge. */
+/* Automatically generated by SBV. Edit as you see fit! */
+
+#include <inttypes.h>
+#include <stdint.h>
+#include <stdbool.h>
+#include <stdio.h>
+#include "merge.h"
+
+int main(void)
+{
+ const SWord8 xs[5] = {
+ 10, 6, 4, 82, 71
+ };
+
+ printf("Contents of input array xs:\n");
+ int xs_ctr;
+ for(xs_ctr = 0; xs_ctr < 5 ; ++xs_ctr)
+ printf(" xs[%d] = %"PRIu8"\n", xs_ctr ,xs[xs_ctr]);
+
+ SWord8 ys[5];
+
+ merge(xs, ys);
+
+ printf("merge(xs, ys) ->\n");
+ int ys_ctr;
+ for(ys_ctr = 0; ys_ctr < 5 ; ++ys_ctr)
+ printf(" ys[%d] = %"PRIu8"\n", ys_ctr ,ys[ys_ctr]);
+
+ return 0;
+}
+== END: "merge_driver.c" ==================
+== BEGIN: "merge.c" ================
+/* File: "merge.c". Automatically generated by SBV. Do not edit! */
+
+#include <inttypes.h>
+#include <stdint.h>
+#include <stdbool.h>
+#include "merge.h"
+
+void merge(const SWord8 *xs, SWord8 *ys)
+{
+ const SWord8 s0 = xs[0];
+ const SWord8 s1 = xs[1];
+ const SWord8 s2 = xs[2];
+ const SWord8 s3 = xs[3];
+ const SWord8 s4 = xs[4];
+ const SBool s5 = s0 < s1;
+ const SWord8 s6 = s5 ? s0 : s1;
+ const SBool s7 = s3 < s4;
+ const SWord8 s8 = s7 ? s3 : s4;
+ const SBool s9 = s2 < s8;
+ const SWord8 s10 = s9 ? s2 : s8;
+ const SBool s11 = s6 < s10;
+ const SWord8 s12 = s11 ? s6 : s10;
+ const SWord8 s13 = s5 ? s1 : s0;
+ const SBool s14 = s13 < s10;
+ const SWord8 s15 = s14 ? s13 : s10;
+ const SWord8 s16 = s7 ? s4 : s3;
+ const SBool s17 = s2 < s16;
+ const SWord8 s18 = s17 ? s2 : s16;
+ const SWord8 s19 = s9 ? s8 : s18;
+ const SBool s20 = s6 < s19;
+ const SWord8 s21 = s20 ? s6 : s19;
+ const SWord8 s22 = s11 ? s15 : s21;
+ const SBool s23 = s13 < s19;
+ const SWord8 s24 = s23 ? s13 : s19;
+ const SWord8 s25 = s14 ? s10 : s24;
+ const SWord8 s26 = s17 ? s16 : s2;
+ const SWord8 s27 = s9 ? s16 : s26;
+ const SBool s28 = s6 < s27;
+ const SWord8 s29 = s28 ? s6 : s27;
+ const SWord8 s30 = s20 ? s24 : s29;
+ const SWord8 s31 = s11 ? s25 : s30;
+ const SBool s32 = s13 < s27;
+ const SWord8 s33 = s32 ? s13 : s27;
+ const SWord8 s34 = s23 ? s19 : s33;
+ const SWord8 s35 = s14 ? s19 : s34;
+ const SWord8 s36 = s28 ? s33 : s6;
+ const SWord8 s37 = s20 ? s34 : s36;
+ const SWord8 s38 = s11 ? s35 : s37;
+ const SWord8 s39 = s32 ? s27 : s13;
+ const SWord8 s40 = s23 ? s27 : s39;
+ const SWord8 s41 = s14 ? s27 : s40;
+ const SWord8 s42 = s28 ? s39 : s13;
+ const SWord8 s43 = s20 ? s40 : s42;
+ const SWord8 s44 = s11 ? s41 : s43;
+
+ ys[0] = s12;
+ ys[1] = s22;
+ ys[2] = s31;
+ ys[3] = s38;
+ ys[4] = s44;
+}
+== END: "merge.c" ==================
View
6 SBVUnitTest/SBVUnitTest.hs
@@ -35,7 +35,8 @@ import qualified TestSuite.Basics.ProofTests as T02_05(testSuite)
import qualified TestSuite.Basics.QRem as T02_06(testSuite)
import qualified TestSuite.BitPrecise.BitTricks as T03_01(testSuite)
import qualified TestSuite.BitPrecise.Legato as T03_02(testSuite)
-import qualified TestSuite.BitPrecise.PrefixSum as T03_03(testSuite)
+import qualified TestSuite.BitPrecise.MergeSort as T03_03(testSuite)
+import qualified TestSuite.BitPrecise.PrefixSum as T03_04(testSuite)
import qualified TestSuite.CRC.CCITT as T04_01(testSuite)
import qualified TestSuite.CRC.CCITT_Unidir as T04_02(testSuite)
import qualified TestSuite.CRC.GenPoly as T04_03(testSuite)
@@ -77,7 +78,8 @@ testCollection = [
, ("qrem", T02_06.testSuite)
, ("bitTricks", T03_01.testSuite)
, ("legato", T03_02.testSuite)
- , ("prefixSum", T03_03.testSuite)
+ , ("mergeSort", T03_03.testSuite)
+ , ("prefixSum", T03_04.testSuite)
, ("ccitt", T04_01.testSuite)
, ("ccitt2", T04_02.testSuite)
, ("genPoly", T04_03.testSuite)
View
2  SBVUnitTest/SBVUnitTestBuildTime.hs
@@ -2,4 +2,4 @@
module SBVUnitTestBuildTime (buildTime) where
buildTime :: String
-buildTime = "Wed Mar 21 22:17:34 PDT 2012"
+buildTime = "Thu Mar 29 22:11:06 PDT 2012"
View
29 SBVUnitTest/TestSuite/BitPrecise/MergeSort.hs
@@ -0,0 +1,29 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module : TestSuite.BitPrecise.MergeSort
+-- Copyright : (c) Levent Erkok
+-- License : BSD3
+-- Maintainer : erkokl@gmail.com
+-- Stability : experimental
+-- Portability : portable
+--
+-- Test suite for Data.SBV.Examples.BitPrecise.MergeSort
+-----------------------------------------------------------------------------
+
+module TestSuite.BitPrecise.MergeSort where
+
+import Data.SBV
+import Data.SBV.Internals
+import Data.SBV.Examples.BitPrecise.MergeSort
+
+import SBVTest
+
+-- Test suite
+testSuite :: SBVTestSuite
+testSuite = mkTestSuite $ \goldCheck -> test [
+ "mergeSort" ~: mergeC `goldCheck` "merge.gold"
+ ]
+ where mergeC = compileToC' "merge" $ do
+ cgSetDriverValues [10, 6, 4, 82, 71]
+ xs <- cgInputArr 5 "xs"
+ cgOutputArr "ys" (mergeSort xs)
View
1  sbv.cabal
@@ -105,6 +105,7 @@ Library
, Data.SBV.Internals
, Data.SBV.Examples.BitPrecise.BitTricks
, Data.SBV.Examples.BitPrecise.Legato
+ , Data.SBV.Examples.BitPrecise.MergeSort
, Data.SBV.Examples.BitPrecise.PrefixSum
, Data.SBV.Examples.CodeGeneration.AddSub
, Data.SBV.Examples.CodeGeneration.CRC_USB5
Please sign in to comment.
Something went wrong with that request. Please try again.