{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}

-- |
-- Module      : OAlg.Category.Unify
-- Description : unification of categories
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- unification of categories, i.e. projecting morphisms by dropping the parameterization by there
-- 'domain' and 'range'.
module OAlg.Category.Unify
  (
    -- * Morphism
    SomeMorphism(..), SomeObjectClass(..)
  , SomeMorphismSite(..)
  
    -- * Path
  , SomePath(..), somePath
  , SomePathSite(..)
  
    -- * Entity
  , SomeEntity(..)

    -- * Application
  , SomeApplication(..)

  )
  where

import Data.Typeable
import Data.Type.Equality

import Data.List ((++))

import OAlg.Category.Definition
import OAlg.Structure.Definition
import OAlg.Category.Path

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

import OAlg.Entity.Definition
--------------------------------------------------------------------------------
-- SomeApplication -

-- | some application.
data SomeApplication h where
  SomeApplication :: h x y -> x -> SomeApplication h

--------------------------------------------------------------------------------
-- SomeMorphism -

-- | some morphism.
data SomeMorphism m where
  SomeMorphism :: m x y -> SomeMorphism m

instance Show2 m => Show (SomeMorphism m) where
  show :: SomeMorphism m -> String
show (SomeMorphism m x y
f) = String
"SomeMorphism[" forall a. [a] -> [a] -> [a]
++ forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 m x y
f forall a. [a] -> [a] -> [a]
++ String
"]"


instance (EmbeddableMorphismTyp m, Typeable m, Eq2 m)
  => Eq (SomeMorphism m) where
  SomeMorphism m x y
f == :: SomeMorphism m -> SomeMorphism m -> Bool
== SomeMorphism m x y
g = case forall (m :: * -> * -> *) x x' y y'.
Typeable m =>
Struct Typ x
-> Struct Typ x'
-> Struct Typ y
-> Struct Typ y'
-> m x y
-> m x' y'
-> Maybe (m x y :~: m x' y')
eqlMorphism Struct (ObjectClass (Forget Typ m)) x
tx Struct (ObjectClass (Forget Typ m)) x
tx' Struct (ObjectClass (Forget Typ m)) y
ty Struct (ObjectClass (Forget Typ m)) y
ty' m x y
f m x y
g of
    Just m x y :~: m x y
Refl -> forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2 m x y
f m x y
g
    Maybe (m x y :~: m x y)
Nothing   -> Bool
False

    where tx :: Struct (ObjectClass (Forget Typ m)) x
tx  = 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 x y
f)
          tx' :: Struct (ObjectClass (Forget Typ m)) x
tx' = 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 x y
g)
          ty :: Struct (ObjectClass (Forget Typ m)) y
ty  = forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range (forall (m :: * -> * -> *) t x y.
Transformable (ObjectClass m) t =>
m x y -> Forget t m x y
Forget m x y
f)
          ty' :: Struct (ObjectClass (Forget Typ m)) y
ty' = forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range (forall (m :: * -> * -> *) t x y.
Transformable (ObjectClass m) t =>
m x y -> Forget t m x y
Forget m x y
g)


instance Validable2 m => Validable (SomeMorphism m) where
  valid :: SomeMorphism m -> Statement
valid (SomeMorphism m x y
f) = forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 m x y
f

instance (EmbeddableMorphismTyp m, Entity2 m) => Entity (SomeMorphism m)

--------------------------------------------------------------------------------
-- SomeEntity -

-- | some entity @x@ in @__x__@ having the given @'ObjectClass' __m__@ as structure.
data SomeEntity m where
  SomeEntity :: Entity x => Struct (ObjectClass m) x -> x -> SomeEntity m

--------------------------------------------------------------------------------
-- SomePath -

-- | some path
data SomePath m where
  SomePath :: Path m x y -> SomePath m 

instance Show2 m => Show (SomePath m) where
  show :: SomePath m -> String
show (SomePath Path m x y
pth) = String
"SomePath[" forall a. [a] -> [a] -> [a]
++ forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 Path m x y
pth forall a. [a] -> [a] -> [a]
++ String
"]"

type instance Dual (SomePath m) = SomePath (Op2 m)

instance Morphism m => Dualisable (SomePath m) where
  toDual :: SomePath m -> Dual (SomePath m)
toDual (SomePath Path m x y
pth) = forall (m :: * -> * -> *) x y. Path m x y -> SomePath m
SomePath forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Dualisable x => x -> Dual x
toDual Path m x y
pth
  fromDual :: Dual (SomePath m) -> SomePath m
fromDual (SomePath Path (Op2 m) x y
pth') = forall (m :: * -> * -> *) x y. Path m x y -> SomePath m
SomePath forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Dualisable x => Dual x -> x
fromDual Path (Op2 m) x y
pth'
  
--------------------------------------------------------------------------------
-- SomeObjectClass -

-- | some object class.
data SomeObjectClass m where
  SomeObjectClass :: Transformable (ObjectClass m) Typ
    => Struct (ObjectClass m) x -> SomeObjectClass m

--------------------------------------------------------------------------------
-- SomeObjectClass - Dualisable -

type instance Dual (SomeObjectClass m) = SomeObjectClass (Op2 m)

instance Dualisable (SomeObjectClass m) where
  toDual :: SomeObjectClass m -> Dual (SomeObjectClass m)
toDual (SomeObjectClass Struct (ObjectClass m) x
s) = forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass Struct (ObjectClass m) x
s
  fromDual :: Dual (SomeObjectClass m) -> SomeObjectClass m
fromDual (SomeObjectClass Struct (ObjectClass (Op2 m)) x
s) = forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass Struct (ObjectClass (Op2 m)) x
s

--------------------------------------------------------------------------------
-- SomeObjectClass - Entity -

deriving instance Show (SomeObjectClass m)

instance Eq (SomeObjectClass m) where
  SomeObjectClass Struct (ObjectClass m) x
o == :: SomeObjectClass m -> SomeObjectClass m -> Bool
== SomeObjectClass Struct (ObjectClass m) x
o' = case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Struct (ObjectClass m) x
o Struct (ObjectClass m) x
o' of
    Just x :~: x
Refl -> Struct (ObjectClass m) x
o forall a. Eq a => a -> a -> Bool
== Struct (ObjectClass m) x
o'
    Maybe (x :~: x)
Nothing   -> Bool
False

instance Validable (SomeObjectClass m) where
  valid :: SomeObjectClass m -> Statement
valid (SomeObjectClass Struct (ObjectClass m) x
o) = forall a. Validable a => a -> Statement
valid Struct (ObjectClass m) x
o

instance Typeable m => Entity (SomeObjectClass m)

--------------------------------------------------------------------------------
-- SomePathSite -

-- | some path parameterized either by its 'domain' or 'range'.
data SomePathSite s m x where
  SomePathDomain :: Path m x y -> SomePathSite From m x
  SomePathRange  :: Path m x y -> SomePathSite To m y

type instance Dual (SomePathSite s m y) = SomePathSite (Dual s) (Op2 m) y

instance Morphism m => Dualisable (SomePathSite To m y) where
  toDual :: SomePathSite 'To m y -> Dual (SomePathSite 'To m y)
toDual (SomePathRange Path m x y
pth) = forall (m :: * -> * -> *) x x. Path m x x -> SomePathSite 'From m x
SomePathDomain (forall x. Dualisable x => x -> Dual x
toDual Path m x y
pth)
  fromDual :: Dual (SomePathSite 'To m y) -> SomePathSite 'To m y
fromDual (SomePathDomain Path (Op2 m) y y
pth') = forall (m :: * -> * -> *) x y. Path m x y -> SomePathSite 'To m y
SomePathRange (forall x. Dualisable x => Dual x -> x
fromDual Path (Op2 m) y y
pth')

--------------------------------------------------------------------------------
-- somePath -

-- | embedding.
somePath :: SomePathSite s m x -> SomePath m
somePath :: forall (s :: Site) (m :: * -> * -> *) x.
SomePathSite s m x -> SomePath m
somePath (SomePathDomain Path m x y
pth) = forall (m :: * -> * -> *) x y. Path m x y -> SomePath m
SomePath Path m x y
pth
somePath (SomePathRange Path m x x
pth) = forall (m :: * -> * -> *) x y. Path m x y -> SomePath m
SomePath Path m x x
pth

--------------------------------------------------------------------------------
-- SomeMorphismSite -

-- | some morphism given by a 'Site'.
data SomeMorphismSite s m x where
  SomeMorphismDomain :: m x y -> SomeMorphismSite From m x
  SomeMorphismRange  :: m x y -> SomeMorphismSite To m y

type instance Dual (SomeMorphismSite s m y) = SomeMorphismSite (Dual s) (Op2 m) y

instance Dualisable (SomeMorphismSite To m y) where
  toDual :: SomeMorphismSite 'To m y -> Dual (SomeMorphismSite 'To m y)
toDual (SomeMorphismRange m x y
m) = forall (m :: * -> * -> *) x x. m x x -> SomeMorphismSite 'From m x
SomeMorphismDomain (forall (h :: * -> * -> *) x y. h y x -> Op2 h x y
Op2 m x y
m)
  fromDual :: Dual (SomeMorphismSite 'To m y) -> SomeMorphismSite 'To m y
fromDual (SomeMorphismDomain (Op2 m y y
m)) = forall (m :: * -> * -> *) x y. m x y -> SomeMorphismSite 'To m y
SomeMorphismRange m y y
m