{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Data.Generator

-- Description : generators or embeddings for finitely presentable points.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- Finitely presentable 'Point's within 'Distributive' structures.

module OAlg.Data.FinitelyPresentable
  (
    -- * Finitely Presentable

    FinitelyPresentable(..), finitePresentation

    -- * Splitable

  , Splitable(..), split
    
    -- * Finite Presentation

  , FinitePresentation(..)
  , finitePoint, generator, embedding
  , SomeSliceN(..)

    -- * X

  , XSomeFreeSliceFromLiftable(..), xsfsfl
  , XStandardSomeFreeSliceFromLiftable(..)

  )
  where

import Data.Typeable
import Data.Kind

import OAlg.Prelude

import OAlg.Structure.Oriented
import OAlg.Structure.Distributive
import OAlg.Structure.Operational

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

import OAlg.Limes.KernelsAndCokernels

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

-- Splitable -


-- | predicate for splitable slices.

--

--  __Propterties__ Let @__d__@ be 'Oriented' and @'Sliced' (__ i k__) __d__@ for all

--  @__k__@, then holds:

--

--  (1) Let @'Splitable' splt@ be in @'Splitable' 'From' __i__ __d__@ then holds:

--  For all @__k__@ and @s@ in @'Slice' 'From' (__i__ __k__) __d__@ holds:

--  @'end' s' '==' 'end' s@ for all @s'@ in @splt s@.

newtype Splitable s i d
  = Splitable
      (forall k. (Attestable k, Sliced (i k) d)
         => Slice s (i k) d -> FinList k (Slice s (i N1) d)
      )

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

-- split -


-- | splitting of a slice of dimension @__i__ __k__@.

split :: (Attestable k, Sliced (i k) d)
  => Splitable s i d -> Slice s (i k) d -> FinList k (Slice s (i N1) d)
split :: forall (k :: N') (i :: N' -> * -> *) d (s :: Site).
(Attestable k, Sliced (i k) d) =>
Splitable s i d -> Slice s (i k) d -> FinList k (Slice s (i N1) d)
split (Splitable forall (k :: N').
(Attestable k, Sliced (i k) d) =>
Slice s (i k) d -> FinList k (Slice s (i N1) d)
s) = Slice s (i k) d -> FinList k (Slice s (i N1) d)
forall (k :: N').
(Attestable k, Sliced (i k) d) =>
Slice s (i k) d -> FinList k (Slice s (i N1) d)
s

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

-- FinitePresentation -


-- | finitely presentable 'Point's within a 'Distributive' structure.

--

-- __Property 1__ Let @'GeneratorTo' d k' k'' coker ker lft@ be in

-- @'FinitePresentation' 'From' __i__ __a__@ and let

-- @'DiagramChainTo' p (g':|'g'':|''Nil') = d@

--

-- @

--          g           g'

--   p <<------- p' <------< p''

--

-- @

--

-- then holds:

--

-- (1) @coker@ is the cokernel of @g'@ with @g@ as the shell factor of its universal cone.

--

-- (2) @ker@ is the kernel of @g@ with @g'@ as the shell factor of its universal cone.

--

-- (3) @'KernelSliceFromSomeFreeTip' k'' k' ker@ is 'valid'.

--

-- (4) For all @h@ in @'Slice' 'From' (__i k__) a@ with

-- @'end' h '==' p@ holds:

--

--     (1) @lft h@ is 'valid'.

--

--     (2) @'orientation' (lft h) '==' 'start' h ':>' 'start' g@.

--

--     (3) @g '*>' lft h '==' h@.

--

-- @

--              p'

--            ^ |

--           /  |

--   lft h  /   | g

--         /    |

--        /     v

--       * ---> p

--          h

-- @

--

-- __Property 2__ Let @'EmbeddingFrom' d k' k'' ker coker lft@ be in

-- -- @'FinitePresentation' 'To' __i__ __a__@ then holds the dual of the property 1 above.

data FinitePresentation s i a where
  GeneratorTo
    :: ( Attestable k' , Sliced (i k') a
       , Attestable k'', Sliced (i k'') a
       )
    => Diagram (Chain To) N3 N2 a
    -> i k' a
    -> i k'' a
    -> Cokernel N1 a
    -> Kernel N1 a
    -> (forall (k :: N') . Slice From (i k) a -> Slice From (i k) a)
    -> FinitePresentation To i a
  EmbeddingFrom
    :: ( Attestable k', Sliced (i k') a
       , Attestable k'', Sliced (i k'') a
       )
    => Diagram (Chain From) N3 N2 a
    -> i k' a
    -> i k'' a
    -> Kernel N1 a
    -> Cokernel N1 a
    -> (forall (k :: N') . Slice To (i k) a -> Slice To (i k) a)
    -> FinitePresentation From i a

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

-- FinitelyPresentable -


-- | predicate for finitely presentable 'Distributive' structures @__a__@, where for each

--   point @p@ in @'Point' __a__@ there is an associated @'FinitePresentation' __s__ __i__ __a__@

--   such that its 'finitePoint' is equal to @p@.

newtype FinitelyPresentable s i a = FinitelyPresentable (Point a -> FinitePresentation s i a)

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

-- finitePoint -


-- | the underlying finite point given by the finite presentation.

finitePoint :: FinitePresentation s i a -> Point a
finitePoint :: forall (s :: Site) (i :: N' -> * -> *) a.
FinitePresentation s i a -> Point a
finitePoint (GeneratorTo (DiagramChainTo Point a
e FinList N2 a
_) i k' a
_ i k'' a
_ Cokernel N1 a
_ Kernel N1 a
_ forall (k :: N'). Slice 'From (i k) a -> Slice 'From (i k) a
_)     = Point a
e
finitePoint (EmbeddingFrom (DiagramChainFrom Point a
s FinList N2 a
_) i k' a
_ i k'' a
_ Kernel N1 a
_ Cokernel N1 a
_ forall (k :: N'). Slice 'To (i k) a -> Slice 'To (i k) a
_) = Point a
s

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

-- SomeSliceN -


-- | some slice.

data SomeSliceN t (i :: N' -> Type -> Type) d where
  SomeSliceN :: (Attestable n, Sliced (i n) d) => Slice t (i n) d -> SomeSliceN t i d

deriving instance Show d => Show (SomeSliceN t i d)

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

-- generator -


-- | the generator 

generator :: FinitePresentation To i a -> SomeSliceN From i a
generator :: forall (i :: N' -> * -> *) a.
FinitePresentation 'To i a -> SomeSliceN 'From i a
generator (GeneratorTo (DiagramChainTo Point a
_ (a
p:|FinList n1 a
_)) i k' a
k' i k'' a
_ Cokernel N1 a
_ Kernel N1 a
_ forall (k :: N'). Slice 'From (i k) a -> Slice 'From (i k) a
_)
  = Slice 'From (i k') a -> SomeSliceN 'From i a
forall (n :: N') (i :: N' -> * -> *) d (t :: Site).
(Attestable n, Sliced (i n) d) =>
Slice t (i n) d -> SomeSliceN t i d
SomeSliceN (i k' a -> a -> Slice 'From (i k') a
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i k' a
k' a
p)

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

-- embedding -


-- | the embedding of the finite point.

embedding :: FinitePresentation From i a -> SomeSliceN To i a
embedding :: forall (i :: N' -> * -> *) a.
FinitePresentation 'From i a -> SomeSliceN 'To i a
embedding (EmbeddingFrom (DiagramChainFrom Point a
_ (a
i:|FinList n1 a
_)) i k' a
k' i k'' a
_ Kernel N1 a
_ Cokernel N1 a
_ forall (k :: N'). Slice 'To (i k) a -> Slice 'To (i k) a
_)
  = Slice 'To (i k') a -> SomeSliceN 'To i a
forall (n :: N') (i :: N' -> * -> *) d (t :: Site).
(Attestable n, Sliced (i n) d) =>
Slice t (i n) d -> SomeSliceN t i d
SomeSliceN (i k' a -> a -> Slice 'To (i k') a
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo i k' a
k' a
i)

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

-- finitePresentation -


-- | the finite presentation of a given point and according to a finitaly presentable structure.

finitePresentation :: FinitelyPresentable s i a -> Point a -> FinitePresentation s i a
finitePresentation :: forall (s :: Site) (i :: N' -> * -> *) a.
FinitelyPresentable s i a -> Point a -> FinitePresentation s i a
finitePresentation (FinitelyPresentable Point a -> FinitePresentation s i a
f) = Point a -> FinitePresentation s i a
f

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

-- XSomeFreeSliceFromLiftable -


-- | random variable of factors in @__a__@ having a free 'start' and as 'end'-point the

--   given one.

newtype XSomeFreeSliceFromLiftable a
  = XSomeFreeSliceFromLiftable (Point a -> X (SomeFreeSlice From a))

instance (Oriented a, XStandardPoint a) => Validable (XSomeFreeSliceFromLiftable a) where
  valid :: XSomeFreeSliceFromLiftable a -> Statement
valid (XSomeFreeSliceFromLiftable Point a -> X (SomeFreeSlice 'From a)
lft) = String -> Label
Prp String
"XSomeFreeSliceFromLiftable" Label -> Statement -> Statement
:<=>:
    X (Point a) -> (Point a -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Point a)
forall x. XStandard x => X x
xStandard
      (\Point a
p -> X (SomeFreeSlice 'From a)
-> (SomeFreeSlice 'From a -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (Point a -> X (SomeFreeSlice 'From a)
lft Point a
p) (\(SomeFreeSlice h :: Slice 'From (Free k) a
h@(SliceFrom Free k a
_ a
h'))
             -> [Statement] -> Statement
And [ Slice 'From (Free k) a -> Statement
forall a. Validable a => a -> Statement
valid Slice 'From (Free k) a
h
                    , (a -> Point a
forall q. Oriented q => q -> Point q
end a
h' Point a -> Point a -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
p) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params []
                    ]
                            )
      )

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

-- xsfsfl -


-- | the underlying random variable for some free slice.

xsfsfl :: XSomeFreeSliceFromLiftable a -> Point a -> X (SomeFreeSlice From a)
xsfsfl :: forall a.
XSomeFreeSliceFromLiftable a
-> Point a -> X (SomeFreeSlice 'From a)
xsfsfl (XSomeFreeSliceFromLiftable Point a -> X (SomeFreeSlice 'From a)
xfl) = Point a -> X (SomeFreeSlice 'From a)
xfl

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

-- XStandardSomeFreeSliceFromLifable -


-- | random variable of lift-able free slice froms.

--

--  __Property__ Let @__a__@ be in instance of 'XStandardSomeFreeSliceFromLiftable' then holds:

-- For all @p@ in @'Point' __a__@ and @'SomeFreeSlice' ('SliceFrom' _ h)@ in the range of

-- @'xStandardSomeFreeSliceFromLiftable' p@ holds: @'end' h '==' p@.

class XStandardSomeFreeSliceFromLiftable a where
  xStandardSomeFreeSliceFromLiftable :: XSomeFreeSliceFromLiftable a

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

-- Validable - FinitePresentation To Free a


instance
  ( Distributive a
  , XStandardEligibleConeCokernel N1 a
  , XStandardEligibleConeFactorCokernel N1 a
  , XStandardEligibleConeKernel N1 a
  , XStandardEligibleConeFactorKernel N1 a
  , XStandardSomeFreeSliceFromLiftable a
  )
  => Validable (FinitePresentation To Free a) where
  valid :: FinitePresentation 'To Free a -> Statement
valid gen :: FinitePresentation 'To Free a
gen@(GeneratorTo Diagram ('Chain 'To) N3 N2 a
d Free k' a
k' Free k'' a
k'' Cokernel N1 a
coker Kernel N1 a
ker forall (k :: N'). Slice 'From (Free k) a -> Slice 'From (Free k) a
lft) = String -> Label
Label (TypeRep -> String
forall a. Show a => a -> String
show (TypeRep -> String) -> TypeRep -> String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ FinitePresentation 'To Free a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf FinitePresentation 'To Free a
gen) Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ (Diagram ('Chain 'To) N3 N2 a, Free k' a, Free k'' a,
 Cokernel N1 a, Kernel N1 a)
-> Statement
forall a. Validable a => a -> Statement
valid (Diagram ('Chain 'To) N3 N2 a
d,Free k' a
k',Free k'' a
k'',Cokernel N1 a
coker,Kernel N1 a
ker)
        , String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: Cokernel N1 a -> FinList N1 a -> a -> Statement
forall x (n :: N').
Distributive x =>
Cokernel n x -> FinList n x -> x -> Statement
prpIsCokernel Cokernel N1 a
coker (a
g'a -> FinList N0 a -> FinList (N0 + 1) a
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList N0 a
forall a. FinList N0 a
Nil) a
g
        , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: Kernel N1 a -> FinList N1 a -> a -> Statement
forall a (n :: N').
Distributive a =>
Kernel n a -> FinList n a -> a -> Statement
prpIsKernel Kernel N1 a
ker (a
ga -> FinList N0 a -> FinList (N0 + 1) a
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList N0 a
forall a. FinList N0 a
Nil) a
g'
        , String -> Label
Label String
"3" Label -> Statement -> Statement
:<=>: KernelSliceFromSomeFreeTip N1 (Free k') a -> Statement
forall a. Validable a => a -> Statement
valid (Free k'' a
-> Free k' a
-> Kernel N1 a
-> KernelSliceFromSomeFreeTip N1 (Free k') a
forall (k' :: N') c (i :: * -> *) (n :: N').
(Attestable k', Sliced (Free k') c) =>
Free k' c -> i c -> Kernel n c -> KernelSliceFromSomeFreeTip n i c
KernelSliceFromSomeFreeTip Free k'' a
k'' Free k' a
k' Kernel N1 a
ker)
        , String -> Label
Label String
"4" Label -> Statement -> Statement
:<=>: X (SomeFreeSlice 'From a)
-> (SomeFreeSlice 'From a -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (XSomeFreeSliceFromLiftable a
-> Point a -> X (SomeFreeSlice 'From a)
forall a.
XSomeFreeSliceFromLiftable a
-> Point a -> X (SomeFreeSlice 'From a)
xsfsfl XSomeFreeSliceFromLiftable a
forall a.
XStandardSomeFreeSliceFromLiftable a =>
XSomeFreeSliceFromLiftable a
xStandardSomeFreeSliceFromLiftable Point a
p)
          (\(SomeFreeSlice Slice 'From (Free k) a
h)
            -> let lh :: Slice 'From (Free k) a
lh = Slice 'From (Free k) a -> Slice 'From (Free k) a
forall (k :: N'). Slice 'From (Free k) a -> Slice 'From (Free k) a
lft Slice 'From (Free k) a
h in
              [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: Slice 'From (Free k) a -> Statement
forall a. Validable a => a -> Statement
valid Slice 'From (Free k) a
lh
                  , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (Slice 'From (Free k) a
-> Orientation (Point (Slice 'From (Free k) a))
forall q. Oriented q => q -> Orientation (Point q)
orientation Slice 'From (Free k) a
lh Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Slice 'From (Free k) a -> Point (Slice 'From (Free k) a)
forall q. Oriented q => q -> Point q
start Slice 'From (Free k) a
h Point a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:> a -> Point a
forall q. Oriented q => q -> Point q
start a
g) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"lh"String -> String -> Parameter
:=Slice 'From (Free k) a -> String
forall a. Show a => a -> String
show Slice 'From (Free k) a
lh]
                  , String -> Label
Label String
"3" Label -> Statement -> Statement
:<=>: (a
g a -> Slice 'From (Free k) a -> Slice 'From (Free k) a
forall f x. Opl f x => f -> x -> x
*> Slice 'From (Free k) a
lh Slice 'From (Free k) a -> Slice 'From (Free k) a -> Bool
forall a. Eq a => a -> a -> Bool
== Slice 'From (Free k) a
h) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"h"String -> String -> Parameter
:=Slice 'From (Free k) a -> String
forall a. Show a => a -> String
show Slice 'From (Free k) a
h]
                  ]
          )

        ]

       where DiagramChainTo Point a
p (a
g:|a
g':|FinList n1 a
Nil) = Diagram ('Chain 'To) N3 N2 a
d