| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Test.StrictCheck.Examples.Map
Description
This module showcases another type of specification different from those in Test.StrictCheck.Examples.Lists. Here, we demonstrate that StrictCheck is able to distinguish value-lazy maps from value-strict maps.
In this module, we first develop the solution of the Knapsack dynamic programming problem by taking the fixpoint of a step function of the solution table. We represent the solution table with a map, and write a specification that is critical for the termination of this solution.
Synopsis
- data Map k v
- type KMap = Map (Int, Int) Int
- pattern Empty' :: Demand (Map (k :: Type) (v :: Type))
- pattern Bin' :: Demand (Map k v) -> Demand k -> Demand v -> Demand (Map k v) -> Demand (Map (k :: Type) (v :: Type))
- replaceThunk :: (Shaped k, Shaped v) => Map k v -> Map k v -> Map k v
- fromList :: [((Int, Int), Int)] -> KMap
- insert :: Ord k => k -> v -> Map k v -> Map k v
- lookup :: KMap -> (Int, Int) -> Maybe Int
- keys :: Map k v -> [k]
- (!) :: KMap -> (Int, Int) -> Int
- weights :: [Int]
- values :: [Int]
- limit :: Int
- solutionStep :: Map (Int, Int) Int -> Map (Int, Int) Int
- solution :: Map (Int, Int) Int
- pattern Pair' :: Demand a -> Demand b -> Demand (a, b)
- iterSolution :: (Int, Int) -> Int -> Map (Int, Int) Int -> Maybe Int
- iterSolutionWithKey :: Key -> Int -> Map (Int, Int) Int -> Maybe Int
- newtype Key = Key {}
- runMapTest :: IO ()
- iterSolution_spec :: Evaluation '[Key, Int, KMap] (Maybe Int) -> Maybe (Int, Int)
Documentation
We roll our own map type to avoid dealing with abstract types.
Instances
type KMap = Map (Int, Int) Int Source #
A specialized map useful for knapsack. The pair of ints represent the two parameters to each knapsack sub-problem solved along the way. These two parameters determine the subsequence of items each sub-problem is concerned with, and the weight limit.
pattern Bin' :: Demand (Map k v) -> Demand k -> Demand v -> Demand (Map k v) -> Demand (Map (k :: Type) (v :: Type)) Source #
replaceThunk :: (Shaped k, Shaped v) => Map k v -> Map k v -> Map k v Source #
This replaces the thunk in a map partial value with the r parameter. This
is very similar to the cap function in the lists example.
insert :: Ord k => k -> v -> Map k v -> Map k v Source #
A simplified insert that ignores rebalancing since rebalancing is not important for the spec we will write.
(!) :: KMap -> (Int, Int) -> Int Source #
A lookup function that returns the default value `0` for keys that are not in the map. This saves us from doing repeated pattern matching when querying the solution table.
Value parameters to the knapsack problem, note that this must be the same
length as weights.
solutionStep :: Map (Int, Int) Int -> Map (Int, Int) Int Source #
One step of the knapsack computation. This is a direct translation from the recurrence relation of the knapsack problem.
solution :: Map (Int, Int) Int Source #
The fixpoint of the recurrence relation, which is also the solution for the knapsack problem.
pattern Pair' :: Demand a -> Demand b -> Demand (a, b) Source #
A pattern synonym for extracting demands of each component from the demand of a pair.
iterSolution :: (Int, Int) -> Int -> Map (Int, Int) Int -> Maybe Int Source #
This function computes the nth pre-fixpoint of the knapsack solution, and looks up the value at the specified cell from the pre-fixpoint.
iterSolutionWithKey :: Key -> Int -> Map (Int, Int) Int -> Maybe Int Source #
This is the same as iterSolution, but uses a newtype wrapper for the
index into the map since we want to write a customized Arbitrary instance
for Key.
The newtype wrapper of index into the knapsack solution table.
Instances
runMapTest :: IO () Source #
This IO action ties the spec together with everything built so far, and runs the StrictCheck randomized testing framework.
iterSolution_spec :: Evaluation '[Key, Int, KMap] (Maybe Int) -> Maybe (Int, Int) Source #
This is the specification that establishes a property important for the
termination of solution: given any pre-fixpoint of `pre-solution`, forcing
the value at pre-solution[i][j] should not induce a demand at the (i, j) cell
of the input that steps to pre-solution, since otherwise this would be an
infinite loop in the fixpoint.
The value-lazy Map defined in this module satisfies this property. However,
if we make this Map value-strict using BangPatterns, StrictCheck will
report a failure when runMapTest is executed.