{-# 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, TransformableMlt, tauMlt

    -- * 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.Kind
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
_ | Bool -> Bool
forall b. Boolean b => b -> b
not (c -> Bool
forall q. Oriented q => q -> Bool
isEndo c
f) = ArithmeticException -> c
forall a e. Exception e => e -> a
throw ArithmeticException
NotExponential
  npower c
f N
n                  = (c -> c -> c) -> c -> [c] -> c
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr c -> c -> c
forall c. Multiplicative c => c -> c -> c
(*) (Point c -> c
forall c. Multiplicative c => Point c -> c
one (c -> Point c
forall q. Oriented q => q -> Point q
start c
f)) ([c] -> c) -> [c] -> c
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> [c] -> [c]
forall a. N -> [a] -> [a]
takeN N
n ([c] -> [c]) -> [c] -> [c]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ c -> [c]
forall a. a -> [a]
repeat (c -> [c]) -> c -> [c]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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
(*) = 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
(*) = 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
(*) = 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
(*) = 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
(*) = 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 = p
Point (Orientation p)
p p -> p -> Orientation p
forall p. p -> p -> Orientation p
:> p
Point (Orientation p)
p
  (p
c :> p
d) * :: Orientation p -> Orientation p -> Orientation p
* (p
a :> p
b) | p
b p -> p -> Bool
forall a. Eq a => a -> a -> Bool
== p
c    = p
a p -> p -> Orientation p
forall p. p -> p -> Orientation p
:> p
d
                      | Bool
otherwise = ArithmeticException -> Orientation p
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
_ | Orientation p -> Bool
forall q. Oriented q => q -> Bool
isEndo Orientation p
o  = Orientation p
o
             | Bool
otherwise = ArithmeticException -> Orientation p
forall a e. Exception e => e -> a
throw ArithmeticException
NotExponential

instance Oriented q => Multiplicative (Path q) where
  one :: Point (Path q) -> Path q
one = Point q -> Path q
Point (Path q) -> Path q
forall q. Point q -> Path q
pthOne
  * :: Path q -> Path q -> Path q
(*) = 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 = c -> Op c
forall x. x -> Op x
Op (c -> Op c) -> (Point c -> c) -> Point c -> Op c
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 c -> c
forall c. Multiplicative c => Point c -> c
one
  Op c
f * :: Op c -> Op c -> Op c
* Op c
g = c -> Op c
forall x. x -> Op x
Op (c
g c -> c -> c
forall c. Multiplicative c => c -> c -> c
* c
f)
  npower :: Op c -> N -> Op c
npower (Op c
f) N
n = c -> Op c
forall x. x -> Op x
Op (c -> N -> c
forall c. Multiplicative c => c -> N -> c
npower c
f N
n)

instance Multiplicative c => Multiplicative (Id c) where
  one :: Point (Id c) -> Id c
one = c -> Id c
forall x. x -> Id x
Id (c -> Id c) -> (Point c -> c) -> Point c -> Id c
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 c -> c
forall c. Multiplicative c => Point c -> c
one
  Id c
f * :: Id c -> Id c -> Id c
* Id c
g = c -> Id c
forall x. x -> Id x
Id (c
f c -> c -> c
forall c. Multiplicative c => c -> c -> c
* c
g)
  npower :: Id c -> N -> Id c
npower (Id c
f) N
n = c -> Id c
forall x. x -> Id x
Id (c -> N -> c
forall c. Multiplicative c => c -> N -> c
npower c
f N
n)


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

-- 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
_ = Point c -> 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 c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== Point c -> c
forall c. Multiplicative c => Point c -> c
one (c -> Point c
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 = Solver c -> c
forall x. Solver x -> x
solve (Solver c -> c) -> (c -> Solver c) -> c -> c
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
. c -> Solver c
forall c. Invertible c => c -> Solver c
tryToInvert

  -- | check for being invertible.

  isInvertible :: c -> Bool
  isInvertible = Solver c -> Bool
forall r. Solver r -> Bool
solvable (Solver c -> Bool) -> (c -> Solver c) -> c -> Bool
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
. c -> Solver c
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 = c -> N -> c
forall c. Multiplicative c => c -> N -> c
npower c
f' (Z -> N
forall a b. Projectible a b => b -> a
prj Z
z) where f' :: c
f' = if Z
z Z -> Z -> Bool
forall a. Ord a => a -> a -> Bool
< Z
0 then c -> c
forall c. Invertible c => c -> c
invert c
f else c
f

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

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

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

instance Invertible Z where
  tryToInvert :: Z -> Solver Z
tryToInvert Z
z = if Z -> Z
forall a. Num a => a -> a
A.abs Z
z Z -> Z -> Bool
forall a. Eq a => a -> a -> Bool
== Z
1 then Z -> Solver Z
forall a. a -> Solver a
forall (m :: * -> *) a. Monad m => a -> m a
return Z
z else ArithmeticException -> Solver Z
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 Q -> Q -> Bool
forall a. Eq a => a -> a -> Bool
== Q
0 then ArithmeticException -> Solver Q
forall e x. Exception e => e -> Solver x
failure ArithmeticException
NotInvertible else Q -> Solver Q
forall a. a -> Solver a
forall (m :: * -> *) a. Monad m => a -> m a
return (Q
1 Q -> Q -> Q
forall a. Fractional a => a -> a -> a
A./ Q
q)

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

instance Invertible c => Invertible (Op c) where
  tryToInvert :: Op c -> Solver (Op c)
tryToInvert (Op c
f) = (c -> Op c) -> Solver c -> Solver (Op c)
forall a b. (a -> b) -> Solver a -> Solver b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> Op c
forall x. x -> Op x
Op (Solver c -> Solver (Op c)) -> Solver c -> Solver (Op c)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ c -> Solver c
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
[Inv c] -> ShowS
Inv c -> String
(Int -> Inv c -> ShowS)
-> (Inv c -> String) -> ([Inv c] -> ShowS) -> Show (Inv c)
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
$cshowsPrec :: forall c. Show c => Int -> Inv c -> ShowS
showsPrec :: Int -> Inv c -> ShowS
$cshow :: forall c. Show c => Inv c -> String
show :: Inv c -> String
$cshowList :: forall c. Show c => [Inv c] -> ShowS
showList :: [Inv c] -> ShowS
Show,Inv c -> Inv c -> Bool
(Inv c -> Inv c -> Bool) -> (Inv c -> Inv c -> Bool) -> Eq (Inv c)
forall c. Eq c => Inv c -> Inv c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: 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 [ (c, c) -> Statement
forall a. Validable a => a -> Statement
valid (c
f,c
f')
        , String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (c -> Orientation (Point c)
forall q. Oriented q => q -> Orientation (Point q)
orientation c
f' Orientation (Point c) -> Orientation (Point c) -> Bool
forall a. Eq a => a -> a -> Bool
== Orientation (Point c) -> Orientation (Point c)
forall p. Orientation p -> Orientation p
opposite (c -> Orientation (Point c)
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' c -> c -> c
forall c. Multiplicative c => c -> c -> c
* c
f c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== Point c -> c
forall c. Multiplicative c => Point c -> c
one (c -> Point c
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 c -> c -> c
forall c. Multiplicative c => c -> c -> c
* c
f' c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== Point c -> c
forall c. Multiplicative c => Point c -> c
one (c -> Point c
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
:=c -> String
forall a. Show a => a -> String
show c
f,String
"f'"String -> String -> Parameter
:=c -> String
forall a. Show a => a -> String
show c
f']

type instance Point (Inv c) = Point c
instance ShowPoint c => ShowPoint (Inv c)
instance EqPoint c => EqPoint (Inv c)
instance ValidablePoint c => ValidablePoint (Inv c)
instance TypeablePoint c => TypeablePoint (Inv c)
instance Multiplicative c => Oriented (Inv c) where
  orientation :: Inv c -> Orientation (Point (Inv c))
orientation (Inv c
f c
_) = c -> Orientation (Point 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 = c -> c -> Inv c
forall c. c -> c -> Inv c
Inv c
o c
o where o :: c
o = Point c -> c
forall c. Multiplicative c => Point c -> c
one Point c
Point (Inv c)
p

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

  npower :: Inv c -> N -> Inv c
npower (Inv c
f c
f') N
n = c -> c -> Inv c
forall c. c -> c -> Inv c
Inv (c -> N -> c
forall c. Multiplicative c => c -> N -> c
npower c
f N
n) (c -> N -> c
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') = Inv c -> Solver (Inv c)
forall a. a -> Solver a
forall (m :: * -> *) a. Monad m => a -> m a
return (c -> c -> Inv c
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') = c -> c -> Inv c
forall c. c -> c -> Inv c
Inv (c -> c
forall x. Transposable x => x -> x
transpose c
f) (c -> c
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 = Struct Typ x
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 = Struct Ent x
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 = Struct Ort x
forall s x. Structure s x => Struct s x
Struct
instance TransformableG Op Mlt Mlt where tauG :: forall x. Struct Mlt x -> Struct Mlt (Op x)
tauG Struct Mlt x
Struct = Struct Mlt (Op x)
forall s x. Structure s x => Struct s x
Struct
instance TransformableG Op (Mlt,t) Mlt where tauG :: forall x. Struct (Mlt, t) x -> Struct Mlt (Op x)
tauG = Struct Mlt x -> Struct Mlt (Op x)
forall x. Struct Mlt x -> Struct Mlt (Op x)
forall (t :: * -> *) u v x.
TransformableG t u v =>
Struct u x -> Struct v (t x)
tauG (Struct Mlt x -> Struct Mlt (Op x))
-> (Struct (Mlt, t) x -> Struct Mlt x)
-> Struct (Mlt, t) x
-> Struct Mlt (Op x)
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
. Struct (Mlt, t) x -> Struct Mlt x
forall s t x. Struct (s, t) x -> Struct s x
tauFst
instance TransformableOp Mlt
instance TransformableGRefl Op Mlt

instance Transformable Mlt Type where tau :: forall x. Struct Mlt x -> Struct (*) x
tau Struct Mlt x
_ = Struct (*) x
forall s x. Structure s x => Struct s x
Struct
instance TransformableType Mlt

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

-- tauMlt -


-- | 'tau' for 'Mlt'.

tauMlt :: Transformable s Mlt => Struct s x -> Struct Mlt x
tauMlt :: forall s x. Transformable s Mlt => Struct s x -> Struct Mlt x
tauMlt = Struct s x -> Struct Mlt x
forall x. Struct s x -> Struct Mlt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau

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

-- TransformableMlt -


-- | helper class to avoid undecidable instances.

class (TransformableOrt s, Transformable s Mlt) => TransformableMlt s

instance TransformableTyp Mlt
instance TransformableOrt Mlt
instance TransformableMlt 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
_) = X (Point c) -> (Point c -> X c) -> XOrtSite 'From c
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point c)
xp (XOrtSite 'From c -> Point c -> X c
forall c. Multiplicative c => XOrtSite 'From c -> Point c -> X c
xq' XOrtSite s c
XOrtSite 'From 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 -> c -> X c
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (c -> X c) -> c -> X c
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Point c -> c
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
_) = Dual (XOrtSite 'To c) -> XOrtSite 'To c
XOrtSite 'From (Op c) -> XOrtSite s c
forall x. Dualisable x => Dual x -> x
fromDual (XOrtSite 'From (Op c) -> XOrtSite s c)
-> XOrtSite 'From (Op c) -> XOrtSite s c
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite 'From (Op c) -> XOrtSite 'From (Op c)
forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> XOrtSite s c
xosAdjOne (XOrtSite 'From (Op c) -> XOrtSite 'From (Op c))
-> XOrtSite 'From (Op c) -> XOrtSite 'From (Op c)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite s c -> Dual (XOrtSite s c)
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 = XOrtSite s c -> N -> Point c -> X (Path c)
forall q (s :: Site).
Oriented q =>
XOrtSite s q -> N -> Point q -> X (Path q)
xosPathMaxAt (XOrtSite s c -> XOrtSite s c
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 = XOrtSite s c -> N -> X (Path c)
forall q (s :: Site). Oriented q => XOrtSite s q -> N -> X (Path q)
xosPathMax (XOrtSite s c -> XOrtSite s c
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 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 ((Path c -> String) -> X (Path c) -> X String
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Path c -> String
forall a. Show a => a -> String
show X (Path c)
xx) where
  xx :: X (Path c)
xx = XOrtSite s c -> X (Point c)
forall (s :: Site) q. XOrtSite s q -> X (Point q)
xosPoint XOrtSite s c
xa X (Point c) -> (Point c -> X (Path c)) -> X (Path c)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= XOrtSite s c -> N -> Point c -> X (Path c)
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 = X (Point (Path c))
-> (Point (Path c) -> X (Path c)) -> XOrtSite 'From (Path c)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point c)
X (Point (Path c))
xp (XOrtSite s c -> N -> Point c -> X (Path c)
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 = X (Point (Path c))
-> (Point (Path c) -> X (Path c)) -> XOrtSite 'To (Path c)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd X (Point c)
X (Point (Path c))
xp (XOrtSite s c -> N -> Point c -> X (Path c)
forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> Point c -> X (Path c)
xosPathAt XOrtSite s c
xe N
n)