{-# LANGUAGE NoImplicitPrelude #-}

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


-- |

-- Module      : OAlg.Structure.Multiplicative.Definition

-- Description : definition of multiplicative structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- multiplicative structures, i.e. structures with a __partially__ defined multiplication @('*')@.

module OAlg.Structure.Multiplicative.Definition
  (
    -- * Multiplicative

    Multiplicative(..), one', isOne, Mlt, ForgetfulMlt

    -- * Transposable

  , TransposableMultiplicative

    -- * Commutative

  , Commutative
  
    -- * Invertible

  , Invertible(..), Inv(..)

    -- * Cayleyan

  , Cayleyan

    -- * X

  , xosPathAt, xosPath, xosXOrtSitePath

  )
  where

import qualified Prelude as A

import Control.Monad
import Control.Exception

import Data.List(repeat)
import Data.Foldable

import OAlg.Control.Solver

import OAlg.Prelude

import OAlg.Data.Canonical

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

--------------------------------------------------------------------------------

-- Multiplicative -


infixl 7 *

-- | 'Oriented' structures with a __partially__ defined __multiplication__ and having

-- 'one' as the __neutral element__ of the multiplication. An entity of a

-- 'Multiplicative' structure will be called a __factor__.

--

-- __Properties__ Let __@c@__ be a type instance of the class 'Multiplicative', then

-- holds:

--

-- (1) #Mlt1#For all @p@ in  @'Point' __c__@ holds: @'orientation' ('one' p) '==' p ':>' p@.

--

-- (2) #Mlt2#For all @f@ and @g@ in __@c@__ holds:

--

--     (1) #Mlt2_1#if @'start' f '==' 'end' g@ then @f '*' g@ is 'valid' and

--     @'start' (f '*' g) '==' 'start' g@ and @'end' (f '*' g) '==' 'end' f@.

--

--     (2) #Mlt2_2#if @'start' f '/=' 'end' g@ then @f '*' g@ is not 'valid' and its

--     evaluation will end up in a 'NotMultiplicable' exception.

--

-- (3) #Mlt3#For all @f@ in __@c@__ holds:

-- @'one' ('end' f) '*' f '==' f@ and @f '*' 'one' ('start' f) '==' f@.

--

-- (4) #Mlt4#For all @f@, @g@ and @h@ in __@c@__ with @'start' g == 'end' h@

-- and @'start' f == 'end' g@ holds: @(f '*' g) '*' h '==' f '*' (g '*' h)@.

--

-- (5) #Mlt5#For all @f@ in __@c@__ holds:

--

--     (1) #Mlt5_1#@'npower' f 1 '==' f@.

--

--     (2) #Mlt5_2#If @f@ is a endo than @'npower' f 0 '==' 'one' ('start' f)@ and

--     For all @n@ in 'N' holds: @'npower' f ('succ' n) '==' f '*' 'npower' f n@.

--

-- Such a __@c@__ will be called a __/multiplicative structure/__ and an entity @f@ of

-- __@c@__ will be called __/factor/__. The associated factor @'one' p@ to a @p@ in

-- @'Point' __c__@ will be called the __/one at/__ @p@.

--

-- __Note__ If the types __@c@__ and @'Point' __c__@ are interpreted as sets

-- __@M@__ and __@O@__ and @'*'@ as a partially defined function from __@M x M -> M@__ then

-- this forms a __/small category/__ with objects in __@O@__ and morphisms in __@M@__.

class Oriented c => Multiplicative c where
  {-# MINIMAL one,(*) #-}

  -- | the neutral element associated to each point. If there is no ambiguity

  --   for @'one' p@ we will briefly denote it by @1 r@ or just @1@.

  one :: Point c -> c

  -- | the multiplication of two factors.

  (*) :: c -> c -> c
  
  -- | @n@ times the multiplication of a given factor @f@.

  npower :: c -> N -> c
  npower c
f N
1                  = c
f
  npower c
f N
_ | forall b. Boolean b => b -> b
not (forall q. Oriented q => q -> Bool
isEndo c
f) = forall a e. Exception e => e -> a
throw ArithmeticException
NotExponential
  npower c
f N
n                  = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr 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 (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. N -> [a] -> [a]
takeN N
n forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. a -> [a]
repeat forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ c
f

--------------------------------------------------------------------------------

-- Multiplicative - Instance -


instance Multiplicative () where
  one :: Point () -> ()
one Point ()
_ = ()
  ()
_ * :: () -> () -> ()
* ()
_ = () 
  npower :: () -> N -> ()
npower ()
_ N
_ = ()
  
instance Multiplicative Int where
  one :: Point Int -> Int
one Point Int
_ = Int
1
  * :: Int -> Int -> Int
(*) = forall a. Num a => a -> a -> a
(A.*)

instance Multiplicative Integer where
  one :: Point Integer -> Integer
one Point Integer
_ = Integer
1
  * :: Integer -> Integer -> Integer
(*) = forall a. Num a => a -> a -> a
(A.*)

instance Multiplicative N where
  one :: Point N -> N
one Point N
_ = N
1
  * :: N -> N -> N
(*) = forall a. Num a => a -> a -> a
(A.*)

instance Multiplicative Z where
  one :: Point Z -> Z
one Point Z
_ = Z
1
  * :: Z -> Z -> Z
(*) = forall a. Num a => a -> a -> a
(A.*)

instance Multiplicative Q where
  one :: Point Q -> Q
one Point Q
_ = Q
1
  * :: Q -> Q -> Q
(*) = forall a. Num a => a -> a -> a
(A.*)

instance Entity p => Multiplicative (Orientation p) where
  one :: Point (Orientation p) -> Orientation p
one Point (Orientation p)
p = Point (Orientation p)
p forall p. p -> p -> Orientation p
:> Point (Orientation p)
p
  (p
c :> p
d) * :: Orientation p -> Orientation p -> Orientation p
* (p
a :> p
b) | p
b forall a. Eq a => a -> a -> Bool
== p
c    = p
a forall p. p -> p -> Orientation p
:> p
d
                      | Bool
otherwise = forall a e. Exception e => e -> a
throw ArithmeticException
NotMultiplicable

  npower :: Orientation p -> N -> Orientation p
npower Orientation p
o N
1             = Orientation p
o
  npower Orientation p
o N
_ | forall q. Oriented q => q -> Bool
isEndo Orientation p
o  = Orientation p
o
             | Bool
otherwise = forall a e. Exception e => e -> a
throw ArithmeticException
NotExponential

instance Oriented q => Multiplicative (Path q) where
  one :: Point (Path q) -> Path q
one = forall q. Point q -> Path q
pthOne
  * :: Path q -> Path q -> Path q
(*) = forall q. Oriented q => Path q -> Path q -> Path q
pthMlt

instance Multiplicative c => Multiplicative (Op c) where
  one :: Point (Op c) -> Op c
one = forall x. x -> Op x
Op forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall c. Multiplicative c => Point c -> c
one
  Op c
f * :: Op c -> Op c -> Op c
* Op c
g = forall x. x -> Op x
Op (c
g forall c. Multiplicative c => c -> c -> c
* c
f)
  npower :: Op c -> N -> Op c
npower (Op c
f) N
n = forall x. x -> Op x
Op (forall c. Multiplicative c => c -> N -> c
npower c
f N
n)

instance Multiplicative c => Projectible c (Path c) where
  prj :: Path c -> c
prj Path c
pth = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall c. Multiplicative c => c -> c -> c
(*) (forall c. Multiplicative c => Point c -> c
one (forall q. Oriented q => q -> Point q
start Path c
pth)) Path c
pth
    
--------------------------------------------------------------------------------

-- one' -


-- | the 'one' to a given point. The type @p c@ serves only as proxy and 'one'' is

-- lazy in it.

--

-- __Note__ As 'Point' may be a non-injective type family,

-- the type checker needs some times a little bit more information

-- to pic the right 'one'.

one' :: Multiplicative c => p c -> Point c -> c
one' :: forall c (p :: * -> *). Multiplicative c => p c -> Point c -> c
one' p c
_ = forall c. Multiplicative c => Point c -> c
one

--------------------------------------------------------------------------------

-- isOne -


-- | check for being equal to 'one'.

isOne :: Multiplicative c => c -> Bool
isOne :: forall c. Multiplicative c => c -> Bool
isOne c
f = c
f forall a. Eq a => a -> a -> Bool
== forall c. Multiplicative c => Point c -> c
one (forall q. Oriented q => q -> Point q
end c
f)

--------------------------------------------------------------------------------

-- Transposable -


-- | transposable 'Multiplicative' structures.

--

-- __Property__ Let __@c@__ be a 'TransposableMultiplicative' structure, then holds:

--

-- (1) For all @p@ in @'Point' __c__@ holds: @'transpose' ('one' p) = 'one' p@.

--

-- (2) For all @f@, @g@ in __@c@__ with @'start' f '==' 'end' g@ holds:

-- @'transpose' (f '*' g) '==' 'transpose' g '*' 'transpose' f@.

class (TransposableOriented c, Multiplicative c) => TransposableMultiplicative c

instance Entity p => TransposableMultiplicative (Orientation p)
instance TransposableMultiplicative N
instance TransposableMultiplicative Z
instance TransposableMultiplicative Q

--------------------------------------------------------------------------------

-- Commutative -


-- | commutative multiplicative structures.

--

-- __Property__ Let @__c__@ be a 'Commutative' structure, then holds: For all @f@ and @g@ in @__c__@

-- with @'start' f '==' 'end' f@, @'start' g '==' 'end' g@ and @'start' f '==' 'end' g@ holds:

-- @f '*' g '==' g '*' f@.

class Multiplicative c => Commutative c

instance Commutative ()
instance Commutative Int
instance Commutative Integer
instance Commutative N
instance Commutative Z
instance Commutative Q
instance Commutative c => Commutative (Op c)

----------------------------------------

-- Invertible - 


-- | multiplicative structures having a __/multiplicative inverse/__.

--

-- __Definition__ Let @f@ and @g@ be two factors in a 'Multiplicative' structure @___c__@

-- then we call @g@ a __/multiplicative inverse/__ to @f@ (or short inverse) if and

-- only if the following hold:

--

-- (1) @'start' g == 'end' f@ and @'end' g == 'start' f@.

--

-- (2) @f '*' g = 'one' ('end' f)@ and @g '*' f == 'one' ('start' f)@.

--

-- __Properties__ For all @f@ in a 'Invertible' structure @__c__@ holds:

--

-- (1) @'isInvertible' f@ is equivalent to @'solvable' ('tryToInvert' f)@.

--

-- (2) if @'isInvertible' f@ holds, then @'invert' f@ is 'valid' and it is the multiplicative

-- inverse of @f@. Furthermore @'invert' f '==' 'solve' ('tryToInvert' m)@.

--

-- (3) if 'not' @'isInvertible' f@ holds, then @'invert' f@ is not 'valid' and evaluating

-- it will end up in a 'NotInvertible'-exception.

--

--  __Note__

--

-- (1) It is not required that every factor has a multiplicative inverse (see 'Cayleyan'

-- for such structures).

--

-- (2) This structure is intended for multiplicative structures having a

-- known algorithm to evaluate for every invertible @f@ its inverse.

class Multiplicative c => Invertible c where
  {-# MINIMAL tryToInvert #-}
  
  -- | solver to evaluate the multiplicative inverse - if it exists.

  tryToInvert :: c -> Solver c

  -- | the inverse.

  invert :: c -> c
  invert = forall x. Solver x -> x
solve forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall c. Invertible c => c -> Solver c
tryToInvert

  -- | check for being invertible.

  isInvertible :: c -> Bool
  isInvertible = forall r. Solver r -> Bool
solvable forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall c. Invertible c => c -> Solver c
tryToInvert

  -- | if @0 '<=' z@ then @n@ times the multiplication for the given factor else @'prj' z@ times the

  -- multiplication of the inverse of the given factor.

  zpower :: c -> Z -> c
  zpower c
f Z
z = forall c. Multiplicative c => c -> N -> c
npower c
f' (forall a b. Projectible a b => b -> a
prj Z
z) where f' :: c
f' = if Z
z forall a. Ord a => a -> a -> Bool
< Z
0 then forall c. Invertible c => c -> c
invert c
f else c
f

instance Invertible () where
  tryToInvert :: () -> Solver ()
tryToInvert ()
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance Invertible Int where
  tryToInvert :: Int -> Solver Int
tryToInvert Int
n = if forall a. Num a => a -> a
A.abs Int
n forall a. Eq a => a -> a -> Bool
== Int
1 then forall (m :: * -> *) a. Monad m => a -> m a
return Int
n else forall e x. Exception e => e -> Solver x
failure ArithmeticException
NotInvertible

instance Invertible Integer where
  tryToInvert :: Integer -> Solver Integer
tryToInvert Integer
z = if forall a. Num a => a -> a
A.abs Integer
z forall a. Eq a => a -> a -> Bool
== Integer
1 then forall (m :: * -> *) a. Monad m => a -> m a
return Integer
z else forall e x. Exception e => e -> Solver x
failure ArithmeticException
NotInvertible

instance Invertible N where
  tryToInvert :: N -> Solver N
tryToInvert N
n = if N
n forall a. Eq a => a -> a -> Bool
== N
1 then forall (m :: * -> *) a. Monad m => a -> m a
return N
1 else forall e x. Exception e => e -> Solver x
failure ArithmeticException
NotInvertible

instance Invertible Z where
  tryToInvert :: Z -> Solver Z
tryToInvert Z
z = if forall a. Num a => a -> a
A.abs Z
z forall a. Eq a => a -> a -> Bool
== Z
1 then forall (m :: * -> *) a. Monad m => a -> m a
return Z
z else forall e x. Exception e => e -> Solver x
failure ArithmeticException
NotInvertible

instance Invertible Q where
  tryToInvert :: Q -> Solver Q
tryToInvert Q
q = if Q
q forall a. Eq a => a -> a -> Bool
== Q
0 then forall e x. Exception e => e -> Solver x
failure ArithmeticException
NotInvertible else forall (m :: * -> *) a. Monad m => a -> m a
return (Q
1 forall a. Fractional a => a -> a -> a
A./ Q
q)

instance Entity p => Invertible (Orientation p) where
  tryToInvert :: Orientation p -> Solver (Orientation p)
tryToInvert = 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
. forall x. Transposable x => x -> x
transpose

instance Invertible c => Invertible (Op c) where
  tryToInvert :: Op c -> Solver (Op c)
tryToInvert (Op c
f) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. x -> Op x
Op forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall c. Invertible c => c -> Solver c
tryToInvert c
f

--------------------------------------------------------------------------------

-- Cayleyan -


-- | 'Invertible' structures where every element is invertible.

--

-- __Property__ Let @__c__@ be a 'Cayleyan' structure, then holds: For all

-- @f@ in @__c__@ holds: @'isInvertible' f '==' 'True'@.

--

-- __Note__

--

-- (1) If the type @'Point' __c__@ is singleton, then the mathematical interpretation of @__c__@

-- is a __group__.

--

-- (2) The name of this structures is given by /Arthur Cayley/ who introduced the concept

-- (and the name) of an abstract group in 1854

-- (<https://en.wikipedia.org/wiki/Arthur_Cayley>).

--

-- (3) Usually in mathematics such a structure is called a __/groupoid/__.

class Invertible c => Cayleyan c

instance Cayleyan ()
instance Entity p => Cayleyan (Orientation p)
instance Cayleyan c => Cayleyan (Op c)

--------------------------------------------------------------------------------

-- Inv -


-- | invertible factors within a 'Multiplicative' structures @__c__@, which forms a /sub/

-- 'Multiplicative' structure on @__c__@, given by the canonical inclusion 'inj' which is

-- given by @\\'Inv' f _ -> f@.

--

-- __Property__ Let @'Inv' f f'@ be in @'Inv' __c__@ where @__c__@ is a 'Multiplicative'

-- structure, then holds:

--

-- (1) @'orientation' f' '==' 'opposite' ('orientation' f)@.

--

-- (2) @f' '*' f '==' 'one' ('start' f)@.

--

-- (3) @f '*' f' '==' 'one' ('end' f)@.

--

-- __Note__ The canonical inclusion is obviously not injective on the /set/ of all values

-- of type @'Inv' __c__@ to @__c__@. But restricted to the 'valid' ones it is injective,

-- because the inverses of a @f@ in @__c__@ are uniquely determined by @f@.

data Inv c = Inv c c deriving (Int -> Inv c -> ShowS
forall c. Show c => Int -> Inv c -> ShowS
forall c. Show c => [Inv c] -> ShowS
forall c. Show c => Inv c -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Inv c] -> ShowS
$cshowList :: forall c. Show c => [Inv c] -> ShowS
show :: Inv c -> String
$cshow :: forall c. Show c => Inv c -> String
showsPrec :: Int -> Inv c -> ShowS
$cshowsPrec :: forall c. Show c => Int -> Inv c -> ShowS
Show,Inv c -> Inv c -> Bool
forall c. Eq c => Inv c -> Inv c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Inv c -> Inv c -> Bool
$c/= :: forall c. Eq c => Inv c -> Inv c -> Bool
== :: Inv c -> Inv c -> Bool
$c== :: forall c. Eq c => Inv c -> Inv c -> Bool
Eq)

instance Embeddable (Inv c) c where
  inj :: Inv c -> c
inj (Inv c
f c
_) = c
f

instance Multiplicative c => Validable (Inv c) where
  valid :: Inv c -> Statement
valid (Inv c
f c
f') = String -> Label
Label String
"Inv" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid (c
f,c
f')
        , String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation c
f' forall a. Eq a => a -> a -> Bool
== forall p. Orientation p -> Orientation p
opposite (forall q. Oriented q => q -> Orientation (Point q)
orientation c
f))Bool -> Message -> Statement
:?>Message
prms
        , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (c
f' forall c. Multiplicative c => c -> c -> c
* c
f 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
:?>Message
prms
        , String -> Label
Label String
"3" Label -> Statement -> Statement
:<=>: (c
f forall c. Multiplicative c => c -> c -> c
* c
f' forall a. Eq a => a -> a -> Bool
== forall c. Multiplicative c => Point c -> c
one (forall q. Oriented q => q -> Point q
end c
f))Bool -> Message -> Statement
:?>Message
prms
        ]
    where prms :: Message
prms = [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall a. Show a => a -> String
show c
f,String
"f'"String -> String -> Parameter
:=forall a. Show a => a -> String
show c
f']

instance Multiplicative c => Entity (Inv c)

instance Multiplicative c => Oriented (Inv c) where
  type Point (Inv c) = Point c
  orientation :: Inv c -> Orientation (Point (Inv c))
orientation (Inv c
f c
_) = forall q. Oriented q => q -> Orientation (Point q)
orientation c
f

instance Multiplicative c => Multiplicative (Inv c) where
  one :: Point (Inv c) -> Inv c
one Point (Inv c)
p = forall c. c -> c -> Inv c
Inv c
o c
o where o :: c
o = forall c. Multiplicative c => Point c -> c
one Point (Inv c)
p

  Inv c
f c
f' * :: Inv c -> Inv c -> Inv c
* Inv c
g c
g'
    | forall q. Oriented q => q -> Point q
end c
g forall a. Eq a => a -> a -> Bool
== forall q. Oriented q => q -> Point q
start c
f = forall c. c -> c -> Inv c
Inv (c
fforall c. Multiplicative c => c -> c -> c
*c
g) (c
g'forall c. Multiplicative c => c -> c -> c
*c
f')
    | Bool
otherwise        = forall a e. Exception e => e -> a
throw ArithmeticException
NotMultiplicable

  npower :: Inv c -> N -> Inv c
npower (Inv c
f c
f') N
n = forall c. c -> c -> Inv c
Inv (forall c. Multiplicative c => c -> N -> c
npower c
f N
n) (forall c. Multiplicative c => c -> N -> c
npower c
f' N
n)

instance Multiplicative c => Invertible (Inv c) where
  tryToInvert :: Inv c -> Solver (Inv c)
tryToInvert (Inv c
f c
f') = forall (m :: * -> *) a. Monad m => a -> m a
return (forall c. c -> c -> Inv c
Inv c
f' c
f)

instance Multiplicative c => Cayleyan (Inv c)

instance TransposableMultiplicative c => Transposable (Inv c) where
  transpose :: Inv c -> Inv c
transpose (Inv c
f c
f') = forall c. c -> c -> Inv c
Inv (forall x. Transposable x => x -> x
transpose c
f) (forall x. Transposable x => x -> x
transpose c
f')

instance TransposableMultiplicative c => TransposableOriented (Inv c)
instance TransposableMultiplicative c => TransposableMultiplicative (Inv c)

--------------------------------------------------------------------------------

-- Mlt -

  
-- | type representing the class of 'Multiplicative' structures.

data Mlt

type instance Structure Mlt x = Multiplicative x

instance Transformable Mlt Typ where tau :: forall x. Struct Mlt x -> Struct Typ x
tau Struct Mlt x
Struct = forall s x. Structure s x => Struct s x
Struct
instance Transformable Mlt Ent where tau :: forall x. Struct Mlt x -> Struct Ent x
tau Struct Mlt x
Struct = forall s x. Structure s x => Struct s x
Struct
instance Transformable Mlt Ort where tau :: forall x. Struct Mlt x -> Struct Ort x
tau Struct Mlt x
Struct = forall s x. Structure s x => Struct s x
Struct
instance Transformable1 Op Mlt where tau1 :: forall x. Struct Mlt x -> Struct Mlt (Op x)
tau1 Struct Mlt x
Struct = forall s x. Structure s x => Struct s x
Struct
instance TransformableOp Mlt

--------------------------------------------------------------------------------

-- ForgetfulMlt -


-- | transformable to 'Multiplicative' structure.

class (ForgetfulOrt s, Transformable s Mlt) => ForgetfulMlt s

instance ForgetfulTyp Mlt
instance ForgetfulOrt Mlt
instance ForgetfulMlt Mlt


--------------------------------------------------------------------------------

-- xosAdjOne -


-- | adjoining a 'one' for empty random variable.

xosAdjOne :: Multiplicative c => XOrtSite s c -> XOrtSite s c
xosAdjOne :: forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> XOrtSite s c
xosAdjOne xs :: XOrtSite s c
xs@(XStart X (Point c)
xp Point c -> X c
_) = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point c)
xp (forall c. Multiplicative c => XOrtSite 'From c -> Point c -> X c
xq' XOrtSite s c
xs) where
  xq' :: Multiplicative c => XOrtSite From c -> Point c -> X c
  xq' :: forall c. Multiplicative c => XOrtSite 'From c -> Point c -> X c
xq' (XStart X (Point c)
_ Point c -> X c
xc) Point c
p = case Point c -> X c
xc Point c
p of
    X c
XEmpty -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall c. Multiplicative c => Point c -> c
one Point c
p
    X c
xf     -> X c
xf
xosAdjOne xe :: XOrtSite s c
xe@(XEnd X (Point c)
_ Point c -> X c
_) = forall x. Dualisable x => Dual x -> x
fromDual forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> XOrtSite s c
xosAdjOne forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Dualisable x => x -> Dual x
toDual XOrtSite s c
xe

--------------------------------------------------------------------------------

-- xosPathAt -


-- | random variable of paths at the given point and the given length (see 'xosPathMaxAt' and as

-- @__c__@ is 'Multiplicative', the underlying random variable for factors for a given point is

-- not empty).

xosPathAt :: Multiplicative c => XOrtSite s c -> N -> Point c -> X (Path c)
xosPathAt :: forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> Point c -> X (Path c)
xosPathAt XOrtSite s c
xa = forall q (s :: Site).
Oriented q =>
XOrtSite s q -> N -> Point q -> X (Path q)
xosPathMaxAt (forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> XOrtSite s c
xosAdjOne XOrtSite s c
xa)

--------------------------------------------------------------------------------

-- xosPath -


-- | random variable of paths with the given length.

xosPath :: Multiplicative c => XOrtSite s c -> N -> X (Path c)
xosPath :: forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> X (Path c)
xosPath XOrtSite s c
xa = forall q (s :: Site). Oriented q => XOrtSite s q -> N -> X (Path q)
xosPathMax (forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> XOrtSite s c
xosAdjOne XOrtSite s c
xa)

--------------------------------------------------------------------------------

-- dstPathDrcn -


-- | puts the distribution.

dstPathDrcn :: Multiplicative c => Int -> N -> XOrtSite s c -> IO ()
dstPathDrcn :: forall c (s :: Site).
Multiplicative c =>
Int -> N -> XOrtSite s c -> IO ()
dstPathDrcn Int
n N
l XOrtSite s c
xa = 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. Show a => a -> String
show X (Path c)
xx) where
  xx :: X (Path c)
xx = forall (s :: Site) q. XOrtSite s q -> X (Point q)
xosPoint XOrtSite s c
xa forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> Point c -> X (Path c)
xosPathAt XOrtSite s c
xa N
l

--------------------------------------------------------------------------------

-- xosXOrtSitePath -


-- | the induced random variable for paths.

xosXOrtSitePath :: Multiplicative c
  => XOrtSite s c -> N -> XOrtSite s (Path c)
xosXOrtSitePath :: forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> XOrtSite s (Path c)
xosXOrtSitePath xs :: XOrtSite s c
xs@(XStart X (Point c)
xp Point c -> X c
_) N
n = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point c)
xp (forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> Point c -> X (Path c)
xosPathAt XOrtSite s c
xs N
n)
xosXOrtSitePath xe :: XOrtSite s c
xe@(XEnd X (Point c)
xp Point c -> X c
_) N
n = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd X (Point c)
xp (forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> Point c -> X (Path c)
xosPathAt XOrtSite s c
xe N
n)