-- |
-- Module      :  $Header$
-- Copyright   :  (c) 2013-2015 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
--
-- This module generates random values for Cryptol types.

{-# LANGUAGE BangPatterns #-}
module Cryptol.Testing.Random where

import Cryptol.Eval.Value     (BV(..),Value,GenValue(..))
import qualified Cryptol.Testing.Eval as Eval
import Cryptol.TypeCheck.AST  (Name,Type(..),TCon(..),TC(..),tNoUser)

import Control.Monad          (forM)
import Data.List              (unfoldr, genericTake)
import System.Random          (RandomGen, split, random, randomR)

type Gen g = Int -> g -> (Value, g)


{- | Apply a testable value to some randomly-generated arguments.
     Returns `Nothing` if the function returned `True`, or
     `Just counterexample` if it returned `False`.

    Please note that this function assumes that the generators match
    the supplied value, otherwise we'll panic.
 -}
runOneTest :: RandomGen g
        => Value   -- ^ Function under test
        -> [Gen g] -- ^ Argument generators
        -> Int     -- ^ Size
        -> g
        -> IO (Eval.TestResult, g)
runOneTest fun argGens sz g0 = do
  let (args, g1) = foldr mkArg ([], g0) argGens
      mkArg argGen (as, g) = let (a, g') = argGen sz g in (a:as, g')
  result <- Eval.runOneTest fun args
  return (result, g1)

{- | Given a (function) type, compute generators for
the function's arguments. Currently we do not support polymorphic functions.
In principle, we could apply these to random types, and test the results. -}
testableType :: RandomGen g => Type -> Maybe [Gen g]
testableType ty =
  case tNoUser ty of
    TCon (TC TCFun) [t1,t2] ->
      do g  <- randomValue t1
         as <- testableType t2
         return (g : as)
    TCon (TC TCBit) [] -> return []
    _ -> Nothing


{- | A generator for values of the given type.  This fails if we are
given a type that lacks a suitable random value generator. -}
randomValue :: RandomGen g => Type -> Maybe (Gen g)
randomValue ty =
  case ty of
    TCon tc ts  ->
      case (tc, map tNoUser ts) of
        (TC TCBit, [])                        -> Just randomBit

        (TC TCSeq, [TCon (TC TCInf) [], el])  ->
          do mk <- randomValue el
             return (randomStream mk)

        (TC TCSeq, [TCon (TC (TCNum n)) [], TCon (TC TCBit) []]) ->
            return (randomWord n)

        (TC TCSeq, [TCon (TC (TCNum n)) [], el]) ->
          do mk <- randomValue el
             return (randomSequence n mk)

        (TC (TCTuple _), els) ->
          do mks <- mapM randomValue els
             return (randomTuple mks)

        _ -> Nothing

    TVar _      -> Nothing
    TUser _ _ t -> randomValue t
    TRec fs     -> do gs <- forM fs $ \(l,t) -> do g <- randomValue t
                                                   return (l,g)
                      return (randomRecord gs)

-- | Generate a random bit value.
randomBit :: RandomGen g => Gen g
randomBit _ g =
  let (b,g1) = random g
  in (VBit b, g1)

-- | Generate a random word of the given length (i.e., a value of type @[w]@)
-- The size parameter is assumed to vary between 1 and 100, and we use
-- it to generate smaller numbers first.
randomWord :: RandomGen g => Integer -> Gen g
randomWord w _sz g =
   let (val, g1) = randomR (0,2^w-1) g
   in (VWord (BV w val), g1)

-- | Generate a random infinite stream value.
randomStream :: RandomGen g => Gen g -> Gen g
randomStream mkElem sz g =
  let (g1,g2) = split g
  in (VStream (unfoldr (Just . mkElem sz) g1), g2)

{- | Generate a random sequence.  Generally, this should be used for sequences
other than bits.  For sequences of bits use "randomWord".  The difference
is mostly about how the results will be displayed. -}
randomSequence :: RandomGen g => Integer -> Gen g -> Gen g
randomSequence w mkElem sz g =
  let (g1,g2) = split g
  in (VSeq False $ genericTake w $ unfoldr (Just . mkElem sz) g1 , g2)

-- | Generate a random tuple value.
randomTuple :: RandomGen g => [Gen g] -> Gen g
randomTuple gens sz = go [] gens
  where
  go els [] g = (VTuple (reverse els), g)
  go els (mkElem : more) g =
    let (v, g1) = mkElem sz g
    in go (v : els) more g1

-- | Generate a random record value.
randomRecord :: RandomGen g => [(Name, Gen g)] -> Gen g
randomRecord gens sz = go [] gens
  where
  go els [] g = (VRecord (reverse els), g)
  go els ((l,mkElem) : more) g =
    let (v, g1) = mkElem sz g
    in go ((l,v) : els) more g1

{-
test = do
  g <- newStdGen
  let (s,_) = randomSequence 100 (randomWord 256) 100 g
  print $ ppValue defaultPPOpts { useBase = 16 } s
-}