{-# LANGUAGE TypeOperators, GADTs #-}
module Test.QuickCheck.Function
  ( Fun(..)
  , apply
  , (:->)
  , FunArbitrary(..)
  , funArbitraryMap
  , funArbitraryShow
  )
 where

--------------------------------------------------------------------------
-- imports

import Test.QuickCheck.Gen
import Test.QuickCheck.Arbitrary
import Test.QuickCheck.Property
import Test.QuickCheck.Poly
import Test.QuickCheck.Modifiers

import Data.Char
import Data.Word

--------------------------------------------------------------------------
-- concrete functions

-- the type of possibly partial concrete functions
data a :-> c where
  Pair  :: (a :-> (b :-> c)) -> ((a,b) :-> c)
  (:+:) :: (a :-> c) -> (b :-> c) -> (Either a b :-> c)
  Unit  :: c -> (() :-> c)
  Nil   :: a :-> c
  Table :: Eq a => [(a,c)] -> (a :-> c)
  Map   :: (a -> b) -> (b -> a) -> (b :-> c) -> (a :-> c)

instance Functor ((:->) a) where
  fmap f (Pair p)    = Pair (fmap (fmap f) p)
  fmap f (p:+:q)     = fmap f p :+: fmap f q
  fmap f (Unit c)    = Unit (f c)
  fmap f Nil         = Nil
  fmap f (Table xys) = Table [ (x,f y) | (x,y) <- xys ]
  fmap f (Map g h p) = Map g h (fmap f p)

instance (Show a, Show b) => Show (a:->b) where
  -- only use this on finite functions
  show p =
    "{" ++ (case table p of
             []        -> ""
             (_,c):xcs -> concat [ show x ++ "->" ++ show c ++ ","
                                 | (x,c) <- xcs
                                 ]
                       ++ "_->" ++ show c)
        ++ "}"
   where
    xcs = table p

-- turning a concrete function into an abstract function (with a default result)
abstract :: (a :-> c) -> c -> (a -> c)
abstract (Pair p)    d (x,y) = abstract (fmap (\q -> abstract q d y) p) d x
abstract (p :+: q)   d exy   = either (abstract p d) (abstract q d) exy
abstract (Unit c)    _ _     = c
abstract Nil         d _     = d
abstract (Table xys) d x     = head ([y | (x',y) <- xys, x == x'] ++ [d])
abstract (Map g _ p) d x     = abstract p d (g x)

-- generating a table from a concrete function
table :: (a :-> c) -> [(a,c)]
table (Pair p)    = [ ((x,y),c) | (x,q) <- table p, (y,c) <- table q ]
table (p :+: q)   = [ (Left x, c) | (x,c) <- table p ]
                 ++ [ (Right y,c) | (y,c) <- table q ]
table (Unit c)    = [ ((), c) ]
table Nil         = []
table (Table xys) = xys
table (Map _ h p) = [ (h x, c) | (x,c) <- table p ]

--------------------------------------------------------------------------
-- FunArbitrary

class FunArbitrary a where
  funArbitrary :: Arbitrary c => Gen (a :-> c)

instance (FunArbitrary a, Arbitrary c) => Arbitrary (a :-> c) where
  arbitrary = funArbitrary
  shrink    = shrinkFun shrink

-- basic instances: pairs, sums, units

instance (FunArbitrary a, FunArbitrary b) => FunArbitrary (a,b) where
  funArbitrary =
    do p <- funArbitrary
       return (Pair p)

instance (FunArbitrary a, FunArbitrary b) => FunArbitrary (Either a b) where
  funArbitrary =
    do p <- funArbitrary
       q <- funArbitrary
       return (p :+: q)

instance FunArbitrary () where
  funArbitrary =
    do c <- arbitrary
       return (Unit c)

instance FunArbitrary Word8 where
  funArbitrary =
    do xys <- sequence [ do y <- arbitrary
                            return (x,y)
                       | x <- [0..255]
                       ]
       return (Table xys)

-- other instances (using Map)

funArbitraryMap :: (FunArbitrary a, Arbitrary c) => (b -> a) -> (a -> b) -> Gen (b :-> c)
funArbitraryMap g h =
  do p <- funArbitrary
     return (Map g h p)

funArbitraryShow :: (Show a, Read a, Arbitrary c) => Gen (a :-> c)
funArbitraryShow = funArbitraryMap show read

instance FunArbitrary a => FunArbitrary [a] where
  funArbitrary = funArbitraryMap g h
   where
    g []     = Left ()
    g (x:xs) = Right (x,xs)

    h (Left _)       = []
    h (Right (x,xs)) = x:xs

instance FunArbitrary a => FunArbitrary (Maybe a) where
  funArbitrary = funArbitraryMap g h
   where
    g Nothing  = Left ()
    g (Just x) = Right x

    h (Left _)  = Nothing
    h (Right x) = Just x

instance FunArbitrary Bool where
  funArbitrary = funArbitraryMap g h
   where
    g False = Left ()
    g True  = Right ()
    
    h (Left _)  = False
    h (Right _) = True

instance FunArbitrary Integer where
  funArbitrary = funArbitraryMap gInteger hInteger
   where
    gInteger n | n < 0     = Left (gNatural (abs n - 1))
               | otherwise = Right (gNatural n)
    
    hInteger (Left ws)  = -(hNatural ws + 1)
    hInteger (Right ws) = hNatural ws
    
    gNatural 0 = []
    gNatural n = (fromIntegral (n `mod` 256) :: Word8) : gNatural (n `div` 256)
    
    hNatural []     = 0
    hNatural (w:ws) = fromIntegral w + 256 * hNatural ws

instance FunArbitrary Int where
  funArbitrary = funArbitraryMap fromIntegral fromInteger

instance FunArbitrary Char where
  funArbitrary = funArbitraryMap ord' chr'
   where
    ord' c = fromIntegral (ord c) :: Word8
    chr' n = chr (fromIntegral n)

-- poly instances

instance FunArbitrary A where
  funArbitrary = funArbitraryMap unA A

instance FunArbitrary B where
  funArbitrary = funArbitraryMap unB B

instance FunArbitrary C where
  funArbitrary = funArbitraryMap unC C

instance FunArbitrary OrdA where
  funArbitrary = funArbitraryMap unOrdA OrdA

instance FunArbitrary OrdB where
  funArbitrary = funArbitraryMap unOrdB OrdB

instance FunArbitrary OrdC where
  funArbitrary = funArbitraryMap unOrdC OrdC

--------------------------------------------------------------------------
-- shrinking

shrinkFun :: (c -> [c]) -> (a :-> c) -> [a :-> c]
shrinkFun shr (Pair p) =
  [ pair p' | p' <- shrinkFun (\q -> shrinkFun shr q) p ]
 where
  pair Nil = Nil
  pair p   = Pair p

shrinkFun shr (p :+: q) =
  [ p .+. Nil | not (isNil q) ] ++
  [ Nil .+. q | not (isNil p) ] ++
  [ p' .+. q  | p' <- shrinkFun shr p ] ++
  [ p  .+. q' | q' <- shrinkFun shr q ]
 where
  isNil :: (a :-> b) -> Bool
  isNil Nil = True
  isNil _   = False
 
  Nil .+. Nil = Nil
  p   .+. q   = p :+: q

shrinkFun shr (Unit c) =
  [ Nil ] ++
  [ Unit c' | c' <- shr c ]

shrinkFun shr (Table xys) =
  [ table xys' | xys' <- shrinkList shrXy xys ]
 where
  shrXy (x,y) = [(x,y') | y' <- shr y]
  
  table []  = Nil
  table xys = Table xys

shrinkFun shr Nil =
  []

shrinkFun shr (Map g h p) =
  [ mapp g h p' | p' <- shrinkFun shr p ]
 where
  mapp g h Nil = Nil
  mapp g h p   = Map g h p

--------------------------------------------------------------------------
-- the Fun modifier

data Fun a b = Fun (a :-> b) (a -> b)

fun :: (a :-> b) -> Fun a b
fun p = Fun p (abstract p (snd (head (table p))))

apply :: Fun a b -> (a -> b)
apply (Fun _ f) = f

instance (Show a, Show b) => Show (Fun a b) where
  show (Fun p _) = show p

instance (FunArbitrary a, Arbitrary b) => Arbitrary (Fun a b) where
  arbitrary = fun `fmap` arbitrary

  shrink (Fun p _) =
    [ fun p' | p' <- shrink p, _:_ <- [table p'] ]

--------------------------------------------------------------------------
-- the end.