{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Structure.Fibred.Root

-- Description : definition of root

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- Definition of 'Root'.

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

    Root, ShowRoot, EqRoot, OrdRoot, SingletonRoot, TotalRoot, ValidableRoot, TypeableRoot
  , EntityRoot, XStandardRoot
  , Rt(..), fromRtG, idRt

  -- * Applicative

  , ApplicativeRoot, rmap, amapRt
  , FunctorialRoot

  -- * R

  , R(..)
  )
  where

import Data.Typeable

import OAlg.Prelude

import OAlg.Data.Singleton

import OAlg.Structure.Oriented

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

-- Root -


-- | the type of roots.

type family Root x

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

-- Root - helper classes -


-- | helper class to avoid undecidable instances.

class Show (Root x) => ShowRoot x

-- | helper class to avoid undecidable instances.

class Eq (Root x) => EqRoot x

-- | helper class to avoid undecidable instances.

class Ord (Root x) => OrdRoot x

-- | helper class to avoid undecidable instances.

class Validable (Root x) => ValidableRoot x

-- | helper class to avoid undecidable instances.

class Typeable (Root x) => TypeableRoot x
-- | helper class to avoid undecidable instances.


-- | helper class to avoid undecidable instances.

class Singleton (Root f) => SingletonRoot f

-- | helper class to avoid undecidable instances.

class XStandard (Root f) => XStandardRoot f

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

-- EntityRoot -


-- | 'Root's as 'Entity's.

type EntityRoot x = (ShowRoot x, EqRoot x, ValidableRoot x, TypeableRoot x)

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

-- TotalRoot -


-- | 'Root's admitting total operations.

type TotalRoot = SingletonRoot

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

-- Root - Instances -


type instance Root () = Orientation ()

type instance Root (Id x) = Root x
instance ShowRoot x => ShowRoot (Id x)
instance EqRoot x => EqRoot (Id x)
instance ValidableRoot x => ValidableRoot (Id x)
instance SingletonRoot x => SingletonRoot (Id x)
instance TypeableRoot x => TypeableRoot (Id x)

type instance Root (Op x) = Root x
instance ShowRoot x => ShowRoot (Op x)
instance EqRoot x => EqRoot (Op x)
instance ValidableRoot x => ValidableRoot (Op x)
instance SingletonRoot x => SingletonRoot (Op x)
instance TypeableRoot x => TypeableRoot (Op x)

instance ShowRoot ()
instance EqRoot ()
instance ValidableRoot ()
instance SingletonRoot ()
instance TypeableRoot ()

type instance Root Int = Orientation ()
instance ShowRoot Int
instance EqRoot Int
instance ValidableRoot Int
instance TypeableRoot Int
instance SingletonRoot Int

type instance Root Integer = Orientation ()
instance ShowRoot Integer
instance EqRoot Integer
instance ValidableRoot Integer
instance SingletonRoot Integer
instance TypeableRoot Integer

type instance Root N = Orientation ()
instance ShowRoot N
instance EqRoot N
instance ValidableRoot N
instance SingletonRoot N
instance TypeableRoot N

type instance Root Z = Orientation ()
instance ShowRoot Z
instance EqRoot Z
instance ValidableRoot Z
instance SingletonRoot Z
instance TypeableRoot Z

type instance Root Q = Orientation ()
instance ShowRoot Q
instance EqRoot Q
instance ValidableRoot Q
instance SingletonRoot Q
instance TypeableRoot Q

type instance Root (Orientation p) = Orientation p
instance Show p => ShowRoot (Orientation p)
instance Eq p => EqRoot (Orientation p)
instance Validable p => ValidableRoot (Orientation p)
instance Singleton p => SingletonRoot (Orientation p)
instance Typeable p => TypeableRoot (Orientation p)
instance XStandard p => XStandardRoot (Orientation p)

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

-- Rt -


-- | wraper for 'Root's.

newtype Rt x = Rt (Root x)

type instance Root (Rt x) = Root x

deriving instance ShowRoot x => Show (Rt x)
deriving instance EqRoot x => Eq (Rt x)
deriving instance ValidableRoot x => Validable (Rt x)

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

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

-- idRt -


-- | casting a 'Root'.

idRt :: Root x ~ Root y => Rt x -> Rt y
idRt :: forall x y. (Root x ~ Root y) => Rt x -> Rt y
idRt (Rt Root x
r) = Root y -> Rt y
forall x. Root x -> Rt x
Rt Root x
Root y
r

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

-- amapRt -


-- | the induced mapping.

amapRt :: (Root x -> Root y) -> Rt x -> Rt y
amapRt :: forall x y. (Root x -> Root y) -> Rt x -> Rt y
amapRt Root x -> Root y
r (Rt Root x
x) = Root y -> Rt y
forall x. Root x -> Rt x
Rt (Root x -> Root y
r Root x
x)

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

-- fromRtG -


-- | from 'Rt'.

fromRtG :: (Rt x -> Rt y) -> Root x -> Root y
fromRtG :: forall x y. (Rt x -> Rt y) -> Root x -> Root y
fromRtG Rt x -> Rt y
f Root x
r = Root y
r' where Rt Root y
r' = Rt x -> Rt y
f (Root x -> Rt x
forall x. Root x -> Rt x
Rt Root x
r)

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

-- ApplicativeRoot -


-- | application on 'Root's.

type ApplicativeRoot h = ApplicativeG Rt h (->)

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

-- rmap -


-- | the induced mapping of 'Root's.

rmap :: ApplicativeRoot h => h x y -> Root x -> Root y
rmap :: forall (h :: * -> * -> *) x y.
ApplicativeRoot h =>
h x y -> Root x -> Root y
rmap h x y
h = (Rt x -> Rt y) -> Root x -> Root y
forall x y. (Rt x -> Rt y) -> Root x -> Root y
fromRtG (h x y -> Rt x -> Rt y
forall x y. h x y -> Rt x -> Rt y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h)

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

-- FunctorialRoot -


-- | functorials for 'Root'.

type FunctorialRoot h = FunctorialG Rt h (->)

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

-- R -


-- | adjoining the total root @()@ to @__x__@.

newtype R x = R x deriving (Int -> R x -> ShowS
[R x] -> ShowS
R x -> String
(Int -> R x -> ShowS)
-> (R x -> String) -> ([R x] -> ShowS) -> Show (R x)
forall x. Show x => Int -> R x -> ShowS
forall x. Show x => [R x] -> ShowS
forall x. Show x => R x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall x. Show x => Int -> R x -> ShowS
showsPrec :: Int -> R x -> ShowS
$cshow :: forall x. Show x => R x -> String
show :: R x -> String
$cshowList :: forall x. Show x => [R x] -> ShowS
showList :: [R x] -> ShowS
Show,R x -> R x -> Bool
(R x -> R x -> Bool) -> (R x -> R x -> Bool) -> Eq (R x)
forall x. Eq x => R x -> R x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall x. Eq x => R x -> R x -> Bool
== :: R x -> R x -> Bool
$c/= :: forall x. Eq x => R x -> R x -> Bool
/= :: R x -> R x -> Bool
Eq,Eq (R x)
Eq (R x) =>
(R x -> R x -> Ordering)
-> (R x -> R x -> Bool)
-> (R x -> R x -> Bool)
-> (R x -> R x -> Bool)
-> (R x -> R x -> Bool)
-> (R x -> R x -> R x)
-> (R x -> R x -> R x)
-> Ord (R x)
R x -> R x -> Bool
R x -> R x -> Ordering
R x -> R x -> R 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 (R x)
forall x. Ord x => R x -> R x -> Bool
forall x. Ord x => R x -> R x -> Ordering
forall x. Ord x => R x -> R x -> R x
$ccompare :: forall x. Ord x => R x -> R x -> Ordering
compare :: R x -> R x -> Ordering
$c< :: forall x. Ord x => R x -> R x -> Bool
< :: R x -> R x -> Bool
$c<= :: forall x. Ord x => R x -> R x -> Bool
<= :: R x -> R x -> Bool
$c> :: forall x. Ord x => R x -> R x -> Bool
> :: R x -> R x -> Bool
$c>= :: forall x. Ord x => R x -> R x -> Bool
>= :: R x -> R x -> Bool
$cmax :: forall x. Ord x => R x -> R x -> R x
max :: R x -> R x -> R x
$cmin :: forall x. Ord x => R x -> R x -> R x
min :: R x -> R x -> R x
Ord,R x -> Statement
(R x -> Statement) -> Validable (R x)
forall x. Validable x => R x -> Statement
forall a. (a -> Statement) -> Validable a
$cvalid :: forall x. Validable x => R x -> Statement
valid :: R x -> Statement
Validable)

type instance Root (R x) = ()

instance ShowRoot (R x)
instance EqRoot (R x)
instance ValidableRoot (R x)
instance TypeableRoot (R x)
instance SingletonRoot (R x)
instance OrdRoot (R x)