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

instance Eq a => Eq (FixedList n a) where
    FixedList n a
NilFixedList == :: FixedList n a -> FixedList n a -> Bool
== FixedList n a
NilFixedList = Bool
True
    (ConsFixedList a
a FixedList n a
la) == (ConsFixedList a
b FixedList n a
lb) =
        if a
a forall a. Eq a => a -> a -> Bool
== a
b
            then FixedList n a
la forall a. Eq a => a -> a -> Bool
== FixedList n a
lb
            else Bool
False

fixedListLength :: FixedList n a -> PeanoNatType n
fixedListLength :: forall (n :: PeanoNat) a. FixedList n a -> PeanoNatType n
fixedListLength FixedList n a
NilFixedList = PeanoNatType 'Zero
ZeroType
fixedListLength (ConsFixedList a
_ FixedList n a
l) = forall (t1 :: PeanoNat). PeanoNatType t1 -> PeanoNatType ('Succ t1)
SuccType forall a b. (a -> b) -> a -> b
$ forall (n :: PeanoNat) a. FixedList n a -> PeanoNatType n
fixedListLength FixedList n a
l

fixedListGenerate :: Applicative m => PeanoNatType n -> m a -> m (FixedList n a)
fixedListGenerate :: forall (m :: Type -> Type) (n :: PeanoNat) a.
Applicative m =>
PeanoNatType n -> m a -> m (FixedList n a)
fixedListGenerate PeanoNatType n
ZeroType m a
_ = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a. FixedList 'Zero a
NilFixedList
fixedListGenerate (SuccType PeanoNatType t1
n) m a
ma = 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 m a
ma forall a b. (a -> b) -> a -> b
$ forall (m :: Type -> Type) (n :: PeanoNat) a.
Applicative m =>
PeanoNatType n -> m a -> m (FixedList n a)
fixedListGenerate PeanoNatType t1
n m a
ma

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