{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving #-}

-- |
-- Module      : OAlg.Structure.Oriented.Proposition
-- Description : propositions on multiplicative structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- Propositions on 'Multiplicative' structures.
module OAlg.Structure.Multiplicative.Proposition
  (
    -- * Multiplicative
    prpMlt, XMlt(..)
  , Endo(..), Mltp2(..), Mltp3(..)
  , prpMlt1, prpMlt2, prpMlt2_1, prpMlt2_2, prpMlt3, prpMlt4, prpMlt5

    -- * X
  , XStandardMlt(..)
  , xMlt, xMltp2, xMltp3
  , xoMlt
  
    -- * Oriented Direction
  -- , xodMlt, xodEndo, xodMltp2, xodMltp3
  
    -- ** Total
  , xMltTtl

    -- ** Orientation
  , xMltOrnt
  
  )
  where

import Control.Monad
import Control.Applicative

import OAlg.Prelude

import OAlg.Data.Singleton
import OAlg.Data.Symbol

import OAlg.Structure.Exception
import OAlg.Structure.Oriented

import OAlg.Structure.Multiplicative.Definition

--------------------------------------------------------------------------------
-- Endo -

-- | predicate for endos.
newtype Endo q = Endo q deriving (Int -> Endo q -> ShowS
forall q. Show q => Int -> Endo q -> ShowS
forall q. Show q => [Endo q] -> ShowS
forall q. Show q => Endo q -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Endo q] -> ShowS
$cshowList :: forall q. Show q => [Endo q] -> ShowS
show :: Endo q -> String
$cshow :: forall q. Show q => Endo q -> String
showsPrec :: Int -> Endo q -> ShowS
$cshowsPrec :: forall q. Show q => Int -> Endo q -> ShowS
Show,Endo q -> Endo q -> Bool
forall q. Eq q => Endo q -> Endo q -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Endo q -> Endo q -> Bool
$c/= :: forall q. Eq q => Endo q -> Endo q -> Bool
== :: Endo q -> Endo q -> Bool
$c== :: forall q. Eq q => Endo q -> Endo q -> Bool
Eq,Endo q -> Endo q -> Bool
Endo q -> Endo q -> Ordering
Endo q -> Endo q -> Endo q
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
forall {q}. Ord q => Eq (Endo q)
forall q. Ord q => Endo q -> Endo q -> Bool
forall q. Ord q => Endo q -> Endo q -> Ordering
forall q. Ord q => Endo q -> Endo q -> Endo q
min :: Endo q -> Endo q -> Endo q
$cmin :: forall q. Ord q => Endo q -> Endo q -> Endo q
max :: Endo q -> Endo q -> Endo q
$cmax :: forall q. Ord q => Endo q -> Endo q -> Endo q
>= :: Endo q -> Endo q -> Bool
$c>= :: forall q. Ord q => Endo q -> Endo q -> Bool
> :: Endo q -> Endo q -> Bool
$c> :: forall q. Ord q => Endo q -> Endo q -> Bool
<= :: Endo q -> Endo q -> Bool
$c<= :: forall q. Ord q => Endo q -> Endo q -> Bool
< :: Endo q -> Endo q -> Bool
$c< :: forall q. Ord q => Endo q -> Endo q -> Bool
compare :: Endo q -> Endo q -> Ordering
$ccompare :: forall q. Ord q => Endo q -> Endo q -> Ordering
Ord)

instance Oriented q => Validable (Endo q) where
  valid :: Endo q -> Statement
valid (Endo q
a) = forall a. Validable a => a -> Statement
valid q
a forall b. Boolean b => b -> b -> b
&& (forall q. Oriented q => q -> Point q
start q
a forall a. Eq a => a -> a -> Statement
.==. forall q. Oriented q => q -> Point q
end q
a)

--------------------------------------------------------------------------------
-- fromEndo -

-- | deconstruction of a 'Endo'.
fromEndo :: Endo q -> q
fromEndo :: forall q. Endo q -> q
fromEndo (Endo q
f) = q
f

--------------------------------------------------------------------------------
-- Mltp2 -

-- | predicate for two multiplicable factors.
data Mltp2 c = Mltp2 c c deriving (Int -> Mltp2 c -> ShowS
forall c. Show c => Int -> Mltp2 c -> ShowS
forall c. Show c => [Mltp2 c] -> ShowS
forall c. Show c => Mltp2 c -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Mltp2 c] -> ShowS
$cshowList :: forall c. Show c => [Mltp2 c] -> ShowS
show :: Mltp2 c -> String
$cshow :: forall c. Show c => Mltp2 c -> String
showsPrec :: Int -> Mltp2 c -> ShowS
$cshowsPrec :: forall c. Show c => Int -> Mltp2 c -> ShowS
Show,Mltp2 c -> Mltp2 c -> Bool
forall c. Eq c => Mltp2 c -> Mltp2 c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Mltp2 c -> Mltp2 c -> Bool
$c/= :: forall c. Eq c => Mltp2 c -> Mltp2 c -> Bool
== :: Mltp2 c -> Mltp2 c -> Bool
$c== :: forall c. Eq c => Mltp2 c -> Mltp2 c -> Bool
Eq,Mltp2 c -> Mltp2 c -> Bool
Mltp2 c -> Mltp2 c -> Ordering
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
forall {c}. Ord c => Eq (Mltp2 c)
forall c. Ord c => Mltp2 c -> Mltp2 c -> Bool
forall c. Ord c => Mltp2 c -> Mltp2 c -> Ordering
forall c. Ord c => Mltp2 c -> Mltp2 c -> Mltp2 c
min :: Mltp2 c -> Mltp2 c -> Mltp2 c
$cmin :: forall c. Ord c => Mltp2 c -> Mltp2 c -> Mltp2 c
max :: Mltp2 c -> Mltp2 c -> Mltp2 c
$cmax :: forall c. Ord c => Mltp2 c -> Mltp2 c -> Mltp2 c
>= :: Mltp2 c -> Mltp2 c -> Bool
$c>= :: forall c. Ord c => Mltp2 c -> Mltp2 c -> Bool
> :: Mltp2 c -> Mltp2 c -> Bool
$c> :: forall c. Ord c => Mltp2 c -> Mltp2 c -> Bool
<= :: Mltp2 c -> Mltp2 c -> Bool
$c<= :: forall c. Ord c => Mltp2 c -> Mltp2 c -> Bool
< :: Mltp2 c -> Mltp2 c -> Bool
$c< :: forall c. Ord c => Mltp2 c -> Mltp2 c -> Bool
compare :: Mltp2 c -> Mltp2 c -> Ordering
$ccompare :: forall c. Ord c => Mltp2 c -> Mltp2 c -> Ordering
Ord)

pthMltp2 :: Oriented c => Mltp2 c -> Path c
pthMltp2 :: forall c. Oriented c => Mltp2 c -> Path c
pthMltp2 (Mltp2 c
f c
g) = forall q. Point q -> [q] -> Path q
Path (forall q. Oriented q => q -> Point q
start c
g) [c
f,c
g]

instance Oriented c => Validable (Mltp2 c) where
  valid :: Mltp2 c -> Statement
valid = forall a. Validable a => a -> Statement
valid forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall c. Oriented c => Mltp2 c -> Path c
pthMltp2

type instance Dual (Mltp2 c) = Mltp2 (Op c)

instance Oriented c => Dualisable (Mltp2 c) where
  toDual :: Mltp2 c -> Dual (Mltp2 c)
toDual Mltp2 c
fg = forall c. c -> c -> Mltp2 c
Mltp2 Op c
f' Op c
g' where Path Point (Op c)
_ [Op c
f',Op c
g'] = forall x. Dualisable x => x -> Dual x
toDual (forall c. Oriented c => Mltp2 c -> Path c
pthMltp2 Mltp2 c
fg)
  fromDual :: Dual (Mltp2 c) -> Mltp2 c
fromDual Dual (Mltp2 c)
fg' = forall c. c -> c -> Mltp2 c
Mltp2 c
f c
g where Path Point c
_ [c
f,c
g] = forall x. Dualisable x => Dual x -> x
fromDual (forall c. Oriented c => Mltp2 c -> Path c
pthMltp2 Dual (Mltp2 c)
fg')
  
--------------------------------------------------------------------------------
-- Mltp3 -

-- | predicate for three multiplicable factors.
data Mltp3 c = Mltp3 c c c deriving (Int -> Mltp3 c -> ShowS
forall c. Show c => Int -> Mltp3 c -> ShowS
forall c. Show c => [Mltp3 c] -> ShowS
forall c. Show c => Mltp3 c -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Mltp3 c] -> ShowS
$cshowList :: forall c. Show c => [Mltp3 c] -> ShowS
show :: Mltp3 c -> String
$cshow :: forall c. Show c => Mltp3 c -> String
showsPrec :: Int -> Mltp3 c -> ShowS
$cshowsPrec :: forall c. Show c => Int -> Mltp3 c -> ShowS
Show,Mltp3 c -> Mltp3 c -> Bool
forall c. Eq c => Mltp3 c -> Mltp3 c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Mltp3 c -> Mltp3 c -> Bool
$c/= :: forall c. Eq c => Mltp3 c -> Mltp3 c -> Bool
== :: Mltp3 c -> Mltp3 c -> Bool
$c== :: forall c. Eq c => Mltp3 c -> Mltp3 c -> Bool
Eq,Mltp3 c -> Mltp3 c -> Bool
Mltp3 c -> Mltp3 c -> Ordering
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
forall {c}. Ord c => Eq (Mltp3 c)
forall c. Ord c => Mltp3 c -> Mltp3 c -> Bool
forall c. Ord c => Mltp3 c -> Mltp3 c -> Ordering
forall c. Ord c => Mltp3 c -> Mltp3 c -> Mltp3 c
min :: Mltp3 c -> Mltp3 c -> Mltp3 c
$cmin :: forall c. Ord c => Mltp3 c -> Mltp3 c -> Mltp3 c
max :: Mltp3 c -> Mltp3 c -> Mltp3 c
$cmax :: forall c. Ord c => Mltp3 c -> Mltp3 c -> Mltp3 c
>= :: Mltp3 c -> Mltp3 c -> Bool
$c>= :: forall c. Ord c => Mltp3 c -> Mltp3 c -> Bool
> :: Mltp3 c -> Mltp3 c -> Bool
$c> :: forall c. Ord c => Mltp3 c -> Mltp3 c -> Bool
<= :: Mltp3 c -> Mltp3 c -> Bool
$c<= :: forall c. Ord c => Mltp3 c -> Mltp3 c -> Bool
< :: Mltp3 c -> Mltp3 c -> Bool
$c< :: forall c. Ord c => Mltp3 c -> Mltp3 c -> Bool
compare :: Mltp3 c -> Mltp3 c -> Ordering
$ccompare :: forall c. Ord c => Mltp3 c -> Mltp3 c -> Ordering
Ord)

pthMltp3 :: Oriented c => Mltp3 c -> Path c
pthMltp3 :: forall c. Oriented c => Mltp3 c -> Path c
pthMltp3 (Mltp3 c
f c
g c
h) = forall q. Point q -> [q] -> Path q
Path (forall q. Oriented q => q -> Point q
start c
h) [c
f,c
g,c
h]

instance Oriented c => Validable (Mltp3 c) where
  valid :: Mltp3 c -> Statement
valid = forall a. Validable a => a -> Statement
valid forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall c. Oriented c => Mltp3 c -> Path c
pthMltp3
  
type instance Dual (Mltp3 c) = Mltp3 (Op c)

instance Oriented c => Dualisable (Mltp3 c) where
  toDual :: Mltp3 c -> Dual (Mltp3 c)
toDual Mltp3 c
fgh    = forall c. c -> c -> c -> Mltp3 c
Mltp3 Op c
f' Op c
g' Op c
h' where Path Point (Op c)
_ [Op c
f',Op c
g',Op c
h'] = forall x. Dualisable x => x -> Dual x
toDual (forall c. Oriented c => Mltp3 c -> Path c
pthMltp3 Mltp3 c
fgh)      
  fromDual :: Dual (Mltp3 c) -> Mltp3 c
fromDual Dual (Mltp3 c)
fgh' = forall c. c -> c -> c -> Mltp3 c
Mltp3 c
f c
g c
h where Path Point c
_ [c
f,c
g,c
h] = forall x. Dualisable x => Dual x -> x
fromDual (forall c. Oriented c => Mltp3 c -> Path c
pthMltp3 Dual (Mltp3 c)
fgh')


--------------------------------------------------------------------------------
-- prpMlt1 -

-- | validity of 'one' according to "OAlg.Structure.Multiplicative.Definition#Mlt1".
prpMlt1 :: Multiplicative c => p c -> X (Point c) -> Statement
prpMlt1 :: forall c (p :: * -> *).
Multiplicative c =>
p c -> X (Point c) -> Statement
prpMlt1 p c
s X (Point c)
xp = String -> Label
Prp String
"Mlt1"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X (Point c)
xp (\Point c
p -> (forall q. Oriented q => q -> Orientation (Point q)
orientation (forall c (p :: * -> *). Multiplicative c => p c -> Point c -> c
one' p c
s Point c
p) forall a. Eq a => a -> a -> Bool
== Point c
p forall p. p -> p -> Orientation p
:> Point c
p) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"p" String -> String -> Parameter
:= forall a. Show a => a -> String
show Point c
p])

--------------------------------------------------------------------------------
-- prpMlt2_1 -

-- | validity of '*' for two multiplicable factors according to
--   "OAlg.Structure.Multiplicative.Definition#Mlt2_1".
prpMlt2_1 :: Multiplicative c => Mltp2 c -> Statement
prpMlt2_1 :: forall c. Multiplicative c => Mltp2 c -> Statement
prpMlt2_1 m :: Mltp2 c
m@(Mltp2 c
f c
g) = String -> Label
Prp String
"Mlt2_1"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid c
fg
            , String -> Label
Label String
"start" Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Point q
start c
fg forall a. Eq a => a -> a -> Bool
== forall q. Oriented q => q -> Point q
start c
g) Bool -> Message -> Statement
:?> Message
prms
            , String -> Label
Label String
"end" Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Point q
end c
fg forall a. Eq a => a -> a -> Bool
== forall q. Oriented q => q -> Point q
end c
f) Bool -> Message -> Statement
:?> Message
prms
            ]
  where fg :: c
fg = c
fforall c. Multiplicative c => c -> c -> c
*c
g
        prms :: Message
prms = [Parameter] -> Message
Params [String
"m"String -> String -> Parameter
:=forall a. Show a => a -> String
show Mltp2 c
m]

--------------------------------------------------------------------------------
-- prpMlt2_2 -

-- | validity of '*' for two not multiplicable factors according to
--   "OAlg.Structure.Multiplicative.Definition#Mlt2_2".
prpMlt2_2 :: Multiplicative c => c -> c -> Statement
prpMlt2_2 :: forall c. Multiplicative c => c -> c -> Statement
prpMlt2_2 c
f c
g = String -> Label
Prp String
"Mlt2_2"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ Statement -> Statement
Not Statement
vfg forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` Statement -> SomeException -> Statement
someException Statement
SValid 
            , Statement
vfg forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` ArithmeticException -> Statement
nmp
            ]
  where vfg :: Statement
vfg = forall a. Validable a => a -> Statement
valid (c
fforall c. Multiplicative c => c -> c -> c
*c
g)
        nmp :: ArithmeticException -> Statement
nmp ArithmeticException
NotMultiplicable = Statement
SValid
        nmp ArithmeticException
_                = Statement
SInvalid
        
--------------------------------------------------------------------------------
-- prpMlt2 -

-- | validity of '*' according to "OAlg.Structure.Multiplicative.Definition#Mlt2".
prpMlt2 :: Multiplicative c => X (c,c) -> Statement
prpMlt2 :: forall c. Multiplicative c => X (c, c) -> Statement
prpMlt2 X (c, c)
xfg = String -> Label
Prp String
"Mlt2"
  Label -> Statement -> Statement
:<=>:  forall e. X e -> (e -> Statement) -> Statement
Forall X (c, c)
xfg (\(c
f,c
g)
                     -> let fg :: Mltp2 c
fg = forall c. c -> c -> Mltp2 c
Mltp2 c
f c
g
                         in [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid Mltp2 c
fg       Statement -> Statement -> Statement
|~> forall c. Multiplicative c => Mltp2 c -> Statement
prpMlt2_1 Mltp2 c
fg
                                , Statement -> Statement
Not (forall a. Validable a => a -> Statement
valid Mltp2 c
fg) Statement -> Statement -> Statement
|~> forall c. Multiplicative c => c -> c -> Statement
prpMlt2_2 c
f c
g
                                ]
                    )

--------------------------------------------------------------------------------
-- prpMlt3 -

-- | validity according to "OAlg.Structure.Multiplicative.Definition#Mlt3".
prpMlt3 :: Multiplicative c => X c -> Statement
prpMlt3 :: forall c. Multiplicative c => X c -> Statement
prpMlt3 X c
xa = String -> Label
Prp String
"Mlt3"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X c
xa (\c
f -> [Statement] -> Statement
And [ (forall c. Multiplicative c => Point c -> c
one (forall q. Oriented q => q -> Point q
end c
f) forall c. Multiplicative c => c -> c -> c
* c
f forall a. Eq a => a -> a -> Bool
== c
f) Bool -> Message -> Statement
:?> forall {a}. Show a => a -> Message
prm c
f
                             , (c
f forall c. Multiplicative c => c -> c -> c
* forall c. Multiplicative c => Point c -> c
one (forall q. Oriented q => q -> Point q
start c
f) forall a. Eq a => a -> a -> Bool
== c
f) Bool -> Message -> Statement
:?> forall {a}. Show a => a -> Message
prm c
f
                             ]
                  )
  where prm :: a -> Message
prm a
f = [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
f]

--------------------------------------------------------------------------------
-- prpMlt4 -

-- | validity according to "OAlg.Structure.Multiplicative.Definition#Mlt4".
prpMlt4 :: Multiplicative c => X (Mltp3 c) -> Statement
prpMlt4 :: forall c. Multiplicative c => X (Mltp3 c) -> Statement
prpMlt4 X (Mltp3 c)
xfgh = String -> Label
Prp String
"Mlt4"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X (Mltp3 c)
xfgh
          (\m :: Mltp3 c
m@(Mltp3 c
f c
g c
h ) -> ((c
f forall c. Multiplicative c => c -> c -> c
* c
g) forall c. Multiplicative c => c -> c -> c
* c
h forall a. Eq a => a -> a -> Bool
== c
f forall c. Multiplicative c => c -> c -> c
* (c
g forall c. Multiplicative c => c -> c -> c
* c
h)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"m"String -> String -> Parameter
:=forall a. Show a => a -> String
show Mltp3 c
m])


--------------------------------------------------------------------------------
-- prpMlt5 -

-- | validity of 'npower' according to "OAlg.Structure.Multiplicative.Definition#Mlt5".
--
-- __Note__ As the multiplication can by very costly the random variable for @t'X' t'N'@
-- - which serves to check "OAlg.Structure.Multiplicative.Definition#Mlt5_2" - has to be chosen
-- carefully.
prpMlt5 :: Multiplicative c => X N -> X c -> X (Endo c) -> Statement
prpMlt5 :: forall c. Multiplicative c => X N -> X c -> X (Endo c) -> Statement
prpMlt5 X N
xn X c
xf X (Endo c)
xfe = String -> Label
Prp String
"Mlt5"
  Label -> Statement -> Statement
:<=>: forall e. X e -> (e -> Statement) -> Statement
Forall X (N, c)
xnf (\(N
n,c
f) ->
                      [Statement] -> Statement
And [ String -> Label
Label String
"5.1"
                            Label -> Statement -> Statement
:<=>: (forall c. Multiplicative c => c -> N -> c
npower c
f N
1 forall a. Eq a => a -> a -> Bool
== c
f) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall a. Show a => a -> String
show c
f]
                          , String -> Label
Label String
"5.2"
                            Label -> Statement -> Statement
:<=>: forall q. Oriented q => q -> Bool
isEndo c
f Bool -> Message -> Statement
:?> Message
MInvalid
                              Statement -> Statement -> Statement
|~> [Statement] -> Statement
And [ (forall c. Multiplicative c => c -> N -> c
npower c
f N
0 forall a. Eq a => a -> a -> Bool
== forall c. Multiplicative c => Point c -> c
one (forall q. Oriented q => q -> Point q
start c
f))
                                        Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall a. Show a => a -> String
show c
f]
                                      , (forall c. Multiplicative c => c -> N -> c
npower c
f (forall a. Enum a => a -> a
succ N
n) forall a. Eq a => a -> a -> Bool
== c
f forall c. Multiplicative c => c -> c -> c
* forall c. Multiplicative c => c -> N -> c
npower c
f N
n)
                                        Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall a. Show a => a -> String
show c
f,String
"n"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
n]
                                      ]
                          ]
                   )
  where xf' :: X c
xf' = 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,forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall q. Endo q -> q
fromEndo X (Endo c)
xfe),(Q
1,X c
xf)]
        xnf :: X (N, c)
xnf = forall a b. X a -> X b -> X (a, b)
xTupple2 X N
xn X c
xf'

--------------------------------------------------------------------------------
-- XMlt -

-- | random variable for 'Multiplicative' structures.
--
--   __Note__ As the multiplication could by costly, it is recommended to
--   use a bounded random variable for 'xMltN' which serves to validate
--   'npower'.
data XMlt c = XMlt
  { forall c. XMlt c -> X N
xMltN      :: X N
  , forall c. XMlt c -> X (Point c)
xMltPoint  :: X (Point c)
  , forall c. XMlt c -> X c
xMltFactor :: X c
  , forall c. XMlt c -> X (Endo c)
xMltEndo   :: X (Endo c)
  , forall c. XMlt c -> X (Mltp2 c)
xMltMltp2  :: X (Mltp2 c)
  , forall c. XMlt c -> X (Mltp3 c)
xMltMltp3  :: X (Mltp3 c)
  }

--------------------------------------------------------------------------------
-- XMlt - Validable -

instance Oriented c => Validable (XMlt c) where
  valid :: XMlt c -> Statement
valid (XMlt X N
xn X (Point c)
xp X c
xc X (Endo c)
xe X (Mltp2 c)
xc2 X (Mltp3 c)
xc3)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid X N
xn
          , forall a. Validable a => a -> Statement
valid X (Point c)
xp
          , forall a. Validable a => a -> Statement
valid X c
xc
          , forall a. Validable a => a -> Statement
valid X (Endo c)
xe
          , forall a. Validable a => a -> Statement
valid X (Mltp2 c)
xc2
          , forall a. Validable a => a -> Statement
valid X (Mltp3 c)
xc3
          ]

--------------------------------------------------------------------------------
-- XMlt - Dualisable -

type instance Dual (XMlt c) = XMlt (Op c)

-- | the dual random variable with inverse 'coXMltInv'.
coXMlt :: XMlt c -> Dual (XMlt c)
coXMlt :: forall c. XMlt c -> Dual (XMlt c)
coXMlt (XMlt X N
xn X (Point c)
xp X c
xf X (Endo c)
xe X (Mltp2 c)
xf2 X (Mltp3 c)
xf3) = forall c.
X N
-> X (Point c)
-> X c
-> X (Endo c)
-> X (Mltp2 c)
-> X (Mltp3 c)
-> XMlt c
XMlt X N
xn X (Point c)
xp X (Op c)
xf' X (Endo (Op c))
xe' X (Mltp2 (Op c))
xf2' X (Mltp3 (Op c))
xf3' where
  xf' :: X (Op c)
xf'  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. x -> Op x
Op X c
xf
  xe' :: X (Endo (Op c))
xe'  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Endo c
e) -> forall q. q -> Endo q
Endo (forall x. x -> Op x
Op c
e)) X (Endo c)
xe
  xf2' :: X (Mltp2 (Op c))
xf2' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Mltp2 c
f c
g) -> forall c. c -> c -> Mltp2 c
Mltp2 (forall x. x -> Op x
Op c
g) (forall x. x -> Op x
Op c
f)) X (Mltp2 c)
xf2
  xf3' :: X (Mltp3 (Op c))
xf3' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Mltp3 c
f c
g c
h) -> forall c. c -> c -> c -> Mltp3 c
Mltp3 (forall x. x -> Op x
Op c
h) (forall x. x -> Op x
Op c
g) (forall x. x -> Op x
Op c
f)) X (Mltp3 c)
xf3


-- | from the bidual.
xMltFromOpOp :: XMlt (Op (Op c)) -> XMlt c
xMltFromOpOp :: forall c. XMlt (Op (Op c)) -> XMlt c
xMltFromOpOp (XMlt X N
xn X (Point (Op (Op c)))
xp X (Op (Op c))
xf X (Endo (Op (Op c)))
xe X (Mltp2 (Op (Op c)))
xf2 X (Mltp3 (Op (Op c)))
xf3) = forall c.
X N
-> X (Point c)
-> X c
-> X (Endo c)
-> X (Mltp2 c)
-> X (Mltp3 c)
-> XMlt c
XMlt X N
xn X (Point (Op (Op c)))
xp X c
xf' X (Endo c)
xe' X (Mltp2 c)
xf2' X (Mltp3 c)
xf3' where
  xf' :: X c
xf'  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Op (Op x) -> x
fromOpOp X (Op (Op c))
xf
  xe' :: X (Endo c)
xe'  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Endo Op (Op c)
e) -> forall q. q -> Endo q
Endo forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Op (Op x) -> x
fromOpOp Op (Op c)
e) X (Endo (Op (Op c)))
xe
  xf2' :: X (Mltp2 c)
xf2' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Mltp2 Op (Op c)
f Op (Op c)
g) -> forall c. c -> c -> Mltp2 c
Mltp2 (forall x. Op (Op x) -> x
fromOpOp Op (Op c)
f) (forall x. Op (Op x) -> x
fromOpOp Op (Op c)
g)) X (Mltp2 (Op (Op c)))
xf2
  xf3' :: X (Mltp3 c)
xf3' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Mltp3 Op (Op c)
f Op (Op c)
g Op (Op c)
h) -> forall c. c -> c -> c -> Mltp3 c
Mltp3 (forall x. Op (Op x) -> x
fromOpOp Op (Op c)
f) (forall x. Op (Op x) -> x
fromOpOp Op (Op c)
g) (forall x. Op (Op x) -> x
fromOpOp Op (Op c)
h)) X (Mltp3 (Op (Op c)))
xf3

-- | from the dual with inverse 'coXMlt'.
coXMltInv :: Dual (XMlt c) -> XMlt c
coXMltInv :: forall c. Dual (XMlt c) -> XMlt c
coXMltInv = forall c. XMlt (Op (Op c)) -> XMlt c
xMltFromOpOp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall c. XMlt c -> Dual (XMlt c)
coXMlt

--------------------------------------------------------------------------------
-- XStandarMultiplicative -

-- | standard random variable for 'Multiplicative' structures.
class XStandardMlt c where
  xStandardMlt :: XMlt c
  
--------------------------------------------------------------------------------
-- prpMlt -

-- | validity of the 'Multiplicative' structure of @__c__@.
prpMlt :: Multiplicative c => XMlt c -> Statement
prpMlt :: forall c. Multiplicative c => XMlt c -> Statement
prpMlt (XMlt X N
xn X (Point c)
xp X c
xf X (Endo c)
xfe X (Mltp2 c)
xf2 X (Mltp3 c)
xf3) = String -> Label
Prp String
"Mlt"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ forall c (p :: * -> *).
Multiplicative c =>
p c -> X (Point c) -> Statement
prpMlt1 X c
xf X (Point c)
xp
            , forall c. Multiplicative c => X (c, c) -> Statement
prpMlt2 X (c, c)
xfg
            , forall c. Multiplicative c => X c -> Statement
prpMlt3 X c
xf
            , forall c. Multiplicative c => X (Mltp3 c) -> Statement
prpMlt4 X (Mltp3 c)
xf3
            , forall c. Multiplicative c => X N -> X c -> X (Endo c) -> Statement
prpMlt5 X N
xn X c
xf X (Endo c)
xfe
            ]
  where xfg :: X (c, c)
xfg = forall a b. X a -> X b -> X (a, b)
xTupple2 X c
xf X c
xf forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Mltp2 c
f c
g) -> (c
f,c
g)) X (Mltp2 c)
xf2

--------------------------------------------------------------------------------
-- xMltTtl -

-- | random variable for total 'Multiplicative' structures.
xMltTtl :: Singleton (Point c) => X N -> X c -> XMlt c
xMltTtl :: forall c. Singleton (Point c) => X N -> X c -> XMlt c
xMltTtl X N
xn X c
xf = forall c.
X N
-> X (Point c)
-> X c
-> X (Endo c)
-> X (Mltp2 c)
-> X (Mltp3 c)
-> XMlt c
XMlt X N
xn (forall (m :: * -> *) a. Monad m => a -> m a
return forall s. Singleton s => s
unit) X c
xf X (Endo c)
xfe X (Mltp2 c)
xf2 X (Mltp3 c)
xf3
  where xfe :: X (Endo c)
xfe = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall q. q -> Endo q
Endo X c
xf -- as the multiplication is total.
        xf2 :: X (Mltp2 c)
xf2 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall c. c -> c -> Mltp2 c
Mltp2) (forall a b. X a -> X b -> X (a, b)
xTupple2 X c
xf X c
xf)
        xf3 :: X (Mltp3 c)
xf3 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 forall c. c -> c -> c -> Mltp3 c
Mltp3) (forall a b c. X a -> X b -> X c -> X (a, b, c)
xTupple3 X c
xf X c
xf X c
xf)

instance XStandardMlt N where
  xStandardMlt :: XMlt N
xStandardMlt = forall c. Singleton (Point c) => X N -> X c -> XMlt c
xMltTtl X N
xn forall x. XStandard x => X x
xStandard where
    xn :: X N
xn = N -> N -> X N
xNB N
0 N
20

instance XStandardMlt Z where
  xStandardMlt :: XMlt Z
xStandardMlt = forall c. Singleton (Point c) => X N -> X c -> XMlt c
xMltTtl X N
xn forall x. XStandard x => X x
xStandard where
    xn :: X N
xn = N -> N -> X N
xNB N
0 N
20

instance XStandardMlt Q where
  xStandardMlt :: XMlt Q
xStandardMlt = forall c. Singleton (Point c) => X N -> X c -> XMlt c
xMltTtl X N
xn forall x. XStandard x => X x
xStandard where
    xn :: X N
xn = N -> N -> X N
xNB N
0 N
20

--------------------------------------------------------------------------------
-- xMltp2 -

-- | random variable of two multiplicable factors.
xMltp2 :: Multiplicative c => XOrtSite d c -> X (Mltp2 c)
xMltp2 :: forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X (Mltp2 c)
xMltp2 XOrtSite d c
xa = do
  Path Point c
_ [c
f,c
g] <- forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> X (Path c)
xosPath XOrtSite d c
xa N
2
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall c. c -> c -> Mltp2 c
Mltp2 c
f c
g)

--------------------------------------------------------------------------------
-- xMltp3 -

-- | random variable of three multiplicable factors.
xMltp3 :: Multiplicative c => XOrtSite d c -> X (Mltp3 c)
xMltp3 :: forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X (Mltp3 c)
xMltp3 XOrtSite d c
xa = do
  Path Point c
_ [c
f,c
g,c
h] <- forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> X (Path c)
xosPath XOrtSite d c
xa N
3
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall c. c -> c -> c -> Mltp3 c
Mltp3 c
f c
g c
h)

--------------------------------------------------------------------------------
-- xMlt -

-- | random variable for 'Multiplicative' structures.
xMlt :: Multiplicative c => XOrtSite d c -> X N -> X (Endo c) -> XMlt c
xMlt :: forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X N -> X (Endo c) -> XMlt c
xMlt XOrtSite d c
xs X N
xn X (Endo c)
xfe = forall c.
X N
-> X (Point c)
-> X c
-> X (Endo c)
-> X (Mltp2 c)
-> X (Mltp3 c)
-> XMlt c
XMlt X N
xn X (Point c)
xp XOrt c
xf X (Endo c)
xfe X (Mltp2 c)
xf2 X (Mltp3 c)
xf3 where
  xp :: X (Point c)
xp  = forall (s :: Site) q. XOrtSite s q -> X (Point q)
xosPoint XOrtSite d c
xs
  xf :: XOrt c
xf  = forall q (s :: Site). Oriented q => XOrtSite s q -> XOrt q
xosOrt XOrtSite d c
xs
  xf2 :: X (Mltp2 c)
xf2 = forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X (Mltp2 c)
xMltp2 XOrtSite d c
xs
  xf3 :: X (Mltp3 c)
xf3 = forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X (Mltp3 c)
xMltp3 XOrtSite d c
xs

--------------------------------------------------------------------------------
-- xoMlt -

-- | the induced random variable for multiplicable structures.
xoMlt :: Multiplicative c => X N -> XOrtOrientation c -> XMlt c
xoMlt :: forall c. Multiplicative c => X N -> XOrtOrientation c -> XMlt c
xoMlt X N
xn XOrtOrientation c
xo = forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X N -> X (Endo c) -> XMlt c
xMlt (forall q. Oriented q => XOrtOrientation q -> XOrtSite 'From q
xoFrom XOrtOrientation c
xo) X N
xn X (Endo c)
xe where
  xe :: X (Endo c)
xe = do
    Point c
p <- forall q. Oriented q => XOrtOrientation q -> X (Point q)
xoPoint XOrtOrientation c
xo
    c
e <- forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation c
xo (Point c
pforall p. p -> p -> Orientation p
:>Point c
p)
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall q. q -> Endo q
Endo c
e)

--------------------------------------------------------------------------------
-- xMltOrnt -

-- | random variable for the 'Multiplicative' structure of @'Orientation' p@.
xMltOrnt :: Entity p => X N -> X p -> XMlt (Orientation p)
xMltOrnt :: forall p. Entity p => X N -> X p -> XMlt (Orientation p)
xMltOrnt X N
xn X p
xp = forall c. Multiplicative c => X N -> XOrtOrientation c -> XMlt c
xoMlt X N
xn (forall p. X p -> XOrtOrientation (Orientation p)
xoOrnt X p
xp)

dst :: Int -> IO ()
dst :: Int -> IO ()
dst Int
n = IO Omega
getOmega forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n X (Mltp3 (Orientation Symbol))
xx where
  xo :: XMlt (Orientation Symbol)
xo = forall p. Entity p => X N -> X p -> XMlt (Orientation p)
xMltOrnt (N -> N -> X N
xNB N
0 N
10) X Symbol
xSymbol
  xx :: X (Mltp3 (Orientation Symbol))
xx = forall c. XMlt c -> X (Mltp3 c)
xMltMltp3 XMlt (Orientation Symbol)
xo

instance (Entity p, XStandard p) => XStandardMlt (Orientation p) where
  xStandardMlt :: XMlt (Orientation p)
xStandardMlt = forall p. Entity p => X N -> X p -> XMlt (Orientation p)
xMltOrnt X N
xn forall x. XStandard x => X x
xStandard where
    xn :: X N
xn = N -> N -> X N
xNB N
0 N
1000