{-# LANGUAGE NoImplicitPrelude #-}

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

{-# LANGUAGE GADTs, StandaloneDeriving #-}

-- |

-- Module      : OAlg.Limes.Cone.ZeroHead.Core

-- Description : basice definitions for cones with a first zero arrow. 

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- basice definitions a 'Cone' with a first zero arrow. 

module OAlg.Limes.Cone.ZeroHead.Core
  (
    ConeZeroHead(..)
  ) where

import OAlg.Prelude

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

import OAlg.Structure.Additive
import OAlg.Structure.Distributive

import OAlg.Limes.Cone.Definition
import OAlg.Limes.Cone.Conic

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

-- ConeZeroHead -


-- | predicate for cones where the first arrow of its underlying diagram is equal to 'zero'.

data ConeZeroHead s p d t n m x where
  ConeZeroHead :: Distributive x => Cone s p d t n (m+1) x -> ConeZeroHead s p d t n (m+1) x

deriving instance Show (d t n (S m) x) => Show (ConeZeroHead s p d t n (S m) x)
deriving instance Eq (d t n (S m) x) => Eq (ConeZeroHead s p d t n (S m) x)

instance Conic ConeZeroHead where cone :: forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
ConeZeroHead s p d t n m x -> Cone s p d t n m x
cone (ConeZeroHead Cone s p d t n (m + 1) x
c) = Cone s p d t n m x
Cone s p d t n (m + 1) x
c
  
--------------------------------------------------------------------------------

-- ConeZeroHead - Validable -


instance (Diagrammatic d, Validable (d t n (S m) x))
  => Validable (ConeZeroHead s p d t n (S m) x) where
  valid :: ConeZeroHead s p d t n ('S m) x -> Statement
valid (ConeZeroHead Cone s p d t n (m + 1) x
c)
    = [Statement] -> Statement
And [ Cone s p d t n ('S m) x -> Statement
forall a. Validable a => a -> Statement
valid Cone s p d t n (m + 1) x
Cone s p d t n ('S m) x
c
          , x -> Statement
forall a. Additive a => a -> Statement
relIsZero (x -> Statement) -> x -> Statement
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ FinList (m + 1) x -> x
FinList ('S m) x -> x
forall (n :: N') a. FinList (n + 1) a -> a
head (FinList ('S m) x -> x) -> FinList ('S m) x -> x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram t n ('S m) x -> FinList ('S m) x
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows (Diagram t n ('S m) x -> FinList ('S m) x)
-> Diagram t n ('S m) x -> FinList ('S m) x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ d t n ('S m) x -> Diagram t n ('S m) x
forall (t :: DiagramType) (n :: N') (m :: N') x.
d t n m x -> Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
d t n m x -> Diagram t n m x
diagram (d t n ('S m) x -> Diagram t n ('S m) x)
-> d t n ('S m) x -> Diagram t n ('S m) x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Cone s p d t n ('S m) x -> d t n ('S m) x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> d t n m a
diagrammaticObject Cone s p d t n (m + 1) x
Cone s p d t n ('S m) x
c
          ]