{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Heterogeneous lists
--
-- Intended for qualified import
module Ouroboros.Consensus.Util.HList (
    -- * Basic definitions
    All
  , HList (..)
    -- * Folding
  , collapse
  , foldMap
  , foldl
  , foldlM
  , foldr
  , repeatedly
  , repeatedlyM
    -- * Singletons
  , IsList (..)
  , SList
    -- * n-ary functions
  , Fn
  , afterFn
  , applyFn
  ) where

import           Data.Kind (Constraint, Type)
import           Data.Proxy
import           Prelude hiding (foldMap, foldl, foldr)

{-------------------------------------------------------------------------------
  Basic definitions
-------------------------------------------------------------------------------}

data HList :: [Type] -> Type where
  Nil  :: HList '[]
  (:*) :: a -> HList as -> HList (a ': as)

infixr :*

type family All c as :: Constraint where
  All c '[]       = ()
  All c (a ': as) = (c a, All c as)

instance All Show as => Show (HList as) where
  show :: HList as -> String
show = [String] -> String
forall a. Show a => a -> String
show ([String] -> String)
-> (HList as -> [String]) -> HList as -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy Show
-> (forall a. Show a => a -> String) -> HList as -> [String]
forall (c :: * -> Constraint) (as :: [*]) b
       (proxy :: (* -> Constraint) -> *).
All c as =>
proxy c -> (forall a. c a => a -> b) -> HList as -> [b]
collapse (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @Show) a -> String
forall a. Show a => a -> String
show

instance (IsList as, All Eq as) => Eq (HList as) where
    == :: HList as -> HList as -> Bool
(==) = SList as -> HList as -> HList as -> Bool
forall (bs :: [*]).
All Eq bs =>
SList bs -> HList bs -> HList bs -> Bool
eq SList as
forall (xs :: [*]). IsList xs => SList xs
isList
      where
        eq :: All Eq bs => SList bs -> HList bs -> HList bs -> Bool
        eq :: forall (bs :: [*]).
All Eq bs =>
SList bs -> HList bs -> HList bs -> Bool
eq SList bs
SNil      HList bs
_         HList bs
_         = Bool
True
        eq (SCons SList as
s) (a
x :* HList as
xs) (a
y :* HList as
ys) = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a
y Bool -> Bool -> Bool
&& SList as -> HList as -> HList as -> Bool
forall (bs :: [*]).
All Eq bs =>
SList bs -> HList bs -> HList bs -> Bool
eq SList as
s HList as
HList as
xs HList as
HList as
ys

instance (IsList as, All Eq as, All Ord as) => Ord (HList as) where
    compare :: HList as -> HList as -> Ordering
compare = SList as -> HList as -> HList as -> Ordering
forall (bs :: [*]).
All Ord bs =>
SList bs -> HList bs -> HList bs -> Ordering
cmp SList as
forall (xs :: [*]). IsList xs => SList xs
isList
      where
        cmp :: All Ord bs => SList bs -> HList bs -> HList bs -> Ordering
        cmp :: forall (bs :: [*]).
All Ord bs =>
SList bs -> HList bs -> HList bs -> Ordering
cmp SList bs
SNil      HList bs
_         HList bs
_         = Ordering
EQ
        cmp (SCons SList as
s) (a
x :* HList as
xs) (a
y :* HList as
ys) = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
a
y Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> SList as -> HList as -> HList as -> Ordering
forall (bs :: [*]).
All Ord bs =>
SList bs -> HList bs -> HList bs -> Ordering
cmp SList as
s HList as
HList as
xs HList as
HList as
ys

{-------------------------------------------------------------------------------
  Folding
-------------------------------------------------------------------------------}

foldl :: forall c as b proxy. All c as
      => proxy c
      -> (forall a. c a => b -> a -> b) -> b -> HList as -> b
foldl :: forall (c :: * -> Constraint) (as :: [*]) b
       (proxy :: (* -> Constraint) -> *).
All c as =>
proxy c -> (forall a. c a => b -> a -> b) -> b -> HList as -> b
foldl proxy c
_ forall a. c a => b -> a -> b
f = b -> HList as -> b
forall (as' :: [*]). All c as' => b -> HList as' -> b
go
  where
    go :: All c as' => b -> HList as' -> b
    go :: forall (as' :: [*]). All c as' => b -> HList as' -> b
go !b
acc HList as'
Nil       = b
acc
    go !b
acc (a
a :* HList as
as) = b -> HList as -> b
forall (as' :: [*]). All c as' => b -> HList as' -> b
go (b -> a -> b
forall a. c a => b -> a -> b
f b
acc a
a) HList as
as

foldlM :: forall c as m b proxy. (All c as, Monad m)
       => proxy c
       -> (forall a. c a => b -> a -> m b) -> b -> HList as -> m b
foldlM :: forall (c :: * -> Constraint) (as :: [*]) (m :: * -> *) b
       (proxy :: (* -> Constraint) -> *).
(All c as, Monad m) =>
proxy c -> (forall a. c a => b -> a -> m b) -> b -> HList as -> m b
foldlM proxy c
_ forall a. c a => b -> a -> m b
f = b -> HList as -> m b
forall (as' :: [*]). All c as' => b -> HList as' -> m b
go
  where
    go :: All c as' => b -> HList as' -> m b
    go :: forall (as' :: [*]). All c as' => b -> HList as' -> m b
go !b
acc HList as'
Nil       = b -> m b
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return b
acc
    go !b
acc (a
a :* HList as
as) = b -> a -> m b
forall a. c a => b -> a -> m b
f b
acc a
a m b -> (b -> m b) -> m b
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b
acc' -> b -> HList as -> m b
forall (as' :: [*]). All c as' => b -> HList as' -> m b
go b
acc' HList as
as

foldr :: forall c as b proxy. All c as
      => proxy c
      -> (forall a. c a => a -> b -> b) -> b -> HList as -> b
foldr :: forall (c :: * -> Constraint) (as :: [*]) b
       (proxy :: (* -> Constraint) -> *).
All c as =>
proxy c -> (forall a. c a => a -> b -> b) -> b -> HList as -> b
foldr proxy c
_ forall a. c a => a -> b -> b
f b
e = HList as -> b
forall (as' :: [*]). All c as' => HList as' -> b
go
  where
    go :: All c as' => HList as' -> b
    go :: forall (as' :: [*]). All c as' => HList as' -> b
go HList as'
Nil       = b
e
    go (a
a :* HList as
as) = a -> b -> b
forall a. c a => a -> b -> b
f a
a (HList as -> b
forall (as' :: [*]). All c as' => HList as' -> b
go HList as
as)

foldMap :: forall c as b proxy. (All c as, Monoid b)
        => proxy c
        -> (forall a. c a => a -> b)
        -> HList as
        -> b
foldMap :: forall (c :: * -> Constraint) (as :: [*]) b
       (proxy :: (* -> Constraint) -> *).
(All c as, Monoid b) =>
proxy c -> (forall a. c a => a -> b) -> HList as -> b
foldMap proxy c
p forall a. c a => a -> b
f = proxy c -> (forall a. c a => b -> a -> b) -> b -> HList as -> b
forall (c :: * -> Constraint) (as :: [*]) b
       (proxy :: (* -> Constraint) -> *).
All c as =>
proxy c -> (forall a. c a => b -> a -> b) -> b -> HList as -> b
foldl proxy c
p (\b
b a
a -> b
b b -> b -> b
forall a. Semigroup a => a -> a -> a
<> a -> b
forall a. c a => a -> b
f a
a) b
forall a. Monoid a => a
mempty

-- | Apply function repeatedly for all elements of the list
--
-- > repeatedly p = flip . foldl p . flip
repeatedly :: forall c as b proxy. All c as
           => proxy c
           -> (forall a. c a => a -> b -> b) -> (HList as -> b -> b)
repeatedly :: forall (c :: * -> Constraint) (as :: [*]) b
       (proxy :: (* -> Constraint) -> *).
All c as =>
proxy c -> (forall a. c a => a -> b -> b) -> HList as -> b -> b
repeatedly proxy c
p forall a. c a => a -> b -> b
f HList as
as b
e = proxy c -> (forall a. c a => b -> a -> b) -> b -> HList as -> b
forall (c :: * -> Constraint) (as :: [*]) b
       (proxy :: (* -> Constraint) -> *).
All c as =>
proxy c -> (forall a. c a => b -> a -> b) -> b -> HList as -> b
foldl proxy c
p (\b
b a
a -> a -> b -> b
forall a. c a => a -> b -> b
f a
a b
b) b
e HList as
as

repeatedlyM :: forall c as b proxy m. (Monad m, All c as)
            => proxy c
            -> (forall a. c a => a -> b -> m b) -> (HList as -> b -> m b)
repeatedlyM :: forall (c :: * -> Constraint) (as :: [*]) b
       (proxy :: (* -> Constraint) -> *) (m :: * -> *).
(Monad m, All c as) =>
proxy c -> (forall a. c a => a -> b -> m b) -> HList as -> b -> m b
repeatedlyM proxy c
p forall a. c a => a -> b -> m b
f HList as
as b
e = proxy c -> (forall a. c a => b -> a -> m b) -> b -> HList as -> m b
forall (c :: * -> Constraint) (as :: [*]) (m :: * -> *) b
       (proxy :: (* -> Constraint) -> *).
(All c as, Monad m) =>
proxy c -> (forall a. c a => b -> a -> m b) -> b -> HList as -> m b
foldlM proxy c
p (\b
b a
a -> a -> b -> m b
forall a. c a => a -> b -> m b
f a
a b
b) b
e HList as
as

collapse :: forall c as b proxy. All c as
         => proxy c
         -> (forall a. c a => a -> b) -> HList as -> [b]
collapse :: forall (c :: * -> Constraint) (as :: [*]) b
       (proxy :: (* -> Constraint) -> *).
All c as =>
proxy c -> (forall a. c a => a -> b) -> HList as -> [b]
collapse proxy c
_ forall a. c a => a -> b
f = HList as -> [b]
forall (as' :: [*]). All c as' => HList as' -> [b]
go
  where
    go :: All c as' => HList as' -> [b]
    go :: forall (as' :: [*]). All c as' => HList as' -> [b]
go HList as'
Nil       = []
    go (a
a :* HList as
as) = a -> b
forall a. c a => a -> b
f a
a b -> [b] -> [b]
forall a. a -> [a] -> [a]
: HList as -> [b]
forall (as' :: [*]). All c as' => HList as' -> [b]
go HList as
as

{-------------------------------------------------------------------------------
  Singleton for HList
-------------------------------------------------------------------------------}

data SList :: [Type] -> Type where
  SNil :: SList '[]
  SCons :: SList as -> SList (a ': as)

class IsList (xs :: [Type]) where
  isList :: SList xs

instance              IsList '[]       where isList :: SList '[]
isList = SList '[]
SNil
instance IsList as => IsList (a ': as) where isList :: SList (a : as)
isList = SList as -> SList (a : as)
forall (as :: [*]) a. SList as -> SList (a : as)
SCons SList as
forall (xs :: [*]). IsList xs => SList xs
isList

{-------------------------------------------------------------------------------
  n-ary functions
-------------------------------------------------------------------------------}

type family Fn as b where
  Fn '[]       b = b
  Fn (a ': as) b = a -> Fn as b

withArgs :: HList as -> Fn as b -> b
withArgs :: forall (as :: [*]) b. HList as -> Fn as b -> b
withArgs HList as
Nil       Fn as b
b = b
Fn as b
b
withArgs (a
a :* HList as
as) Fn as b
f = HList as -> Fn as b -> b
forall (as :: [*]) b. HList as -> Fn as b -> b
withArgs HList as
as (Fn as b
a -> Fn as b
f a
a)

applyFn :: Fn as b -> HList as -> b
applyFn :: forall (as :: [*]) b. Fn as b -> HList as -> b
applyFn = (HList as -> Fn as b -> b) -> Fn as b -> HList as -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip HList as -> Fn as b -> b
forall (as :: [*]) b. HList as -> Fn as b -> b
withArgs

afterFn :: SList as -> (b -> c) -> Fn as b -> Fn as c
afterFn :: forall (as :: [*]) b c. SList as -> (b -> c) -> Fn as b -> Fn as c
afterFn SList as
SNil       b -> c
g Fn as b
b = b -> c
g b
Fn as b
b
afterFn (SCons SList as
ss) b -> c
g Fn as b
f = SList as -> (b -> c) -> Fn as b -> Fn as c
forall (as :: [*]) b c. SList as -> (b -> c) -> Fn as b -> Fn as c
afterFn SList as
ss b -> c
g (Fn as b -> Fn as c) -> (a -> Fn as b) -> a -> Fn as c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fn as b
a -> Fn as b
f