{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeAbstractions #-}

module Data.PTraversable.Internal.Day (ptraverseDay) where

import Prelude hiding (Enum)
import Data.Profunctor.Cocartesian.Free

import Data.Profunctor
import Data.Profunctor.Cartesian

import Data.Functor.Day ( Day(..) )
import Control.Monad.Trans.State.Lazy (State, state, evalState)

import qualified Data.Vector as V
import Data.Bifunctor (Bifunctor(..))
import GHC.TypeNats
import Data.Finite (Finite, getFinite, finite)
import Data.Monoid (Endo(..))

type Optic p s t a b = p a b -> p s t
type Traversal s t a b = forall p. (Cartesian p, Cocartesian p) => Optic p s t a b

-- An "instance" of (PTraversable t). They are used instead of constraint (PTraversable t),
-- because this module can't depend on Data.PTraversable module to avoid circular import.
type PT t = forall a b. Traversal (t a) (t b) a b

-- Explicit versions of superclasses of Traversal
traverseWith :: (Applicative f) => PT t -> (a -> f b) -> t a -> f (t b)
traverseWith :: forall (f :: * -> *) (t :: * -> *) a b.
Applicative f =>
PT t -> (a -> f b) -> t a -> f (t b)
traverseWith PT t
travT a -> f b
f = Star f (t a) (t b) -> t a -> f (t b)
forall {k} (f :: k -> *) d (c :: k). Star f d c -> d -> f c
runStar (Optic (Star f) (t a) (t b) a b
PT t
travT ((a -> f b) -> Star f a b
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star a -> f b
f))

fmapWith :: PT t -> (a -> b) -> t a -> t b
fmapWith :: forall (t :: * -> *) a b. PT t -> (a -> b) -> t a -> t b
fmapWith = Optic (->) (t a) (t b) a b -> Optic (->) (t a) (t b) a b
PT t -> Optic (->) (t a) (t b) a b
forall a. a -> a
id

foldrWith :: PT t -> (a -> r -> r) -> r -> t a -> r
foldrWith :: forall (t :: * -> *) a r. PT t -> (a -> r -> r) -> r -> t a -> r
foldrWith PT t
travT a -> r -> r
f r
z t a
ta = ((r -> r) -> r -> r
forall a b. (a -> b) -> a -> b
$ r
z) ((r -> r) -> r) -> (r -> r) -> r
forall a b. (a -> b) -> a -> b
$ Endo r -> r -> r
forall a. Endo a -> a -> a
appEndo (Endo r -> r -> r) -> Endo r -> r -> r
forall a b. (a -> b) -> a -> b
$ Forget (Endo r) (t a) (t (ZonkAny 0)) -> t a -> Endo r
forall {k} r a (b :: k). Forget r a b -> a -> r
runForget (Optic (Forget (Endo r)) (t a) (t (ZonkAny 0)) a (ZonkAny 0)
PT t
travT ((a -> Endo r) -> Forget (Endo r) a (ZonkAny 0)
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget ((a -> Endo r) -> Forget (Endo r) a (ZonkAny 0))
-> (a -> Endo r) -> Forget (Endo r) a (ZonkAny 0)
forall a b. (a -> b) -> a -> b
$ (r -> r) -> Endo r
forall a. (a -> a) -> Endo a
Endo ((r -> r) -> Endo r) -> (a -> r -> r) -> a -> Endo r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> r -> r
f)) t a
ta

toListWith :: PT t -> t a -> [a]
toListWith :: forall (t :: * -> *) a. PT t -> t a -> [a]
toListWith PT t
travT = PT t -> (a -> [a] -> [a]) -> [a] -> t a -> [a]
forall (t :: * -> *) a r. PT t -> (a -> r -> r) -> r -> t a -> r
foldrWith Optic p (t a) (t b) a b
PT t
travT (:) []

indices :: PT t -> t a -> t Int
indices :: forall (t :: * -> *) a. PT t -> t a -> t Int
indices PT t
travT t a
ta = State Int (t Int) -> Int -> t Int
forall s a. State s a -> s -> a
evalState (PT t -> (a -> StateT Int Identity Int) -> t a -> State Int (t Int)
forall (f :: * -> *) (t :: * -> *) a b.
Applicative f =>
PT t -> (a -> f b) -> t a -> f (t b)
traverseWith Optic p (t a) (t b) a b
PT t
travT a -> StateT Int Identity Int
forall x. x -> StateT Int Identity Int
indexStep t a
ta) Int
0
  where
    indexStep :: x -> State Int Int
    indexStep :: forall x. x -> StateT Int Identity Int
indexStep x
_ = (Int -> (Int, Int)) -> StateT Int Identity Int
forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state ((Int -> (Int, Int)) -> StateT Int Identity Int)
-> (Int -> (Int, Int)) -> StateT Int Identity Int
forall a b. (a -> b) -> a -> b
$ \Int
n -> Int
n Int -> (Int, Int) -> (Int, Int)
forall a b. a -> b -> b
`seq` (Int
n, Int -> Int
forall a. Enum a => a -> a
succ Int
n)

-- * Auxiliary definitions

-- Mono
data Mono a b = M b Natural

instance Profunctor Mono where
  dimap :: forall a b c d. (a -> b) -> (c -> d) -> Mono b c -> Mono a d
dimap a -> b
_ c -> d
g (M c
b Natural
e) = d -> Natural -> Mono a d
forall a b. b -> Natural -> Mono a b
M (c -> d
g c
b) Natural
e

instance Cartesian Mono where
  proUnit :: forall a. Mono a ()
proUnit = () -> Natural -> Mono a ()
forall a b. b -> Natural -> Mono a b
M () Natural
0
  M b
b Natural
e *** :: forall a b a' b'. Mono a b -> Mono a' b' -> Mono (a, a') (b, b')
*** M b'
b' Natural
f = (b, b') -> Natural -> Mono (a, a') (b, b')
forall a b. b -> Natural -> Mono a b
M (b
b, b'
b') (Natural
e Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
f)

-- Polynomial is sum of monomials
type Poly = FreeCocartesian Mono

idPoly :: Poly () ()
idPoly :: Poly () ()
idPoly = Mono () () -> Poly () ()
forall (p :: * -> * -> *) a b. p a b -> FreeCocartesian p a b
liftF (() -> Natural -> Mono () ()
forall a b. b -> Natural -> Mono a b
M () Natural
1)

-- Adds context @s,t@ to a @Cocartesian p@.
newtype ContextT s t p a b = ContextT {
    forall s t (p :: * -> * -> *) a b.
ContextT s t p a b -> p (a, s) (b, t)
unContextT :: p (a,s) (b,t)
  }

instance Profunctor p => Profunctor (ContextT s t p) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> ContextT s t p b c -> ContextT s t p a d
dimap a -> b
f c -> d
g = p (a, s) (d, t) -> ContextT s t p a d
forall s t (p :: * -> * -> *) a b.
p (a, s) (b, t) -> ContextT s t p a b
ContextT (p (a, s) (d, t) -> ContextT s t p a d)
-> (ContextT s t p b c -> p (a, s) (d, t))
-> ContextT s t p b c
-> ContextT s t p a d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, s) -> (b, s))
-> ((c, t) -> (d, t)) -> p (b, s) (c, t) -> p (a, s) (d, t)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((a -> b) -> (a, s) -> (b, s)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a -> b
f) ((c -> d) -> (c, t) -> (d, t)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first c -> d
g) (p (b, s) (c, t) -> p (a, s) (d, t))
-> (ContextT s t p b c -> p (b, s) (c, t))
-> ContextT s t p b c
-> p (a, s) (d, t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextT s t p b c -> p (b, s) (c, t)
forall s t (p :: * -> * -> *) a b.
ContextT s t p a b -> p (a, s) (b, t)
unContextT

instance Cocartesian p => Cocartesian (ContextT s t p) where
  proEmpty :: forall b. ContextT s t p Void b
proEmpty = p (Void, s) (b, t) -> ContextT s t p Void b
forall s t (p :: * -> * -> *) a b.
p (a, s) (b, t) -> ContextT s t p a b
ContextT (p (Void, s) (b, t) -> ContextT s t p Void b)
-> p (Void, s) (b, t) -> ContextT s t p Void b
forall a b. (a -> b) -> a -> b
$ ((Void, s) -> Void)
-> ((b, t) -> (b, t)) -> p Void (b, t) -> p (Void, s) (b, t)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (Void, s) -> Void
forall a b. (a, b) -> a
fst (b, t) -> (b, t)
forall a. a -> a
id p Void (b, t)
forall b. p Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty
  ContextT p (a, s) (b, t)
p +++ :: forall a b a' b'.
ContextT s t p a b
-> ContextT s t p a' b'
-> ContextT s t p (Either a a') (Either b b')
+++ ContextT p (a', s) (b', t)
q = p (Either a a', s) (Either b b', t)
-> ContextT s t p (Either a a') (Either b b')
forall s t (p :: * -> * -> *) a b.
p (a, s) (b, t) -> ContextT s t p a b
ContextT (p (Either a a', s) (Either b b', t)
 -> ContextT s t p (Either a a') (Either b b'))
-> p (Either a a', s) (Either b b', t)
-> ContextT s t p (Either a a') (Either b b')
forall a b. (a -> b) -> a -> b
$ ((Either a a', s) -> Either (a, s) (a', s))
-> (Either (b, t) (b', t) -> (Either b b', t))
-> p (Either (a, s) (a', s)) (Either (b, t) (b', t))
-> p (Either a a', s) (Either b b', t)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (Either a a', s) -> Either (a, s) (a', s)
forall a1 a2 b. (Either a1 a2, b) -> Either (a1, b) (a2, b)
distR Either (b, t) (b', t) -> (Either b b', t)
forall a1 b a2. Either (a1, b) (a2, b) -> (Either a1 a2, b)
undistR (p (a, s) (b, t)
p p (a, s) (b, t)
-> p (a', s) (b', t)
-> p (Either (a, s) (a', s)) (Either (b, t) (b', t))
forall a b a' b'. p a b -> p a' b' -> p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ p (a', s) (b', t)
q)

-----------

type Day' t u x = ((t (), u ()), Int -> Int -> x)

ptraverseDay :: forall t u p a b.
     (Cartesian p, Cocartesian p)
  => PT t -> PT u
  -> p a b -> p (Day t u a) (Day t u b)
ptraverseDay :: forall (t :: * -> *) (u :: * -> *) (p :: * -> * -> *) a b.
(Cartesian p, Cocartesian p) =>
PT t -> PT u -> p a b -> p (Day t u a) (Day t u b)
ptraverseDay PT t
travT PT u
travU p a b
p = (Day t u a -> Day' t u a)
-> (Day' t u b -> Day t u b)
-> p (Day' t u a) (Day' t u b)
-> p (Day t u a) (Day t u b)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap Day t u a -> Day' t u a
pre Day' t u b -> Day t u b
post p (Day' t u a) (Day' t u b)
travDay'
  where
    tShapes :: Poly (t ()) (t ())
    tShapes :: Poly (t ()) (t ())
tShapes = Optic (FreeCocartesian Mono) (t ()) (t ()) () ()
PT t
travT Poly () ()
idPoly

    uShapes :: Poly (u ()) (u ())
    uShapes :: Poly (u ()) (u ())
uShapes = Optic (FreeCocartesian Mono) (u ()) (u ()) () ()
PT u
travU Poly () ()
idPoly

    travDay' :: p (Day' t u a) (Day' t u b)
    travDay' :: p (Day' t u a) (Day' t u b)
travDay' = ContextT
  (Int -> Int -> a) (Int -> Int -> b) p (t (), u ()) (t (), u ())
-> p (Day' t u a) (Day' t u b)
forall s t (p :: * -> * -> *) a b.
ContextT s t p a b -> p (a, s) (b, t)
unContextT (ContextT
   (Int -> Int -> a) (Int -> Int -> b) p (t (), u ()) (t (), u ())
 -> p (Day' t u a) (Day' t u b))
-> ContextT
     (Int -> Int -> a) (Int -> Int -> b) p (t (), u ()) (t (), u ())
-> p (Day' t u a) (Day' t u b)
forall a b. (a -> b) -> a -> b
$ (ContextT (Int -> Int -> a) (Int -> Int -> b) p
 :-> ContextT (Int -> Int -> a) (Int -> Int -> b) p)
-> FreeCocartesian (ContextT (Int -> Int -> a) (Int -> Int -> b) p)
   :-> ContextT (Int -> Int -> a) (Int -> Int -> b) p
forall (q :: * -> * -> *) (p :: * -> * -> *).
Cocartesian q =>
(p :-> q) -> FreeCocartesian p :-> q
foldFree ContextT (Int -> Int -> a) (Int -> Int -> b) p a b
-> ContextT (Int -> Int -> a) (Int -> Int -> b) p a b
forall a. a -> a
ContextT (Int -> Int -> a) (Int -> Int -> b) p
:-> ContextT (Int -> Int -> a) (Int -> Int -> b) p
id (ProductOp
  Mono Mono (ContextT (Int -> Int -> a) (Int -> Int -> b) p)
-> Poly (t ()) (t ())
-> Poly (u ()) (u ())
-> FreeCocartesian
     (ContextT (Int -> Int -> a) (Int -> Int -> b) p)
     (t (), u ())
     (t (), u ())
forall (p :: * -> * -> *) (q :: * -> * -> *) (r :: * -> * -> *) a b
       a' b'.
ProductOp p q r
-> FreeCocartesian p a b
-> FreeCocartesian q a' b'
-> FreeCocartesian r (a, a') (b, b')
multF (p a b
-> Mono a1 b1
-> Mono a2 b2
-> ContextT (Int -> Int -> a) (Int -> Int -> b) p (a1, a2) (b1, b2)
forall (p :: * -> * -> *) a b s0 t0 s1 t1.
Cartesian p =>
p a b
-> Mono s0 t0
-> Mono s1 t1
-> ContextT (Int -> Int -> a) (Int -> Int -> b) p (s0, s1) (t0, t1)
interpretMonos p a b
p) Poly (t ()) (t ())
tShapes Poly (u ()) (u ())
uShapes)

    pre :: Day t u a -> Day' t u a
    pre :: Day t u a -> Day' t u a
pre (Day t b
tb u c
uc b -> c -> a
op) = ((t ()
t1, u ()
u1), Int -> Int -> a
op')
      where
        t1 :: t ()
t1 = PT t -> (b -> ()) -> t b -> t ()
forall (t :: * -> *) a b. PT t -> (a -> b) -> t a -> t b
fmapWith Optic p (t a) (t b) a b
PT t
travT (() -> b -> ()
forall a b. a -> b -> a
const ()) t b
tb
        bs :: Vector b
bs = [b] -> Vector b
forall a. [a] -> Vector a
V.fromList (PT t -> t b -> [b]
forall (t :: * -> *) a. PT t -> t a -> [a]
toListWith Optic p (t a) (t b) a b
PT t
travT t b
tb)
        u1 :: u ()
u1 = PT u -> (c -> ()) -> u c -> u ()
forall (t :: * -> *) a b. PT t -> (a -> b) -> t a -> t b
fmapWith Optic p (u a) (u b) a b
PT u
travU (() -> c -> ()
forall a b. a -> b -> a
const ()) u c
uc
        cs :: Vector c
cs = [c] -> Vector c
forall a. [a] -> Vector a
V.fromList (PT u -> u c -> [c]
forall (t :: * -> *) a. PT t -> t a -> [a]
toListWith Optic p (u a) (u b) a b
PT u
travU u c
uc)
        op' :: Int -> Int -> a
op' Int
i Int
j = b -> c -> a
op (Vector b
bs Vector b -> Int -> b
forall a. Vector a -> Int -> a
V.! Int
i) (Vector c
cs Vector c -> Int -> c
forall a. Vector a -> Int -> a
V.! Int
j)

    post :: Day' t u b -> Day t u b
    post :: Day' t u b -> Day t u b
post ((t ()
t1, u ()
u1), Int -> Int -> b
op) = t Int -> u Int -> (Int -> Int -> b) -> Day t u b
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day (PT t -> t () -> t Int
forall (t :: * -> *) a. PT t -> t a -> t Int
indices Optic p (t a) (t b) a b
PT t
travT t ()
t1) (PT u -> u () -> u Int
forall (t :: * -> *) a. PT t -> t a -> t Int
indices Optic p (u a) (u b) a b
PT u
travU u ()
u1) Int -> Int -> b
op

interpretMonos ::
  forall p a b s0 t0 s1 t1.
     (Cartesian p)
  => p a b
  -> Mono s0 t0 -> Mono s1 t1 -> ContextT (Int -> Int -> a) (Int -> Int -> b) p (s0, s1) (t0, t1)
interpretMonos :: forall (p :: * -> * -> *) a b s0 t0 s1 t1.
Cartesian p =>
p a b
-> Mono s0 t0
-> Mono s1 t1
-> ContextT (Int -> Int -> a) (Int -> Int -> b) p (s0, s1) (t0, t1)
interpretMonos p a b
p (M t0
t0 Natural
m) (M t1
t1 Natural
n)
  | Natural
m Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0 Bool -> Bool -> Bool
|| Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0 = p ((s0, s1), Int -> Int -> a) ((t0, t1), Int -> Int -> b)
-> ContextT (Int -> Int -> a) (Int -> Int -> b) p (s0, s1) (t0, t1)
forall s t (p :: * -> * -> *) a b.
p (a, s) (b, t) -> ContextT s t p a b
ContextT (p ((s0, s1), Int -> Int -> a) ((t0, t1), Int -> Int -> b)
 -> ContextT
      (Int -> Int -> a) (Int -> Int -> b) p (s0, s1) (t0, t1))
-> p ((s0, s1), Int -> Int -> a) ((t0, t1), Int -> Int -> b)
-> ContextT (Int -> Int -> a) (Int -> Int -> b) p (s0, s1) (t0, t1)
forall a b. (a -> b) -> a -> b
$ (() -> ((t0, t1), Int -> Int -> b))
-> p ((s0, s1), Int -> Int -> a) ()
-> p ((s0, s1), Int -> Int -> a) ((t0, t1), Int -> Int -> b)
forall b c a. (b -> c) -> p a b -> p a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap (((t0, t1), Int -> Int -> b) -> () -> ((t0, t1), Int -> Int -> b)
forall a b. a -> b -> a
const ((t0
t0,t1
t1), \Int
_ Int
_ -> [Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"should not reach here")) p ((s0, s1), Int -> Int -> a) ()
forall a. p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit
  | Bool
otherwise = p ((s0, s1), Int -> Int -> a) ((t0, t1), Int -> Int -> b)
-> ContextT (Int -> Int -> a) (Int -> Int -> b) p (s0, s1) (t0, t1)
forall s t (p :: * -> * -> *) a b.
p (a, s) (b, t) -> ContextT s t p a b
ContextT (p ((s0, s1), Int -> Int -> a) ((t0, t1), Int -> Int -> b)
 -> ContextT
      (Int -> Int -> a) (Int -> Int -> b) p (s0, s1) (t0, t1))
-> p ((s0, s1), Int -> Int -> a) ((t0, t1), Int -> Int -> b)
-> ContextT (Int -> Int -> a) (Int -> Int -> b) p (s0, s1) (t0, t1)
forall a b. (a -> b) -> a -> b
$ (((s0, s1), Int -> Int -> a) -> Natural -> a)
-> ((Natural -> b) -> ((t0, t1), Int -> Int -> b))
-> p (Natural -> a) (Natural -> b)
-> p ((s0, s1), Int -> Int -> a) ((t0, t1), Int -> Int -> b)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((s0, s1), Int -> Int -> a) -> Natural -> a
pre (Natural -> b) -> ((t0, t1), Int -> Int -> b)
post (p (Natural -> a) (Natural -> b)
 -> p ((s0, s1), Int -> Int -> a) ((t0, t1), Int -> Int -> b))
-> p (Natural -> a) (Natural -> b)
-> p ((s0, s1), Int -> Int -> a) ((t0, t1), Int -> Int -> b)
forall a b. (a -> b) -> a -> b
$ p a b -> Natural -> p (Natural -> a) (Natural -> b)
forall (p :: * -> * -> *) a b.
Cartesian p =>
p a b -> Natural -> p (Natural -> a) (Natural -> b)
powPowerPartial p a b
p (Natural
m Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
n)
    where
      pre :: ((s0, s1), Int -> Int -> a) -> Natural -> a
      pre :: ((s0, s1), Int -> Int -> a) -> Natural -> a
pre ((s0, s1)
_, Int -> Int -> a
op) Natural
i = case Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
quotRem (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
i) (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
m) of
        (Int
j,Int
k) -> Int -> Int -> a
op Int
j Int
k
      
      post :: (Natural -> b) -> ((t0, t1), Int -> Int -> b)
      post :: (Natural -> b) -> ((t0, t1), Int -> Int -> b)
post Natural -> b
f = ((t0
t0, t1
t1), \Int
j Int
k -> Natural -> b
f (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
j Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
m Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k))

powPowerPartial :: Cartesian p => p a b -> Natural -> p (Natural -> a) (Natural -> b)
powPowerPartial :: forall (p :: * -> * -> *) a b.
Cartesian p =>
p a b -> Natural -> p (Natural -> a) (Natural -> b)
powPowerPartial p a b
p Natural
n = case Natural -> SomeNat
someNatVal Natural
n of
  SomeNat Proxy n
sn -> ((Natural -> a) -> Finite n -> a)
-> ((Finite n -> b) -> Natural -> b)
-> p (Finite n -> a) (Finite n -> b)
-> p (Natural -> a) (Natural -> b)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((Natural -> a) -> (Finite n -> Natural) -> Finite n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural)
-> (Finite n -> Integer) -> Finite n -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> Integer
forall (n :: Natural). Finite n -> Integer
getFinite) ((Finite n -> b) -> (Natural -> Finite n) -> Natural -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy n -> Natural -> Finite n
forall (proxy :: Natural -> *) (n :: Natural).
KnownNat n =>
proxy n -> Natural -> Finite n
toFinite' Proxy n
sn) (p a b -> p (Finite n -> a) (Finite n -> b)
forall (n :: Natural) a b.
KnownNat n =>
p a b -> p (Finite n -> a) (Finite n -> b)
forall (p :: * -> * -> *) (n :: Natural) a b.
(Cartesian p, KnownNat n) =>
p a b -> p (Finite n -> a) (Finite n -> b)
proPower p a b
p)
  where
    toFinite' :: forall proxy n. KnownNat n => proxy n -> Natural -> Finite n
    toFinite' :: forall (proxy :: Natural -> *) (n :: Natural).
KnownNat n =>
proxy n -> Natural -> Finite n
toFinite' proxy n
_ = Integer -> Finite n
forall (n :: Natural). KnownNat n => Integer -> Finite n
finite (Integer -> Finite n)
-> (Natural -> Integer) -> Natural -> Finite n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Integer
forall a. Integral a => a -> Integer
toInteger