module Pandora.Pattern (module Exports, (.|..), (.|...), (.|....)) where

import Pandora.Pattern.Object as Exports
import Pandora.Pattern.Transformer as Exports
import Pandora.Pattern.Functor as Exports
import Pandora.Pattern.Category as Exports

import Pandora.Core.Functor (type (:.), type (:=))

infixr 7 .|.., .|..., .|....

(.|..) :: (Category v, Covariant (v a))
	=> v c d -> v a :. v b := c -> v a :. v b := d
v c d
f .|.. :: v c d -> ((v a :. v b) := c) -> (v a :. v b) := d
.|.. (v a :. v b) := c
g = (v c d
f v c d -> v b c -> v b d
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
.) (v b c -> v b d) -> ((v a :. v b) := c) -> (v a :. v b) := d
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (v a :. v b) := c
g

(.|...) :: (Category v, Covariant (v a), Covariant (v b))
	=> v d e -> v a :. v b :. v c := d -> v a :. v b :. v c := e
v d e
f .|... :: v d e -> ((v a :. (v b :. v c)) := d) -> (v a :. (v b :. v c)) := e
.|... (v a :. (v b :. v c)) := d
g = (v d e
f v d e -> v c d -> v c e
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
.) (v c d -> v c e)
-> ((v a :. (v b :. v c)) := d) -> (v a :. (v b :. v c)) := e
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
<$$> (v a :. (v b :. v c)) := d
g

(.|....) :: (Category v, Covariant (v a), Covariant (v b), Covariant (v c))
	=> v e f -> v a :. v b :. v c :. v d := e -> v a :. v b :. v c :. v d := f
v e f
f .|.... :: v e f
-> ((v a :. (v b :. (v c :. v d))) := e)
-> (v a :. (v b :. (v c :. v d))) := f
.|.... (v a :. (v b :. (v c :. v d))) := e
g = (v e f
f v e f -> v d e -> v d f
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
.) (v d e -> v d f)
-> ((v a :. (v b :. (v c :. v d))) := e)
-> (v a :. (v b :. (v c :. v d))) := f
forall (t :: * -> *) (u :: * -> *) (v :: * -> *) a b.
(Covariant t, Covariant u, Covariant v) =>
(a -> b) -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b
<$$$> (v a :. (v b :. (v c :. v d))) := e
g