{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}

-- |
-- Module      : OAlg.Entity.Diagram.Quiver
-- Description : the underlying quiver of a diagram
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- the underlying 'Quiver' of a 'OAlg.Entity.Diagram.Definition.Diagram'.
module OAlg.Entity.Diagram.Quiver
  ( -- * Quiver
    Quiver(..), qvOrientations 

    -- * Duality
  , coQuiver, coQuiverInv
  ) where

import Data.Typeable

import OAlg.Prelude

import OAlg.Structure.Oriented

import OAlg.Entity.Natural
import OAlg.Entity.FinList

--------------------------------------------------------------------------------
-- Quiver -

-- | quiver of @n@ points and @m@ arrows.
--
-- __Property__ Let @Quiver w o@ be in @'Quiver' __n__ __m__@, then holds:
-- For all @0 '<=' j '<' m@ holds: @s j '<' n@ and @e j '<' n@ where
-- @n = 'lengthN' w@, @s j = 'start' (o j)@ and @e j = 'end' (o j)@.
data Quiver n m = Quiver (Any n) (FinList m (Orientation N))
  deriving (Int -> Quiver n m -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: N') (m :: N'). Int -> Quiver n m -> ShowS
forall (n :: N') (m :: N'). [Quiver n m] -> ShowS
forall (n :: N') (m :: N'). Quiver n m -> String
showList :: [Quiver n m] -> ShowS
$cshowList :: forall (n :: N') (m :: N'). [Quiver n m] -> ShowS
show :: Quiver n m -> String
$cshow :: forall (n :: N') (m :: N'). Quiver n m -> String
showsPrec :: Int -> Quiver n m -> ShowS
$cshowsPrec :: forall (n :: N') (m :: N'). Int -> Quiver n m -> ShowS
Show, Quiver n m -> Quiver n m -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (n :: N') (m :: N'). Quiver n m -> Quiver n m -> Bool
/= :: Quiver n m -> Quiver n m -> Bool
$c/= :: forall (n :: N') (m :: N'). Quiver n m -> Quiver n m -> Bool
== :: Quiver n m -> Quiver n m -> Bool
$c== :: forall (n :: N') (m :: N'). Quiver n m -> Quiver n m -> Bool
Eq)

--------------------------------------------------------------------------------
-- qvOrientaitons -

-- | the orientation of the arrows of a quiver.
qvOrientations :: Quiver n m -> FinList m (Orientation N)
qvOrientations :: forall (n :: N') (m :: N'). Quiver n m -> FinList m (Orientation N)
qvOrientations (Quiver Any n
_ FinList m (Orientation N)
os) = FinList m (Orientation N)
os

--------------------------------------------------------------------------------
-- Validable -

instance Validable (Quiver n m) where
  valid :: Quiver n m -> Statement
valid (Quiver Any n
wn FinList m (Orientation N)
os) = forall (m :: N'). N -> N -> FinList m (Orientation N) -> Statement
vld N
0 (forall x. LengthN x => x -> N
lengthN Any n
wn) FinList m (Orientation N)
os where
    vld :: N -> N -> FinList m (Orientation N) -> Statement
    vld :: forall (m :: N'). N -> N -> FinList m (Orientation N) -> Statement
vld N
_ N
_ FinList m (Orientation N)
Nil = Statement
SValid
    vld N
j N
n ((N
s :> N
e):|FinList n (Orientation N)
os)
      = [Statement] -> Statement
And [ (N
s forall a. Ord a => a -> a -> Bool
< N
n) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(j,s,n)"String -> String -> Parameter
:= forall a. Show a => a -> String
show (N
j,N
s,N
n)]
            , (N
e forall a. Ord a => a -> a -> Bool
< N
n) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(j,e,n)"String -> String -> Parameter
:= forall a. Show a => a -> String
show (N
j,N
e,N
n)]
            , forall (m :: N'). N -> N -> FinList m (Orientation N) -> Statement
vld (forall a. Enum a => a -> a
succ N
j) N
n FinList n (Orientation N)
os
            ]

instance (Typeable n, Typeable m) => Entity (Quiver n m)

--------------------------------------------------------------------------------
-- Duality -

type instance Dual (Quiver n m) = Quiver n m

-- | the dual of a quiver, with inverse 'coQuiverInv'.
coQuiver :: Quiver n m -> Dual (Quiver n m)
coQuiver :: forall (n :: N') (m :: N'). Quiver n m -> Dual (Quiver n m)
coQuiver (Quiver Any n
wn FinList m (Orientation N)
os) = forall (n :: N') (m :: N').
Any n -> FinList m (Orientation N) -> Quiver n m
Quiver Any n
wn (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall p. Orientation p -> Orientation p
opposite FinList m (Orientation N)
os)

-- | from the dual quiver, with inverse 'coQuiver'.
coQuiverInv :: Dual (Quiver n m) -> Quiver n m
coQuiverInv :: forall (n :: N') (m :: N'). Dual (Quiver n m) -> Quiver n m
coQuiverInv = forall (n :: N') (m :: N'). Quiver n m -> Dual (Quiver n m)
coQuiver