{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Structure.Oriented.Proposition

-- Description : propositions on multiplicative structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- Propositions on 'Multiplicative' structures.

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

    prpMlt, XMlt(..)
  , Endo(..), Mltp2(..), Mltp3(..)
  , prpMlt1, prpMlt2, prpMlt2_1, prpMlt2_2, prpMlt3, prpMlt4, prpMlt5

    -- * Duality

  , coXMlt

    -- * X

  , MltX
  , XStandardMlt(..)
  , xMlt, xMltp2, xMltp3
  , xoMlt
  
    -- * Oriented Direction

  -- , xodMlt, xodEndo, xodMltp2, xodMltp3

  
    -- ** Total

  , xMltTtl

    -- ** Orientation

  , xMltOrnt
  
  )
  where

import Control.Monad
import Control.Applicative

import Data.Kind

import OAlg.Prelude

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

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

import OAlg.Structure.Multiplicative.Definition

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

-- Endo -


-- | predicate for endos.

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

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

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

-- fromEndo -


-- | deconstruction of a 'Endo'.

fromEndo :: Endo q -> q
fromEndo :: forall q. Endo q -> q
fromEndo (Endo q
f) = q
f

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

-- Mltp2 -


-- | predicate for two multiplicable factors.

data Mltp2 c = Mltp2 c c deriving (Int -> Mltp2 c -> ShowS
[Mltp2 c] -> ShowS
Mltp2 c -> String
(Int -> Mltp2 c -> ShowS)
-> (Mltp2 c -> String) -> ([Mltp2 c] -> ShowS) -> Show (Mltp2 c)
forall c. Show c => Int -> Mltp2 c -> ShowS
forall c. Show c => [Mltp2 c] -> ShowS
forall c. Show c => Mltp2 c -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall c. Show c => Int -> Mltp2 c -> ShowS
showsPrec :: Int -> Mltp2 c -> ShowS
$cshow :: forall c. Show c => Mltp2 c -> String
show :: Mltp2 c -> String
$cshowList :: forall c. Show c => [Mltp2 c] -> ShowS
showList :: [Mltp2 c] -> ShowS
Show,Mltp2 c -> Mltp2 c -> Bool
(Mltp2 c -> Mltp2 c -> Bool)
-> (Mltp2 c -> Mltp2 c -> Bool) -> Eq (Mltp2 c)
forall c. Eq c => Mltp2 c -> Mltp2 c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall c. Eq c => Mltp2 c -> Mltp2 c -> Bool
== :: Mltp2 c -> Mltp2 c -> Bool
$c/= :: forall c. Eq c => Mltp2 c -> Mltp2 c -> Bool
/= :: Mltp2 c -> Mltp2 c -> Bool
Eq,Eq (Mltp2 c)
Eq (Mltp2 c) =>
(Mltp2 c -> Mltp2 c -> Ordering)
-> (Mltp2 c -> Mltp2 c -> Bool)
-> (Mltp2 c -> Mltp2 c -> Bool)
-> (Mltp2 c -> Mltp2 c -> Bool)
-> (Mltp2 c -> Mltp2 c -> Bool)
-> (Mltp2 c -> Mltp2 c -> Mltp2 c)
-> (Mltp2 c -> Mltp2 c -> Mltp2 c)
-> Ord (Mltp2 c)
Mltp2 c -> Mltp2 c -> Bool
Mltp2 c -> Mltp2 c -> Ordering
Mltp2 c -> Mltp2 c -> Mltp2 c
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall c. Ord c => Eq (Mltp2 c)
forall c. Ord c => Mltp2 c -> Mltp2 c -> Bool
forall c. Ord c => Mltp2 c -> Mltp2 c -> Ordering
forall c. Ord c => Mltp2 c -> Mltp2 c -> Mltp2 c
$ccompare :: forall c. Ord c => Mltp2 c -> Mltp2 c -> Ordering
compare :: Mltp2 c -> Mltp2 c -> Ordering
$c< :: forall c. Ord c => Mltp2 c -> Mltp2 c -> Bool
< :: Mltp2 c -> Mltp2 c -> Bool
$c<= :: forall c. Ord c => Mltp2 c -> Mltp2 c -> Bool
<= :: Mltp2 c -> Mltp2 c -> Bool
$c> :: forall c. Ord c => Mltp2 c -> Mltp2 c -> Bool
> :: Mltp2 c -> Mltp2 c -> Bool
$c>= :: forall c. Ord c => Mltp2 c -> Mltp2 c -> Bool
>= :: Mltp2 c -> Mltp2 c -> Bool
$cmax :: forall c. Ord c => Mltp2 c -> Mltp2 c -> Mltp2 c
max :: Mltp2 c -> Mltp2 c -> Mltp2 c
$cmin :: forall c. Ord c => Mltp2 c -> Mltp2 c -> Mltp2 c
min :: Mltp2 c -> Mltp2 c -> Mltp2 c
Ord)

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

instance Oriented c => Validable (Mltp2 c) where
  valid :: Mltp2 c -> Statement
valid = Path c -> Statement
forall a. Validable a => a -> Statement
valid (Path c -> Statement)
-> (Mltp2 c -> Path c) -> Mltp2 c -> Statement
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
. Mltp2 c -> Path c
forall c. Oriented c => Mltp2 c -> Path c
pthMltp2

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

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

-- Mltp3 -


-- | predicate for three multiplicable factors.

data Mltp3 c = Mltp3 c c c deriving (Int -> Mltp3 c -> ShowS
[Mltp3 c] -> ShowS
Mltp3 c -> String
(Int -> Mltp3 c -> ShowS)
-> (Mltp3 c -> String) -> ([Mltp3 c] -> ShowS) -> Show (Mltp3 c)
forall c. Show c => Int -> Mltp3 c -> ShowS
forall c. Show c => [Mltp3 c] -> ShowS
forall c. Show c => Mltp3 c -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall c. Show c => Int -> Mltp3 c -> ShowS
showsPrec :: Int -> Mltp3 c -> ShowS
$cshow :: forall c. Show c => Mltp3 c -> String
show :: Mltp3 c -> String
$cshowList :: forall c. Show c => [Mltp3 c] -> ShowS
showList :: [Mltp3 c] -> ShowS
Show,Mltp3 c -> Mltp3 c -> Bool
(Mltp3 c -> Mltp3 c -> Bool)
-> (Mltp3 c -> Mltp3 c -> Bool) -> Eq (Mltp3 c)
forall c. Eq c => Mltp3 c -> Mltp3 c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall c. Eq c => Mltp3 c -> Mltp3 c -> Bool
== :: Mltp3 c -> Mltp3 c -> Bool
$c/= :: forall c. Eq c => Mltp3 c -> Mltp3 c -> Bool
/= :: Mltp3 c -> Mltp3 c -> Bool
Eq,Eq (Mltp3 c)
Eq (Mltp3 c) =>
(Mltp3 c -> Mltp3 c -> Ordering)
-> (Mltp3 c -> Mltp3 c -> Bool)
-> (Mltp3 c -> Mltp3 c -> Bool)
-> (Mltp3 c -> Mltp3 c -> Bool)
-> (Mltp3 c -> Mltp3 c -> Bool)
-> (Mltp3 c -> Mltp3 c -> Mltp3 c)
-> (Mltp3 c -> Mltp3 c -> Mltp3 c)
-> Ord (Mltp3 c)
Mltp3 c -> Mltp3 c -> Bool
Mltp3 c -> Mltp3 c -> Ordering
Mltp3 c -> Mltp3 c -> Mltp3 c
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall c. Ord c => Eq (Mltp3 c)
forall c. Ord c => Mltp3 c -> Mltp3 c -> Bool
forall c. Ord c => Mltp3 c -> Mltp3 c -> Ordering
forall c. Ord c => Mltp3 c -> Mltp3 c -> Mltp3 c
$ccompare :: forall c. Ord c => Mltp3 c -> Mltp3 c -> Ordering
compare :: Mltp3 c -> Mltp3 c -> Ordering
$c< :: forall c. Ord c => Mltp3 c -> Mltp3 c -> Bool
< :: Mltp3 c -> Mltp3 c -> Bool
$c<= :: forall c. Ord c => Mltp3 c -> Mltp3 c -> Bool
<= :: Mltp3 c -> Mltp3 c -> Bool
$c> :: forall c. Ord c => Mltp3 c -> Mltp3 c -> Bool
> :: Mltp3 c -> Mltp3 c -> Bool
$c>= :: forall c. Ord c => Mltp3 c -> Mltp3 c -> Bool
>= :: Mltp3 c -> Mltp3 c -> Bool
$cmax :: forall c. Ord c => Mltp3 c -> Mltp3 c -> Mltp3 c
max :: Mltp3 c -> Mltp3 c -> Mltp3 c
$cmin :: forall c. Ord c => Mltp3 c -> Mltp3 c -> Mltp3 c
min :: Mltp3 c -> Mltp3 c -> Mltp3 c
Ord)

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

instance Oriented c => Validable (Mltp3 c) where
  valid :: Mltp3 c -> Statement
valid = Path c -> Statement
forall a. Validable a => a -> Statement
valid (Path c -> Statement)
-> (Mltp3 c -> Path c) -> Mltp3 c -> Statement
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
. Mltp3 c -> Path c
forall c. Oriented c => Mltp3 c -> Path c
pthMltp3
  
type instance Dual (Mltp3 c) = Mltp3 (Op c)

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


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

-- prpMlt1 -


-- | validity of 'one' according to "OAlg.Structure.Multiplicative.Definition#Mlt1".

prpMlt1 :: Multiplicative c => p c -> X (Point c) -> Statement
prpMlt1 :: forall c (p :: * -> *).
Multiplicative c =>
p c -> X (Point c) -> Statement
prpMlt1 p c
s X (Point c)
xp = String -> Label
Prp String
"Mlt1"
  Label -> Statement -> Statement
:<=>: X (Point c) -> (Point c -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Point c)
xp (\Point c
p -> (c -> Orientation (Point c)
forall q. Oriented q => q -> Orientation (Point q)
orientation (p c -> Point c -> c
forall c (p :: * -> *). Multiplicative c => p c -> Point c -> c
one' p c
s Point c
p) Orientation (Point c) -> Orientation (Point c) -> Bool
forall a. Eq a => a -> a -> Bool
== Point c
p Point c -> Point c -> Orientation (Point c)
forall p. p -> p -> Orientation p
:> Point c
p) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"p" String -> String -> Parameter
:= Point c -> String
forall a. Show a => a -> String
show Point c
p])

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

-- prpMlt2_1 -


-- | validity of '*' for two multiplicable factors according to

--   "OAlg.Structure.Multiplicative.Definition#Mlt2_1".

prpMlt2_1 :: Multiplicative c => Mltp2 c -> Statement
prpMlt2_1 :: forall c. Multiplicative c => Mltp2 c -> Statement
prpMlt2_1 m :: Mltp2 c
m@(Mltp2 c
f c
g) = String -> Label
Prp String
"Mlt2_1"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ c -> Statement
forall a. Validable a => a -> Statement
valid c
fg
            , String -> Label
Label String
"start" Label -> Statement -> Statement
:<=>: (c -> Point c
forall q. Oriented q => q -> Point q
start c
fg Point c -> Point c -> Bool
forall a. Eq a => a -> a -> Bool
== c -> Point c
forall q. Oriented q => q -> Point q
start c
g) Bool -> Message -> Statement
:?> Message
prms
            , String -> Label
Label String
"end" Label -> Statement -> Statement
:<=>: (c -> Point c
forall q. Oriented q => q -> Point q
end c
fg Point c -> Point c -> Bool
forall a. Eq a => a -> a -> Bool
== c -> Point c
forall q. Oriented q => q -> Point q
end c
f) Bool -> Message -> Statement
:?> Message
prms
            ]
  where fg :: c
fg = c
fc -> c -> c
forall c. Multiplicative c => c -> c -> c
*c
g
        prms :: Message
prms = [Parameter] -> Message
Params [String
"m"String -> String -> Parameter
:=Mltp2 c -> String
forall a. Show a => a -> String
show Mltp2 c
m]

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

-- prpMlt2_2 -


-- | validity of '*' for two not multiplicable factors according to

--   "OAlg.Structure.Multiplicative.Definition#Mlt2_2".

prpMlt2_2 :: Multiplicative c => c -> c -> Statement
prpMlt2_2 :: forall c. Multiplicative c => c -> c -> Statement
prpMlt2_2 c
f c
g = String -> Label
Prp String
"Mlt2_2"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ Statement -> Statement
Not Statement
vfg Statement -> (SomeException -> Statement) -> Statement
forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` Statement -> SomeException -> Statement
someException Statement
SValid 
            , Statement
vfg Statement -> (ArithmeticException -> Statement) -> Statement
forall e. Exception e => Statement -> (e -> Statement) -> Statement
`Catch` ArithmeticException -> Statement
nmp
            ]
  where vfg :: Statement
vfg = c -> Statement
forall a. Validable a => a -> Statement
valid (c
fc -> c -> c
forall c. Multiplicative c => c -> c -> c
*c
g)
        nmp :: ArithmeticException -> Statement
nmp ArithmeticException
NotMultiplicable = Statement
SValid
        nmp ArithmeticException
_                = Statement
SInvalid
        
--------------------------------------------------------------------------------

-- prpMlt2 -


-- | validity of '*' according to "OAlg.Structure.Multiplicative.Definition#Mlt2".

prpMlt2 :: Multiplicative c => X (c,c) -> Statement
prpMlt2 :: forall c. Multiplicative c => X (c, c) -> Statement
prpMlt2 X (c, c)
xfg = String -> Label
Prp String
"Mlt2"
  Label -> Statement -> Statement
:<=>:  X (c, c) -> ((c, c) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (c, c)
xfg (\(c
f,c
g)
                     -> let fg :: Mltp2 c
fg = c -> c -> Mltp2 c
forall c. c -> c -> Mltp2 c
Mltp2 c
f c
g
                         in [Statement] -> Statement
And [ Mltp2 c -> Statement
forall a. Validable a => a -> Statement
valid Mltp2 c
fg       Statement -> Statement -> Statement
|~> Mltp2 c -> Statement
forall c. Multiplicative c => Mltp2 c -> Statement
prpMlt2_1 Mltp2 c
fg
                                , Statement -> Statement
Not (Mltp2 c -> Statement
forall a. Validable a => a -> Statement
valid Mltp2 c
fg) Statement -> Statement -> Statement
|~> c -> c -> Statement
forall c. Multiplicative c => c -> c -> Statement
prpMlt2_2 c
f c
g
                                ]
                    )

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

-- prpMlt3 -


-- | validity according to "OAlg.Structure.Multiplicative.Definition#Mlt3".

prpMlt3 :: Multiplicative c => X c -> Statement
prpMlt3 :: forall c. Multiplicative c => X c -> Statement
prpMlt3 X c
xa = String -> Label
Prp String
"Mlt3"
  Label -> Statement -> Statement
:<=>: X c -> (c -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X c
xa (\c
f -> [Statement] -> Statement
And [ (Point c -> c
forall c. Multiplicative c => Point c -> c
one (c -> Point c
forall q. Oriented q => q -> Point q
end c
f) c -> c -> c
forall c. Multiplicative c => c -> c -> c
* c
f c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c
f) Bool -> Message -> Statement
:?> c -> Message
forall {a}. Show a => a -> Message
prm c
f
                             , (c
f 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 -> Bool
forall a. Eq a => a -> a -> Bool
== c
f) Bool -> Message -> Statement
:?> c -> Message
forall {a}. Show a => a -> Message
prm c
f
                             ]
                  )
  where prm :: a -> Message
prm a
f = [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
f]

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

-- prpMlt4 -


-- | validity according to "OAlg.Structure.Multiplicative.Definition#Mlt4".

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


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

-- prpMlt5 -


-- | validity of 'npower' according to "OAlg.Structure.Multiplicative.Definition#Mlt5".

--

-- __Note__ As the multiplication can by very costly the random variable for @t'X' t'N'@

-- - which serves to check "OAlg.Structure.Multiplicative.Definition#Mlt5_2" - has to be chosen

-- carefully.

prpMlt5 :: Multiplicative c => X N -> X c -> X (Endo c) -> Statement
prpMlt5 :: forall c. Multiplicative c => X N -> X c -> X (Endo c) -> Statement
prpMlt5 X N
xn X c
xf X (Endo c)
xfe = String -> Label
Prp String
"Mlt5"
  Label -> Statement -> Statement
:<=>: X (N, c) -> ((N, c) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (N, c)
xnf (\(N
n,c
f) ->
                      [Statement] -> Statement
And [ String -> Label
Label String
"5.1"
                            Label -> Statement -> Statement
:<=>: (c -> N -> c
forall c. Multiplicative c => c -> N -> c
npower c
f N
1 c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c
f) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=c -> String
forall a. Show a => a -> String
show c
f]
                          , String -> Label
Label String
"5.2"
                            Label -> Statement -> Statement
:<=>: c -> Bool
forall q. Oriented q => q -> Bool
isEndo c
f Bool -> Message -> Statement
:?> Message
MInvalid
                              Statement -> Statement -> Statement
|~> [Statement] -> Statement
And [ (c -> N -> c
forall c. Multiplicative c => c -> N -> c
npower c
f N
0 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
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=c -> String
forall a. Show a => a -> String
show c
f]
                                      , (c -> N -> c
forall c. Multiplicative c => c -> N -> c
npower c
f (N -> N
forall a. Enum a => a -> a
succ N
n) c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c
f c -> c -> c
forall c. Multiplicative c => c -> c -> c
* c -> N -> c
forall c. Multiplicative c => c -> N -> c
npower c
f N
n)
                                        Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=c -> String
forall a. Show a => a -> String
show c
f,String
"n"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
n]
                                      ]
                          ]
                   )
  where xf' :: X c
xf' = X (X c) -> X c
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (X (X c) -> X c) -> X (X c) -> X c
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(Q, X c)] -> X (X c)
forall a. [(Q, a)] -> X a
xOneOfW [(Q
10,(Endo c -> c) -> X (Endo c) -> X c
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Endo c -> c
forall q. Endo q -> q
fromEndo X (Endo c)
xfe),(Q
1,X c
xf)]
        xnf :: X (N, c)
xnf = X N -> X c -> X (N, c)
forall a b. X a -> X b -> X (a, b)
xTupple2 X N
xn X c
xf'

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

-- XMlt -


-- | random variable for 'Multiplicative' structures.

--

--   __Note__ As the multiplication could by costly, it is recommended to

--   use a bounded random variable for 'xMltN' which serves to validate

--   'npower'.

data XMlt c = XMlt
  { forall c. XMlt c -> X N
xMltN      :: X N
  , forall c. XMlt c -> X (Point c)
xMltPoint  :: X (Point c)
  , forall c. XMlt c -> X c
xMltFactor :: X c
  , forall c. XMlt c -> X (Endo c)
xMltEndo   :: X (Endo c)
  , forall c. XMlt c -> X (Mltp2 c)
xMltMltp2  :: X (Mltp2 c)
  , forall c. XMlt c -> X (Mltp3 c)
xMltMltp3  :: X (Mltp3 c)
  }

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

-- XMlt - Validable -


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

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

-- XMlt - Dualisable -


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

-- | the dual random variable with inverse 'coXMltInv'.

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


-- | from the bidual.

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

-- | from the dual with inverse 'coXMlt'.

coXMltInv :: Dual (XMlt c) -> XMlt c
coXMltInv :: forall c. Dual (XMlt c) -> XMlt c
coXMltInv = XMlt (Op (Op c)) -> XMlt c
forall c. XMlt (Op (Op c)) -> XMlt c
xMltFromOpOp (XMlt (Op (Op c)) -> XMlt c)
-> (XMlt (Op c) -> XMlt (Op (Op c))) -> XMlt (Op c) -> XMlt 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
. XMlt (Op c) -> Dual (XMlt (Op c))
XMlt (Op c) -> XMlt (Op (Op c))
forall c. XMlt c -> Dual (XMlt c)
coXMlt

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

-- MltX -


-- | index for 'Multiplicative' structures with a 'XStandardMlt'.

data MltX

type instance Structure MltX x = (Multiplicative x, XStandardMlt x)

instance TransformableG Op MltX MltX where tauG :: forall x. Struct MltX x -> Struct MltX (Op x)
tauG Struct MltX x
Struct = Struct MltX (Op x)
forall s x. Structure s x => Struct s x
Struct
instance TransformableOp MltX

instance XStandardMlt x => XStandardMlt (Op x) where
  xStandardMlt :: XMlt (Op x)
xStandardMlt = XMlt x -> Dual (XMlt x)
forall c. XMlt c -> Dual (XMlt c)
coXMlt XMlt x
forall c. XStandardMlt c => XMlt c
xStandardMlt

instance Transformable MltX Ort where tau :: forall x. Struct MltX x -> Struct Ort x
tau Struct MltX x
Struct = Struct Ort x
forall s x. Structure s x => Struct s x
Struct
instance TransformableOrt MltX

instance Transformable MltX Mlt where tau :: forall x. Struct MltX x -> Struct Mlt x
tau Struct MltX x
Struct = Struct Mlt x
forall s x. Structure s x => Struct s x
Struct
instance TransformableMlt MltX

instance Transformable MltX Typ where tau :: forall x. Struct MltX x -> Struct Typ x
tau Struct MltX x
Struct = Struct Typ x
forall s x. Structure s x => Struct s x
Struct

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

instance XStandardMlt c => XStandardMlt (Id c) where
  xStandardMlt :: XMlt (Id c)
xStandardMlt = X N
-> X (Point (Id c))
-> X (Id c)
-> X (Endo (Id c))
-> X (Mltp2 (Id c))
-> X (Mltp3 (Id c))
-> XMlt (Id c)
forall c.
X N
-> X (Point c)
-> X c
-> X (Endo c)
-> X (Mltp2 c)
-> X (Mltp3 c)
-> XMlt c
XMlt X N
xn X (Point c)
X (Point (Id c))
xp X (Id c)
x' X (Endo (Id c))
xe' X (Mltp2 (Id c))
x2' X (Mltp3 (Id c))
x3' where
    XMlt X N
xn X (Point c)
xp X c
x X (Endo c)
xe X (Mltp2 c)
x2 X (Mltp3 c)
x3 = XMlt c
forall c. XStandardMlt c => XMlt c
xStandardMlt
    x' :: X (Id c)
x'  = (c -> Id c) -> X c -> X (Id c)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 c -> Id c
forall x. x -> Id x
Id X c
x
    xe' :: X (Endo (Id c))
xe' = (Endo c -> Endo (Id c)) -> X (Endo c) -> X (Endo (Id c))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(Endo c
f) -> Id c -> Endo (Id c)
forall q. q -> Endo q
Endo (c -> Id c
forall x. x -> Id x
Id c
f)) X (Endo c)
xe
    x2' :: X (Mltp2 (Id c))
x2' = (Mltp2 c -> Mltp2 (Id c)) -> X (Mltp2 c) -> X (Mltp2 (Id c))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(Mltp2 c
f c
g) -> Id c -> Id c -> Mltp2 (Id c)
forall c. c -> c -> Mltp2 c
Mltp2 (c -> Id c
forall x. x -> Id x
Id c
f) (c -> Id c
forall x. x -> Id x
Id c
g)) X (Mltp2 c)
x2
    x3' :: X (Mltp3 (Id c))
x3' = (Mltp3 c -> Mltp3 (Id c)) -> X (Mltp3 c) -> X (Mltp3 (Id c))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(Mltp3 c
f c
g c
h) -> Id c -> Id c -> Id c -> Mltp3 (Id c)
forall c. c -> c -> c -> Mltp3 c
Mltp3 (c -> Id c
forall x. x -> Id x
Id c
f) (c -> Id c
forall x. x -> Id x
Id c
g) (c -> Id c
forall x. x -> Id x
Id c
h)) X (Mltp3 c)
x3

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

-- XStandarMlt -


-- | standard random variable for 'Multiplicative' structures.

class XStandardMlt c where
  xStandardMlt :: XMlt c
  
--------------------------------------------------------------------------------

-- prpMlt -


-- | validity of the 'Multiplicative' structure of @__c__@.

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

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

-- xMltTtl -


-- | random variable for total 'Multiplicative' structures.

xMltTtl :: Singleton (Point c) => X N -> X c -> XMlt c
xMltTtl :: forall c. Singleton (Point c) => X N -> X c -> XMlt c
xMltTtl X N
xn X c
xf = X N
-> X (Point c)
-> X c
-> X (Endo c)
-> X (Mltp2 c)
-> X (Mltp3 c)
-> XMlt c
forall c.
X N
-> X (Point c)
-> X c
-> X (Endo c)
-> X (Mltp2 c)
-> X (Mltp3 c)
-> XMlt c
XMlt X N
xn (Point c -> X (Point c)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return Point c
forall s. Singleton s => s
unit) X c
xf X (Endo c)
xfe X (Mltp2 c)
xf2 X (Mltp3 c)
xf3
  where xfe :: X (Endo c)
xfe = (c -> Endo c) -> X c -> X (Endo c)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> Endo c
forall q. q -> Endo q
Endo X c
xf -- as the multiplication is total.

        xf2 :: X (Mltp2 c)
xf2 = ((c, c) -> Mltp2 c) -> X (c, c) -> X (Mltp2 c)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((c -> c -> Mltp2 c) -> (c, c) -> Mltp2 c
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry c -> c -> Mltp2 c
forall c. c -> c -> Mltp2 c
Mltp2) (X c -> X c -> X (c, c)
forall a b. X a -> X b -> X (a, b)
xTupple2 X c
xf X c
xf)
        xf3 :: X (Mltp3 c)
xf3 = ((c, c, c) -> Mltp3 c) -> X (c, c, c) -> X (Mltp3 c)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((c -> c -> c -> Mltp3 c) -> (c, c, c) -> Mltp3 c
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 c -> c -> c -> Mltp3 c
forall c. c -> c -> c -> Mltp3 c
Mltp3) (X c -> X c -> X c -> X (c, c, c)
forall a b c. X a -> X b -> X c -> X (a, b, c)
xTupple3 X c
xf X c
xf X c
xf)

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

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

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

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

-- xMltp2 -


-- | random variable of two multiplicable factors.

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

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

-- xMltp3 -


-- | random variable of three multiplicable factors.

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

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

-- xMlt -


-- | random variable for 'Multiplicative' structures.

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

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

-- xoMlt -


-- | the induced random variable for multiplicable structures.

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

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

-- xMltOrnt -


-- | random variable for the 'Multiplicative' structure of @'Orientation' p@.

xMltOrnt :: Entity p => X N -> X p -> XMlt (Orientation p)
xMltOrnt :: forall p. Entity p => X N -> X p -> XMlt (Orientation p)
xMltOrnt X N
xn X p
xp = X N -> XOrtOrientation (Orientation p) -> XMlt (Orientation p)
forall c. Multiplicative c => X N -> XOrtOrientation c -> XMlt c
xoMlt X N
xn (X p -> XOrtOrientation (Orientation p)
forall p. X p -> XOrtOrientation (Orientation p)
xoOrnt X p
xp)

dst :: Int -> IO ()
dst :: Int -> IO ()
dst Int
n = 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 (Mltp3 (Orientation Symbol)) -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n X (Mltp3 (Orientation Symbol))
xx where
  xo :: XMlt (Orientation Symbol)
xo = X N -> X Symbol -> XMlt (Orientation Symbol)
forall p. Entity p => X N -> X p -> XMlt (Orientation p)
xMltOrnt (N -> N -> X N
xNB N
0 N
10) X Symbol
xSymbol
  xx :: X (Mltp3 (Orientation Symbol))
xx = XMlt (Orientation Symbol) -> X (Mltp3 (Orientation Symbol))
forall c. XMlt c -> X (Mltp3 c)
xMltMltp3 XMlt (Orientation Symbol)
xo

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