---------------------------------------------------------------------
--
--  Haskell: The Craft of Functional Programming, 3e
--  Simon Thompson
--  (c) Addison-Wesley, 1996-2011.
-- 
--  Chapter 9
--
---------------------------------------------------------------------

-- Reasoning about programs
-- ^^^^^^^^^^^^^^^^^^^^^^^^

module Chapter9 where

import Prelude hiding (sum,length,(++),reverse,unzip)
import Test.QuickCheck


-- Testing and verification
-- ^^^^^^^^^^^^^^^^^^^^^^^^
-- A function supposed to give the maximum of three (integer) values.

mysteryMax :: Integer -> Integer -> Integer -> Integer
mysteryMax :: Integer -> Integer -> Integer -> Integer
mysteryMax Integer
x Integer
y Integer
z
  | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
y Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
z      = Integer
x
  | Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
x Bool -> Bool -> Bool
&& Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
z      = Integer
y
  | Bool
otherwise           = Integer
z

prop_mystery :: Integer -> Integer -> Integer -> Bool

prop_mystery :: Integer -> Integer -> Integer -> Bool
prop_mystery Integer
x Integer
y Integer
z =
    Integer -> Integer -> Integer -> Integer
mysteryMax Integer
x Integer
y Integer
z Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer
x Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
`max` Integer
y) Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
`max` Integer
z

-- Definedness and termination
-- ^^^^^^^^^^^^^^^^^^^^^^^^^^^

-- A factorial function, giving an undefined result on negative integers.

fact :: Integer -> Integer
fact :: Integer -> Integer
fact Integer
n
  | Integer
nInteger -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
==Integer
0        = Integer
1
  | Bool
otherwise   = Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer -> Integer
fact (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)

-- An infinite list

posInts :: [Integer]
posInts :: [Integer]
posInts = [Integer
1, Integer
2 .. ]


-- Induction
-- ^^^^^^^^^

-- The sum function, defined recursively.

sum :: [Integer] -> Integer

sum :: [Integer] -> Integer
sum []     = Integer
0                  -- (sum.1)
sum (Integer
x:[Integer]
xs) = Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ [Integer] -> Integer
sum [Integer]
xs             -- (sum.2)

-- Double every element of an integer list.

doubleAll :: [Integer] -> [Integer]

doubleAll :: [Integer] -> [Integer]
doubleAll []     = []               -- (doubleAll.1)
doubleAll (Integer
z:[Integer]
zs) = Integer
2Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
z Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer] -> [Integer]
doubleAll [Integer]
zs       -- (doubleAll.2)

-- The property linking the two:
--  sum (doubleAll xs) = 2 * sum xs         -- (sum+dblAll)

prop_SumDoubleAll :: [Integer] -> Bool

prop_SumDoubleAll :: [Integer] -> Bool
prop_SumDoubleAll [Integer]
xs =
    [Integer] -> Integer
sum ([Integer] -> [Integer]
doubleAll [Integer]
xs) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* [Integer] -> Integer
sum [Integer]
xs

-- Other functions used in the examples
-- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

-- The definitions given here use explicit recursion, rather than applying 
-- higher-order functions as may happen in the Prelude definitions.

length :: [a] -> Int

length :: forall a. [a] -> Int
length []     = Int
0               -- (length.1)
length (a
z:[a]
zs) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [a] -> Int
forall a. [a] -> Int
length [a]
zs           -- (length.2)
 
(++) :: [a] -> [a] -> [a]

[]     ++ :: forall a. [a] -> [a] -> [a]
++ [a]
zs = [a]
zs               -- (++.1)
(a
w:[a]
ws) ++ [a]
zs = a
wa -> [a] -> [a]
forall a. a -> [a] -> [a]
:([a]
ws[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++[a]
zs)           -- (++.2)

-- QuickCheck property

prop_lengthPlusPlus :: [a] -> [a] -> Bool

prop_lengthPlusPlus :: forall a. [a] -> [a] -> Bool
prop_lengthPlusPlus [a]
xs [a]
ys =
    [a] -> Int
forall a. [a] -> Int
length ([a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
ys) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> Int
forall a. [a] -> Int
length [a]
xs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [a] -> Int
forall a. [a] -> Int
length [a]
ys

reverse :: [a] -> [a]

reverse :: forall a. [a] -> [a]
reverse []     = []             -- (reverse.1)
reverse (a
z:[a]
zs) = [a] -> [a]
forall a. [a] -> [a]
reverse [a]
zs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
z]      -- (reverse.2)

-- QuickCheck properties
-- Why does prop_reversePlusPlus' not fail?  Because a defaults to ().
-- See note on "QuickCheck and properties over [a]" at the end of 
-- Section 9.6.

prop_reversePlusPlus' :: Eq a => [a] -> [a] -> Bool

prop_reversePlusPlus' :: forall a. Eq a => [a] -> [a] -> Bool
prop_reversePlusPlus' [a]
xs [a]
ys =
    [a] -> [a]
forall a. [a] -> [a]
reverse ([a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
ys) [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> [a]
forall a. [a] -> [a]
reverse [a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a] -> [a]
forall a. [a] -> [a]
reverse [a]
ys

-- The "right" property here.

prop_reversePlusPlusOops :: [Integer] -> [Integer] -> Bool

prop_reversePlusPlusOops :: [Integer] -> [Integer] -> Bool
prop_reversePlusPlusOops [Integer]
xs [Integer]
ys =
    [Integer] -> [Integer]
forall a. [a] -> [a]
reverse ([Integer]
xs [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
++ [Integer]
ys) [Integer] -> [Integer] -> Bool
forall a. Eq a => a -> a -> Bool
== [Integer] -> [Integer]
forall a. [a] -> [a]
reverse [Integer]
xs [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
++ [Integer] -> [Integer]
forall a. [a] -> [a]
reverse [Integer]
ys

-- The "right" property here.

prop_reversePlusPlus :: [Integer] -> [Integer] -> Bool

prop_reversePlusPlus :: [Integer] -> [Integer] -> Bool
prop_reversePlusPlus [Integer]
xs [Integer]
ys =
    [Integer] -> [Integer]
forall a. [a] -> [a]
reverse ([Integer]
xs [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
++ [Integer]
ys) [Integer] -> [Integer] -> Bool
forall a. Eq a => a -> a -> Bool
== [Integer] -> [Integer]
forall a. [a] -> [a]
reverse [Integer]
ys [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
++ [Integer] -> [Integer]
forall a. [a] -> [a]
reverse [Integer]
xs

-- Associativity of ++

prop_assocPlusPlus :: [Integer] -> [Integer] -> [Integer] -> Bool

prop_assocPlusPlus :: [Integer] -> [Integer] -> [Integer] -> Bool
prop_assocPlusPlus [Integer]
xs [Integer]
ys [Integer]
zs =
     ([Integer]
xs [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
++ [Integer]
ys) [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
++ [Integer]
zs [Integer] -> [Integer] -> Bool
forall a. Eq a => a -> a -> Bool
== [Integer]
xs [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
++ ([Integer]
ys [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
++ [Integer]
zs)



unzip :: [(a,b)] -> ([a],[b])

unzip :: forall a b. [(a, b)] -> ([a], [b])
unzip [] = ([],[])
unzip ((a
x,b
y):[(a, b)]
ps) 
  = (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs,b
yb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
ys)
    where
    ([a]
xs,[b]
ys) = [(a, b)] -> ([a], [b])
forall a b. [(a, b)] -> ([a], [b])
unzip [(a, b)]
ps                   


-- Generalizing the proof goal
-- ^^^^^^^^^^^^^^^^^^^^^^^^^^^

-- The shunting function

shunt :: [a] -> [a] -> [a]

shunt :: forall a. [a] -> [a] -> [a]
shunt []     [a]
ys = [a]
ys                -- (shunt.1)
shunt (a
x:[a]
xs) [a]
ys = [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
shunt [a]
xs (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys)       -- (shunt.2)

-- QuickCheck property of shunt.

prop_shunt :: [Integer] -> [Integer] -> Bool

prop_shunt :: [Integer] -> [Integer] -> Bool
prop_shunt [Integer]
xs [Integer]
zs =
    [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
shunt ([Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
shunt [Integer]
xs [Integer]
zs) [] [Integer] -> [Integer] -> Bool
forall a. Eq a => a -> a -> Bool
== [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
shunt [Integer]
zs [Integer]
xs

-- Alternative reverse.

rev :: [a] -> [a]

rev :: forall a. [a] -> [a]
rev [a]
xs = [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
shunt [a]
xs []                -- (rev.1)

-- Do they always match?

prop_reverses :: [Integer] -> Bool

prop_reverses :: [Integer] -> Bool
prop_reverses [Integer]
xs =
    [Integer] -> [Integer]
forall a. [a] -> [a]
reverse [Integer]
xs [Integer] -> [Integer] -> Bool
forall a. Eq a => a -> a -> Bool
== [Integer] -> [Integer]
forall a. [a] -> [a]
rev [Integer]
xs

-- An alternative definition of the factorial function.

fac2 :: Integer -> Integer

fac2 :: Integer -> Integer
fac2 Integer
n = Integer -> Integer -> Integer
facAux Integer
n Integer
1

facAux :: Integer -> Integer -> Integer

facAux :: Integer -> Integer -> Integer
facAux Integer
0 Integer
p = Integer
p
facAux Integer
n Integer
p = Integer -> Integer -> Integer
facAux (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
p)

-- QuickChecking the two factorials:

prop_facs' :: Integer -> Bool

prop_facs' :: Integer -> Bool
prop_facs' Integer
x =
    Integer -> Integer
fact Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Integer
fac2 Integer
x 

prop_facs :: Integer -> Bool

prop_facs :: Integer -> Bool
prop_facs Integer
x =
    (Integer
xInteger -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<Integer
0) Bool -> Bool -> Bool
|| Integer -> Integer
fact Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Integer
fac2 Integer
x