module Language.Parser.Ptera.Data.HFList ( T, HFList (..), Membership, Concat, hconcat, hfoldrWithIndex, htraverseWithIndex, hmapWithIndex, hfoldMWithIndex, hforMWithIndex, hfoldlWithIndex, DictF (..), ) where import Language.Parser.Ptera.Prelude import Type.Membership (Membership) import qualified Unsafe.Coerce as Unsafe type T = HFList data HFList :: (k -> Type) -> [k] -> Type where HFNil :: HFList f '[] HFCons :: f x -> HFList f xs -> HFList f (x ': xs) type family Concat (xs1 :: [k]) (xs2 :: [k]) :: [k] where Concat '[] xs2 = xs2 Concat (x ': xs1) xs2 = x ': Concat xs1 xs2 hconcat :: HFList f xs1 -> HFList f xs2 -> HFList f (Concat xs1 xs2) hconcat :: forall {k} (f :: k -> *) (xs1 :: [k]) (xs2 :: [k]). HFList f xs1 -> HFList f xs2 -> HFList f (Concat xs1 xs2) hconcat HFList f xs1 l1 HFList f xs2 l2 = case HFList f xs1 l1 of HFList f xs1 HFNil -> HFList f xs2 l2 HFCons f x x HFList f xs l1' -> forall {k} (f :: k -> *) (x :: k) (xs :: [k]). f x -> HFList f xs -> HFList f (x : xs) HFCons f x x do forall {k} (f :: k -> *) (xs1 :: [k]) (xs2 :: [k]). HFList f xs1 -> HFList f xs2 -> HFList f (Concat xs1 xs2) hconcat HFList f xs l1' HFList f xs2 l2 hfoldrWithIndex :: forall f r xs . (forall x ys. Membership xs x -> f x -> r ys -> r (x ': ys)) -> r '[] -> HFList f xs -> r xs hfoldrWithIndex :: forall {k} (f :: k -> *) (r :: [k] -> *) (xs :: [k]). (forall (x :: k) (ys :: [k]). Membership xs x -> f x -> r ys -> r (x : ys)) -> r '[] -> HFList f xs -> r xs hfoldrWithIndex forall (x :: k) (ys :: [k]). Membership xs x -> f x -> r ys -> r (x : ys) f r '[] z0 = forall (ys :: [k]). Int -> HFList f ys -> r ys go Int 0 where go :: Int -> HFList f ys -> r ys go :: forall (ys :: [k]). Int -> HFList f ys -> r ys go Int m0 = \case HFList f ys HFNil -> r '[] z0 HFCons f x y HFList f xs l -> do let m1 :: Int m1 = Int m0 forall a. Num a => a -> a -> a + Int 1 forall (x :: k) (ys :: [k]). Membership xs x -> f x -> r ys -> r (x : ys) f do forall {k} (xs :: [k]) (x :: k). Int -> Membership xs x unsafeMembership Int m0 do f x y do forall (ys :: [k]). Int -> HFList f ys -> r ys go Int m1 HFList f xs l htraverseWithIndex :: forall m f g xs . Applicative m => (forall x. Membership xs x -> f x -> m (g x)) -> HFList f xs -> m (HFList g xs) htraverseWithIndex :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (xs :: [k]). Applicative m => (forall (x :: k). Membership xs x -> f x -> m (g x)) -> HFList f xs -> m (HFList g xs) htraverseWithIndex forall (x :: k). Membership xs x -> f x -> m (g x) f = coerce :: forall a b. Coercible a b => a -> b coerce HFList f xs -> TraverseHFList m g xs go0 where go0 :: HFList f xs -> TraverseHFList m g xs go0 = forall {k} (f :: k -> *) (r :: [k] -> *) (xs :: [k]). (forall (x :: k) (ys :: [k]). Membership xs x -> f x -> r ys -> r (x : ys)) -> r '[] -> HFList f xs -> r xs hfoldrWithIndex forall (x :: k) (ys :: [k]). Membership xs x -> f x -> TraverseHFList m g ys -> TraverseHFList m g (x : ys) go do forall {k} (m :: * -> *) (f :: k -> *) (xs :: [k]). m (HFList f xs) -> TraverseHFList m f xs TraverseHFList do forall (f :: * -> *) a. Applicative f => a -> f a pure forall {k} (f :: k -> *). HFList f '[] HFNil go :: forall x ys. Membership xs x -> f x -> TraverseHFList m g ys -> TraverseHFList m g (x ': ys) go :: forall (x :: k) (ys :: [k]). Membership xs x -> f x -> TraverseHFList m g ys -> TraverseHFList m g (x : ys) go Membership xs x m f x x = \case TraverseHFList m (HFList g ys) acc0 -> forall {k} (m :: * -> *) (f :: k -> *) (xs :: [k]). m (HFList f xs) -> TraverseHFList m f xs TraverseHFList do forall {k} (f :: k -> *) (x :: k) (xs :: [k]). f x -> HFList f xs -> HFList f (x : xs) HFCons forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall (x :: k). Membership xs x -> f x -> m (g x) f Membership xs x m f x x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> m (HFList g ys) acc0 newtype TraverseHFList m f xs = TraverseHFList (m (HFList f xs)) hmapWithIndex :: (forall x. Membership xs x -> f x -> g x) -> HFList f xs -> HFList g xs hmapWithIndex :: forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *). (forall (x :: k). Membership xs x -> f x -> g x) -> HFList f xs -> HFList g xs hmapWithIndex forall (x :: k). Membership xs x -> f x -> g x f HFList f xs l = forall a. Identity a -> a runIdentity do forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (xs :: [k]). Applicative m => (forall (x :: k). Membership xs x -> f x -> m (g x)) -> HFList f xs -> m (HFList g xs) htraverseWithIndex do \Membership xs x m f x x -> forall a. a -> Identity a Identity do forall (x :: k). Membership xs x -> f x -> g x f Membership xs x m f x x do HFList f xs l hfoldMWithIndex :: forall m r f xs . Monad m => r -> (forall x. r -> Membership xs x -> f x -> m r) -> HFList f xs -> m r hfoldMWithIndex :: forall {k} (m :: * -> *) r (f :: k -> *) (xs :: [k]). Monad m => r -> (forall (x :: k). r -> Membership xs x -> f x -> m r) -> HFList f xs -> m r hfoldMWithIndex r z0 forall (x :: k). r -> Membership xs x -> f x -> m r f = forall (ys :: [k]). Int -> r -> HFList f ys -> m r go Int 0 r z0 where go :: Int -> r -> HFList f ys -> m r go :: forall (ys :: [k]). Int -> r -> HFList f ys -> m r go Int m1 r z1 = \case HFList f ys HFNil -> forall (f :: * -> *) a. Applicative f => a -> f a pure r z1 HFCons f x y HFList f xs l -> do r z2 <- forall (x :: k). r -> Membership xs x -> f x -> m r f r z1 do forall {k} (xs :: [k]) (x :: k). Int -> Membership xs x unsafeMembership Int m1 do f x y let m2 :: Int m2 = Int m1 forall a. Num a => a -> a -> a + Int 1 forall (ys :: [k]). Int -> r -> HFList f ys -> m r go Int m2 r z2 HFList f xs l hforMWithIndex :: forall m f xs . Applicative m => HFList f xs -> (forall x. Membership xs x -> f x -> m ()) -> m () hforMWithIndex :: forall {k} (m :: * -> *) (f :: k -> *) (xs :: [k]). Applicative m => HFList f xs -> (forall (x :: k). Membership xs x -> f x -> m ()) -> m () hforMWithIndex HFList f xs l0 forall (x :: k). Membership xs x -> f x -> m () f = forall (ys :: [k]). Int -> HFList f ys -> m () go Int 0 HFList f xs l0 where go :: Int -> HFList f ys -> m () go :: forall (ys :: [k]). Int -> HFList f ys -> m () go Int m1 = \case HFList f ys HFNil -> forall (f :: * -> *) a. Applicative f => a -> f a pure () HFCons f x y HFList f xs l -> forall a b. a -> b -> a const forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> forall (x :: k). Membership xs x -> f x -> m () f do forall {k} (xs :: [k]) (x :: k). Int -> Membership xs x unsafeMembership Int m1 do f x y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall (ys :: [k]). Int -> HFList f ys -> m () go do Int m1 forall a. Num a => a -> a -> a + Int 1 HFList f xs l hfoldlWithIndex :: r -> (forall x. r -> Membership xs x -> f x -> r) -> HFList f xs -> r hfoldlWithIndex :: forall {k} r (xs :: [k]) (f :: k -> *). r -> (forall (x :: k). r -> Membership xs x -> f x -> r) -> HFList f xs -> r hfoldlWithIndex r z0 forall (x :: k). r -> Membership xs x -> f x -> r f = coerce :: forall a b. Coercible a b => a -> b coerce do forall {k} (m :: * -> *) r (f :: k -> *) (xs :: [k]). Monad m => r -> (forall (x :: k). r -> Membership xs x -> f x -> m r) -> HFList f xs -> m r hfoldMWithIndex r z0 \r z Membership xs x m f x x -> forall a. a -> Identity a Identity do forall (x :: k). r -> Membership xs x -> f x -> r f r z Membership xs x m f x x data DictF :: (k -> Constraint) -> k -> Type where DictF :: c x => DictF c x unsafeMembership :: Int -> Membership xs x unsafeMembership :: forall {k} (xs :: [k]) (x :: k). Int -> Membership xs x unsafeMembership = forall a b. a -> b Unsafe.unsafeCoerce