{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Structure.Oriented.Definition

-- Description : general definition of oriented structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- General definition of 'Oriented' structures.

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

    Oriented(..), isEndo, isEndoAt
  , Ort, tauOrt, TransformableOrt
  , module Pnt
  , module Orn

    -- * Duality

  
    -- ** Transposable

  , TransposableOriented

    -- * Extensional Equlity

  , EqualExtOrt, EqEOrt
  
    -- * X

  , OrtX
  )
  where

import Data.Kind

import OAlg.Prelude

import OAlg.Category.Unify

import OAlg.Structure.Oriented.Point as Pnt
import OAlg.Structure.Oriented.Orientation as Orn

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

-- 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, EntityPoint q) => Oriented q where
  {-# MINIMAL orientation | (start,end) #-}
  
  -- | the orientation of an arrow.

  orientation :: q -> Orientation (Point q)
  orientation q
a = 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

  -- | the start point of an arrow.

  start :: q -> Point q
  start q
a = Point q
s where Point q
s :> Point q
_ = q -> Orientation (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 = q -> Orientation (Point q)
forall q. Oriented q => q -> Orientation (Point q)
orientation q
a

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

-- Oriented - Instance -


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

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

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

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

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

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

instance Oriented x => Oriented (Id x) where
  orientation :: Id x -> Orientation (Point (Id x))
orientation (Id x
x) = x -> Orientation (Point x)
forall q. Oriented q => q -> Orientation (Point q)
orientation x
x

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

instance (Morphism m, TransformableObjectClassTyp m, Entity2 m) => Oriented (SomeMorphism m) where
  start :: SomeMorphism m -> Point (SomeMorphism m)
start (SomeMorphism m x y
f) = Struct (ObjectClass m) x -> SomeObjectClass m
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (m x y -> Struct (ObjectClass m) x
forall x y. m x y -> Struct (ObjectClass m) x
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) = Struct (ObjectClass m) y -> SomeObjectClass m
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (m x y -> Struct (ObjectClass m) y
forall x y. m x y -> Struct (ObjectClass m) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range m x y
f)

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

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

-- 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 = q -> Point q
forall q. Oriented q => q -> Point q
start q
a Point q -> Point q -> Bool
forall a. Eq a => a -> a -> Bool
== q -> Point q
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 = a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
a Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
p Point a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:> Point a
p

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

-- 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 Entity p => TransposableOriented (Orientation p)

instance TransposableOriented N
instance TransposableOriented Z
instance TransposableOriented 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 = Struct Typ x
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 = Struct Ent x
forall s x. Structure s x => Struct s x
Struct

instance Transformable Ort Type where tau :: forall x. Struct Ort x -> Struct (*) x
tau Struct Ort x
_ = Struct (*) x
forall s x. Structure s x => Struct s x
Struct
instance TransformableType Ort

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

-- TransformableOrt -


-- | helper class to avoid undecidable instances.

class Transformable s Ort => TransformableOrt s

instance TransformableTyp Ort
instance TransformableOrt Ort

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

-- tauOrt -


-- | transforming to 'Ort'.

tauOrt :: Transformable s Ort => Struct s x -> Struct Ort x
tauOrt :: forall s x. Transformable s Ort => Struct s x -> Struct Ort x
tauOrt = Struct s x -> Struct Ort x
forall x. Struct s x -> Struct Ort x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau

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

-- OrtX -


-- | type representing the class of 'Oriented' structures with associated standard random

-- variables.

data OrtX

type instance Structure OrtX x
  = (Oriented x, XStandard x, XStandardPoint x)

instance Transformable OrtX XStd where tau :: forall x. Struct OrtX x -> Struct XStd x
tau Struct OrtX x
Struct = Struct XStd x
forall s x. Structure s x => Struct s x
Struct

instance Transformable OrtX Typ where tau :: forall x. Struct OrtX x -> Struct Typ x
tau Struct OrtX x
Struct = Struct Typ x
forall s x. Structure s x => Struct s x
Struct
instance TransformableTyp OrtX

instance Transformable OrtX Ort where tau :: forall x. Struct OrtX x -> Struct Ort x
tau Struct OrtX x
Struct = Struct Ort x
forall s x. Structure s x => Struct s x
Struct
instance TransformableOrt OrtX 
instance TransformableG Id OrtX EqE where tauG :: forall x. Struct OrtX x -> Struct EqE (Id x)
tauG Struct OrtX x
Struct = Struct EqE (Id x)
forall s x. Structure s x => Struct s x
Struct
instance TransformableG Pnt OrtX EqE where tauG :: forall x. Struct OrtX x -> Struct EqE (Pnt x)
tauG Struct OrtX x
Struct = Struct EqE (Pnt x)
forall s x. Structure s x => Struct s x
Struct
instance Transformable OrtX Type where tau :: forall x. Struct OrtX x -> Struct (*) x
tau Struct OrtX x
_ = Struct (*) x
forall s x. Structure s x => Struct s x
Struct
instance TransformableType OrtX

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

-- EqEOrt


-- | type representing extensional equality for 'Oriented' structures.

data EqEOrt

type instance Structure EqEOrt x
  = (Show x, ShowPoint x, Eq x, EqPoint x, XStandard x, XStandardPoint x) 

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

-- EqualExtOrt -


-- | category of extensional equality for 'Oriented' structures.

type EqualExtOrt = Sub EqEOrt (->)

instance EqExt EqualExtOrt where
  Sub x -> y
f .=. :: forall x y. EqualExtOrt x y -> EqualExtOrt x y -> Statement
.=. Sub x -> y
g = X x -> (x -> y) -> (x -> y) -> Statement
forall x y.
(Show x, Eq y) =>
X x -> (x -> y) -> (x -> y) -> Statement
prpEqualExt X x
forall x. XStandard x => X x
xStandard x -> y
f x -> y
g

instance Transformable OrtX EqEOrt where tau :: forall x. Struct OrtX x -> Struct EqEOrt x
tau Struct OrtX x
Struct = Struct EqEOrt x
forall s x. Structure s x => Struct s x
Struct
instance TransformableObjectClass OrtX EqualExtOrt

instance TransformableG Id OrtX EqEOrt where tauG :: forall x. Struct OrtX x -> Struct EqEOrt (Id x)
tauG Struct OrtX x
Struct = Struct EqEOrt (Id x)
forall s x. Structure s x => Struct s x
Struct
instance TransformableGObjectClassRange Id OrtX EqualExtOrt

instance TransformableG Pnt OrtX EqEOrt where tauG :: forall x. Struct OrtX x -> Struct EqEOrt (Pnt x)
tauG Struct OrtX x
Struct = Struct EqEOrt (Pnt x)
forall s x. Structure s x => Struct s x
Struct
instance TransformableGObjectClassRange Pnt OrtX EqualExtOrt

instance Transformable EqEOrt Type where tau :: forall x. Struct EqEOrt x -> Struct (*) x
tau Struct EqEOrt x
_ = Struct (*) x
forall s x. Structure s x => Struct s x
Struct