{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Structure.Oriented.X

-- Description : random variables for oriented structures.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- random variables for 'Oriented' structures.

module OAlg.Structure.Oriented.X
  (

    -- * Site

    XOrtSite(..), OrtSiteX, XStandardOrtSite(..)
  , XStandardOrtSiteTo, XStandardOrtSiteFrom
  , coXOrtSite, coXOrtSiteInv, xosFromOpOp
  , xosStart, xosEnd
  , xosPathMaxAt, xosPathMax

    -- * Orientation

  , XOrtOrientation(..), xoOrientation, xoArrow, xoPoint
  , coXOrtOrientation
  , xoTo, xoFrom
  , xoTtl, xoOrnt
  , XStandardOrtOrientation(..)

    -- * Orientation

  , xStartOrnt, xEndOrnt
  )
  where

import Control.Monad as M
import Control.Applicative ((<|>))

import Data.Kind
import Data.Typeable

import OAlg.Prelude

import OAlg.Data.Singleton

import OAlg.Structure.Oriented.Definition
import OAlg.Structure.Oriented.Opposite
import OAlg.Structure.Oriented.Path


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

-- XOrtSite -


-- | random variables @'OAlg.Data.X.X' __q__@ and @'OAlg.Data.X.X' ('Point' __q__)@ for

-- 'Oriented' structure @__q__@.

--

-- __Properties__ Let @__q__@ be an instance of the class 'Oriented', then holds:

--

-- (1) Let @'XStart' xp xStart@ be in @'XOrtSite' 'From' __q__@, then holds:

-- For all @p@ in @'Point' __q__@ and @x@ in the range of @xStart p@ holds: @'start' x '==' p@.

--

-- (2) Let @'XEnd' xp xEnd@ be in @'XOrtSite' 'To' __q__@, then holds:

-- For all @p@ in @'Point' __q__@ and @x@ in the range of @xEnd p@ holds: @'end' x '==' p@.

--

-- __Note__ The random variables @xp@ should have a bias to non trivial random variables

-- @xp '>>=' xStart@ or @xp '>>=' xEnd@.

data XOrtSite s q where
  XStart :: X (Point q) -> (Point q -> X q) -> XOrtSite From q
  XEnd   :: X (Point q) -> (Point q -> X q) -> XOrtSite To q


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

-- XOrtSite - Dualisable -


type instance Dual (XOrtSite s q) = XOrtSite (Dual s) (Op q)

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

-- coXOrtSite -


-- | to the dual of a @'XOrtSite' __s__ __q__@, with inverse 'coXOrtSiteInv'.

coXOrtSite :: XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite :: forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite (XStart X (Point q)
xp Point q -> X q
xs) = X (Point (Op q))
-> (Point (Op q) -> X (Op q)) -> XOrtSite 'To (Op q)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd X (Point q)
X (Point (Op q))
xp Point q -> X (Op q)
Point (Op q) -> X (Op q)
xs' where xs' :: Point q -> X (Op q)
xs' Point q
p = (q -> Op q) -> X q -> X (Op q)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap q -> Op q
forall x. x -> Op x
Op (Point q -> X q
xs Point q
p)
coXOrtSite (XEnd X (Point q)
xp Point q -> X q
xe)   = X (Point (Op q))
-> (Point (Op q) -> X (Op q)) -> XOrtSite 'From (Op q)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point q)
X (Point (Op q))
xp Point q -> X (Op q)
Point (Op q) -> X (Op q)
xe' where xe' :: Point q -> X (Op q)
xe' Point q
p = (q -> Op q) -> X q -> X (Op q)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap q -> Op q
forall x. x -> Op x
Op (Point q -> X q
xe Point q
p)

-- | from the bidual.

xosFromOpOp :: XOrtSite s (Op (Op q)) -> XOrtSite s q
xosFromOpOp :: forall (s :: Site) q. XOrtSite s (Op (Op q)) -> XOrtSite s q
xosFromOpOp (XStart X (Point (Op (Op q)))
xp Point (Op (Op q)) -> X (Op (Op q))
xs) = X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point q)
X (Point (Op (Op q)))
xp Point q -> X q
xs' where xs' :: Point q -> X q
xs' Point q
p = (Op (Op q) -> q) -> X (Op (Op q)) -> X q
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Op (Op q) -> q
forall x. Op (Op x) -> x
fromOpOp (Point (Op (Op q)) -> X (Op (Op q))
xs Point q
Point (Op (Op q))
p)
xosFromOpOp (XEnd X (Point (Op (Op q)))
xp Point (Op (Op q)) -> X (Op (Op q))
xe)   = X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd X (Point q)
X (Point (Op (Op q)))
xp Point q -> X q
xe' where xe' :: Point q -> X q
xe' Point q
p = (Op (Op q) -> q) -> X (Op (Op q)) -> X q
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Op (Op q) -> q
forall x. Op (Op x) -> x
fromOpOp (Point (Op (Op q)) -> X (Op (Op q))
xe Point q
Point (Op (Op q))
p)

-- | from the dual of a @'Dual' ('XOrtSite' __s__ __q__)@, with inverse 'coXOrtSite'.

coXOrtSiteInv :: Dual (Dual s) :~: s -> Dual (XOrtSite s q) -> XOrtSite s q
coXOrtSiteInv :: forall (s :: Site) q.
(Dual (Dual s) :~: s) -> Dual (XOrtSite s q) -> XOrtSite s q
coXOrtSiteInv Dual (Dual s) :~: s
Refl = XOrtSite s (Op (Op q)) -> XOrtSite s q
forall (s :: Site) q. XOrtSite s (Op (Op q)) -> XOrtSite s q
xosFromOpOp (XOrtSite s (Op (Op q)) -> XOrtSite s q)
-> (XOrtSite (Dual s) (Op q) -> XOrtSite s (Op (Op q)))
-> XOrtSite (Dual s) (Op q)
-> XOrtSite s q
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
. XOrtSite (Dual s) (Op q) -> Dual (XOrtSite (Dual s) (Op q))
XOrtSite (Dual s) (Op q) -> XOrtSite s (Op (Op q))
forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite

instance Dualisable (XOrtSite To q) where
  toDual :: XOrtSite 'To q -> Dual (XOrtSite 'To q)
toDual = XOrtSite 'To q -> Dual (XOrtSite 'To q)
forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite
  fromDual :: Dual (XOrtSite 'To q) -> XOrtSite 'To q
fromDual = (Dual (Dual 'To) :~: 'To)
-> Dual (XOrtSite 'To q) -> XOrtSite 'To q
forall (s :: Site) q.
(Dual (Dual s) :~: s) -> Dual (XOrtSite s q) -> XOrtSite s q
coXOrtSiteInv 'To :~: 'To
Dual (Dual 'To) :~: 'To
forall {k} (a :: k). a :~: a
Refl

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

-- XOrtSite - Validable -


instance Oriented q => Validable (XOrtSite s q) where
  valid :: XOrtSite s q -> Statement
valid (XStart X (Point q)
xp Point q -> X q
xq)
    = X (Point q) -> (Point q -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Point q)
xp
        (\Point q
p
         ->    Point q -> Statement
forall a. Validable a => a -> Statement
valid Point q
p                  
            Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& X q -> (q -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (Point q -> X q
xq Point q
p)
                 (\q
x
                  ->    q -> Statement
forall a. Validable a => a -> Statement
valid q
x
                     Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& (q -> Point q
forall q. Oriented q => q -> Point q
start q
x Point q -> Point q -> Bool
forall a. Eq a => a -> a -> Bool
== Point q
p) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"p"String -> String -> Parameter
:=Point q -> String
forall a. Show a => a -> String
show Point q
p,String
"x"String -> String -> Parameter
:=q -> String
forall a. Show a => a -> String
show q
x]
                 )
        )
  valid xe :: XOrtSite s q
xe@(XEnd X (Point q)
_ Point q -> X q
_) = XOrtSite 'From (Op q) -> Statement
forall a. Validable a => a -> Statement
valid (XOrtSite s q -> Dual (XOrtSite s q)
forall x. Dualisable x => x -> Dual x
toDual XOrtSite s q
xe)

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

-- xosStart -


-- | the random variable of arrows in @__q__@ having all as 'start' the given point.

xosStart :: XOrtSite From q -> Point q -> X q
xosStart :: forall q. XOrtSite 'From q -> Point q -> X q
xosStart (XStart X (Point q)
_ Point q -> X q
xs) = Point q -> X q
xs

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

-- xosEnd -


-- | the random variable of arrows in @__q__@ having all as 'end' the given point.

xosEnd :: XOrtSite To q -> Point q -> X q
xosEnd :: forall q. XOrtSite 'To q -> Point q -> X q
xosEnd (XEnd X (Point q)
_ Point q -> X q
xe) = Point q -> X q
xe

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

-- xosPathMaxAt -


-- | tries to make a path at the given point with maximal length of the given length.

--

-- __Properties__ Let @xPath = 'xosPathMaxAt' xos n x@, then holds:

--

-- (1) If @xos@ matches @'XStart' _ xq@ then for all @p@ in the range of @xPath@ holds:

--

--     (1) @'start' p '==' x@.

--

--     (2) If @'pthLength' p '<' n@ then @xq ('end' p)@ matches 'XEmpty'.

--

-- (2) If @xos@ matches @'XEnd' _ xq@ then for all @p@ in the range of @xPath@ holds:

--

--     (1) @'end' p '==' x@.

--

--     (2) If @'pthLength' p '<' n@ then @xq ('start' p)@ matches 'XEmpty'.

xosPathMaxAt :: Oriented q => XOrtSite s q -> N -> Point q -> X (Path q)
xosPathMaxAt :: forall q (s :: Site).
Oriented q =>
XOrtSite s q -> N -> Point q -> X (Path q)
xosPathMaxAt (XStart X (Point q)
_ Point q -> X q
xq) N
n Point q
s = N -> Point q -> Path q -> X (Path q)
pth N
n Point q
s (Point q -> Path q
forall q. Point q -> Path q
pthOne Point q
s) where

  * :: Path q -> Path q -> Path q
(*) = Path q -> Path q -> Path q
forall q. Oriented q => Path q -> Path q -> Path q
pthMlt
  
  pth :: N -> Point q -> Path q -> X (Path q)
pth N
0 Point q
_ Path q
fs = Path q -> X (Path q)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return Path q
fs  
  pth N
n Point q
s Path q
fs = case Point q -> X q
xq Point q
s of
    X q
XEmpty -> Path q -> X (Path q)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return Path q
fs
    X q
xf     -> X q
xf X q -> (q -> X (Path q)) -> X (Path q)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \q
f -> N -> Point q -> Path q -> X (Path q)
pth (N -> N
forall a. Enum a => a -> a
pred N
n) (q -> Point q
forall q. Oriented q => q -> Point q
end q
f) (q -> Path q
forall {q}. Oriented q => q -> Path q
inj q
f Path q -> Path q -> Path q
* Path q
fs)

  inj :: q -> Path q
inj q
f = Point q -> [q] -> Path q
forall q. Point q -> [q] -> Path q
Path (q -> Point q
forall q. Oriented q => q -> Point q
start q
f) [q
f]
xosPathMaxAt xe :: XOrtSite s q
xe@(XEnd X (Point q)
_ Point q -> X q
_) N
n Point q
e = (Path (Op q) -> Path q) -> X (Path (Op q)) -> X (Path q)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dual (Path q) -> Path q
Path (Op q) -> Path q
forall x. Dualisable x => Dual x -> x
fromDual (X (Path (Op q)) -> X (Path q)) -> X (Path (Op q)) -> X (Path q)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite 'From (Op q) -> N -> Point (Op q) -> X (Path (Op q))
forall q (s :: Site).
Oriented q =>
XOrtSite s q -> N -> Point q -> X (Path q)
xosPathMaxAt (XOrtSite s q -> Dual (XOrtSite s q)
forall x. Dualisable x => x -> Dual x
toDual XOrtSite s q
xe) N
n Point q
Point (Op q)
e

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

-- xosPathMax -


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

xosPathMax :: Oriented q => XOrtSite s q -> N -> X (Path q)
xosPathMax :: forall q (s :: Site). Oriented q => XOrtSite s q -> N -> X (Path q)
xosPathMax xs :: XOrtSite s q
xs@(XStart X (Point q)
xp Point q -> X q
_) N
n = X (Point q)
xp X (Point q) -> (Point q -> X (Path q)) -> X (Path q)
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 q -> N -> Point q -> X (Path q)
forall q (s :: Site).
Oriented q =>
XOrtSite s q -> N -> Point q -> X (Path q)
xosPathMaxAt XOrtSite s q
xs N
n
xosPathMax xe :: XOrtSite s q
xe@(XEnd X (Point q)
_ Point q -> X q
_) N
n    = (Path (Op q) -> Path q) -> X (Path (Op q)) -> X (Path q)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dual (Path q) -> Path q
Path (Op q) -> Path q
forall x. Dualisable x => Dual x -> x
fromDual (X (Path (Op q)) -> X (Path q)) -> X (Path (Op q)) -> X (Path q)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite 'From (Op q) -> N -> X (Path (Op q))
forall q (s :: Site). Oriented q => XOrtSite s q -> N -> X (Path q)
xosPathMax (XOrtSite s q -> Dual (XOrtSite s q)
forall x. Dualisable x => x -> Dual x
toDual XOrtSite s q
xe) N
n

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

-- xStartOrnt -


-- | the @'XOrtSite' 'From'@ for @'Orientation' __p__@ of the given random variable.

xStartOrnt :: X p -> XOrtSite From (Orientation p)
xStartOrnt :: forall p. X p -> XOrtSite 'From (Orientation p)
xStartOrnt X p
xp = X (Point (Orientation p))
-> (Point (Orientation p) -> X (Orientation p))
-> XOrtSite 'From (Orientation p)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X p
X (Point (Orientation p))
xp p -> X (Orientation p)
Point (Orientation p) -> X (Orientation p)
xq where xq :: p -> X (Orientation p)
xq p
s = X p
xp X p -> (p -> X (Orientation p)) -> X (Orientation p)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Orientation p -> X (Orientation p)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Orientation p -> X (Orientation p))
-> (p -> Orientation p) -> p -> X (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
. (p
sp -> p -> Orientation p
forall p. p -> p -> Orientation p
:>)

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

-- xEndOrnt -


-- | the @'XOrtSite' 'To'@ of @'Orientation' __p__@ of the given random variable.

xEndOrnt :: X p -> XOrtSite To (Orientation p)
xEndOrnt :: forall p. X p -> XOrtSite 'To (Orientation p)
xEndOrnt X p
xp = X (Point (Orientation p))
-> (Point (Orientation p) -> X (Orientation p))
-> XOrtSite 'To (Orientation p)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd X p
X (Point (Orientation p))
xp p -> X (Orientation p)
Point (Orientation p) -> X (Orientation p)
xq where xq :: p -> X (Orientation p)
xq p
e = X p
xp X p -> (p -> X (Orientation p)) -> X (Orientation p)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Orientation p -> X (Orientation p)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Orientation p -> X (Orientation p))
-> (p -> Orientation p) -> p -> X (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
. (p -> p -> Orientation p
forall p. p -> p -> Orientation p
:>p
e)

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

-- XStandardOrtSite -


-- | standard random variable for 'XOrtSite'.

class XStandardOrtSite s a where
  xStandardOrtSite :: XOrtSite s a

instance XStandard p => XStandardOrtSite To (Orientation p) where
  xStandardOrtSite :: XOrtSite 'To (Orientation p)
xStandardOrtSite = X p -> XOrtSite 'To (Orientation p)
forall p. X p -> XOrtSite 'To (Orientation p)
xEndOrnt X p
forall x. XStandard x => X x
xStandard

instance XStandard p => XStandardOrtSite From (Orientation p) where
  xStandardOrtSite :: XOrtSite 'From (Orientation p)
xStandardOrtSite = X p -> XOrtSite 'From (Orientation p)
forall p. X p -> XOrtSite 'From (Orientation p)
xStartOrnt X p
forall x. XStandard x => X x
xStandard

instance XStandardOrtSite From a => XStandardOrtSite To (Op a) where
  xStandardOrtSite :: XOrtSite 'To (Op a)
xStandardOrtSite = XOrtSite 'From a -> XOrtSite 'To (Op a)
forall a. XOrtSite 'From a -> XOrtSite 'To (Op a)
co XOrtSite 'From a
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite where
    co :: XOrtSite From a -> XOrtSite To (Op a)
    co :: forall a. XOrtSite 'From a -> XOrtSite 'To (Op a)
co = XOrtSite 'From a -> Dual (XOrtSite 'From a)
XOrtSite 'From a -> XOrtSite 'To (Op a)
forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite

instance XStandardOrtSite To a => XStandardOrtSite From (Op a) where
  xStandardOrtSite :: XOrtSite 'From (Op a)
xStandardOrtSite = XOrtSite 'To a -> XOrtSite 'From (Op a)
forall a. XOrtSite 'To a -> XOrtSite 'From (Op a)
co XOrtSite 'To a
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite where
    co :: XOrtSite To a -> XOrtSite From (Op a)
    co :: forall a. XOrtSite 'To a -> XOrtSite 'From (Op a)
co = XOrtSite 'To a -> Dual (XOrtSite 'To a)
XOrtSite 'To a -> XOrtSite 'From (Op a)
forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite

instance XStandardOrtSite To N where
  xStandardOrtSite :: XOrtSite 'To N
xStandardOrtSite = X (Point N) -> (Point N -> X N) -> XOrtSite 'To N
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd (() -> X ()
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (X N -> () -> X N
forall b a. b -> a -> b
const X N
xN)

instance XStandardOrtSite From N where
  xStandardOrtSite :: XOrtSite 'From N
xStandardOrtSite = X (Point N) -> (Point N -> X N) -> XOrtSite 'From N
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart (() -> X ()
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (X N -> () -> X N
forall b a. b -> a -> b
const X N
xN)

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

-- XStandardOrtSiteTo -


-- | standard random variable for @'XOrtSite' 'To'@, helper class to avoid undecidable instances.

class XStandardOrtSite To a => XStandardOrtSiteTo a

instance XStandard p => XStandardOrtSiteTo (Orientation p)
instance XStandardOrtSiteFrom x => XStandardOrtSiteTo (Op x)

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

-- XStandardOrtSiteFrom -


-- | standard random variable for @'XOrtSite' 'From'@, helper class to avoid undecidable instances.

class XStandardOrtSite From a => XStandardOrtSiteFrom a

instance XStandard p => XStandardOrtSiteFrom (Orientation p)
instance XStandardOrtSiteTo x => XStandardOrtSiteFrom (Op x)

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

-- xosIdTo -


-- | to 'Id' promoted random variable.

xosIdTo :: XOrtSite To x -> XOrtSite To (Id x)
xosIdTo :: forall x. XOrtSite 'To x -> XOrtSite 'To (Id x)
xosIdTo (XEnd X (Point x)
xp Point x -> X x
xa) = X (Point (Id x))
-> (Point (Id x) -> X (Id x)) -> XOrtSite 'To (Id x)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd X (Point x)
X (Point (Id x))
xp ((x -> Id x) -> X x -> X (Id x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> Id x
forall x. x -> Id x
Id (X x -> X (Id x)) -> (Point x -> X x) -> Point x -> X (Id 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
. Point x -> X x
xa)

instance XStandardOrtSite To x => XStandardOrtSite To (Id x) where
  xStandardOrtSite :: XOrtSite 'To (Id x)
xStandardOrtSite = XOrtSite 'To x -> XOrtSite 'To (Id x)
forall x. XOrtSite 'To x -> XOrtSite 'To (Id x)
xosIdTo XOrtSite 'To x
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite
  
instance XStandardOrtSiteTo x => XStandardOrtSiteTo (Id x)

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

-- xosIdFrom


-- | to 'Id' promoted random variable.

xosIdFrom :: XOrtSite From x -> XOrtSite From (Id x)
xosIdFrom :: forall x. XOrtSite 'From x -> XOrtSite 'From (Id x)
xosIdFrom (XStart X (Point x)
xp Point x -> X x
xa) = X (Point (Id x))
-> (Point (Id x) -> X (Id x)) -> XOrtSite 'From (Id x)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point x)
X (Point (Id x))
xp ((x -> Id x) -> X x -> X (Id x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> Id x
forall x. x -> Id x
Id (X x -> X (Id x)) -> (Point x -> X x) -> Point x -> X (Id 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
. Point x -> X x
xa)
  
instance XStandardOrtSite From x => XStandardOrtSite From (Id x) where
  xStandardOrtSite :: XOrtSite 'From (Id x)
xStandardOrtSite = XOrtSite 'From x -> XOrtSite 'From (Id x)
forall x. XOrtSite 'From x -> XOrtSite 'From (Id x)
xosIdFrom XOrtSite 'From x
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite
  
instance XStandardOrtSiteFrom x => XStandardOrtSiteFrom (Id x)

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

-- XStandardOrtSite t U -


-- | to 'U' promoted random variable.

xosUFrom :: X x -> XOrtSite From (U x)
xosUFrom :: forall x. X x -> XOrtSite 'From (U x)
xosUFrom X x
xx = X (Point (U x)) -> (Point (U x) -> X (U x)) -> XOrtSite 'From (U x)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart (() -> X ()
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (X (U x) -> () -> X (U x)
forall b a. b -> a -> b
const ((x -> U x) -> X x -> X (U x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> U x
forall x. x -> U x
U X x
xx))

-- | to 'Id' promoted random variable.

xosUTo :: X x -> XOrtSite To (U x)
xosUTo :: forall x. X x -> XOrtSite 'To (U x)
xosUTo X x
xx = X (Point (U x)) -> (Point (U x) -> X (U x)) -> XOrtSite 'To (U x)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd (() -> X ()
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (X (U x) -> () -> X (U x)
forall b a. b -> a -> b
const ((x -> U x) -> X x -> X (U x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> U x
forall x. x -> U x
U X x
xx))

instance XStandard x => XStandardOrtSite To (U x) where
  xStandardOrtSite :: XOrtSite 'To (U x)
xStandardOrtSite = X x -> XOrtSite 'To (U x)
forall x. X x -> XOrtSite 'To (U x)
xosUTo X x
forall x. XStandard x => X x
xStandard

instance XStandard x => XStandardOrtSite From (U x) where
  xStandardOrtSite :: XOrtSite 'From (U x)
xStandardOrtSite = X x -> XOrtSite 'From (U x)
forall x. X x -> XOrtSite 'From (U x)
xosUFrom X x
forall x. XStandard x => X x
xStandard
  
instance XStandard x => XStandardOrtSiteTo (U x)
instance XStandard x => XStandardOrtSiteFrom (U x)

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

-- OrtSiteX -


-- | type for 'Oriented' structures admitting 'XStandardOrtSiteTo' and 'XStandardOrtSiteFrom'.

--

-- __Note__ The main point is that @'TransformableG' 'Op' 'OrtSiteX' 'OrtSiteX'@ holds!

data OrtSiteX

type instance Structure OrtSiteX x
  = ( Oriented x
    , XStandardOrtSiteTo x
    , XStandardOrtSiteFrom x
    )

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

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

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

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

instance TransformableGRefl Op OrtSiteX

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

-- XOrtOrientation -


-- | random variable of arrows given by an orientation.

--

-- __Properties__ Let @'XOrtOrientation' xo xArrow@ be in @'XOrtOrientation' __q__@ for a

-- 'Oriented' structure @__q__@, then holds: For all @o@ in @'Orientation' __q__@ and @x@ in the

-- range of @xArrow o@ holds: @'orientation' x '==' o@.

--

-- __Note__ The random variable @xo@ should have a bias to non trivial random variables

-- @xo '>>=' xArrow@ and as such the range of @xo@ should be included in one connection component

-- of @__q__@.

data XOrtOrientation q
  = XOrtOrientation (X (Orientation (Point q))) (Orientation (Point q) -> X q)

instance Oriented q => Validable (XOrtOrientation q) where
  valid :: XOrtOrientation q -> Statement
valid x :: XOrtOrientation q
x@(XOrtOrientation X (Orientation (Point q))
xo Orientation (Point q) -> X q
xq) = String -> Label
Label (TypeRep -> String
forall a. Show a => a -> String
show (TypeRep -> String) -> TypeRep -> String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtOrientation q -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf XOrtOrientation q
x) Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ X (Orientation (Point q)) -> Statement
forall a. Validable a => a -> Statement
valid X (Orientation (Point q))
xo
        , X (Orientation (Point q))
-> (Orientation (Point q) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Orientation (Point q))
xo
            (\Orientation (Point q)
o -> X q -> (q -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (Orientation (Point q) -> X q
xq Orientation (Point q)
o)
              (\q
q -> [Statement] -> Statement
And [ q -> Statement
forall a. Validable a => a -> Statement
valid q
q
                         , (q -> Orientation (Point q)
forall q. Oriented q => q -> Orientation (Point q)
orientation q
q Orientation (Point q) -> Orientation (Point q) -> Bool
forall a. Eq a => a -> a -> Bool
== Orientation (Point q)
o)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"o"String -> String -> Parameter
:=Orientation (Point q) -> String
forall a. Show a => a -> String
show Orientation (Point q)
o,String
"q"String -> String -> Parameter
:=q -> String
forall a. Show a => a -> String
show q
q]
                         ]
              )
            )
        ]

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

-- XOrtOrientation - Dual -


type instance Dual (XOrtOrientation q) = XOrtOrientation (Op q)

-- | to the dual.

coXOrtOrientation :: XOrtOrientation q -> Dual (XOrtOrientation q)
coXOrtOrientation :: forall q. XOrtOrientation q -> Dual (XOrtOrientation q)
coXOrtOrientation (XOrtOrientation X (Orientation (Point q))
xo Orientation (Point q) -> X q
xq) = X (Orientation (Point (Op q)))
-> (Orientation (Point (Op q)) -> X (Op q))
-> XOrtOrientation (Op q)
forall q.
X (Orientation (Point q))
-> (Orientation (Point q) -> X q) -> XOrtOrientation q
XOrtOrientation X (Orientation (Point q))
X (Orientation (Point (Op q)))
xo' Orientation (Point q) -> X (Op q)
Orientation (Point (Op q)) -> X (Op q)
xq' where
  xo' :: X (Orientation (Point q))
xo' = (Orientation (Point q) -> Orientation (Point q))
-> X (Orientation (Point q)) -> X (Orientation (Point q))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Orientation (Point q) -> Orientation (Point q)
forall p. Orientation p -> Orientation p
opposite X (Orientation (Point q))
xo
  xq' :: Orientation (Point q) -> X (Op q)
xq' Orientation (Point q)
o' = (q -> Op q) -> X q -> X (Op q)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 q -> Op q
forall x. x -> Op x
Op (Orientation (Point q) -> X q
xq (Orientation (Point q) -> Orientation (Point q)
forall p. Orientation p -> Orientation p
opposite Orientation (Point q)
o'))

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

-- xoOrientation -


-- | the underlying random variable of orientations.

xoOrientation :: XOrtOrientation q -> X (Orientation (Point q))
xoOrientation :: forall q. XOrtOrientation q -> X (Orientation (Point q))
xoOrientation (XOrtOrientation X (Orientation (Point q))
xo Orientation (Point q) -> X q
_) = X (Orientation (Point q))
xo

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

-- xoArrow -


-- | the underlying random variable of arrow given by the orientation.

xoArrow :: XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow :: forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow (XOrtOrientation X (Orientation (Point q))
_ Orientation (Point q) -> X q
xq) = Orientation (Point q) -> X q
xq

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

-- xoPoint -


-- | the underlying random variable of points, i.e. the union of the induced 'start' and 'end'

-- random variable of 'xoOrientation'.

xoPoint :: Oriented q => XOrtOrientation q -> X (Point q)
xoPoint :: forall q. Oriented q => XOrtOrientation q -> X (Point q)
xoPoint (XOrtOrientation X (Orientation (Point q))
xo Orientation (Point q) -> X q
_) = (Orientation (Point q) -> Point q)
-> X (Orientation (Point q)) -> X (Point q)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Orientation (Point q) -> Point q
Orientation (Point q) -> Point (Orientation (Point q))
forall q. Oriented q => q -> Point q
start X (Orientation (Point q))
xo X (Point q) -> X (Point q) -> X (Point q)
forall a. X a -> X a -> X a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Orientation (Point q) -> Point q)
-> X (Orientation (Point q)) -> X (Point q)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Orientation (Point q) -> Point q
Orientation (Point q) -> Point (Orientation (Point q))
forall q. Oriented q => q -> Point q
end X (Orientation (Point q))
xo

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

-- xoTo -


-- | the induced @'XOrtSite' 'To'@

xoTo :: Oriented q => XOrtOrientation q -> XOrtSite To q
xoTo :: forall q. Oriented q => XOrtOrientation q -> XOrtSite 'To q
xoTo (XOrtOrientation X (Orientation (Point q))
xo Orientation (Point q) -> X q
xq) = X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd X (Point q)
X (Point (Orientation (Point q)))
xp Point q -> X q
xTo where
  xp :: X (Point (Orientation (Point q)))
xp    = (Orientation (Point q) -> Point (Orientation (Point q)))
-> X (Orientation (Point q)) -> X (Point (Orientation (Point q)))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Orientation (Point q) -> Point (Orientation (Point q))
forall q. Oriented q => q -> Point q
end X (Orientation (Point q))
xo
  xTo :: Point q -> X q
xTo Point q
e = (Orientation (Point q) -> Point (Orientation (Point q)))
-> X (Orientation (Point q)) -> X (Point (Orientation (Point q)))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Orientation (Point q) -> Point (Orientation (Point q))
forall q. Oriented q => q -> Point q
start X (Orientation (Point q))
xo X (Point (Orientation (Point q)))
-> (Point (Orientation (Point q)) -> X q) -> X q
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Orientation (Point q) -> X q
xq (Orientation (Point q) -> X q)
-> (Point q -> Orientation (Point q)) -> Point q -> X q
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 q -> Point q -> Orientation (Point q)
forall p. p -> p -> Orientation p
:>Point q
e)

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

-- xoFrom -


-- | the induced @'XOrtSite' 'From'@.

xoFrom :: Oriented q => XOrtOrientation q -> XOrtSite From q
xoFrom :: forall q. Oriented q => XOrtOrientation q -> XOrtSite 'From q
xoFrom XOrtOrientation q
xo = (Dual (Dual 'From) :~: 'From)
-> Dual (XOrtSite 'From q) -> XOrtSite 'From q
forall (s :: Site) q.
(Dual (Dual s) :~: s) -> Dual (XOrtSite s q) -> XOrtSite s q
coXOrtSiteInv 'From :~: 'From
Dual (Dual 'From) :~: 'From
forall {k} (a :: k). a :~: a
Refl (XOrtSite 'To (Op q) -> XOrtSite 'From q)
-> XOrtSite 'To (Op q) -> XOrtSite 'From q
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtOrientation (Op q) -> XOrtSite 'To (Op q)
forall q. Oriented q => XOrtOrientation q -> XOrtSite 'To q
xoTo (XOrtOrientation (Op q) -> XOrtSite 'To (Op q))
-> XOrtOrientation (Op q) -> XOrtSite 'To (Op q)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtOrientation q -> Dual (XOrtOrientation q)
forall q. XOrtOrientation q -> Dual (XOrtOrientation q)
coXOrtOrientation XOrtOrientation q
xo 

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

-- xoTtl -


-- | random variable of @'XOrtOrientation' __q__@ for a total @__q__@.

xoTtl :: Total q => X q -> XOrtOrientation q
xoTtl :: forall q. Total q => X q -> XOrtOrientation q
xoTtl X q
xx = X (Orientation (Point q))
-> (Orientation (Point q) -> X q) -> XOrtOrientation q
forall q.
X (Orientation (Point q))
-> (Orientation (Point q) -> X q) -> XOrtOrientation q
XOrtOrientation X (Orientation (Point q))
xo Orientation (Point q) -> X q
xq where
  xo :: X (Orientation (Point q))
xo = Orientation (Point q) -> X (Orientation (Point q))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Point q
forall s. Singleton s => s
unit Point q -> Point q -> Orientation (Point q)
forall p. p -> p -> Orientation p
:> Point q
forall s. Singleton s => s
unit)
  xq :: Orientation (Point q) -> X q
xq = X q -> Orientation (Point q) -> X q
forall b a. b -> a -> b
const X q
xx

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

-- xoOrnt -


-- | the induced random variable of @'Orientation' __q__@.

xoOrnt :: X p -> XOrtOrientation (Orientation p)
xoOrnt :: forall p. X p -> XOrtOrientation (Orientation p)
xoOrnt X p
xp = X (Orientation (Point (Orientation p)))
-> (Orientation (Point (Orientation p)) -> X (Orientation p))
-> XOrtOrientation (Orientation p)
forall q.
X (Orientation (Point q))
-> (Orientation (Point q) -> X q) -> XOrtOrientation q
XOrtOrientation X (Orientation p)
X (Orientation (Point (Orientation p)))
xo Orientation p -> X (Orientation p)
Orientation (Point (Orientation p)) -> X (Orientation p)
forall a. a -> X a
xq where
  xo :: X (Orientation p)
xo = ((p, p) -> Orientation p) -> X (p, p) -> X (Orientation p)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 ((p -> p -> Orientation p) -> (p, p) -> Orientation p
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry p -> p -> Orientation p
forall p. p -> p -> Orientation p
(:>)) (X (p, p) -> X (Orientation p)) -> X (p, p) -> X (Orientation p)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X p -> X p -> X (p, p)
forall a b. X a -> X b -> X (a, b)
xTupple2 X p
xp X p
xp
  xq :: a -> X a
xq = a -> X a
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return

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

-- XStandardOrtOrientation -


-- | standard random variable for 'XOrtOrientation'.

class XStandardOrtOrientation q where
  xStandardOrtOrientation :: XOrtOrientation q

instance XStandard p => XStandardOrtOrientation (Orientation p) where
  xStandardOrtOrientation :: XOrtOrientation (Orientation p)
xStandardOrtOrientation = X p -> XOrtOrientation (Orientation p)
forall p. X p -> XOrtOrientation (Orientation p)
xoOrnt X p
forall x. XStandard x => X x
xStandard

instance XStandardOrtOrientation Z where
  xStandardOrtOrientation :: XOrtOrientation Z
xStandardOrtOrientation = X (Orientation (Point Z))
-> (Orientation (Point Z) -> X Z) -> XOrtOrientation Z
forall q.
X (Orientation (Point q))
-> (Orientation (Point q) -> X q) -> XOrtOrientation q
XOrtOrientation (Orientation () -> X (Orientation ())
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (()() -> () -> Orientation ()
forall p. p -> p -> Orientation p
:>())) (X Z -> Orientation () -> X Z
forall b a. b -> a -> b
const X Z
forall x. XStandard x => X x
xStandard)

instance XStandardOrtOrientation x => XStandardOrtOrientation (Op x) where
  xStandardOrtOrientation :: XOrtOrientation (Op x)
xStandardOrtOrientation = X (Orientation (Point (Op x)))
-> (Orientation (Point (Op x)) -> X (Op x))
-> XOrtOrientation (Op x)
forall q.
X (Orientation (Point q))
-> (Orientation (Point q) -> X q) -> XOrtOrientation q
XOrtOrientation X (Orientation (Point x))
X (Orientation (Point (Op x)))
xo' Orientation (Point x) -> X (Op x)
Orientation (Point (Op x)) -> X (Op x)
xq' where
    XOrtOrientation X (Orientation (Point x))
xo Orientation (Point x) -> X x
xq = XOrtOrientation x
forall q. XStandardOrtOrientation q => XOrtOrientation q
xStandardOrtOrientation
    xo' :: X (Orientation (Point x))
xo'   = (Orientation (Point x) -> Orientation (Point x))
-> X (Orientation (Point x)) -> X (Orientation (Point x))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Orientation (Point x) -> Orientation (Point x)
forall p. Orientation p -> Orientation p
opposite X (Orientation (Point x))
xo
    xq' :: Orientation (Point x) -> X (Op x)
xq' Orientation (Point x)
o = Orientation (Point x) -> X x
xq (Orientation (Point x) -> Orientation (Point x)
forall p. Orientation p -> Orientation p
opposite Orientation (Point x)
o) X x -> (x -> X (Op x)) -> X (Op x)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Op x -> X (Op x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Op x -> X (Op x)) -> (x -> Op x) -> x -> X (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
. x -> Op x
forall x. x -> Op x
Op

instance XStandard x => XStandardOrtOrientation (U x) where
  xStandardOrtOrientation :: XOrtOrientation (U x)
xStandardOrtOrientation = X (Orientation (Point (U x)))
-> (Orientation (Point (U x)) -> X (U x)) -> XOrtOrientation (U x)
forall q.
X (Orientation (Point q))
-> (Orientation (Point q) -> X q) -> XOrtOrientation q
XOrtOrientation X (Orientation ())
X (Orientation (Point (U x)))
xo Orientation () -> X (U x)
Orientation (Point (U x)) -> X (U x)
forall {x} {p}. XStandard x => p -> X (U x)
xq where
    xo :: X (Orientation ())
xo = Orientation () -> X (Orientation ())
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (()() -> () -> Orientation ()
forall p. p -> p -> Orientation p
:>())
    xq :: p -> X (U x)
xq p
_ = (x -> U x) -> X x -> X (U x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> U x
forall x. x -> U x
U X x
forall x. XStandard x => X x
xStandard
    
--------------------------------------------------------------------------------

-- xooId -


-- | to 'Id' promoted random variable.

xooId :: XOrtOrientation x -> XOrtOrientation (Id x)
xooId :: forall x. XOrtOrientation x -> XOrtOrientation (Id x)
xooId (XOrtOrientation X (Orientation (Point x))
xo Orientation (Point x) -> X x
xa) = X (Orientation (Point (Id x)))
-> (Orientation (Point (Id x)) -> X (Id x))
-> XOrtOrientation (Id x)
forall q.
X (Orientation (Point q))
-> (Orientation (Point q) -> X q) -> XOrtOrientation q
XOrtOrientation X (Orientation (Point x))
X (Orientation (Point (Id x)))
xo ((x -> Id x) -> X x -> X (Id x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> Id x
forall x. x -> Id x
Id (X x -> X (Id x))
-> (Orientation (Point x) -> X x)
-> Orientation (Point x)
-> X (Id 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
. Orientation (Point x) -> X x
xa)

instance XStandardOrtOrientation x => XStandardOrtOrientation (Id x) where
  xStandardOrtOrientation :: XOrtOrientation (Id x)
xStandardOrtOrientation = XOrtOrientation x -> XOrtOrientation (Id x)
forall x. XOrtOrientation x -> XOrtOrientation (Id x)
xooId XOrtOrientation x
forall q. XStandardOrtOrientation q => XOrtOrientation q
xStandardOrtOrientation