{-# 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 :: 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 :: 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 j. f a j -> a j) -> Fix f i -> a i
cata forall j. f a j -> a j
alg = Fix f i -> a i
forall j. Fix f j -> a j
go where
  go :: Fix f j -> a j
  go :: Fix f j -> a j
go (In f (Fix f) j
x) = f a j -> a j
forall j. f a j -> a j
alg ((forall j. Fix f j -> a j) -> f (Fix f) j -> f a j
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 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 = Fix f i -> a i
forall j. Fix f j -> a j
go where
  go :: Fix f j -> a j
  go :: Fix f j -> a j
go i :: Fix f j
i@(In f (Fix f) j
x) = Fix f j -> f a j -> a j
forall j. Fix f j -> f a j -> a j
alg Fix f j
i ((forall j. Fix f j -> a j) -> f (Fix f) j -> f a j
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 (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 = Fix4 f i j k x -> a i j k x
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 :: Fix4 f i' j' k' x -> a i' j' k' x
go (In4 f (Fix4 f) i' j' k' x
x) = f a i' j' k' x -> a i' j' k' x
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)
-> f (Fix4 f) i' j' k' x -> f a i' j' k' x
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 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) = f b i -> (:+:) f g b i
forall k k (f :: k -> k -> Type) (k :: k) (a :: k)
       (g :: k -> k -> Type).
f k a -> (:+:) f g k a
L ((forall j. a j -> b j) -> f a i -> f b 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. a j -> b j
f f a i
x)
  imap forall j. a j -> b j
f (R g a i
y) = g b i -> (:+:) f g b i
forall k k (g :: k -> k -> Type) (k :: k) (a :: k)
       (f :: k -> k -> Type).
g k a -> (:+:) f g k a
R ((forall j. a j -> b j) -> g a i -> g b 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. 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 \/ :: (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 :: 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 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) = a i -> b i
forall j. a j -> b j
f a i
x b i -> f (Cofree f b) i -> Cofree f b i
forall k (f :: (k -> Type) -> k -> Type) (a :: k -> Type) (i :: k).
a i -> f (Cofree f a) i -> Cofree f a i
:< (forall j. Cofree f a j -> Cofree f b j)
-> f (Cofree f a) i -> f (Cofree f b) 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. a j -> b j) -> Cofree f a j -> Cofree f b j
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 j. f (Cofree f a) j -> a j) -> Fix f i -> a i
histo forall j. f (Cofree f a) j -> a j
alg = Cofree f a i -> a i
forall k (f :: (k -> Type) -> k -> Type) (a :: k -> Type) (i :: k).
Cofree f a i -> a i
extract (Cofree f a i -> a i)
-> (Fix f i -> Cofree f a i) -> Fix f i -> a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall j. f (Cofree f a) j -> Cofree f a j)
-> Fix f i -> Cofree f a i
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 (f (Cofree f a) j -> a j
forall j. f (Cofree f a) j -> a j
alg (f (Cofree f a) j -> a j)
-> (a j -> f (Cofree f a) j -> Cofree f a j)
-> f (Cofree f a) j
-> Cofree f a j
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= a j -> f (Cofree f a) j -> Cofree f a j
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 /\ :: (a -> f i) -> (a -> g i) -> a -> (:*:) f g i
/\ a -> g i
g) a
x = a -> f i
f a
x f i -> g i -> (:*:) f g i
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 :: (:*:) f g i -> f i
ifst (f i
x :*: g i
_) = f i
x
{-# INLINE isnd #-}
isnd :: (f :*: g) i -> g i
isnd :: (:*:) 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 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 j. f (a :*: b) j -> (:*:) a b j) -> Fix f i -> (:*:) a b i
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 (f (a :*: b) j -> a j
forall j. f (a :*: b) j -> a j
algl (f (a :*: b) j -> a j)
-> (f (a :*: b) j -> b j) -> f (a :*: b) j -> (:*:) a b j
forall k a (f :: k -> Type) (i :: k) (g :: k -> Type).
(a -> f i) -> (a -> g i) -> a -> (:*:) f g i
/\ f (a :*: b) j -> b j
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 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 = (:*:) a b i -> a i
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst ((:*:) a b i -> a i) -> (Fix f i -> (:*:) a b i) -> Fix f i -> a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall j. f (a :*: b) j -> a j)
-> (forall j. f (a :*: b) j -> b j) -> Fix f i -> (:*:) a b i
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 (f b j -> b j
forall j. f b j -> b j
aux (f b j -> b j) -> (f (a :*: b) j -> f b j) -> f (a :*: b) j -> b j
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall j. (:*:) a b j -> b j) -> f (a :*: b) j -> f b j
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 b j -> b j
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 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 j. f (a :*: b) j -> a j)
-> (forall j. f (a :*: b) j -> b j) -> Fix f i -> (:*:) a b i
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 (f a j -> a j
forall j. f a j -> a j
algl (f a j -> a j) -> (f (a :*: b) j -> f a j) -> f (a :*: b) j -> a j
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall j. (:*:) a b j -> a j) -> f (a :*: b) j -> f a j
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 b j -> a j
forall k (f :: k -> Type) (g :: k -> Type) (i :: k).
(:*:) f g i -> f i
ifst) (f b j -> b j
forall j. f b j -> b j
algr (f b j -> b j) -> (f (a :*: b) j -> f b j) -> f (a :*: b) j -> b j
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall j. (:*:) a b j -> b j) -> f (a :*: b) j -> f b j
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 b j -> b j
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 |> :: (a -> Maybe a) -> (a -> a) -> a -> a
(|>) = (Maybe a -> a -> 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 ((a -> Maybe a -> a) -> Maybe a -> a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe)
instance {-# OVERLAPS #-}     Chain a (Maybe a) where |> :: (a -> Maybe a) -> (a -> Maybe a) -> a -> Maybe a
(|>) = (Maybe a -> Maybe a -> Maybe 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 Maybe a -> Maybe a -> Maybe a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
(<|>)

data Unit1 k = Unit
newtype Const1 a k = Const1 {Const1 a k -> a
getConst1 :: a}

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