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
type role FixedList nominal representational
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 = FixedList n b
FixedList 'Zero b
forall a. FixedList 'Zero a
NilFixedList
    fmap a -> b
ab (ConsFixedList a
a FixedList n a
l) = b -> FixedList n b -> FixedList ('Succ n) b
forall a (n :: PeanoNat).
a -> FixedList n a -> FixedList ('Succ n) a
ConsFixedList (a -> b
ab a
a) (FixedList n b -> FixedList ('Succ n) b)
-> FixedList n b -> FixedList ('Succ n) b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> FixedList n a -> FixedList n b
forall a b. (a -> b) -> FixedList n a -> FixedList n 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
_ = FixedList n' a
FixedList 'Zero a
forall a. FixedList 'Zero a
NilFixedList
        pure' (SuccType PeanoNatType t1
n) a
a = a -> FixedList t1 a -> FixedList ('Succ t1) a
forall a (n :: PeanoNat).
a -> FixedList n a -> FixedList ('Succ n) a
ConsFixedList a
a (FixedList t1 a -> FixedList ('Succ t1) a)
-> FixedList t1 a -> FixedList ('Succ t1) a
forall a b. (a -> b) -> a -> b
$ PeanoNatType t1 -> a -> FixedList t1 a
forall (n' :: PeanoNat) a. PeanoNatType n' -> a -> FixedList n' a
pure' PeanoNatType t1
n a
a
        in PeanoNatType n -> a -> FixedList n a
forall (n' :: PeanoNat) a. PeanoNatType n' -> a -> FixedList n' a
pure' PeanoNatType n
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 = FixedList n' b
FixedList 'Zero b
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) = b -> FixedList t1 b -> FixedList ('Succ t1) b
forall a (n :: PeanoNat).
a -> FixedList n a -> FixedList ('Succ n) a
ConsFixedList (a -> b
ab a
a) (FixedList t1 b -> FixedList ('Succ t1) b)
-> FixedList t1 b -> FixedList ('Succ t1) b
forall a b. (a -> b) -> a -> b
$ PeanoNatType t1
-> FixedList t1 (a -> b) -> FixedList t1 a -> FixedList t1 b
forall (n' :: PeanoNat) a b.
PeanoNatType n'
-> FixedList n' (a -> b) -> FixedList n' a -> FixedList n' b
ap' PeanoNatType t1
n FixedList t1 (a -> b)
FixedList n (a -> b)
lab FixedList t1 a
FixedList n a
la
        in PeanoNatType n
-> FixedList n (a -> b) -> FixedList n a -> FixedList n b
forall (n' :: PeanoNat) a b.
PeanoNatType n'
-> FixedList n' (a -> b) -> FixedList n' a -> FixedList n' b
ap' PeanoNatType n
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 = m
forall a. Monoid a => a
mempty
    foldMap a -> m
am (ConsFixedList a
a FixedList n a
l) = a -> m
am a
a m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (a -> m) -> FixedList n a -> m
forall m a. Monoid m => (a -> m) -> FixedList n a -> m
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 = FixedList n a -> f (FixedList n a)
forall a. a -> f a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure FixedList n a
FixedList 'Zero a
forall a. FixedList 'Zero a
NilFixedList
    sequenceA (ConsFixedList f a
fa FixedList n (f a)
l) = (a -> FixedList n a -> FixedList n a)
-> f a -> f (FixedList n a) -> f (FixedList n a)
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> FixedList n a -> FixedList n a
a -> FixedList n a -> FixedList ('Succ n) a
forall a (n :: PeanoNat).
a -> FixedList n a -> FixedList ('Succ n) a
ConsFixedList f a
fa (f (FixedList n a) -> f (FixedList n a))
-> f (FixedList n a) -> f (FixedList n a)
forall a b. (a -> b) -> a -> b
$ FixedList n (f a) -> f (FixedList n a)
forall (t :: Type -> Type) (f :: Type -> Type) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: Type -> Type) a.
Applicative f =>
FixedList n (f a) -> f (FixedList n 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 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
            then FixedList n a
la FixedList n a -> FixedList n a -> Bool
forall a. Eq a => a -> a -> Bool
== FixedList n a
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 n
PeanoNatType 'Zero
ZeroType
fixedListLength (ConsFixedList a
_ FixedList n a
l) = PeanoNatType n -> PeanoNatType ('Succ n)
forall (t1 :: PeanoNat). PeanoNatType t1 -> PeanoNatType ('Succ t1)
SuccType (PeanoNatType n -> PeanoNatType ('Succ n))
-> PeanoNatType n -> PeanoNatType ('Succ n)
forall a b. (a -> b) -> a -> b
$ FixedList n a -> PeanoNatType n
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
_ = FixedList n a -> m (FixedList n a)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure FixedList n a
FixedList 'Zero a
forall a. FixedList 'Zero a
NilFixedList
fixedListGenerate (SuccType PeanoNatType t1
n) m a
ma = (a -> FixedList t1 a -> FixedList n a)
-> m a -> m (FixedList t1 a) -> m (FixedList n a)
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> FixedList t1 a -> FixedList n a
a -> FixedList t1 a -> FixedList ('Succ t1) a
forall a (n :: PeanoNat).
a -> FixedList n a -> FixedList ('Succ n) a
ConsFixedList m a
ma (m (FixedList t1 a) -> m (FixedList n a))
-> m (FixedList t1 a) -> m (FixedList n a)
forall a b. (a -> b) -> a -> b
$ PeanoNatType t1 -> m a -> m (FixedList t1 a)
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 = PeanoNatType 'Zero -> FixedList 'Zero a -> r
forall (n :: PeanoNat). PeanoNatType n -> FixedList n a -> r
call PeanoNatType 'Zero
ZeroType FixedList 'Zero a
forall a. FixedList 'Zero a
NilFixedList
fixedFromList (a
a:[a]
aa) forall (n :: PeanoNat). PeanoNatType n -> FixedList n a -> r
call = [a]
-> (forall (n :: PeanoNat). PeanoNatType n -> FixedList n a -> r)
-> r
forall a r.
[a]
-> (forall (n :: PeanoNat). PeanoNatType n -> FixedList n a -> r)
-> r
fixedFromList [a]
aa ((forall (n :: PeanoNat). PeanoNatType n -> FixedList n a -> r)
 -> r)
-> (forall (n :: PeanoNat). PeanoNatType n -> FixedList n a -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \PeanoNatType n
n FixedList n a
l -> PeanoNatType ('Succ n) -> FixedList ('Succ n) a -> r
forall (n :: PeanoNat). PeanoNatType n -> FixedList n a -> r
call (PeanoNatType n -> PeanoNatType ('Succ n)
forall (t1 :: PeanoNat). PeanoNatType t1 -> PeanoNatType ('Succ t1)
SuccType PeanoNatType n
n) (FixedList ('Succ n) a -> r) -> FixedList ('Succ n) a -> r
forall a b. (a -> b) -> a -> b
$ a -> FixedList n a -> FixedList ('Succ n) a
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 = (FixedList n a -> ()) -> arrow (FixedList n a) ()
forall b c. (b -> c) -> arrow b c
forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr ((FixedList n a -> ()) -> arrow (FixedList n a) ())
-> (FixedList n a -> ()) -> arrow (FixedList n a) ()
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
        FixedList n (arrow a ()) -> arrow (FixedList n a) ()
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
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 = (FixedList n a -> FixedList n b)
-> arrow (FixedList n a) (FixedList n b)
forall b c. (b -> c) -> arrow b c
forall (a :: Type -> Type -> Type) b c.
Arrow a =>
(b -> c) -> a b c
arr ((FixedList n a -> FixedList n b)
 -> arrow (FixedList n a) (FixedList n b))
-> (FixedList n a -> FixedList n b)
-> arrow (FixedList n a) (FixedList n b)
forall a b. (a -> b) -> a -> b
$ \FixedList n a
_ -> FixedList n b
FixedList 'Zero b
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 <-
            FixedList n (arrow a b) -> arrow (FixedList n a) (FixedList n b)
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
FixedList n a
ar
        arrow (FixedList n b) (FixedList n b)
forall (a :: Type -> Type -> Type) b. Arrow a => a b b
returnA -< b -> FixedList n b -> FixedList ('Succ n) b
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) =
    Some (Greater ('Succ a1)) -> FixedList ('Succ a1) a -> a
forall (n :: PeanoNat) a. Some (Greater n) -> FixedList n a -> a
fixedListElement (Greater ('Succ a1) b1 -> Some (Greater ('Succ a1))
forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome (Greater ('Succ a1) b1 -> Some (Greater ('Succ a1)))
-> Greater ('Succ a1) b1 -> Some (Greater ('Succ a1))
forall a b. (a -> b) -> a -> b
$ GreaterEqual a1 b1 -> Greater ('Succ a1) b1
forall (a1 :: PeanoNat) (b :: PeanoNat).
GreaterEqual a1 b -> Greater ('Succ a1) b
MkGreater GreaterEqual a1 b1
n) FixedList n a
FixedList ('Succ a1) a
l