module Data.Type.Witness.Specific.FixedList where import Data.PeanoNat import Data.Type.Witness.General.Representative import Data.Type.Witness.Specific.PeanoNat import Data.Type.Witness.Specific.Some import Import type FixedList :: PeanoNat -> Type -> Type data FixedList n a where NilFixedList :: FixedList 'Zero a ConsFixedList :: a -> FixedList n a -> FixedList ('Succ n) a instance Functor (FixedList n) where fmap :: forall a b. (a -> b) -> FixedList n a -> FixedList n b fmap a -> b _ FixedList n a NilFixedList = forall a. FixedList 'Zero a NilFixedList fmap a -> b ab (ConsFixedList a a FixedList n a l) = forall a (n :: PeanoNat). a -> FixedList n a -> FixedList ('Succ n) a ConsFixedList (a -> b ab a a) forall a b. (a -> b) -> a -> b $ forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b fmap a -> b ab FixedList n a l instance Is PeanoNatType n => Applicative (FixedList n) where pure :: forall a. a -> FixedList n a pure = let pure' :: PeanoNatType n' -> a -> FixedList n' a pure' :: forall (n' :: PeanoNat) a. PeanoNatType n' -> a -> FixedList n' a pure' PeanoNatType n' ZeroType a _ = forall a. FixedList 'Zero a NilFixedList pure' (SuccType PeanoNatType t1 n) a a = forall a (n :: PeanoNat). a -> FixedList n a -> FixedList ('Succ n) a ConsFixedList a a forall a b. (a -> b) -> a -> b $ forall (n' :: PeanoNat) a. PeanoNatType n' -> a -> FixedList n' a pure' PeanoNatType t1 n a a in forall (n' :: PeanoNat) a. PeanoNatType n' -> a -> FixedList n' a pure' forall k (rep :: k -> Type) (a :: k). Is rep a => rep a representative <*> :: forall a b. FixedList n (a -> b) -> FixedList n a -> FixedList n b (<*>) = let ap' :: PeanoNatType n' -> FixedList n' (a -> b) -> FixedList n' a -> FixedList n' b ap' :: forall (n' :: PeanoNat) a b. PeanoNatType n' -> FixedList n' (a -> b) -> FixedList n' a -> FixedList n' b ap' PeanoNatType n' ZeroType FixedList n' (a -> b) NilFixedList FixedList n' a NilFixedList = forall a. FixedList 'Zero a NilFixedList ap' (SuccType PeanoNatType t1 n) (ConsFixedList a -> b ab FixedList n (a -> b) lab) (ConsFixedList a a FixedList n a la) = forall a (n :: PeanoNat). a -> FixedList n a -> FixedList ('Succ n) a ConsFixedList (a -> b ab a a) forall a b. (a -> b) -> a -> b $ forall (n' :: PeanoNat) a b. PeanoNatType n' -> FixedList n' (a -> b) -> FixedList n' a -> FixedList n' b ap' PeanoNatType t1 n FixedList n (a -> b) lab FixedList n a la in forall (n' :: PeanoNat) a b. PeanoNatType n' -> FixedList n' (a -> b) -> FixedList n' a -> FixedList n' b ap' forall k (rep :: k -> Type) (a :: k). Is rep a => rep a representative instance Foldable (FixedList n) where foldMap :: forall m a. Monoid m => (a -> m) -> FixedList n a -> m foldMap a -> m _ FixedList n a NilFixedList = forall a. Monoid a => a mempty foldMap a -> m am (ConsFixedList a a FixedList n a l) = a -> m am a a forall a. Semigroup a => a -> a -> a <> forall (t :: Type -> Type) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap a -> m am FixedList n a l instance Traversable (FixedList n) where sequenceA :: forall (f :: Type -> Type) a. Applicative f => FixedList n (f a) -> f (FixedList n a) sequenceA FixedList n (f a) NilFixedList = forall (f :: Type -> Type) a. Applicative f => a -> f a pure forall a. FixedList 'Zero a NilFixedList sequenceA (ConsFixedList f a fa FixedList n (f a) l) = forall (f :: Type -> Type) a b c. Applicative f => (a -> b -> c) -> f a -> f b -> f c liftA2 forall a (n :: PeanoNat). a -> FixedList n a -> FixedList ('Succ n) a ConsFixedList f a fa forall a b. (a -> b) -> a -> b $ forall (t :: Type -> Type) (f :: Type -> Type) a. (Traversable t, Applicative f) => t (f a) -> f (t a) sequenceA FixedList n (f a) l fixedFromList :: [a] -> (forall n. PeanoNatType n -> FixedList n a -> r) -> r fixedFromList :: forall a r. [a] -> (forall (n :: PeanoNat). PeanoNatType n -> FixedList n a -> r) -> r fixedFromList [] forall (n :: PeanoNat). PeanoNatType n -> FixedList n a -> r call = forall (n :: PeanoNat). PeanoNatType n -> FixedList n a -> r call PeanoNatType 'Zero ZeroType forall a. FixedList 'Zero a NilFixedList fixedFromList (a a:[a] aa) forall (n :: PeanoNat). PeanoNatType n -> FixedList n a -> r call = forall a r. [a] -> (forall (n :: PeanoNat). PeanoNatType n -> FixedList n a -> r) -> r fixedFromList [a] aa forall a b. (a -> b) -> a -> b $ \PeanoNatType n n FixedList n a l -> forall (n :: PeanoNat). PeanoNatType n -> FixedList n a -> r call (forall (t1 :: PeanoNat). PeanoNatType t1 -> PeanoNatType ('Succ t1) SuccType PeanoNatType n n) forall a b. (a -> b) -> a -> b $ forall a (n :: PeanoNat). a -> FixedList n a -> FixedList ('Succ n) a ConsFixedList a a FixedList n a l fixedListArrowSequence_ :: forall arrow n a. Arrow arrow => FixedList n (arrow a ()) -> arrow (FixedList n a) () fixedListArrowSequence_ :: forall (arrow :: Type -> Type -> Type) (n :: PeanoNat) a. Arrow arrow => FixedList n (arrow a ()) -> arrow (FixedList n a) () fixedListArrowSequence_ FixedList n (arrow a ()) NilFixedList = forall (a :: Type -> Type -> Type) b c. Arrow a => (b -> c) -> a b c arr forall a b. (a -> b) -> a -> b $ \FixedList n a _ -> () fixedListArrowSequence_ (ConsFixedList arrow a () x1 FixedList n (arrow a ()) xr) = proc FixedList n a a1r -> do arrow a () x1 -< case FixedList n a a1r of ConsFixedList a a1 FixedList n a _ -> a a1 forall (arrow :: Type -> Type -> Type) (n :: PeanoNat) a. Arrow arrow => FixedList n (arrow a ()) -> arrow (FixedList n a) () fixedListArrowSequence_ FixedList n (arrow a ()) xr -< case FixedList n a a1r of ConsFixedList a _ FixedList n a ar -> FixedList n a ar fixedListArrowSequence :: forall arrow n a b. Arrow arrow => FixedList n (arrow a b) -> arrow (FixedList n a) (FixedList n b) fixedListArrowSequence :: forall (arrow :: Type -> Type -> Type) (n :: PeanoNat) a b. Arrow arrow => FixedList n (arrow a b) -> arrow (FixedList n a) (FixedList n b) fixedListArrowSequence FixedList n (arrow a b) NilFixedList = forall (a :: Type -> Type -> Type) b c. Arrow a => (b -> c) -> a b c arr forall a b. (a -> b) -> a -> b $ \FixedList n a _ -> forall a. FixedList 'Zero a NilFixedList fixedListArrowSequence (ConsFixedList arrow a b x1 FixedList n (arrow a b) xr) = proc FixedList n a a1r -> do b b1 <- arrow a b x1 -< case FixedList n a a1r of ConsFixedList a a1 FixedList n a _ -> a a1 FixedList n b br <- forall (arrow :: Type -> Type -> Type) (n :: PeanoNat) a b. Arrow arrow => FixedList n (arrow a b) -> arrow (FixedList n a) (FixedList n b) fixedListArrowSequence FixedList n (arrow a b) xr -< case FixedList n a a1r of ConsFixedList a _ FixedList n a ar -> FixedList n a ar forall (a :: Type -> Type -> Type) b. Arrow a => a b b returnA -< forall a (n :: PeanoNat). a -> FixedList n a -> FixedList ('Succ n) a ConsFixedList b b1 FixedList n b br fixedListElement :: Some (Greater n) -> FixedList n a -> a fixedListElement :: forall (n :: PeanoNat) a. Some (Greater n) -> FixedList n a -> a fixedListElement (MkSome (MkGreater GreaterEqual a1 a ZeroGreaterEqual)) (ConsFixedList a a FixedList n a _) = a a fixedListElement (MkSome (MkGreater (SuccGreaterEqual GreaterEqual a1 b1 n))) (ConsFixedList a _ FixedList n a l) = forall (n :: PeanoNat) a. Some (Greater n) -> FixedList n a -> a fixedListElement (forall {k} (w :: k -> Type) (a :: k). w a -> Some w MkSome forall a b. (a -> b) -> a -> b $ forall (a1 :: PeanoNat) (b :: PeanoNat). GreaterEqual a1 b -> Greater ('Succ a1) b MkGreater GreaterEqual a1 b1 n) FixedList n a l