module Control.Concurrent.CHPSpec.LazySmallCheck
( Serial(series)
, Series
, Cons
, cons
, (><)
, (\/)
, drawnFrom
, cons0
, cons1
, cons2
, cons3
, cons4
, cons5
, fuzz
)
where
import Control.Applicative ((<$>))
import Control.Arrow
import Control.Exception
import Control.Monad.State
infixr 3 \/
infixl 4 ><
type Pos = [Int]
data Term = Var Pos Type | Ctr Int [Term]
data Type = SumOfProd [[Type]]
type Series a = Int -> Cons a
data Cons a = C Type ([[Term] -> a]) Bool
class Serial a where
series :: Series a
cons :: a -> Series a
cons a d = C (SumOfProd [[]]) [const a] True
(><) :: Series (a -> b) -> Series a -> Series b
(f >< a) d = C (SumOfProd [ta:p | shallow, p <- ps]) cs (shallow && fComplete && aComplete)
where
C (SumOfProd ps) cfs fComplete = f d
C ta cas aComplete = a (d1)
cs = [\(x:xs) -> cf xs (conv cas x) | shallow, cf <- cfs]
shallow = d > 0 && nonEmpty ta
nonEmpty :: Type -> Bool
nonEmpty (SumOfProd ps) = not (null ps)
(\/) :: Series a -> Series a -> Series a
(a \/ b) d = C (SumOfProd (ssa ++ ssb)) (ca ++ cb) (aComplete && bComplete)
where
C (SumOfProd ssa) ca aComplete = a d
C (SumOfProd ssb) cb bComplete = b d
conv :: [[Term] -> a] -> Term -> a
conv cs (Var p _) = error ('\0':map toEnum p)
conv cs (Ctr i xs) = (cs !! i) xs
drawnFrom :: [a] -> Cons a
drawnFrom xs = C (SumOfProd (map (const []) xs)) (map const xs) False
cons0 :: a -> Series a
cons0 f = cons f
cons1 :: Serial a => (a -> b) -> Series b
cons1 f = cons f >< series
cons2 :: (Serial a, Serial b) => (a -> b -> c) -> Series c
cons2 f = cons f >< series >< series
cons3 :: (Serial a, Serial b, Serial c) => (a -> b -> c -> d) -> Series d
cons3 f = cons f >< series >< series >< series
cons4 :: (Serial a, Serial b, Serial c, Serial d) =>
(a -> b -> c -> d -> e) -> Series e
cons4 f = cons f >< series >< series >< series >< series
cons5 :: (Serial a, Serial b, Serial c, Serial d, Serial e) =>
(a -> b -> c -> d -> e -> f) -> Series f
cons5 f = cons f >< series >< series >< series >< series >< series
instance Serial () where
series = cons0 ()
instance Serial Bool where
series = cons0 False \/ cons0 True
instance Serial a => Serial (Maybe a) where
series = cons0 Nothing \/ cons1 Just
instance (Serial a, Serial b) => Serial (Either a b) where
series = cons1 Left \/ cons1 Right
instance Serial a => Serial [a] where
series = cons0 [] \/ cons2 (:)
instance (Serial a, Serial b) => Serial (a, b) where
series = cons2 (,) . (+1)
instance (Serial a, Serial b, Serial c) => Serial (a, b, c) where
series = cons3 (,,) . (+1)
instance (Serial a, Serial b, Serial c, Serial d) =>
Serial (a, b, c, d) where
series = cons4 (,,,) . (+1)
instance (Serial a, Serial b, Serial c, Serial d, Serial e) =>
Serial (a, b, c, d, e) where
series = cons5 (,,,,) . (+1)
instance Serial Int where
series d = drawnFrom [d..d]
instance Serial Integer where
series d = drawnFrom (map toInteger [d..d])
instance Serial Char where
series d = drawnFrom (take (d+1) ['a'..])
instance Serial Float where
series d = drawnFrom (floats d)
instance Serial Double where
series d = drawnFrom (floats d)
floats :: RealFloat a => Int -> [a]
floats d = [ encodeFloat sig exp
| sig <- map toInteger [d..d]
, exp <- [d..d]
, odd sig || sig == 0 && exp == 0
]
refine :: Term -> Pos -> [Term]
refine (Var p (SumOfProd ss)) [] = new p ss
refine (Ctr c xs) p = map (Ctr c) (refineList xs p)
refineList :: [Term] -> Pos -> [[Term]]
refineList xs (i:is) = [ls ++ y:rs | y <- refine x is]
where (ls, x:rs) = splitAt i xs
new :: Pos -> [[Type]] -> [Term]
new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
| (c, ts) <- zip [0..] ps ]
total :: Term -> [Term]
total val = tot val
where
tot (Ctr c xs) = [Ctr c ys | ys <- mapM tot xs]
tot (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- tot x]
answer :: IO a -> (a -> IO b) -> (Pos -> IO b) -> IO b
answer a known unknown =
do res <- try a
case res of
Right b -> known b
Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
Left e -> throw e
resultVal :: forall b s. Result s b -> StateT s IO ([b], Bool)
resultVal r = ref (args r)
where
ref :: [Term] -> StateT s IO ([b], Bool)
ref xs = StateT $ \s -> answer (flip runStateT s $ apply r xs) (\(x, s) -> return (([x], complete r), s)) (unknown s)
where
unknown :: s -> Pos -> IO (([b], Bool), s)
unknown s p = (first $ (concat *** and) . unzip) <$> (flip runStateT s $ mapM ref (refineList xs p))
data Result s b =
Result { args :: [Term]
, apply :: [Term] -> StateT s IO b
, complete :: Bool
}
runEnd :: ([Term] -> StateT s IO r) -> Int -> Int -> Result s r
runEnd f _ _ = Result [] (f . reverse) True
runParam :: Serial a => ([Term] -> a -> StateT s IO r) -> Int -> Int -> Result s r
runParam f n d =
let C t c comp = series d
c' = conv c
r = runEnd (\(x:xs) -> f xs (c' x)) (n+1) d
in r { args = Var [n] t : args r, complete = complete r && comp }
depthCheck :: Serial a => Int -> (a -> StateT s IO r) -> StateT s IO ([r], Bool)
depthCheck d p = resultVal $ runParam (const p) 0 d
smallCheck :: Serial a => Int -> (a -> StateT s IO r) -> StateT s IO ([r], Bool)
smallCheck d p = smallCheck' [] 0
where
smallCheck' prev n
| n <= d = do (xs, comp) <- depthCheck n p
if comp
then return (xs, True)
else smallCheck' xs (succ n)
| otherwise = return (prev, False)
fuzz :: (Serial a) => (a -> StateT s IO b) -> StateT s IO ([b], Bool)
fuzz = smallCheck 10