{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs, StandaloneDeriving #-}

{-# LANGUAGE RankNTypes #-}

-- |
-- Module      : OAlg.Category.Path
-- Description : category of paths over morphisms
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- category of paths over morphisms.
module OAlg.Category.Path
  (
    -- * Path
    Path(..), toOp2Path, fromOp2Path, compose, mPath, reverse, pthFoldr, pthLength
  )
  where


import Control.Monad (join)

import Data.Typeable
import qualified Data.List as L

import OAlg.Category.Definition
import OAlg.Structure.Definition
import OAlg.Entity.Definition

import OAlg.Data.Equal
import OAlg.Data.Validable
import OAlg.Data.Maybe
import OAlg.Data.Show
import OAlg.Data.Dualisable
import OAlg.Data.Opposite
import OAlg.Data.Number
import OAlg.Data.Boolean


--------------------------------------------------------------------------------
-- Path -

infixr 9 :.
  
-- | paths over morphisms.
data Path m x y where
  IdPath :: Struct (ObjectClass m) x -> Path m x x
  (:.)   :: m y z -> Path m x y -> Path m x z

--------------------------------------------------------------------------------
-- ($.) -

infixr 9 $.

-- | composing paths.
($.) :: Path m y z -> Path m x y -> Path m x z
IdPath Struct (ObjectClass m) y
_ $. :: forall (m :: * -> * -> *) y z x.
Path m y z -> Path m x y -> Path m x z
$. Path m x y
q = Path m x y
q
(m y z
f :. Path m y y
p) $. Path m x y
q = m y z
f forall (m :: * -> * -> *) y z x. m y z -> Path m x y -> Path m x z
:. (Path m y y
p forall (m :: * -> * -> *) y z x.
Path m y z -> Path m x y -> Path m x z
$. Path m x y
q)

--------------------------------------------------------------------------------
-- pthFoldr -

-- | folding from the right.
pthFoldr :: (forall x y . m x y -> f x -> f y) -> f a -> Path m a b -> f b
pthFoldr :: forall (m :: * -> * -> *) (f :: * -> *) a b.
(forall x y. m x y -> f x -> f y) -> f a -> Path m a b -> f b
pthFoldr forall x y. m x y -> f x -> f y
_ f a
x (IdPath Struct (ObjectClass m) a
_) = f a
x
pthFoldr forall x y. m x y -> f x -> f y
(/$/) f a
x (m y b
h :. Path m a y
p) = m y b
h forall x y. m x y -> f x -> f y
/$/ ((forall (m :: * -> * -> *) (f :: * -> *) a b.
(forall x y. m x y -> f x -> f y) -> f a -> Path m a b -> f b
pthFoldr forall x y. m x y -> f x -> f y
(/$/) f a
x Path m a y
p))

--------------------------------------------------------------------------------
-- pthLength

data C a = C N

-- | the length of a path.
pthLength :: Path m x y -> N
pthLength :: forall (m :: * -> * -> *) x y. Path m x y -> N
pthLength Path m x y
p = N
l where
  
  C N
l = forall (m :: * -> * -> *) (f :: * -> *) a b.
(forall x y. m x y -> f x -> f y) -> f a -> Path m a b -> f b
pthFoldr forall (m :: * -> * -> *) x y. m x y -> C x -> C y
inc (forall a. N -> C a
C N
0) Path m x y
p
  
  inc :: m x y -> C x -> C y
  inc :: forall (m :: * -> * -> *) x y. m x y -> C x -> C y
inc m x y
_ (C N
i) = forall a. N -> C a
C (forall a. Enum a => a -> a
succ N
i)

--------------------------------------------------------------------------------
-- compose -

-- | composing the morphisms of a path.
compose :: Category m => Path m x y -> m x y
compose :: forall (m :: * -> * -> *) x y. Category m => Path m x y -> m x y
compose (IdPath Struct (ObjectClass m) x
s) = forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne Struct (ObjectClass m) x
s
compose (m y y
m :. Path m x y
p)   = m y y
m forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (m :: * -> * -> *) x y. Category m => Path m x y -> m x y
compose Path m x y
p

--------------------------------------------------------------------------------
-- mPath -

-- | embedding morphisms into paths.
mPath :: Morphism m => m x y -> Path m x y
mPath :: forall (m :: * -> * -> *) x y. Morphism m => m x y -> Path m x y
mPath m x y
f = m x y
f forall (m :: * -> * -> *) y z x. m y z -> Path m x y -> Path m x z
:. forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain m x y
f)

--------------------------------------------------------------------------------
-- reverse -

-- | reversing a path given by the formal /inverse/ function.
reverse :: (Morphism m, Morphism f)
  => (forall u . Struct (ObjectClass m) u -> Struct (ObjectClass f) u) 
  -> (forall u v . m u v -> f v u)
  -> Path m x y -> Path f y x
reverse :: forall (m :: * -> * -> *) (f :: * -> * -> *) x y.
(Morphism m, Morphism f) =>
(forall u. Struct (ObjectClass m) u -> Struct (ObjectClass f) u)
-> (forall u v. m u v -> f v u) -> Path m x y -> Path f y x
reverse forall u. Struct (ObjectClass m) u -> Struct (ObjectClass f) u
t forall u v. m u v -> f v u
_ (IdPath Struct (ObjectClass m) x
s) = forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath (forall u. Struct (ObjectClass m) u -> Struct (ObjectClass f) u
t Struct (ObjectClass m) x
s)
reverse forall u. Struct (ObjectClass m) u -> Struct (ObjectClass f) u
t forall u v. m u v -> f v u
rev (m y y
f :. Path m x y
p)   = forall (m :: * -> * -> *) (f :: * -> * -> *) x y.
(Morphism m, Morphism f) =>
(forall u. Struct (ObjectClass m) u -> Struct (ObjectClass f) u)
-> (forall u v. m u v -> f v u) -> Path m x y -> Path f y x
reverse forall u. Struct (ObjectClass m) u -> Struct (ObjectClass f) u
t forall u v. m u v -> f v u
rev Path m x y
p forall (m :: * -> * -> *) y z x.
Path m y z -> Path m x y -> Path m x z
$. forall (m :: * -> * -> *) x y. Morphism m => m x y -> Path m x y
mPath (forall u v. m u v -> f v u
rev m y y
f)

--------------------------------------------------------------------------------
-- toOp2Path -

-- | the opposite path.
toOp2Path :: Morphism m => Path m x y -> Path (Op2 m) y x
toOp2Path :: forall (m :: * -> * -> *) x y.
Morphism m =>
Path m x y -> Path (Op2 m) y x
toOp2Path = forall (m :: * -> * -> *) (f :: * -> * -> *) x y.
(Morphism m, Morphism f) =>
(forall u. Struct (ObjectClass m) u -> Struct (ObjectClass f) u)
-> (forall u v. m u v -> f v u) -> Path m x y -> Path f y x
reverse forall x. x -> x
id forall (h :: * -> * -> *) x y. h y x -> Op2 h x y
Op2

--------------------------------------------------------------------------------
-- fromOp2Path -

-- | from the opposite path.
fromOp2Path :: Morphism m => Path (Op2 m) x y -> Path m y x
fromOp2Path :: forall (m :: * -> * -> *) x y.
Morphism m =>
Path (Op2 m) x y -> Path m y x
fromOp2Path = forall (m :: * -> * -> *) (f :: * -> * -> *) x y.
(Morphism m, Morphism f) =>
(forall u. Struct (ObjectClass m) u -> Struct (ObjectClass f) u)
-> (forall u v. m u v -> f v u) -> Path m x y -> Path f y x
reverse forall x. x -> x
id (\(Op2 m v u
m) -> m v u
m)

--------------------------------------------------------------------------------
-- Path - Dualisable -

type instance Dual (Path m x y) = Path (Op2 m) y x

instance Morphism m => Dualisable (Path m x y) where
  toDual :: Path m x y -> Dual (Path m x y)
toDual = forall (m :: * -> * -> *) x y.
Morphism m =>
Path m x y -> Path (Op2 m) y x
toOp2Path
  fromDual :: Dual (Path m x y) -> Path m x y
fromDual = forall (m :: * -> * -> *) x y.
Morphism m =>
Path (Op2 m) x y -> Path m y x
fromOp2Path
  
--------------------------------------------------------------------------------
-- Path - Entity2 -

instance Show2 m => Show2 (Path m) where
  show2 :: forall a b. Path m a b -> String
show2 Path m a b
p = String
"Path[" forall {a}. [a] -> [a] -> [a]
++ (forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. a -> [a] -> [a]
tween String
"," forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x y. Show2 m => Path m x y -> [String]
shws Path m a b
p) forall {a}. [a] -> [a] -> [a]
++ String
"]" where
    ++ :: [a] -> [a] -> [a]
(++) = forall {a}. [a] -> [a] -> [a]
(L.++)
    shws :: Show2 m => Path m x y -> [String]
    shws :: forall (m :: * -> * -> *) x y. Show2 m => Path m x y -> [String]
shws (IdPath Struct (ObjectClass m) x
_) = []
    shws (m y y
f :. Path m x y
p')   = forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 m y y
f forall a. a -> [a] -> [a]
: forall (m :: * -> * -> *) x y. Show2 m => Path m x y -> [String]
shws Path m x y
p'

instance Show2 (Path m) => Show (Path m x y) where
  show :: Path m x y -> String
show = forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2
    
instance (Morphism m, Validable2 m) => Validable2 (Path m) where
  valid2 :: forall x y. Path m x y -> Statement
valid2 (IdPath Struct (ObjectClass m) x
o) = forall (p :: * -> *) x. Validable1 p => p x -> Statement
valid1 Struct (ObjectClass m) x
o
  valid2 (m y y
f :. Path m x y
p)   = forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 m y y
f forall b. Boolean b => b -> b -> b
&& forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 Path m x y
p

instance Validable2 (Path m) => Validable (Path m x y) where
  valid :: Path m x y -> Statement
valid = forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2
  
instance (EmbeddableMorphismTyp m, Eq2 m) => Eq2 (Path m) where
  eq2 :: forall x y. Path m x y -> Path m x y -> Bool
eq2 Path m x y
p Path m x y
q = case (Path m x y
p,Path m x y
q) of
    (IdPath Struct (ObjectClass m) x
Struct,IdPath Struct (ObjectClass m) x
Struct) -> Bool
True
    
    (m y y
f :. Path m x y
p',m y y
g :. Path m x y
q') -> case forall x x' (m :: * -> * -> *) y.
Struct Typ x
-> Struct Typ x' -> m x y -> m x' y -> Maybe (x :~: x')
eqlDomain (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain (forall (m :: * -> * -> *) t x y.
Transformable (ObjectClass m) t =>
m x y -> Forget t m x y
Forget m y y
f)) (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain(forall (m :: * -> * -> *) t x y.
Transformable (ObjectClass m) t =>
m x y -> Forget t m x y
Forget m y y
g)) m y y
f m y y
g of
      Just y :~: y
Refl       -> forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2 m y y
f m y y
g forall b. Boolean b => b -> b -> b
&& forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2 Path m x y
p' Path m x y
q'
      Maybe (y :~: y)
Nothing         -> Bool
False
      
    (Path m x y, Path m x y)
_                 -> Bool
False

instance Eq2 (Path m) => Eq (Path m x y) where
  == :: Path m x y -> Path m x y -> Bool
(==) = forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2

instance (Entity2 h, EmbeddableMorphismTyp h) => Entity2 (Path h)  
--------------------------------------------------------------------------------
-- Path - Morphism -

instance Morphism m => Morphism (Path m) where
  type ObjectClass (Path m) = ObjectClass m
  domain :: forall x y. Path m x y -> Struct (ObjectClass (Path m)) x
domain (IdPath Struct (ObjectClass m) x
s) = Struct (ObjectClass m) x
s
  domain (m y y
_ :. Path m x y
p)   = forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain Path m x y
p

  range :: forall x y. Path m x y -> Struct (ObjectClass (Path m)) y
range (IdPath Struct (ObjectClass m) x
s) = Struct (ObjectClass m) x
s
  range (m y y
f :. Path m x y
_)   = forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range m y y
f

instance EmbeddableMorphism m t => EmbeddableMorphism (Path m) t

instance EmbeddableMorphismTyp m => EmbeddableMorphismTyp (Path m)

--------------------------------------------------------------------------------
-- Path - Category -

instance Morphism m => Category (Path m) where
  cOne :: forall x. Struct (ObjectClass (Path m)) x -> Path m x x
cOne Struct (ObjectClass (Path m)) x
s = forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath Struct (ObjectClass (Path m)) x
s
  . :: forall y z x. Path m y z -> Path m x y -> Path m x z
(.)   = forall (m :: * -> * -> *) y z x.
Path m y z -> Path m x y -> Path m x z
($.)

--------------------------------------------------------------------------------
-- Path - Applicative -

instance Applicative m => Applicative (Path m) where
  amap :: forall a b. Path m a b -> a -> b
amap (IdPath Struct (ObjectClass m) a
_) a
x = a
x
  amap (m y b
p :. Path m a y
f) a
x   = forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap m y b
p (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap Path m a y
f a
x)

--------------------------------------------------------------------------------
-- Path - Functorial -
instance (Applicative m, Morphism m) => Functorial (Path m)

--------------------------------------------------------------------------------
-- Path - Cayleyan2 -

instance (Cayleyan2 m, EmbeddableMorphismTyp m) => Cayleyan2 (Path m) where
  invert2 :: forall x y. Path m x y -> Path m y x
invert2 f :: Path m x y
f@(IdPath Struct (ObjectClass m) x
_) = Path m x y
f
  invert2 (m y y
f :. Path m x y
p)     = forall (c :: * -> * -> *) x y. Cayleyan2 c => c x y -> c y x
invert2 Path m x y
p forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (m :: * -> * -> *) x y. Morphism m => m x y -> Path m x y
mPath (forall (c :: * -> * -> *) x y. Cayleyan2 c => c x y -> c y x
invert2 m y y
f)