{-# 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
  = X (Point (ProductForm r a))
-> (Point (ProductForm r a) -> X (ProductForm r a))
-> XOrtSite 'From (ProductForm r a)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point a)
X (Point (ProductForm r a))
xp (N -> XOrtSite 'From a -> X r -> Point a -> X (ProductForm r a)
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
dN -> N -> N
forall a. Additive a => a -> a -> a
+N
1)
    N
-> XOrtSite 'From a
-> X r
-> Point (ProductForm r a)
-> X (ProductForm r 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
d' XOrtSite 'From a
xs X r
xr Point a
Point (ProductForm r a)
p
  
  xBoolExp :: X Bool
xBoolExp = [(Q, Bool)] -> X Bool
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 Maybe r
forall r. Number r => Maybe r
minusOne of
    Just r
e  -> [r] -> X r
forall a. [a] -> X a
xOneOf [r
forall r. Semiring r => r
rOne,r
e]
    Maybe r
Nothing -> r -> X r
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return r
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             = ProductForm r a -> X (ProductForm r a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ProductForm r a
pf
  xExp Bool
True X r
xr ProductForm r a
pf | ProductForm r a -> Bool
forall q. Oriented q => q -> Bool
isEndo ProductForm r a
pf = X r
xr X r -> (r -> X (ProductForm r a)) -> X (ProductForm r a)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ProductForm r a -> X (ProductForm r a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProductForm r a -> X (ProductForm r a))
-> (r -> ProductForm r a) -> r -> X (ProductForm r a)
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
. (ProductForm r a
pfProductForm r a -> r -> ProductForm r a
forall r a. ProductForm r a -> r -> ProductForm r a
:^)
                  | Bool
otherwise = do
    r
r   <- X r
forall r. Number r => X r
xOneMinusOne
    ProductForm r a
pf' <- ProductForm r a -> X (ProductForm r a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProductForm r a -> X (ProductForm r a))
-> ProductForm r a -> X (ProductForm r a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ if r
r r -> r -> Bool
forall a. Ord a => a -> a -> Bool
< r
forall r. Semiring r => r
rZero then ProductForm r a -> ProductForm r a
forall r a. Number r => ProductForm r a -> ProductForm r a
prfInverse ProductForm r a
pf else ProductForm r a
pf
    ProductForm r a -> X (ProductForm r a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProductForm r a
pf'ProductForm r a -> r -> ProductForm r a
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 <- Bool -> X r -> ProductForm r a -> X (ProductForm r a)
forall a r.
(Oriented a, Number r) =>
Bool -> X r -> ProductForm r a -> X (ProductForm r a)
xExp Bool
b X r
xr (Point a -> ProductForm r a
forall r a. Point a -> ProductForm r a
One Point a
Point f
p)
    f -> X f
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return f
ProductForm r a
pf

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

  xPrdFrm N
d XOrtSite 'From a
xs X r
xr Point f
p = do
    (N
df,N
dg) <- X N -> X N -> X (N, N)
forall a b. X a -> X b -> X (a, b)
xTupple2 X N
xd X N
xd
    ProductForm r a
g       <- N
-> XOrtSite 'From a
-> X r
-> Point (ProductForm r a)
-> X (ProductForm r 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
df XOrtSite 'From a
xs X r
xr Point f
Point (ProductForm r a)
p
    ProductForm r a
f       <- N
-> XOrtSite 'From a
-> X r
-> Point (ProductForm r a)
-> X (ProductForm r 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
dg XOrtSite 'From a
xs X r
xr (ProductForm r a -> Point (ProductForm r a)
forall q. Oriented q => q -> Point q
end ProductForm r a
g)
    (Bool
bf,Bool
bg) <- X Bool -> X Bool -> X (Bool, Bool)
forall a b. X a -> X b -> X (a, b)
xTupple2 X Bool
xBoolExp X Bool
xBoolExp
    ProductForm r a
g'      <- Bool -> X r -> ProductForm r a -> X (ProductForm r a)
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'      <- Bool -> X r -> ProductForm r a -> X (ProductForm r a)
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
    Bool -> X r -> ProductForm r a -> X (ProductForm r a)
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'ProductForm r a -> ProductForm r a -> ProductForm r a
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:*ProductForm r a
g')
    where xd :: X N
xd = X (X N) -> X N
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (X (X N) -> X N) -> X (X N) -> X N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(Q, X N)] -> X (X N)
forall a. [(Q, a)] -> X a
xOneOfW [(Q
10,N -> N -> X N
xNB N
1 (N
dN -> N -> N
>-N
1)),(Q
1,N -> X N
forall a. a -> X a
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 = XOrtSite 'From (ProductForm r (Op a))
-> XOrtSite 'To (ProductForm r a)
forall r a.
XOrtSite 'From (ProductForm r (Op a))
-> XOrtSite 'To (ProductForm r a)
fDual (XOrtSite 'From (ProductForm r (Op a))
 -> XOrtSite 'To (ProductForm r a))
-> XOrtSite 'From (ProductForm r (Op a))
-> XOrtSite 'To (ProductForm r a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite 'From (Op a)
-> X r -> N -> XOrtSite 'From (ProductForm r (Op a))
forall a r.
(Oriented a, Number r) =>
XOrtSite 'From a -> X r -> N -> XOrtSite 'From (ProductForm r a)
xStartProductForm (XOrtSite 'To a -> Dual (XOrtSite 'To a)
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 = Dual (XOrtSite 'To (ProductForm r a))
-> XOrtSite 'To (ProductForm r a)
forall x. Dualisable x => Dual x -> x
fromDual (XOrtSite 'From (ProductForm r (Op a))
-> XOrtSite 'From (Op (ProductForm r a))
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) = X (Point (Op (ProductForm r a)))
-> (Point (Op (ProductForm r a)) -> X (Op (ProductForm r a)))
-> XOrtSite 'From (Op (ProductForm r a))
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point (Op (ProductForm r a)))
X (Point (ProductForm r (Op a)))
xp Point a -> X (Op (ProductForm r a))
Point (Op (ProductForm r a)) -> X (Op (ProductForm r a))
xof' where
    xof' :: Point a -> X (Op (ProductForm r a))
xof' Point a
p = X (ProductForm r (Op a)) -> X (Op (ProductForm r a))
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
Point (ProductForm r (Op 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 = (ProductForm r (Op a) -> Op (ProductForm r a))
-> X (ProductForm r (Op a)) -> X (Op (ProductForm r a))
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ProductForm r a -> Op (ProductForm r a)
forall x. x -> Op x
Op (ProductForm r a -> Op (ProductForm r a))
-> (ProductForm r (Op a) -> ProductForm r a)
-> ProductForm r (Op a)
-> Op (ProductForm r a)
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
. ProductForm r (Op a) -> ProductForm r a
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 IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X (N, N) -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n ((ProductForm Z (Orientation Symbol) -> (N, N))
-> X (ProductForm Z (Orientation Symbol)) -> X (N, N)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProductForm Z (Orientation Symbol) -> (N, N)
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 = (ProductForm r a -> N
forall r a. ProductForm r a -> N
dpth ProductForm r a
pf,ProductForm r a -> N
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 = XOrtSite 'From (ProductForm Z (Orientation Symbol))
-> Point (ProductForm Z (Orientation Symbol))
-> X (ProductForm Z (Orientation Symbol))
forall q. XOrtSite 'From q -> Point q -> X q
xosStart (XOrtSite 'From (Orientation Symbol)
-> X Z -> N -> XOrtSite 'From (ProductForm Z (Orientation Symbol))
forall a r.
(Oriented a, Number r) =>
XOrtSite 'From a -> X r -> N -> XOrtSite 'From (ProductForm r a)
xStartProductForm (X Symbol -> XOrtSite 'From (Orientation Symbol)
forall p. X p -> XOrtSite 'From (Orientation p)
xStartOrnt X Symbol
xSymbol) X Z
xr N
d) Symbol
Point (ProductForm Z (Orientation 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
_)  = ProductForm r a -> N
forall r a. ProductForm r a -> N
dpth ProductForm r a
f
dpth (ProductForm r a
f:*ProductForm r a
g)  = N -> N -> N
forall a. Ord a => a -> a -> a
max (ProductForm r a -> N
forall r a. ProductForm r a -> N
dpth ProductForm r a
f) (ProductForm r a -> N
forall r a. ProductForm r a -> N
dpth ProductForm r a
g) N -> N -> N
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
_)  = ProductForm r a -> Z
forall r a. ProductForm r a -> Z
skew ProductForm r a
f
skew (ProductForm r a
f:*ProductForm r a
g)  = ProductForm r a -> Z
forall r a. ProductForm r a -> Z
skew ProductForm r a
g Z -> Z -> Z
forall a. Abelian a => a -> a -> a
- ProductForm r a -> Z
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
_) = ProductForm r a -> N
forall r a. ProductForm r a -> N
exp ProductForm r a
f N -> N -> N
forall a. Additive a => a -> a -> a
+ N
1
exp (ProductForm r a
f:*ProductForm r a
g) = ProductForm r a -> N
forall r a. ProductForm r a -> N
exp ProductForm r a
f N -> N -> N
forall a. Additive a => a -> a -> a
+ ProductForm r a -> N
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
  = X (Point (Product r a))
-> (Point (Product r a) -> X (Product r a))
-> XOrtSite 'From (Product r a)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart (XOrtSite 'From a -> X (Point a)
forall (s :: Site) q. XOrtSite s q -> X (Point q)
xosPoint XOrtSite 'From a
xs) ((Point a -> X (ProductForm r a)) -> Point a -> X (Product r a)
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)) -> Point a -> X (Product r a))
-> (Point a -> X (ProductForm r a)) -> Point a -> X (Product r a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite 'From (ProductForm r a) -> Point a -> X (ProductForm r a)
XOrtSite 'From (ProductForm r a)
-> Point (ProductForm r a) -> X (ProductForm r a)
forall q. XOrtSite 'From q -> Point q -> X q
xosStart (XOrtSite 'From (ProductForm r a)
 -> Point a -> X (ProductForm r a))
-> XOrtSite 'From (ProductForm r a)
-> Point a
-> X (ProductForm r a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite 'From a -> X r -> N -> XOrtSite 'From (ProductForm r a)
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 = (ProductForm r a -> Product r a)
-> X (ProductForm r a) -> X (Product r a)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Form (Product r a) -> Product r a
ProductForm r a -> Product r a
forall x. Constructable x => Form x -> x
make (X (ProductForm r a) -> X (Product r a))
-> (Point a -> X (ProductForm r a)) -> Point a -> X (Product r a)
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
. 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
  = X (Point (Product r a))
-> (Point (Product r a) -> X (Product r a))
-> XOrtSite 'To (Product r a)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd (XOrtSite 'To a -> X (Point a)
forall (s :: Site) q. XOrtSite s q -> X (Point q)
xosPoint XOrtSite 'To a
xe) ((Point a -> X (ProductForm r a)) -> Point a -> X (Product r a)
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)) -> Point a -> X (Product r a))
-> (Point a -> X (ProductForm r a)) -> Point a -> X (Product r a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite 'To (ProductForm r a) -> Point a -> X (ProductForm r a)
XOrtSite 'To (ProductForm r a)
-> Point (ProductForm r a) -> X (ProductForm r a)
forall q. XOrtSite 'To q -> Point q -> X q
xosEnd (XOrtSite 'To (ProductForm r a) -> Point a -> X (ProductForm r a))
-> XOrtSite 'To (ProductForm r a) -> Point a -> X (ProductForm r a)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite 'To a -> X r -> N -> XOrtSite 'To (ProductForm r a)
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 = (ProductForm r a -> Product r a)
-> X (ProductForm r a) -> X (Product r a)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Form (Product r a) -> Product r a
ProductForm r a -> Product r a
forall x. Constructable x => Form x -> x
make (X (ProductForm r a) -> X (Product r a))
-> (Point a -> X (ProductForm r a)) -> Point a -> X (Product r a)
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
. Point a -> X (ProductForm r a)
ixpf


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

dstXStartProduct :: Int -> N -> IO ()
dstXStartProduct :: Int -> N -> IO ()
dstXStartProduct Int
n N
d = IO Omega
getOmega IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X (N, N) -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n ((Product Z (Orientation Symbol) -> (N, N))
-> X (Product Z (Orientation Symbol)) -> X (N, N)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Product Z (Orientation Symbol) -> (N, N)
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 = ((Form x -> N) -> x -> N
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form x -> N
ProductForm r a -> N
forall r a. ProductForm r a -> N
dpth x
p,(Form x -> N) -> x -> N
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form x -> N
ProductForm r a -> N
forall r a. ProductForm r a -> N
exp x
p)
    
    xprd :: X (Product Z (Orientation Symbol))
xprd = XOrtSite 'From (Product Z (Orientation Symbol))
-> Point (Product Z (Orientation Symbol))
-> X (Product Z (Orientation Symbol))
forall q. XOrtSite 'From q -> Point q -> X q
xosStart (XOrtSite 'From (Orientation Symbol)
-> X Z -> N -> XOrtSite 'From (Product Z (Orientation Symbol))
forall a r.
(Oriented a, Integral r) =>
XOrtSite 'From a -> X r -> N -> XOrtSite 'From (Product r a)
xStartProduct (X Symbol -> XOrtSite 'From (Orientation Symbol)
forall p. X p -> XOrtSite 'From (Orientation p)
xStartOrnt X Symbol
xSymbol) X Z
xr N
d) Symbol
Point (Product Z (Orientation 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 IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X (N, N, Bool) -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n ((Product Z (Orientation Symbol) -> (N, N, Bool))
-> X (Product Z (Orientation Symbol)) -> X (N, N, Bool)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Product Z (Orientation Symbol) -> (N, N, Bool)
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 = ((Form a -> N) -> a -> N
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form a -> N
ProductForm r a -> N
forall r a. ProductForm r a -> N
dpth a
p,(Form a -> N) -> a -> N
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form a -> N
ProductForm r a -> N
forall r a. ProductForm r a -> N
exp a
p,Statement -> Bool
validate' (a -> Statement
forall a. Validable a => a -> Statement
valid a
p))
    
    xprd :: X (Product Z (Orientation Symbol))
xprd = XOrtSite 'To (Product Z (Orientation Symbol))
-> Point (Product Z (Orientation Symbol))
-> X (Product Z (Orientation Symbol))
forall q. XOrtSite 'To q -> Point q -> X q
xosEnd (XOrtSite 'To (Orientation Symbol)
-> X Z -> N -> XOrtSite 'To (Product Z (Orientation Symbol))
forall a r.
(Oriented a, Integral r) =>
XOrtSite 'To a -> X r -> N -> XOrtSite 'To (Product r a)
xEndProduct (X Symbol -> XOrtSite 'To (Orientation Symbol)
forall p. X p -> XOrtSite 'To (Orientation p)
xEndOrnt X Symbol
xSymbol) X Z
xr N
d) Symbol
Point (Product Z (Orientation 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 = XOrtSite 'From (Orientation Symbol)
-> X r -> N -> XOrtSite 'From (Product r (Orientation Symbol))
forall a r.
(Oriented a, Integral r) =>
XOrtSite 'From a -> X r -> N -> XOrtSite 'From (Product r a)
xStartProduct (X Symbol -> XOrtSite 'From (Orientation Symbol)
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
  Endo (Product r (Orientation p)) -> X (Endo m)
Endo (Product r (Orientation p))
-> X (Endo (Product r (Orientation p)))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Endo (Product r (Orientation p)) -> X (Endo m))
-> Endo (Product r (Orientation p)) -> X (Endo m)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ m -> Endo (Product r (Orientation p))
Product r (Orientation p) -> Endo (Product r (Orientation p))
forall q. q -> Endo q
Endo (m -> Endo (Product r (Orientation p)))
-> m -> Endo (Product r (Orientation p))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ if m -> Bool
forall q. Oriented q => q -> Bool
isEndo m
p then m
p else (Orientation p -> m
forall a b. Embeddable a b => a -> b
inj (m -> Point m
forall q. Oriented q => q -> Point q
end m
pp -> p -> Orientation p
forall p. p -> p -> Orientation p
:>m -> Point m
forall q. Oriented q => q -> Point q
start m
p) m -> m -> m
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 = XOrtSite 'From (Product r (Orientation Symbol))
-> X N
-> X (Endo (Product r (Orientation Symbol)))
-> XMlt (Product r (Orientation Symbol))
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 = N -> X r -> XOrtSite 'From (Product r (Orientation Symbol))
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 = X (Product r (Orientation Symbol))
-> X (Endo (Product r (Orientation Symbol)))
forall p r m.
(Entity p, Integral r, m ~ Product r (Orientation p)) =>
X m -> X (Endo m)
xPrdSymEndo (X (Product r (Orientation Symbol))
 -> X (Endo (Product r (Orientation Symbol))))
-> X (Product r (Orientation Symbol))
-> X (Endo (Product r (Orientation Symbol)))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite 'From (Product r (Orientation Symbol))
-> X (Product r (Orientation Symbol))
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
:<=>: XOrt (Product N (Orientation Symbol)) -> 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 = XOrtSite 'From (Product N (Orientation Symbol))
-> XOrt (Product N (Orientation Symbol))
forall q (s :: Site). Oriented q => XOrtSite s q -> XOrt q
xosOrt (XOrtSite 'From (Product N (Orientation Symbol))
 -> XOrt (Product N (Orientation Symbol)))
-> XOrtSite 'From (Product N (Orientation Symbol))
-> XOrt (Product N (Orientation Symbol))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> X N -> XOrtSite 'From (Product N (Orientation Symbol))
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
:<=>: X (Product Z (Orientation Symbol)) -> 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 = XOrtSite 'From (Product Z (Orientation Symbol))
-> X (Product Z (Orientation Symbol))
forall q (s :: Site). Oriented q => XOrtSite s q -> XOrt q
xosOrt (XOrtSite 'From (Product Z (Orientation Symbol))
 -> X (Product Z (Orientation Symbol)))
-> XOrtSite 'From (Product Z (Orientation Symbol))
-> X (Product Z (Orientation Symbol))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> X Z -> XOrtSite 'From (Product Z (Orientation Symbol))
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
:<=>: XMlt (Product N (Orientation Symbol)) -> 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 = N -> X N -> XMlt (Product N (Orientation Symbol))
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
:<=>: XMlt (Product Z (Orientation Symbol)) -> 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 = N -> X Z -> XMlt (Product Z (Orientation Symbol))
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 = X (Point (Orientation Char))
-> (Point (Orientation Char) -> X (Orientation Char))
-> XOrtSite 'From (Orientation Char)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X Char
X (Point (Orientation Char))
xp Char -> X (Orientation Char)
Point (Orientation Char) -> X (Orientation Char)
mxs where
  xp :: X Char
xp  = [(Q, Char)] -> X Char
forall a. [(Q, a)] -> X a
xOneOfW [(Q
10,Char
'a'),(Q
1,Char
'b')]
  mxs :: Char -> X (Orientation Char)
mxs Char
'a' = [(Q, Orientation Char)] -> X (Orientation Char)
forall a. [(Q, a)] -> X a
xOneOfW [(Q
2,(Char
'a'Char -> Char -> Orientation Char
forall p. p -> p -> Orientation p
:>Char
'a')),(Q
1,(Char
'a'Char -> Char -> Orientation Char
forall p. p -> p -> Orientation p
:>Char
'b'))]
  mxs Char
_   = X (Orientation Char)
forall x. X x
XEmpty

-- | its distribution
dstT :: Int -> N -> IO ()
dstT :: Int -> N -> IO ()
dstT Int
n N
d = IO Omega
getOmega IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X String -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n ((Product N (Orientation Char) -> String)
-> X (Product N (Orientation Char)) -> X String
forall a b. (a -> b) -> X a -> X b
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 = Product N (Orientation Char) -> String
forall a. Show a => a -> String
show
  xprd :: X (Product N (Orientation Char))
xprd = XOrtSite 'From (Product N (Orientation Char))
-> Point (Product N (Orientation Char))
-> X (Product N (Orientation Char))
forall q. XOrtSite 'From q -> Point q -> X q
xosStart (XOrtSite 'From (Orientation Char)
-> X N -> N -> XOrtSite 'From (Product N (Orientation Char))
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
Point (Product N (Orientation Char))
'a'
  xn :: X N
xn = N -> N -> X N
xNB N
0 N
10