{-# LANGUAGE NoImplicitPrelude #-}

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


-- |

-- Module      : OAlg.Structure.Oriented.Point

-- Description : associating a point type.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- Associating a point type for structured algebraic types.

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

    Point, EntityPoint
  , U(..), fromU

    -- * Applicative

  , ApplicativePoint, pmap
  , FunctorialPoint, pmapf

    -- * Point Wrapper

  , Pnt(..)
  , idPnt, toPntG, fromPntG
   
    -- * Total

  , Total

    -- * Helper Classes

  , ShowPoint, EqPoint, OrdPoint, ValidablePoint
  , TypeablePoint, SingletonPoint
  , XStandardPoint
  )
  where

import Control.Monad as M (Functor)

import Data.Typeable
import Data.Foldable

import OAlg.Prelude

import OAlg.Category.Unify

import OAlg.Data.Singleton

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

-- Point -


-- | the associated type of points.

type family Point x

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

-- Point - helper classes -


-- | helper class to avoid undecidable instances.

class Show (Point x) => ShowPoint x

-- | helper class to avoid undecidable instances.

class Eq (Point x) => EqPoint x

-- | helper class to avoid undecidable instances.

class Ord (Point x) => OrdPoint x

-- | helper class to avoid undecidable instances.

class Validable (Point x) => ValidablePoint x

-- | helper class to avoid undecidable instances.

class Typeable (Point x) => TypeablePoint x

-- | helper class to avoid undecidable instances.

class Singleton (Point x) => SingletonPoint x

-- | helper class to avoid undecidable instances.

class XStandard (Point a) => XStandardPoint a

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

-- EntityPoint -


-- | 'Point' as 'Entity'.

type EntityPoint x = (ShowPoint x, EqPoint x, ValidablePoint x, TypeablePoint x)

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

-- Total -


-- | total orientations.

type Total = SingletonPoint

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

-- Point - Associations -


type instance Point (Id x) = Point x
instance ShowPoint x => ShowPoint (Id x)
instance EqPoint x => EqPoint (Id x)
instance OrdPoint x => OrdPoint (Id x)
instance SingletonPoint x => SingletonPoint (Id x)
instance ValidablePoint x => ValidablePoint (Id x)
instance TypeablePoint x => TypeablePoint (Id x)
instance XStandardPoint x => XStandardPoint (Id x)

type instance Point () = ()
instance ShowPoint ()
instance EqPoint ()
instance OrdPoint ()
instance SingletonPoint ()
instance ValidablePoint ()
instance TypeablePoint ()
instance XStandardPoint ()

type instance Point Int = ()
instance ShowPoint Int
instance EqPoint Int
instance OrdPoint Int
instance SingletonPoint Int
instance ValidablePoint Int
instance TypeablePoint Int
instance XStandardPoint Int

type instance Point Integer = ()
instance ShowPoint Integer
instance EqPoint Integer
instance OrdPoint Integer
instance SingletonPoint Integer
instance ValidablePoint Integer
instance TypeablePoint Integer
instance XStandardPoint Integer

type instance Point N = ()
instance ShowPoint N
instance EqPoint N
instance OrdPoint N
instance SingletonPoint N
instance ValidablePoint N
instance TypeablePoint N
instance XStandardPoint N

type instance Point Z = ()
instance ShowPoint Z
instance EqPoint Z
instance OrdPoint Z
instance SingletonPoint Z
instance ValidablePoint Z
instance TypeablePoint Z
instance XStandardPoint Z

type instance Point Q = ()
instance ShowPoint Q
instance EqPoint Q
instance OrdPoint Q
instance SingletonPoint Q
instance ValidablePoint Q
instance TypeablePoint Q
instance XStandardPoint Q

type instance Point (SomeMorphism m) = SomeObjectClass m
instance ShowPoint (SomeMorphism m)
instance EqPoint (SomeMorphism m)
instance ValidablePoint (SomeMorphism m)
instance Typeable m => TypeablePoint (SomeMorphism m)

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

-- Pnt -


-- | wrapper for 'Point's.

newtype Pnt x = Pnt (Point x)

type instance Point (Pnt x) = Point x

deriving instance ShowPoint x => Show (Pnt x)
deriving instance EqPoint x => Eq (Pnt x)
deriving instance ValidablePoint x => Validable (Pnt x)
deriving instance XStandardPoint x => XStandard (Pnt x)


instance ShowPoint x => ShowPoint (Pnt x)
instance EqPoint x => EqPoint (Pnt x)
instance ValidablePoint x => ValidablePoint (Pnt x)
instance XStandardPoint x => XStandardPoint (Pnt x)

instance ApplicativeG Pnt h c => ApplicativeG Pnt (Inv2 h) c where amapG :: forall x y. Inv2 h x y -> c (Pnt x) (Pnt y)
amapG (Inv2 h x y
t h y x
_) = h x y -> c (Pnt x) (Pnt y)
forall x y. h x y -> c (Pnt x) (Pnt y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
t
instance FunctorialG Pnt h c => FunctorialG Pnt (Inv2 h) c

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

-- idPnt -


-- | casting a 'Point'.

idPnt :: Point x ~ Point y => Pnt x -> Pnt y
idPnt :: forall x y. (Point x ~ Point y) => Pnt x -> Pnt y
idPnt (Pnt Point x
p) = Point y -> Pnt y
forall x. Point x -> Pnt x
Pnt Point x
Point y
p  

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

-- toPntG -


-- | to 'Pnt',

toPntG :: (Point x -> Point y) -> Pnt x -> Pnt y
toPntG :: forall x y. (Point x -> Point y) -> Pnt x -> Pnt y
toPntG Point x -> Point y
f (Pnt Point x
x) = Point y -> Pnt y
forall x. Point x -> Pnt x
Pnt (Point x -> Point y
f Point x
x)

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

-- fromPntG -


-- | from 'Pnt'.

fromPntG :: (Pnt x -> Pnt y) -> Point x -> Point y
fromPntG :: forall x y. (Pnt x -> Pnt y) -> Point x -> Point y
fromPntG Pnt x -> Pnt y
f Point x
p = Point y
p' where Pnt Point y
p' = Pnt x -> Pnt y
f (Point x -> Pnt x
forall x. Point x -> Pnt x
Pnt Point x
p)

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

-- U -


-- | accosiating @()@ as 'Point'

newtype U x = U x deriving (U x -> U x -> Bool
(U x -> U x -> Bool) -> (U x -> U x -> Bool) -> Eq (U x)
forall x. Eq x => U x -> U x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall x. Eq x => U x -> U x -> Bool
== :: U x -> U x -> Bool
$c/= :: forall x. Eq x => U x -> U x -> Bool
/= :: U x -> U x -> Bool
Eq,Eq (U x)
Eq (U x) =>
(U x -> U x -> Ordering)
-> (U x -> U x -> Bool)
-> (U x -> U x -> Bool)
-> (U x -> U x -> Bool)
-> (U x -> U x -> Bool)
-> (U x -> U x -> U x)
-> (U x -> U x -> U x)
-> Ord (U x)
U x -> U x -> Bool
U x -> U x -> Ordering
U x -> U x -> U x
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall x. Ord x => Eq (U x)
forall x. Ord x => U x -> U x -> Bool
forall x. Ord x => U x -> U x -> Ordering
forall x. Ord x => U x -> U x -> U x
$ccompare :: forall x. Ord x => U x -> U x -> Ordering
compare :: U x -> U x -> Ordering
$c< :: forall x. Ord x => U x -> U x -> Bool
< :: U x -> U x -> Bool
$c<= :: forall x. Ord x => U x -> U x -> Bool
<= :: U x -> U x -> Bool
$c> :: forall x. Ord x => U x -> U x -> Bool
> :: U x -> U x -> Bool
$c>= :: forall x. Ord x => U x -> U x -> Bool
>= :: U x -> U x -> Bool
$cmax :: forall x. Ord x => U x -> U x -> U x
max :: U x -> U x -> U x
$cmin :: forall x. Ord x => U x -> U x -> U x
min :: U x -> U x -> U x
Ord,Int -> U x -> ShowS
[U x] -> ShowS
U x -> String
(Int -> U x -> ShowS)
-> (U x -> String) -> ([U x] -> ShowS) -> Show (U x)
forall x. Show x => Int -> U x -> ShowS
forall x. Show x => [U x] -> ShowS
forall x. Show x => U x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall x. Show x => Int -> U x -> ShowS
showsPrec :: Int -> U x -> ShowS
$cshow :: forall x. Show x => U x -> String
show :: U x -> String
$cshowList :: forall x. Show x => [U x] -> ShowS
showList :: [U x] -> ShowS
Show,(forall a b. (a -> b) -> U a -> U b)
-> (forall a b. a -> U b -> U a) -> Functor U
forall a b. a -> U b -> U a
forall a b. (a -> b) -> U a -> U b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> U a -> U b
fmap :: forall a b. (a -> b) -> U a -> U b
$c<$ :: forall a b. a -> U b -> U a
<$ :: forall a b. a -> U b -> U a
M.Functor,U x -> Statement
(U x -> Statement) -> Validable (U x)
forall x. Validable x => U x -> Statement
forall a. (a -> Statement) -> Validable a
$cvalid :: forall x. Validable x => U x -> Statement
valid :: U x -> Statement
Validable,(forall m. Monoid m => U m -> m)
-> (forall m a. Monoid m => (a -> m) -> U a -> m)
-> (forall m a. Monoid m => (a -> m) -> U a -> m)
-> (forall a b. (a -> b -> b) -> b -> U a -> b)
-> (forall a b. (a -> b -> b) -> b -> U a -> b)
-> (forall b a. (b -> a -> b) -> b -> U a -> b)
-> (forall b a. (b -> a -> b) -> b -> U a -> b)
-> (forall a. (a -> a -> a) -> U a -> a)
-> (forall a. (a -> a -> a) -> U a -> a)
-> (forall a. U a -> [a])
-> (forall a. U a -> Bool)
-> (forall a. U a -> Int)
-> (forall a. Eq a => a -> U a -> Bool)
-> (forall a. Ord a => U a -> a)
-> (forall a. Ord a => U a -> a)
-> (forall a. Num a => U a -> a)
-> (forall a. Num a => U a -> a)
-> Foldable U
forall a. Eq a => a -> U a -> Bool
forall a. Num a => U a -> a
forall a. Ord a => U a -> a
forall m. Monoid m => U m -> m
forall a. U a -> Bool
forall a. U a -> Int
forall a. U a -> [a]
forall a. (a -> a -> a) -> U a -> a
forall m a. Monoid m => (a -> m) -> U a -> m
forall b a. (b -> a -> b) -> b -> U a -> b
forall a b. (a -> b -> b) -> b -> U a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => U m -> m
fold :: forall m. Monoid m => U m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> U a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> U a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> U a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> U a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> U a -> b
foldr :: forall a b. (a -> b -> b) -> b -> U a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> U a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> U a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> U a -> b
foldl :: forall b a. (b -> a -> b) -> b -> U a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> U a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> U a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> U a -> a
foldr1 :: forall a. (a -> a -> a) -> U a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> U a -> a
foldl1 :: forall a. (a -> a -> a) -> U a -> a
$ctoList :: forall a. U a -> [a]
toList :: forall a. U a -> [a]
$cnull :: forall a. U a -> Bool
null :: forall a. U a -> Bool
$clength :: forall a. U a -> Int
length :: forall a. U a -> Int
$celem :: forall a. Eq a => a -> U a -> Bool
elem :: forall a. Eq a => a -> U a -> Bool
$cmaximum :: forall a. Ord a => U a -> a
maximum :: forall a. Ord a => U a -> a
$cminimum :: forall a. Ord a => U a -> a
minimum :: forall a. Ord a => U a -> a
$csum :: forall a. Num a => U a -> a
sum :: forall a. Num a => U a -> a
$cproduct :: forall a. Num a => U a -> a
product :: forall a. Num a => U a -> a
Foldable)

type instance Point (U x) = ()

instance ShowPoint (U x)
instance EqPoint (U x)
instance ValidablePoint (U x)
instance TypeablePoint (U x)
instance SingletonPoint (U x)
instance OrdPoint (U x)

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

-- fromU -


-- | deconstructor.

fromU :: U x -> x
fromU :: forall x. U x -> x
fromU (U x
x) = x
x

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

-- ApplicativePoint -


-- | applications on 'Point's.

type ApplicativePoint h = ApplicativeG Pnt h (->)

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

-- pmap -


-- | the induced mapping of 'Point's given by 'amapG'. 

pmap :: ApplicativePoint h => h x y -> Point x -> Point y
pmap :: forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap = (Pnt x -> Pnt y) -> Point x -> Point y
forall x y. (Pnt x -> Pnt y) -> Point x -> Point y
fromPntG ((Pnt x -> Pnt y) -> Point x -> Point y)
-> (h x y -> Pnt x -> Pnt y) -> h x y -> Point x -> Point y
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. h x y -> Pnt x -> Pnt y
forall x y. h x y -> Pnt x -> Pnt y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG

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

-- pmapf -


-- | the induced functoiral mapping of 'Point's given by 'pmap'. 

pmapf :: FunctorialPoint h => h x y -> Point x -> Point y
pmapf :: forall (h :: * -> * -> *) x y.
FunctorialPoint h =>
h x y -> Point x -> Point y
pmapf = h x y -> Point x -> Point y
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap
--------------------------------------------------------------------------------

-- FunctorialPoint -


-- | functorial application for 'Pnt'.

type FunctorialPoint h = FunctorialG Pnt h (->)

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

-- ApplicativG - Pnt - Id2 -


instance ApplicativeG Pnt h c => ApplicativeG Pnt (Id2 h) c where
  amapG :: forall x y. Id2 h x y -> c (Pnt x) (Pnt y)
amapG (Id2 h x y
h) = h x y -> c (Pnt x) (Pnt y)
forall x y. h x y -> c (Pnt x) (Pnt y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h