{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Entity.Slice.Free
-- Description : slicing by free points
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- sliced structures with an assigned /free/ 'Point' of some given /dimension/.
module OAlg.Entity.Slice.Free
  (
    -- * Free
    Free(..), freeN, castFree, isFree
  , SomeFree(..), SomeFreeSlice(..)

    -- * Limes
  , LimesFree(..), limesFree
  , DiagramFree(..),dgfDiagram
  , KernelSliceFromSomeFreeTip(..), ksfKernel

    -- ** Kernel
  , KernelFree, KernelDiagramFree
    -- ** Cokernel
  , CokernelDiagramFree    

    -- ** Pullback
  , PullbackFree, PullbackDiagramFree  
  
  ) where

import Data.Typeable
import Data.List ((++))

import OAlg.Prelude

import OAlg.Data.Singleton

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

import OAlg.Limes.Definition
import OAlg.Limes.Cone
import OAlg.Limes.KernelsAndCokernels

import OAlg.Entity.Natural hiding ((++))
import OAlg.Entity.FinList hiding ((++))
import OAlg.Entity.Diagram
import OAlg.Entity.Slice.Definition


--------------------------------------------------------------------------------
-- Free -

-- | index for free points within a 'Multiplicative' structure @__c__@.
--
-- >>> lengthN (Free attest :: Free N3 c)
-- 3
newtype Free k c = Free (Any k) deriving (Int -> Free k c -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (k :: N') c. Int -> Free k c -> ShowS
forall (k :: N') c. [Free k c] -> ShowS
forall (k :: N') c. Free k c -> String
showList :: [Free k c] -> ShowS
$cshowList :: forall (k :: N') c. [Free k c] -> ShowS
show :: Free k c -> String
$cshow :: forall (k :: N') c. Free k c -> String
showsPrec :: Int -> Free k c -> ShowS
$cshowsPrec :: forall (k :: N') c. Int -> Free k c -> ShowS
Show,Free k c -> Free k c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (k :: N') c. Free k c -> Free k c -> Bool
/= :: Free k c -> Free k c -> Bool
$c/= :: forall (k :: N') c. Free k c -> Free k c -> Bool
== :: Free k c -> Free k c -> Bool
$c== :: forall (k :: N') c. Free k c -> Free k c -> Bool
Eq,Free k c -> Statement
forall a. (a -> Statement) -> Validable a
forall (k :: N') c. Free k c -> Statement
valid :: Free k c -> Statement
$cvalid :: forall (k :: N') c. Free k c -> Statement
Validable,forall a. Show a -> Eq a -> Validable a -> Typeable a -> Entity a
forall {k :: N'} {c}. (Typeable c, Typeable k) => Eq (Free k c)
forall {k :: N'} {c}. (Typeable c, Typeable k) => Show (Free k c)
forall {k :: N'} {c}.
(Typeable c, Typeable k) =>
Typeable (Free k c)
forall {k :: N'} {c}.
(Typeable c, Typeable k) =>
Validable (Free k c)
Entity)

instance Attestable k => Singleton1 (Free k) where
  unit1 :: forall x. Free k x
unit1 = forall (k :: N') c. Any k -> Free k c
Free forall (n :: N'). Attestable n => W n
attest

instance Show1 (Free k)
instance Eq1 (Free k)
instance Validable1 (Free k)
instance Typeable k => Entity1 (Free k)

--------------------------------------------------------------------------------
-- freeN -

-- | the underlying natural number.
freeN :: Free k c -> N
freeN :: forall (k :: N') c. Free k c -> N
freeN (Free Any k
k) = forall x. LengthN x => x -> N
lengthN Any k
k

--------------------------------------------------------------------------------
-- castFree -

-- | casting between 'Free' types.
castFree :: Free k x -> Free k y
castFree :: forall (k :: N') x y. Free k x -> Free k y
castFree (Free Any k
k) = forall (k :: N') c. Any k -> Free k c
Free Any k
k

--------------------------------------------------------------------------------
-- isFree -

-- | check for being a free point, i.e. if it is equal to 'slicePoint'.
--
-- __Definition__ Let @n@ be in @'Free' __n__ __c__@ and @p@ in @'Point' __c__@ then
-- we call @p@ of __/order/__ @n@ if and only if @'slicePoint' i '==' p@.
isFree :: (Eq (Point c), Sliced (Free k) c) => Free k c -> Point c -> Bool
isFree :: forall c (k :: N').
(Eq (Point c), Sliced (Free k) c) =>
Free k c -> Point c -> Bool
isFree Free k c
i Point c
p = forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint Free k c
i forall a. Eq a => a -> a -> Bool
== Point c
p

--------------------------------------------------------------------------------
-- SomeFree -

-- | some free attest.
data SomeFree c where
  SomeFree :: (Attestable k, Sliced (Free k) c) => Free k c -> SomeFree c

deriving instance Show (SomeFree c)

instance Validable (SomeFree c) where
  valid :: SomeFree c -> Statement
valid (SomeFree Free k c
k) = String -> Label
Label String
"SomeFree" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid Free k c
k
--------------------------------------------------------------------------------
-- SomeFreeSlice -

-- | some free point within a 'Multiplicative' structure @__c__@.
data SomeFreeSlice s c where
  SomeFreeSlice :: (Attestable k, Sliced (Free k) c)
    => Slice s (Free k) c -> SomeFreeSlice s c
    
deriving instance Show c => Show (SomeFreeSlice s c)

instance Oriented c => Validable (SomeFreeSlice s c) where
  valid :: SomeFreeSlice s c -> Statement
valid (SomeFreeSlice Slice s (Free k) c
s) = String -> Label
Label String
"SomeFreeSlice" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid Slice s (Free k) c
s

--------------------------------------------------------------------------------
-- XStandardSomeFreeSliceFrom -

class XStandardSomeFreeSliceFrom c where
  xStandardSomeFreeSliceFrom :: X (SomeFreeSlice From c)
  
--------------------------------------------------------------------------------
-- LimesFree -

-- | predicate for a limes with a /free/ tip of its universal cone.
--
-- __Property__ Let @'LimesFree k l@ be in
-- @'LimesFree' __s__ __p__ __t__ __n__ __m__ __a__@ and
-- then holds: @'slicePoint' k '==' t@ where @t = 'tip' ('universalCone' l)@. 
data LimesFree s p t n m a where
  LimesFree :: (Attestable k, Sliced (Free k) a)
    => Free k a -> Limes s p t n m a -> LimesFree s p t n m a

deriving instance Oriented a => Show (LimesFree s p t n m a)

instance ( Distributive a, XStandardOrtPerspective p a
         , Typeable p, Typeable t, Typeable n, Typeable m
         )
  => Validable (LimesFree Dst p t n m a) where
  valid :: LimesFree Dst p t n m a -> Statement
valid (LimesFree Free k a
k Limes Dst p t n m a
l) = String -> Label
Label String
"LimesFree" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid Free k a
k
        , forall a. Validable a => a -> Statement
valid Limes Dst p t n m a
l
        , (forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint Free k a
k forall a. Eq a => a -> a -> Bool
== Point a
t)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"(k,t)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (Free k a
k,Point a
t)]  
        ] where t :: Point a
t = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Limes Dst p t n m a
l

--------------------------------------------------------------------------------
-- limesFree -

-- | the underlying free limes.
limesFree :: LimesFree s p t n m a -> Limes s p t n m a
limesFree :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
LimesFree s p t n m a -> Limes s p t n m a
limesFree (LimesFree Free k a
_ Limes s p t n m a
l) = Limes s p t n m a
l

--------------------------------------------------------------------------------
-- KernelSliceFromSomeFreeTip -

-- | predicate for a kernel with a start point of its diagram given by the slice index and
-- a free universal tip.
--
-- __Property__ Let @'KernelSliceFromSomeFreeTip' k' i ker@ be in
-- @'KernelSliceFromSomeFreeTip' __n__ __c__@, then holds:
--
-- (1) @'slicePoint' i '==' s@ where @'DiagramParallelLR' s _ _ = 'diagram' ker@.
--
-- (2) @'slicePoint' k' '==' 'tip' ('universalCone' ker)@.
data KernelSliceFromSomeFreeTip n i c where
  KernelSliceFromSomeFreeTip :: (Attestable k', Sliced (Free k') c)
    => Free k' c -> i c -> Kernel n c -> KernelSliceFromSomeFreeTip n i c

instance (Oriented c, Sliced i c) => Show (KernelSliceFromSomeFreeTip n i c) where
  show :: KernelSliceFromSomeFreeTip n i c -> String
show (KernelSliceFromSomeFreeTip Free k' c
k i c
i Kernel n c
ker)
    = String
"KernelSliceFromSomeFreeTip[" forall a. [a] -> [a] -> [a]
++ forall (p :: * -> *) x. Show1 p => p x -> String
show1 Free k' c
k forall a. [a] -> [a] -> [a]
++ String
"," forall a. [a] -> [a] -> [a]
++ forall (p :: * -> *) x. Show1 p => p x -> String
show1 i c
i forall a. [a] -> [a] -> [a]
++ String
"] ("
    forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kernel n c
ker forall a. [a] -> [a] -> [a]
++ String
")" 

instance (Distributive c, Sliced i c, XStandardOrtSiteTo c, Typeable n)
  => Validable (KernelSliceFromSomeFreeTip n i c) where
  valid :: KernelSliceFromSomeFreeTip n i c -> Statement
valid (KernelSliceFromSomeFreeTip Free k' c
k' i c
i Kernel n c
ker) = String -> Label
Label String
"KernelSliceFromSomeFreeTip" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ forall (p :: * -> *) x. Validable1 p => p x -> Statement
valid1 Free k' c
k'
        , forall a. Validable a => a -> Statement
valid Kernel n c
ker
        , String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: let DiagramParallelLR Point c
s Point c
_ FinList n c
_ = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Kernel n c
ker in
            (forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i c
i forall a. Eq a => a -> a -> Bool
== Point c
s) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"i"String -> String -> Parameter
:=forall (p :: * -> *) x. Show1 p => p x -> String
show1 i c
i,String
"s"String -> String -> Parameter
:= forall a. Show a => a -> String
show Point c
s]
        , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint Free k' c
k' forall a. Eq a => a -> a -> Bool
== forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Kernel n c
ker))
            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"k'"String -> String -> Parameter
:=forall (p :: * -> *) x. Show1 p => p x -> String
show1 Free k' c
k',String
"ker"String -> String -> Parameter
:=forall a. Show a => a -> String
show Kernel n c
ker]
        ]

--------------------------------------------------------------------------------
-- ksfKernel -

-- | the underlying kernel.
ksfKernel :: KernelSliceFromSomeFreeTip n i c -> Kernel n c
ksfKernel :: forall (n :: N') (i :: * -> *) c.
KernelSliceFromSomeFreeTip n i c -> Kernel n c
ksfKernel (KernelSliceFromSomeFreeTip Free k' c
_ i c
_ Kernel n c
ker) = Kernel n c
ker

--------------------------------------------------------------------------------
-- DiagramFree -

-- | predicate for diagrams with free points.
data DiagramFree t n m a = DiagramFree (FinList n (SomeFree a)) (Diagram t n m a)
  deriving (Int -> DiagramFree t n m a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
Int -> DiagramFree t n m a -> ShowS
forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
[DiagramFree t n m a] -> ShowS
forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
DiagramFree t n m a -> String
showList :: [DiagramFree t n m a] -> ShowS
$cshowList :: forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
[DiagramFree t n m a] -> ShowS
show :: DiagramFree t n m a -> String
$cshow :: forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
DiagramFree t n m a -> String
showsPrec :: Int -> DiagramFree t n m a -> ShowS
$cshowsPrec :: forall (t :: DiagramType) (n :: N') (m :: N') a.
Oriented a =>
Int -> DiagramFree t n m a -> ShowS
Show)

instance Oriented a => Validable (DiagramFree t n m a) where
  valid :: DiagramFree t n m a -> Statement
valid (DiagramFree FinList n (SomeFree a)
sfs Diagram t n m a
d) = String -> Label
Label String
"DiagramFree"
    Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid (FinList n (SomeFree a)
sfs,Diagram t n m a
d) forall b. Boolean b => b -> b -> b
&& forall a (n :: N').
Oriented a =>
N -> FinList n (SomeFree a) -> FinList n (Point a) -> Statement
vld N
0 FinList n (SomeFree a)
sfs (forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t n m a
d) where
    vld :: Oriented a => N -> FinList n (SomeFree a) -> FinList n (Point a) -> Statement
    vld :: forall a (n :: N').
Oriented a =>
N -> FinList n (SomeFree a) -> FinList n (Point a) -> Statement
vld N
_ FinList n (SomeFree a)
Nil FinList n (Point a)
Nil = Statement
SValid
    vld N
i (SomeFree Free k a
k:|FinList n (SomeFree a)
sfs) (Point a
p:|FinList n (Point a)
ps)
      = [Statement] -> Statement
And [ forall c (k :: N').
(Eq (Point c), Sliced (Free k) c) =>
Free k c -> Point c -> Bool
isFree Free k a
k Point a
p Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"i"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
i,String
"k"String -> String -> Parameter
:=forall a. Show a => a -> String
show Free k a
k,String
"p"String -> String -> Parameter
:=forall a. Show a => a -> String
show Point a
p]
            , forall a (n :: N').
Oriented a =>
N -> FinList n (SomeFree a) -> FinList n (Point a) -> Statement
vld (forall a. Enum a => a -> a
succ N
i) FinList n (SomeFree a)
sfs FinList n (Point a)
ps
            ] 

--------------------------------------------------------------------------------
-- dgfDiagram -

-- | the underlying diagram.
dgfDiagram :: DiagramFree t n m a -> Diagram t n m a
dgfDiagram :: forall (t :: DiagramType) (n :: N') (m :: N') a.
DiagramFree t n m a -> Diagram t n m a
dgfDiagram (DiagramFree FinList n (SomeFree a)
_ Diagram t n m a
d) = Diagram t n m a
d

--------------------------------------------------------------------------------
-- KernelFree -

-- | kerne diagram with free points. 
type KernelDiagramFree = DiagramFree (Parallel LeftToRight) N2

-- | kernel of a diagram with free points.
type KernelFree = LimesFree Dst Projective (Parallel LeftToRight) N2

--------------------------------------------------------------------------------
-- CokernelFree -

-- | cokernel diagrams with free points.
type CokernelDiagramFree = DiagramFree (Parallel RightToLeft) N2

--------------------------------------------------------------------------------
-- PullbackFree -

-- | pullback diagram with free points.
type PullbackDiagramFree n c = DiagramFree (Star To) (n+1) n c

-- | pullback of a diagram with free points.
type PullbackFree n c = LimesFree Mlt Projective (Star To) (n+1) n c