{-# 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

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

-- 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
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X q
xa (\q
a -> forall a. Validable a => a -> Statement
valid q
a forall b. Boolean b => b -> b -> b
~> [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid (forall q. Oriented q => q -> Orientation (Point q)
orientation q
a)
                                        , forall a. Validable a => a -> Statement
valid (forall q. Oriented q => q -> Point q
start q
a)
                                        , forall a. Validable a => a -> Statement
valid (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
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X q
xa (\q
a -> (forall q. Oriented q => q -> Orientation (Point q)
orientation q
a forall a. Eq a => a -> a -> Bool
== (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))
                         Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=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
:<=>: forall b. Boolean b => [b] -> b
and [ forall q. Oriented q => X q -> Statement
prpOrt0 XOrt q
xa
            , 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] <- forall q (s :: Site). Oriented q => XOrtSite s q -> N -> X (Path q)
xosPathMax XOrtSite s q
xa N
1
  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 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 = forall q. XOrtOrientation q -> XOrt q
xoOrt forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall p. X p -> XOrtOrientation (Orientation p)
xoOrnt