
   0 | module Main
   1 | 
   2 | import Data.List
   3 | import Data.SOP
   4 | import Data.String
   5 | import Data.Vect
   6 | import Data.SortedSet
   7 | import Hedgehog
   8 | 
   9 | import PriorityQueue
  10 | import PriorityQueue.BinomialQueue
  11 | import PriorityQueue.SkewBinomialQueue
  12 | import PriorityQueue.Bootstrap
  13 | 
  14 | %default total
  15 | 
  16 | fromList' : {q : Type -> Type} -> PriorityQueue q => List Integer -> q Integer
  17 | fromList' is = fromFoldable is
  18 | 
  19 | ||| Lists, of up to length 32, with integers up to 40
  20 | listGen : Gen (List Integer)
  21 | listGen = list (linear 0 32) (integer (constant 0 40))
  22 | 
  23 | sameUniqueElements : (q : Type -> Type) -> PriorityQueue q => Property
  24 | sameUniqueElements q = property $ do
  25 |   input <- forAll listGen
  26 |   let input : SortedSet _ = foldl (\acc, e => insert e acc) empty input
  27 |   let queue : q Integer =
  28 |     foldl (\acc, e => insert e acc) empty input
  29 |   let output : SortedSet _ =
  30 |     foldl (\acc, e => insert e acc) empty $ toList queue
  31 |   input === output
  32 | 
  33 | sortsElements : (q : Type -> Type) -> PriorityQueue q => Property
  34 | sortsElements q = property $ do
  35 |   input <- forAll listGen
  36 |   let queue : q Integer =
  37 |     foldl (\acc, e => insert e acc) empty input
  38 |   let output : List _ =
  39 |     foldr (::) [] $ toList queue
  40 |   (sort input) === output
  41 | 
  42 | emptyTree : (q : Type -> Type) -> PriorityQueue q => Property
  43 | emptyTree q = property $ do
  44 |   let e : q Integer = empty
  45 |   let out = toList e
  46 |   out === []
  47 | 
  48 | emptyNull : (q : Type -> Type) -> PriorityQueue q => Property
  49 | emptyNull q = property $ do
  50 |   let e : q Integer = empty
  51 |   let out = isNull e
  52 |   out === True
  53 | 
  54 | meldSortConcat : (q : Type -> Type) -> PriorityQueue q => Property
  55 | meldSortConcat q = property $ do
  56 |   xs <- forAll listGen
  57 |   ys <- forAll listGen
  58 |   let x : q _ = meld (fromList' xs) (fromList' ys)
  59 |   let y : q _ = fromList' (xs ++ ys)
  60 |   toList x === toList y
  61 | 
  62 | meldSingletons : (q : Type -> Type) -> PriorityQueue q => Property
  63 | meldSingletons q = property $ do
  64 |   xs <- forAll listGen
  65 |   let x : q _ = foldl meld empty . map singleton $ xs
  66 |   let y : q _ = fromList' xs
  67 |   toList x === toList y
  68 | 
  69 | minIsMin : (q : Type -> Type) -> PriorityQueue q => Property
  70 | minIsMin q = property $ do
  71 |   xs <- forAll listGen
  72 |   let x : q _ = fromList' xs
  73 |   findMin x === head' (sort xs)
  74 | 
  75 | deleteRemovesMin : (q : Type -> Type) -> PriorityQueue q => Property
  76 | deleteRemovesMin q = property $ do
  77 |   xs <- forAll listGen
  78 |   let x : q _ = fromList' xs
  79 |   let ys = fromMaybe [] (tail' $ sort xs)
  80 |   let xs = toList (deleteMin x)
  81 |   xs === ys
  82 | 
  83 | lengthCheck : (q : Type -> Type) -> PriorityQueue q => Property
  84 | lengthCheck q = property $ do
  85 |   xs <- forAll listGen
  86 |   let x : q _ = fromList' xs
  87 |   length xs === length x
  88 | 
  89 | all : (q : Type -> Type) -> (name : String) -> PriorityQueue q => Group
  90 | all q name =
  91 |   MkGroup
  92 |     (MkTagged name)
  93 |     [ ("empty: empty -> []", emptyTree q)
  94 |     , ("empty: empty -> null", emptyNull q)
  95 |     , ("length: xs : List x -> pq -> length xs == length pq", lengthCheck q)
  96 |     , ("min: min [a, ...] -> a", minIsMin q)
  97 |     , ("min: deleteMin [a, b, ...] -> [b, ...]", deleteRemovesMin q)
  98 |     , ("insert: SortedSet -> Queue -> SortedSet", sameUniqueElements q)
  99 |     , ("insert: List -> Queue -> Sorted List", sortsElements q)
 100 |     , ("meld: [a] meld [b] -> [a] ++ [b]", meldSortConcat q)
 101 |     , ("meld: foldl meld [a, b, ...] -> fromList' [a, b, ...]", meldSortConcat q)
 102 |     ]
 103 | 
 104 | partial
 105 | main : IO ()
 106 | main =
 107 |   test [ all BinomialQueue "BinomialQueue"
 108 |        , all SkewBinomialQueue "SkewBinomialQueue"
 109 |        , all (Bootstrap SkewBinomialQueue) "Bootstrap SkewBinomialQueue"
 110 |        ]
 111 |