{-# 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 9 :*

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