{-# 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 hiding ((||),and,(&&),not) -- (Num(..),Bounded(..))


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

import System.IO.Unsafe

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

import OAlg.Data.Logical
import OAlg.Data.Boolean.Definition
import OAlg.Data.X
import OAlg.Data.Show 
import OAlg.Data.Maybe
import OAlg.Data.Canonical

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

-- ValidateingException -


-- | validating exceptions which are sub exceptions from 'SomeOAlgException'.

data ValidateingException
  = NonDeterministic
  deriving (ValidateingException -> ValidateingException -> Bool
(ValidateingException -> ValidateingException -> Bool)
-> (ValidateingException -> ValidateingException -> Bool)
-> Eq ValidateingException
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ValidateingException -> ValidateingException -> Bool
== :: ValidateingException -> ValidateingException -> Bool
$c/= :: ValidateingException -> ValidateingException -> Bool
/= :: ValidateingException -> ValidateingException -> Bool
Eq,Int -> ValidateingException -> ShowS
[ValidateingException] -> ShowS
ValidateingException -> String
(Int -> ValidateingException -> ShowS)
-> (ValidateingException -> String)
-> ([ValidateingException] -> ShowS)
-> Show ValidateingException
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ValidateingException -> ShowS
showsPrec :: Int -> ValidateingException -> ShowS
$cshow :: ValidateingException -> String
show :: ValidateingException -> String
$cshowList :: [ValidateingException] -> ShowS
showList :: [ValidateingException] -> ShowS
Show)

instance Exception ValidateingException where
  toException :: ValidateingException -> SomeException
toException   = ValidateingException -> SomeException
forall e. Exception e => e -> SomeException
oalgExceptionToException
  fromException :: SomeException -> Maybe ValidateingException
fromException = SomeException -> Maybe ValidateingException
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
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
    Prp String
p   -> String
"prp" String -> ShowS
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) = String -> [String] -> String
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
(Int -> Message -> ShowS)
-> (Message -> String) -> ([Message] -> ShowS) -> Show Message
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Message -> ShowS
showsPrec :: Int -> Message -> ShowS
$cshow :: Message -> String
show :: Message -> String
$cshowList :: [Message] -> ShowS
showList :: [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)   = Verbosity -> [Parameter] -> String
forall a. Verbose a => Verbosity -> a -> String
vshow Verbosity
v [Parameter]
ps
  vshow Verbosity
_ Message
m             = Message -> String
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 Logical Statement where
  || :: Statement -> Statement -> Statement
(||)  = Statement -> Statement -> Statement
(:||)
  && :: Statement -> Statement -> Statement
(&&)  = Statement -> Statement -> Statement
(:&&)
  
instance Boolean Statement where
  false :: Statement
false = Statement
SInvalid
  true :: Statement
true  = Statement
SValid
  not :: Statement -> Statement
not   = Statement -> Statement
Not
  or :: [Statement] -> Statement
or    = [Statement] -> Statement
Or
  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 a -> a -> Bool
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 a -> a -> Bool
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 Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
|| 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
(Int -> Valid -> ShowS)
-> (Valid -> String) -> ([Valid] -> ShowS) -> Show Valid
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Valid -> ShowS
showsPrec :: Int -> Valid -> ShowS
$cshow :: Valid -> String
show :: Valid -> String
$cshowList :: [Valid] -> ShowS
showList :: [Valid] -> ShowS
Show,Valid -> Valid -> Bool
(Valid -> Valid -> Bool) -> (Valid -> Valid -> Bool) -> Eq Valid
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Valid -> Valid -> Bool
== :: Valid -> Valid -> Bool
$c/= :: Valid -> Valid -> Bool
/= :: Valid -> Valid -> Bool
Eq,Eq Valid
Eq Valid =>
(Valid -> Valid -> Ordering)
-> (Valid -> Valid -> Bool)
-> (Valid -> Valid -> Bool)
-> (Valid -> Valid -> Bool)
-> (Valid -> Valid -> Bool)
-> (Valid -> Valid -> Valid)
-> (Valid -> Valid -> Valid)
-> Ord 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
$ccompare :: Valid -> Valid -> Ordering
compare :: Valid -> Valid -> Ordering
$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
>= :: Valid -> Valid -> Bool
$cmax :: Valid -> Valid -> Valid
max :: Valid -> Valid -> Valid
$cmin :: Valid -> Valid -> Valid
min :: Valid -> Valid -> Valid
Ord,Int -> Valid
Valid -> Int
Valid -> [Valid]
Valid -> Valid
Valid -> Valid -> [Valid]
Valid -> Valid -> Valid -> [Valid]
(Valid -> Valid)
-> (Valid -> Valid)
-> (Int -> Valid)
-> (Valid -> Int)
-> (Valid -> [Valid])
-> (Valid -> Valid -> [Valid])
-> (Valid -> Valid -> [Valid])
-> (Valid -> Valid -> Valid -> [Valid])
-> Enum 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
$csucc :: Valid -> Valid
succ :: Valid -> Valid
$cpred :: Valid -> Valid
pred :: Valid -> Valid
$ctoEnum :: Int -> Valid
toEnum :: Int -> Valid
$cfromEnum :: Valid -> Int
fromEnum :: Valid -> Int
$cenumFrom :: Valid -> [Valid]
enumFrom :: Valid -> [Valid]
$cenumFromThen :: Valid -> Valid -> [Valid]
enumFromThen :: Valid -> Valid -> [Valid]
$cenumFromTo :: Valid -> Valid -> [Valid]
enumFromTo :: Valid -> Valid -> [Valid]
$cenumFromThenTo :: Valid -> Valid -> Valid -> [Valid]
enumFromThenTo :: Valid -> Valid -> Valid -> [Valid]
Enum,Valid
Valid -> Valid -> Bounded Valid
forall a. a -> a -> Bounded a
$cminBound :: Valid
minBound :: Valid
$cmaxBound :: Valid
maxBound :: Valid
Bounded)

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

instance Logical Valid where
  Valid
a || :: Valid -> Valid -> Valid
|| Valid
b  | Valid
a Valid -> Valid -> Bool
forall a. Eq a => a -> a -> Bool
== Valid
Valid = Valid
a -- to make (||) in its first argument lazy

          | Bool
otherwise  = case Valid
a Valid -> Valid -> Ordering
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 Valid -> Valid -> Bool
forall a. Eq a => a -> a -> Bool
== Valid
Invalid = Valid
a -- to make (&&) in its first argument lazy

          | Bool
otherwise   = case Valid
a Valid -> Valid -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Valid
b of
                            Ordering
LT -> Valid
a
                            Ordering
_  -> Valid
b
  
instance Boolean Valid where
  false :: Valid
false = Valid
Invalid
  true :: Valid
true  = Valid
Valid
  not :: Valid -> Valid
not Valid
t = Int -> Valid
forall a. Enum a => Int -> a
toEnum (Valid -> Int
forall a. Enum a => a -> Int
fromEnum Valid
Valid Int -> Int -> Int
forall a. Num a => a -> a -> a
- Valid -> Int
forall a. Enum a => a -> Int
fromEnum Valid
t)

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 = X Valid
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
iString -> ShowS
forall a. [a] -> [a] -> [a]
++String
is)

-- | the indentation as string.

indent :: Indent -> String
indent :: Indent -> String
indent = Indent -> String
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" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Indent -> String
indent Indent
is String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
ind String
ss
  ind (Char
s:String
ss)    = Char
sChar -> ShowS
forall 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 (e -> String
forall a. Show a => a -> String
show e
e) String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ Valid -> String
forall a. Show a => a -> String
show Valid
v String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"failure " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Indent -> e -> String
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)  = Indent -> e -> String
forall e. Exception e => Indent -> e -> String
showFailure Indent
is e
e

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

-- showTNode -


showTNode :: T -> String
showTNode :: T -> String
showTNode (HNFValue Valid
b) = Valid -> String
forall a. Show a => a -> String
show Valid
b
showTNode (Failure e
e)  = e -> String
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
v
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" := "
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Indent -> ShowS
showIndent (Indent -> Indent
isucc Indent
is) String
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"message: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
  Params [Parameter]
ps -> Indent -> String
indent Indent
is String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"parameters" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"check " String -> ShowS
forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
                 String -> ShowS
forall a. [a] -> [a] -> [a]
++ Indent -> T -> String
showTLeaf Indent
is' T
t
                 String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"catched" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"substitution" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"catch " String -> ShowS
forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
                          String -> ShowS
forall a. [a] -> [a] -> [a]
++ Indent -> V -> String
showCatched Indent
is' V
c
                          String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"not " String -> ShowS
forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
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 String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
                String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"or " String -> ShowS
forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
                String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"=> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
                String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ Label -> String
forall a. Show a => a -> String
show Label
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
                     String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"<=> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
                String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"for all " String -> ShowS
forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
                  String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"exist " String -> ShowS
forall a. [a] -> [a] -> [a]
++ T -> String
showTNode T
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
                 String -> ShowS
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     -> Indent -> e -> String
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   -> [Bool] -> Bool
forall b. Boolean b => [b] -> b
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (V -> Bool) -> [V] -> [Bool]
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             -> [Bool] -> Bool
forall b. Boolean b => [b] -> b
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (V -> Bool) -> [V] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map V -> Bool
valDeterministic [V]
vs
  VOr T
_ [V]
vs              -> [Bool] -> Bool
forall b. Boolean b => [b] -> b
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (V -> Bool) -> [V] -> [Bool]
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              -> Valid -> T
forall x. x -> HNFValue x
HNFValue Valid
t
  VFailure e
e       -> e -> T
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 <- Statement -> IO (HNFValue Statement)
forall x. HNFData x => x -> IO (HNFValue x)
hnfValue Statement
p
  case HNFValue Statement
hfp of
    Failure e
e  -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (e -> V
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     -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ Valid -> V
V Valid
Invalid
      Statement
SValid       -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (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    -> Statement -> (e -> Statement) -> Int -> Omega -> IO V
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  -> X x -> (x -> Statement) -> Int -> Omega -> IO V
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   -> X x -> (x -> Statement) -> Int -> Omega -> IO V
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 <- Bool -> IO (HNFValue Bool)
forall x. HNFData x => x -> IO (HNFValue x)
hnfValue Bool
b
  case HNFValue Bool
hfb of
    Failure e
e -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> Maybe Message -> V
VCheck (e -> T
forall x e. Exception e => e -> HNFValue x
Failure e
e) Maybe Message
forall a. Maybe a
Nothing
    HNFValue Bool
b -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ case Bool
b of
      Bool
True    -> T -> Maybe Message -> V
VCheck (Valid -> T
forall x. x -> HNFValue x
HNFValue Valid
Valid) Maybe Message
forall a. Maybe a
Nothing
      Bool
False   -> T -> Maybe Message -> V
VCheck (Valid -> T
forall x. x -> HNFValue x
HNFValue Valid
Invalid) (Message -> Maybe Message
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 (e -> Statement) -> e -> Maybe e
forall s e x.
(Exception s, Exception e) =>
(e -> x) -> s -> Maybe e
castException e -> Statement
h e
s of
                   Maybe e
Nothing -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> Maybe V -> V -> V
VCatch (e -> T
forall x e. Exception e => e -> HNFValue x
Failure e
s) Maybe V
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
                     V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> Maybe V -> V -> V
VCatch (V -> T
valT V
v') (V -> Maybe V
forall a. a -> Maybe a
Just V
v) V
v' 
    T
t         -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> Maybe V -> V -> V
VCatch T
t Maybe V
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 = SomeException -> Maybe e
forall e. Exception e => SomeException -> Maybe e
fromException (SomeException -> Maybe e) -> SomeException -> Maybe e
forall a b. (a -> b) -> a -> b
$ s -> SomeException
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  -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> V -> V
VNot (e -> T
forall x e. Exception e => e -> HNFValue x
Failure e
e) V
v
    HNFValue Valid
t -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> V -> V
VNot (Valid -> T
forall x. x -> HNFValue x
HNFValue (Valid -> Valid
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 <- [Statement] -> IO (HNFValue [Statement])
forall x. HNFData x => x -> IO (HNFValue x)
hnfValue [Statement]
ps
  case HNFValue [Statement]
hfps of
    Failure e
e   -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> [V] -> V
VAnd (e -> T
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                    = V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> [V] -> V
VAnd (Valid -> T
forall x. x -> HNFValue x
HNFValue Valid
s) [V]
vs
        allTrue Valid
s [Statement]
_ [V]
vs | Valid
s Valid -> Valid -> Bool
forall a. Ord a => a -> a -> Bool
< Valid
ProbablyValid = V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> [V] -> V
VAnd (Valid -> T
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
sValid -> Valid -> Valid
forall a. Logical a => a -> a -> a
&&Valid
t) [Statement]
ps (V
vV -> [V] -> [V]
forall a. a -> [a] -> [a]
:[V]
vs)
            T
f          -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> [V] -> V
VAnd T
f (V
vV -> [V] -> [V]
forall 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 <- [Statement] -> IO (HNFValue [Statement])
forall x. HNFData x => x -> IO (HNFValue x)
hnfValue [Statement]
ps
  case HNFValue [Statement]
hfps of
    Failure e
e  -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> [V] -> V
VOr (e -> T
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                      = V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> [V] -> V
VOr (Valid -> T
forall x. x -> HNFValue x
HNFValue Valid
s) [V]
vs
        existTrue Valid
s [Statement]
_ [V]
vs | Valid
s Valid -> Valid -> Bool
forall a. Ord a => a -> a -> Bool
> Valid
ProbablyInvalid = V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> [V] -> V
VOr (Valid -> T
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
sValid -> Valid -> Valid
forall a. Logical a => a -> a -> a
||Valid
t) [Statement]
ps (V
vV -> [V] -> [V]
forall a. a -> [a] -> [a]
:[V]
vs)
            T
f          -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> [V] -> V
VOr T
f (V
vV -> [V] -> [V]
forall 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
  V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (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
  V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (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
_     = V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (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
  V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> V -> V
VEqvl (V -> T
valT V
v) V
v
  where impls :: [Statement]
impls = ((Statement, Statement) -> Statement)
-> [(Statement, Statement)] -> [Statement]
forall a b. (a -> b) -> [a] -> [b]
map ((Statement -> Statement -> Statement)
-> (Statement, Statement) -> Statement
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Statement -> Statement -> Statement
(:=>)) ([(Statement, Statement)] -> [Statement])
-> [(Statement, Statement)] -> [Statement]
forall a b. (a -> b) -> a -> b
$ [Statement] -> [Statement] -> [(Statement, Statement)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Statement
aStatement -> [Statement] -> [Statement]
forall a. a -> [a] -> [a]
:[Statement]
as) ([Statement]
as[Statement] -> [Statement] -> [Statement]
forall 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 [] -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> V -> V
VForall T
t V
v
    V
_         -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> V -> V
VForall ((Valid -> Valid) -> T -> T
forall a b. (a -> b) -> HNFValue a -> HNFValue b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Valid
ProbablyValidValid -> Valid -> Valid
forall a. Logical a => a -> a -> a
&&) (T -> T) -> T -> T
forall a b. (a -> b) -> a -> b
$ V -> T
valT V
v) V
v
  where ps :: [Statement]
ps = (x -> Statement) -> [x] -> [Statement]
forall a b. (a -> b) -> [a] -> [b]
map x -> Statement
p ([x] -> [Statement]) -> [x] -> [Statement]
forall a b. (a -> b) -> a -> b
$ Int -> [x] -> [x]
forall a. Int -> [a] -> [a]
take Int
w ([x] -> [x]) -> [x] -> [x]
forall a b. (a -> b) -> a -> b
$ X x -> Omega -> [x]
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 [] -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> V -> V
VExist T
t V
v
    V
_        -> V -> IO V
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> IO V) -> V -> IO V
forall a b. (a -> b) -> a -> b
$ T -> V -> V
VExist ((Valid -> Valid) -> T -> T
forall a b. (a -> b) -> HNFValue a -> HNFValue b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Valid
ProbablyInvalidValid -> Valid -> Valid
forall a. Logical a => a -> a -> a
||) (T -> T) -> T -> T
forall a b. (a -> b) -> a -> b
$ V -> T
valT V
v) V
v
  where ps :: [Statement]
ps = (x -> Statement) -> [x] -> [Statement]
forall a b. (a -> b) -> [a] -> [b]
map x -> Statement
p ([x] -> [Statement]) -> [x] -> [Statement]
forall a b. (a -> b) -> a -> b
$ Int -> [x] -> [x]
forall a. Int -> [a] -> [a]
take Int
w ([x] -> [x]) -> [x] -> [x]
forall a b. (a -> b) -> a -> b
$ X x -> Omega -> [x]
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 = (V -> Valid) -> IO V -> IO Valid
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (T -> Valid
forall x. HNFValue x -> x
fromHNFValue (T -> Valid) -> (V -> T) -> V -> Valid
forall b c a. (b -> c) -> (a -> b) -> a -> c
. V -> T
valT) (IO V -> IO Valid) -> IO V -> IO Valid
forall a b. (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 = IO Bool -> Bool
forall a. IO a -> a
unsafePerformIO (IO Bool -> Bool) -> IO Bool -> Bool
forall a b. (a -> b) -> a -> b
$ do
  V
v <- Statement -> Int -> Omega -> IO V
value Statement
p (ValidateingException -> Int
forall a e. Exception e => e -> a
throw ValidateingException
NonDeterministic) (ValidateingException -> Omega
forall a e. Exception e => e -> a
throw ValidateingException
NonDeterministic)
  case V -> T
valT V
v of
    Failure e
e  -> e -> IO Bool
forall a e. Exception e => e -> a
throw e
e
    HNFValue Valid
s -> case Valid
s of
      Valid
Valid    -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
      Valid
Invalid  -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      Valid
st       -> AlgebraicException -> IO Bool
forall a e. Exception e => e -> a
throw (AlgebraicException -> IO Bool) -> AlgebraicException -> IO Bool
forall a b. (a -> b) -> a -> b
$ String -> AlgebraicException
ImplementationError
                    (String -> AlgebraicException) -> String -> AlgebraicException
forall a b. (a -> b) -> a -> b
$ (String
"deterministic statement with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Valid -> String
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 Valid -> Valid -> Bool
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 | Bool -> Bool
forall b. Boolean b => b -> b
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ T -> Bool
isTrueT (T -> Bool) -> T -> Bool
forall a b. (a -> b) -> a -> b
$ V -> T
valT V
v = Maybe V
forall a. Maybe a
Nothing
rdcTrue V
v = case V
v of
  V Valid
_             -> V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VCheck T
_ Maybe Message
_      -> V -> Maybe V
forall a. a -> Maybe a
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' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> Maybe V -> V -> V
VCatch T
t Maybe V
e
  VNot T
t V
v'       -> V -> Maybe V
rdcFalse V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VNot T
t 
  VAnd T
t [V]
vs       -> ([Maybe V] -> Maybe [V]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([Maybe V] -> Maybe [V]) -> [Maybe V] -> Maybe [V]
forall a b. (a -> b) -> a -> b
$ (V -> Maybe V) -> [V] -> [Maybe V]
forall a b. (a -> b) -> [a] -> [b]
map V -> Maybe V
rdcTrue [V]
vs) Maybe [V] -> ([V] -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> ([V] -> V) -> [V] -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> [V] -> V
VAnd T
t
  VOr T
t (V
v':[V]
_)    -> V -> Maybe V
rdcTrue V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> [V] -> V
VOr T
t ([V] -> V) -> (V -> [V]) -> V -> V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. V -> [V]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return 
  VImpl T
t V
v'      -> V -> Maybe V
rdcTrue V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VImpl T
t
  VEqvl T
t V
v'      -> V -> Maybe V
rdcTrue V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VEqvl T
t
  VDefEqvl Label
l T
t V
v' -> V -> Maybe V
rdcTrue V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label -> T -> V -> V
VDefEqvl Label
l T
t
  VForall T
t V
v'    -> V -> Maybe V
rdcTrue V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VForall T
t
  VExist T
t V
v'     -> V -> Maybe V
rdcTrue V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VExist T
t
  V
_               -> Maybe V
forall a. Maybe a
Nothing

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

-- rdcFalse -


-- | checking for being 'False'.

isFalseT :: T -> Bool
isFalseT :: T -> Bool
isFalseT (HNFValue Valid
sb) = Valid
sb Valid -> Valid -> Bool
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 | Bool -> Bool
forall b. Boolean b => b -> b
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ T -> Bool
isFalseT (T -> Bool) -> T -> Bool
forall a b. (a -> b) -> a -> b
$ V -> T
valT V
v = Maybe V
forall a. Maybe a
Nothing
rdcFalse V
v = case V
v of
  V Valid
_             -> V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VCheck T
_ Maybe Message
_      -> V -> Maybe V
forall a. a -> Maybe a
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' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> Maybe V -> V -> V
VCatch T
t Maybe V
e
  VNot T
t V
v'       -> V -> Maybe V
rdcTrue V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VNot T
t
  VAnd T
t (V
v':[V]
_)   -> V -> Maybe V
rdcFalse V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> [V] -> V
VAnd T
t ([V] -> V) -> (V -> [V]) -> V -> V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. V -> [V]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return
  VOr T
t [V]
vs        -> ([Maybe V] -> Maybe [V]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([Maybe V] -> Maybe [V]) -> [Maybe V] -> Maybe [V]
forall a b. (a -> b) -> a -> b
$ (V -> Maybe V) -> [V] -> [Maybe V]
forall a b. (a -> b) -> [a] -> [b]
map V -> Maybe V
rdcFalse [V]
vs) Maybe [V] -> ([V] -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> ([V] -> V) -> [V] -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> [V] -> V
VOr T
t
  VImpl T
t V
v'      -> V -> Maybe V
rdcFalse V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VImpl T
t 
  VEqvl T
t V
v'      -> V -> Maybe V
rdcFalse V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VEqvl T
t
  VDefEqvl Label
l T
t V
v' -> V -> Maybe V
rdcFalse V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label -> T -> V -> V
VDefEqvl Label
l T
t
  VForall T
t V
v'    -> V -> Maybe V
rdcFalse V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VForall T
t
  VExist T
t V
v'     -> V -> Maybe V
rdcFalse V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VExist T
t
  V
_               -> Maybe 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
_])) = V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return V
c
getCncl V
_                                      = Maybe 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
_                                                          = Maybe V
forall a. Maybe a
Nothing

-- | reduces false values having denied premisis

rdcDndPrmsFalse :: V -> Maybe V
rdcDndPrmsFalse :: V -> Maybe V
rdcDndPrmsFalse V
v | Bool -> Bool
forall b. Boolean b => b -> b
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ T -> Bool
isFalseT (T -> Bool) -> T -> Bool
forall a b. (a -> b) -> a -> b
$ V -> T
valT V
v = Maybe 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' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> Maybe V -> V -> V
VCatch T
t Maybe V
e
  VNot T
t V
v'           -> V -> Maybe V
rdcDndPrms V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VNot T
t
  VAnd T
t (V
v':[V]
_)       -> V -> Maybe V
rdcDndPrmsFalse V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> [V] -> V
VAnd T
t ([V] -> V) -> (V -> [V]) -> V -> V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. V -> [V]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return
  VOr T
t [V]
vs            -> ([Maybe V] -> Maybe [V]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([Maybe V] -> Maybe [V]) -> [Maybe V] -> Maybe [V]
forall a b. (a -> b) -> a -> b
$ (V -> Maybe V) -> [V] -> [Maybe V]
forall a b. (a -> b) -> [a] -> [b]
map V -> Maybe V
rdcDndPrmsFalse [V]
vs) Maybe [V] -> ([V] -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> ([V] -> V) -> [V] -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> [V] -> V
VOr T
t
  VDefEqvl Label
l T
t V
v'     -> V -> Maybe V
rdcDndPrmsFalse V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label -> T -> V -> V
VDefEqvl Label
l T
t
  VForall T
t V
v'        -> V -> Maybe V
rdcDndPrmsFalse V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VForall T
t
  VExist T
_ (VOr T
_ []) -> V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VExist T
t V
v'         -> V -> Maybe V
rdcDndPrmsFalse V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VExist T
t
  V
_                   -> Maybe 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 | Bool -> Bool
forall b. Boolean b => b -> b
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ T -> Bool
isTrueT (T -> Bool) -> T -> Bool
forall a b. (a -> b) -> a -> b
$ V -> T
valT V
v = Maybe 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
_  -> Maybe V
forall a. Maybe a
Nothing
  VCatch T
t Maybe V
e V
v'         -> V -> Maybe V
rdcDndPrms V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> Maybe V -> V -> V
VCatch T
t Maybe V
e
  VNot T
t V
v'             -> V -> Maybe V
rdcDndPrmsFalse V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VNot T
t 
  VAnd T
t [V]
vs             -> ([Maybe V] -> Maybe [V]
forall v. [Maybe v] -> Maybe [v]
exstJust ([Maybe V] -> Maybe [V]) -> [Maybe V] -> Maybe [V]
forall a b. (a -> b) -> a -> b
$ (V -> Maybe V) -> [V] -> [Maybe V]
forall a b. (a -> b) -> [a] -> [b]
map V -> Maybe V
rdcDndPrms [V]
vs) Maybe [V] -> ([V] -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> ([V] -> V) -> [V] -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> [V] -> V
VAnd T
t
  VOr T
t [V]
vs              -> ([Maybe V] -> Maybe [V]
forall v. [Maybe v] -> Maybe [v]
exstJust ([Maybe V] -> Maybe [V]) -> [Maybe V] -> Maybe [V]
forall a b. (a -> b) -> a -> b
$ (V -> Maybe V) -> [V] -> [Maybe V]
forall a b. (a -> b) -> [a] -> [b]
map V -> Maybe V
rdcDndPrms [V]
vs) Maybe [V] -> ([V] -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> ([V] -> V) -> [V] -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label -> T -> V -> V
VDefEqvl Label
l T
t
  VForall T
_ (VAnd T
_ []) -> V -> Maybe V
forall a. a -> Maybe a
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' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VForall T
t
  VExist T
t V
v'           -> V -> Maybe V
rdcDndPrms V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VExist T
t
  V
_                     -> Maybe 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
_                  -> V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VCheck (Failure e
_) Maybe Message
_        -> V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return V
v
  VCatch (Failure e
_) Maybe V
_ V
_      -> V -> Maybe V
forall a. a -> Maybe a
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' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VNot T
f
  VAnd f :: T
f@(Failure e
_) (V
v':[V]
_)   -> V -> Maybe V
rdcFailed V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> [V] -> V
VAnd T
f ([V] -> V) -> (V -> [V]) -> V -> V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. V -> [V]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return
  VAnd (Failure e
_) []         -> V -> Maybe V
forall a. a -> Maybe a
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' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> [V] -> V
VOr T
f ([V] -> V) -> (V -> [V]) -> V -> V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. V -> [V]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return
  VOr (Failure e
_) []          -> V -> Maybe V
forall a. a -> Maybe a
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' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VImpl T
f
  VEqvl f :: T
f@(Failure e
_) V
v'      -> V -> Maybe V
rdcFailed V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VEqvl T
f
  VDefEqvl Label
l f :: T
f@(Failure e
_) V
v' -> V -> Maybe V
rdcFailed V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label -> T -> V -> V
VDefEqvl Label
l T
f
  VForall f :: T
f@(Failure e
_) V
v'    -> V -> Maybe V
rdcFailed V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VForall T
f
  VExist f :: T
f@(Failure e
_) V
v'     -> V -> Maybe V
rdcFailed V
v' Maybe V -> (V -> Maybe V) -> Maybe V
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= V -> Maybe V
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (V -> Maybe V) -> (V -> V) -> V -> Maybe V
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> V -> V
VExist T
f
  V
_                           -> Maybe 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 -> ((Int, [String]) -> (Int, [String]))
-> [(Int, [String])] -> [(Int, [String])]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
n,[String]
p) -> (Int
n,Label -> String
forall a. Show a => a -> String
show Label
lString -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
p)) ([(Int, [String])] -> [(Int, [String])])
-> [(Int, [String])] -> [(Int, [String])]
forall a b. (a -> b) -> a -> b
$ V -> [(Int, [String])]
tests V
v'
                  | Bool
otherwise       -> V -> [(Int, [String])]
tests V
v'
  VCatch T
_ Maybe V
_ V
v'   -> (Int, [String])
forall {a}. (Int, [a])
t1 (Int, [String]) -> [(Int, [String])] -> [(Int, [String])]
forall a. a -> [a] -> [a]
: V -> [(Int, [String])]
tests V
v'
  VNot T
_ V
v'       -> (Int, [String])
forall {a}. (Int, [a])
t1 (Int, [String]) -> [(Int, [String])] -> [(Int, [String])]
forall a. a -> [a] -> [a]
: V -> [(Int, [String])]
tests V
v'
  VAnd T
_ [V]
vs       -> (Int, [String])
forall {a}. (Int, [a])
t1 (Int, [String]) -> [(Int, [String])] -> [(Int, [String])]
forall a. a -> [a] -> [a]
: ([[(Int, [String])]] -> [(Int, [String])]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ([[(Int, [String])]] -> [(Int, [String])])
-> [[(Int, [String])]] -> [(Int, [String])]
forall a b. (a -> b) -> a -> b
$ (V -> [(Int, [String])]) -> [V] -> [[(Int, [String])]]
forall a b. (a -> b) -> [a] -> [b]
map V -> [(Int, [String])]
tests ([V] -> [[(Int, [String])]]) -> [V] -> [[(Int, [String])]]
forall a b. (a -> b) -> a -> b
$ [V]
vs)
  VOr T
_ [V]
vs        -> (Int, [String])
forall {a}. (Int, [a])
t1 (Int, [String]) -> [(Int, [String])] -> [(Int, [String])]
forall a. a -> [a] -> [a]
: ([[(Int, [String])]] -> [(Int, [String])]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ([[(Int, [String])]] -> [(Int, [String])])
-> [[(Int, [String])]] -> [(Int, [String])]
forall a b. (a -> b) -> a -> b
$ (V -> [(Int, [String])]) -> [V] -> [[(Int, [String])]]
forall a b. (a -> b) -> [a] -> [b]
map V -> [(Int, [String])]
tests ([V] -> [[(Int, [String])]]) -> [V] -> [[(Int, [String])]]
forall a b. (a -> b) -> a -> b
$ [V]
vs)
  VImpl T
_ V
v'      -> (Int, [String])
forall {a}. (Int, [a])
t1 (Int, [String]) -> [(Int, [String])] -> [(Int, [String])]
forall a. a -> [a] -> [a]
: V -> [(Int, [String])]
tests V
v'
  VEqvl T
_ V
v'      -> (Int, [String])
forall {a}. (Int, [a])
t1 (Int, [String]) -> [(Int, [String])] -> [(Int, [String])]
forall a. a -> [a] -> [a]
: V -> [(Int, [String])]
tests V
v'
  VForall T
_ V
v'    -> (Int, [String])
forall {a}. (Int, [a])
t1 (Int, [String]) -> [(Int, [String])] -> [(Int, [String])]
forall a. a -> [a] -> [a]
: V -> [(Int, [String])]
tests V
v'
  VExist T
_ V
v'     -> (Int, [String])
forall {a}. (Int, [a])
t1 (Int, [String]) -> [(Int, [String])] -> [(Int, [String])]
forall a. a -> [a] -> [a]
: V -> [(Int, [String])]
tests V
v'
  V
_               -> [(Int, [String])
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
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+(Int -> Int -> Int) -> Int -> [Int] -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) Int
0 ((V -> Int) -> [V] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map V -> Int
cntTests [V]
vs)
  VOr T
_ [V]
vs        -> Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+(Int -> Int -> Int) -> Int -> [Int] -> Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) Int
0 ((V -> Int) -> [V] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map V -> Int
cntTests [V]
vs)
  VCatch T
_ Maybe V
_ V
v'   -> Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+V -> Int
cntTests V
v'
  VNot T
_ V
v'       -> Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+V -> Int
cntTests V
v'
  VImpl T
_ V
v'      -> Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+V -> Int
cntTests V
v'
  VEqvl T
_ V
v'      -> Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+V -> Int
cntTests V
v'
  VForall T
_ V
v'    -> Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+V -> Int
cntTests V
v'
  VExist T
_ V
v'     -> Int
1Int -> Int -> Int
forall 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 = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Maybe Int -> Int) -> (V -> Maybe Int) -> V -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (V -> Int) -> Maybe V -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap V -> Int
cntTests (Maybe V -> Maybe Int) -> (V -> Maybe V) -> V -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Maybe Int -> Int) -> (V -> Maybe Int) -> V -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (V -> Int) -> Maybe V -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap V -> Int
cntTests (Maybe V -> Maybe Int) -> (V -> Maybe V) -> V -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Maybe Int -> Int) -> (V -> Maybe Int) -> V -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (V -> Int) -> Maybe V -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap V -> Int
cntTests (Maybe V -> Maybe Int) -> (V -> Maybe V) -> V -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Maybe Int -> Int) -> (V -> Maybe Int) -> V -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (V -> Int) -> Maybe V -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap V -> Int
cntTests (Maybe V -> Maybe Int) -> (V -> Maybe V) -> V -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = X Int -> X Omega -> X (Int, Omega)
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 = ((Int, Omega) -> IO V) -> X (Int, Omega) -> X (IO V)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Int, Omega) -> IO V) -> X (Int, Omega) -> X (IO V))
-> ((Int, Omega) -> IO V) -> X (Int, Omega) -> X (IO V)
forall a b. (a -> b) -> a -> b
$ (Int -> Omega -> IO V) -> (Int, Omega) -> IO V
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Int -> Omega -> IO V) -> (Int, Omega) -> IO V)
-> (Int -> Omega -> IO V) -> (Int, Omega) -> IO V
forall a b. (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 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Indent -> V -> String
showV (String -> Indent
indent0 String
"  ") V
v