{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Solidity.Event.Internal where
import Data.Kind (Type)
import Data.Proxy (Proxy (..))
import Data.Tagged (Tagged (..))
import Generics.SOP (I (..), NP (..), NS (..), SOP (..))
import GHC.TypeLits (CmpNat)
data HList :: [Type] -> Type where
HNil :: HList '[]
(:<) :: a -> HList as -> HList (a : as)
infixr 0 :<
class HListRep a xs | a -> xs, a -> xs where
toHList :: a -> HList xs
fromHList :: HList xs -> a
instance HListRep (NP I '[]) '[] where
toHList :: NP I '[] -> HList '[]
toHList NP I '[]
_ = HList '[]
HNil
fromHList :: HList '[] -> NP I '[]
fromHList HList '[]
_ = NP I '[]
forall k (a :: k -> *). NP a '[]
Nil
instance HListRep (NP I as) as => HListRep (NP I (a:as)) (a:as) where
toHList :: NP I (a : as) -> HList (a : as)
toHList (I x
a :* NP I xs
rest) = x
a x -> HList as -> HList (x : as)
forall a (as :: [*]). a -> HList as -> HList (a : as)
:< NP I xs -> HList as
forall a (xs :: [*]). HListRep a xs => a -> HList xs
toHList NP I xs
rest
fromHList :: HList (a : as) -> NP I (a : as)
fromHList (a
a :< HList as
rest) = a -> I a
forall a. a -> I a
I a
a I a -> NP I as -> NP I (a : as)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* HList as -> NP I as
forall a (xs :: [*]). HListRep a xs => HList xs -> a
fromHList HList as
rest
instance HListRep (NP f as') as => HListRep (SOP f '[as']) as where
toHList :: SOP f '[as'] -> HList as
toHList (SOP (Z NP f x
rep)) = NP f x -> HList as
forall a (xs :: [*]). HListRep a xs => a -> HList xs
toHList NP f x
rep
toHList SOP f '[as']
_ = [Char] -> HList as
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible branch"
fromHList :: HList as -> SOP f '[as']
fromHList = NS (NP f) '[as'] -> SOP f '[as']
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP (NS (NP f) '[as'] -> SOP f '[as'])
-> (HList as -> NS (NP f) '[as']) -> HList as -> SOP f '[as']
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP f as' -> NS (NP f) '[as']
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (NP f as' -> NS (NP f) '[as'])
-> (HList as -> NP f as') -> HList as -> NS (NP f) '[as']
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HList as -> NP f as'
forall a (xs :: [*]). HListRep a xs => HList xs -> a
fromHList
class Sort (xs :: [Type]) where
type Sort' xs :: [Type]
sort :: HList xs -> HList (Sort' xs)
instance Sort '[] where
type Sort' '[] = '[]
sort :: HList '[] -> HList (Sort' '[])
sort HList '[]
HNil = HList '[]
HList (Sort' '[])
HNil
instance (Sort xs, Insert x (Sort' xs)) => Sort (x : xs) where
type Sort' (x : xs) = Insert' x (Sort' xs)
sort :: HList (x : xs) -> HList (Sort' (x : xs))
sort (a
x :< HList as
xs) = a -> HList (Sort' xs) -> HList (Insert' a (Sort' xs))
forall x (xs :: [*]).
Insert x xs =>
x -> HList xs -> HList (Insert' x xs)
insert a
x (HList as -> HList (Sort' as)
forall (xs :: [*]). Sort xs => HList xs -> HList (Sort' xs)
sort HList as
xs)
class Insert (x :: Type) (xs :: [Type]) where
type Insert' x xs :: [Type]
insert :: x -> HList xs -> HList (Insert' x xs)
instance Insert x '[] where
type Insert' x '[] = '[x]
insert :: x -> HList '[] -> HList (Insert' x '[])
insert x
x HList '[]
HNil = x
x x -> HList '[] -> HList '[x]
forall a (as :: [*]). a -> HList as -> HList (a : as)
:< HList '[]
HNil
instance InsertCmp (CmpNat n m) (Tagged n x) (Tagged m y) ys => Insert (Tagged n x) (Tagged m y : ys) where
type Insert' (Tagged n x) (Tagged m y : ys) = InsertCmp' (CmpNat n m) (Tagged n x) (Tagged m y) ys
insert :: Tagged n x
-> HList (Tagged m y : ys)
-> HList (Insert' (Tagged n x) (Tagged m y : ys))
insert (Tagged n x
x :: Tagged n x) ((y :: Tagged m y) :< HList as
ys) = Proxy (CmpNat n m)
-> Tagged n x
-> Tagged m y
-> HList as
-> HList (InsertCmp' (CmpNat n m) (Tagged n x) (Tagged m y) as)
forall (b :: Ordering) x y (ys :: [*]).
InsertCmp b x y ys =>
Proxy b -> x -> y -> HList ys -> HList (InsertCmp' b x y ys)
insertCmp (Proxy (CmpNat n m)
forall k (t :: k). Proxy t
Proxy :: Proxy (CmpNat n m)) Tagged n x
x Tagged m y
y HList as
ys
class InsertCmp (b :: Ordering) (x :: Type) (y :: Type) (ys :: [Type]) where
type InsertCmp' b x y ys :: [Type]
insertCmp :: Proxy (b :: Ordering) -> x -> y -> HList ys -> HList (InsertCmp' b x y ys)
instance InsertCmp 'LT x y ys where
type InsertCmp' 'LT x y ys = x : (y : ys)
insertCmp :: Proxy 'LT -> x -> y -> HList ys -> HList (InsertCmp' 'LT x y ys)
insertCmp Proxy 'LT
_ x
x y
y HList ys
ys = x
x x -> HList (y : ys) -> HList (x : y : ys)
forall a (as :: [*]). a -> HList as -> HList (a : as)
:< y
y y -> HList ys -> HList (y : ys)
forall a (as :: [*]). a -> HList as -> HList (a : as)
:< HList ys
ys
instance Insert x ys => InsertCmp 'GT x y ys where
type InsertCmp' 'GT x y ys = y : Insert' x ys
insertCmp :: Proxy 'GT -> x -> y -> HList ys -> HList (InsertCmp' 'GT x y ys)
insertCmp Proxy 'GT
_ x
x y
y HList ys
ys = y
y y -> HList (Insert' x ys) -> HList (y : Insert' x ys)
forall a (as :: [*]). a -> HList as -> HList (a : as)
:< x -> HList ys -> HList (Insert' x ys)
forall x (xs :: [*]).
Insert x xs =>
x -> HList xs -> HList (Insert' x xs)
insert x
x HList ys
ys
class UnTag t where
type UnTag' t :: [Type]
unTag :: HList t -> HList (UnTag' t)
instance UnTag '[] where
type UnTag' '[] = '[]
unTag :: HList '[] -> HList (UnTag' '[])
unTag HList '[]
a = HList '[]
HList (UnTag' '[])
a
instance UnTag ts => UnTag (Tagged n a : ts) where
type UnTag' (Tagged n a : ts) = a : UnTag' ts
unTag :: HList (Tagged n a : ts) -> HList (UnTag' (Tagged n a : ts))
unTag (Tagged a :< HList as
ts) = a
a a -> HList (UnTag' ts) -> HList (a : UnTag' ts)
forall a (as :: [*]). a -> HList as -> HList (a : as)
:< HList as -> HList (UnTag' as)
forall (t :: [*]). UnTag t => HList t -> HList (UnTag' t)
unTag HList as
ts
class HListMerge (as :: [Type]) (bs :: [Type]) where
type Concat as bs :: [Type]
mergeHList :: HList as -> HList bs -> HList (Concat as bs)
instance HListMerge '[] bs where
type Concat '[] bs = bs
mergeHList :: HList '[] -> HList bs -> HList (Concat '[] bs)
mergeHList HList '[]
_ HList bs
bs = HList bs
HList (Concat '[] bs)
bs
instance HListMerge as bs => HListMerge (a : as) bs where
type Concat (a : as) bs = a : Concat as bs
mergeHList :: HList (a : as) -> HList bs -> HList (Concat (a : as) bs)
mergeHList (a
a :< HList as
as) HList bs
bs = a
a a -> HList (Concat as bs) -> HList (a : Concat as bs)
forall a (as :: [*]). a -> HList as -> HList (a : as)
:< HList as -> HList bs -> HList (Concat as bs)
forall (as :: [*]) (bs :: [*]).
HListMerge as bs =>
HList as -> HList bs -> HList (Concat as bs)
mergeHList HList as
as HList bs
bs
class HListMergeSort as bs where
type MergeSort' as bs :: [Type]
mergeSortHList :: HList as -> HList bs -> HList (MergeSort' as bs)
instance (HListMerge as bs, Concat as bs ~ cs, Sort cs, Sort' cs ~ cs') => HListMergeSort as bs where
type MergeSort' as bs = Sort' (Concat as bs)
mergeSortHList :: HList as -> HList bs -> HList (MergeSort' as bs)
mergeSortHList HList as
as HList bs
bs = HList cs -> HList (Sort' cs)
forall (xs :: [*]). Sort xs => HList xs -> HList (Sort' xs)
sort (HList cs -> HList (Sort' cs)) -> HList cs -> HList (Sort' cs)
forall a b. (a -> b) -> a -> b
$ (HList as -> HList bs -> HList (Concat as bs)
forall (as :: [*]) (bs :: [*]).
HListMerge as bs =>
HList as -> HList bs -> HList (Concat as bs)
mergeHList HList as
as HList bs
bs :: HList cs)
class MergeIndexedArguments as bs where
type MergeIndexedArguments' as bs :: [Type]
mergeIndexedArguments :: HList as -> HList bs -> HList (MergeIndexedArguments' as bs)
instance (HListMergeSort as bs, MergeSort' as bs ~ cs, UnTag cs, UnTag cs' ~ ds) => MergeIndexedArguments as bs where
type MergeIndexedArguments' as bs = (UnTag' (MergeSort' as bs))
mergeIndexedArguments :: HList as -> HList bs -> HList (MergeIndexedArguments' as bs)
mergeIndexedArguments HList as
as HList bs
bs = HList cs -> HList (UnTag' cs)
forall (t :: [*]). UnTag t => HList t -> HList (UnTag' t)
unTag (HList cs -> HList (UnTag' cs)) -> HList cs -> HList (UnTag' cs)
forall a b. (a -> b) -> a -> b
$ HList as -> HList bs -> HList (MergeSort' as bs)
forall (as :: [*]) (bs :: [*]).
HListMergeSort as bs =>
HList as -> HList bs -> HList (MergeSort' as bs)
mergeSortHList HList as
as HList bs
bs