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

--------------------------------------------------------------------------------
-- stdCnf -

-- | standard configuration
stdCnf :: Cnfg
stdCnf :: Cnfg
stdCnf = Cnfg { cnfOmega :: Maybe Omega
cnfOmega         = 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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Result] -> ShowS
$cshowList :: [Result] -> ShowS
show :: Result -> String
$cshow :: Result -> String
showsPrec :: Int -> Result -> ShowS
$cshowsPrec :: Int -> 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  -> forall (m :: * -> *) a. Monad m => a -> m a
return Omega
o
  String -> IO ()
putMessage forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Show a => a -> String
show forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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     = forall a. Int -> [a] -> [a]
take (Cnfg -> Int
cnfSamples Cnfg
cnf) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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]
_       -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
  Result -> IO ()
putSummary Result
res
  forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. HasCallStack => Maybe a -> a
fromJust forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Result -> Maybe Valid
rsValid Result
res

----------------------------------------
-- doValidation -

type Pico = Integer

toPico :: Int -> Pico
toPico :: Int -> Pico
toPico Int
d = forall a. Enum a => Int -> a
toEnum Int
d 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 forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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
  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 forall a. a -> Maybe a
Just [] else forall a. Maybe a
Nothing)
  where res :: Result
res = Result
              { rsValid :: Maybe Valid
rsValid             = 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 forall b. Boolean b => b -> b -> b
&& 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 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 = forall (m :: * -> *) a. Monad m => a -> m a
return SystemTime
tLast
          where drtn :: Bool
drtn = SystemTime -> SystemTime -> Pico
tDiff SystemTime
tLast SystemTime
t forall a. Ord a => a -> a -> Bool
> (Int -> Pico
toPico forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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            = forall (m :: * -> *) a. Monad m => a -> m a
return []
          | Bool
drtn                = forall (m :: * -> *) a. Monad m => a -> m a
return []
          | Bool
otherwise           = forall (m :: * -> *) a. Monad m => a -> m a
return [a]
ivs
          where drtn :: Bool
drtn = SystemTime -> SystemTime -> Pico
tDiff SystemTime
tStart SystemTime
t forall a. Ord a => a -> a -> Bool
> (Int -> Pico
toPico forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Cnfg -> Int
cnfMaxDuration Cnfg
cnf)

        dvld :: SystemTime -> [IO V] -> Result -> m [V] -> IO (Result, m [V])
dvld SystemTime
_ [] Result
res m [V]
mvs           = 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 seq :: 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 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (V
vforall a. a -> [a] -> [a]
:)) 

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

----------------------------------------
-- putMessage -
putMessage :: String -> IO ()
putMessage :: String -> IO ()
putMessage String
msg = String -> IO ()
putStrLn (String
">> " 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  = forall (m :: * -> *) a. Monad m => a -> m a
return ()
putValue (Just V
v) = String -> IO ()
putStrLn forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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"
  forall x. (Show x, Ord x) => [x -> String] -> [(Int, x)] -> IO ()
putStatisticW [] forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Maybe Int -> [V] -> [(Int, [String])]
tsts (forall a. a -> Maybe a
Just forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Cnfg -> Int
cnfStcPathLength Cnfg
cnf) [V]
vs
  String -> IO ()
putMessage String
"statistics of false"
  forall x. (Show x, Ord x) => [x -> String] -> [(Int, x)] -> IO ()
putStatisticW [] forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Maybe Int -> [V] -> [(Int, [String])]
tsts forall a. Maybe a
Nothing forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map V -> Maybe V
rdcFalse [V]
vs
  String -> IO ()
putMessage String
"statistics of denied premises"
  forall x. (Show x, Ord x) => [x -> String] -> [(Int, x)] -> IO ()
putStatisticW [] forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Maybe Int -> [V] -> [(Int, [String])]
tsts forall a. Maybe a
Nothing forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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 = forall a b. (a -> b) -> [a] -> [b]
map (\(Int
n,[String]
p) -> (Int
n,forall a. [a] -> [a]
reverse forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. [a] -> [a]
mtake [String]
p)) forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. 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 -> forall a. Int -> [a] -> [a]
take Int
n
                          Maybe Int
_      -> 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 = forall a. [a] -> [[a]] -> [a]
jtween String
" " [forall a. Show a => a -> String
show Int
n,String
s'] where s' :: String
s' = String
s forall a. [a] -> [a] -> [a]
++ if Int
n 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 forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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"
                          , 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 forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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 = forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a. Eq a => a -> a -> Bool
== Char
' ') forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Verbose a => Verbosity -> a -> String
vshow Verbosity
Low forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. x -> Percent x
Percent (Double
a' forall a. Fractional a => a -> a -> a
/ Double
b')
          where a' :: Double
a' = forall a. Enum a => Int -> a
toEnum Int
a :: Double
                b' :: Double
b' = forall a. Enum a => Int -> a
toEnum Int
b

putRsTests Maybe Valid
Nothing Result
r = String -> IO ()
putMessage forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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 :: Int
cnfSamples     = Int
10
                    , cnfMaxDuration :: Int
cnfMaxDuration = Int
2
                    }
  Stochastic
Standard -> Cnfg
stdCnf
  Stochastic
Massive  -> Cnfg
stdCnf{ cnfSamples :: Int
cnfSamples     = Int
10000
                    , cnfMaxDuration :: Int
cnfMaxDuration = Int
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 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 :: Bool
cnfStatistics = Bool
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 :: Bool
cnfStatistics = Bool
True} Statement
s where cnf :: Cnfg
cnf = Stochastic -> Cnfg
stdStc Stochastic
c