{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE GADTs #-}

-- |

-- Module      : OAlg.Structure.Oriented.Proposition

-- Description : propositions on oriented structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- Propositions on 'Oriented' structure.

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

    prpOrt, XOrt, prpOrt0, prpOrt1

    -- * X

  , xosOrt, xosPoint, xoOrt

    -- ** Orientation

  , xOrtOrnt
  )
  where

import Control.Monad

import OAlg.Prelude

import OAlg.Structure.Oriented.Definition
import OAlg.Structure.Oriented.Path
import OAlg.Structure.Oriented.X

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

-- prpOrt0 -


-- | validity of the functions 'orientation', 'start' and 'end'.

prpOrt0 :: Oriented q => X q -> Statement
prpOrt0 :: forall q. Oriented q => X q -> Statement
prpOrt0 X q
xa = String -> Label
Prp String
"Ort0"
  Label -> Statement -> Statement
:<=>: X q -> (q -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X q
xa (\q
a -> q -> Statement
forall a. Validable a => a -> Statement
valid q
a Statement -> Statement -> Statement
forall b. Boolean b => b -> b -> b
~> [Statement] -> Statement
And [ Orientation (Point q) -> Statement
forall a. Validable a => a -> Statement
valid (q -> Orientation (Point q)
forall q. Oriented q => q -> Orientation (Point q)
orientation q
a)
                                        , Point q -> Statement
forall a. Validable a => a -> Statement
valid (q -> Point q
forall q. Oriented q => q -> Point q
start q
a)
                                        , Point q -> Statement
forall a. Validable a => a -> Statement
valid (q -> Point q
forall q. Oriented q => q -> Point q
end q
a)
                                        ]
                  )
  
--------------------------------------------------------------------------------

-- prpOrt1 -


-- | validity of the relation between 'orientation', 'start' and 'end' according to

--   "OAlg.Structure.Oriented.Definition#Ort1".

prpOrt1 :: Oriented q => X q -> Statement
prpOrt1 :: forall q. Oriented q => X q -> Statement
prpOrt1 X q
xa = String -> Label
Prp String
"Ort1"
  Label -> Statement -> Statement
:<=>: X q -> (q -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X q
xa (\q
a -> (q -> Orientation (Point q)
forall q. Oriented q => q -> Orientation (Point q)
orientation q
a Orientation (Point q) -> Orientation (Point q) -> Bool
forall a. Eq a => a -> a -> Bool
== (q -> Point q
forall q. Oriented q => q -> Point q
start q
a Point q -> Point q -> Orientation (Point q)
forall p. p -> p -> Orientation p
:> q -> Point q
forall q. Oriented q => q -> Point q
end q
a))
                         Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=q -> String
forall a. Show a => a -> String
show q
a]
                  )

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

-- XOrt -


-- | random variable for 'Oriented' structures.

type XOrt = X

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

-- prpOrt -


-- | validity of the 'Oriented' structure of @__q__@.

prpOrt :: Oriented q => XOrt q -> Statement
prpOrt :: forall q. Oriented q => X q -> Statement
prpOrt XOrt q
xa = String -> Label
Prp String
"Ort"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
forall b. Boolean b => [b] -> b
and [ XOrt q -> Statement
forall q. Oriented q => X q -> Statement
prpOrt0 XOrt q
xa
            , XOrt q -> Statement
forall q. Oriented q => X q -> Statement
prpOrt1 XOrt q
xa
            ]

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

-- xosOrt -


-- | the underlying random variable for 'Oriented' structures.

xosOrt :: Oriented q => XOrtSite s q -> XOrt q
xosOrt :: forall q (s :: Site). Oriented q => XOrtSite s q -> XOrt q
xosOrt XOrtSite s q
xa = do
  Path Point q
_ [q
f] <- XOrtSite s q -> N -> X (Path q)
forall q (s :: Site). Oriented q => XOrtSite s q -> N -> X (Path q)
xosPathMax XOrtSite s q
xa N
1
  q -> XOrt q
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return q
f

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

-- xosPoint -


-- | the underlying random variable of @'Point' __g__@.

xosPoint :: XOrtSite s q -> X (Point q)
xosPoint :: forall (s :: Site) q. XOrtSite s q -> X (Point q)
xosPoint (XStart X (Point q)
xp Point q -> X q
_) = X (Point q)
xp
xosPoint (XEnd X (Point q)
xp Point q -> X q
_)   = X (Point q)
xp

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

-- xoOrt -


-- | the underlying random variable for 'Oriented' structures.

xoOrt :: XOrtOrientation q -> XOrt q
xoOrt :: forall q. XOrtOrientation q -> XOrt q
xoOrt (XOrtOrientation X (Orientation (Point q))
xo Orientation (Point q) -> X q
xq) = X (Orientation (Point q))
xo X (Orientation (Point q)) -> (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

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

-- xOrtOrnt -


-- | the induced random variable of 'Oriented' structures for @'Orientation' __p__@.

xOrtOrnt :: X p -> XOrt (Orientation p)
xOrtOrnt :: forall p. X p -> XOrt (Orientation p)
xOrtOrnt = XOrtOrientation (Orientation p) -> XOrt (Orientation p)
forall q. XOrtOrientation q -> XOrt q
xoOrt (XOrtOrientation (Orientation p) -> XOrt (Orientation p))
-> (X p -> XOrtOrientation (Orientation p))
-> X p
-> XOrt (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
. X p -> XOrtOrientation (Orientation p)
forall p. X p -> XOrtOrientation (Orientation p)
xoOrnt