module Cryptol.Testing.Exhaust where
import qualified Cryptol.Testing.Eval as Eval
import Cryptol.TypeCheck.AST
import Cryptol.Eval.Value
import Control.Applicative((<$>))
import Data.List(genericReplicate)
testableType :: Type -> Maybe (Integer, [[Value]])
testableType ty =
case tNoUser ty of
TCon (TC TCFun) [t1,t2] ->
do sz <- typeSize t1
(tot,vss) <- testableType t2
return (sz * tot, [ v : vs | v <- typeValues t1, vs <- vss ])
TCon (TC TCBit) [] -> return (1, [[]])
_ -> Nothing
runOneTest :: Value -> [Value] -> IO Eval.TestResult
runOneTest = Eval.runOneTest
typeSize :: Type -> Maybe Integer
typeSize ty =
case ty of
TVar _ -> Nothing
TUser _ _ t -> typeSize t
TRec fs -> product <$> mapM (typeSize . snd) fs
TCon (TC tc) ts ->
case (tc, ts) of
(TCNum _, _) -> Nothing
(TCInf, _) -> Nothing
(TCBit, _) -> Just 2
(TCSeq, [sz,el]) -> case tNoUser sz of
TCon (TC (TCNum n)) _ -> (^ n) <$> typeSize el
_ -> Nothing
(TCSeq, _) -> Nothing
(TCFun, _) -> Nothing
(TCTuple _, els) -> product <$> mapM typeSize els
(TCNewtype _, _) -> Nothing
TCon _ _ -> Nothing
typeValues :: Type -> [Value]
typeValues ty =
case ty of
TVar _ -> []
TUser _ _ t -> typeValues t
TRec fs -> [ VRecord xs
| xs <- sequence [ [ (f,v) | v <- typeValues t ]
| (f,t) <- fs ]
]
TCon (TC tc) ts ->
case (tc, ts) of
(TCNum _, _) -> []
(TCInf, _) -> []
(TCBit, _) -> [ VBit False, VBit True ]
(TCSeq, ts1) ->
case map tNoUser ts1 of
[ TCon (TC (TCNum n)) _, TCon (TC TCBit) [] ] ->
[ VWord (BV n x) | x <- [ 0 .. 2^n 1 ] ]
[ TCon (TC (TCNum n)) _, t ] ->
[ VSeq False xs | xs <- sequence $ genericReplicate n
$ typeValues t ]
_ -> []
(TCFun, _) -> []
(TCTuple _, els) -> [ VTuple xs | xs <- sequence (map typeValues els)]
(TCNewtype _, _) -> []
TCon _ _ -> []