{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Structure.Oriented.Definition
-- Description : definition of oriented structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- definition of 'Oriented' structures.
module OAlg.Structure.Oriented.Definition
  (
    -- * Oriented
    Oriented(..), Total, EntityPoint, OrdPoint, isEndo, isEndoAt
  , OS, Ort, structOrtOp, ForgetfulOrt

    -- * Transposable
  , TransposableOriented

    -- * Orientation
  , Orientation(..), opposite

    -- * Path
  , Path(..), pthLength, pthOne, pthMlt

    -- * X
    -- ** Site
  , XOrtSite(..), XStandardOrtSite(..)
  , XStandardOrtSiteTo, XStandardOrtSiteFrom
  , coXOrtSite, coXOrtSiteInv, xosFromOpOp
  , xosStart, xosEnd
  , xosPathMaxAt, xosPathMax

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

    -- ** Orientation
  , XStandardPoint
  , xStartOrnt, xEndOrnt
  
  )
  where

import Control.Monad
import Control.Applicative ((<|>))
import Data.Typeable
import Data.Foldable
import Data.List (map,reverse,(++))

import OAlg.Prelude

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

import OAlg.Category.Unify

import OAlg.Structure.Exception

--------------------------------------------------------------------------------
-- Orientation -
infix 5 :>
  
-- | orientation given by the start point as its first component and the end point as its
--   second.
--
--  __Property__ For all @o@ in __@'Orientation' p@__ holds:
--  @o '==' 'start' o ':>' 'end' o@.
--
--  __Note__ As 'Orientation's are instances of almost all algebraic structures
--  defined here, they serve as a /proof/ that this structures are instanceable.
data Orientation p = p :> p deriving (Int -> Orientation p -> ShowS
forall p. Show p => Int -> Orientation p -> ShowS
forall p. Show p => [Orientation p] -> ShowS
forall p. Show p => Orientation p -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Orientation p] -> ShowS
$cshowList :: forall p. Show p => [Orientation p] -> ShowS
show :: Orientation p -> String
$cshow :: forall p. Show p => Orientation p -> String
showsPrec :: Int -> Orientation p -> ShowS
$cshowsPrec :: forall p. Show p => Int -> Orientation p -> ShowS
Show,Orientation p -> Orientation p -> Bool
forall p. Eq p => Orientation p -> Orientation p -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Orientation p -> Orientation p -> Bool
$c/= :: forall p. Eq p => Orientation p -> Orientation p -> Bool
== :: Orientation p -> Orientation p -> Bool
$c== :: forall p. Eq p => Orientation p -> Orientation p -> Bool
Eq,Orientation p -> Orientation p -> Bool
Orientation p -> Orientation p -> Ordering
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 {p}. Ord p => Eq (Orientation p)
forall p. Ord p => Orientation p -> Orientation p -> Bool
forall p. Ord p => Orientation p -> Orientation p -> Ordering
forall p. Ord p => Orientation p -> Orientation p -> Orientation p
min :: Orientation p -> Orientation p -> Orientation p
$cmin :: forall p. Ord p => Orientation p -> Orientation p -> Orientation p
max :: Orientation p -> Orientation p -> Orientation p
$cmax :: forall p. Ord p => Orientation p -> Orientation p -> Orientation p
>= :: Orientation p -> Orientation p -> Bool
$c>= :: forall p. Ord p => Orientation p -> Orientation p -> Bool
> :: Orientation p -> Orientation p -> Bool
$c> :: forall p. Ord p => Orientation p -> Orientation p -> Bool
<= :: Orientation p -> Orientation p -> Bool
$c<= :: forall p. Ord p => Orientation p -> Orientation p -> Bool
< :: Orientation p -> Orientation p -> Bool
$c< :: forall p. Ord p => Orientation p -> Orientation p -> Bool
compare :: Orientation p -> Orientation p -> Ordering
$ccompare :: forall p. Ord p => Orientation p -> Orientation p -> Ordering
Ord)

instance Validable p => Validable (Orientation p) where
  valid :: Orientation p -> Statement
valid (p
s :> p
e) = [Statement] -> Statement
And [forall a. Validable a => a -> Statement
valid p
s,forall a. Validable a => a -> Statement
valid p
e]

instance Entity p => Entity (Orientation p)

instance Singleton u => Singleton (Orientation u) where
  unit :: Orientation u
unit = forall s. Singleton s => s
unit forall p. p -> p -> Orientation p
:> forall s. Singleton s => s
unit

instance Functor Orientation where
  fmap :: forall a b. (a -> b) -> Orientation a -> Orientation b
fmap a -> b
f (a
a :> a
b) = a -> b
f a
a forall p. p -> p -> Orientation p
:> a -> b
f a
b

instance XStandard p => XStandard (Orientation p) where
  xStandard :: X (Orientation p)
xStandard = forall a b. X a -> X b -> X (a, b)
xTupple2 forall x. XStandard x => X x
xStandard forall x. XStandard x => X x
xStandard forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall p. p -> p -> Orientation p
(:>)

--------------------------------------------------------------------------------
-- opposite -

-- | the opposite orientation.
opposite :: Orientation p -> Orientation p
opposite :: forall p. Orientation p -> Orientation p
opposite (p
s:>p
e) = p
eforall p. p -> p -> Orientation p
:>p
s

--------------------------------------------------------------------------------
-- OS -

-- | as @'Orientation' p@ is an instance of almost every structured class it
--   serves as a standard type for validating.
type OS = Orientation Symbol

--------------------------------------------------------------------------------
-- Oriented -

-- | types with a 'Oriented' structure. The values of an 'Oriented' structure will
-- be called __/arrows/__ and the values of the associated 'Point' type __/points/__. To each
-- arrow there is a __/'start'/__ and a __/'end'/__ point assigned.
--
-- __Property__ Let __@q@__ be a type instance of the class 'Oriented', then holds:
--
-- (1) #Ort1#For all @a@ in __@q@__ holds: @'orientation' a '==' 'start' a ':>' 'end' a@.
--
-- __Note__
--
-- (1) If the types @__q__@ and @'Point' __q__@ are interpreted as sets
-- @__A__@ and @__P__@ and 'start', 'end' as functions from @__A__@ to @__P__@
-- then this structure forms a __/quiver/__ with __/arrows/__ in @__A__@
-- and __/points/__ in @__P__@.
-- 
-- (2) 'Morphism's can be interpreted as 'Oriented' structures via 'SomeMorphism'.
-- The bad thing about this is that we lose the check for /composability/ of two
-- 'Morphism's given by the type checker, but we gain all the functionality of
-- 'Oriented' structures, i.e we can define homomorphisms,
-- limits etc on 'Morphism's.
class (Entity q, Entity (Point q)) => Oriented q where
  {-# MINIMAL orientation | (start,end) #-}
  
  -- | the associated type of points.
  type Point q
  
  -- | the orientation of an arrow.
  orientation :: q -> Orientation (Point q)
  orientation q
a = forall q. Oriented q => q -> Point q
start q
a forall p. p -> p -> Orientation p
:> forall q. Oriented q => q -> Point q
end q
a

  -- | the start point of an arrow.
  start :: q -> Point q
  start q
a = Point q
s where Point q
s :> Point q
_ = forall q. Oriented q => q -> Orientation (Point q)
orientation q
a

  -- | the end point of an arrow.
  end :: q -> Point q
  end q
a = Point q
e where Point q
_ :> Point q
e = forall q. Oriented q => q -> Orientation (Point q)
orientation q
a

--------------------------------------------------------------------------------
-- isEndo -

-- | check for being an endo.
--
--  __Definition__ Let @__q__@ be a 'Oriented' structure, then an arrow @a@ in @__q__@
--  is called __/endo/__ if and only if @'start' a '==' 'end' a@.
isEndo :: Oriented q => q -> Bool
isEndo :: forall q. Oriented q => q -> Bool
isEndo q
a = forall q. Oriented q => q -> Point q
start q
a forall a. Eq a => a -> a -> Bool
== forall q. Oriented q => q -> Point q
end q
a

--------------------------------------------------------------------------------
-- isEndoAt -

-- | check for being an endo at the given point.
isEndoAt :: Oriented a => Point a -> a -> Bool
isEndoAt :: forall a. Oriented a => Point a -> a -> Bool
isEndoAt Point a
p a
a = forall q. Oriented q => q -> Orientation (Point q)
orientation a
a forall a. Eq a => a -> a -> Bool
== Point a
p forall p. p -> p -> Orientation p
:> Point a
p

--------------------------------------------------------------------------------
-- Oriented - Instance -

instance Oriented () where
  type Point () = ()
  orientation :: () -> Orientation (Point ())
orientation ()
_ = ()forall p. p -> p -> Orientation p
:>()

instance Oriented Int where
  type Point Int = ()
  orientation :: Int -> Orientation (Point Int)
orientation Int
_ = ()forall p. p -> p -> Orientation p
:>()
  
instance Oriented Integer where
  type Point Integer = ()
  orientation :: Integer -> Orientation (Point Integer)
orientation Integer
_ = ()forall p. p -> p -> Orientation p
:>()
  
instance Oriented N where
  type Point N = ()
  orientation :: N -> Orientation (Point N)
orientation N
_ = ()forall p. p -> p -> Orientation p
:>()

instance Oriented Z where
  type Point Z = ()
  orientation :: Z -> Orientation (Point Z)
orientation Z
_ = ()forall p. p -> p -> Orientation p
:>()

instance Oriented Q where
  type Point Q = ()
  orientation :: Q -> Orientation (Point Q)
orientation Q
_ = ()forall p. p -> p -> Orientation p
:>()

instance Entity p => Oriented (Orientation p) where
  type Point (Orientation p) = p
  orientation :: Orientation p -> Orientation (Point (Orientation p))
orientation = forall x. x -> x
id

instance Oriented q => Oriented (Op q) where
  type Point (Op q) = Point q
  orientation :: Op q -> Orientation (Point (Op q))
orientation (Op q
a) = forall p. Orientation p -> Orientation p
opposite (forall q. Oriented q => q -> Orientation (Point q)
orientation q
a)
  
instance (EmbeddableMorphismTyp m, Entity2 m) => Oriented (SomeMorphism m) where
  type Point (SomeMorphism m) = SomeObjectClass m
  start :: SomeMorphism m -> Point (SomeMorphism m)
start (SomeMorphism m x y
f) = forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain m x y
f)
  end :: SomeMorphism m -> Point (SomeMorphism m)
end (SomeMorphism m x y
f) = forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range m x y
f)
  
--------------------------------------------------------------------------------
-- TransposableOriented -

-- | transposable oriented structures.
--
--  __Property__ Let @__q__@ be a 'TransposableOriented' structure, then holds:
--  For all @a@ in @__q__@ holds:
--  @'orientation' ('transpose' a) '==' 'opposite' ('orientation' a)@.
class (Transposable q, Oriented q) => TransposableOriented q

instance Transposable (Orientation p) where
  transpose :: Orientation p -> Orientation p
transpose = forall p. Orientation p -> Orientation p
opposite
instance Entity p => TransposableOriented (Orientation p)

instance TransposableOriented N
instance TransposableOriented Z
instance TransposableOriented Q
--------------------------------------------------------------------------------
-- Path -

-- | a path in a 'Oriented' structure @__q__@ starting at a given point.
--
-- __Definition__ Let @__q__@ be a 'Oriented' structure and @p = 'Path' s [a 0..a (n-1)]@ a
-- path in @__q__@, then @p@ is 'valid' if and only if
--
-- (1) @s@ is 'valid' and @a i@ are 'valid' for all @i = 0..n-1@.
--
-- (2) @'start' (a (n-1)) '==' s@ and @'start' (a i) '==' 'end' (a (n+1))@ for all @i = 0..n-2@.
--
-- furthermore @n@ is called the __/length/__ of @p@.
--
-- __Note__ Paths admit a canonical embedding in to 'OAlg.Entity.Product.Product'.
data Path q = Path (Point q) [q]

deriving instance Oriented q => Show (Path q)
deriving instance Oriented q => Eq (Path q)

instance Foldable Path where
  foldr :: forall a b. (a -> b -> b) -> b -> Path a -> b
foldr a -> b -> b
op b
b (Path Point a
_ [a]
fs) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
op b
b [a]
fs 

instance Oriented q => Validable (Path q) where
  valid :: Path q -> Statement
valid (Path Point q
s [])     = forall a. Validable a => a -> Statement
valid Point q
s
  valid (Path Point q
s (q
f:[q]
gs)) = forall a. Validable a => a -> Statement
valid Point q
s forall b. Boolean b => b -> b -> b
&& forall a. Validable a => a -> Statement
valid q
f forall b. Boolean b => b -> b -> b
&& forall {t}. Oriented t => Point t -> t -> [t] -> Statement
vld Point q
s q
f [q]
gs where
    vld :: Point t -> t -> [t] -> Statement
vld Point t
s t
f []     = forall q. Oriented q => q -> Point q
start t
f forall a. Eq a => a -> a -> Statement
.==. Point t
s
    vld Point t
s t
f (t
g:[t]
gs) = forall a. Validable a => a -> Statement
valid t
g forall b. Boolean b => b -> b -> b
&& forall q. Oriented q => q -> Point q
start t
f forall a. Eq a => a -> a -> Statement
.==. forall q. Oriented q => q -> Point q
end t
g forall b. Boolean b => b -> b -> b
&& Point t -> t -> [t] -> Statement
vld Point t
s t
g [t]
gs 

instance Oriented q => Entity (Path q)

instance Oriented q => Oriented (Path q) where
  type Point (Path q) = Point q
  orientation :: Path q -> Orientation (Point (Path q))
orientation (Path Point q
s [])    = Point q
sforall p. p -> p -> Orientation p
:>Point q
s
  orientation (Path Point q
s (q
f:[q]
_)) = Point q
sforall p. p -> p -> Orientation p
:>forall q. Oriented q => q -> Point q
end q
f
 
type instance Dual (Path q) = Path (Op q)

instance Oriented q => Dualisable (Path q) where
  toDual :: Path q -> Dual (Path q)
toDual p :: Path q
p@(Path Point q
_ [q]
fs)   = forall q. Point q -> [q] -> Path q
Path (forall q. Oriented q => q -> Point q
end Path q
p) (forall a. [a] -> [a]
reverse forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall x. x -> Op x
Op [q]
fs)
  fromDual :: Dual (Path q) -> Path q
fromDual p :: Dual (Path q)
p@(Path Point (Op q)
_ [Op q]
fs) = forall q. Point q -> [q] -> Path q
Path (forall q. Oriented q => q -> Point q
end Dual (Path q)
p) (forall a. [a] -> [a]
reverse forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall x. Op x -> x
fromOp [Op q]
fs)

instance Reflexive (Path q) where
  toBidual :: Path q -> Dual (Dual (Path q))
toBidual (Path Point q
s [q]
fs) = forall q. Point q -> [q] -> Path q
Path Point q
s (forall a b. (a -> b) -> [a] -> [b]
map (forall x. x -> Op x
Op forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. x -> Op x
Op) [q]
fs)
  fromBidual :: Dual (Dual (Path q)) -> Path q
fromBidual (Path Point (Op (Op q))
s [Op (Op q)]
fs) = forall q. Point q -> [q] -> Path q
Path Point (Op (Op q))
s (forall a b. (a -> b) -> [a] -> [b]
map (forall x. Op x -> x
fromOp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. Op x -> x
fromOp) [Op (Op q)]
fs)

instance Oriented q => Embeddable q (Path q) where
  inj :: q -> Path q
inj q
f = forall q. Point q -> [q] -> Path q
Path (forall q. Oriented q => q -> Point q
start q
f) [q
f]

--------------------------------------------------------------------------------
-- pthLength -

-- | the length of a path.
pthLength :: Path q -> N
pthLength :: forall q. Path q -> N
pthLength (Path Point q
_ [q]
fs) = forall {a} {a}. (Num a, Enum a) => [a] -> a
lgth [q]
fs where
  lgth :: [a] -> a
lgth []     = a
0
  lgth (a
_:[a]
fs) = forall a. Enum a => a -> a
succ ([a] -> a
lgth [a]
fs)
  
instance LengthN (Path q) where
  lengthN :: Path q -> N
lengthN = forall q. Path q -> N
pthLength

--------------------------------------------------------------------------------
-- pthOne -

-- | path of length 0 at the given point.
pthOne :: Point q -> Path q
pthOne :: forall q. Point q -> Path q
pthOne Point q
s = forall q. Point q -> [q] -> Path q
Path Point q
s []

--------------------------------------------------------------------------------
-- pthMlt -

-- | composition of two paths.
pthMlt :: Oriented q => Path q -> Path q -> Path q
pthMlt :: forall q. Oriented q => Path q -> Path q -> Path q
pthMlt (Path Point q
s [q]
fs) p :: Path q
p@(Path Point q
t [q]
gs)
  | Point q
s forall a. Eq a => a -> a -> Bool
== forall q. Oriented q => q -> Point q
end Path q
p = forall q. Point q -> [q] -> Path q
Path Point q
t ([q]
fsforall a. [a] -> [a] -> [a]
++[q]
gs)
  | Bool
otherwise  = forall a e. Exception e => e -> a
throw ArithmeticException
NotMultiplicable

--------------------------------------------------------------------------------
-- Total -

-- | structures where its associated 'Point' type is singleton. They yield
-- globally defiend algebraic operations.
class Singleton (Point x) => Total x

instance Total ()
instance Total Int
instance Total Integer
instance Total N
instance Total Z
instance Total Q
instance Total q => Total (Path q)
instance Total x => Total (Op x)

--------------------------------------------------------------------------------
-- EntityPoint -

-- | helper class to avoid undecidable instances.
class Entity (Point x) => EntityPoint x

instance EntityPoint ()
instance EntityPoint Int
instance EntityPoint Integer
instance EntityPoint N
instance EntityPoint Z
instance EntityPoint Q
instance EntityPoint q => EntityPoint (Path q)
instance EntityPoint x => EntityPoint (Op x)

--------------------------------------------------------------------------------
-- OrdPoint -

-- | helper class to circumvent undecidable instances.
class Ord (Point x) => OrdPoint x

instance OrdPoint ()
instance OrdPoint Int
instance OrdPoint Integer
instance OrdPoint N
instance OrdPoint Z
instance OrdPoint Q
instance OrdPoint q => OrdPoint (Path q)

--------------------------------------------------------------------------------
-- Ort -

-- | type representing the class of 'Oriented' structures.
data Ort

type instance Structure Ort x = Oriented x

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

--------------------------------------------------------------------------------
-- ForgetfulOrt -

-- | transformable to 'Oriented' structure.
class Transformable s Ort => ForgetfulOrt s

instance ForgetfulTyp Ort
instance ForgetfulOrt Ort

--------------------------------------------------------------------------------
-- structOrtOp -

-- | attest that if @__x__@ is 'Oriented' then also @'Op' __x__@ is 'Oriented'.
structOrtOp :: Struct Ort x -> Struct Ort (Op x)
structOrtOp :: forall x. Struct Ort x -> Struct Ort (Op x)
structOrtOp Struct Ort x
Struct = forall s x. Structure s x => Struct s x
Struct

--------------------------------------------------------------------------------
-- 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) = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd X (Point q)
xp Point q -> X (Op q)
xs' where xs' :: Point q -> X (Op q)
xs' Point q
p = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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)   = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point q)
xp Point q -> X (Op q)
xe' where xe' :: Point q -> X (Op q)
xe' Point q
p = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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) = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point (Op (Op q)))
xp Point q -> X q
xs' where xs' :: Point q -> X q
xs' Point q
p = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Op (Op x) -> x
fromOpOp (Point (Op (Op q)) -> X (Op (Op q))
xs Point q
p)
xosFromOpOp (XEnd X (Point (Op (Op q)))
xp Point (Op (Op q)) -> X (Op (Op q))
xe)   = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd X (Point (Op (Op q)))
xp Point q -> X q
xe' where xe' :: Point q -> X q
xe' Point q
p = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Op (Op x) -> x
fromOpOp (Point (Op (Op q)) -> X (Op (Op q))
xe Point 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 = forall (s :: Site) q. XOrtSite s (Op (Op q)) -> XOrtSite s q
xosFromOpOp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. 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 = forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite
  fromDual :: Dual (XOrtSite 'To q) -> XOrtSite 'To q
fromDual = forall (s :: Site) q.
(Dual (Dual s) :~: s) -> Dual (XOrtSite s q) -> XOrtSite s q
coXOrtSiteInv 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)
    = forall x. X x -> (x -> Statement) -> Statement
Forall X (Point q)
xp
        (\Point q
p
         ->    forall a. Validable a => a -> Statement
valid Point q
p                  
            forall b. Boolean b => b -> b -> b
&& forall x. X x -> (x -> Statement) -> Statement
Forall (Point q -> X q
xq Point q
p)
                 (\q
x
                  ->    forall a. Validable a => a -> Statement
valid q
x
                     forall b. Boolean b => b -> b -> b
&& (forall q. Oriented q => q -> Point q
start q
x forall a. Eq a => a -> a -> Bool
== Point q
p) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"p"String -> String -> Parameter
:=forall a. Show a => a -> String
show Point q
p,String
"x"String -> String -> Parameter
:=forall a. Show a => a -> String
show q
x]
                 )
        )
  valid xe :: XOrtSite s q
xe@(XEnd X (Point q)
_ Point q -> X q
_) = forall a. Validable a => a -> Statement
valid (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 (forall q. Point q -> Path q
pthOne Point q
s) where

  * :: 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 = 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Path q
fs
    X q
xf     -> X q
xf forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \q
f -> N -> Point q -> Path q -> X (Path q)
pth (forall a. Enum a => a -> a
pred N
n) (forall q. Oriented q => q -> Point q
end q
f) (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 = forall q. Point q -> [q] -> Path q
Path (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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Dualisable x => Dual x -> x
fromDual forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall q (s :: Site).
Oriented q =>
XOrtSite s q -> N -> Point q -> X (Path q)
xosPathMaxAt (forall x. Dualisable x => x -> Dual x
toDual XOrtSite s q
xe) N
n Point 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 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    = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Dualisable x => Dual x -> x
fromDual forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall q (s :: Site). Oriented q => XOrtSite s q -> N -> X (Path q)
xosPathMax (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 = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X p
xp p -> X (Orientation p)
xq where xq :: p -> X (Orientation p)
xq p
s = X p
xp forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (p
sforall 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 = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd X p
xp p -> X (Orientation p)
xq where xq :: p -> X (Orientation p)
xq p
e = X p
xp forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (forall 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 = forall p. X p -> XOrtSite 'To (Orientation p)
xEndOrnt forall x. XStandard x => X x
xStandard

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

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

--------------------------------------------------------------------------------
-- 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)

--------------------------------------------------------------------------------
-- 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)

--------------------------------------------------------------------------------
-- XStandardPoint -

-- | standard random variable of 'Point's of @__a__@.
class XStandard (Point a) => XStandardPoint a

instance XStandardPoint N
instance XStandardPoint Z
instance XStandardPoint Q
instance XStandard p => XStandardPoint (Orientation p)

--------------------------------------------------------------------------------
-- 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 (forall a. Show a => a -> String
show forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Typeable a => a -> TypeRep
typeOf XOrtOrientation q
x) Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid X (Orientation (Point q))
xo
        , forall x. X x -> (x -> Statement) -> Statement
Forall X (Orientation (Point q))
xo
            (\Orientation (Point q)
o -> forall x. X x -> (x -> Statement) -> Statement
Forall (Orientation (Point q) -> X q
xq Orientation (Point q)
o)
              (\q
q -> [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid q
q
                         , (forall q. Oriented q => q -> Orientation (Point q)
orientation q
q forall a. Eq a => a -> a -> Bool
== Orientation (Point q)
o)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"o"String -> String -> Parameter
:=forall a. Show a => a -> String
show Orientation (Point q)
o,String
"q"String -> String -> Parameter
:=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) = forall q.
X (Orientation (Point q))
-> (Orientation (Point q) -> X q) -> XOrtOrientation q
XOrtOrientation X (Orientation (Point q))
xo' Orientation (Point q) -> X (Op q)
xq' where
  xo' :: X (Orientation (Point q))
xo' = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall p. Orientation p -> Orientation p
opposite X (Orientation (Point q))
xo
  xq' :: Orientation (Point q) -> X (Op q)
xq' Orientation (Point q)
o' = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall x. x -> Op x
Op (Orientation (Point q) -> X q
xq (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
_) = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall q. Oriented q => q -> Point q
start X (Orientation (Point q))
xo forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 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) = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd X (Point (Orientation (Point q)))
xp Point q -> X q
xTo where
  xp :: X (Point (Orientation (Point q)))
xp    = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall q. Oriented q => q -> Point q
end X (Orientation (Point q))
xo
  xTo :: Point q -> X q
xTo Point q
e = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall q. Oriented q => q -> Point q
start X (Orientation (Point q))
xo forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Orientation (Point q) -> X q
xq forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (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 = forall (s :: Site) q.
(Dual (Dual s) :~: s) -> Dual (XOrtSite s q) -> XOrtSite s q
coXOrtSiteInv forall {k} (a :: k). a :~: a
Refl forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall q. Oriented q => XOrtOrientation q -> XOrtSite 'To q
xoTo forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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 = 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 = forall (m :: * -> *) a. Monad m => a -> m a
return (forall s. Singleton s => s
unit forall p. p -> p -> Orientation p
:> forall s. Singleton s => s
unit)
  xq :: Orientation (Point q) -> X q
xq = 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 = forall q.
X (Orientation (Point q))
-> (Orientation (Point q) -> X q) -> XOrtOrientation q
XOrtOrientation X (Orientation p)
xo forall {a}. a -> X a
xq where
  xo :: X (Orientation p)
xo = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall p. p -> p -> Orientation p
(:>)) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a b. X a -> X b -> X (a, b)
xTupple2 X p
xp X p
xp
  xq :: a -> X a
xq = 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 = forall p. X p -> XOrtOrientation (Orientation p)
xoOrnt forall x. XStandard x => X x
xStandard

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