{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DataKinds #-}

-- |
-- Module      : OAlg.Entity.Product.Proposition
-- Description : propositions on products over oriented symbols
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- propositions on free products over 'Oriented' symbols with exponents in a 'Number'.
module OAlg.Entity.Product.Proposition
  (
    -- * Proposition
    prpProduct
  , prpOrtProductNOrntSymbol, prpOrtProductZOrntSymbol
  , prpMltProductNOrntSymbol, prpMltProductZOrntSymbol
  

    -- * Random Variables
  , xStartProduct, xStartProductForm
  , xPrdSymStart, xPrdSymMlt

    -- * Example
  , xT, dstT
  )
  where

import Control.Monad

import OAlg.Prelude

import OAlg.Data.Symbol hiding (P)
import OAlg.Data.Canonical
import OAlg.Data.Constructable

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Additive
import OAlg.Structure.Ring
import OAlg.Structure.Number

import OAlg.Entity.Product.Definition

--------------------------------------------------------------------------------
-- xStartProductForm -

-- | random variable of product forms with maximal /depth/ @d@ (a ':^' constructor
-- dose not increases the depth).
xStartProductForm :: (Oriented a, Number r)
  => XOrtSite From a -> X r -> N -> XOrtSite From (ProductForm r a)
xStartProductForm :: forall a r.
(Oriented a, Number r) =>
XOrtSite 'From a -> X r -> N -> XOrtSite 'From (ProductForm r a)
xStartProductForm xs :: XOrtSite 'From a
xs@(XStart X (Point a)
xp Point a -> X a
_) X r
xr N
d
  = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point a)
xp (forall {r} {a}.
(Number r, Oriented a) =>
N -> XOrtSite 'From a -> X r -> Point a -> X (ProductForm r a)
xPrdFrm' N
d XOrtSite 'From a
xs X r
xr) where

  xPrdFrm' :: N -> XOrtSite 'From a -> X r -> Point a -> X (ProductForm r a)
xPrdFrm' N
d XOrtSite 'From a
xs X r
xr Point a
p = do
    N
d' <- N -> N -> X N
xNB N
0 (N
dforall a. Additive a => a -> a -> a
+N
1)
    forall a r f.
(Oriented a, Number r, f ~ ProductForm r a) =>
N -> XOrtSite 'From a -> X r -> Point f -> X f
xPrdFrm N
d' XOrtSite 'From a
xs X r
xr Point a
p
  
  xBoolExp :: X Bool
xBoolExp = forall a. [(Q, a)] -> X a
xOneOfW [(Q
10,Bool
False),(Q
1,Bool
True)]

  -- random variable of 1 and -1 - if -1 exists.
  xOneMinusOne :: Number r => X r
  xOneMinusOne :: forall r. Number r => X r
xOneMinusOne = case forall r. Number r => Maybe r
minusOne of
    Just r
e  -> forall a. [a] -> X a
xOneOf [forall r. Semiring r => r
rOne,r
e]
    Maybe r
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall r. Semiring r => r
rOne 
  
  -- xExp True enriches the product form by a randomly picked exponent, but
  -- lets the orientation unchanged.
  xExp :: (Oriented a, Number r) => Bool -> X r -> ProductForm r a -> X (ProductForm r a)
  xExp :: forall a r.
(Oriented a, Number r) =>
Bool -> X r -> ProductForm r a -> X (ProductForm r a)
xExp Bool
False X r
_ ProductForm r a
pf             = forall (m :: * -> *) a. Monad m => a -> m a
return ProductForm r a
pf
  xExp Bool
True X r
xr ProductForm r a
pf | forall q. Oriented q => q -> Bool
isEndo ProductForm r a
pf = X r
xr forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (ProductForm r a
pfforall r a. ProductForm r a -> r -> ProductForm r a
:^)
                  | Bool
otherwise = do
    r
r   <- forall r. Number r => X r
xOneMinusOne
    ProductForm r a
pf' <- forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ if r
r forall a. Ord a => a -> a -> Bool
< forall r. Semiring r => r
rZero then forall r a. Number r => ProductForm r a -> ProductForm r a
prfInverse ProductForm r a
pf else ProductForm r a
pf
    forall (m :: * -> *) a. Monad m => a -> m a
return (ProductForm r a
pf'forall r a. ProductForm r a -> r -> ProductForm r a
:^r
r)

  xPrdFrm :: (Oriented a, Number r, f ~ ProductForm r a)
    => N -> XOrtSite From a -> X r -> Point f -> X f
  xPrdFrm :: forall a r f.
(Oriented a, Number r, f ~ ProductForm r a) =>
N -> XOrtSite 'From a -> X r -> Point f -> X f
xPrdFrm N
0 XOrtSite 'From a
_ X r
xr Point f
p = do
    Bool
b  <- X Bool
xBoolExp
    ProductForm r a
pf <- forall a r.
(Oriented a, Number r) =>
Bool -> X r -> ProductForm r a -> X (ProductForm r a)
xExp Bool
b X r
xr (forall r a. Point a -> ProductForm r a
One Point f
p)
    forall (m :: * -> *) a. Monad m => a -> m a
return ProductForm r a
pf

  xPrdFrm N
1 XOrtSite 'From a
xs X r
xr Point f
p = do
    Path a
pth <- forall q (s :: Site).
Oriented q =>
XOrtSite s q -> N -> Point q -> X (Path q)
xosPathMaxAt XOrtSite 'From a
xs N
1 Point f
p
    case Path a
pth of
      Path Point a
_ []    -> forall a r f.
(Oriented a, Number r, f ~ ProductForm r a) =>
N -> XOrtSite 'From a -> X r -> Point f -> X f
xPrdFrm N
0 XOrtSite 'From a
xs X r
xr Point f
p
      Path Point a
_ (a
a:[a]
_) -> do
        Bool
b  <- X Bool
xBoolExp
        ProductForm r a
pf <- forall a r.
(Oriented a, Number r) =>
Bool -> X r -> ProductForm r a -> X (ProductForm r a)
xExp Bool
b X r
xr (forall r a. a -> ProductForm r a
P a
a)
        forall (m :: * -> *) a. Monad m => a -> m a
return ProductForm r a
pf

  xPrdFrm N
d XOrtSite 'From a
xs X r
xr Point f
p = do
    (N
df,N
dg) <- forall a b. X a -> X b -> X (a, b)
xTupple2 X N
xd X N
xd
    ProductForm r a
g       <- forall a r f.
(Oriented a, Number r, f ~ ProductForm r a) =>
N -> XOrtSite 'From a -> X r -> Point f -> X f
xPrdFrm N
df XOrtSite 'From a
xs X r
xr Point f
p
    ProductForm r a
f       <- forall a r f.
(Oriented a, Number r, f ~ ProductForm r a) =>
N -> XOrtSite 'From a -> X r -> Point f -> X f
xPrdFrm N
dg XOrtSite 'From a
xs X r
xr (forall q. Oriented q => q -> Point q
end ProductForm r a
g)
    (Bool
bf,Bool
bg) <- forall a b. X a -> X b -> X (a, b)
xTupple2 X Bool
xBoolExp X Bool
xBoolExp
    ProductForm r a
g'      <- forall a r.
(Oriented a, Number r) =>
Bool -> X r -> ProductForm r a -> X (ProductForm r a)
xExp Bool
bg X r
xr ProductForm r a
g
    ProductForm r a
f'      <- forall a r.
(Oriented a, Number r) =>
Bool -> X r -> ProductForm r a -> X (ProductForm r a)
xExp Bool
bf X r
xr ProductForm r a
f
    Bool
b       <- X Bool
xBoolExp
    forall a r.
(Oriented a, Number r) =>
Bool -> X r -> ProductForm r a -> X (ProductForm r a)
xExp Bool
b X r
xr (ProductForm r a
f'forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:*ProductForm r a
g')
    where xd :: X N
xd = 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,N -> N -> X N
xNB N
1 (N
dN -> N -> N
>-N
1)),(Q
1,forall (m :: * -> *) a. Monad m => a -> m a
return N
0)]


--------------------------------------------------------------------------------
-- xEndProductForm -

-- | the induced random variable.
xEndProductForm :: (Oriented a, Number r) 
  => XOrtSite To a -> X r -> N -> XOrtSite To (ProductForm r a)
xEndProductForm :: forall a r.
(Oriented a, Number r) =>
XOrtSite 'To a -> X r -> N -> XOrtSite 'To (ProductForm r a)
xEndProductForm XOrtSite 'To a
xEnd X r
xr N
n = forall r a.
XOrtSite 'From (ProductForm r (Op a))
-> XOrtSite 'To (ProductForm r a)
fDual forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a r.
(Oriented a, Number r) =>
XOrtSite 'From a -> X r -> N -> XOrtSite 'From (ProductForm r a)
xStartProductForm (forall x. Dualisable x => x -> Dual x
toDual XOrtSite 'To a
xEnd) X r
xr N
n where
  fDual :: XOrtSite From (ProductForm r (Op a)) -> XOrtSite To (ProductForm r a)
  fDual :: forall r a.
XOrtSite 'From (ProductForm r (Op a))
-> XOrtSite 'To (ProductForm r a)
fDual XOrtSite 'From (ProductForm r (Op a))
xs = forall x. Dualisable x => Dual x -> x
fromDual (forall r a.
XOrtSite 'From (ProductForm r (Op a))
-> XOrtSite 'From (Op (ProductForm r a))
hh XOrtSite 'From (ProductForm r (Op a))
xs)

  hh :: XOrtSite From (ProductForm r (Op a)) -> XOrtSite From (Op (ProductForm r a))
  hh :: forall r a.
XOrtSite 'From (ProductForm r (Op a))
-> XOrtSite 'From (Op (ProductForm r a))
hh (XStart X (Point (ProductForm r (Op a)))
xp Point (ProductForm r (Op a)) -> X (ProductForm r (Op a))
xof) = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point (ProductForm r (Op a)))
xp Point a -> X (Op (ProductForm r a))
xof' where
    xof' :: Point a -> X (Op (ProductForm r a))
xof' Point a
p = forall r a. X (ProductForm r (Op a)) -> X (Op (ProductForm r a))
ff (Point (ProductForm r (Op a)) -> X (ProductForm r (Op a))
xof Point a
p)

  ff :: X (ProductForm r (Op a)) -> X (Op (ProductForm r a))
  ff :: forall r a. X (ProductForm r (Op a)) -> X (Op (ProductForm r a))
ff = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall x. x -> Op x
Op forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall r a. ProductForm r (Op a) -> ProductForm r a
prfFromOp)

--------------------------------------------------------------------------------
-- dstXStartProductFrom -

dstXStartProductForm :: Int -> N -> IO ()
dstXStartProductForm :: Int -> N -> IO ()
dstXStartProductForm Int
n N
d = 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 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {r} {a}. ProductForm r a -> (N, N)
asps X (ProductForm Z (Orientation Symbol))
xpf)
  where
    -- asps pf = (dpth pf,skew pf,exp pf)
    -- asps pf = start pf == E && validate' (valid pf)
    asps :: ProductForm r a -> (N, N)
asps ProductForm r a
pf = (forall r a. ProductForm r a -> N
dpth ProductForm r a
pf,forall r a. ProductForm r a -> N
exp ProductForm r a
pf)
    -- asps pf = exp pf
    -- asps pf = (dpth pf,endos pf,exp pf)
    -- asps pf = dpth pf
  
    xpf :: X (ProductForm Z (Orientation Symbol))
xpf = forall q. XOrtSite 'From q -> Point q -> X q
xosStart (forall a r.
(Oriented a, Number r) =>
XOrtSite 'From a -> X r -> N -> XOrtSite 'From (ProductForm r a)
xStartProductForm (forall p. X p -> XOrtSite 'From (Orientation p)
xStartOrnt X Symbol
xSymbol) X Z
xr N
d) Symbol
E
  
    xr :: X Z
xr = Z -> Z -> X Z
xZB (-Z
10) Z
10

dpth :: ProductForm r a -> N
dpth :: forall r a. ProductForm r a -> N
dpth (One Point a
_) = N
0
dpth (P a
_)   = N
1
dpth (ProductForm r a
f:^r
_)  = forall r a. ProductForm r a -> N
dpth ProductForm r a
f
dpth (ProductForm r a
f:*ProductForm r a
g)  = forall a. Ord a => a -> a -> a
max (forall r a. ProductForm r a -> N
dpth ProductForm r a
f) (forall r a. ProductForm r a -> N
dpth ProductForm r a
g) forall a. Additive a => a -> a -> a
+ N
1
  
skew :: ProductForm r a -> Z
skew :: forall r a. ProductForm r a -> Z
skew (One Point a
_) = Z
0
skew (P a
_)   = Z
1
skew (ProductForm r a
f:^r
_)  = forall r a. ProductForm r a -> Z
skew ProductForm r a
f
skew (ProductForm r a
f:*ProductForm r a
g)  = forall r a. ProductForm r a -> Z
skew ProductForm r a
g forall a. Abelian a => a -> a -> a
- forall r a. ProductForm r a -> Z
skew ProductForm r a
f
  
exp :: ProductForm r a -> N
exp :: forall r a. ProductForm r a -> N
exp (ProductForm r a
f:^r
_) = forall r a. ProductForm r a -> N
exp ProductForm r a
f forall a. Additive a => a -> a -> a
+ N
1
exp (ProductForm r a
f:*ProductForm r a
g) = forall r a. ProductForm r a -> N
exp ProductForm r a
f forall a. Additive a => a -> a -> a
+ forall r a. ProductForm r a -> N
exp ProductForm r a
g
exp ProductForm r a
_      = N
0
{-
true1 True = 1
true1 _    = 0

endos :: (Oriented a, Number r) => ProductForm r a -> N
endos (One _) = 1
endos (P a)   = true1 $ isEndo a
endos (f:^_)  = endos f
endos (f:*g)  = endos f + endos g + true1 (isEndo (f:*g))
-}


--------------------------------------------------------------------------------
-- xStartProduct -

-- | random variable of products generated from product forms with a maximal given /depth/
-- (':^' dose not increases the depth).
xStartProduct :: (Oriented a, Integral r) => XOrtSite From a -> X r
  -> N -> XOrtSite From (Product r a)
xStartProduct :: forall a r.
(Oriented a, Integral r) =>
XOrtSite 'From a -> X r -> N -> XOrtSite 'From (Product r a)
xStartProduct XOrtSite 'From a
xs X r
xr N
d
  = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart (forall (s :: Site) q. XOrtSite s q -> X (Point q)
xosPoint XOrtSite 'From a
xs) (forall a r.
(Oriented a, Integral r) =>
(Point a -> X (ProductForm r a)) -> Point a -> X (Product r a)
xPrd forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall q. XOrtSite 'From q -> Point q -> X q
xosStart forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a r.
(Oriented a, Number r) =>
XOrtSite 'From a -> X r -> N -> XOrtSite 'From (ProductForm r a)
xStartProductForm XOrtSite 'From a
xs X r
xr N
d) where
    xPrd :: (Oriented a, Integral r)
         => (Point a -> X (ProductForm r a))
         -> Point a -> X (Product r a)
    xPrd :: forall a r.
(Oriented a, Integral r) =>
(Point a -> X (ProductForm r a)) -> Point a -> X (Product r a)
xPrd Point a -> X (ProductForm r a)
ixpf = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Constructable x => Form x -> x
make forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Point a -> X (ProductForm r a)
ixpf


--------------------------------------------------------------------------------
-- xEndProduct -

-- | random variable of products generated from product forms with a maximal given /depth/
-- (':^' dose not increases the depth).
xEndProduct :: (Oriented a, Integral r) => XOrtSite To a -> X r
  -> N -> XOrtSite To (Product r a)
xEndProduct :: forall a r.
(Oriented a, Integral r) =>
XOrtSite 'To a -> X r -> N -> XOrtSite 'To (Product r a)
xEndProduct XOrtSite 'To a
xe X r
xr N
d
  = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd (forall (s :: Site) q. XOrtSite s q -> X (Point q)
xosPoint XOrtSite 'To a
xe) (forall a r.
(Oriented a, Integral r) =>
(Point a -> X (ProductForm r a)) -> Point a -> X (Product r a)
xPrd forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall q. XOrtSite 'To q -> Point q -> X q
xosEnd forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a r.
(Oriented a, Number r) =>
XOrtSite 'To a -> X r -> N -> XOrtSite 'To (ProductForm r a)
xEndProductForm XOrtSite 'To a
xe X r
xr N
d) where
    xPrd :: (Oriented a, Integral r)
         => (Point a -> X (ProductForm r a))
         -> Point a -> X (Product r a)
    xPrd :: forall a r.
(Oriented a, Integral r) =>
(Point a -> X (ProductForm r a)) -> Point a -> X (Product r a)
xPrd Point a -> X (ProductForm r a)
ixpf = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Constructable x => Form x -> x
make forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Point a -> X (ProductForm r a)
ixpf


--------------------------------------------------------------------------------
-- dstXStartProduct -

dstXStartProduct :: Int -> N -> IO ()
dstXStartProduct :: Int -> N -> IO ()
dstXStartProduct Int
n N
d = 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 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {x} {r} {a}.
(Form x ~ ProductForm r a, Exposable x) =>
x -> (N, N)
asps X (Product Z (Orientation Symbol))
xprd)
  where
    -- asps pf = (dpth pf,skew pf,exp pf)
    -- asps pf = 
    -- asps pf = (dpth pf,exp pf)
    -- asps pf = exp pf
    
    -- asps (Just p) = start p == 'e' && validate' (valid p)
    asps :: x -> (N, N)
asps x
p = (forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall r a. ProductForm r a -> N
dpth x
p,forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall r a. ProductForm r a -> N
exp x
p)
    
    xprd :: X (Product Z (Orientation Symbol))
xprd = forall q. XOrtSite 'From q -> Point q -> X q
xosStart (forall a r.
(Oriented a, Integral r) =>
XOrtSite 'From a -> X r -> N -> XOrtSite 'From (Product r a)
xStartProduct (forall p. X p -> XOrtSite 'From (Orientation p)
xStartOrnt X Symbol
xSymbol) X Z
xr N
d) Symbol
E
    -- xprd = xStartProduct (XStart xPthChar) xr d
  
    xr :: X Z
xr = Z -> Z -> X Z
xZB (-Z
10) Z
10

--------------------------------------------------------------------------------
-- dstXEndProduct -

dstXEndProduct :: Int -> N -> IO ()
dstXEndProduct :: Int -> N -> IO ()
dstXEndProduct Int
n N
d = 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 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a} {r} {a}.
(Form a ~ ProductForm r a, Exposable a, Validable a) =>
a -> (N, N, Bool)
asps X (Product Z (Orientation Symbol))
xprd)
  where
    -- asps pf = (dpth pf,skew pf,exp pf)
    -- asps pf = 
    -- asps pf = (dpth pf,exp pf)
    -- asps pf = exp pf
    
    -- asps (Just p) = start p == 'e' && validate' (valid p)
    asps :: a -> (N, N, Bool)
asps a
p = (forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall r a. ProductForm r a -> N
dpth a
p,forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall r a. ProductForm r a -> N
exp a
p,Statement -> Bool
validate' (forall a. Validable a => a -> Statement
valid a
p))
    
    xprd :: X (Product Z (Orientation Symbol))
xprd = forall q. XOrtSite 'To q -> Point q -> X q
xosEnd (forall a r.
(Oriented a, Integral r) =>
XOrtSite 'To a -> X r -> N -> XOrtSite 'To (Product r a)
xEndProduct (forall p. X p -> XOrtSite 'To (Orientation p)
xEndOrnt X Symbol
xSymbol) X Z
xr N
d) Symbol
E
    -- xprd = xEndProduct (XEnd xPthChar) xr d
  
    xr :: X Z
xr = Z -> Z -> X Z
xZB (-Z
10) Z
10

--------------------------------------------------------------------------------
-- xStartProductSymbol -

-- | the induced random variable on @'Orientation' 'Symbol')@.
xPrdSymStart :: Integral r => N -> X r -> XOrtSite From (Product r (Orientation Symbol))
xPrdSymStart :: forall r.
Integral r =>
N -> X r -> XOrtSite 'From (Product r (Orientation Symbol))
xPrdSymStart N
d X r
xr = forall a r.
(Oriented a, Integral r) =>
XOrtSite 'From a -> X r -> N -> XOrtSite 'From (Product r a)
xStartProduct (forall p. X p -> XOrtSite 'From (Orientation p)
xStartOrnt X Symbol
xSymbol) X r
xr N
d

xPrdSymEndo :: (Entity p, Integral r, m ~ Product r (Orientation p))
  => X m -> X (Endo m)
xPrdSymEndo :: forall p r m.
(Entity p, Integral r, m ~ Product r (Orientation p)) =>
X m -> X (Endo m)
xPrdSymEndo X m
xpr = do
  m
p <- X m
xpr
  forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall q. q -> Endo q
Endo forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ if forall q. Oriented q => q -> Bool
isEndo m
p then m
p else (forall a b. Embeddable a b => a -> b
inj (forall q. Oriented q => q -> Point q
end m
pforall p. p -> p -> Orientation p
:>forall q. Oriented q => q -> Point q
start m
p) forall c. Multiplicative c => c -> c -> c
* m
p)

--------------------------------------------------------------------------------
-- xPrdSymMlt -

-- | the induced random variable for validating 'Multiplicative' structures.
xPrdSymMlt :: Integral r => N -> X r -> XMlt (Product r (Orientation Symbol))
xPrdSymMlt :: forall r.
Integral r =>
N -> X r -> XMlt (Product r (Orientation Symbol))
xPrdSymMlt N
d X r
xr = forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X N -> X (Endo c) -> XMlt c
xMlt XOrtSite 'From (Product r (Orientation Symbol))
xs X N
xn X (Endo (Product r (Orientation Symbol)))
xe where
  xn :: X N
xn = N -> N -> X N
xNB N
0 N
10
  xs :: XOrtSite 'From (Product r (Orientation Symbol))
xs = forall r.
Integral r =>
N -> X r -> XOrtSite 'From (Product r (Orientation Symbol))
xPrdSymStart N
d X r
xr
  xe :: X (Endo (Product r (Orientation Symbol)))
xe = forall p r m.
(Entity p, Integral r, m ~ Product r (Orientation p)) =>
X m -> X (Endo m)
xPrdSymEndo forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall q (s :: Site). Oriented q => XOrtSite s q -> XOrt q
xosOrt XOrtSite 'From (Product r (Orientation Symbol))
xs

--------------------------------------------------------------------------------
-- prpOrtProductNOrntSymbol -

-- | validity of @'Product' t'N' ('Orientation' 'Symbol')@ being 'Oriented'.
prpOrtProductNOrntSymbol :: Statement
prpOrtProductNOrntSymbol :: Statement
prpOrtProductNOrntSymbol = String -> Label
Prp String
"OrtProductNOrntSymbol"
  Label -> Statement -> Statement
:<=>: forall q. Oriented q => XOrt q -> Statement
prpOrt XOrt (Product N (Orientation Symbol))
xprd where
    xr :: X N
xr   = N -> N -> X N
xNB N
0 N
3
    xprd :: XOrt (Product N (Orientation Symbol))
xprd = forall q (s :: Site). Oriented q => XOrtSite s q -> XOrt q
xosOrt forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r.
Integral r =>
N -> X r -> XOrtSite 'From (Product r (Orientation Symbol))
xPrdSymStart N
7 X N
xr

--------------------------------------------------------------------------------
-- prpOrtProductZOrntSymbol -

-- | validity of @'Product' t'Z' ('Orientation' 'Symbol')@ being 'Oriented'.
prpOrtProductZOrntSymbol :: Statement
prpOrtProductZOrntSymbol :: Statement
prpOrtProductZOrntSymbol = String -> Label
Prp String
"OrtProductZOrntSymbol"
  Label -> Statement -> Statement
:<=>: forall q. Oriented q => XOrt q -> Statement
prpOrt X (Product Z (Orientation Symbol))
xprd where
    xr :: X Z
xr   = Z -> Z -> X Z
xZB (-Z
5) Z
5
    xprd :: X (Product Z (Orientation Symbol))
xprd = forall q (s :: Site). Oriented q => XOrtSite s q -> XOrt q
xosOrt forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall r.
Integral r =>
N -> X r -> XOrtSite 'From (Product r (Orientation Symbol))
xPrdSymStart N
11 X Z
xr 

--------------------------------------------------------------------------------
-- prpMltProductNOrntSymbol -

-- | validity of @'Product' t'N' ('Orientation' 'Symbol')@ being 'Multiplicative'.
prpMltProductNOrntSymbol :: Statement
prpMltProductNOrntSymbol :: Statement
prpMltProductNOrntSymbol = String -> Label
Prp String
"MltProductNOrntSymbol"
  Label -> Statement -> Statement
:<=>: forall c. Multiplicative c => XMlt c -> Statement
prpMlt XMlt (Product N (Orientation Symbol))
xprd where
    xr :: X N
xr   = N -> N -> X N
xNB N
0 N
7
    xprd :: XMlt (Product N (Orientation Symbol))
xprd = forall r.
Integral r =>
N -> X r -> XMlt (Product r (Orientation Symbol))
xPrdSymMlt N
7 X N
xr

--------------------------------------------------------------------------------
-- prpMltProductZOrntSymbol -

-- | validity of @'Product' t'Z' ('Orientation' 'Symbol')@ being 'Multiplicative'.
prpMltProductZOrntSymbol :: Statement
prpMltProductZOrntSymbol :: Statement
prpMltProductZOrntSymbol = String -> Label
Prp String
"MltProductZOrntSymbol"
  Label -> Statement -> Statement
:<=>: forall c. Multiplicative c => XMlt c -> Statement
prpMlt XMlt (Product Z (Orientation Symbol))
xprd where
    xr :: X Z
xr   = Z -> Z -> X Z
xZB (-Z
7) Z
7
    xprd :: XMlt (Product Z (Orientation Symbol))
xprd = forall r.
Integral r =>
N -> X r -> XMlt (Product r (Orientation Symbol))
xPrdSymMlt N
7 X Z
xr

--------------------------------------------------------------------------------
-- prpProduct -

-- | validity of @'Product' __r__ ('Orientation' 'Symbol')@ for @__r__@ equal to t'N' and t'Z'
-- respectively
prpProduct :: Statement
prpProduct :: Statement
prpProduct = String -> Label
Prp String
"Product"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ Statement
prpOrtProductNOrntSymbol
            , Statement
prpOrtProductZOrntSymbol
            , Statement
prpMltProductNOrntSymbol
            , Statement
prpMltProductZOrntSymbol
            ]


--------------------------------------------------------------------------------
-- Example -

-- | example of a 'XStart' for the quiver having two points \'a\' and \'b\' and two
--   arrows @\'a\':>\'a\'@ and @\'a\':>\'b\'@.
xT :: XOrtSite From (Orientation Char)
xT :: XOrtSite 'From (Orientation Char)
xT = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X Char
xp Char -> X (Orientation Char)
mxs where
  xp :: X Char
xp  = forall a. [(Q, a)] -> X a
xOneOfW [(Q
10,Char
'a'),(Q
1,Char
'b')]
  mxs :: Char -> X (Orientation Char)
mxs Char
'a' = forall a. [(Q, a)] -> X a
xOneOfW [(Q
2,(Char
'a'forall p. p -> p -> Orientation p
:>Char
'a')),(Q
1,(Char
'a'forall p. p -> p -> Orientation p
:>Char
'b'))]
  mxs Char
_   = forall x. X x
XEmpty

-- | its distribution
dstT :: Int -> N -> IO ()
dstT :: Int -> N -> IO ()
dstT Int
n N
d = 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 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Product N (Orientation Char) -> String
asps X (Product N (Orientation Char))
xprd) where
  asps :: Product N (Orientation Char) -> String
asps = forall a. Show a => a -> String
show
  xprd :: X (Product N (Orientation Char))
xprd = forall q. XOrtSite 'From q -> Point q -> X q
xosStart (forall a r.
(Oriented a, Integral r) =>
XOrtSite 'From a -> X r -> N -> XOrtSite 'From (Product r a)
xStartProduct XOrtSite 'From (Orientation Char)
xT X N
xn N
d) Char
'a'
  xn :: X N
xn = N -> N -> X N
xNB N
0 N
10