    -- |
    -- Module      :  $Header$
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE RecordWildCards #-}
    module Cryptol.Testing.Concrete where

    import Cryptol.Eval.Error
    import Cryptol.Eval.Value
    import Cryptol.TypeCheck.AST
    import Cryptol.Utils.Panic (panic)

    import qualified Control.Exception as X
    import Data.List(genericReplicate)

    import Prelude ()
    import Prelude.Compat

    -- | A test result is either a pass, a failure due to evaluating to
    -- @False@, or a failure due to an exception raised during evaluation
    data TestResult
      = Pass
      | FailFalse [Value]
      | FailError EvalError [Value]

    isPass :: TestResult -> Bool
    isPass Pass = True
    isPass _    = False

    -- | Apply a testable value to some arguments.
    -- Note that this function assumes that the values come from a call to
    -- `testableType` (i.e., things are type-correct). We run in the IO
    -- monad in order to catch any @EvalError@s.
    runOneTest :: Value -> [Value] -> IO TestResult
    runOneTest v0 vs0 = run `X.catch` handle
      where
        run = do
          result <- X.evaluate (go v0 vs0)
          if result
            then return Pass
            else return (FailFalse vs0)
        handle e = return (FailError e vs0)

        go :: Value -> [Value] -> Bool
        go (VFun f) (v : vs) = go (f v) vs
        go (VFun _) []       = panic "Not enough arguments while applying function"
                               []
        go (VBit b) []       = b
        go v vs              = panic "Type error while running test" $
                               [ "Function:"
                               , show $ ppValue defaultPPOpts v
                               , "Arguments:"
                               ] ++ map (show . ppValue defaultPPOpts) vs

    {- | Given a (function) type, compute all possible inputs for it.
    We also return the total number of test (i.e., the length of the outer list. -}
    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

    {- | Given a fully-evaluated type, try to compute the number of values in it.
    Returns `Nothing` for infinite types, user-defined types, polymorhic types,
    and, currently, function spaces.  Of course, we can easily compute the
    sizes of function spaces, but we can't easily enumerate their inhabitants. -}
    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

    {- | Returns all the values in a type.  Returns an empty list of values,
    for types where 'typeSize' returned '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, _)       -> []  -- We don't generate function values.
            (TCTuple _, els) -> [ VTuple xs | xs <- sequence (map typeValues els)]
            (TCNewtype _, _) -> []

        TCon _ _ -> []

    --------------------------------------------------------------------------------
    -- Driver function

    data TestSpec m s = TestSpec {
        testFn :: Integer -> s -> m (TestResult, s)
      , testProp :: String -- ^ The property as entered by the user
      , testTotal :: Integer
      , testPossible :: Integer
      , testRptProgress :: Integer -> Integer -> m ()
      , testClrProgress :: m ()
      , testRptFailure :: TestResult -> m ()
      , testRptSuccess :: m ()
      }

    data TestReport = TestReport {
        reportResult :: TestResult
      , reportProp :: String -- ^ The property as entered by the user
      , reportTestsRun :: Integer
      , reportTestsPossible :: Integer
      }

    runTests :: Monad m => TestSpec m s -> s -> m TestReport
    runTests TestSpec {..} st0 = go 0 st0
      where
      go testNum _ | testNum >= testTotal = do
        testRptSuccess
        return $ TestReport Pass testProp testNum testPossible
      go testNum st =
       do testRptProgress testNum testTotal
          res <- testFn (div (100 * (1 + testNum)) testTotal) st
          testClrProgress
          case res of
            (Pass, st') -> do -- delProgress -- unnecessary?
              go (testNum + 1) st'
            (failure, _st') -> do
              testRptFailure failure
              return $ TestReport failure testProp testNum testPossible