{-# 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.Identity
import OAlg.Data.Logical
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 = [Statement -> Statement -> Statement]
-> X (Statement -> Statement -> Statement)
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 = [[Statement] -> Statement] -> X ([Statement] -> Statement)
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 = X (X Statement) -> X Statement
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (X (X Statement) -> X Statement) -> X (X Statement) -> X Statement
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(Q, X Statement)] -> X (X Statement)
forall a. [(Q, a)] -> X a
xOneOfW [ (Q
10,X Statement
xOp)
                                , (Q
4,X Statement
xOps)
                                , (Q
3,X Statement
xNot)
                                , (Q
2,X (X x, x -> Statement) -> X Statement
forall {m :: * -> *} {x}.
Monad m =>
m (X x, x -> Statement) -> m Statement
xForall X (X x, x -> Statement)
xxp)
                                , (Q
2,X (X x, x -> Statement) -> X Statement
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' = Int -> Int
forall a. Enum a => a -> a
pred Int
n

                xCheck :: X Statement
xCheck = do
                  Bool
b <- [Bool] -> X Bool
forall a. [a] -> X a
xOneOf [Bool
False,Bool
True]
                  Statement -> X Statement
forall a. a -> X a
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 <- [AlgebraicException] -> X AlgebraicException
forall a. [a] -> X a
xOneOf [String -> AlgebraicException
AlgebraicException String
"",String -> AlgebraicException
ImplementationError String
""]
                  Statement -> X Statement
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (AlgebraicException -> Statement
forall a e. Exception e => e -> a
throw AlgebraicException
e Statement -> (AlgebraicException -> Statement) -> Statement
forall e. Exception e => Statement -> (e -> 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
                  Statement -> X Statement
forall a. a -> X a
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 X (Statement -> Statement -> Statement)
-> X Statement -> X (Statement -> Statement)
forall a b. X (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> X Statement
xprp Int
i X (Statement -> Statement) -> X Statement -> X Statement
forall a b. X (a -> b) -> X a -> X b
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  <- [X Statement] -> X [Statement]
forall x. [X x] -> X [x]
xList ([X Statement] -> X [Statement]) -> [X Statement] -> X [Statement]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (X Int -> X Statement) -> [X Int] -> [X Statement]
forall a b. (a -> b) -> [a] -> [b]
map (X (X Statement) -> X Statement
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (X (X Statement) -> X Statement)
-> (X Int -> X (X Statement)) -> X Int -> X Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (Int -> X Statement) -> X Int -> X (X Statement)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> X Statement
xprp)
                                     ([X Int] -> [X Statement]) -> [X Int] -> [X Statement]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Int -> [X Int] -> [X Int]
forall a. Int -> [a] -> [a]
take Int
l) ([X Int] -> [X Int]) -> [X Int] -> [X Int]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X Int -> [X Int]
forall a. a -> [a]
repeat (X Int -> [X Int]) -> X Int -> [X Int]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Int -> Int -> X Int
xIntB Int
0 Int
n'
                  [Statement] -> Statement
ops <- X ([Statement] -> Statement)
xPrpOps
                  Statement -> X Statement
forall a. a -> X a
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
                  Statement -> X Statement
forall a. a -> X a
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
                  Statement -> m Statement
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (X x -> (x -> Statement) -> Statement
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
                  Statement -> m Statement
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (X x -> (x -> Statement) -> Statement
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 = Int -> X Statement -> X (X Int, Int -> Statement) -> X Statement
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 = [Statement] -> X Statement
forall a. [a] -> X a
xOneOf [Statement
SValid,Statement
SInvalid]
        xxp :: X (X Int, Int -> Statement)
xxp = [(X Int, Int -> Statement)] -> X (X Int, Int -> Statement)
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) Bool -> Message -> Statement
:?> String -> Message
Message (Int -> String
forall a. Show a => a -> String
show Int
n))
                      , (Int -> Int -> X Int
xIntB Int
0 Int
100, \Int
n -> (Int
90 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n) Bool -> Message -> Statement
:?> String -> Message
Message (Int -> String
forall a. Show a => a -> String
show Int
n))
                      , (Int -> Int -> X Int
xIntB Int
0 Int
100, \Int
n -> (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
10) Bool -> Message -> Statement
:?> String -> Message
Message (Int -> String
forall a. Show a => a -> String
show Int
n))
                      , (X Int
xInt       , Statement -> Int -> Statement
forall b a. b -> a -> b
const Statement
SValid)
                      , (X Int
xInt       , Statement -> Int -> Statement
forall b a. b -> a -> b
const Statement
SInvalid)
                      ]
                      [(X Int, Int -> Statement)]
-> [(X Int, Int -> Statement)] -> [(X Int, Int -> Statement)]
forall a. [a] -> [a] -> [a]
++ if Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n'
                           then [(X Int
xInt,\Int
n -> X Statement -> Omega -> Statement
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' <- Omega -> IO Omega
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Omega -> IO Omega) -> Omega -> IO Omega
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X Omega -> Omega -> Omega
forall x. X x -> Omega -> x
sample X Omega
xOmega Omega
o 
  [Statement]
ps <- [Statement] -> IO [Statement]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Statement] -> IO [Statement]) -> [Statement] -> IO [Statement]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Int -> [Statement] -> [Statement]
forall a. Int -> [a] -> [a]
take Int
m ([Statement] -> [Statement]) -> [Statement] -> [Statement]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X Statement -> Omega -> [Statement]
forall x. X x -> Omega -> [x]
samples (Int -> X Statement
xStatement Int
n) Omega
o
  [V]
vs <- [IO V] -> IO [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 ([IO V] -> IO [V]) -> [IO V] -> IO [V]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Statement -> IO V) -> [Statement] -> [IO V]
forall a b. (a -> b) -> [a] -> [b]
map (\Statement
p -> Statement -> Int -> Omega -> IO V
value Statement
p Int
w Omega
o') [Statement]
ps
  [String -> String] -> [String] -> IO ()
forall x. (Show x, Ord x) => [x -> String] -> [x] -> IO ()
putStatistic [String -> String
forall x. x -> x
id] ([String] -> IO ()) -> [String] -> IO ()
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (V -> String) -> [V] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (T -> String
forall a. Show a => a -> String
show (T -> String) -> (V -> T) -> V -> String
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. V -> 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
:<=>: (Statement -> Statement)
-> X Statement -> X [Statement] -> Statement
forall b.
Boolean b =>
(b -> Statement) -> X b -> X [b] -> Statement
prpTautologies Statement -> Statement
forall x. x -> x
id X Statement
xPrp (N -> N -> X Statement -> X [Statement]
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
:<=>: (Valid -> Statement) -> X Valid -> X [Valid] -> Statement
forall b.
Boolean b =>
(b -> Statement) -> X b -> X [b] -> Statement
prpTautologies Valid -> Statement
stm X Valid
xValid (N -> N -> X Valid -> X [Valid]
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 = X Int -> (Int -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Exist X Int
xInt (Statement -> Int -> Statement
forall b a. b -> a -> b
const Statement
SInvalid)
        stm Valid
ProbablyValid   = X Int -> (Int -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X Int
xInt (Statement -> Int -> Statement
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 [ (AlgebraicException -> Statement
forall a e. Exception e => e -> a
throw (String -> AlgebraicException
AlgebraicException String
"") Statement -> (AlgebraicException -> Statement) -> Statement
forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` AlgebraicException -> Statement
algException) Statement -> Statement -> Statement
forall b. Boolean b => b -> b -> b
<~> Statement
forall b. Boolean b => b
true
            , (AlgebraicException -> Statement
forall a e. Exception e => e -> a
throw (String -> AlgebraicException
ImplementationError String
"") Statement -> (AlgebraicException -> Statement) -> Statement
forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` AlgebraicException -> Statement
algException) Statement -> Statement -> Statement
forall b. Boolean b => b -> b -> b
<~> Statement
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
:<=>: Bool
forall b. Boolean b => b
false Bool -> Message -> Statement
:?> String -> Message
Message String
"" Statement -> Statement -> Statement
forall b. Boolean b => b -> b -> b
<~> Statement
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 Valid
forall b. Boolean b => b
true Bool -> Bool -> Statement
forall a. Eq a => a -> a -> Statement
.==. Bool
forall b. Boolean b => b
true
            , Valid -> Bool
h Valid
forall b. Boolean b => b
false Bool -> Bool -> Statement
forall a. Eq a => a -> a -> Statement
.==. Bool
forall b. Boolean b => b
false
            , X Valid -> (Valid -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X Valid
xa  (\Valid
a -> Valid -> Bool
h (Valid -> Valid
forall b. Boolean b => b -> b
not Valid
a) Bool -> Bool -> Statement
forall a. Eq a => a -> a -> Statement
.==. Bool -> Bool
forall b. Boolean b => b -> b
not (Valid -> Bool
h Valid
a))
            , X (Valid, Valid) -> ((Valid, Valid) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Valid, Valid)
xab (\(Valid
a,Valid
b) -> Valid -> Bool
h (Valid
a Valid -> Valid -> Valid
forall a. Logical a => a -> a -> a
&& Valid
b) Bool -> Bool -> Statement
forall a. Eq a => a -> a -> Statement
.==. (Valid -> Bool
h Valid
a Bool -> Bool -> Bool
forall a. Logical a => a -> a -> a
&& Valid -> Bool
h Valid
b))
            , X (Valid, Valid) -> ((Valid, Valid) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Valid, Valid)
xab (\(Valid
a,Valid
b) -> Valid -> Bool
h (Valid
a Valid -> Valid -> Valid
forall a. Logical a => a -> a -> a
|| Valid
b) Bool -> Bool -> Statement
forall a. Eq a => a -> a -> Statement
.==. (Valid -> Bool
h Valid
a Bool -> Bool -> Bool
forall a. Logical a => a -> a -> a
|| Valid -> Bool
h Valid
b))
            , X (Valid, Valid) -> ((Valid, Valid) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Valid, Valid)
xab (\(Valid
a,Valid
b) -> Valid -> Bool
h (Valid
a Valid -> Valid -> Valid
forall b. Boolean b => b -> b -> b
~> Valid
b) Bool -> Bool -> Statement
forall a. Eq a => a -> a -> Statement
.==. (Valid -> Bool
h Valid
a Bool -> Bool -> Bool
forall b. Boolean b => b -> b -> b
~> Valid -> Bool
h Valid
b))
            ]
  where h :: Valid -> Bool
h   = Valid -> Bool
forall a b. Projectible a b => b -> a
prj :: Valid -> Bool
        xa :: X Valid
xa  = X Valid
xValid
        xab :: X (Valid, Valid)
xab = X Valid -> X Valid -> X (Valid, Valid)
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
            , (Statement -> Statement) -> Statement
forall b. Boolean b => (b -> Statement) -> Statement
prpLazy Statement -> Statement
forall x. x -> x
id
            , Statement
prpCheckTrue
            , Statement
prpCheckFalse
            , Statement
prpCatch
            , Statement
prpPrjHom
            ]