{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}

-- |
-- Module      : OAlg.Data.Statement.Definition
-- Description : definition of statements on properties
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- Statements on properties which can be validated via 'validateStoch'. They serve to
-- implement automatic testing (see "OAlg.Control.Validate").
-- 
-- __Examples__ Deterministic
-- 
-- Validation of the valid and invalid statement
-- 
-- >>> getOmega >>= validateStoch SValid 10
-- Valid
-- 
-- >>> getOmega >>= validateStoch SInvalid 5
-- Invalid
-- 
-- As no stochastic was used to evaluate the two examples, the result is 'Valid' and 'Invalid'
-- respectively!
-- 
-- __Examples__ Stochastic
-- 
-- Validation of a 'Forall' and 'Exist' statement
-- 
-- >>> getOmega >>= validateStoch (Forall (xIntB 0 10) (\i -> (0 <= i && i <= 10):?>Params["i":=show i]-- )) 100
-- ProbablyValid
-- 
-- >>> getOmega >>= validateStoch (Exist (xIntB 0 10) (\i -> (11 <= i):?>Params["i":=show i])) 100
-- ProbablyInvalid
-- 
-- The valuation of these two examples uses the given 'Omega' and 'Wide' of @100@ to pick randomly
-- @100@ samples of the given random variable @'xIntB' 0 10@ and applies these samples to the given
-- test function. The result is 'ProbablyValid' and 'ProbablyInvalid' respectively!
module OAlg.Data.Statement.Definition
  (
    -- * Statement
    Statement(..),(.==.), (./=.),(|~>), someException
  , Label(Label,Prp), Message(..), Variable, Parameter(..)


    -- * Validating
    -- ** Stochastic
  , validateStoch, Wide, value, V(), valDeterministic, valT, T, Valid(..)
  , showV, indent0, showVStatement

    -- ** Deterministic
  , validateDet
  
    -- * Reducing Values
  , tests, SPath, cntTests
  , rdcTrue, cntTestsRdcTrue
  , rdcFalse, cntTestsRdcFalse
  , rdcDndPrms, cntTestsRdcDndPrms
  , rdcFailed, cntTestsRdcFailed

    -- * X
  , xValue, xWO, xValid

    -- * Exception
  , ValidateingException(..)
  )
  where

import Prelude (Num(..),Ord(..),Ordering(..),Bounded(..))

import Control.Monad
import Control.Exception
import Control.DeepSeq

import System.IO.Unsafe
import System.IO

import Data.List (map,(++),take,zip)
import Data.Foldable hiding (and)

import OAlg.Category.Definition

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

import OAlg.Data.Boolean.Definition
import OAlg.Data.Equal
import OAlg.Data.X
import OAlg.Data.Show 
import OAlg.Data.Maybe
import OAlg.Data.Canonical
import OAlg.Data.Number

--------------------------------------------------------------------------------
-- ValidateingException -

-- | validating exceptions which are sub exceptions from 'SomeOAlgException'.
data ValidateingException
  = NonDeterministic
  deriving (ValidateingException -> ValidateingException -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ValidateingException -> ValidateingException -> Bool
$c/= :: ValidateingException -> ValidateingException -> Bool
== :: ValidateingException -> ValidateingException -> Bool
$c== :: ValidateingException -> ValidateingException -> Bool
Eq,Int -> ValidateingException -> ShowS
[ValidateingException] -> ShowS
ValidateingException -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ValidateingException] -> ShowS
$cshowList :: [ValidateingException] -> ShowS
show :: ValidateingException -> String
$cshow :: ValidateingException -> String
showsPrec :: Int -> ValidateingException -> ShowS
$cshowsPrec :: Int -> ValidateingException -> ShowS
Show)

instance Exception ValidateingException where
  toException :: ValidateingException -> SomeException
toException   = forall e. Exception e => e -> SomeException
oalgExceptionToException
  fromException :: SomeException -> Maybe ValidateingException
fromException = forall e. Exception e => SomeException -> Maybe e
oalgExceptionFromException

--------------------------------------------------------------------------------
-- Label -

-- if you add or change the internal Labels, you need to adappt relevantLabel!
-- | a labels.
data Label
  = Label String
  | Prp String

    -- internal
  | Prms -- premises
  | Cncl -- conclusion

instance Show Label where
  show :: Label -> String
show Label
l = case Label
l of
    Label String
s -> String
"(" forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
")"
    Prp String
p   -> String
"prp" forall a. [a] -> [a] -> [a]
++ String
p
    Label
Prms    -> String
"premise"
    Label
Cncl    -> String
"conclusion"

instance Verbose Label

--------------------------------------------------------------------------------
-- Variable -

-- | type of variables.
type Variable = String

--------------------------------------------------------------------------------
-- Parameter -

-- | showing the involved parameters of a statement.
data Parameter where
  (:=) :: Variable -> String -> Parameter

deriving instance Show Parameter

instance Verbose Parameter where
  vshow :: Verbosity -> Parameter -> String
vshow Verbosity
v (String
var := String
x) = forall a. [a] -> [[a]] -> [a]
jtween String
" " [String
var,String
":=",Maybe Int -> ShowS
vshowStr (Verbosity -> Maybe Int
mnString Verbosity
v) String
x] 

--------------------------------------------------------------------------------
-- Message -

-- | a message.
data Message
  = MInvalid -- ^ used for relations where no further information is desired or possible to give (see @relRelation@ as an example). 
  | Message String -- ^ a message
  | Params [Parameter] -- ^ a list of parameters
  deriving (Int -> Message -> ShowS
[Message] -> ShowS
Message -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Message] -> ShowS
$cshowList :: [Message] -> ShowS
show :: Message -> String
$cshow :: Message -> String
showsPrec :: Int -> Message -> ShowS
$cshowsPrec :: Int -> Message -> ShowS
Show)

instance Verbose Message where
  vshow :: Verbosity -> Message -> String
vshow Verbosity
v (Message String
m  ) = Maybe Int -> ShowS
vshowStr (Verbosity -> Maybe Int
mnString Verbosity
v) String
m 
  vshow Verbosity
v (Params [Parameter]
ps)   = forall a. Verbose a => Verbosity -> a -> String
vshow Verbosity
v [Parameter]
ps
  vshow Verbosity
_ Message
m             = forall a. Show a => a -> String
show Message
m

--------------------------------------------------------------------------------
-- Statement -

infix  4 :?>, .==., ./=.
infixr 3 :&&
infixr 2 :||
infixr 1 :=>, :<=>
infixr 0 :<=>:

-- | statement on properties..
data Statement where
  
  -- | the invalid statement.
  SInvalid :: Statement

  -- | the valid statement.
  SValid   :: Statement

  -- | checking a boolean.
  (:?>)    :: Bool -> Message -> Statement

  -- | catching an exception.
  Catch    :: Exception e => Statement -> (e -> Statement) -> Statement

  -- | not
  Not      :: Statement -> Statement

  -- | and
  (:&&)    :: Statement -> Statement -> Statement

  -- | and
  And      :: [Statement] -> Statement

  -- | or
  (:||)    :: Statement -> Statement -> Statement

  -- | or
  Or       :: [Statement] -> Statement

  -- | implication
  (:=>)    :: Statement -> Statement -> Statement

  -- | implication
  Impl     :: [Statement] -> Statement -> Statement

  -- | efinitional equivalence
  (:<=>:)  :: Label -> Statement -> Statement

  -- | equivalence
  (:<=>)   :: Statement -> Statement -> Statement

  -- | equivalence
  Eqvl     :: [Statement] -> Statement

  -- | the for all constructor
  Forall   :: X x -> (x -> Statement) -> Statement

  -- | the exist constructor.
  Exist    :: X x -> (x -> Statement) -> Statement
    
instance Boolean Statement where
  false :: Statement
false = Statement
SInvalid
  true :: Statement
true  = Statement
SValid
  not :: Statement -> Statement
not   = Statement -> Statement
Not
  || :: Statement -> Statement -> Statement
(||)  = Statement -> Statement -> Statement
(:||)
  or :: [Statement] -> Statement
or    = [Statement] -> Statement
Or
  && :: Statement -> Statement -> Statement
(&&)  = Statement -> Statement -> Statement
(:&&)
  and :: [Statement] -> Statement
and   = [Statement] -> Statement
And
  ~> :: Statement -> Statement -> Statement
(~>)  = Statement -> Statement -> Statement
(:=>)
  eqvl :: [Statement] -> Statement
eqvl  = [Statement] -> Statement
Eqvl

instance HNFData Statement where
  rhnf :: Statement -> ()
rhnf Statement
p = case Statement
p of
             Statement
SInvalid -> ()
             Statement
_      -> ()

--------------------------------------------------------------------------------
-- someException -

-- | convenient catcher for 'SomeException'.
someException :: Statement -> SomeException -> Statement
someException :: Statement -> SomeException -> Statement
someException Statement
p SomeException
_ = Statement
p

--------------------------------------------------------------------------------
-- (.==.) -

-- | checking for equality.
(.==.) :: Eq a => a -> a -> Statement
a
a .==. :: forall a. Eq a => a -> a -> Statement
.==. a
b = (a
a forall a. Eq a => a -> a -> Bool
== a
b) Bool -> Message -> Statement
:?> Message
MInvalid

--------------------------------------------------------------------------------
-- (./=.) -

-- | checking for inequality.
(./=.) :: Eq a => a -> a -> Statement
a
a ./=. :: forall a. Eq a => a -> a -> Statement
./=. a
b = (a
a forall a. Eq a => a -> a -> Bool
/= a
b) Bool -> Message -> Statement
:?> Message
MInvalid

--------------------------------------------------------------------------------
-- (|~>) -

infixr 1 |~>

-- | implication without resulting in denied premises for a 'false' premises. This
--   is useful for /switch/ cases.
(|~>) :: Statement -> Statement -> Statement
Statement
a |~> :: Statement -> Statement -> Statement
|~> Statement
b = Statement -> Statement
Not Statement
a forall b. Boolean b => b -> b -> b
|| Statement
b 
        
--------------------------------------------------------------------------------
-- Valid -

-- | weak form of classical boolean values arising from stochastically performed valuation
--   of 'Statement's.
--
--  __Definition__ Let @a@, @b@ be in 'Valid', then we define:
--
--  (1) @'not' a = 'toEnum' ('fromEnum' 'Valid' '-' 'fromEnum' a)@.
--
--  (1) @a '||' b = max a b@.
--
--  (1) @a '&&' b = min a b@.
--
--  (1) @a '~>' b = 'not' a '||' b@.
--
--  __Note__ @min@ and @max@ are implemented lazy as 'Valid' is bounded. This
--  is important that '~>' behaves as desired, i.e. for @a '~>' b@ and @a = 'Invalid'@ then
--  @b@ has not to be evaluated, because the maximum is already reached..
data Valid = Invalid | ProbablyInvalid | ProbablyValid | Valid
  deriving (Int -> Valid -> ShowS
[Valid] -> ShowS
Valid -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Valid] -> ShowS
$cshowList :: [Valid] -> ShowS
show :: Valid -> String
$cshow :: Valid -> String
showsPrec :: Int -> Valid -> ShowS
$cshowsPrec :: Int -> Valid -> ShowS
Show,Valid -> Valid -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Valid -> Valid -> Bool
$c/= :: Valid -> Valid -> Bool
== :: Valid -> Valid -> Bool
$c== :: Valid -> Valid -> Bool
Eq,Eq Valid
Valid -> Valid -> Bool
Valid -> Valid -> Ordering
Valid -> Valid -> Valid
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 :: Valid -> Valid -> Valid
$cmin :: Valid -> Valid -> Valid
max :: Valid -> Valid -> Valid
$cmax :: Valid -> Valid -> Valid
>= :: Valid -> Valid -> Bool
$c>= :: Valid -> Valid -> Bool
> :: Valid -> Valid -> Bool
$c> :: Valid -> Valid -> Bool
<= :: Valid -> Valid -> Bool
$c<= :: Valid -> Valid -> Bool
< :: Valid -> Valid -> Bool
$c< :: Valid -> Valid -> Bool
compare :: Valid -> Valid -> Ordering
$ccompare :: Valid -> Valid -> Ordering
Ord,Int -> Valid
Valid -> Int
Valid -> [Valid]
Valid -> Valid
Valid -> Valid -> [Valid]
Valid -> Valid -> Valid -> [Valid]
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 :: Valid -> Valid -> Valid -> [Valid]
$cenumFromThenTo :: Valid -> Valid -> Valid -> [Valid]
enumFromTo :: Valid -> Valid -> [Valid]
$cenumFromTo :: Valid -> Valid -> [Valid]
enumFromThen :: Valid -> Valid -> [Valid]
$cenumFromThen :: Valid -> Valid -> [Valid]
enumFrom :: Valid -> [Valid]
$cenumFrom :: Valid -> [Valid]
fromEnum :: Valid -> Int
$cfromEnum :: Valid -> Int
toEnum :: Int -> Valid
$ctoEnum :: Int -> Valid
pred :: Valid -> Valid
$cpred :: Valid -> Valid
succ :: Valid -> Valid
$csucc :: Valid -> Valid
Enum,Valid
forall a. a -> a -> Bounded a
maxBound :: Valid
$cmaxBound :: Valid
minBound :: Valid
$cminBound :: Valid
Bounded)

instance NFData Valid where
  rnf :: Valid -> ()
rnf Valid
Invalid = ()
  rnf Valid
_       = ()

instance Boolean Valid where
  false :: Valid
false = Valid
Invalid
  true :: Valid
true  = Valid
Valid
  not :: Valid -> Valid
not Valid
t = forall a. Enum a => Int -> a
toEnum (forall a. Enum a => a -> Int
fromEnum Valid
Valid forall a. Num a => a -> a -> a
- forall a. Enum a => a -> Int
fromEnum Valid
t)
  Valid
a || :: Valid -> Valid -> Valid
|| Valid
b  | Valid
a forall a. Eq a => a -> a -> Bool
== Valid
Valid = Valid
a -- to make (||) in its first argument lazy
          | Bool
otherwise  = case Valid
a forall a. Ord a => a -> a -> Ordering
`compare`Valid
b of
                           Ordering
GT -> Valid
a
                           Ordering
_  -> Valid
b
  Valid
a && :: Valid -> Valid -> Valid
&& Valid
b  | Valid
a forall a. Eq a => a -> a -> Bool
== Valid
Invalid = Valid
a -- to make (&&) in its first argument lazy
          | Bool
otherwise   = case Valid
a forall a. Ord a => a -> a -> Ordering
`compare` Valid
b of
                            Ordering
LT -> Valid
a
                            Ordering
_  -> Valid
b

instance Projectible Bool Valid where
  prj :: Valid -> Bool
prj Valid
Valid            = Bool
True
  prj Valid
ProbablyValid    = Bool
True
  prj Valid
ProbablyInvalid  = Bool
False
  prj Valid
Invalid          = Bool
False

--------------------------------------------------------------------------------
-- xValid -

-- | uniformly distributed random variable of 'Valid'.
xValid :: X Valid
xValid :: X Valid
xValid = forall a. (Enum a, Bounded a) => X a
xEnum

--------------------------------------------------------------------------------
-- T -

-- | the /truth/ type of a value @v@.
type T = HNFValue Valid

--------------------------------------------------------------------------------
-- V -

-- | the 'value' of a statement resulting from its validation.  'Forall' and 'Exist' are resolved
-- by finite samples.
data V
  = V Valid
  | forall e . Exception e => VFailure e
  | VCheck T (Maybe Message)
  | VCatch T (Maybe V) V -- Just v has been catched
  | VNot T V
  | VAnd T [V]    
  | VOr T [V]  
  | VImpl T V
  | VDefEqvl Label T V
  | VEqvl T V
  | VForall T V
  | VExist T V

deriving instance Show V
instance Verbose V

--------------------------------------------------------------------------------
-- Indent -

-- | indentation, where the first component is the basic indentation and the second the actual.
type Indent = (String,String)

-- | the next deeper indentation.
isucc :: Indent -> Indent
isucc :: Indent -> Indent
isucc (String
i,String
is) = (String
i,String
iforall a. [a] -> [a] -> [a]
++String
is)

-- | the indentation as string.
indent :: Indent -> String
indent :: Indent -> String
indent = forall a b. (a, b) -> b
snd

-- | the initial indentation given by a indentation string.
indent0 :: String -> Indent
indent0 :: String -> Indent
indent0 String
i = (String
i,String
"")

--------------------------------------------------------------------------------
-- showIndent -

showIndent :: Indent -> String -> String
showIndent :: Indent -> ShowS
showIndent Indent
is String
ss = ShowS
ind String
ss where
  ind :: ShowS
ind []        = []
  ind (Char
'\n':String
ss) = String
"\n" forall a. [a] -> [a] -> [a]
++ Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ ShowS
ind String
ss
  ind (Char
s:String
ss)    = Char
sforall a. a -> [a] -> [a]
:ShowS
ind String
ss
  
--------------------------------------------------------------------------------
-- showException -

showException :: Exception e => Indent -> e -> String
showException :: forall e. Exception e => Indent -> e -> String
showException Indent
is e
e = Indent -> ShowS
showIndent Indent
is (forall a. Show a => a -> String
show e
e) forall a. [a] -> [a] -> [a]
++ String
"\n"

--------------------------------------------------------------------------------
-- showValid -

showValid :: Indent -> Valid -> String
showValid :: Indent -> Valid -> String
showValid Indent
is Valid
v = Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Valid
v forall a. [a] -> [a] -> [a]
++ String
"\n"

--------------------------------------------------------------------------------
-- showFailure -

showFailure :: Exception e => Indent -> e -> String
showFailure :: forall e. Exception e => Indent -> e -> String
showFailure Indent
is e
e = Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
"failure " forall a. [a] -> [a] -> [a]
++ forall e. Exception e => Indent -> e -> String
showException (Indent -> Indent
isucc Indent
is) e
e

--------------------------------------------------------------------------------
-- showTLeaf -

showTLeaf :: Indent -> T -> String
showTLeaf :: Indent -> T -> String
showTLeaf Indent
is (HNFValue Valid
b) = Indent -> Valid -> String
showValid Indent
is Valid
b
showTLeaf Indent
is (Failure e
e)  = forall e. Exception e => Indent -> e -> String
showFailure Indent
is e
e

--------------------------------------------------------------------------------
-- showTNode -

showTNode :: T -> String
showTNode :: T -> String
showTNode (HNFValue Valid
b) = forall a. Show a => a -> String
show Valid
b
showTNode (Failure e
e)  = forall a. Show a => a -> String
show e
e

--------------------------------------------------------------------------------
-- showParams -

showParams :: Indent -> [Parameter] -> String
showParams :: Indent -> [Parameter] -> String
showParams Indent
_ [] = String
""
showParams Indent
is ((String
v := String
p):[Parameter]
ps)
  =  Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
v
  forall a. [a] -> [a] -> [a]
++ String
" := "
  forall a. [a] -> [a] -> [a]
++ Indent -> ShowS
showIndent (Indent -> Indent
isucc Indent
is) String
p forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ Indent -> [Parameter] -> String
showParams Indent
is [Parameter]
ps

--------------------------------------------------------------------------------
-- showMessage -

showMessage :: Indent -> Message -> String
showMessage :: Indent -> Message -> String
showMessage Indent
is Message
m = case Message
m of
  Message
MInvalid    -> String
""
  Message String
s -> Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
"message: " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
"\n"
  Params [Parameter]
ps -> Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
"parameters" forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ Indent -> [Parameter] -> String
showParams (Indent -> Indent
isucc Indent
is) [Parameter]
ps

--------------------------------------------------------------------------------
-- showMaybeMessage -

showMaybeMessage :: Indent -> Maybe Message -> String
showMaybeMessage :: Indent -> Maybe Message -> String
showMaybeMessage Indent
_ Maybe Message
Nothing   = String
""
showMaybeMessage Indent
is (Just Message
m) = Indent -> Message -> String
showMessage Indent
is Message
m

--------------------------------------------------------------------------------
-- showCheck -

showCheck :: Indent -> T -> (Maybe Message) -> String
showCheck :: Indent -> T -> Maybe Message -> String
showCheck Indent
is T
t Maybe Message
m =  Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
"check " forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t forall a. [a] -> [a] -> [a]
++ String
"\n"
                 forall a. [a] -> [a] -> [a]
++ Indent -> T -> String
showTLeaf Indent
is' T
t
                 forall a. [a] -> [a] -> [a]
++ Indent -> Maybe Message -> String
showMaybeMessage Indent
is' Maybe Message
m
  where is' :: Indent
is' = Indent -> Indent
isucc Indent
is

--------------------------------------------------------------------------------
-- showCatched -

showCatched :: Indent -> V -> String
showCatched :: Indent -> V -> String
showCatched Indent
is V
v = Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
"catched" forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ Indent -> V -> String
showV (Indent -> Indent
isucc Indent
is) V
v

--------------------------------------------------------------------------------
-- showCatchSubs -

showCatchSubs :: Indent -> V -> String
showCatchSubs :: Indent -> V -> String
showCatchSubs Indent
is V
v = Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
"substitution" forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ Indent -> V -> String
showV (Indent -> Indent
isucc Indent
is) V
v

--------------------------------------------------------------------------------
-- showCatch -

showCatch :: Indent -> T -> Maybe V -> V -> String
showCatch :: Indent -> T -> Maybe V -> V -> String
showCatch Indent
is T
_ Maybe V
Nothing V
v  = Indent -> V -> String
showV Indent
is V
v
showCatch Indent
is T
t (Just V
c) V
v = Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
"catch " forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t forall a. [a] -> [a] -> [a]
++ String
"\n"
                          forall a. [a] -> [a] -> [a]
++ Indent -> V -> String
showCatched Indent
is' V
c
                          forall a. [a] -> [a] -> [a]
++ Indent -> V -> String
showCatchSubs Indent
is' V
v
  where is' :: Indent
is' = Indent -> Indent
isucc Indent
is

--------------------------------------------------------------------------------
-- showNot -

showNot :: Indent -> T -> V -> String
showNot :: Indent -> T -> V -> String
showNot Indent
is T
t V
v = Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
"not " forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ Indent -> V -> String
showV (Indent -> Indent
isucc Indent
is) V
v

--------------------------------------------------------------------------------
-- showVs -

showVs :: Indent -> [V] -> String
showVs :: Indent -> [V] -> String
showVs Indent
_ []      = String
""
showVs Indent
is (V
v:[V]
vs) = Indent -> V -> String
showV Indent
is V
v forall a. [a] -> [a] -> [a]
++ Indent -> [V] -> String
showVs Indent
is [V]
vs

--------------------------------------------------------------------------------
-- showAnd -

showAnd :: Indent -> T -> [V] -> String
showAnd :: Indent -> T -> [V] -> String
showAnd Indent
is T
t [V]
vs = Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
"and " forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t forall a. [a] -> [a] -> [a]
++ String
"\n"
                forall a. [a] -> [a] -> [a]
++ Indent -> [V] -> String
showVs (Indent -> Indent
isucc Indent
is) [V]
vs

--------------------------------------------------------------------------------
-- showOr -

showOr :: Indent -> T -> [V] -> String
showOr :: Indent -> T -> [V] -> String
showOr Indent
is T
t [V]
vs = Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
"or " forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t forall a. [a] -> [a] -> [a]
++ String
"\n"
                forall a. [a] -> [a] -> [a]
++ Indent -> [V] -> String
showVs (Indent -> Indent
isucc Indent
is) [V]
vs

--------------------------------------------------------------------------------
-- showImpl -

showImpl :: Indent -> T -> V -> String
showImpl :: Indent -> T -> V -> String
showImpl Indent
is T
t V
v = Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
"=> " forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t forall a. [a] -> [a] -> [a]
++ String
"\n"
                forall a. [a] -> [a] -> [a]
++ Indent -> V -> String
showV (Indent -> Indent
isucc Indent
is) V
v

--------------------------------------------------------------------------------
-- showDefEqvl -

showDefEqvl :: Indent -> Label -> T -> V -> String
showDefEqvl :: Indent -> Label -> T -> V -> String
showDefEqvl Indent
is Label
l T
t V
v = Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Label
l forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t forall a. [a] -> [a] -> [a]
++ String
"\n"
                     forall a. [a] -> [a] -> [a]
++ Indent -> V -> String
showV (Indent -> Indent
isucc Indent
is) V
v

--------------------------------------------------------------------------------
-- showEqvl -

showEqvl :: Indent -> T -> V -> String
showEqvl :: Indent -> T -> V -> String
showEqvl Indent
is T
t V
v = Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
"<=> " forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t forall a. [a] -> [a] -> [a]
++ String
"\n"
                forall a. [a] -> [a] -> [a]
++ Indent -> V -> String
showV (Indent -> Indent
isucc Indent
is) V
v
--------------------------------------------------------------------------------
-- showForall -

showForall :: Indent -> T -> V -> String
showForall :: Indent -> T -> V -> String
showForall Indent
is T
t V
v = Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
"for all " forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t forall a. [a] -> [a] -> [a]
++ String
"\n"
                  forall a. [a] -> [a] -> [a]
++ Indent -> V -> String
showV (Indent -> Indent
isucc Indent
is) V
v

--------------------------------------------------------------------------------
-- showExist -

showExist :: Indent -> T -> V -> String
showExist :: Indent -> T -> V -> String
showExist Indent
is T
t V
v = Indent -> String
indent Indent
is forall a. [a] -> [a] -> [a]
++ String
"exist " forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t forall a. [a] -> [a] -> [a]
++ String
"\n"
                 forall a. [a] -> [a] -> [a]
++ Indent -> V -> String
showV (Indent -> Indent
isucc Indent
is) V
v
                 
--------------------------------------------------------------------------------
-- showV -

-- | pretty showing a value with the given indentation.
showV :: Indent -> V -> String
showV :: Indent -> V -> String
showV Indent
is V
v = case V
v of
  V Valid
b            -> Indent -> Valid -> String
showValid Indent
is Valid
b
  VFailure e
e     -> forall e. Exception e => Indent -> e -> String
showFailure Indent
is e
e
  VCatch T
t Maybe V
mv V
v  -> Indent -> T -> Maybe V -> V -> String
showCatch Indent
is T
t Maybe V
mv V
v
  VCheck T
t Maybe Message
m     -> Indent -> T -> Maybe Message -> String
showCheck Indent
is T
t Maybe Message
m
  VNot T
t V
v'      -> Indent -> T -> V -> String
showNot Indent
is T
t V
v'
  VAnd T
t [V]
vs      -> Indent -> T -> [V] -> String
showAnd Indent
is T
t [V]
vs
  VOr T
t [V]
vs       -> Indent -> T -> [V] -> String
showOr Indent
is T
t [V]
vs
  VImpl T
t V
v      -> Indent -> T -> V -> String
showImpl Indent
is T
t V
v
  VDefEqvl Label
l T
t V
v -> Indent -> Label -> T -> V -> String
showDefEqvl Indent
is Label
l T
t V
v
  VEqvl T
t V
v      -> Indent -> T -> V -> String
showEqvl Indent
is T
t V
v
  VForall T
t V
v    -> Indent -> T -> V -> String
showForall Indent
is T
t V
v
  VExist T
t V
v     -> Indent -> T -> V -> String
showExist Indent
is T
t V
v


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

-- | determines whether the value is deterministic, i.e. dose not contain a 'VForall'
--   or 'VExist' constructor.
valDeterministic :: V -> Bool
valDeterministic :: V -> Bool
valDeterministic V
v = case V
v of
  VForall T
_ (VAnd T
_ []) -> Bool
True
  VForall T
_ V
_           -> Bool
False
  VExist T
_ (VOr T
_ [])   -> Bool
True
  VExist T
_ V
_            -> Bool
False
  VCatch T
_ Maybe V
Nothing V
v    -> V -> Bool
valDeterministic V
v
  VCatch T
_ (Just V
v) V
w   -> forall b. Boolean b => [b] -> b
and forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map V -> Bool
valDeterministic [V
v,V
w]
  VNot T
_ V
v              -> V -> Bool
valDeterministic V
v
  VAnd T
_ [V]
vs             -> forall b. Boolean b => [b] -> b
and forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map V -> Bool
valDeterministic [V]
vs
  VOr T
_ [V]
vs              -> forall b. Boolean b => [b] -> b
and forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map V -> Bool
valDeterministic [V]
vs
  VImpl T
_ V
v             -> V -> Bool
valDeterministic V
v
  VDefEqvl Label
_ T
_ V
v        -> V -> Bool
valDeterministic V
v
  VEqvl T
_ V
v             -> V -> Bool
valDeterministic V
v
  V
_                     -> Bool
True

--------------------------------------------------------------------------------
-- valT -

-- | validating a value @v@.
valT :: V -> T
valT :: V -> T
valT V
v = case V
v of
  V Valid
t              -> forall x. x -> HNFValue x
HNFValue Valid
t
  VFailure e
e       -> forall x e. Exception e => e -> HNFValue x
Failure e
e
  VCheck T
t Maybe Message
_       -> T
t
  VCatch T
t Maybe V
_ V
_     -> T
t
  VNot T
t V
_         -> T
t
  VAnd T
t [V]
_         -> T
t
  VOr T
t [V]
_          -> T
t
  VImpl T
t V
_        -> T
t
  VDefEqvl Label
_ T
t V
_   -> T
t
  VEqvl T
t V
_        -> T
t
  VForall T
t V
_      -> T
t
  VExist T
t V
_       -> T
t

--------------------------------------------------------------------------------
-- Wide -

-- | the wide for a 'Forall' and 'Exist' resolution.
type Wide = Int

--------------------------------------------------------------------------------
-- value -

-- | evaluates the value of a statement according a given 'Wide' and 'Omega'.
--
--  __Note__
--
--  (1) The only reason to valuate a statement in the 'IO' monad is
--  to be able to catch exceptions. Other interactions with the /real world/ during
--  the valuation are not performed.
--
--  (2) During the evaluation process the given wide and omega will not be changed and as
--  such all /same/ random variables will produce exactly the same samples. This restricts
--  the stochastic, but it is necessary for the sound behavior of the validation of statements.
value :: Statement -> Wide -> Omega -> IO V
value :: Statement -> Int -> Omega -> IO V
value Statement
p Int
w Omega
o = do
  HNFValue Statement
hfp <- forall x. HNFData x => x -> IO (HNFValue x)
hnfValue Statement
p
  case HNFValue Statement
hfp of
    Failure e
e  -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall e. Exception e => e -> V
VFailure e
e)
    HNFValue Statement
p -> Statement -> Int -> Omega -> IO V
val Statement
p Int
w Omega
o
  where
    val :: Statement -> Int -> Omega -> IO V
val Statement
p Int
w Omega
o = case Statement
p of
      Statement
SInvalid     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Valid -> V
V Valid
Invalid
      Statement
SValid       -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Valid -> V
V Valid
Valid
      Bool
b :?> Message
m      -> Bool -> Message -> IO V
valCheck Bool
b Message
m
      Catch Statement
p e -> Statement
h    -> forall e.
Exception e =>
Statement -> (e -> Statement) -> Int -> Omega -> IO V
valCatch Statement
p e -> Statement
h Int
w Omega
o
      Not Statement
p        -> Statement -> Int -> Omega -> IO V
valNot Statement
p Int
w Omega
o
      Statement
a :&& Statement
b      -> [Statement] -> Int -> Omega -> IO V
valAnd [Statement
a,Statement
b] Int
w Omega
o
      And [Statement]
ps       -> [Statement] -> Int -> Omega -> IO V
valAnd [Statement]
ps Int
w Omega
o
      Statement
a :|| Statement
b      -> [Statement] -> Int -> Omega -> IO V
valOr [Statement
a,Statement
b] Int
w Omega
o
      Or [Statement]
ps        -> [Statement] -> Int -> Omega -> IO V
valOr [Statement]
ps Int
w Omega
o
      Statement
a :=> Statement
b      -> [Statement] -> Statement -> Int -> Omega -> IO V
valImpl [Statement
a] Statement
b Int
w Omega
o
      Impl [Statement]
as Statement
b    -> [Statement] -> Statement -> Int -> Omega -> IO V
valImpl [Statement]
as Statement
b Int
w Omega
o
      Label
l :<=>: Statement
p    -> Label -> Statement -> Int -> Omega -> IO V
valDefEqvl Label
l Statement
p Int
w Omega
o
      Statement
a :<=> Statement
b     -> [Statement] -> Int -> Omega -> IO V
valEqvl [Statement
a,Statement
b] Int
w Omega
o
      Eqvl [Statement]
as      -> [Statement] -> Int -> Omega -> IO V
valEqvl [Statement]
as Int
w Omega
o
      Forall X x
x x -> Statement
px  -> forall x. X x -> (x -> Statement) -> Int -> Omega -> IO V
valForall X x
x x -> Statement
px Int
w Omega
o
      Exist X x
x x -> Statement
px   -> forall x. X x -> (x -> Statement) -> Int -> Omega -> IO V
valExist X x
x x -> Statement
px Int
w Omega
o

----------------------------------------
-- valCheck -

valCheck :: Bool -> Message -> IO V
valCheck :: Bool -> Message -> IO V
valCheck Bool
b Message
m = do
  HNFValue Bool
hfb <- forall x. HNFData x => x -> IO (HNFValue x)
hnfValue Bool
b
  case HNFValue Bool
hfb of
    Failure e
e -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> Maybe Message -> V
VCheck (forall x e. Exception e => e -> HNFValue x
Failure e
e) forall a. Maybe a
Nothing
    HNFValue Bool
b -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ case Bool
b of
      Bool
True    -> T -> Maybe Message -> V
VCheck (forall x. x -> HNFValue x
HNFValue Valid
Valid) forall a. Maybe a
Nothing
      Bool
False   -> T -> Maybe Message -> V
VCheck (forall x. x -> HNFValue x
HNFValue Valid
Invalid) (forall a. a -> Maybe a
Just Message
m)

----------------------------------------
-- valCatch -

valCatch :: Exception e => Statement -> (e -> Statement) -> Wide -> Omega -> IO V
valCatch :: forall e.
Exception e =>
Statement -> (e -> Statement) -> Int -> Omega -> IO V
valCatch Statement
p e -> Statement
h Int
w Omega
o = do
  V
v <- Statement -> Int -> Omega -> IO V
value Statement
p Int
w Omega
o
  case V -> T
valT V
v of
    Failure e
s -> case forall s e x.
(Exception s, Exception e) =>
(e -> x) -> s -> Maybe e
castException e -> Statement
h e
s of
                   Maybe e
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> Maybe V -> V -> V
VCatch (forall x e. Exception e => e -> HNFValue x
Failure e
s) forall a. Maybe a
Nothing V
v
                   Just e
e  -> do
                     V
v' <- Statement -> Int -> Omega -> IO V
value (e -> Statement
h e
e) Int
w Omega
o
                     forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> Maybe V -> V -> V
VCatch (V -> T
valT V
v') (forall a. a -> Maybe a
Just V
v) V
v' 
    T
t         -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> Maybe V -> V -> V
VCatch T
t forall a. Maybe a
Nothing V
v

  where castException :: (Exception s,Exception e) => (e -> x) -> s -> Maybe e
        castException :: forall s e x.
(Exception s, Exception e) =>
(e -> x) -> s -> Maybe e
castException e -> x
_ s
s = forall e. Exception e => SomeException -> Maybe e
fromException forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall e. Exception e => e -> SomeException
toException s
s

----------------------------------------
-- valNot -

valNot :: Statement -> Wide -> Omega -> IO V
valNot :: Statement -> Int -> Omega -> IO V
valNot Statement
p Int
w Omega
o = do
  V
v <- Statement -> Int -> Omega -> IO V
value Statement
p Int
w Omega
o
  case V -> T
valT V
v of
    Failure e
e  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> V -> V
VNot (forall x e. Exception e => e -> HNFValue x
Failure e
e) V
v
    HNFValue Valid
t -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> V -> V
VNot (forall x. x -> HNFValue x
HNFValue (forall b. Boolean b => b -> b
not Valid
t)) V
v

----------------------------------------
-- valAnd -

valAnd :: [Statement] -> Wide -> Omega -> IO V
valAnd :: [Statement] -> Int -> Omega -> IO V
valAnd [Statement]
ps Int
w Omega
o = do
  HNFValue [Statement]
hfps <- forall x. HNFData x => x -> IO (HNFValue x)
hnfValue [Statement]
ps
  case HNFValue [Statement]
hfps of
    Failure e
e   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> [V] -> V
VAnd (forall x e. Exception e => e -> HNFValue x
Failure e
e) []
    HNFValue [Statement]
ps -> Valid -> [Statement] -> [V] -> IO V
allTrue Valid
Valid [Statement]
ps []
  where allTrue :: Valid -> [Statement] -> [V] -> IO V
allTrue Valid
s [] [V]
vs                    = forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> [V] -> V
VAnd (forall x. x -> HNFValue x
HNFValue Valid
s) [V]
vs
        allTrue Valid
s [Statement]
_ [V]
vs | Valid
s forall a. Ord a => a -> a -> Bool
< Valid
ProbablyValid = forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> [V] -> V
VAnd (forall x. x -> HNFValue x
HNFValue Valid
s) [V]
vs  
        allTrue Valid
s (Statement
p:[Statement]
ps) [V]
vs                = do
          V
v <- Statement -> Int -> Omega -> IO V
value Statement
p Int
w Omega
o 
          case V -> T
valT V
v of
            HNFValue Valid
t -> Valid -> [Statement] -> [V] -> IO V
allTrue (Valid
sforall b. Boolean b => b -> b -> b
&&Valid
t) [Statement]
ps (V
vforall a. a -> [a] -> [a]
:[V]
vs)
            T
f          -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> [V] -> V
VAnd T
f (V
vforall a. a -> [a] -> [a]
:[V]
vs)

----------------------------------------
-- valOr -

valOr :: [Statement] -> Wide -> Omega -> IO V
valOr :: [Statement] -> Int -> Omega -> IO V
valOr [Statement]
ps Int
w Omega
o = do
  HNFValue [Statement]
hfps <- forall x. HNFData x => x -> IO (HNFValue x)
hnfValue [Statement]
ps
  case HNFValue [Statement]
hfps of
    Failure e
e  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> [V] -> V
VOr (forall x e. Exception e => e -> HNFValue x
Failure e
e) []
    HNFValue [Statement]
ps -> Valid -> [Statement] -> [V] -> IO V
existTrue Valid
Invalid [Statement]
ps []
  where existTrue :: Valid -> [Statement] -> [V] -> IO V
existTrue Valid
s [] [V]
vs                      = forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> [V] -> V
VOr (forall x. x -> HNFValue x
HNFValue Valid
s) [V]
vs
        existTrue Valid
s [Statement]
_ [V]
vs | Valid
s forall a. Ord a => a -> a -> Bool
> Valid
ProbablyInvalid = forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> [V] -> V
VOr (forall x. x -> HNFValue x
HNFValue Valid
s) [V]
vs
        existTrue Valid
s (Statement
p:[Statement]
ps) [V]
vs                  = do
          V
v <- Statement -> Int -> Omega -> IO V
value Statement
p Int
w Omega
o
          case V -> T
valT V
v of
            HNFValue Valid
t -> Valid -> [Statement] -> [V] -> IO V
existTrue (Valid
sforall b. Boolean b => b -> b -> b
||Valid
t) [Statement]
ps (V
vforall a. a -> [a] -> [a]
:[V]
vs)
            T
f          -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> [V] -> V
VOr T
f (V
vforall a. a -> [a] -> [a]
:[V]
vs)

----------------------------------------
-- valImpl -

valImpl :: [Statement] -> Statement -> Wide -> Omega -> IO V
valImpl :: [Statement] -> Statement -> Int -> Omega -> IO V
valImpl [Statement]
pms Statement
cn Int
w Omega
o = do
  V
v <- Statement -> Int -> Omega -> IO V
value ([Statement] -> Statement
Or [Statement -> Statement
Not (Label
PrmsLabel -> Statement -> Statement
:<=>:([Statement] -> Statement
And [Statement]
pms)),(Label
CnclLabel -> Statement -> Statement
:<=>:Statement
cn)]) Int
w Omega
o
  forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> V -> V
VImpl (V -> T
valT V
v) V
v 

----------------------------------------
-- valDefEqvl -

valDefEqvl :: Label -> Statement -> Wide -> Omega -> IO V
valDefEqvl :: Label -> Statement -> Int -> Omega -> IO V
valDefEqvl Label
l Statement
p Int
w Omega
o = do
  V
v <- Statement -> Int -> Omega -> IO V
value Statement
p Int
w Omega
o
  forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Label -> T -> V -> V
VDefEqvl Label
l (V -> T
valT V
v) V
v

----------------------------------------
-- valEqvl -

valEqvl :: [Statement] -> Wide -> Omega -> IO V
valEqvl :: [Statement] -> Int -> Omega -> IO V
valEqvl [] Int
_ Omega
_     = forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Valid -> V
V Valid
Valid
valEqvl (Statement
a:[Statement]
as) Int
w Omega
o = do
  V
v <- Statement -> Int -> Omega -> IO V
value ([Statement] -> Statement
And [Statement]
impls) Int
w Omega
o
  forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> V -> V
VEqvl (V -> T
valT V
v) V
v
  where impls :: [Statement]
impls = forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Statement -> Statement -> Statement
(:=>)) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (Statement
aforall a. a -> [a] -> [a]
:[Statement]
as) ([Statement]
asforall a. [a] -> [a] -> [a]
++[Statement
a])

----------------------------------------
-- valForall -

valForall :: X x -> (x -> Statement) -> Wide -> Omega -> IO V
valForall :: forall x. X x -> (x -> Statement) -> Int -> Omega -> IO V
valForall X x
x x -> Statement
p Int
w Omega
o = do
  V
v <- Statement -> Int -> Omega -> IO V
value ([Statement] -> Statement
And [Statement]
ps) Int
w Omega
o
  case V
v of
    VAnd T
t [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> V -> V
VForall T
t V
v
    V
_         -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> V -> V
VForall (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Valid
ProbablyValidforall b. Boolean b => b -> b -> b
&&) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ V -> T
valT V
v) V
v
  where ps :: [Statement]
ps = forall a b. (a -> b) -> [a] -> [b]
map x -> Statement
p forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
w forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. X x -> Omega -> [x]
samples X x
x Omega
o

----------------------------------------
-- valExist -
valExist :: X x -> (x -> Statement) -> Wide -> Omega -> IO V
valExist :: forall x. X x -> (x -> Statement) -> Int -> Omega -> IO V
valExist X x
x x -> Statement
p Int
w Omega
o = do
  V
v <- Statement -> Int -> Omega -> IO V
value ([Statement] -> Statement
Or [Statement]
ps) Int
w Omega
o
  case V
v of
    VOr T
t [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> V -> V
VExist T
t V
v
    V
_        -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> V -> V
VExist (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Valid
ProbablyInvalidforall b. Boolean b => b -> b -> b
||) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ V -> T
valT V
v) V
v
  where ps :: [Statement]
ps = forall a b. (a -> b) -> [a] -> [b]
map x -> Statement
p forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
w forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. X x -> Omega -> [x]
samples X x
x Omega
o


--------------------------------------------------------------------------------
-- validateStoch -

-- | validates the statement according to a given 'Wide' and 'Omega'. For
--   deterministic statements better use 'validateDet' and for non deterministic
--   or to get more information 'OAlg.Control.Validate.validate'.
validateStoch :: Statement -> Wide -> Omega -> IO Valid
validateStoch :: Statement -> Int -> Omega -> IO Valid
validateStoch Statement
p Int
w Omega
o = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall x. HNFValue x -> x
fromHNFValue forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. V -> T
valT) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Statement -> Int -> Omega -> IO V
value Statement
p Int
w Omega
o

--------------------------------------------------------------------------------
-- validateDet -

-- | validation for /deterministic/ statements.
--
--  __Definition__ A statement s is called __/deterministic/__ if and only if it dose not depend
--  on the stochastic nor on the state of the machine.
--
-- __Examples__
--
-- >>> validateDet SValid
-- True
--
-- >>> validateDet (Forall xBool (\_ -> SValid))
-- *** Exception: NonDeterministic
--
-- >>> validateDet (SValid || Exist xInt (\i -> (i==0):?>MInvalid))
-- True
validateDet :: Statement -> Bool
validateDet :: Statement -> Bool
validateDet Statement
p = forall a. IO a -> a
unsafePerformIO forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ do
  V
v <- Statement -> Int -> Omega -> IO V
value Statement
p (forall a e. Exception e => e -> a
throw ValidateingException
NonDeterministic) (forall a e. Exception e => e -> a
throw ValidateingException
NonDeterministic)
  case V -> T
valT V
v of
    Failure e
e  -> forall a e. Exception e => e -> a
throw e
e
    HNFValue Valid
s -> case Valid
s of
      Valid
Valid    -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
      Valid
Invalid  -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Valid
st       -> forall a e. Exception e => e -> a
throw forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ String -> AlgebraicException
ImplementationError
                    forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (String
"deterministic statement with " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Valid
st)

--------------------------------------------------------------------------------
-- isTrueT -

-- | checking for being 'True'.
isTrueT :: T -> Bool
isTrueT :: T -> Bool
isTrueT (HNFValue Valid
sb ) = Valid
ProbablyValid forall a. Ord a => a -> a -> Bool
<= Valid
sb
isTrueT T
_              = Bool
False

--------------------------------------------------------------------------------
-- rdcTrue -

-- | reduces true valus to its relevant part.
rdcTrue :: V -> Maybe V
rdcTrue :: V -> Maybe V
rdcTrue V
v | forall b. Boolean b => b -> b
not forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> Bool
isTrueT forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ V -> T
valT V
v = forall a. Maybe a
Nothing
rdcTrue V
v = case V
v of
  V Valid
_             -> forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VCheck T
_ Maybe Message
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VCatch T
t Maybe V
e V
v'   -> V -> Maybe V
rdcTrue V
v' 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
. T -> Maybe V -> V -> V
VCatch T
t Maybe V
e
  VNot T
t V
v'       -> V -> Maybe V
rdcFalse V
v' 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
. T -> V -> V
VNot T
t 
  VAnd T
t [V]
vs       -> (forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map V -> Maybe V
rdcTrue [V]
vs) 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
. T -> [V] -> V
VAnd T
t
  VOr T
t (V
v':[V]
_)    -> V -> Maybe V
rdcTrue V
v' 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
. T -> [V] -> V
VOr T
t forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (m :: * -> *) a. Monad m => a -> m a
return 
  VImpl T
t V
v'      -> V -> Maybe V
rdcTrue V
v' 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
. T -> V -> V
VImpl T
t
  VEqvl T
t V
v'      -> V -> Maybe V
rdcTrue V
v' 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
. T -> V -> V
VEqvl T
t
  VDefEqvl Label
l T
t V
v' -> V -> Maybe V
rdcTrue V
v' 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
. Label -> T -> V -> V
VDefEqvl Label
l T
t
  VForall T
t V
v'    -> V -> Maybe V
rdcTrue V
v' 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
. T -> V -> V
VForall T
t
  VExist T
t V
v'     -> V -> Maybe V
rdcTrue V
v' 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
. T -> V -> V
VExist T
t
  V
_               -> forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
-- rdcFalse -

-- | checking for being 'False'.
isFalseT :: T -> Bool
isFalseT :: T -> Bool
isFalseT (HNFValue Valid
sb) = Valid
sb forall a. Ord a => a -> a -> Bool
< Valid
ProbablyValid
isFalseT T
_             = Bool
False

-- | reduces false valus to its relevant part.
rdcFalse :: V -> Maybe V
rdcFalse :: V -> Maybe V
rdcFalse V
v | forall b. Boolean b => b -> b
not forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> Bool
isFalseT forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ V -> T
valT V
v = forall a. Maybe a
Nothing
rdcFalse V
v = case V
v of
  V Valid
_             -> forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VCheck T
_ Maybe Message
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VCatch T
t Maybe V
e V
v'   -> V -> Maybe V
rdcFalse V
v' 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
. T -> Maybe V -> V -> V
VCatch T
t Maybe V
e
  VNot T
t V
v'       -> V -> Maybe V
rdcTrue V
v' 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
. T -> V -> V
VNot T
t
  VAnd T
t (V
v':[V]
_)   -> V -> Maybe V
rdcFalse V
v' 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
. T -> [V] -> V
VAnd T
t forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (m :: * -> *) a. Monad m => a -> m a
return
  VOr T
t [V]
vs        -> (forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence 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) 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
. T -> [V] -> V
VOr T
t
  VImpl T
t V
v'      -> V -> Maybe V
rdcFalse V
v' 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
. T -> V -> V
VImpl T
t 
  VEqvl T
t V
v'      -> V -> Maybe V
rdcFalse V
v' 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
. T -> V -> V
VEqvl T
t
  VDefEqvl Label
l T
t V
v' -> V -> Maybe V
rdcFalse V
v' 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
. Label -> T -> V -> V
VDefEqvl Label
l T
t
  VForall T
t V
v'    -> V -> Maybe V
rdcFalse V
v' 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
. T -> V -> V
VForall T
t
  VExist T
t V
v'     -> V -> Maybe V
rdcFalse V
v' 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
. T -> V -> V
VExist T
t
  V
_               -> forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
-- rdcDndPrms -

-- | gets the conclusion - if there is - of a true implication.
--
--   pre: v is true implication
getCncl :: V -> Maybe V
getCncl :: V -> Maybe V
getCncl (VImpl (HNFValue Valid
Valid) (VOr T
_ [V
c,V
_])) = forall (m :: * -> *) a. Monad m => a -> m a
return V
c
getCncl V
_                                      = forall a. Maybe a
Nothing

-- | reduces true implication having no conclusion to the relevant
--   of its false premisis.
rdcFalsePrms :: V -> Maybe V
rdcFalsePrms :: V -> Maybe V
rdcFalsePrms (VImpl (HNFValue Valid
Valid) (VOr T
_ [VNot (HNFValue Valid
Valid) V
p])) = V -> Maybe V
rdcFalse V
p
rdcFalsePrms V
_                                                          = forall a. Maybe a
Nothing

-- | reduces false values having denied premisis
rdcDndPrmsFalse :: V -> Maybe V
rdcDndPrmsFalse :: V -> Maybe V
rdcDndPrmsFalse V
v | forall b. Boolean b => b -> b
not forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> Bool
isFalseT forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ V -> T
valT V
v = forall a. Maybe a
Nothing
rdcDndPrmsFalse V
v = case V
v of
  VCatch T
t Maybe V
e V
v'       -> V -> Maybe V
rdcDndPrmsFalse V
v' 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
. T -> Maybe V -> V -> V
VCatch T
t Maybe V
e
  VNot T
t V
v'           -> V -> Maybe V
rdcDndPrms V
v' 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
. T -> V -> V
VNot T
t
  VAnd T
t (V
v':[V]
_)       -> V -> Maybe V
rdcDndPrmsFalse V
v' 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
. T -> [V] -> V
VAnd T
t forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (m :: * -> *) a. Monad m => a -> m a
return
  VOr T
t [V]
vs            -> (forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map V -> Maybe V
rdcDndPrmsFalse [V]
vs) 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
. T -> [V] -> V
VOr T
t
  VDefEqvl Label
l T
t V
v'     -> V -> Maybe V
rdcDndPrmsFalse V
v' 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
. Label -> T -> V -> V
VDefEqvl Label
l T
t
  VForall T
t V
v'        -> V -> Maybe V
rdcDndPrmsFalse V
v' 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
. T -> V -> V
VForall T
t
  VExist T
_ (VOr T
_ []) -> forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VExist T
t V
v'         -> V -> Maybe V
rdcDndPrmsFalse V
v' 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
. T -> V -> V
VExist T
t
  V
_                   -> forall a. Maybe a
Nothing

-- | reduces ture values - having implications with no conclusions, i.e. denied premises
--   - to its relevant part.
rdcDndPrms :: V -> Maybe V
rdcDndPrms :: V -> Maybe V
rdcDndPrms V
v | forall b. Boolean b => b -> b
not forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ T -> Bool
isTrueT forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ V -> T
valT V
v = forall a. Maybe a
Nothing
rdcDndPrms V
v = case V
v of
  VImpl T
_ V
_             -> case V -> Maybe V
getCncl V
v of
                             Maybe V
Nothing -> V -> Maybe V
rdcFalsePrms V
v
                             Just V
_  -> forall a. Maybe a
Nothing
  VCatch T
t Maybe V
e V
v'         -> V -> Maybe V
rdcDndPrms V
v' 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
. T -> Maybe V -> V -> V
VCatch T
t Maybe V
e
  VNot T
t V
v'             -> V -> Maybe V
rdcDndPrmsFalse V
v' 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
. T -> V -> V
VNot T
t 
  VAnd T
t [V]
vs             -> (forall v. [Maybe v] -> Maybe [v]
exstJust 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) 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
. T -> [V] -> V
VAnd T
t
  VOr T
t [V]
vs              -> (forall v. [Maybe v] -> Maybe [v]
exstJust 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) 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
. T -> [V] -> V
VOr T
t
  -- VEqvl t v'         -> are considered not having denied premises
  VDefEqvl Label
l T
t V
v'       -> V -> Maybe V
rdcDndPrms V
v' 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
. Label -> T -> V -> V
VDefEqvl Label
l T
t
  VForall T
_ (VAnd T
_ []) -> forall (m :: * -> *) a. Monad m => a -> m a
return V
v  -- XEmpty or wide = 0!
  VForall T
t V
v'          -> V -> Maybe V
rdcDndPrms V
v' 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
. T -> V -> V
VForall T
t
  VExist T
t V
v'           -> V -> Maybe V
rdcDndPrms V
v' 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
. T -> V -> V
VExist T
t
  V
_                     -> forall a. Maybe a
Nothing
  
--------------------------------------------------------------------------------
-- rdcFailed -

-- | reduces failed values to its relevant part.
rdcFailed :: V -> Maybe V
rdcFailed :: V -> Maybe V
rdcFailed V
v = case V
v of
  VFailure e
_                  -> forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VCheck (Failure e
_) Maybe Message
_        -> forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VCatch (Failure e
_) Maybe V
_ V
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VNot f :: T
f@(Failure e
_) V
v'       -> V -> Maybe V
rdcFailed V
v' 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
. T -> V -> V
VNot T
f
  VAnd f :: T
f@(Failure e
_) (V
v':[V]
_)   -> V -> Maybe V
rdcFailed V
v' 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
. T -> [V] -> V
VAnd T
f forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (m :: * -> *) a. Monad m => a -> m a
return
  VAnd (Failure e
_) []         -> forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VOr f :: T
f@(Failure e
_) (V
v':[V]
_)    -> V -> Maybe V
rdcFailed V
v' 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
. T -> [V] -> V
VOr T
f forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (m :: * -> *) a. Monad m => a -> m a
return
  VOr (Failure e
_) []          -> forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VImpl f :: T
f@(Failure e
_) V
v'      -> V -> Maybe V
rdcFailed V
v' 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
. T -> V -> V
VImpl T
f
  VEqvl f :: T
f@(Failure e
_) V
v'      -> V -> Maybe V
rdcFailed V
v' 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
. T -> V -> V
VEqvl T
f
  VDefEqvl Label
l f :: T
f@(Failure e
_) V
v' -> V -> Maybe V
rdcFailed V
v' 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
. Label -> T -> V -> V
VDefEqvl Label
l T
f
  VForall f :: T
f@(Failure e
_) V
v'    -> V -> Maybe V
rdcFailed V
v' 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
. T -> V -> V
VForall T
f
  VExist f :: T
f@(Failure e
_) V
v'     -> V -> Maybe V
rdcFailed V
v' 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
. T -> V -> V
VExist T
f
  V
_                           -> forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
-- relevantLabel -

-- | defines the relevant labels to be /counted/ by 'tests'.
relevantLabel :: Label -> Bool
relevantLabel :: Label -> Bool
relevantLabel Label
l = case Label
l of
                    Label
Prms -> Bool
False
                    Label
Cncl -> Bool
False
                    Label
_    -> Bool
True 

--------------------------------------------------------------------------------
-- tests -

-- | path of strings.
type SPath = [String]

-- | the list of all relevant tests - i.e @'VDedEqvl l _@ where @l = 'Label' _@
--   - together with the number of tests.
tests :: V -> [(Int,SPath)]
tests :: V -> [(Int, [String])]
tests V
v = case V
v of
  VDefEqvl Label
l T
_ V
v' | Label -> Bool
relevantLabel Label
l -> forall a b. (a -> b) -> [a] -> [b]
map (\(Int
n,[String]
p) -> (Int
n,forall a. Show a => a -> String
show Label
lforall a. a -> [a] -> [a]
:[String]
p)) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ V -> [(Int, [String])]
tests V
v'
                  | Bool
otherwise       -> V -> [(Int, [String])]
tests V
v'
  VCatch T
_ Maybe V
_ V
v'   -> forall {a}. (Int, [a])
t1 forall a. a -> [a] -> [a]
: V -> [(Int, [String])]
tests V
v'
  VNot T
_ V
v'       -> forall {a}. (Int, [a])
t1 forall a. a -> [a] -> [a]
: V -> [(Int, [String])]
tests V
v'
  VAnd T
_ [V]
vs       -> forall {a}. (Int, [a])
t1 forall a. a -> [a] -> [a]
: (forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map V -> [(Int, [String])]
tests forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [V]
vs)
  VOr T
_ [V]
vs        -> forall {a}. (Int, [a])
t1 forall a. a -> [a] -> [a]
: (forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map V -> [(Int, [String])]
tests forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [V]
vs)
  VImpl T
_ V
v'      -> forall {a}. (Int, [a])
t1 forall a. a -> [a] -> [a]
: V -> [(Int, [String])]
tests V
v'
  VEqvl T
_ V
v'      -> forall {a}. (Int, [a])
t1 forall a. a -> [a] -> [a]
: V -> [(Int, [String])]
tests V
v'
  VForall T
_ V
v'    -> forall {a}. (Int, [a])
t1 forall a. a -> [a] -> [a]
: V -> [(Int, [String])]
tests V
v'
  VExist T
_ V
v'     -> forall {a}. (Int, [a])
t1 forall a. a -> [a] -> [a]
: V -> [(Int, [String])]
tests V
v'
  V
_               -> [forall {a}. (Int, [a])
t1]
  where t1 :: (Int, [a])
t1 = (Int
1,[])

----------------------------------------
-- cntTests -

-- | number of 'tests'.
cntTests :: V -> Int
cntTests :: V -> Int
cntTests V
v = case V
v of
  VDefEqvl Label
_ T
_ V
v' -> V -> Int
cntTests V
v'
  VAnd T
_ [V]
vs       -> Int
1forall a. Num a => a -> a -> a
+forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Num a => a -> a -> a
(+) Int
0 (forall a b. (a -> b) -> [a] -> [b]
map V -> Int
cntTests [V]
vs)
  VOr T
_ [V]
vs        -> Int
1forall a. Num a => a -> a -> a
+forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Num a => a -> a -> a
(+) Int
0 (forall a b. (a -> b) -> [a] -> [b]
map V -> Int
cntTests [V]
vs)
  VCatch T
_ Maybe V
_ V
v'   -> Int
1forall a. Num a => a -> a -> a
+V -> Int
cntTests V
v'
  VNot T
_ V
v'       -> Int
1forall a. Num a => a -> a -> a
+V -> Int
cntTests V
v'
  VImpl T
_ V
v'      -> Int
1forall a. Num a => a -> a -> a
+V -> Int
cntTests V
v'
  VEqvl T
_ V
v'      -> Int
1forall a. Num a => a -> a -> a
+V -> Int
cntTests V
v'
  VForall T
_ V
v'    -> Int
1forall a. Num a => a -> a -> a
+V -> Int
cntTests V
v'
  VExist T
_ V
v'     -> Int
1forall a. Num a => a -> a -> a
+V -> Int
cntTests V
v'
  V
_               -> Int
1


-- | number of 'tests' for true values. __Note__ Before counting the tests they
--   will be first reduced to there relevant part (see 'rdcTrue').
cntTestsRdcTrue :: V -> Int
cntTestsRdcTrue :: V -> Int
cntTestsRdcTrue = forall a. a -> Maybe a -> a
fromMaybe Int
0 forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap V -> Int
cntTests forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. V -> Maybe V
rdcTrue
  -- sum . map fst . fromMaybe [] . fmap tests . rdcTrue

-- | number of 'tests' for false values. __Note__ Before counting the tests they
--   will be first reduced to there relevant part (see 'rdcFalse').
cntTestsRdcFalse :: V -> Int
cntTestsRdcFalse :: V -> Int
cntTestsRdcFalse = forall a. a -> Maybe a -> a
fromMaybe Int
0 forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap V -> Int
cntTests forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. V -> Maybe V
rdcFalse
  -- sum . map fst . fromMaybe [] . fmap tests . rdcFalse

-- | number of 'tests' for values containing denied premises. __Note__ Before counting
--   the tests they will be first reduced to there relevant part (see 'rdcDndPrms').
cntTestsRdcDndPrms :: V -> Int
cntTestsRdcDndPrms :: V -> Int
cntTestsRdcDndPrms = forall a. a -> Maybe a -> a
fromMaybe Int
0 forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap V -> Int
cntTests forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. V -> Maybe V
rdcDndPrms
  -- sum . map fst . fromMaybe [] . fmap tests . rdcDndPrms

-- | number of 'tests' for failed values. __Note__ Before counting the tests they
--   will be first reduced to there relevant part (see 'rdcFailed').
cntTestsRdcFailed :: V -> Int
cntTestsRdcFailed :: V -> Int
cntTestsRdcFailed = forall a. a -> Maybe a -> a
fromMaybe Int
0 forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap V -> Int
cntTests forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. V -> Maybe V
rdcFailed

--------------------------------------------------------------------------------
-- xValue' -

-- | @xWO l h@ is the random variable over wide and omgea, where the wide is bounded between @l@ and
-- @h@. 
xWO :: Wide -> Wide -> X (Wide,Omega) 
xWO :: Int -> Int -> X (Int, Omega)
xWO Int
l Int
h = forall a b. X a -> X b -> X (a, b)
xTupple2 (Int -> Int -> X Int
xIntB Int
l Int
h) X Omega
xOmega

-- | random variable of valuation values according to the randomly given 'Wide' and 'Omega'.
xValue :: Statement -> X (Wide,Omega) -> X (IO V)
xValue :: Statement -> X (Int, Omega) -> X (IO V)
xValue Statement
p = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Statement -> Int -> Omega -> IO V
value Statement
p

-- | pretty showing the value of a statement according to the given 'Wide' and randomly given 'Omega'. 
showVStatement :: Wide -> Statement -> IO ()
showVStatement :: Int -> Statement -> IO ()
showVStatement Int
w Statement
s = do
  Omega
o <- IO Omega
getOmega
  V
v <- Statement -> Int -> Omega -> IO V
value Statement
s Int
w Omega
o
  String -> IO ()
putStr forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Indent -> V -> String
showV (String -> Indent
indent0 String
"  ") V
v