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

-- | Intended for qualified import
--
-- > import Ouroboros.Consensus.HardFork.Combinator.Util.InPairs (InPairs(..))
-- > import qualified Ouroboros.Consensus.HardFork.Combinator.Util.InPairs as InPairs
module Ouroboros.Consensus.HardFork.Combinator.Util.InPairs (
    -- * InPairs
    InPairs (..)
    -- * Convenience constructors
  , mk1
  , mk2
  , mk3
    -- * SOP-like operators
  , hcmap
  , hcpure
  , hmap
  , hpure
    -- * Requiring
  , Requiring (..)
  , RequiringBoth (..)
  , ignoring
  , ignoringBoth
  , requiring
  , requiringBoth
  ) where

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

import           Ouroboros.Consensus.Util.SOP

{-------------------------------------------------------------------------------
  InPairs
-------------------------------------------------------------------------------}

-- | We have an @f x y@ for each pair @(x, y)@ of successive list elements
data InPairs (f :: k -> k -> Type) (xs :: [k]) where
  PNil  :: InPairs f '[x]
  PCons :: f x y -> InPairs f (y ': zs) -> InPairs f (x ': y ': zs)

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

mk1 :: InPairs f '[x]
mk1 :: InPairs f '[x]
mk1 = InPairs f '[x]
forall k (f :: k -> k -> *) (x :: k). InPairs f '[x]
PNil

mk2 :: f x y -> InPairs f '[x, y]
mk2 :: f x y -> InPairs f '[x, y]
mk2 f x y
xy = f x y -> InPairs f '[y] -> InPairs f '[x, y]
forall a (f :: a -> a -> *) (x :: a) (y :: a) (zs :: [a]).
f x y -> InPairs f (y : zs) -> InPairs f (x : y : zs)
PCons f x y
xy InPairs f '[y]
forall k (f :: k -> k -> *) (x :: k). InPairs f '[x]
mk1

mk3 :: f x y -> f y z -> InPairs f '[x, y, z]
mk3 :: f x y -> f y z -> InPairs f '[x, y, z]
mk3 f x y
xy f y z
yz = f x y -> InPairs f '[y, z] -> InPairs f '[x, y, z]
forall a (f :: a -> a -> *) (x :: a) (y :: a) (zs :: [a]).
f x y -> InPairs f (y : zs) -> InPairs f (x : y : zs)
PCons f x y
xy (f y z -> InPairs f '[y, z]
forall k (f :: k -> k -> *) (x :: k) (y :: k).
f x y -> InPairs f '[x, y]
mk2 f y z
yz)

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

hmap :: SListI xs => (forall x y. f x y -> g x y) -> InPairs f xs -> InPairs g xs
hmap :: (forall (x :: k) (y :: k). f x y -> g x y)
-> InPairs f xs -> InPairs g xs
hmap = Proxy Top
-> (forall (x :: k) (y :: k). (Top x, Top y) => f x y -> g x y)
-> InPairs f xs
-> InPairs 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)
-> InPairs f xs
-> InPairs 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)
      -> InPairs f xs -> InPairs g xs
hcmap :: proxy c
-> (forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y)
-> InPairs f xs
-> InPairs g xs
hcmap proxy c
_ forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y
f = InPairs f xs -> InPairs g xs
forall (xs' :: [k]). All c xs' => InPairs f xs' -> InPairs g xs'
go
  where
    go :: All c xs' => InPairs f xs' -> InPairs g xs'
    go :: InPairs f xs' -> InPairs g xs'
go InPairs f xs'
PNil         = InPairs g xs'
forall k (f :: k -> k -> *) (x :: k). InPairs f '[x]
PNil
    go (PCons f x y
x InPairs f (y : zs)
xs) = g x y -> InPairs g (y : zs) -> InPairs g (x : y : zs)
forall a (f :: a -> a -> *) (x :: a) (y :: a) (zs :: [a]).
f x y -> InPairs f (y : zs) -> InPairs f (x : y : zs)
PCons (f x y -> g x y
forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y
f f x y
x) (InPairs f (y : zs) -> InPairs g (y : zs)
forall (xs' :: [k]). All c xs' => InPairs f xs' -> InPairs g xs'
go InPairs f (y : zs)
xs)

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

hcpure :: forall proxy c xs f. (All c xs, IsNonEmpty xs)
       => proxy c
       -> (forall x y. (c x, c y) => f x y) -> InPairs f xs
hcpure :: proxy c
-> (forall (x :: k) (y :: k). (c x, c y) => f x y) -> InPairs f xs
hcpure proxy c
_ forall (x :: k) (y :: k). (c x, c y) => f x y
f =
    case Proxy xs -> ProofNonEmpty xs
forall a (xs :: [a]) (proxy :: [a] -> *).
IsNonEmpty xs =>
proxy xs -> ProofNonEmpty xs
isNonEmpty (Proxy xs
forall k (t :: k). Proxy t
Proxy @xs) of
      ProofNonEmpty {} -> SList xs -> InPairs f (x : xs)
forall (x :: k) (xs' :: [k]).
(c x, All c xs') =>
SList xs' -> InPairs f (x : xs')
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: (c x, All c xs') => SList xs' -> InPairs f (x ': xs')
    go :: SList xs' -> InPairs f (x : xs')
go SList xs'
SNil  = InPairs f (x : xs')
forall k (f :: k -> k -> *) (x :: k). InPairs f '[x]
PNil
    go SList xs'
SCons = f x x -> InPairs f (x : xs) -> InPairs f (x : x : xs)
forall a (f :: a -> a -> *) (x :: a) (y :: a) (zs :: [a]).
f x y -> InPairs f (y : zs) -> InPairs f (x : y : zs)
PCons f x x
forall (x :: k) (y :: k). (c x, c y) => f x y
f (SList xs -> InPairs f (x : xs)
forall (x :: k) (xs' :: [k]).
(c x, All c xs') =>
SList xs' -> InPairs f (x : xs')
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList)

{-------------------------------------------------------------------------------
  RequiringBoth
-------------------------------------------------------------------------------}

data Requiring h f x y = Require {
      Requiring h f x y -> h x -> f x y
provide :: h x -> f x y
    }

data RequiringBoth h f x y = RequireBoth {
      RequiringBoth h f x y -> h x -> h y -> f x y
provideBoth :: h x -> h y -> f x y
    }

ignoring :: f x y -> Requiring h f x y
ignoring :: f x y -> Requiring h f x y
ignoring f x y
fxy = (h x -> f x y) -> Requiring h f x y
forall k k (h :: k -> *) (f :: k -> k -> *) (x :: k) (y :: k).
(h x -> f x y) -> Requiring h f x y
Require ((h x -> f x y) -> Requiring h f x y)
-> (h x -> f x y) -> Requiring h f x y
forall a b. (a -> b) -> a -> b
$ \h x
_ -> f x y
fxy

ignoringBoth :: f x y -> RequiringBoth h f x y
ignoringBoth :: f x y -> RequiringBoth h f x y
ignoringBoth f x y
fxy = (h x -> h y -> f x y) -> RequiringBoth h f x y
forall k (h :: k -> *) (f :: k -> k -> *) (x :: k) (y :: k).
(h x -> h y -> f x y) -> RequiringBoth h f x y
RequireBoth ((h x -> h y -> f x y) -> RequiringBoth h f x y)
-> (h x -> h y -> f x y) -> RequiringBoth h f x y
forall a b. (a -> b) -> a -> b
$ \h x
_ h y
_ -> f x y
fxy

requiring :: SListI xs => NP h xs -> InPairs (Requiring h f) xs -> InPairs f xs
requiring :: NP h xs -> InPairs (Requiring h f) xs -> InPairs f xs
requiring NP h xs
np =
      NP h xs -> InPairs (RequiringBoth h f) xs -> InPairs f xs
forall k (h :: k -> *) (xs :: [k]) (f :: k -> k -> *).
NP h xs -> InPairs (RequiringBoth h f) xs -> InPairs f xs
requiringBoth NP h xs
np
    (InPairs (RequiringBoth h f) xs -> InPairs f xs)
-> (InPairs (Requiring h f) xs -> InPairs (RequiringBoth h f) xs)
-> InPairs (Requiring h f) xs
-> InPairs f xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: k) (y :: k).
 Requiring h f x y -> RequiringBoth h f x y)
-> InPairs (Requiring h f) xs -> InPairs (RequiringBoth h f) xs
forall k (xs :: [k]) (f :: k -> k -> *) (g :: k -> k -> *).
SListI xs =>
(forall (x :: k) (y :: k). f x y -> g x y)
-> InPairs f xs -> InPairs g xs
hmap (\Requiring h f x y
f -> (h x -> h y -> f x y) -> RequiringBoth h f x y
forall k (h :: k -> *) (f :: k -> k -> *) (x :: k) (y :: k).
(h x -> h y -> f x y) -> RequiringBoth h f x y
RequireBoth ((h x -> h y -> f x y) -> RequiringBoth h f x y)
-> (h x -> h y -> f x y) -> RequiringBoth h f x y
forall a b. (a -> b) -> a -> b
$ \h x
hx h y
_hy -> Requiring h f x y -> h x -> f x y
forall k (h :: k -> *) k (f :: k -> k -> *) (x :: k) (y :: k).
Requiring h f x y -> h x -> f x y
provide Requiring h f x y
f h x
hx)

requiringBoth :: NP h xs -> InPairs (RequiringBoth h f) xs -> InPairs f xs
requiringBoth :: NP h xs -> InPairs (RequiringBoth h f) xs -> InPairs f xs
requiringBoth = (InPairs (RequiringBoth h f) xs -> NP h xs -> InPairs f xs)
-> NP h xs -> InPairs (RequiringBoth h f) xs -> InPairs f xs
forall a b c. (a -> b -> c) -> b -> a -> c
flip InPairs (RequiringBoth h f) xs -> NP h xs -> InPairs f xs
forall k (h :: k -> *) (f :: k -> k -> *) (xs :: [k]).
InPairs (RequiringBoth h f) xs -> NP h xs -> InPairs f xs
go
  where
    go :: InPairs (RequiringBoth h f) xs -> NP h xs -> InPairs f xs
    go :: InPairs (RequiringBoth h f) xs -> NP h xs -> InPairs f xs
go InPairs (RequiringBoth h f) xs
PNil         NP h xs
_              = InPairs f xs
forall k (f :: k -> k -> *) (x :: k). InPairs f '[x]
PNil
    go (PCons RequiringBoth h f x y
f InPairs (RequiringBoth h f) (y : zs)
fs) (h x
x :* h x
y :* NP h xs
zs) = f x y -> InPairs f (y : zs) -> InPairs f (x : y : zs)
forall a (f :: a -> a -> *) (x :: a) (y :: a) (zs :: [a]).
f x y -> InPairs f (y : zs) -> InPairs f (x : y : zs)
PCons (RequiringBoth h f x y -> h x -> h y -> f x y
forall k (h :: k -> *) (f :: k -> k -> *) (x :: k) (y :: k).
RequiringBoth h f x y -> h x -> h y -> f x y
provideBoth RequiringBoth h f x y
f h x
h x
x h y
h x
y) (InPairs (RequiringBoth h f) (y : zs)
-> NP h (y : zs) -> InPairs f (y : zs)
forall k (h :: k -> *) (f :: k -> k -> *) (xs :: [k]).
InPairs (RequiringBoth h f) xs -> NP h xs -> InPairs f xs
go InPairs (RequiringBoth h f) (y : zs)
fs (h x
y h x -> NP h xs -> NP h (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* NP h xs
zs))