{-# LANGUAGE NoImplicitPrelude #-}

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



-- |

-- Module      : OAlg.Limes.Cone.Structure

-- Description : definition of eligible cone structures.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- definition of eligible cone structures.

module OAlg.Limes.Cone.Structure
  (
    -- * Cone Struct

    ConeStruct(..), cnStructO, cnStructMlt, cnStruct
  , cnStructMltOrDst

  ) where

import Data.Typeable

import OAlg.Prelude

import OAlg.Category.Dualisable

import OAlg.Data.Either

import OAlg.Structure.Multiplicative
import OAlg.Structure.Distributive

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

-- ConeStruct -


-- | cone structures.

data ConeStruct s a where
  ConeStructMlt :: Multiplicative a => ConeStruct Mlt a
  ConeStructDst :: Distributive a => ConeStruct Dst a

deriving instance Show (ConeStruct s a)
deriving instance Eq (ConeStruct s a)

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

-- cnStruct -


-- | the associated structure of a cone structure.

cnStruct :: ConeStruct s a -> Struct s a
cnStruct :: forall s a. ConeStruct s a -> Struct s a
cnStruct ConeStruct s a
cs = case ConeStruct s a
cs of
  ConeStruct s a
ConeStructMlt -> Struct s a
forall s x. Structure s x => Struct s x
Struct
  ConeStruct s a
ConeStructDst -> Struct s a
forall s x. Structure s x => Struct s x
Struct

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

-- cnStructO -


cnStructOStruct :: ConeStruct s x -> Struct s (o x) -> ConeStruct s (o x)
cnStructOStruct :: forall s x (o :: * -> *).
ConeStruct s x -> Struct s (o x) -> ConeStruct s (o x)
cnStructOStruct ConeStruct s x
ConeStructMlt Struct s (o x)
Struct = ConeStruct s (o x)
ConeStruct Mlt (o x)
forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt
cnStructOStruct ConeStruct s x
ConeStructDst Struct s (o x)
Struct = ConeStruct s (o x)
ConeStruct Dst (o x)
forall a. Distributive a => ConeStruct Dst a
ConeStructDst


-- | the opposite cone structure.

cnStructO :: TransformableG o s s => ConeStruct s a -> ConeStruct s (o a)
cnStructO :: forall (o :: * -> *) s a.
TransformableG o s s =>
ConeStruct s a -> ConeStruct s (o a)
cnStructO ConeStruct s a
cs = ConeStruct s a -> Struct s (o a) -> ConeStruct s (o a)
forall s x (o :: * -> *).
ConeStruct s x -> Struct s (o x) -> ConeStruct s (o x)
cnStructOStruct ConeStruct s a
cs (Struct s a -> Struct s (o a)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO (ConeStruct s a -> Struct s a
forall s a. ConeStruct s a -> Struct s a
cnStruct ConeStruct s a
cs))

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

-- cnStructMlt -


-- | the 'Multiplicative' structure of a cone structure.

cnStructMlt :: ConeStruct s a -> Struct Mlt a
cnStructMlt :: forall s a. ConeStruct s a -> Struct Mlt a
cnStructMlt ConeStruct s a
cs = case ConeStruct s a
cs of
  ConeStruct s a
ConeStructMlt -> Struct Mlt a
forall s x. Structure s x => Struct s x
Struct
  ConeStruct s a
ConeStructDst -> Struct Mlt a
forall s x. Structure s x => Struct s x
Struct

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

-- cnStructMltOrDst -


-- | proof of @__s__@ being either 'Mlt' or 'Dst'.

cnStructMltOrDst :: ConeStruct s a -> Either (s :~: Mlt) (s :~: Dst)
cnStructMltOrDst :: forall s a. ConeStruct s a -> Either (s :~: Mlt) (s :~: Dst)
cnStructMltOrDst ConeStruct s a
cs = case ConeStruct s a
cs of
  ConeStruct s a
ConeStructMlt -> (s :~: Mlt) -> Either (s :~: Mlt) (s :~: Dst)
forall a b. a -> Either a b
Left s :~: s
s :~: Mlt
forall {k} (a :: k). a :~: a
Refl
  ConeStruct s a
ConeStructDst -> (s :~: Dst) -> Either (s :~: Mlt) (s :~: Dst)
forall a b. b -> Either a b
Right s :~: s
s :~: Dst
forall {k} (a :: k). a :~: a
Refl