{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE CPP                 #-}
{-# LANGUAGE InstanceSigs        #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE MonoLocalBinds      #-}

{-# OPTIONS_GHC -Wall #-}
-- {-# OPTIONS_GHC -Wno-unused-imports #-} -- TEMP

-- | Various functions to ease syntax construction from the plugin

module ConCat.Translators where

import Prelude hiding (id,(.),curry,uncurry,const,unzip,zip,zipWith)
import qualified Prelude as P
import GHC.Exts (Coercible,coerce) -- inline

import Data.Pointed
import Data.Key (Zip(..))

import ConCat.Misc ((:*),result)
import ConCat.AltCat hiding (Strong, strength)

-- I could use this simpler style to simplify the plugin, e.g.,

appT :: forall a b c. (a -> b -> c) -> (a -> b) -> (a -> c)
appT :: forall a b c. (a -> b -> c) -> (a -> b) -> a -> c
appT a -> Exp (->) b c
f a -> b
g = Prod (->) (Exp (->) b c) b -> c
forall (k :: * -> * -> *) a b.
(ClosedCat k, Ok2 k a b) =>
k (Prod k (Exp k a b) a) b
apply (Prod (->) (Exp (->) b c) b -> c)
-> (a -> Prod (->) (Exp (->) b c) b) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (a -> Exp (->) b c
f (a -> Exp (->) b c) -> (a -> b) -> a -> Prod (->) (Exp (->) b c) b
forall (k :: * -> * -> *) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& a -> b
g)
{-# INLINE appT #-}

-- The plugin would then turn `\ x -> U V` into `appT (\ x -> U) (\ x -> V)`.
-- Or leave the `toCcc'` call in the plugin for separation of concerns.

casePairTopT :: forall b c d. b :* c -> (b -> c -> d) -> d
casePairTopT :: forall b c d. (b :* c) -> (b -> c -> d) -> d
casePairTopT b :* c
bc b -> c -> d
g = (b -> c -> d) -> (b :* c) -> d
forall a b c. (a -> b -> c) -> (a :* b) -> c
uncurryC b -> c -> d
g b :* c
bc
{-# INLINE casePairTopT #-}

casePairT :: forall a b c d. (a -> b :* c) -> (a -> b -> c -> d) -> (a -> d)
casePairT :: forall a b c d. (a -> b :* c) -> (a -> b -> c -> d) -> a -> d
casePairT a -> b :* c
f a -> b -> c -> d
g = (a -> (b :* c) -> d) -> Prod (->) a (b :* c) -> d
forall a b c. (a -> b -> c) -> (a :* b) -> c
uncurryC (((b -> c -> d) -> (b :* c) -> d)
-> (a -> b -> c -> d) -> a -> (b :* c) -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
result (b -> c -> d) -> (b :* c) -> d
forall a b c. (a -> b -> c) -> (a :* b) -> c
uncurryC a -> b -> c -> d
g) (Prod (->) a (b :* c) -> d)
-> (a -> Prod (->) a (b :* c)) -> a -> d
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (a -> a
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id (a -> a) -> (a -> b :* c) -> a -> Prod (->) a (b :* c)
forall (k :: * -> * -> *) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& a -> b :* c
f)
{-# INLINE casePairT #-}

uncurryC :: (a -> b -> c) -> (a :* b -> c)
uncurryC :: forall a b c. (a -> b -> c) -> (a :* b) -> c
uncurryC a -> b -> c
f a :* b
w = a -> b -> c
f ((a :* b) -> a
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exl a :* b
w) ((a :* b) -> b
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exr a :* b
w)
{-# INLINE uncurryC #-}

-- Unused a
casePairQT :: forall a b c d. (a -> b :* c) -> (b -> c -> d) -> (a -> d)
casePairQT :: forall a b c d. (a -> b :* c) -> (b -> c -> d) -> a -> d
casePairQT a -> b :* c
f b -> c -> d
g = (b -> c -> d) -> (b :* c) -> d
forall a b c. (a -> b -> c) -> (a :* b) -> c
uncurryC b -> c -> d
g ((b :* c) -> d) -> (a -> b :* c) -> a -> d
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. a -> b :* c
f
{-# INLINE casePairQT #-}

-- Unused c
casePairLT :: forall a b c d. (a -> b :* c) -> (a -> b -> d) -> (a -> d)
casePairLT :: forall a b c d. (a -> b :* c) -> (a -> b -> d) -> a -> d
casePairLT a -> Prod (->) b c
f a -> b -> d
g = (a -> b -> d) -> Prod (->) a b -> d
forall a b c. (a -> b -> c) -> (a :* b) -> c
uncurryC a -> b -> d
g (Prod (->) a b -> d) -> (a -> Prod (->) a b) -> a -> d
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (a -> a
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id (a -> a) -> (a -> b) -> a -> Prod (->) a b
forall (k :: * -> * -> *) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& Prod (->) b c -> b
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exl (Prod (->) b c -> b) -> (a -> Prod (->) b c) -> a -> b
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. a -> Prod (->) b c
f)
{-# INLINE casePairLT #-}

-- Unused b
casePairRT :: forall a b c d. (a -> b :* c) -> (a -> c -> d) -> (a -> d)
casePairRT :: forall a b c d. (a -> b :* c) -> (a -> c -> d) -> a -> d
casePairRT a -> Prod (->) b c
f a -> c -> d
g = (a -> c -> d) -> Prod (->) a c -> d
forall a b c. (a -> b -> c) -> (a :* b) -> c
uncurryC a -> c -> d
g (Prod (->) a c -> d) -> (a -> Prod (->) a c) -> a -> d
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (a -> a
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id (a -> a) -> (a -> c) -> a -> Prod (->) a c
forall (k :: * -> * -> *) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& Prod (->) b c -> c
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exr (Prod (->) b c -> c) -> (a -> Prod (->) b c) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. a -> Prod (->) b c
f)
{-# INLINE casePairRT #-}

-- TODO: given examples of casePairLT and casePairRT, try using the general
-- casePairT instead, and see how well GHC optimizes it. And/or dig up the
-- journal notes I made when I chose to make these special cases.

-- One drawback of using these function-only definitions is that the plugin
-- cannot first check whether the target category has the required properties,
-- such as `ClosedCat`.

-- TODO: Maybe use the following function-only definition instead, and wrap
-- toCcc' around it in the plugin.

type Strong h = (Zip h, Pointed h)

-- Functorial strength
strength :: (Zip h, Pointed h) => a :* h b -> h (a :* b)
strength :: forall (h :: * -> *) a b.
(Zip h, Pointed h) =>
(a :* h b) -> h (a :* b)
strength = (h a :* h b) -> h (a :* b)
forall (k :: * -> * -> *) (h :: * -> *) a b.
(ZipCat k h, Ok2 k a b) =>
k (h a :* h b) (h (a :* b))
zipC ((h a :* h b) -> h (a :* b))
-> (Prod (->) a (h b) -> h a :* h b)
-> Prod (->) a (h b)
-> h (a :* b)
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (a -> h a) -> Prod (->) a (h b) -> h a :* h b
forall (k :: * -> * -> *) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first a -> h a
forall (k :: * -> * -> *) (h :: * -> *) a.
PointedCat k h a =>
k a (h a)
pointC
{-# INLINE strength #-}

fmapT1 :: forall h a b c. Strong h => (a -> b -> c) -> (a -> h b -> h c)
fmapT1 :: forall (h :: * -> *) a b c.
Strong h =>
(a -> b -> c) -> a -> h b -> h c
fmapT1 a -> b -> c
f = ((a, h b) -> h c) -> a -> h b -> h c
forall a b c. ((a, b) -> c) -> a -> b -> c
P.curry (((a, b) -> c) -> h (a, b) -> h c
forall (k :: * -> * -> *) (h :: * -> *) a b.
(FunctorCat k h, Ok2 k a b) =>
k a b -> k (h a) (h b)
fmapC ((a -> b -> c) -> (a, b) -> c
forall a b c. (a -> b -> c) -> (a :* b) -> c
P.uncurry a -> b -> c
f) (h (a, b) -> h c) -> ((a, h b) -> h (a, b)) -> (a, h b) -> h c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (a, h b) -> h (a, b)
forall (h :: * -> *) a b.
(Zip h, Pointed h) =>
(a :* h b) -> h (a :* b)
strength)
{-# INLINE fmapT1 #-}

fmapT2 :: forall h a b c. (Zip h, Pointed h)
       => (a -> b -> c) -> (a -> h b) -> (a -> h c)
-- fmapT2 f g = fmapC (P.uncurry f) . strength . (id &&& g)
fmapT2 :: forall (h :: * -> *) a b c.
(Zip h, Pointed h) =>
(a -> b -> c) -> (a -> h b) -> a -> h c
fmapT2 a -> b -> c
f a -> h b
g = ((a :* b) -> c) -> h (a :* b) -> h c
forall (k :: * -> * -> *) (h :: * -> *) a b.
(FunctorCat k h, Ok2 k a b) =>
k a b -> k (h a) (h b)
fmapC ((a -> b -> c) -> (a :* b) -> c
forall a b c. (a -> b -> c) -> (a :* b) -> c
P.uncurry a -> b -> c
f) (h (a :* b) -> h c) -> (a -> h (a :* b)) -> a -> h c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (h a :* h b) -> h (a :* b)
forall (k :: * -> * -> *) (h :: * -> *) a b.
(ZipCat k h, Ok2 k a b) =>
k (h a :* h b) (h (a :* b))
zipC ((h a :* h b) -> h (a :* b))
-> (a -> h a :* h b) -> a -> h (a :* b)
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (a -> h a
forall (k :: * -> * -> *) (h :: * -> *) a.
PointedCat k h a =>
k a (h a)
pointC (a -> h a) -> (a -> h b) -> a -> h a :* h b
forall (k :: * -> * -> *) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& a -> h b
g)
{-# INLINE fmapT2 #-}

#if 0

id &&& g          :: a -> a :* h b
strength          :: a :* h b -> h (a :* b)
fmapC (uncurry f) :: h (a :* b) -> h c

pointC &&& g      :: a -> h a * h b
zipC              :: h a :* h b -> h (a :* b)
fmapC (uncurry f) :: h (a :* b) -> h c

#endif

flipForkT :: forall k z a b. (IxProductCat k ((->) a), Ok2 k z b)
          => (z -> a -> b) -> (z `k` (a -> b))
-- flipForkT f = forkF (toCcc' P.. flip f)
-- flipForkT f = forkF (\ a -> toCcc' (flip f a))
flipForkT :: forall (k :: * -> * -> *) z a b.
(IxProductCat k ((->) a), Ok2 k z b) =>
(z -> a -> b) -> k z (a -> b)
flipForkT z -> a -> b
f = (a -> k z b) -> k z (a -> b)
forall (k :: * -> * -> *) (h :: * -> *) a b.
(IxProductCat k h, Ok2 k a b) =>
h (k a b) -> k a (h b)
forkF (\ a
a -> (z -> b) -> k z b
forall (k :: * -> * -> *) a b. (a -> b) -> k a b
toCcc' (\ z
z -> z -> a -> b
f z
z a
a))
{-# INLINE flipForkT #-}

--        f :: z -> a -> b
-- toCcc' f :: z `k` (a -> b)

-- flip f :: a -> z -> b  -- or forkF f
-- toCcc' . flip f :: a -> (z `k` b)
-- forkF (toCcc' . flip f) :: z `k` (a -> b)

forkUnforkT :: forall k h a b.
       (IxProductCat (->) h, Functor h, IxProductCat k h, Ok2 k a b)
    => (a -> h b) -> (a `k` h b)
forkUnforkT :: forall (k :: * -> * -> *) (h :: * -> *) a b.
(IxProductCat (->) h, Functor h, IxProductCat k h, Ok2 k a b) =>
(a -> h b) -> k a (h b)
forkUnforkT a -> h b
f = h (k a b) -> k a (h b)
forall (k :: * -> * -> *) (h :: * -> *) a b.
(IxProductCat k h, Ok2 k a b) =>
h (k a b) -> k a (h b)
forkF (((a -> b) -> k a b) -> h (a -> b) -> h (k a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap' (a -> b) -> k a b
forall (k :: * -> * -> *) a b. (a -> b) -> k a b
toCcc' ((a -> h b) -> h (a -> b)
forall (k :: * -> * -> *) (h :: * -> *) a b.
(IxProductCat k h, Functor h, Ok2 k a b) =>
k a (h b) -> h (k a b)
unforkF a -> h b
f))
{-# INLINE forkUnforkT #-}

--                           f  :: a -> h b
--                   unforkF f  :: h (a -> b)
--        toCcc' <$> unforkF f  :: h (a `k` b)
-- forkF (toCcc' <$> unforkF f) :: a `k` h b

-- castConstT :: forall a b b'. Coercible b b' => b -> (a -> b')
-- -- castConstT b = P.const (coerce b)
-- castConstT b = const (coerce b)
-- {-# INLINE castConstT #-}

castConstT :: forall k a b b'. (ConstCat k b', Ok k a, Coercible b b')
           => b -> (a `k` b')
castConstT :: forall (k :: * -> * -> *) a b b'.
(ConstCat k b', Ok k a, Coercible b b') =>
b -> k a b'
castConstT b
b = b' -> k a b'
forall (k :: * -> * -> *) b a. (ConstCat k b, Ok k a) => b -> k a b
const (b -> b'
forall a b. Coercible a b => a -> b
coerce b
b)
{-# INLINE castConstT #-}

bottomT :: forall k a b. (Category k, TerminalCat k, BottomCat k () b, Ok2 k a b)
        => a `k` b
bottomT :: forall (k :: * -> * -> *) a b.
(Category k, TerminalCat k, BottomCat k () b, Ok2 k a b) =>
k a b
bottomT = k () b
forall (k :: * -> * -> *) a b. BottomCat k a b => k a b
bottomC k () b -> k a () -> k a b
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. k a ()
forall (k :: * -> * -> *) a. (TerminalCat k, Ok k a) => k a ()
it
{-# INLINE bottomT #-}