{-# 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 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
[Quiver n m] -> ShowS
Quiver n m -> String
(Int -> Quiver n m -> ShowS)
-> (Quiver n m -> String)
-> ([Quiver n m] -> ShowS)
-> Show (Quiver n m)
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
$cshowsPrec :: forall (n :: N') (m :: N'). Int -> Quiver n m -> ShowS
showsPrec :: Int -> Quiver n m -> ShowS
$cshow :: forall (n :: N') (m :: N'). Quiver n m -> String
show :: Quiver n m -> String
$cshowList :: forall (n :: N') (m :: N'). [Quiver n m] -> ShowS
showList :: [Quiver n m] -> ShowS
Show, Quiver n m -> Quiver n m -> Bool
(Quiver n m -> Quiver n m -> Bool)
-> (Quiver n m -> Quiver n m -> Bool) -> Eq (Quiver n m)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (n :: N') (m :: N'). 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
/= :: 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) = N -> N -> FinList m (Orientation N) -> Statement
forall (m :: N'). N -> N -> FinList m (Orientation N) -> Statement
vld N
0 (Any n -> N
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 n1 (Orientation N)
os)
      = [Statement] -> Statement
And [ (N
s N -> N -> Bool
forall a. Ord a => a -> a -> Bool
< N
n) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(j,s,n)"String -> String -> Parameter
:= (N, N, N) -> String
forall a. Show a => a -> String
show (N
j,N
s,N
n)]
            , (N
e N -> N -> Bool
forall a. Ord a => a -> a -> Bool
< N
n) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"(j,e,n)"String -> String -> Parameter
:= (N, N, N) -> String
forall a. Show a => a -> String
show (N
j,N
e,N
n)]
            , N -> N -> FinList n1 (Orientation N) -> Statement
forall (m :: N'). N -> N -> FinList m (Orientation N) -> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
j) N
n FinList n1 (Orientation N)
os
            ]

--------------------------------------------------------------------------------
-- 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) = Any n -> FinList m (Orientation N) -> Quiver n m
forall (n :: N') (m :: N').
Any n -> FinList m (Orientation N) -> Quiver n m
Quiver Any n
wn ((Orientation N -> Orientation N)
-> FinList m (Orientation N) -> FinList m (Orientation N)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Orientation N -> Orientation N
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 = Dual (Quiver n m) -> Quiver n m
Quiver n m -> Dual (Quiver n m)
forall (n :: N') (m :: N'). Quiver n m -> Dual (Quiver n m)
coQuiver