{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE GADTs, StandaloneDeriving, ExistentialQuantification, RankNTypes #-}


-- |
-- Module      : OAlg.Data.Statement.Proposition
-- Description : proposition on statements
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- Propositions on statements.
module OAlg.Data.Statement.Proposition
  (
    -- * Proposition
    prpStatement
  , prpStatementTautologies
  , prpValidTautologies

  , prpCheckTrue, prpCheckFalse
  , prpCatch
  , prpPrjHom

    -- * X
  , xStatement
  
  )
  where

import System.IO (IO)

import Control.Monad
import Control.Applicative ((<*>))

import Data.List (map,(++),take,repeat)

import OAlg.Control.Exception
import OAlg.Category.Definition

import OAlg.Data.Ord
import OAlg.Data.Show
import OAlg.Data.Equal
import OAlg.Data.Statistics
import OAlg.Data.Canonical
import OAlg.Data.Number
import OAlg.Data.X

import OAlg.Data.Boolean
import OAlg.Data.Statement.Definition



--------------------------------------------------------------------------------
-- xPoroposition -

xPrpOp :: X (Statement -> Statement -> Statement)
xPrpOp :: X (Statement -> Statement -> Statement)
xPrpOp = forall a. [a] -> X a
xOneOf [Statement -> Statement -> Statement
(:||),Statement -> Statement -> Statement
(:&&),Statement -> Statement -> Statement
(:=>),Statement -> Statement -> Statement
(:<=>)]

xPrpOps ::X ([Statement] -> Statement)
xPrpOps :: X ([Statement] -> Statement)
xPrpOps = forall a. [a] -> X a
xOneOf [[Statement] -> Statement
And,[Statement] -> Statement
Or]

xStatement' :: Int -> X Statement -> X (X x,x -> Statement) -> X Statement
xStatement' :: forall x.
Int -> X Statement -> X (X x, x -> Statement) -> X Statement
xStatement' Int
n X Statement
xp0 X (X x, x -> Statement)
xxp = Int -> X Statement
xprp Int
n
  where -- xprp :: Int -> X Statement
        xprp :: Int -> X Statement
xprp Int
0 = X Statement
xp0        
        xprp Int
n = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. [(Q, a)] -> X a
xOneOfW [ (Q
10,X Statement
xOp)
                                , (Q
4,X Statement
xOps)
                                , (Q
3,X Statement
xNot)
                                , (Q
2,forall {m :: * -> *} {x}.
Monad m =>
m (X x, x -> Statement) -> m Statement
xForall X (X x, x -> Statement)
xxp)
                                , (Q
2,forall {m :: * -> *} {x}.
Monad m =>
m (X x, x -> Statement) -> m Statement
xExist X (X x, x -> Statement)
xxp)
                                , (Q
1,X Statement
xCatch)
                                , (Q
1,X Statement
xCheck)
                                , (Q
1,X Statement
xEqvDef)
                                ]
          where n' :: Int
n' = forall a. Enum a => a -> a
pred Int
n

                xCheck :: X Statement
xCheck = do
                  Bool
b <- forall a. [a] -> X a
xOneOf [Bool
False,Bool
True]
                  forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
b Bool -> Message -> Statement
:?> String -> Message
Message String
"m")

                xCatch :: X Statement
xCatch = do
                  AlgebraicException
e <- forall a. [a] -> X a
xOneOf [String -> AlgebraicException
AlgebraicException String
"",String -> AlgebraicException
ImplementationError String
""]
                  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a e. Exception e => e -> a
throw AlgebraicException
e forall x. Exception x => Statement -> (x -> Statement) -> Statement
`Catch` AlgebraicException -> Statement
algExcp)
                  where algExcp :: AlgebraicException -> Statement
algExcp (AlgebraicException String
_) = Statement
SValid
                        algExcp AlgebraicException
_                      = Statement
SInvalid

                xNot :: X Statement
xNot = do
                  Int
i <- Int -> Int -> X Int
xIntB Int
0 Int
n'
                  Statement
p <- Int -> X Statement
xprp Int
i
                  forall (m :: * -> *) a. Monad m => a -> m a
return (Statement -> Statement
Not Statement
p)

                -- xOp :: X Statement
                xOp :: X Statement
xOp = do
                  Int
i  <- Int -> Int -> X Int
xIntB Int
0 Int
n'
                  Int
j  <- Int -> Int -> X Int
xIntB Int
0 Int
n'
                  X (Statement -> Statement -> Statement)
xPrpOp forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> X Statement
xprp Int
i forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> X Statement
xprp Int
j

                -- xOps :: X Statement
                xOps :: X Statement
xOps = do
                  Int
l   <- Int -> Int -> X Int
xIntB Int
0 Int
10
                  [Statement]
ps  <- forall x. [X x] -> X [x]
xList forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> X Statement
xprp)
                                     forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (forall a. Int -> [a] -> [a]
take Int
l) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. a -> [a]
repeat forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Int -> Int -> X Int
xIntB Int
0 Int
n'
                  [Statement] -> Statement
ops <- X ([Statement] -> Statement)
xPrpOps
                  forall (m :: * -> *) a. Monad m => a -> m a
return ([Statement] -> Statement
ops [Statement]
ps)

                -- xEqvDef :: X Statement
                xEqvDef :: X Statement
xEqvDef = do
                  Int
i <- Int -> Int -> X Int
xIntB Int
0 Int
n'
                  Statement
p <- Int -> X Statement
xprp Int
i
                  forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Label
Label String
"s" Label -> Statement -> Statement
:<=>: Statement
p)

                -- xForall :: X Statement
                xForall :: m (X x, x -> Statement) -> m Statement
xForall m (X x, x -> Statement)
xxp = do
                  (X x
x,x -> Statement
p) <- m (X x, x -> Statement)
xxp
                  forall (m :: * -> *) a. Monad m => a -> m a
return (forall x. X x -> (x -> Statement) -> Statement
Forall X x
x x -> Statement
p)

                xExist :: m (X x, x -> Statement) -> m Statement
xExist m (X x, x -> Statement)
xxp = do
                  (X x
x,x -> Statement
p) <- m (X x, x -> Statement)
xxp
                  forall (m :: * -> *) a. Monad m => a -> m a
return (forall x. X x -> (x -> Statement) -> Statement
Exist X x
x x -> Statement
p)

--------------------------------------------------------------------------------
-- xStatement -

-- | random variable of statements with the maximal given depth.  
xStatement :: Int -> X Statement
xStatement :: Int -> X Statement
xStatement Int
n = forall x.
Int -> X Statement -> X (X x, x -> Statement) -> X Statement
xStatement' Int
n X Statement
xp0 X (X Int, Int -> Statement)
xxp
  where xp0 :: X Statement
xp0 = forall a. [a] -> X a
xOneOf [Statement
SValid,Statement
SInvalid]
        xxp :: X (X Int, Int -> Statement)
xxp = forall a. [a] -> X a
xOneOf ([ (Int -> Int -> X Int
xIntB Int
0 Int
100, \Int
n -> (Int
n Int -> Int -> Int
`modInt` Int
2 forall a. Eq a => a -> a -> Bool
== Int
0) Bool -> Message -> Statement
:?> String -> Message
Message (forall a. Show a => a -> String
show Int
n))
                      , (Int -> Int -> X Int
xIntB Int
0 Int
100, \Int
n -> (Int
90 forall a. Ord a => a -> a -> Bool
<= Int
n) Bool -> Message -> Statement
:?> String -> Message
Message (forall a. Show a => a -> String
show Int
n))
                      , (Int -> Int -> X Int
xIntB Int
0 Int
100, \Int
n -> (Int
n forall a. Ord a => a -> a -> Bool
<= Int
10) Bool -> Message -> Statement
:?> String -> Message
Message (forall a. Show a => a -> String
show Int
n))
                      , (X Int
xInt       , forall b a. b -> a -> b
const Statement
SValid)
                      , (X Int
xInt       , forall b a. b -> a -> b
const Statement
SInvalid)
                      ]
                      forall a. [a] -> [a] -> [a]
++ if Int
0 forall a. Ord a => a -> a -> Bool
< Int
n'
                           then [(X Int
xInt,\Int
n -> forall x. X x -> Omega -> x
sample (Int -> X Statement
xStatement Int
n') (Int -> Omega
mkOmega Int
n))]
                           else []
                     )
                     
        n' :: Int
n' = Int
n Int -> Int -> Int
`divInt` Int
3
            
dstXStatement :: Wide -> Int -> Int -> IO ()
dstXStatement :: Int -> Int -> Int -> IO ()
dstXStatement Int
w Int
n Int
m = do
  Omega
o  <- IO Omega
getOmega
  Omega
o' <- forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. X x -> Omega -> x
sample X Omega
xOmega Omega
o 
  [Statement]
ps <- forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
m forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. X x -> Omega -> [x]
samples (Int -> X Statement
xStatement Int
n) Omega
o
  [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 (\Statement
p -> Statement -> Int -> Omega -> IO V
value Statement
p Int
w Omega
o') [Statement]
ps
  forall x. (Show x, Ord x) => [x -> String] -> [x] -> IO ()
putStatistic [forall x. x -> x
id] forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => a -> String
show forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. V -> T
valT) [V]
vs


--------------------------------------------------------------------------------
-- prpStatementTautologies -

-- | logical tautologies of 'Statement'.
--
--  __Note__ Validating this proposition produces about 15% denied premises, which is OK.
prpStatementTautologies :: Statement
prpStatementTautologies :: Statement
prpStatementTautologies = String -> Label
Prp String
"StatementTautologies" 
    Label -> Statement -> Statement
:<=>: forall b.
Boolean b =>
(b -> Statement) -> X b -> X [b] -> Statement
prpTautologies forall x. x -> x
id X Statement
xPrp (forall x. N -> N -> X x -> X [x]
xTakeB N
0 N
11 X Statement
xPrp)
  where
    xPrp :: X Statement
xPrp = Int -> X Statement
xStatement Int
7
    
--------------------------------------------------------------------------------
-- prpValidTautologies -

-- | logical tautologies of 'Valid'.
prpValidTautologies :: Statement
prpValidTautologies :: Statement
prpValidTautologies = String -> Label
Prp String
"ValidTautologies"
  Label -> Statement -> Statement
:<=>: forall b.
Boolean b =>
(b -> Statement) -> X b -> X [b] -> Statement
prpTautologies Valid -> Statement
stm X Valid
xValid (forall x. N -> N -> X x -> X [x]
xTakeB N
0 N
20 X Valid
xValid)
  where stm :: Valid -> Statement
stm Valid
Invalid         = Statement
SInvalid
        stm Valid
ProbablyInvalid = forall x. X x -> (x -> Statement) -> Statement
Exist X Int
xInt (forall b a. b -> a -> b
const Statement
SInvalid)
        stm Valid
ProbablyValid   = forall x. X x -> (x -> Statement) -> Statement
Forall X Int
xInt (forall b a. b -> a -> b
const Statement
SValid)
        stm Valid
Valid           = Statement
SValid

--------------------------------------------------------------------------------
-- prpCatch -

-- | catch algebraic exceptions.
prpCatch :: Statement
prpCatch :: Statement
prpCatch = String -> Label
Prp String
"Catch"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ (forall a e. Exception e => e -> a
throw (String -> AlgebraicException
AlgebraicException String
"") forall x. Exception x => Statement -> (x -> Statement) -> Statement
`Catch` AlgebraicException -> Statement
algException) forall b. Boolean b => b -> b -> b
<~> forall b. Boolean b => b
true
            , (forall a e. Exception e => e -> a
throw (String -> AlgebraicException
ImplementationError String
"") forall x. Exception x => Statement -> (x -> Statement) -> Statement
`Catch` AlgebraicException -> Statement
algException) forall b. Boolean b => b -> b -> b
<~> forall b. Boolean b => b
false
            ]
            
  where algException :: AlgebraicException -> Statement
        algException :: AlgebraicException -> Statement
algException (AlgebraicException String
_) = Statement
SValid
        algException AlgebraicException
_                      = Statement
SInvalid

--------------------------------------------------------------------------------
-- prpCheckFalse -

-- | @'false' ':?>' 'MInvalid' '<~>' 'false'@.
prpCheckFalse :: Statement
prpCheckFalse :: Statement
prpCheckFalse = String -> Label
Prp String
"CheckFalse" Label -> Statement -> Statement
:<=>: forall b. Boolean b => b
false Bool -> Message -> Statement
:?> String -> Message
Message String
"" forall b. Boolean b => b -> b -> b
<~> forall b. Boolean b => b
false

--------------------------------------------------------------------------------
-- prpCheckTrue -

-- | @'true' ':?>' 'MInvalid'@.
prpCheckTrue :: Statement
prpCheckTrue :: Statement
prpCheckTrue = String -> Label
Prp String
"CheckTrue" Label -> Statement -> Statement
:<=>: Bool
True Bool -> Message -> Statement
:?> String -> Message
Message String
""

--------------------------------------------------------------------------------
-- prpPrjHom -

-- | @'prj' :: 'Valid' -> 'Bool'@ is a homomorphism between 'Boolean' structures.
prpPrjHom :: Statement
prpPrjHom :: Statement
prpPrjHom = String -> Label
Prp String
"PrjHom" Label -> Statement -> Statement
:<=>: String -> Label
Label String
"Valid -> Bool"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ Valid -> Bool
h forall b. Boolean b => b
true forall a. Eq a => a -> a -> Statement
.==. forall b. Boolean b => b
true
            , Valid -> Bool
h forall b. Boolean b => b
false forall a. Eq a => a -> a -> Statement
.==. forall b. Boolean b => b
false
            , forall x. X x -> (x -> Statement) -> Statement
Forall X Valid
xa  (\Valid
a -> Valid -> Bool
h (forall b. Boolean b => b -> b
not Valid
a) forall a. Eq a => a -> a -> Statement
.==. forall b. Boolean b => b -> b
not (Valid -> Bool
h Valid
a))
            , forall x. X x -> (x -> Statement) -> Statement
Forall X (Valid, Valid)
xab (\(Valid
a,Valid
b) -> Valid -> Bool
h (Valid
a forall b. Boolean b => b -> b -> b
&& Valid
b) forall a. Eq a => a -> a -> Statement
.==. (Valid -> Bool
h Valid
a forall b. Boolean b => b -> b -> b
&& Valid -> Bool
h Valid
b))
            , forall x. X x -> (x -> Statement) -> Statement
Forall X (Valid, Valid)
xab (\(Valid
a,Valid
b) -> Valid -> Bool
h (Valid
a forall b. Boolean b => b -> b -> b
|| Valid
b) forall a. Eq a => a -> a -> Statement
.==. (Valid -> Bool
h Valid
a forall b. Boolean b => b -> b -> b
|| Valid -> Bool
h Valid
b))
            , forall x. X x -> (x -> Statement) -> Statement
Forall X (Valid, Valid)
xab (\(Valid
a,Valid
b) -> Valid -> Bool
h (Valid
a forall b. Boolean b => b -> b -> b
~> Valid
b) forall a. Eq a => a -> a -> Statement
.==. (Valid -> Bool
h Valid
a forall b. Boolean b => b -> b -> b
~> Valid -> Bool
h Valid
b))
            ]
  where h :: Valid -> Bool
h   = forall a b. Projectible a b => b -> a
prj :: Valid -> Bool
        xa :: X Valid
xa  = X Valid
xValid
        xab :: X (Valid, Valid)
xab = forall a b. X a -> X b -> X (a, b)
xTupple2 X Valid
xa X Valid
xa
        
--------------------------------------------------------------------------------
-- prpStatement -

-- | validity of the logic of 'Statement'..
prpStatement :: Statement
prpStatement :: Statement
prpStatement = String -> Label
Prp String
"Statement"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ Statement
prpStatementTautologies
            , forall b. Boolean b => (b -> Statement) -> Statement
prpLazy forall x. x -> x
id
            , Statement
prpCheckTrue
            , Statement
prpCheckFalse
            , Statement
prpCatch
            , Statement
prpPrjHom
            ]