{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}

-- |
-- Module      : OAlg.Structure.Fibred.Proposition
-- Description : propositions on fibred structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- propositions on 'Fibred' structures.
module OAlg.Structure.Fibred.Proposition
  (
    -- * Fibred
    prpFbr, XFbr

    -- * Fibre Oriented
  , prpFbrOrt, XFbrOrt

    -- * X

    -- ** Orientation
  , xFbrOrnt, xFbrOrtOrnt, xStalkOrnt  

     -- ** Stalk
  , XStalk(..), xRoot, xSheafRootMax, xSheafRoot, xSheafMax, xSheaf

    -- ** Fibred Oriented
  , xoFbr, xoFbrOrt

  )
  where

import Control.Monad

import OAlg.Prelude

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative

import OAlg.Structure.Fibred.Definition
import OAlg.Structure.Additive.Definition


--------------------------------------------------------------------------------
-- XFbr -

-- | random variable for validating 'Fibred' structures.
type XFbr = X

--------------------------------------------------------------------------------
-- prpFbr -

-- | validity for 'Fibred' structures.
prpFbr :: Fibred f => XFbr f -> Statement
prpFbr :: forall f. Fibred f => XFbr f -> Statement
prpFbr XFbr f
xs = String -> Label
Prp String
"Fbr"
  Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall XFbr f
xs (\f
s -> forall a. Validable a => a -> Statement
valid f
s forall b. Boolean b => b -> b -> b
~> forall a. Validable a => a -> Statement
valid (forall f. Fibred f => f -> Root f
root f
s))

--------------------------------------------------------------------------------
-- XFbrOrt -

-- | random variable type for validating 'FibredOriented' structures. 
type XFbrOrt = X

--------------------------------------------------------------------------------
-- prpFbrOrt -

-- | validity for 'FibredOriented' structures.
prpFbrOrt :: FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt :: forall f. FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt XFbrOrt f
xs = String -> Label
Prp String
"FbrOrt"
  Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall XFbrOrt f
xs (\f
s -> (forall q. Oriented q => q -> Orientation (Point q)
orientation f
s forall a. Eq a => a -> a -> Bool
== forall f. Fibred f => f -> Root f
root f
s) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"s"String -> String -> Parameter
:=forall a. Show a => a -> String
show f
s])

--------------------------------------------------------------------------------
-- XStalk -

-- | random variable for stalks.
data XStalk x = XStalk (X (Root x)) (Root x -> X x)

--------------------------------------------------------------------------------
-- xRoot -

-- | the underlying random variable of 'root's.
xRoot :: XStalk x -> X (Root x)
xRoot :: forall x. XStalk x -> X (Root x)
xRoot (XStalk X (Root x)
xr Root x -> X x
_) = X (Root x)
xr

--------------------------------------------------------------------------------
-- xSheafRootMax -

-- | random variable of sheafs in a 'Fibred' structure all rooted in the given root and
-- with a length of either 0 - for empty 'root's - or with the given length.
xSheafRootMax :: Fibred f => XStalk f -> N -> Root f -> X (Sheaf f)
xSheafRootMax :: forall f. Fibred f => XStalk f -> N -> Root f -> X (Sheaf f)
xSheafRootMax (XStalk X (Root f)
_ Root f -> X f
xrs) N
n Root f
r = case Root f -> X f
xrs Root f
r of
  X f
XEmpty -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall c. Multiplicative c => Point c -> c
one Root f
r
  X f
xs     -> forall {t} {m :: * -> *} {f}.
(Num t, Monad m, Enum t, Fibred f, Eq t) =>
m f -> t -> Sheaf f -> m (Sheaf f)
shf X f
xs N
n (forall c. Multiplicative c => Point c -> c
one Root f
r) where
    shf :: m f -> t -> Sheaf f -> m (Sheaf f)
shf m f
_ t
0 Sheaf f
ss  = forall (m :: * -> *) a. Monad m => a -> m a
return Sheaf f
ss
    shf m f
xs t
n Sheaf f
ss = do
      f
s <- m f
xs
      m f -> t -> Sheaf f -> m (Sheaf f)
shf m f
xs (forall a. Enum a => a -> a
pred t
n) (forall {f}. Fibred f => f -> Sheaf f
inj f
s forall c. Multiplicative c => c -> c -> c
* Sheaf f
ss)
      
    inj :: f -> Sheaf f
inj f
s = forall f. Root f -> [f] -> Sheaf f
Sheaf (forall f. Fibred f => f -> Root f
root f
s) [f
s]


--------------------------------------------------------------------------------
-- xSheafMax -

-- | random variable of sheafs, based on the underlying random variable of roots, with
-- a length of either 0 - for empty 'root's - or with the given length.
xSheafMax :: Fibred f => XStalk f -> N -> X (Sheaf f)
xSheafMax :: forall f. Fibred f => XStalk f -> N -> X (Sheaf f)
xSheafMax xs :: XStalk f
xs@(XStalk X (Root f)
xr Root f -> X f
_) N
n = X (Root f)
xr forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall f. Fibred f => XStalk f -> N -> Root f -> X (Sheaf f)
xSheafRootMax XStalk f
xs N
n 

--------------------------------------------------------------------------------
-- adjZero -

-- | adjoins a 'zero' stalk for empty 'root's.
adjZero :: Additive a => XStalk a -> XStalk a
adjZero :: forall a. Additive a => XStalk a -> XStalk a
adjZero (XStalk X (Root a)
xr Root a -> X a
xrs) = forall x. X (Root x) -> (Root x -> X x) -> XStalk x
XStalk X (Root a)
xr Root a -> X a
xrs' where
  xrs' :: Root a -> X a
xrs' Root a
r = case Root a -> X a
xrs Root a
r of
    X a
XEmpty -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Additive a => Root a -> a
zero Root a
r)
    X a
xs     -> X a
xs

--------------------------------------------------------------------------------
-- xSheafRoot -

-- | random variable of sheafs, all based on the given 'root' and with the given length.
xSheafRoot :: Additive a => XStalk a -> N -> Root a -> X (Sheaf a)
xSheafRoot :: forall a. Additive a => XStalk a -> N -> Root a -> X (Sheaf a)
xSheafRoot XStalk a
xs = forall f. Fibred f => XStalk f -> N -> Root f -> X (Sheaf f)
xSheafRootMax (forall a. Additive a => XStalk a -> XStalk a
adjZero XStalk a
xs)

--------------------------------------------------------------------------------
-- xSheaf -

-- | random variable of sheafs with the given length.
xSheaf :: Additive a => XStalk a -> N -> X (Sheaf a)
xSheaf :: forall a. Additive a => XStalk a -> N -> X (Sheaf a)
xSheaf XStalk a
xs = forall f. Fibred f => XStalk f -> N -> X (Sheaf f)
xSheafMax (forall a. Additive a => XStalk a -> XStalk a
adjZero XStalk a
xs)


--------------------------------------------------------------------------------
-- xFbrOrnt -

-- | random variable for the 'Fibred' structure of @'Orientation' p@.
xFbrOrnt :: X p -> XFbr (Orientation p)
xFbrOrnt :: forall p. X p -> XFbr (Orientation p)
xFbrOrnt X p
xp = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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

---------------------------------------------------------------------------------
-- xStalkOrnt -

-- | random variable of 'XStalk' on @'Orientation' __p__@.
xStalkOrnt :: X p -> XStalk (Orientation p)
xStalkOrnt :: forall p. X p -> XStalk (Orientation p)
xStalkOrnt X p
xp = forall x. X (Root x) -> (Root x -> X x) -> XStalk x
XStalk (forall p. X p -> XFbr (Orientation p)
xFbrOrnt X p
xp) forall (m :: * -> *) a. Monad m => a -> m a
return

--------------------------------------------------------------------------------
-- xFbrOrtOrnt -

-- | random variable for the 'FibredOriented' structure of @'Orientation' p@.
xFbrOrtOrnt :: X p -> XFbrOrt (Orientation p)
xFbrOrtOrnt :: forall p. X p -> XFbr (Orientation p)
xFbrOrtOrnt = forall p. X p -> XFbr (Orientation p)
xFbrOrnt


--------------------------------------------------------------------------------
-- xoFbr -

-- | the associated random variable for validating 'Fibred' structures.
xoFbr :: XOrtOrientation f -> XFbr f
xoFbr :: forall f. XOrtOrientation f -> XFbr f
xoFbr = forall f. XOrtOrientation f -> XFbr f
xoOrt

--------------------------------------------------------------------------------
-- xoFbrOrt -

-- | the associated random variable for validation 'FibredOriented' structures.
xoFbrOrt :: XOrtOrientation f -> XFbrOrt f
xoFbrOrt :: forall f. XOrtOrientation f -> XFbr f
xoFbrOrt = forall f. XOrtOrientation f -> XFbr f
xoOrt