{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}

-- |
-- Module      : OAlg.Structure.Distributive.Proposition
-- Description : propositions on distributive structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- propositions about 'Distributive' structure.
module OAlg.Structure.Distributive.Proposition
  (

    -- * Distributive
    prpDst, XDst(..), DstX
  , prpDst1, prpDst2, prpDst3, prpDst4
  , DstRootSide(..), DstSide(..)


    -- * X
  , XStandardDst(..)
  , xDstStalkStartEnd
  
    -- ** Total
  , xDstTtl
    -- ** Orientation
  , xDstOrnt

    -- ** Oriented Direction
  , xoDst
    -- * Tools
  , dstDst

  )
  where

import Control.Monad

import Data.Kind

import OAlg.Prelude

import OAlg.Data.Singleton

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Fibred
import OAlg.Structure.FibredOriented
import OAlg.Structure.Additive
import OAlg.Structure.Distributive.Definition

--------------------------------------------------------------------------------
-- DstRootSide -

-- | predicate for a root and a factor at the root.
--
-- __Properties__ Let @p@ be in @'DstRootSide' __s__ __d__@ for a 'Distributive' structure @__d__@,
-- then holds:
--
-- (1) If @p@ matches @'LDstRoot' r f@ then holds: @'start' r '==' 'end' f@.
--
-- (2) If @p@ matches @'RDstRoot' f r@ then holds: @'start' f '==' 'end' r@.
data DstRootSide (s :: Side) d where
  LDstRoot :: Root d -> d -> DstRootSide LeftSide d
  RDstRoot :: d -> Root d -> DstRootSide RightSide d

deriving instance Distributive d => Show (DstRootSide s d)

--------------------------------------------------------------------------------
-- DstRootSide - Dualisable -

type instance Dual (DstRootSide s d) = DstRootSide (Dual s) (Op d)

instance Distributive d => Dualisable (DstRootSide RightSide d) where
  toDual :: DstRootSide 'RightSide d -> Dual (DstRootSide 'RightSide d)
toDual (RDstRoot d
f Root d
r)         = Root (Op d) -> Op d -> DstRootSide 'LeftSide (Op d)
forall d. Root d -> d -> DstRootSide 'LeftSide d
LDstRoot (Orientation (Point d) -> Orientation (Point d)
forall x. Transposable x => x -> x
transpose Orientation (Point d)
Root d
r) (d -> Op d
forall x. x -> Op x
Op d
f)
  fromDual :: Dual (DstRootSide 'RightSide d) -> DstRootSide 'RightSide d
fromDual (LDstRoot Root (Op d)
r' (Op d
f)) = d -> Root d -> DstRootSide 'RightSide d
forall d. d -> Root d -> DstRootSide 'RightSide d
RDstRoot d
f (Orientation (Point d) -> Orientation (Point d)
forall x. Transposable x => x -> x
transpose Orientation (Point d)
Root (Op d)
r')
  
--------------------------------------------------------------------------------
-- DstRootSide - Validable -

instance Distributive d => Validable (DstRootSide s d) where
  valid :: DstRootSide s d -> Statement
valid (LDstRoot Root d
r d
f)    = (Orientation (Point d), d) -> Statement
forall a. Validable a => a -> Statement
valid (Orientation (Point d)
Root d
r,d
f) Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& (Orientation (Point d) -> Point (Orientation (Point d))
forall q. Oriented q => q -> Point q
start Orientation (Point d)
Root d
r Point (Orientation (Point d))
-> Point (Orientation (Point d)) -> Statement
forall a. Eq a => a -> a -> Statement
.==. d -> Point d
forall q. Oriented q => q -> Point q
end d
f )
  valid rd :: DstRootSide s d
rd@(RDstRoot d
_ Root d
_) = DstRootSide 'LeftSide (Op d) -> Statement
forall a. Validable a => a -> Statement
valid (DstRootSide s d -> Dual (DstRootSide s d)
forall x. Dualisable x => x -> Dual x
toDual DstRootSide s d
rd)

--------------------------------------------------------------------------------
-- prpDst1 -

-- | validity according to "OAlg.Structure.Distributive#Dst1".
prpDst1 :: Distributive d => X (DstRootSide LeftSide d) -> Statement
prpDst1 :: forall d.
Distributive d =>
X (DstRootSide 'LeftSide d) -> Statement
prpDst1 X (DstRootSide 'LeftSide d)
xrg = String -> Label
Prp String
"Dst1"
  Label -> Statement -> Statement
:<=>: X (DstRootSide 'LeftSide d)
-> (DstRootSide 'LeftSide d -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (DstRootSide 'LeftSide d)
xrg (\rg :: DstRootSide 'LeftSide d
rg@(LDstRoot Root d
r d
g)
                    -> (Root d -> d
forall a. Additive a => Root a -> a
zero Root d
r d -> d -> d
forall c. Multiplicative c => c -> c -> c
* d
g d -> d -> Bool
forall a. Eq a => a -> a -> Bool
== Root d -> d
forall a. Additive a => Root a -> a
zero (d -> Point d
forall q. Oriented q => q -> Point q
start d
g Point d -> Point d -> Orientation (Point d)
forall p. p -> p -> Orientation p
:> Orientation (Point d) -> Point (Orientation (Point d))
forall q. Oriented q => q -> Point q
end Orientation (Point d)
Root d
r))
                       Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"rg"String -> String -> Parameter
:=DstRootSide 'LeftSide d -> String
forall a. Show a => a -> String
show DstRootSide 'LeftSide d
rg]
                   )

--------------------------------------------------------------------------------
-- prpDst3 -

-- | validity according to "OAlg.Structure.Distributive#Dst3".
prpDst3 :: Distributive d => X (DstRootSide RightSide d) -> Statement
prpDst3 :: forall d.
Distributive d =>
X (DstRootSide 'RightSide d) -> Statement
prpDst3 X (DstRootSide 'RightSide d)
xfr = String -> Label
Prp String
"Dst3" Label -> Statement -> Statement
:<=>: X (DstRootSide 'LeftSide (Op d)) -> Statement
forall d.
Distributive d =>
X (DstRootSide 'LeftSide d) -> Statement
prpDst1 ((DstRootSide 'RightSide d -> DstRootSide 'LeftSide (Op d))
-> X (DstRootSide 'RightSide d) -> X (DstRootSide 'LeftSide (Op d))
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DstRootSide 'RightSide d -> Dual (DstRootSide 'RightSide d)
DstRootSide 'RightSide d -> DstRootSide 'LeftSide (Op d)
forall x. Dualisable x => x -> Dual x
toDual X (DstRootSide 'RightSide d)
xfr)

--------------------------------------------------------------------------------
-- DstSide -

-- | predicate for two addable summands together with a matching factor.
--
-- __Properties__ Let @p@ be in @'DstSide' __s__ __d__@ for a 'Distributive' structure, then holds:
--
-- (1) If @p@ matches @'LDst' (a,b) g@ then holds:
--
--     (1) @'root' a '==' 'root' b@.
--
--     (2) @'start' a '==' 'end' g@.
--
-- (2) If @p@ matches @'RDst' f (a,b)@ then holds:
--
--     (1) @'root' a '==' 'root' b@.
--
--     (2) @'start' f '==' 'end' a@.
data DstSide (s :: Side) d where
  LDst :: (d,d) -> d -> DstSide LeftSide d
  RDst :: d -> (d,d) -> DstSide RightSide d

deriving instance Distributive d => Show (DstSide s d)

--------------------------------------------------------------------------------
-- DstSide - Dualisable -

type instance Dual (DstSide s d) = DstSide (Dual s) (Op d)

instance Distributive d => Dualisable (DstSide RightSide d) where
  toDual :: DstSide 'RightSide d -> Dual (DstSide 'RightSide d)
toDual (RDst d
f (d
a,d
b)) = (Op d, Op d) -> Op d -> DstSide 'LeftSide (Op d)
forall d. (d, d) -> d -> DstSide 'LeftSide d
LDst (d -> Op d
forall x. x -> Op x
Op d
a,d -> Op d
forall x. x -> Op x
Op d
b) (d -> Op d
forall x. x -> Op x
Op d
f)
  fromDual :: Dual (DstSide 'RightSide d) -> DstSide 'RightSide d
fromDual (LDst (Op d
a,Op d
b) (Op d
f)) = d -> (d, d) -> DstSide 'RightSide d
forall d. d -> (d, d) -> DstSide 'RightSide d
RDst d
f (d
a,d
b)

--------------------------------------------------------------------------------
-- DstSide - Validable -

instance Distributive d => Validable (DstSide s d) where
  valid :: DstSide s d -> Statement
valid (LDst (d
a,d
b) d
g) = Adbl2 d -> Statement
forall a. Validable a => a -> Statement
valid (d -> d -> Adbl2 d
forall a. a -> a -> Adbl2 a
Adbl2 d
a d
b) Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& Mltp2 d -> Statement
forall a. Validable a => a -> Statement
valid (d -> d -> Mltp2 d
forall c. c -> c -> Mltp2 c
Mltp2 d
a d
g)
  valid rd :: DstSide s d
rd@(RDst d
_ (d, d)
_)  = DstSide 'LeftSide (Op d) -> Statement
forall a. Validable a => a -> Statement
valid (DstSide s d -> Dual (DstSide s d)
forall x. Dualisable x => x -> Dual x
toDual DstSide s d
rd)
  
--------------------------------------------------------------------------------
-- prpDst2 -

-- | validity according to "OAlg.Structure.Distributive#Dst2".
prpDst2 :: Distributive d => X (DstSide LeftSide d) -> Statement
prpDst2 :: forall d. Distributive d => X (DstSide 'LeftSide d) -> Statement
prpDst2 X (DstSide 'LeftSide d)
xabg = String -> Label
Prp String
"Dst2"
  Label -> Statement -> Statement
:<=>: X (DstSide 'LeftSide d)
-> (DstSide 'LeftSide d -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (DstSide 'LeftSide d)
xabg
          (\abg :: DstSide 'LeftSide d
abg@(LDst (d
a,d
b) d
g)
           -> ((d
a d -> d -> d
forall a. Additive a => a -> a -> a
+ d
b) d -> d -> d
forall c. Multiplicative c => c -> c -> c
* d
g d -> d -> Bool
forall a. Eq a => a -> a -> Bool
== d
ad -> d -> d
forall c. Multiplicative c => c -> c -> c
*d
g d -> d -> d
forall a. Additive a => a -> a -> a
+ d
bd -> d -> d
forall c. Multiplicative c => c -> c -> c
*d
g) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"abg"String -> String -> Parameter
:=DstSide 'LeftSide d -> String
forall a. Show a => a -> String
show DstSide 'LeftSide d
abg]
          )
          
--------------------------------------------------------------------------------
-- prpDst4 -

-- | validity according to "OAlg.Structure.Distributive#Dst4".
prpDst4 :: Distributive d => X (DstSide RightSide d) -> Statement
prpDst4 :: forall d. Distributive d => X (DstSide 'RightSide d) -> Statement
prpDst4 X (DstSide 'RightSide d)
xfab = String -> Label
Prp String
"Dst4" Label -> Statement -> Statement
:<=>: X (DstSide 'LeftSide (Op d)) -> Statement
forall d. Distributive d => X (DstSide 'LeftSide d) -> Statement
prpDst2 ((DstSide 'RightSide d -> DstSide 'LeftSide (Op d))
-> X (DstSide 'RightSide d) -> X (DstSide 'LeftSide (Op d))
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DstSide 'RightSide d -> Dual (DstSide 'RightSide d)
DstSide 'RightSide d -> DstSide 'LeftSide (Op d)
forall x. Dualisable x => x -> Dual x
toDual X (DstSide 'RightSide d)
xfab) 
                               

--------------------------------------------------------------------------------
-- XDst -

-- | random variable for validating 'Distributive' structures.
data XDst d = XDst (X (DstRootSide LeftSide d))  (X (DstSide LeftSide d))
                   (X (DstRootSide RightSide d)) (X (DstSide RightSide d))

--------------------------------------------------------------------------------
-- XStandardDst -

-- | standard random variable for 'Distributive' structures.
class XStandardDst d where
  xStandardDst :: XDst d

instance (FibredOriented x, XStandardDst x) => XStandardDst (Op x) where
  xStandardDst :: XDst (Op x)
xStandardDst = X (DstRootSide 'LeftSide (Op x))
-> X (DstSide 'LeftSide (Op x))
-> X (DstRootSide 'RightSide (Op x))
-> X (DstSide 'RightSide (Op x))
-> XDst (Op x)
forall d.
X (DstRootSide 'LeftSide d)
-> X (DstSide 'LeftSide d)
-> X (DstRootSide 'RightSide d)
-> X (DstSide 'RightSide d)
-> XDst d
XDst X (DstRootSide 'LeftSide (Op x))
xdrl' X (DstSide 'LeftSide (Op x))
xdl' X (DstRootSide 'RightSide (Op x))
xdrr' X (DstSide 'RightSide (Op x))
xdr' where
    XDst X (DstRootSide 'LeftSide x)
xdrl X (DstSide 'LeftSide x)
xdl X (DstRootSide 'RightSide x)
xdrr X (DstSide 'RightSide x)
xdr = XDst x
forall d. XStandardDst d => XDst d
xStandardDst
    xdrl' :: X (DstRootSide 'LeftSide (Op x))
xdrl' = do
      RDstRoot x
f Root x
r <- X (DstRootSide 'RightSide x)
xdrr
      DstRootSide 'LeftSide (Op x) -> X (DstRootSide 'LeftSide (Op x))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Root (Op x) -> Op x -> DstRootSide 'LeftSide (Op x)
forall d. Root d -> d -> DstRootSide 'LeftSide d
LDstRoot (Orientation (Point x) -> Orientation (Point x)
forall p. Orientation p -> Orientation p
opposite Orientation (Point x)
Root x
r) (x -> Op x
forall x. x -> Op x
Op x
f))
    xdl' :: X (DstSide 'LeftSide (Op x))
xdl'  = do
      RDst x
f (x
a,x
b) <- X (DstSide 'RightSide x)
xdr
      DstSide 'LeftSide (Op x) -> X (DstSide 'LeftSide (Op x))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Op x, Op x) -> Op x -> DstSide 'LeftSide (Op x)
forall d. (d, d) -> d -> DstSide 'LeftSide d
LDst (x -> Op x
forall x. x -> Op x
Op x
a,x -> Op x
forall x. x -> Op x
Op x
b) (x -> Op x
forall x. x -> Op x
Op x
f))
    xdrr' :: X (DstRootSide 'RightSide (Op x))
xdrr' = do
      LDstRoot Root x
r x
f <- X (DstRootSide 'LeftSide x)
xdrl
      DstRootSide 'RightSide (Op x) -> X (DstRootSide 'RightSide (Op x))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Op x -> Root (Op x) -> DstRootSide 'RightSide (Op x)
forall d. d -> Root d -> DstRootSide 'RightSide d
RDstRoot (x -> Op x
forall x. x -> Op x
Op x
f) (Orientation (Point x) -> Orientation (Point x)
forall p. Orientation p -> Orientation p
opposite Orientation (Point x)
Root x
r))
    xdr' :: X (DstSide 'RightSide (Op x))
xdr'   = do
      LDst (x
a,x
b) x
f <- X (DstSide 'LeftSide x)
xdl
      DstSide 'RightSide (Op x) -> X (DstSide 'RightSide (Op x))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Op x -> (Op x, Op x) -> DstSide 'RightSide (Op x)
forall d. d -> (d, d) -> DstSide 'RightSide d
RDst (x -> Op x
forall x. x -> Op x
Op x
f) (x -> Op x
forall x. x -> Op x
Op x
a,x -> Op x
forall x. x -> Op x
Op x
b))

instance XStandardDst x => XStandardDst (Id x) where
  xStandardDst :: XDst (Id x)
xStandardDst = X (DstRootSide 'LeftSide (Id x))
-> X (DstSide 'LeftSide (Id x))
-> X (DstRootSide 'RightSide (Id x))
-> X (DstSide 'RightSide (Id x))
-> XDst (Id x)
forall d.
X (DstRootSide 'LeftSide d)
-> X (DstSide 'LeftSide d)
-> X (DstRootSide 'RightSide d)
-> X (DstSide 'RightSide d)
-> XDst d
XDst X (DstRootSide 'LeftSide (Id x))
xdrl' X (DstSide 'LeftSide (Id x))
xdl' X (DstRootSide 'RightSide (Id x))
xdrr' X (DstSide 'RightSide (Id x))
xdr' where
    XDst X (DstRootSide 'LeftSide x)
xdrl X (DstSide 'LeftSide x)
xdl X (DstRootSide 'RightSide x)
xdrr X (DstSide 'RightSide x)
xdr = XDst x
forall d. XStandardDst d => XDst d
xStandardDst
    xdrl' :: X (DstRootSide 'LeftSide (Id x))
xdrl' = do
      LDstRoot Root x
r x
f <- X (DstRootSide 'LeftSide x)
xdrl
      DstRootSide 'LeftSide (Id x) -> X (DstRootSide 'LeftSide (Id x))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Root (Id x) -> Id x -> DstRootSide 'LeftSide (Id x)
forall d. Root d -> d -> DstRootSide 'LeftSide d
LDstRoot Root x
Root (Id x)
r (x -> Id x
forall x. x -> Id x
Id x
f))
    xdl' :: X (DstSide 'LeftSide (Id x))
xdl'  = do
      LDst (x
a,x
b) x
f <- X (DstSide 'LeftSide x)
xdl
      DstSide 'LeftSide (Id x) -> X (DstSide 'LeftSide (Id x))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Id x, Id x) -> Id x -> DstSide 'LeftSide (Id x)
forall d. (d, d) -> d -> DstSide 'LeftSide d
LDst (x -> Id x
forall x. x -> Id x
Id x
a,x -> Id x
forall x. x -> Id x
Id x
b) (x -> Id x
forall x. x -> Id x
Id x
f))
    xdrr' :: X (DstRootSide 'RightSide (Id x))
xdrr' = do
      RDstRoot x
f Root x
r <- X (DstRootSide 'RightSide x)
xdrr
      DstRootSide 'RightSide (Id x) -> X (DstRootSide 'RightSide (Id x))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Id x -> Root (Id x) -> DstRootSide 'RightSide (Id x)
forall d. d -> Root d -> DstRootSide 'RightSide d
RDstRoot (x -> Id x
forall x. x -> Id x
Id x
f) Root x
Root (Id x)
r)
    xdr' :: X (DstSide 'RightSide (Id x))
xdr'  = do
      RDst x
f (x
a,x
b) <- X (DstSide 'RightSide x)
xdr
      DstSide 'RightSide (Id x) -> X (DstSide 'RightSide (Id x))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Id x -> (Id x, Id x) -> DstSide 'RightSide (Id x)
forall d. d -> (d, d) -> DstSide 'RightSide d
RDst (x -> Id x
forall x. x -> Id x
Id x
f) (x -> Id x
forall x. x -> Id x
Id x
a, x -> Id x
forall x. x -> Id x
Id x
b))
  
--------------------------------------------------------------------------------
-- prpDst -

-- | validity for the 'Distributive' structure of the type @a@.
prpDst :: Distributive d => XDst d -> Statement
prpDst :: forall d. Distributive d => XDst d -> Statement
prpDst (XDst X (DstRootSide 'LeftSide d)
xrg X (DstSide 'LeftSide d)
xabg X (DstRootSide 'RightSide d)
xfr X (DstSide 'RightSide d)
xfab) = String -> Label
Prp String
"Dst"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ X (DstRootSide 'LeftSide d) -> Statement
forall d.
Distributive d =>
X (DstRootSide 'LeftSide d) -> Statement
prpDst1 X (DstRootSide 'LeftSide d)
xrg
            , X (DstSide 'LeftSide d) -> Statement
forall d. Distributive d => X (DstSide 'LeftSide d) -> Statement
prpDst2 X (DstSide 'LeftSide d)
xabg
            , X (DstRootSide 'RightSide d) -> Statement
forall d.
Distributive d =>
X (DstRootSide 'RightSide d) -> Statement
prpDst3 X (DstRootSide 'RightSide d)
xfr
            , X (DstSide 'RightSide d) -> Statement
forall d. Distributive d => X (DstSide 'RightSide d) -> Statement
prpDst4 X (DstSide 'RightSide d)
xfab
            ]

--------------------------------------------------------------------------------
-- xDstTtl -

-- | random variable to validate 'Total' 'Distributive' structures.
xDstTtl :: Singleton (Root m) => X m -> XDst m
xDstTtl :: forall m. Singleton (Root m) => X m -> XDst m
xDstTtl X m
xm = X (DstRootSide 'LeftSide m)
-> X (DstSide 'LeftSide m)
-> X (DstRootSide 'RightSide m)
-> X (DstSide 'RightSide m)
-> XDst m
forall d.
X (DstRootSide 'LeftSide d)
-> X (DstSide 'LeftSide d)
-> X (DstRootSide 'RightSide d)
-> X (DstSide 'RightSide d)
-> XDst d
XDst X (DstRootSide 'LeftSide m)
xrg X (DstSide 'LeftSide m)
xabg X (DstRootSide 'RightSide m)
xfr X (DstSide 'RightSide m)
xfab where
  xrg :: X (DstRootSide 'LeftSide m)
xrg = do
    m
g <- X m
xm
    DstRootSide 'LeftSide m -> X (DstRootSide 'LeftSide m)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (DstRootSide 'LeftSide m -> X (DstRootSide 'LeftSide m))
-> DstRootSide 'LeftSide m -> X (DstRootSide 'LeftSide m)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Root m -> m -> DstRootSide 'LeftSide m
forall d. Root d -> d -> DstRootSide 'LeftSide d
LDstRoot Root m
forall s. Singleton s => s
unit m
g
  xabg :: X (DstSide 'LeftSide m)
xabg = do
    m
a <- X m
xm
    m
b <- X m
xm
    m
g <- X m
xm
    DstSide 'LeftSide m -> X (DstSide 'LeftSide m)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (DstSide 'LeftSide m -> X (DstSide 'LeftSide m))
-> DstSide 'LeftSide m -> X (DstSide 'LeftSide m)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (m, m) -> m -> DstSide 'LeftSide m
forall d. (d, d) -> d -> DstSide 'LeftSide d
LDst (m
a,m
b) m
g
  xfr :: X (DstRootSide 'RightSide m)
xfr  = do
    m
f <- X m
xm
    DstRootSide 'RightSide m -> X (DstRootSide 'RightSide m)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (DstRootSide 'RightSide m -> X (DstRootSide 'RightSide m))
-> DstRootSide 'RightSide m -> X (DstRootSide 'RightSide m)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ m -> Root m -> DstRootSide 'RightSide m
forall d. d -> Root d -> DstRootSide 'RightSide d
RDstRoot m
f Root m
forall s. Singleton s => s
unit
  xfab :: X (DstSide 'RightSide m)
xfab = do
    m
f <- X m
xm
    m
a <- X m
xm
    m
b <- X m
xm
    DstSide 'RightSide m -> X (DstSide 'RightSide m)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (DstSide 'RightSide m -> X (DstSide 'RightSide m))
-> DstSide 'RightSide m -> X (DstSide 'RightSide m)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ m -> (m, m) -> DstSide 'RightSide m
forall d. d -> (d, d) -> DstSide 'RightSide d
RDst m
f (m
a,m
b)

instance XStandardDst N where
  xStandardDst :: XDst N
xStandardDst = X N -> XDst N
forall m. Singleton (Root m) => X m -> XDst m
xDstTtl X N
forall x. XStandard x => X x
xStandard
  
instance XStandardDst Z where
  xStandardDst :: XDst Z
xStandardDst = X Z -> XDst Z
forall m. Singleton (Root m) => X m -> XDst m
xDstTtl X Z
forall x. XStandard x => X x
xStandard
  
instance XStandardDst Q where
  xStandardDst :: XDst Q
xStandardDst = X Q -> XDst Q
forall m. Singleton (Root m) => X m -> XDst m
xDstTtl X Q
forall x. XStandard x => X x
xStandard
  
--------------------------------------------------------------------------------
-- xDstStalkStartEnd -

-- | the induced random variable for 'Distributive' structures.
xDstStalkStartEnd :: Distributive m
     => XStalk m
     -> XOrtSite From m
     -> XOrtSite To m
     -> XDst m
xDstStalkStartEnd :: forall m.
Distributive m =>
XStalk m -> XOrtSite 'From m -> XOrtSite 'To m -> XDst m
xDstStalkStartEnd XStalk m
xa XOrtSite 'From m
xs XOrtSite 'To m
xe = X (DstRootSide 'LeftSide m)
-> X (DstSide 'LeftSide m)
-> X (DstRootSide 'RightSide m)
-> X (DstSide 'RightSide m)
-> XDst m
forall d.
X (DstRootSide 'LeftSide d)
-> X (DstSide 'LeftSide d)
-> X (DstRootSide 'RightSide d)
-> X (DstSide 'RightSide d)
-> XDst d
XDst X (DstRootSide 'LeftSide m)
xrg X (DstSide 'LeftSide m)
xabg X (DstRootSide 'RightSide m)
xfr X (DstSide 'RightSide m)
xfab where
  xrg :: X (DstRootSide 'LeftSide m)
xrg = do
    Orientation (Point m)
r          <- XStalk m -> X (Root m)
forall x. XStalk x -> X (Root x)
xRoot XStalk m
xa
    Path Point m
_ [m
g] <- XOrtSite 'To m -> N -> Point m -> X (Path m)
forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> Point c -> X (Path c)
xosPathAt XOrtSite 'To m
xe N
1 (Orientation (Point m) -> Point (Orientation (Point m))
forall q. Oriented q => q -> Point q
start Orientation (Point m)
r)
    DstRootSide 'LeftSide m -> X (DstRootSide 'LeftSide m)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (DstRootSide 'LeftSide m -> X (DstRootSide 'LeftSide m))
-> DstRootSide 'LeftSide m -> X (DstRootSide 'LeftSide m)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Root m -> m -> DstRootSide 'LeftSide m
forall d. Root d -> d -> DstRootSide 'LeftSide d
LDstRoot Orientation (Point m)
Root m
r m
g
  xabg :: X (DstSide 'LeftSide m)
xabg = do
    Orientation (Point m)
r          <- XStalk m -> X (Root m)
forall x. XStalk x -> X (Root x)
xRoot XStalk m
xa
    Adbl2 m
a m
b  <- XStalk m -> Root m -> X (Adbl2 m)
forall a. Additive a => XStalk a -> Root a -> X (Adbl2 a)
xStalkAdbl2 XStalk m
xa Orientation (Point m)
Root m
r
    Path Point m
_ [m
g] <- XOrtSite 'To m -> N -> Point m -> X (Path m)
forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> Point c -> X (Path c)
xosPathAt XOrtSite 'To m
xe N
1 (Orientation (Point m) -> Point (Orientation (Point m))
forall q. Oriented q => q -> Point q
start Orientation (Point m)
r)
    DstSide 'LeftSide m -> X (DstSide 'LeftSide m)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (DstSide 'LeftSide m -> X (DstSide 'LeftSide m))
-> DstSide 'LeftSide m -> X (DstSide 'LeftSide m)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (m, m) -> m -> DstSide 'LeftSide m
forall d. (d, d) -> d -> DstSide 'LeftSide d
LDst (m
a,m
b) m
g
  xfr :: X (DstRootSide 'RightSide m)
xfr = do
    Orientation (Point m)
r          <- XStalk m -> X (Root m)
forall x. XStalk x -> X (Root x)
xRoot XStalk m
xa
    Path Point m
_ [m
f] <- XOrtSite 'From m -> N -> Point m -> X (Path m)
forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> Point c -> X (Path c)
xosPathAt XOrtSite 'From m
xs N
1 (Orientation (Point m) -> Point (Orientation (Point m))
forall q. Oriented q => q -> Point q
end Orientation (Point m)
r)
    DstRootSide 'RightSide m -> X (DstRootSide 'RightSide m)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (DstRootSide 'RightSide m -> X (DstRootSide 'RightSide m))
-> DstRootSide 'RightSide m -> X (DstRootSide 'RightSide m)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ m -> Root m -> DstRootSide 'RightSide m
forall d. d -> Root d -> DstRootSide 'RightSide d
RDstRoot m
f Orientation (Point m)
Root m
r
    
  xfab :: X (DstSide 'RightSide m)
xfab = do
    Orientation (Point m)
r          <- XStalk m -> X (Root m)
forall x. XStalk x -> X (Root x)
xRoot XStalk m
xa
    Path Point m
_ [m
f] <- XOrtSite 'From m -> N -> Point m -> X (Path m)
forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> Point c -> X (Path c)
xosPathAt XOrtSite 'From m
xs N
1 (Orientation (Point m) -> Point (Orientation (Point m))
forall q. Oriented q => q -> Point q
end Orientation (Point m)
r)
    Adbl2 m
a m
b  <- XStalk m -> Root m -> X (Adbl2 m)
forall a. Additive a => XStalk a -> Root a -> X (Adbl2 a)
xStalkAdbl2 XStalk m
xa Orientation (Point m)
Root m
r
    DstSide 'RightSide m -> X (DstSide 'RightSide m)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (DstSide 'RightSide m -> X (DstSide 'RightSide m))
-> DstSide 'RightSide m -> X (DstSide 'RightSide m)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ m -> (m, m) -> DstSide 'RightSide m
forall d. d -> (d, d) -> DstSide 'RightSide d
RDst m
f (m
a,m
b)

--------------------------------------------------------------------------------
-- xDstOrnt -

-- | random variable for the 'Distributive' structure of @'Orientation' __p__@.
xDstOrnt :: Entity p => X p -> XDst (Orientation p)
xDstOrnt :: forall p. Entity p => X p -> XDst (Orientation p)
xDstOrnt X p
xp = XStalk (Orientation p)
-> XOrtSite 'From (Orientation p)
-> XOrtSite 'To (Orientation p)
-> XDst (Orientation p)
forall m.
Distributive m =>
XStalk m -> XOrtSite 'From m -> XOrtSite 'To m -> XDst m
xDstStalkStartEnd XStalk (Orientation p)
xa XOrtSite 'From (Orientation p)
xs XOrtSite 'To (Orientation p)
xe where
  xa :: XStalk (Orientation p)
xa = X p -> XStalk (Orientation p)
forall p. X p -> XStalk (Orientation p)
xStalkOrnt X p
xp
  xs :: XOrtSite 'From (Orientation p)
xs = X p -> XOrtSite 'From (Orientation p)
forall p. X p -> XOrtSite 'From (Orientation p)
xStartOrnt X p
xp
  xe :: XOrtSite 'To (Orientation p)
xe = X p -> XOrtSite 'To (Orientation p)
forall p. X p -> XOrtSite 'To (Orientation p)
xEndOrnt X p
xp
  
instance (Entity p, XStandard p) => XStandardDst (Orientation p) where
  xStandardDst :: XDst (Orientation p)
xStandardDst = X p -> XDst (Orientation p)
forall p. Entity p => X p -> XDst (Orientation p)
xDstOrnt X p
forall x. XStandard x => X x
xStandard
  
--------------------------------------------------------------------------------
-- dstDst -

-- | distribution of @'XDst' __d__@.
dstDst :: Distributive d => Int -> XDst d -> IO ()
dstDst :: forall d. Distributive d => Int -> XDst d -> IO ()
dstDst Int
n (XDst X (DstRootSide 'LeftSide d)
xrg X (DstSide 'LeftSide d)
xabg X (DstRootSide 'RightSide d)
xfr X (DstSide 'RightSide d)
xfab) = do
  Omega
o <- IO Omega
getOmega
  String -> IO ()
putStrLn String
"xrg"
  Int -> X String -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n ((DstRootSide 'LeftSide d -> String)
-> X (DstRootSide 'LeftSide d) -> X String
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DstRootSide 'LeftSide d -> String
forall a. Show a => a -> String
show X (DstRootSide 'LeftSide d)
xrg) Omega
o
  String -> IO ()
putStrLn String
"xabg"
  Int -> X String -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n ((DstSide 'LeftSide d -> String)
-> X (DstSide 'LeftSide d) -> X String
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DstSide 'LeftSide d -> String
forall a. Show a => a -> String
show X (DstSide 'LeftSide d)
xabg) Omega
o
  String -> IO ()
putStrLn String
"xfr"
  Int -> X String -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n ((DstRootSide 'RightSide d -> String)
-> X (DstRootSide 'RightSide d) -> X String
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DstRootSide 'RightSide d -> String
forall a. Show a => a -> String
show X (DstRootSide 'RightSide d)
xfr) Omega
o
  String -> IO ()
putStrLn String
"xfab"
  Int -> X String -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n ((DstSide 'RightSide d -> String)
-> X (DstSide 'RightSide d) -> X String
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DstSide 'RightSide d -> String
forall a. Show a => a -> String
show X (DstSide 'RightSide d)
xfab) Omega
o

--------------------------------------------------------------------------------
-- xoDstRootSideL -

-- | the induced random variable for @'DstRootSide' 'LeftSide' __d__'@.
xoDstRootSideL :: Distributive d
  => XOrtOrientation d -> XOrtSite To d -> X (DstRootSide LeftSide d)
xoDstRootSideL :: forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'To d -> X (DstRootSide 'LeftSide d)
xoDstRootSideL XOrtOrientation d
xo XOrtSite 'To d
xt = do
  Orientation (Point d)
r <- XOrtOrientation d -> X (Root d)
forall a. FibredOriented a => XOrtOrientation a -> X (Root a)
xoRoot XOrtOrientation d
xo
  d
f <- XOrtSite 'To d -> Point d -> X d
forall q. XOrtSite 'To q -> Point q -> X q
xosEnd XOrtSite 'To d
xt (Orientation (Point d) -> Point (Orientation (Point d))
forall q. Oriented q => q -> Point q
start Orientation (Point d)
r)
  DstRootSide 'LeftSide d -> X (DstRootSide 'LeftSide d)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Root d -> d -> DstRootSide 'LeftSide d
forall d. Root d -> d -> DstRootSide 'LeftSide d
LDstRoot Orientation (Point d)
Root d
r d
f)

--------------------------------------------------------------------------------
-- xoDstRootSideR -

-- | the induced random variable for @'DstRootSide' 'RightSide' __d__'@.
xoDstRootSideR :: Distributive d
  => XOrtOrientation d -> XOrtSite From d -> X (DstRootSide RightSide d)
xoDstRootSideR :: forall d.
Distributive d =>
XOrtOrientation d
-> XOrtSite 'From d -> X (DstRootSide 'RightSide d)
xoDstRootSideR XOrtOrientation d
xo XOrtSite 'From d
xs
  = (DstRootSide 'LeftSide (Op d) -> DstRootSide 'RightSide d)
-> X (DstRootSide 'LeftSide (Op d)) -> X (DstRootSide 'RightSide d)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Dual (DstRootSide 'RightSide d) -> DstRootSide 'RightSide d
DstRootSide 'LeftSide (Op d) -> DstRootSide 'RightSide d
forall x. Dualisable x => Dual x -> x
fromDual (X (DstRootSide 'LeftSide (Op d)) -> X (DstRootSide 'RightSide d))
-> X (DstRootSide 'LeftSide (Op d)) -> X (DstRootSide 'RightSide d)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtOrientation (Op d)
-> XOrtSite 'To (Op d) -> X (DstRootSide 'LeftSide (Op d))
forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'To d -> X (DstRootSide 'LeftSide d)
xoDstRootSideL (XOrtOrientation d -> Dual (XOrtOrientation d)
forall q. XOrtOrientation q -> Dual (XOrtOrientation q)
coXOrtOrientation XOrtOrientation d
xo) (XOrtSite 'From d -> Dual (XOrtSite 'From d)
forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'From d
xs)

--------------------------------------------------------------------------------
-- xoDstSideL -

-- | the induced random variable for @'DstSide' 'LeftSide' __d__'@.
xoDstSideL :: Distributive d
  => XOrtOrientation d -> XOrtSite To d -> X (DstSide LeftSide d)
xoDstSideL :: forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'To d -> X (DstSide 'LeftSide d)
xoDstSideL XOrtOrientation d
xo XOrtSite 'To d
xt = do
  Adbl2 d
a d
b <- XOrtOrientation d -> X (Adbl2 d)
forall a. FibredOriented a => XOrtOrientation a -> X (Adbl2 a)
xoAdbl2 XOrtOrientation d
xo
  d
f <- XOrtSite 'To d -> Point d -> X d
forall q. XOrtSite 'To q -> Point q -> X q
xosEnd XOrtSite 'To d
xt (d -> Point d
forall q. Oriented q => q -> Point q
start d
a)
  DstSide 'LeftSide d -> X (DstSide 'LeftSide d)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ((d, d) -> d -> DstSide 'LeftSide d
forall d. (d, d) -> d -> DstSide 'LeftSide d
LDst (d
a,d
b) d
f)

--------------------------------------------------------------------------------
-- xoDstSideR -

-- | the induced random variable for @'DstSide' 'RightSide' __d__'@.
xoDstSideR :: Distributive d
  => XOrtOrientation d -> XOrtSite From d -> X (DstSide RightSide d)
xoDstSideR :: forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'From d -> X (DstSide 'RightSide d)
xoDstSideR XOrtOrientation d
xo XOrtSite 'From d
xf = (DstSide 'LeftSide (Op d) -> DstSide 'RightSide d)
-> X (DstSide 'LeftSide (Op d)) -> X (DstSide 'RightSide d)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Dual (DstSide 'RightSide d) -> DstSide 'RightSide d
DstSide 'LeftSide (Op d) -> DstSide 'RightSide d
forall x. Dualisable x => Dual x -> x
fromDual (X (DstSide 'LeftSide (Op d)) -> X (DstSide 'RightSide d))
-> X (DstSide 'LeftSide (Op d)) -> X (DstSide 'RightSide d)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtOrientation (Op d)
-> XOrtSite 'To (Op d) -> X (DstSide 'LeftSide (Op d))
forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'To d -> X (DstSide 'LeftSide d)
xoDstSideL (XOrtOrientation d -> Dual (XOrtOrientation d)
forall q. XOrtOrientation q -> Dual (XOrtOrientation q)
coXOrtOrientation XOrtOrientation d
xo) (XOrtSite 'From d -> Dual (XOrtSite 'From d)
forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'From d
xf)

--------------------------------------------------------------------------------
-- xodDst -

-- | the induced random variable for 'Distributive' structures.
xoDst :: Distributive d
  => XOrtOrientation d -> XOrtSite From d -> XOrtSite To d -> XDst d
xoDst :: forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'From d -> XOrtSite 'To d -> XDst d
xoDst XOrtOrientation d
xo XOrtSite 'From d
xf XOrtSite 'To d
xt = X (DstRootSide 'LeftSide d)
-> X (DstSide 'LeftSide d)
-> X (DstRootSide 'RightSide d)
-> X (DstSide 'RightSide d)
-> XDst d
forall d.
X (DstRootSide 'LeftSide d)
-> X (DstSide 'LeftSide d)
-> X (DstRootSide 'RightSide d)
-> X (DstSide 'RightSide d)
-> XDst d
XDst X (DstRootSide 'LeftSide d)
xrsl X (DstSide 'LeftSide d)
xsl X (DstRootSide 'RightSide d)
xrsr X (DstSide 'RightSide d)
xsr where
  xrsl :: X (DstRootSide 'LeftSide d)
xrsl = XOrtOrientation d -> XOrtSite 'To d -> X (DstRootSide 'LeftSide d)
forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'To d -> X (DstRootSide 'LeftSide d)
xoDstRootSideL XOrtOrientation d
xo XOrtSite 'To d
xt
  xsl :: X (DstSide 'LeftSide d)
xsl = XOrtOrientation d -> XOrtSite 'To d -> X (DstSide 'LeftSide d)
forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'To d -> X (DstSide 'LeftSide d)
xoDstSideL XOrtOrientation d
xo XOrtSite 'To d
xt
  xrsr :: X (DstRootSide 'RightSide d)
xrsr = XOrtOrientation d
-> XOrtSite 'From d -> X (DstRootSide 'RightSide d)
forall d.
Distributive d =>
XOrtOrientation d
-> XOrtSite 'From d -> X (DstRootSide 'RightSide d)
xoDstRootSideR XOrtOrientation d
xo XOrtSite 'From d
xf
  xsr :: X (DstSide 'RightSide d)
xsr = XOrtOrientation d -> XOrtSite 'From d -> X (DstSide 'RightSide d)
forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'From d -> X (DstSide 'RightSide d)
xoDstSideR XOrtOrientation d
xo XOrtSite 'From d
xf

--------------------------------------------------------------------------------
-- DstX -

-- | type index for 'Distributive' structures admitting 'XStandardOrtOrientation'.
data DstX

type instance Structure DstX x = (Distributive x, XStandardOrtOrientation x)

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

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

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

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

instance Transformable DstX Fbr where tau :: forall x. Struct DstX x -> Struct Fbr x
tau Struct DstX x
Struct = Struct Fbr x
forall s x. Structure s x => Struct s x
Struct
instance TransformableFbr DstX

instance Transformable DstX Add where tau :: forall x. Struct DstX x -> Struct Add x
tau Struct DstX x
Struct = Struct Add x
forall s x. Structure s x => Struct s x
Struct
instance TransformableAdd DstX

instance Transformable DstX FbrOrt where tau :: forall x. Struct DstX x -> Struct FbrOrt x
tau Struct DstX x
Struct = Struct FbrOrt x
forall s x. Structure s x => Struct s x
Struct
instance TransformableFbrOrt DstX

instance Transformable DstX Dst where tau :: forall x. Struct DstX x -> Struct Dst x
tau Struct DstX x
Struct = Struct Dst x
forall s x. Structure s x => Struct s x
Struct
instance TransformableDst DstX

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