--- QuickCheck properties that are supposed to hold
-
-{-
-type Bag a = [a]
-
-(=~) :: Ord a => Bag a -> Bag a -> Bool
-xs =~ ys = sort xs == sort ys
-
-prop_Get_Nil =
- readP_to_S get [] =~ []
-
-prop_Get_Cons c s =
- readP_to_S get (c:s) =~ [(c,s)]
-
-prop_Look s =
- readP_to_S look s =~ [(s,s)]
-
-prop_Fail s =
- readP_to_S pfail s =~ ([] :: Bag (Int,String))
-
-prop_Return x s =
- readP_to_S (return x) s =~ ([(x,s)] :: Bag (Int,String))
-
-prop_ReadS r s =
- readP_to_S (readS_to_P r) s =~ (r s :: Bag (Int,String))
-
-prop_Bind p k s =
- readP_to_S ((p :: ReadP Int) >>= k) s =~
- ([ ys'' | (x,s') <- readP_to_S p s, ys'' <- readP_to_S (k x) s' ]
- :: Bag (Int,String)
- )
-
-prop_Plus p q s =
- readP_to_S ((p :: ReadP Int) +++ q) s =~
- (readP_to_S p s ++ readP_to_S q s)
-
-prop_LeftPlus p q s =
- readP_to_S ((p :: ReadP Int) <++ q) s =~
- (readP_to_S p s +<+ readP_to_S q s)
- where
- [] +<+ ys = ys
- xs +<+ _ = xs
+-- QuickCheck properties that hold for the combinators
+
+{- $properties
+The following are QuickCheck specifications of what the combinators do.
+These can be seen as formal specifications of the behavior of the
+combinators.
+
+We use bags to give semantics to the combinators.
+@
+ type Bag a = [a]
+@
+Equality on bags does not care about the order of elements.
+@
+ (=~) :: Ord a => Bag a -> Bag a -> Bool
+ xs =~ ys = sort xs == sort ys
+@
+A special equality operator to avoid unresolved overloading
+when testing the properties.
+@
+ (=~.) :: Bag (Int,String) -> Bag (Int,String) -> Bool
+ (=~.) = (=~)
+@
+Here follow the properties:
+@
+ prop_Get_Nil =
+ readP_to_S get [] =~ []
+
+ prop_Get_Cons c s =
+ readP_to_S get (c:s) =~ [(c,s)]
+
+ prop_Look s =
+ readP_to_S look s =~ [(s,s)]
+
+ prop_Fail s =
+ readP_to_S pfail s =~. []
+
+ prop_Return x s =
+ readP_to_S (return x) s =~. [(x,s)]
+
+ prop_Bind p k s =
+ readP_to_S (p >>= k) s =~.
+ [ ys''
+ | (x,s') <- readP_to_S p s
+ , ys'' <- readP_to_S (k (x::Int)) s'
+ ]
+
+ prop_Plus p q s =
+ readP_to_S (p +++ q) s =~.
+ (readP_to_S p s ++ readP_to_S q s)
+
+ prop_LeftPlus p q s =
+ readP_to_S (p <++ q) s =~.
+ (readP_to_S p s +<+ readP_to_S q s)
+ where
+ [] +<+ ys = ys
+ xs +<+ _ = xs
+
+ prop_Gather s =
+ forAll readPWithoutReadS $ \p ->
+ readP_to_S (gather p) s =~
+ [ ((pre,x::Int),s')
+ | (x,s') <- readP_to_S p s
+ , let pre = take (length s - length s') s
+ ]
+
+ prop_String_Yes this s =
+ readP_to_S (string this) (this ++ s) =~
+ [(this,s)]
+
+ prop_String_Maybe this s =
+ readP_to_S (string this) s =~
+ [(this, drop (length this) s) | this `isPrefixOf` s]
+
+ prop_Munch p s =
+ readP_to_S (munch p) s =~
+ [(takeWhile p s, dropWhile p s)]
+
+ prop_Munch1 p s =
+ readP_to_S (munch1 p) s =~
+ [(res,s') | let (res,s') = (takeWhile p s, dropWhile p s), not (null res)]
+
+ prop_Choice ps s =
+ readP_to_S (choice ps) s =~.
+ readP_to_S (foldr (+++) pfail ps) s
+
+ prop_ReadS r s =
+ readP_to_S (readS_to_P r) s =~. r s
+@