{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Data.Generator
-- Description : generator for finitely generated points
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- 'Generator' for finitely generated 'Point's within a 'Distributive' structure.
module OAlg.Data.Generator
  ( -- * Generator
    Generator(..)

    -- * X
  , XSomeFreeSliceFromLiftable(..), xsfsfl
  , XStandardSomeFreeSliceFromLiftable(..)
  )
  where

import Data.Typeable

import OAlg.Prelude

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

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


import OAlg.Limes.KernelsAndCokernels

--------------------------------------------------------------------------------
-- Generator -

-- | generator for finitely generated 'Point's within a 'Distributive' structure.
--
-- __Property__ Let @'Generator' d k' k'' coker ker lft@ be in 'Generator' and let
-- @'DiagramChainTo' g (p':|'p'':|''Nil') = d@
--
-- @
--          p           p'
--   g <<------- g' <------< g''
--
-- @
--
-- then holds:
--
-- (1) @coker@ is the cokernel of @p'@ with @p@ as the shell of its universal cone.
--
-- (2) @ker@ is the kernel of @p@ with @p'@ as the shell of its universal cone.
--
-- (3) @'KenrelSliceFromSomeFreeTip k'' k' ker@ is 'valid'.
--
-- (4) For all @h = 'SliceFrom' _ h'@ in @'Slice' 'From' ('Free' __k__) a@ with
-- @'end' h' '==' g@ holds:
--
--     (1) @lft h@ is 'valid'.
--
--     (2) @'orientation' (lft h) '==' 'start' h ':>' 'start' p@.
--
--     (3) @p 'M.*' lft h '==' h'@.
--
-- @
--             g'
--            ^ |
--           /  |
--   lft h  /   | p
--         /    |
--        /     v
--       * ---> g
--          h'
-- @
data Generator s a where
  GeneratorTo
    :: ( Attestable k', Sliced (Free k') a
       , Attestable k'', Sliced (Free k'') a
       )
    => Diagram (Chain To) N3 N2 a
    -> Free k' a
    -> Free k'' a
    -> Cokernel N1 a
    -> Kernel N1 a
    -> (forall (k :: N') . Slice From (Free k) a -> a)
    -> Generator To a

instance ( Distributive a, XStandardOrtSiteFrom a, XStandardOrtSiteTo a
         , XStandardSomeFreeSliceFromLiftable a
         )
  => Validable (Generator To a) where
  valid :: Generator 'To a -> Statement
valid gen :: Generator 'To 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 -> a
lft) = String -> Label
Label (forall a. Show a => a -> String
show forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Typeable a => a -> TypeRep
typeOf Generator 'To a
gen) Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ 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
:<=>: forall a (n :: N').
Distributive a =>
Cokernel n a -> FinList n a -> a -> Statement
prpIsCokernel Cokernel N1 a
coker (a
p'forall a (x :: N'). a -> FinList x a -> FinList (x + 1) a
:|forall a. FinList N0 a
Nil) a
p
        , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: forall a (n :: N').
Distributive a =>
Kernel n a -> FinList n a -> a -> Statement
prpIsKernel Kernel N1 a
ker (a
pforall a (x :: N'). a -> FinList x a -> FinList (x + 1) a
:|forall a. FinList N0 a
Nil) a
p'
        , String -> Label
Label String
"3" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid (forall (x :: N') c (i :: * -> *) (n :: N').
(Attestable x, Sliced (Free x) c) =>
Free x 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
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall (forall a.
XSomeFreeSliceFromLiftable a
-> Point a -> X (SomeFreeSlice 'From a)
xsfsfl forall a.
XStandardSomeFreeSliceFromLiftable a =>
XSomeFreeSliceFromLiftable a
xStandardSomeFreeSliceFromLiftable Point a
g)
          (\(SomeFreeSlice h :: Slice 'From (Free k) a
h@(SliceFrom Free k a
_ a
h'))
            -> let lh :: a
lh = forall (k :: N'). Slice 'From (Free k) a -> a
lft Slice 'From (Free k) a
h in
              [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid a
lh
                  , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
lh forall a. Eq a => a -> a -> Bool
== forall q. Oriented q => q -> Point q
start a
h' forall p. p -> p -> Orientation p
:> forall q. Oriented q => q -> Point q
start a
p) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params []
                  , String -> Label
Label String
"3" Label -> Statement -> Statement
:<=>: (a
p forall c. Multiplicative c => c -> c -> c
* a
lh forall a. Eq a => a -> a -> Bool
== a
h') Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"h'"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
h']
                  ]
          )

        ]

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

--------------------------------------------------------------------------------
-- 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
:<=>:
    forall x. X x -> (x -> Statement) -> Statement
Forall forall x. XStandard x => X x
xStandard
      (\Point a
p -> 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 [ forall a. Validable a => a -> Statement
valid Slice 'From (Free k) a
h
                    , (forall q. Oriented q => q -> Point q
end a
h' 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