{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeOperators       #-}

-- > import Ouroboros.Consensus.HardFork.Combinator.Util.Tails (Tails(..))
-- > import qualified Ouroboros.Consensus.HardFork.Combinator.Util.Tails as Tails
module Ouroboros.Consensus.HardFork.Combinator.Util.Tails (
    Tails (..)
    -- * Convenience constructors
  , mk1
  , mk2
  , mk3
    -- * SOP-like operators
  , hcmap
  , hcpure
  , hmap
  , hpure
  ) where

import           Data.Kind (Type)
import           Data.SOP.Strict hiding (hcmap, hcpure, hmap, hpure)
import qualified Data.SOP.Strict as SOP

{-------------------------------------------------------------------------------
  Tails
-------------------------------------------------------------------------------}

-- | For every tail @(x ': xs)@ of the list, an @f x y@ for every @y@ in @xs@
data Tails (f :: k -> k -> Type) (xs :: [k]) where
  TNil  :: Tails f '[]
  TCons :: NP (f x) xs -> Tails f xs -> Tails f (x ': xs)

{-------------------------------------------------------------------------------
  Convenience constructors
-------------------------------------------------------------------------------}

mk1 :: Tails f '[x]
mk1 :: Tails f '[x]
mk1 = NP (f x) '[] -> Tails f '[] -> Tails f '[x]
forall a (f :: a -> a -> *) (x :: a) (xs :: [a]).
NP (f x) xs -> Tails f xs -> Tails f (x : xs)
TCons NP (f x) '[]
forall k (f :: k -> *). NP f '[]
Nil Tails f '[]
forall k (f :: k -> k -> *). Tails f '[]
TNil

mk2 :: f x y -> Tails f '[x, y]
mk2 :: f x y -> Tails f '[x, y]
mk2 f x y
xy = NP (f x) '[y] -> Tails f '[y] -> Tails f '[x, y]
forall a (f :: a -> a -> *) (x :: a) (xs :: [a]).
NP (f x) xs -> Tails f xs -> Tails f (x : xs)
TCons (f x y
xy f x y -> NP (f x) '[] -> NP (f x) '[y]
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* NP (f x) '[]
forall k (f :: k -> *). NP f '[]
Nil) Tails f '[y]
forall k (f :: k -> k -> *) (x :: k). Tails f '[x]
mk1

mk3 :: f x y -> f x z -> f y z -> Tails f '[x, y, z]
mk3 :: f x y -> f x z -> f y z -> Tails f '[x, y, z]
mk3 f x y
xy f x z
xz f y z
yz = NP (f x) '[y, z] -> Tails f '[y, z] -> Tails f '[x, y, z]
forall a (f :: a -> a -> *) (x :: a) (xs :: [a]).
NP (f x) xs -> Tails f xs -> Tails f (x : xs)
TCons (f x y
xy f x y -> NP (f x) '[z] -> NP (f x) '[y, z]
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* f x z
xz f x z -> NP (f x) '[] -> NP (f x) '[z]
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* NP (f x) '[]
forall k (f :: k -> *). NP f '[]
Nil) (f y z -> Tails f '[y, z]
forall k (f :: k -> k -> *) (x :: k) (y :: k).
f x y -> Tails f '[x, y]
mk2 f y z
yz)

{-------------------------------------------------------------------------------
  SOP-like operators
-------------------------------------------------------------------------------}

hmap :: SListI xs
     => (forall x y. f x y -> g x y)
     -> Tails f xs -> Tails g xs
hmap :: (forall (x :: k) (y :: k). f x y -> g x y)
-> Tails f xs -> Tails g xs
hmap = Proxy Top
-> (forall (x :: k) (y :: k). (Top x, Top y) => f x y -> g x y)
-> Tails f xs
-> Tails g xs
forall k (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint)
       (f :: k -> k -> *) (g :: k -> k -> *) (xs :: [k]).
All c xs =>
proxy c
-> (forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y)
-> Tails f xs
-> Tails g xs
hcmap (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top)

hcmap :: forall proxy c f g xs. All c xs
      => proxy c
      -> (forall x y. (c x, c y) => f x y -> g x y)
      -> Tails f xs -> Tails g xs
hcmap :: proxy c
-> (forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y)
-> Tails f xs
-> Tails g xs
hcmap proxy c
p forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y
g = Tails f xs -> Tails g xs
forall (xs' :: [k]). All c xs' => Tails f xs' -> Tails g xs'
go
  where
    go :: All c xs' => Tails f xs' -> Tails g xs'
    go :: Tails f xs' -> Tails g xs'
go Tails f xs'
TNil           = Tails g xs'
forall k (f :: k -> k -> *). Tails f '[]
TNil
    go (TCons NP (f x) xs
fs Tails f xs
fss) = NP (g x) xs -> Tails g xs -> Tails g (x : xs)
forall a (f :: a -> a -> *) (x :: a) (xs :: [a]).
NP (f x) xs -> Tails f xs -> Tails f (x : xs)
TCons (proxy c
-> (forall (a :: k). c a => f x a -> g x a)
-> NP (f x) xs
-> NP (g x) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
SOP.hcmap proxy c
p forall (a :: k). c a => f x a -> g x a
forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y
g NP (f x) xs
fs) (Tails f xs -> Tails g xs
forall (xs' :: [k]). All c xs' => Tails f xs' -> Tails g xs'
go Tails f xs
fss)

hpure :: SListI xs => (forall x y. f x y) -> Tails f xs
hpure :: (forall (x :: k) (y :: k). f x y) -> Tails f xs
hpure = Proxy Top
-> (forall (x :: k) (y :: k). (Top x, Top y) => f x y)
-> Tails f xs
forall k (proxy :: (k -> Constraint) -> *) (f :: k -> k -> *)
       (c :: k -> Constraint) (xs :: [k]).
All c xs =>
proxy c
-> (forall (x :: k) (y :: k). (c x, c y) => f x y) -> Tails f xs
hcpure (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top)

hcpure :: forall proxy f c xs. All c xs
       => proxy c
       -> (forall x y. (c x, c y) => f x y) -> Tails f xs
hcpure :: proxy c
-> (forall (x :: k) (y :: k). (c x, c y) => f x y) -> Tails f xs
hcpure proxy c
p forall (x :: k) (y :: k). (c x, c y) => f x y
f = SList xs -> Tails f xs
forall (xs' :: [k]). All c xs' => SList xs' -> Tails f xs'
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: All c xs' => SList xs' -> Tails f xs'
    go :: SList xs' -> Tails f xs'
go SList xs'
SNil  = Tails f xs'
forall k (f :: k -> k -> *). Tails f '[]
TNil
    go SList xs'
SCons = NP (f x) xs -> Tails f xs -> Tails f (x : xs)
forall a (f :: a -> a -> *) (x :: a) (xs :: [a]).
NP (f x) xs -> Tails f xs -> Tails f (x : xs)
TCons (proxy c -> (forall (a :: k). c a => f x a) -> NP (f x) xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
SOP.hcpure proxy c
p forall (a :: k). c a => f x a
forall (x :: k) (y :: k). (c x, c y) => f x y
f) (SList xs -> Tails f xs
forall (xs' :: [k]). All c xs' => SList xs' -> Tails f xs'
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList)