module HListExtras where
import Data.HList.CommonMain
data FApply = FApply
instance (ApplyAB f a b, ab ~ (a -> b)) => ApplyAB FApply f ab where
applyAB _ = applyAB
class HReplicate2 (n ::HNat) e l | n e -> l, l -> n
where hReplicate2 :: Proxy n -> e -> HList l
instance HReplicate2 HZero e '[] where
hReplicate2 _ _ = HNil
instance (HReplicate2 n e es') => HReplicate2 (HSucc n) e (e ': es') where
hReplicate2 n e = e `HCons` hReplicate2 (hPred n) e
hReplicateApp e = let r = hMap FApply (hReplicate2 (hLength r) e) in r
hSplitAt n xs = hSplitAtAux n xs HNil
class HSplitAtAux (n :: HNat) l a0 a b | n -> l a0 a b where
hSplitAtAux :: Proxy n -> HList l -> HList a0 -> (HList a, HList b)
instance (l ~ b, a ~ HRevApp a0 '[]) => HSplitAtAux HZero l a0 a b where
hSplitAtAux _ l acc = (hReverse acc, l)
instance ( (x ': xs) ~ ls, acc' ~ (x ': acc),
HSplitAtAux n xs acc' a b) => HSplitAtAux (HSucc n) ls acc a b where
hSplitAtAux n (HCons x xs) acc = hSplitAtAux (hPred n) xs (HCons x acc)
hEnumFromTo :: Proxy a -> Proxy b -> Proxy (HEnumFromTo a b)
hEnumFromTo a b = proxy
type family HEnumFromTo (from::HNat) (to::HNat) :: [HNat]
type instance HEnumFromTo a HZero = '[a]
type instance HEnumFromTo a (HSucc b) = a ': HEnumFromTo (HSucc a) b
class (SameLength a b, SameLength b a) => HReverse2 a b | a -> b, b -> a where
hReverse2 :: HList a -> HList b
instance (SameLength a b, SameLength b a, HRevApp a '[] ~ b, HRevApp b '[] ~ a) => HReverse2 a b where
hReverse2 = hReverse
class HMap1 f a b where hMap1 :: f -> HList a -> HList b
instance (a ~ '[]) => HMap1 f a '[] where
hMap1 _ _ = HNil
instance (ApplyAB f a b, (a ': as) ~ aas, HMap1 f as bs) =>
HMap1 f aas (b ': bs) where
hMap1 f (HCons a as) = HCons (applyAB f a) (hMap1 f as)
class HMap2 f a b where hMap2 :: f -> HList a -> HList b
instance (a ~ '[]) => HMap2 f '[] a where
hMap2 _ _ = HNil
instance (ApplyAB f a b, (b ': bs) ~ bbs, HMap2 f as bs) =>
HMap2 f (a ': as) bbs where
hMap2 f (HCons a as) = HCons (applyAB f a) (hMap2 f as)