{-# LANGUAGE NoImplicitPrelude #-}

-- |

-- Module      : OAlg.Control.Validate

-- Description : a tool kit for automatic testing

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- Validation of 'Statement's, based on a stochastic approach.

-- 

-- __Example__ Deterministic statements

-- 

-- >>> validate (SValid && (SInvalid || SValid))

-- Valid

-- 

-- The validation shows the following output:

-- 

-- @

-- >> Omega (StdGen {unStdGen = SMGen 1872899651221430933 9051984386581193015})

-- >> --------------------------------------------------------------------------------

-- >> Summary

-- >> 1 sample tested where 0 tests are false, having 0 denied premises

-- >> 5 tests with a false ratio of 0% and a denied premises ratio of 0%

-- @

-- 

-- From the third line on the number of samples is shown and how many tests over all have been

-- performed to determine the result.

-- As the above statement is obviously deterministic, only one sample has been tested, as the result

-- is independent of the used stochastic.

-- 

--  __Example__ Non deterministic statements

-- 

-- >>> validate (Forall (xIntB 0 100) (\i -> (i <= 100) :?> Params["i":=show i]))

-- ProbablyValid

-- 

-- The validation shows the following output:

-- 

-- @

-- >> Omega (StdGen {unStdGen = SMGen 8429292192981378265 11527977991108410805})

-- >> --------------------------------------------------------------------------------

-- >> Summary

-- >> 10 samples tested where 0 tests are false, having 0 denied premises

-- >> 94 tests with a false ratio of 0% and a denied premises ratio of 

-- @

-- 

-- As this statement is non deterministic, the validation of it pics randomly 10 samples of

-- 'Omega's and 'Wide's (see the number of samples in the summery above) - starting from the shown

-- 'Omega' - and uses 'validateStoch' to determine for each sample the result. All this results are

-- combined with the '&&'-operator to yield the final result.

-- 

-- __Example__ Lazy validation

-- 

-- >>> validate (SValid || throw DivideByZero)

-- Valid

-- 

-- __Example__ Denied premises

--

-- >>> let s = Forall xInt (\i -> (i == i+1):?>Params["i":=show i]) in validate (s :=> s)

-- Valid

-- 

-- The validation shows the following output:

-- 

-- @

-- >> Omega (StdGen {unStdGen = SMGen 1872899651221430933 9051984386581193015})

-- >> --------------------------------------------------------------------------------

-- >> Summary

-- >> 1 sample tested where 0 tests are false, having 4 denied premises

-- >> 7 tests with a false ratio of 0% and a denied premises ratio of 57%

-- @

-- 

-- The statement @s@ is obviously invalid but the tautology @s ':=>' s@ is valid because of denied

-- premises, which is shown in the summery.

-- 

-- __Example__ Invalid statements

-- 

-- >>> validate (Forall (xIntB 0 10) (\i -> (10 < i):?>Params["i":=show i]))

-- Invalid

-- 

-- The validation shows the following output:

-- 

-- @

-- >> Omega (StdGen {unStdGen = SMGen 8429292192981378265 11527977991108410805})

-- >> --------------------------------------------------------------------------------

-- for all Invalid

--   and Invalid

--     check Invalid

--       Invalid

--       parameters

--         i := 9

-- 

-- >> --------------------------------------------------------------------------------

-- >> Summary

-- >> 1 sample tested where 3 tests are false, having 0 denied premises

-- >> 3 tests with a false ratio of 100% and a denied premises ratio of 0%

-- @

-- 

-- where from the third line on the invalid test is shown and the summery shows that in the first

-- sample for 'Omega' and 'Wide' an invalid test has been found.

-- 

--  __Example__ Tracking of exceptions

-- 

-- >>> validate (SValid && (Label "bad" :<=>: throw DivideByZero))

-- *** Exception: FailedStatement divide by zero

-- 

-- The validation shows the following output:

-- 

-- @

-- >> Omega (StdGen {unStdGen = SMGen 3069986384088197145 15225250911862971905})

-- >> --------------------------------------------------------------------------------

-- >> failed sample

-- and divide by zero

--   (bad) divide by zero

--     failure divide by zero

-- 

-- >> --------------------------------------------------------------------------------

-- >> Summary

-- >> 1 sample tested where 0 tests are false, having 0 denied premises

-- >> 3 tests

-- @

-- 

-- The failed sample part of the output shows that in an /and/ construct the component - labeled by

-- @bad@ - has been throwing an exception during the validation process.

-- 

-- __Example__ Extended stochastic

-- 

-- If we validate the obviously false statement

-- 

-- >> validate Forall (xIntB 0 1000) (\i -> (i < 1000) :?> Params["i":=show i])

-- 

-- the validation may nevertheless yield 'ProbablyValid' - because all randomly picked 'Omega's

-- and 'Wide's may produce only values which are strict smaller then @1000@. To overcome this

-- /problem/ and to get more confidence of the result it is possible to adapt the stochastic and use

-- @'validateStochastic' 'Massive'@ instead ('validate' is equivalent to

-- @'validateStochastic' 'Sparse'@).

-- 

-- __Note__ The here defined validation is highly inspired by the QuickCheck package. But we have

-- chosen to adopt the idea to fit more our needs. For example, if a statement throws an exception,

-- then the occurrence can be tracked. Also we devoted special attention to the logic of statements

-- (as 'Statement' is an instance 'Boolean', they fulfill all the logical tautologies). For example,

-- the simple tautology @s ':=>' s@ breaks, if you don't take special care during the validating

-- process or if you allow user interactions.

module OAlg.Control.Validate
  (
    validate, validate'

  , validateStochastic, Stochastic(..)
  , validateStatistics
  , validateWith, Cnfg(..), Result(..), stdCnf, stdStc

  )
  where

import Prelude(Enum(..),Bounded,seq,Int,Integer,Double,Num(..),Fractional(..))
import Control.Monad
import Control.Exception
import System.IO (IO,hFlush,stdout,putStrLn)

import Data.Time
import Data.Time.Clock.System
import Data.Time.Clock.TAI

import Data.List (take,dropWhile,(++),reverse,map)

import OAlg.Category.Definition

import OAlg.Control.Verbose
import OAlg.Control.HNFData

import OAlg.Data.Identity
import OAlg.Data.Logical
import OAlg.Data.Ord
import OAlg.Data.Statement

import OAlg.Data.Boolean
import OAlg.Data.Equal
import OAlg.Data.X
import OAlg.Data.Maybe
import OAlg.Data.Show
import OAlg.Data.Statistics

data ValidateException
  = FailedStatement SomeException
  deriving Int -> ValidateException -> ShowS
[ValidateException] -> ShowS
ValidateException -> String
(Int -> ValidateException -> ShowS)
-> (ValidateException -> String)
-> ([ValidateException] -> ShowS)
-> Show ValidateException
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ValidateException -> ShowS
showsPrec :: Int -> ValidateException -> ShowS
$cshow :: ValidateException -> String
show :: ValidateException -> String
$cshowList :: [ValidateException] -> ShowS
showList :: [ValidateException] -> ShowS
Show

instance Exception ValidateException

--------------------------------------------------------------------------------

-- Stochastic -


-- | defines the stochastic behavior of 'validateStochastic'.

data Stochastic
  = Sparse 
  | Standard
  | Massive
  deriving (Int -> Stochastic -> ShowS
[Stochastic] -> ShowS
Stochastic -> String
(Int -> Stochastic -> ShowS)
-> (Stochastic -> String)
-> ([Stochastic] -> ShowS)
-> Show Stochastic
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Stochastic -> ShowS
showsPrec :: Int -> Stochastic -> ShowS
$cshow :: Stochastic -> String
show :: Stochastic -> String
$cshowList :: [Stochastic] -> ShowS
showList :: [Stochastic] -> ShowS
Show,ReadPrec [Stochastic]
ReadPrec Stochastic
Int -> ReadS Stochastic
ReadS [Stochastic]
(Int -> ReadS Stochastic)
-> ReadS [Stochastic]
-> ReadPrec Stochastic
-> ReadPrec [Stochastic]
-> Read Stochastic
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Stochastic
readsPrec :: Int -> ReadS Stochastic
$creadList :: ReadS [Stochastic]
readList :: ReadS [Stochastic]
$creadPrec :: ReadPrec Stochastic
readPrec :: ReadPrec Stochastic
$creadListPrec :: ReadPrec [Stochastic]
readListPrec :: ReadPrec [Stochastic]
Read,Stochastic -> Stochastic -> Bool
(Stochastic -> Stochastic -> Bool)
-> (Stochastic -> Stochastic -> Bool) -> Eq Stochastic
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Stochastic -> Stochastic -> Bool
== :: Stochastic -> Stochastic -> Bool
$c/= :: Stochastic -> Stochastic -> Bool
/= :: Stochastic -> Stochastic -> Bool
Eq,Eq Stochastic
Eq Stochastic =>
(Stochastic -> Stochastic -> Ordering)
-> (Stochastic -> Stochastic -> Bool)
-> (Stochastic -> Stochastic -> Bool)
-> (Stochastic -> Stochastic -> Bool)
-> (Stochastic -> Stochastic -> Bool)
-> (Stochastic -> Stochastic -> Stochastic)
-> (Stochastic -> Stochastic -> Stochastic)
-> Ord Stochastic
Stochastic -> Stochastic -> Bool
Stochastic -> Stochastic -> Ordering
Stochastic -> Stochastic -> Stochastic
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Stochastic -> Stochastic -> Ordering
compare :: Stochastic -> Stochastic -> Ordering
$c< :: Stochastic -> Stochastic -> Bool
< :: Stochastic -> Stochastic -> Bool
$c<= :: Stochastic -> Stochastic -> Bool
<= :: Stochastic -> Stochastic -> Bool
$c> :: Stochastic -> Stochastic -> Bool
> :: Stochastic -> Stochastic -> Bool
$c>= :: Stochastic -> Stochastic -> Bool
>= :: Stochastic -> Stochastic -> Bool
$cmax :: Stochastic -> Stochastic -> Stochastic
max :: Stochastic -> Stochastic -> Stochastic
$cmin :: Stochastic -> Stochastic -> Stochastic
min :: Stochastic -> Stochastic -> Stochastic
Ord,Int -> Stochastic
Stochastic -> Int
Stochastic -> [Stochastic]
Stochastic -> Stochastic
Stochastic -> Stochastic -> [Stochastic]
Stochastic -> Stochastic -> Stochastic -> [Stochastic]
(Stochastic -> Stochastic)
-> (Stochastic -> Stochastic)
-> (Int -> Stochastic)
-> (Stochastic -> Int)
-> (Stochastic -> [Stochastic])
-> (Stochastic -> Stochastic -> [Stochastic])
-> (Stochastic -> Stochastic -> [Stochastic])
-> (Stochastic -> Stochastic -> Stochastic -> [Stochastic])
-> Enum Stochastic
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Stochastic -> Stochastic
succ :: Stochastic -> Stochastic
$cpred :: Stochastic -> Stochastic
pred :: Stochastic -> Stochastic
$ctoEnum :: Int -> Stochastic
toEnum :: Int -> Stochastic
$cfromEnum :: Stochastic -> Int
fromEnum :: Stochastic -> Int
$cenumFrom :: Stochastic -> [Stochastic]
enumFrom :: Stochastic -> [Stochastic]
$cenumFromThen :: Stochastic -> Stochastic -> [Stochastic]
enumFromThen :: Stochastic -> Stochastic -> [Stochastic]
$cenumFromTo :: Stochastic -> Stochastic -> [Stochastic]
enumFromTo :: Stochastic -> Stochastic -> [Stochastic]
$cenumFromThenTo :: Stochastic -> Stochastic -> Stochastic -> [Stochastic]
enumFromThenTo :: Stochastic -> Stochastic -> Stochastic -> [Stochastic]
Enum,Stochastic
Stochastic -> Stochastic -> Bounded Stochastic
forall a. a -> a -> Bounded a
$cminBound :: Stochastic
minBound :: Stochastic
$cmaxBound :: Stochastic
maxBound :: Stochastic
Bounded)

--------------------------------------------------------------------------------

-- validate'


-- | short cut for 'validateDet' and should be used mainly in interactiv mode.

validate' :: Statement -> Bool
validate' :: Statement -> Bool
validate' Statement
s = Statement -> Bool
validateDet Statement
s

--------------------------------------------------------------------------------

-- Cnfg -


-- | configuration of validating.

data Cnfg
  = Cnfg
  { -- | initial state.

    Cnfg -> Maybe Omega
cnfOmega            :: Maybe Omega

    -- | number of samples to be validated. 

  , Cnfg -> Int
cnfSamples          :: Int

    -- | range of wide.

  , Cnfg -> (Int, Int)
cnfWide             :: (Int,Int)

    -- | maximal time for validateing in seconds.

  , Cnfg -> Int
cnfMaxDuration      :: Int

    -- | duration between two log entires in seconds.

  , Cnfg -> Int
cnfLogDuration      :: Int

    -- | 'True' with statistics.

  , Cnfg -> Bool
cnfStatistics       :: Bool

    -- | number of labels to be shown for the statistics over all.

  , Cnfg -> Int
cnfStcPathLength    :: Int

  } deriving Int -> Cnfg -> ShowS
[Cnfg] -> ShowS
Cnfg -> String
(Int -> Cnfg -> ShowS)
-> (Cnfg -> String) -> ([Cnfg] -> ShowS) -> Show Cnfg
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Cnfg -> ShowS
showsPrec :: Int -> Cnfg -> ShowS
$cshow :: Cnfg -> String
show :: Cnfg -> String
$cshowList :: [Cnfg] -> ShowS
showList :: [Cnfg] -> ShowS
Show

--------------------------------------------------------------------------------

-- stdCnf -


-- | standard configuration

stdCnf :: Cnfg
stdCnf :: Cnfg
stdCnf = Cnfg { cnfOmega :: Maybe Omega
cnfOmega         = Maybe Omega
forall a. Maybe a
Nothing
              , cnfSamples :: Int
cnfSamples       = Int
100
              , cnfWide :: (Int, Int)
cnfWide          = (Int
5,Int
10)
              , cnfMaxDuration :: Int
cnfMaxDuration   = Int
5
              , cnfLogDuration :: Int
cnfLogDuration   = Int
20
              , cnfStatistics :: Bool
cnfStatistics    = Bool
False
              , cnfStcPathLength :: Int
cnfStcPathLength = Int
3
              }

--------------------------------------------------------------------------------

-- Result -


-- | result of the validation.

data Result
  = Result
  { Result -> Maybe Valid
rsValid            :: Maybe Valid
  , Result -> Int
rsValidatedSamples :: Int
    -- | number of tests over all

  , Result -> Int
rsTests      :: Int

    -- | number of false tests from a non valid sample

  , Result -> Int
rsTestsFalse   :: Int

    -- | number of tests from reduced denied premises

  , Result -> Int
rsTestsRdcDndPrms    :: Int
  }
  deriving (Int -> Result -> ShowS
[Result] -> ShowS
Result -> String
(Int -> Result -> ShowS)
-> (Result -> String) -> ([Result] -> ShowS) -> Show Result
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Result -> ShowS
showsPrec :: Int -> Result -> ShowS
$cshow :: Result -> String
show :: Result -> String
$cshowList :: [Result] -> ShowS
showList :: [Result] -> ShowS
Show)

--------------------------------------------------------------------------------

-- validateWith -


-- | validates the proposition with the given configuration and stochastic.

validateWith :: Cnfg -> Statement -> IO Valid
validateWith :: Cnfg -> Statement -> IO Valid
validateWith Cnfg
cnf Statement
s = do
  SystemTime
tStart <- IO SystemTime
getSystemTime
  Omega
o      <- case Cnfg -> Maybe Omega
cnfOmega Cnfg
cnf of
              Maybe Omega
Nothing -> IO Omega
getOmega
              Just Omega
o  -> Omega -> IO Omega
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Omega
o
  String -> IO ()
putMessage (String -> IO ()) -> String -> IO ()
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Omega -> String
forall a. Show a => a -> String
show (Omega -> String) -> Omega -> String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Omega
o
  (Result
res,Maybe [V]
mvs) <- let (Int
wl,Int
wh) = Cnfg -> (Int, Int)
cnfWide Cnfg
cnf
                   sts :: Bool
sts     = Cnfg -> Bool
cnfStatistics Cnfg
cnf
                   ivs :: [IO V]
ivs     = Int -> [IO V] -> [IO V]
forall a. Int -> [a] -> [a]
take (Cnfg -> Int
cnfSamples Cnfg
cnf) ([IO V] -> [IO V]) -> [IO V] -> [IO V]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X (IO V) -> Omega -> [IO V]
forall x. X x -> Omega -> [x]
samples (Statement -> X (Int, Omega) -> X (IO V)
xValue Statement
s (Int -> Int -> X (Int, Omega)
xWO Int
wl Int
wh)) Omega
o
                in Cnfg -> SystemTime -> Bool -> [IO V] -> IO (Result, Maybe [V])
doValidation Cnfg
cnf SystemTime
tStart Bool
sts [IO V]
ivs
  case Maybe [V]
mvs of
    Just [V]
vs -> Cnfg -> [V] -> IO ()
putStatisticV Cnfg
cnf [V]
vs
    Maybe [V]
_       -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  Result -> IO ()
putSummary Result
res
  Valid -> IO Valid
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Valid -> IO Valid) -> Valid -> IO Valid
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Maybe Valid -> Valid
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Valid -> Valid) -> Maybe Valid -> Valid
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Result -> Maybe Valid
rsValid Result
res

----------------------------------------

-- doValidation -


type Pico = Integer

toPico :: Int -> Pico
toPico :: Int -> Pico
toPico Int
d = Int -> Pico
forall a. Enum a => Int -> a
toEnum Int
d Pico -> Pico -> Pico
forall a. Num a => a -> a -> a
* Pico
1000000000000 -- = 1e12


tDiff :: SystemTime -> SystemTime -> Pico
tDiff :: SystemTime -> SystemTime -> Pico
tDiff SystemTime
s SystemTime
e = DiffTime -> Pico
diffTimeToPicoseconds (DiffTime -> Pico) -> DiffTime -> Pico
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ AbsoluteTime -> AbsoluteTime -> DiffTime
diffAbsoluteTime (SystemTime -> AbsoluteTime
t SystemTime
e) (SystemTime -> AbsoluteTime
t SystemTime
s)
  where t :: SystemTime -> AbsoluteTime
t = SystemTime -> AbsoluteTime
systemToTAITime

doValidation :: Cnfg -> SystemTime -> Bool -> [IO V] -> IO (Result,Maybe [V])
doValidation :: Cnfg -> SystemTime -> Bool -> [IO V] -> IO (Result, Maybe [V])
doValidation Cnfg
cnf SystemTime
tStart Bool
sts [IO V]
ivs = do
  SystemTime
-> [IO V] -> Result -> Maybe [V] -> IO (Result, Maybe [V])
forall {m :: * -> *}.
Monad m =>
SystemTime -> [IO V] -> Result -> m [V] -> IO (Result, m [V])
dvld SystemTime
tStart [IO V]
ivs Result
res (if Bool
sts then [V] -> Maybe [V]
forall a. a -> Maybe a
Just [] else Maybe [V]
forall a. Maybe a
Nothing)
  where res :: Result
res = Result
              { rsValid :: Maybe Valid
rsValid             = Valid -> Maybe Valid
forall a. a -> Maybe a
Just Valid
Valid
              , rsValidatedSamples :: Int
rsValidatedSamples  = Int
0
              , rsTests :: Int
rsTests             = Int
0
              , rsTestsFalse :: Int
rsTestsFalse        = Int
0
              , rsTestsRdcDndPrms :: Int
rsTestsRdcDndPrms   = Int
0
              }

        Valid
Valid &&> :: Valid -> Valid -> Valid
&&> Valid
_ = Valid
Valid
        Valid
a     &&> Valid
b = Valid
a Valid -> Valid -> Valid
forall a. Logical a => a -> a -> a
&& Valid
b

        halt :: Result -> Bool
halt Result
res = case Result -> Maybe Valid
rsValid Result
res of
          Maybe Valid
Nothing -> Bool
True
          Just Valid
b  -> Valid
b Valid -> Valid -> Bool
forall a. Eq a => a -> a -> Bool
/= Valid
ProbablyValid
          
        putLog :: Result -> SystemTime -> SystemTime -> IO SystemTime
putLog Result
res SystemTime
tLast SystemTime
t
          | Bool
drtn      = do
              Result -> IO ()
putRsSamples Result
res
              Handle -> IO ()
hFlush Handle
stdout
              IO SystemTime
getSystemTime
          | Bool
otherwise = SystemTime -> IO SystemTime
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SystemTime
tLast
          where drtn :: Bool
drtn = SystemTime -> SystemTime -> Pico
tDiff SystemTime
tLast SystemTime
t Pico -> Pico -> Bool
forall a. Ord a => a -> a -> Bool
> (Int -> Pico
toPico (Int -> Pico) -> Int -> Pico
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Cnfg -> Int
cnfLogDuration Cnfg
cnf)

        more :: Result -> [a] -> SystemTime -> SystemTime -> m [a]
more Result
res [a]
ivs SystemTime
tStart SystemTime
t
          | Result -> Bool
halt Result
res            = [a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
          | Bool
drtn                = [a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
          | Bool
otherwise           = [a] -> m [a]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
ivs
          where drtn :: Bool
drtn = SystemTime -> SystemTime -> Pico
tDiff SystemTime
tStart SystemTime
t Pico -> Pico -> Bool
forall a. Ord a => a -> a -> Bool
> (Int -> Pico
toPico (Int -> Pico) -> Int -> Pico
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Cnfg -> Int
cnfMaxDuration Cnfg
cnf)

        dvld :: SystemTime -> [IO V] -> Result -> m [V] -> IO (Result, m [V])
dvld SystemTime
_ [] Result
res m [V]
mvs           = (Result, m [V]) -> IO (Result, m [V])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result
res,m [V]
mvs)
        dvld SystemTime
tLast (IO V
iv:[IO V]
ivs) Result
res m [V]
mvs = m [V]
mvs m [V] -> IO (Result, m [V]) -> IO (Result, m [V])
forall a b. a -> b -> b
`seq` do
          V
v      <- IO V
iv
          Result
res'   <- HNFValue Valid -> V -> Result -> IO Result
dres (V -> HNFValue Valid
valT V
v) V
v Result
res
          SystemTime
tLast' <- IO SystemTime
getSystemTime IO SystemTime -> (SystemTime -> IO SystemTime) -> IO SystemTime
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Result -> SystemTime -> SystemTime -> IO SystemTime
putLog Result
res SystemTime
tLast
          [IO V]
ivs'   <- IO SystemTime
getSystemTime IO SystemTime -> (SystemTime -> IO [IO V]) -> IO [IO V]
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Result -> [IO V] -> SystemTime -> SystemTime -> IO [IO V]
forall {m :: * -> *} {a}.
Monad m =>
Result -> [a] -> SystemTime -> SystemTime -> m [a]
more Result
res' [IO V]
ivs SystemTime
tStart
          SystemTime -> [IO V] -> Result -> m [V] -> IO (Result, m [V])
dvld SystemTime
tLast' [IO V]
ivs' Result
res' (m [V]
mvs m [V] -> ([V] -> m [V]) -> m [V]
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [V] -> m [V]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([V] -> m [V]) -> ([V] -> [V]) -> [V] -> m [V]
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (V
vV -> [V] -> [V]
forall a. a -> [a] -> [a]
:)) 

        dres :: HNFValue Valid -> V -> Result -> IO Result
dres (HNFValue Valid
sb) V
v Result
res | Valid
sb Valid -> Valid -> Bool
forall a. Ord a => a -> a -> Bool
< Valid
ProbablyValid = do
          V -> IO ()
putFalse V
v
          Result -> IO Result
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
res{ rsValid            = fmap (sb&&>) $ rsValid res 
                    , rsValidatedSamples = rsValidatedSamples res + 1
                    , rsTests            = rsTests res + cntTests v
                    , rsTestsFalse       = rsTestsFalse res + cntTestsRdcFalse v
                    }
          
        dres (HNFValue Valid
sb) V
v Result
res = do
          Result -> IO Result
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
res{ rsValid            = fmap (sb&&>) $ rsValid res
                    , rsValidatedSamples = rsValidatedSamples res + 1
                    , rsTests            = rsTests res + cntTests v
                    , rsTestsRdcDndPrms  = rsTestsRdcDndPrms res + cntTestsRdcDndPrms v
                    }
          
        dres (Failure e
e) V
v Result
res = do
          Result
res' <- Result -> IO Result
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result
res{ rsValid            = Nothing
                            , rsValidatedSamples = rsValidatedSamples res + 1
                            , rsTests            = rsTests res + cntTests v
                            }
          V -> IO ()
putFailed V
v
          Result -> IO ()
putSummary Result
res'
          ValidateException -> IO Result
forall a e. Exception e => e -> a
throw (ValidateException -> IO Result) -> ValidateException -> IO Result
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ SomeException -> ValidateException
FailedStatement (SomeException -> ValidateException)
-> SomeException -> ValidateException
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ e -> SomeException
forall e. Exception e => e -> SomeException
toException e
e

----------------------------------------

-- putMessage -

putMessage :: String -> IO ()
putMessage :: String -> IO ()
putMessage String
msg = String -> IO ()
putStrLn (String
">> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg)

----------------------------------------

-- putFalse -


putFalse :: V -> IO ()
putFalse :: V -> IO ()
putFalse V
v = do
  String -> IO ()
putMessage String
"--------------------------------------------------------------------------------"
  Maybe V -> IO ()
putValue (V -> Maybe V
rdcFalse V
v)

----------------------------------------

-- putFailed -

putFailed :: V -> IO ()
putFailed :: V -> IO ()
putFailed V
v = do
  String -> IO ()
putMessage String
"--------------------------------------------------------------------------------"
  String -> IO ()
putMessage String
"failed sample"
  Maybe V -> IO ()
putValue (V -> Maybe V
rdcFailed V
v)
  
----------------------------------------

-- putValue -


putValue :: Maybe V -> IO ()
putValue :: Maybe V -> IO ()
putValue Maybe V
Nothing  = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
putValue (Just V
v) = String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Indent -> V -> String
showV (String -> Indent
indent0 String
"  ") V
v

----------------------------------------

-- putStatisticV -

putStatisticV :: Cnfg -> [V] -> IO ()
putStatisticV :: Cnfg -> [V] -> IO ()
putStatisticV Cnfg
cnf [V]
vs = do
  -- putMessage "statistics of false "

  String -> IO ()
putMessage String
"statistics over all"
  [[String] -> String] -> [(Int, [String])] -> IO ()
forall x. (Show x, Ord x) => [x -> String] -> [(Int, x)] -> IO ()
putStatisticW [] ([(Int, [String])] -> IO ()) -> [(Int, [String])] -> IO ()
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Maybe Int -> [V] -> [(Int, [String])]
tsts (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Cnfg -> Int
cnfStcPathLength Cnfg
cnf) [V]
vs
  String -> IO ()
putMessage String
"statistics of false"
  [[String] -> String] -> [(Int, [String])] -> IO ()
forall x. (Show x, Ord x) => [x -> String] -> [(Int, x)] -> IO ()
putStatisticW [] ([(Int, [String])] -> IO ()) -> [(Int, [String])] -> IO ()
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Maybe Int -> [V] -> [(Int, [String])]
tsts Maybe Int
forall a. Maybe a
Nothing ([V] -> [(Int, [String])]) -> [V] -> [(Int, [String])]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [Maybe V] -> [V]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe V] -> [V]) -> [Maybe V] -> [V]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (V -> Maybe V) -> [V] -> [Maybe V]
forall a b. (a -> b) -> [a] -> [b]
map V -> Maybe V
rdcFalse [V]
vs
  String -> IO ()
putMessage String
"statistics of denied premises"
  [[String] -> String] -> [(Int, [String])] -> IO ()
forall x. (Show x, Ord x) => [x -> String] -> [(Int, x)] -> IO ()
putStatisticW [] ([(Int, [String])] -> IO ()) -> [(Int, [String])] -> IO ()
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Maybe Int -> [V] -> [(Int, [String])]
tsts Maybe Int
forall a. Maybe a
Nothing ([V] -> [(Int, [String])]) -> [V] -> [(Int, [String])]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [Maybe V] -> [V]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe V] -> [V]) -> [Maybe V] -> [V]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (V -> Maybe V) -> [V] -> [Maybe V]
forall a b. (a -> b) -> [a] -> [b]
map V -> Maybe V
rdcDndPrms [V]
vs
  where tsts :: Maybe Int -> [V] -> [(Int, [String])]
tsts Maybe Int
mn = ((Int, [String]) -> (Int, [String]))
-> [(Int, [String])] -> [(Int, [String])]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
n,[String]
p) -> (Int
n,[String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String]) -> [String] -> [String]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [String] -> [String]
forall a. [a] -> [a]
mtake [String]
p)) ([(Int, [String])] -> [(Int, [String])])
-> ([V] -> [(Int, [String])]) -> [V] -> [(Int, [String])]
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. [[(Int, [String])]] -> [(Int, [String])]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ([[(Int, [String])]] -> [(Int, [String])])
-> ([V] -> [[(Int, [String])]]) -> [V] -> [(Int, [String])]
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (V -> [(Int, [String])]) -> [V] -> [[(Int, [String])]]
forall a b. (a -> b) -> [a] -> [b]
map V -> [(Int, [String])]
tests
          where mtake :: [a] -> [a]
mtake = case Maybe Int
mn of
                          Just Int
n -> Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
n
                          Maybe Int
_      -> [a] -> [a]
forall x. x -> x
id

----------------------------------------

-- putSummary -

putSummary :: Result -> IO ()
putSummary :: Result -> IO ()
putSummary Result
r = do
  String -> IO ()
putMessage String
"--------------------------------------------------------------------------------"
  String -> IO ()
putMessage String
"Summary"
  Result -> IO ()
putRsSamples Result
r
  Maybe Valid -> Result -> IO ()
putRsTests (Result -> Maybe Valid
rsValid Result
r) Result
r


nshow :: Int -> String -> String
nshow :: Int -> ShowS
nshow Int
n String
s = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
jtween String
" " [Int -> String
forall a. Show a => a -> String
show Int
n,String
s'] where s' :: String
s' = String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then String
"" else String
"s"

putRsSamples :: Result -> IO ()
putRsSamples :: Result -> IO ()
putRsSamples Result
r = do
  String -> IO ()
putMessage (String -> IO ()) -> String -> IO ()
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
jtween String
" " [ Int -> ShowS
nshow (Result -> Int
rsValidatedSamples Result
r) String
"sample"
                          , String
"tested where"
                          , Int -> ShowS
nshow (Result -> Int
rsTestsFalse Result
r) String
"test"
                          , String
"are false, having"
                          , Int -> String
forall a. Show a => a -> String
show (Result -> Int
rsTestsRdcDndPrms Result
r)
                          , String
"denied premises"
                          ]

putRsTests :: Maybe Valid -> Result -> IO ()
putRsTests :: Maybe Valid -> Result -> IO ()
putRsTests (Just Valid
_) Result
r = do
  String -> IO ()
putMessage (String -> IO ()) -> String -> IO ()
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
jtween String
" " [ Int -> ShowS
nshow (Result -> Int
rsTests Result
r) String
"test"
                          , String
"with a false ratio of"
                          , Int -> Int -> String
pshow (Result -> Int
rsTestsFalse Result
r) (Result -> Int
rsTests Result
r)
                          , String
"and a denied premises ratio of"
                          , Int -> Int -> String
pshow (Result -> Int
rsTestsRdcDndPrms Result
r) (Result -> Int
rsTests Result
r) 
                          ]
  where pshow :: Int -> Int -> String
pshow Int
a Int
b = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
' ') ShowS -> ShowS
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Verbosity -> Percent Double -> String
forall a. Verbose a => Verbosity -> a -> String
vshow Verbosity
Low (Percent Double -> String) -> Percent Double -> String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Double -> Percent Double
forall x. x -> Percent x
Percent (Double
a' Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
b')
          where a' :: Double
a' = Int -> Double
forall a. Enum a => Int -> a
toEnum Int
a :: Double
                b' :: Double
b' = Int -> Double
forall a. Enum a => Int -> a
toEnum Int
b

putRsTests Maybe Valid
Nothing Result
r = String -> IO ()
putMessage (String -> IO ()) -> String -> IO ()
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Int -> ShowS
nshow (Result -> Int
rsTests Result
r) String
"test"
        
--------------------------------------------------------------------------------

-- test -


-- | adapts the standard configuration 'stdCnf' according to the given stochastic.

stdStc :: Stochastic -> Cnfg
stdStc :: Stochastic -> Cnfg
stdStc Stochastic
s = case Stochastic
s of
  Stochastic
Sparse   -> Cnfg
stdCnf{ cnfSamples     = 10
                    , cnfMaxDuration = 2
                    }
  Stochastic
Standard -> Cnfg
stdCnf
  Stochastic
Massive  -> Cnfg
stdCnf{ cnfSamples     = 10000
                    , cnfMaxDuration = 300
                    }

--------------------------------------------------------------------------------

-- validateStochastic -


-- | validates the statement with the configuration given by 'stdStc',

validateStochastic :: Stochastic -> Statement -> IO Valid
validateStochastic :: Stochastic -> Statement -> IO Valid
validateStochastic = Cnfg -> Statement -> IO Valid
validateWith (Cnfg -> Statement -> IO Valid)
-> (Stochastic -> Cnfg) -> Stochastic -> Statement -> IO Valid
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Stochastic -> Cnfg
stdStc 

--------------------------------------------------------------------------------

-- validate -


-- | validates a statement.

validate :: Statement -> IO Valid
validate :: Statement -> IO Valid
validate = Cnfg -> Statement -> IO Valid
validateWith Cnfg
cnf{cnfStatistics = False} where cnf :: Cnfg
cnf = Stochastic -> Cnfg
stdStc Stochastic
Sparse

--------------------------------------------------------------------------------

-- validateStatistics -


-- | validates a statement according to the given stochastic with showing the statistics.

validateStatistics :: Stochastic -> Statement -> IO Valid
validateStatistics :: Stochastic -> Statement -> IO Valid
validateStatistics Stochastic
c Statement
s = Cnfg -> Statement -> IO Valid
validateWith Cnfg
cnf{cnfStatistics = True} Statement
s where cnf :: Cnfg
cnf = Stochastic -> Cnfg
stdStc Stochastic
c