{-# LANGUAGE MultiParamTypeClasses #-}
module Parsley.Internal.Common.Indexed (module Parsley.Internal.Common.Indexed) where

import Control.Applicative ((<|>), liftA2)
import Data.Kind           (Type)
import Data.Maybe          (fromMaybe)

data Nat = Zero | Succ Nat
type One = Succ Zero

class IFunctor (f :: (Type -> Type) -> Type -> Type) where
  imap :: (forall j. a j -> b j) -> f a i -> f b i

class IFunctor4 (f :: ([Type] -> Nat -> Type -> Type -> Type) -> [Type] -> Nat -> Type -> Type -> Type) where
  imap4 :: (forall i' j' k'. a i' j' k' x -> b i' j' k' x) -> f a i j k x -> f b i j k x

newtype Fix f a = In (f (Fix f) a)
newtype Fix4 f i j k l = In4 (f (Fix4 f) i j k l)

inop :: Fix f a -> f (Fix f) a
inop :: forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
Fix f a -> f (Fix f) a
inop (In f (Fix f) a
x) = f (Fix f) a
x

inop4 :: Fix4 f i j k l -> f (Fix4 f) i j k l
inop4 :: forall {k} {k} {k} {k}
       (f :: (k -> k -> k -> k -> Type) -> k -> k -> k -> k -> Type)
       (i :: k) (j :: k) (k :: k) (l :: k).
Fix4 f i j k l -> f (Fix4 f) i j k l
inop4 (In4 f (Fix4 f) i j k l
x) = f (Fix4 f) i j k l
x

cata :: forall f a i. IFunctor f => (forall j. f a j -> a j) -> Fix f i -> a i
cata :: forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type) i.
IFunctor f =>
(forall j. f a j -> a j) -> Fix f i -> a i
cata forall j. f a j -> a j
alg = forall j. Fix f j -> a j
go where
  go :: Fix f j -> a j
  go :: forall j. Fix f j -> a j
go (In f (Fix f) j
x) = forall j. f a j -> a j
alg (forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. a j -> b j) -> f a i -> f b i
imap forall j. Fix f j -> a j
go f (Fix f) j
x)

cata' :: forall f a i. IFunctor f =>
         (forall j. Fix f j -> f a j -> a j) ->
         Fix f i -> a i
cata' :: forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type) i.
IFunctor f =>
(forall j. Fix f j -> f a j -> a j) -> Fix f i -> a i
cata' forall j. Fix f j -> f a j -> a j
alg = forall j. Fix f j -> a j
go where
  go :: Fix f j -> a j
  go :: forall j. Fix f j -> a j
go i :: Fix f j
i@(In f (Fix f) j
x) = forall j. Fix f j -> f a j -> a j
alg Fix f j
i (forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. a j -> b j) -> f a i -> f b i
imap forall j. Fix f j -> a j
go f (Fix f) j
x)

cata4 :: forall f a i j k x. IFunctor4 f =>
         (forall i' j' k'. f a i' j' k' x -> a i' j' k' x) ->
         Fix4 f i j k x -> a i j k x
cata4 :: forall (f :: ([Type] -> Nat -> Type -> Type -> Type)
             -> [Type] -> Nat -> Type -> Type -> Type)
       (a :: [Type] -> Nat -> Type -> Type -> Type) (i :: [Type])
       (j :: Nat) k x.
IFunctor4 f =>
(forall (i' :: [Type]) (j' :: Nat) k'.
 f a i' j' k' x -> a i' j' k' x)
-> Fix4 f i j k x -> a i j k x
cata4 forall (i' :: [Type]) (j' :: Nat) k'.
f a i' j' k' x -> a i' j' k' x
alg = forall (i' :: [Type]) (j' :: Nat) k'.
Fix4 f i' j' k' x -> a i' j' k' x
go where
  go :: Fix4 f i' j' k' x -> a i' j' k' x
  go :: forall (i' :: [Type]) (j' :: Nat) k'.
Fix4 f i' j' k' x -> a i' j' k' x
go (In4 f (Fix4 f) i' j' k' x
x) = forall (i' :: [Type]) (j' :: Nat) k'.
f a i' j' k' x -> a i' j' k' x
alg (forall (f :: ([Type] -> Nat -> Type -> Type -> Type)
             -> [Type] -> Nat -> Type -> Type -> Type)
       (a :: [Type] -> Nat -> Type -> Type -> Type) x
       (b :: [Type] -> Nat -> Type -> Type -> Type) (i :: [Type])
       (j :: Nat) k.
IFunctor4 f =>
(forall (i' :: [Type]) (j' :: Nat) k'.
 a i' j' k' x -> b i' j' k' x)
-> f a i j k x -> f b i j k x
imap4 forall (i' :: [Type]) (j' :: Nat) k'.
Fix4 f i' j' k' x -> a i' j' k' x
go f (Fix4 f) i' j' k' x
x)

data (f :+: g) k a where
  L :: f k a -> (f :+: g) k a
  R :: g k a -> (f :+: g) k a

instance (IFunctor f, IFunctor g) => IFunctor (f :+: g) where
  imap :: forall (a :: Type -> Type) (b :: Type -> Type) i.
(forall j. a j -> b j) -> (:+:) f g a i -> (:+:) f g b i
imap forall j. a j -> b j
f (L f a i
x) = forall {k} {k} (f :: k -> k -> Type) (k :: k) (a :: k)
       (g :: k -> k -> Type).
f k a -> (:+:) f g k a
L (forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. a j -> b j) -> f a i -> f b i
imap forall j. a j -> b j
f f a i
x)
  imap forall j. a j -> b j
f (R g a i
y) = forall {k} {k} (g :: k -> k -> Type) (k :: k) (a :: k)
       (f :: k -> k -> Type).
g k a -> (:+:) f g k a
R (forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. a j -> b j) -> f a i -> f b i
imap forall j. a j -> b j
f g a i
y)

(\/) :: (f a i -> b) -> (g a i -> b) -> (f :+: g) a i -> b
(f a i -> b
f \/ :: forall {k} {k} (f :: k -> k -> Type) (a :: k) (i :: k) b
       (g :: k -> k -> Type).
(f a i -> b) -> (g a i -> b) -> (:+:) f g a i -> b
\/ g a i -> b
_) (L f a i
x) = f a i -> b
f f a i
x
(f a i -> b
_ \/ g a i -> b
g) (R g a i
y) = g a i -> b
g g a i
y

data Cofree f a i = a i :< f (Cofree f a) i
{-# INLINE extract #-}
extract :: Cofree f a i -> a i
extract :: forall {k} (f :: (k -> Type) -> k -> Type) (a :: k -> Type)
       (i :: k).
Cofree f a i -> a i
extract (a i
x :< f (Cofree f a) i
_) = a i
x

instance IFunctor f => IFunctor (Cofree f) where
  imap :: forall (a :: Type -> Type) (b :: Type -> Type) i.
(forall j. a j -> b j) -> Cofree f a i -> Cofree f b i
imap forall j. a j -> b j
f (a i
x :< f (Cofree f a) i
xs) = forall j. a j -> b j
f a i
x forall {k} (f :: (k -> Type) -> k -> Type) (a :: k -> Type)
       (i :: k).
a i -> f (Cofree f a) i -> Cofree f a i
:< forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. a j -> b j) -> f a i -> f b i
imap (forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. a j -> b j) -> f a i -> f b i
imap forall j. a j -> b j
f) f (Cofree f a) i
xs

histo :: IFunctor f => (forall j. f (Cofree f a) j -> a j) -> Fix f i -> a i
histo :: forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type) i.
IFunctor f =>
(forall j. f (Cofree f a) j -> a j) -> Fix f i -> a i
histo forall j. f (Cofree f a) j -> a j
alg = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k -> Type)
       (i :: k).
Cofree f a i -> a i
extract forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type) i.
IFunctor f =>
(forall j. f a j -> a j) -> Fix f i -> a i
cata (forall j. f (Cofree f a) j -> a j
alg forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {k} (f :: (k -> Type) -> k -> Type) (a :: k -> Type)
       (i :: k).
a i -> f (Cofree f a) i -> Cofree f a i
(:<))

data (f :*: g) i = f i :*: g i

{-# INLINE (/\) #-}
(/\) :: (a -> f i) -> (a -> g i) -> (a -> (f :*: g) i)
(a -> f i
f /\ :: forall {k} a (f :: k -> Type) (i :: k) (g :: k -> Type).
(a -> f i) -> (a -> g i) -> a -> (:*:) f g i
/\ a -> g i
g) a
x = a -> f i
f a
x forall {k} (f :: k -> Type) (g :: k -> Type) (i :: k).
f i -> g i -> (:*:) f g i
:*: a -> g i
g a
x

{-# INLINE ifst #-}
ifst :: (f :*: g) i -> f i
ifst :: forall {k} (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst (f i
x :*: g i
_) = f i
x
{-# INLINE isnd #-}
isnd :: (f :*: g) i -> g i
isnd :: forall {k} (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> g i
isnd (f i
_ :*: g i
y) = g i
y

mutu :: IFunctor f => (forall j. f (a :*: b) j -> a j) -> (forall j. f (a :*: b) j -> b j) -> Fix f i -> (a :*: b) i
mutu :: forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. f (a :*: b) j -> a j)
-> (forall j. f (a :*: b) j -> b j) -> Fix f i -> (:*:) a b i
mutu forall j. f (a :*: b) j -> a j
algl forall j. f (a :*: b) j -> b j
algr = forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type) i.
IFunctor f =>
(forall j. f a j -> a j) -> Fix f i -> a i
cata (forall j. f (a :*: b) j -> a j
algl forall {k} a (f :: k -> Type) (i :: k) (g :: k -> Type).
(a -> f i) -> (a -> g i) -> a -> (:*:) f g i
/\ forall j. f (a :*: b) j -> b j
algr)

zygo :: IFunctor f => (forall j. f (a :*: b) j -> a j) -> (forall j. f b j -> b j) -> Fix f i -> a i
zygo :: forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. f (a :*: b) j -> a j)
-> (forall j. f b j -> b j) -> Fix f i -> a i
zygo forall j. f (a :*: b) j -> a j
alg forall j. f b j -> b j
aux = forall {k} (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. f (a :*: b) j -> a j)
-> (forall j. f (a :*: b) j -> b j) -> Fix f i -> (:*:) a b i
mutu forall j. f (a :*: b) j -> a j
alg (forall j. f b j -> b j
aux forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. a j -> b j) -> f a i -> f b i
imap forall {k} (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> g i
isnd)

zipper :: IFunctor f => (forall j. f a j -> a j) -> (forall j. f b j -> b j) -> Fix f i -> (a :*: b) i
zipper :: forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. f a j -> a j)
-> (forall j. f b j -> b j) -> Fix f i -> (:*:) a b i
zipper forall j. f a j -> a j
algl forall j. f b j -> b j
algr = forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. f (a :*: b) j -> a j)
-> (forall j. f (a :*: b) j -> b j) -> Fix f i -> (:*:) a b i
mutu (forall j. f a j -> a j
algl forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. a j -> b j) -> f a i -> f b i
imap forall {k} (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst) (forall j. f b j -> b j
algr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: (Type -> Type) -> Type -> Type) (a :: Type -> Type)
       (b :: Type -> Type) i.
IFunctor f =>
(forall j. a j -> b j) -> f a i -> f b i
imap forall {k} (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> g i
isnd)

class                         Chain r k         where (|>) :: (a -> Maybe r) -> (a -> k) -> a -> k
instance {-# OVERLAPPABLE #-} Chain a a         where |> :: forall a. (a -> Maybe a) -> (a -> a) -> a -> a
(|>) = forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. a -> Maybe a -> a
fromMaybe)
instance {-# OVERLAPS #-}     Chain a (Maybe a) where |> :: forall a. (a -> Maybe a) -> (a -> Maybe a) -> a -> Maybe a
(|>) = forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
(<|>)

data Unit1 k = Unit
newtype Const1 a k = Const1 {forall {k} a (k :: k). Const1 a k -> a
getConst1 :: a}

data Unit4 i j k l = Unit4
newtype Const4 a i j k l = Const4 {forall {k} {k} {k} {k} a (i :: k) (j :: k) (k :: k) (l :: k).
Const4 a i j k l -> a
getConst4 :: a}