{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Structure.Fibred.Definition

-- Description : definition of fibred structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- fibred structures, i.e. type @__f__@ with an associated root type @'Root' __f__@ such that

-- every value in @__f__@ has a 'root'.

module OAlg.Structure.Fibred.Definition
  (
    -- * Fibred

    Fibred(..)
  , Fbr, TransformableFbr, tauFbr
  , module Rt

    -- * Sheaf

  , Sheaf(..)

    -- * X

  , XFbr, xoFbr
  , xFbrOrnt
     -- ** Stalk

  , XStalk(..), xRoot, xSheafRootMax, xSheafMax
  , xStalkOrnt  
  )
  where

import Control.Monad
import Control.Exception

import Data.List((++))
import Data.Foldable

import OAlg.Prelude

import OAlg.Data.Canonical

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

import OAlg.Structure.Fibred.Root as Rt

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

-- Fibred -


-- | types with a 'Fibred' structure. An entity of a 'Fibred' structure will be

-- called a __stalk__.

--

--  __Note__

--

-- (1) On should accept the @default@ for 'root' only if one intens to implement a

-- 'OAlg.Structure.FibredOriented.FibredOriented' structure!

--

-- (2) For 'OAlg.Structure.Distributive.Definition.Distributive' structures the only thing to be

-- implemented is the 'Root' type and should be defined as @'Root' d = 'Orientation' p@ where-- @p = 'Point' d@ (see the default implementation of 'root').

class (Entity f, EntityRoot f) => Fibred f where
  -- | the 'root' of a stalk in @f@.

  root :: f -> Root f
  default root :: (Root f ~ Orientation (Point f), Oriented f) => f -> Root f
  root = f -> Orientation (Point f)
f -> Root f
forall q. Oriented q => q -> Orientation (Point q)
orientation

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

-- Fibred - Instance -


instance Fibred ()
instance Fibred Int
instance Fibred Integer
instance Fibred N
instance Fibred Z
instance Fibred Q
instance Entity p => Fibred (Orientation p)
instance Fibred x => Fibred (Id x) where root :: Id x -> Root (Id x)
root (Id x
x) = x -> Root x
forall f. Fibred f => f -> Root f
root x
x
instance Entity a => Fibred (R a) where  root :: R a -> Root (R a)
root R a
_ = ()

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

-- Sheaf -


-- | a list in a 'Fibred' structure having all the same 'root'.

--

-- __Definition__ Let __@f@__ be a 'Fibred' structure and @s = 'Sheaf' r [t 0 .. t (n-1)]@ a

-- sheaf in __@'Sheaf' f@__, then @s@ is 'valid' if and only if

--

-- (1) @r@ is 'valid' and @t i@ are valid for all @i = 0..n-1@.

--

-- (2) @'root' (t i) '==' r@ for all @i = 0..n-1@.

--

-- furthermore @n@ is called the __/length/__ of @s@.

--

-- If two sheafs have the same 'root' then there stalks can be composed - via @('++')@ -

-- to a new sheaf having the same 'root'. But as @('++')@ is not commutative they

-- are equipped with a 'Multiplicative' structure.

data Sheaf f = Sheaf (Root f) [f]

deriving instance (Show f, ShowRoot f) => Show (Sheaf f)
deriving instance (Eq f, EqRoot f) => Eq (Sheaf f)

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

instance Fibred f => Validable (Sheaf f) where
  valid :: Sheaf f -> Statement
valid (Sheaf Root f
r [f]
fs) = Root f -> Statement
forall a. Validable a => a -> Statement
valid Root f
r Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& Root f -> [f] -> Statement
forall {f}. Fibred f => Root f -> [f] -> Statement
vld Root f
r [f]
fs where
    vld :: Root f -> [f] -> Statement
vld Root f
_ []     = Statement
SValid 
    vld Root f
r (f
f:[f]
fs) = f -> Statement
forall a. Validable a => a -> Statement
valid f
f Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& (f -> Root f
forall f. Fibred f => f -> Root f
root f
f Root f -> Root f -> Statement
forall a. Eq a => a -> a -> Statement
.==. Root f
r) Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& Root f -> [f] -> Statement
vld Root f
r [f]
fs

type instance Root (Sheaf f) = Root f
instance ShowRoot f => ShowRoot (Sheaf f)
instance EqRoot f => EqRoot (Sheaf f)
instance ValidableRoot f => ValidableRoot (Sheaf f)
instance TypeableRoot f => TypeableRoot (Sheaf f)
instance Fibred f => Fibred (Sheaf f) where
  root :: Sheaf f -> Root (Sheaf f)
root (Sheaf Root f
r [f]
_) = Root f
Root (Sheaf f)
r


type instance Point (Sheaf f) = Root f
instance ShowRoot f => ShowPoint (Sheaf f)
instance EqRoot f => EqPoint (Sheaf f)
instance ValidableRoot f => ValidablePoint (Sheaf f)
instance TypeableRoot f => TypeablePoint (Sheaf f)
instance Fibred f => Oriented (Sheaf f) where
  orientation :: Sheaf f -> Orientation (Point (Sheaf f))
orientation Sheaf f
s = Sheaf f -> Root (Sheaf f)
forall f. Fibred f => f -> Root f
root Sheaf f
s Root f -> Root f -> Orientation (Root f)
forall p. p -> p -> Orientation p
:> Sheaf f -> Root (Sheaf f)
forall f. Fibred f => f -> Root f
root Sheaf f
s

-- | @'Data.List.(++)'@ is not commutative!

instance Fibred f => Multiplicative (Sheaf f) where
  one :: Point (Sheaf f) -> Sheaf f
one Point (Sheaf f)
r = Root f -> [f] -> Sheaf f
forall f. Root f -> [f] -> Sheaf f
Sheaf Point (Sheaf f)
Root f
r []
  Sheaf Root f
r [f]
fs * :: Sheaf f -> Sheaf f -> Sheaf f
* Sheaf Root f
s [f]
gs | Root f
r Root f -> Root f -> Bool
forall a. Eq a => a -> a -> Bool
== Root f
s    = Root f -> [f] -> Sheaf f
forall f. Root f -> [f] -> Sheaf f
Sheaf Root f
r ([f]
fs[f] -> [f] -> [f]
forall a. [a] -> [a] -> [a]
++[f]
gs)
                          | Bool
otherwise = ArithmeticException -> Sheaf f
forall a e. Exception e => e -> a
throw ArithmeticException
NotMultiplicable

type instance Dual (Sheaf f) = Sheaf (Op f)

instance Fibred f => Embeddable f (Sheaf f) where
  inj :: f -> Sheaf f
inj f
a = Root f -> [f] -> Sheaf f
forall f. Root f -> [f] -> Sheaf f
Sheaf (f -> Root f
forall f. Fibred f => f -> Root f
root f
a) [f
a]

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

-- Fbr -


-- | type representing the class of 'Fibred' structures.

data Fbr

type instance Structure Fbr x = Fibred x

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

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

-- tauFbr -


-- | 'tau' for 'Fbr'.

tauFbr :: Transformable s Fbr => Struct s x -> Struct Fbr x
tauFbr :: forall s x. Transformable s Fbr => Struct s x -> Struct Fbr x
tauFbr = Struct s x -> Struct Fbr x
forall x. Struct s x -> Struct Fbr x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau

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

-- TransformableFbr -


-- | helper class to avoid undecidable instances.

class Transformable s Fbr => TransformableFbr s

instance TransformableTyp Fbr
instance TransformableFbr Fbr

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

-- XFbr -


-- | random variable for validating 'Fibred' structures.

type XFbr = X

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

-- 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 -> Sheaf f -> X (Sheaf f)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sheaf f -> X (Sheaf f)) -> Sheaf f -> X (Sheaf f)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Point (Sheaf f) -> Sheaf f
forall c. Multiplicative c => Point c -> c
one Point (Sheaf f)
Root f
r
  X f
xs     -> X f -> N -> Sheaf f -> X (Sheaf f)
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 (Point (Sheaf f) -> Sheaf f
forall c. Multiplicative c => Point c -> c
one Point (Sheaf f)
Root f
r) where
    shf :: m f -> t -> Sheaf f -> m (Sheaf f)
shf m f
_ t
0 Sheaf f
ss  = Sheaf f -> m (Sheaf f)
forall a. a -> m a
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 (t -> t
forall a. Enum a => a -> a
pred t
n) (f -> Sheaf f
forall f. Fibred f => f -> Sheaf f
inj f
s Sheaf f -> Sheaf f -> Sheaf f
forall c. Multiplicative c => c -> c -> c
* Sheaf f
ss)
      
    inj :: f -> Sheaf f
inj f
s = Root f -> [f] -> Sheaf f
forall f. Root f -> [f] -> Sheaf f
Sheaf (f -> Root f
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 X (Root f) -> (Root f -> X (Sheaf f)) -> X (Sheaf f)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= XStalk f -> N -> Root f -> X (Sheaf f)
forall f. Fibred f => XStalk f -> N -> Root f -> X (Sheaf f)
xSheafRootMax XStalk f
xs N
n 

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

-- 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 = ((p, p) -> Orientation p) -> X (p, p) -> X (Orientation p)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((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

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

-- 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 = X (Root (Orientation p))
-> (Root (Orientation p) -> X (Orientation p))
-> XStalk (Orientation p)
forall x. X (Root x) -> (Root x -> X x) -> XStalk x
XStalk (X p -> X (Orientation p)
forall p. X p -> XFbr (Orientation p)
xFbrOrnt X p
xp) Orientation p -> X (Orientation p)
Root (Orientation p) -> X (Orientation p)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return

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

-- xoFbr -


-- | the associated random variable for validating 'Fibred' structures.

xoFbr :: XOrtOrientation f -> XFbr f
xoFbr :: forall f. XOrtOrientation f -> XFbr f
xoFbr = XOrtOrientation f -> XOrt f
forall f. XOrtOrientation f -> XFbr f
xoOrt