{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE GADTs #-}

-- | Indiscrete category <-> 'Store' comonad
module Control.Comonad.Travel.Store where

import Control.Category.Indiscrete
import Control.Comonad.Store
import Control.Comonad.Travel
import Data.Singletons
import Data.Singletons.Sigma (Sigma (..))

fromStore :: (SingKind k) => Store (Demote k) r -> Travel (Indiscrete @k) r
fromStore :: forall k r. SingKind k => Store (Demote k) r -> Travel Indiscrete r
fromStore Store (Demote k) r
w = case Demote k -> SomeSing k
forall k. SingKind k => Demote k -> SomeSing k
toSing (Store (Demote k) r -> Demote k
forall a. StoreT (Demote k) Identity a -> Demote k
forall s (w :: * -> *) a. ComonadStore s w => w a -> s
pos Store (Demote k) r
w) of
  SomeSing Sing a
sPos -> Sing a
-> (Sigma k (TyCon (Indiscrete a)) -> r) -> Travel Indiscrete r
forall k (cat :: k -> k -> *) r (a :: k).
Sing a -> (Sigma k (TyCon (cat a)) -> r) -> Travel cat r
MkTravel Sing a
sPos \(Sing fst
sPos' :&: TyCon (Indiscrete a) @@ fst
_) -> Demote k -> Store (Demote k) r -> r
forall a. Demote k -> StoreT (Demote k) Identity a -> a
forall s (w :: * -> *) a. ComonadStore s w => s -> w a -> a
peek (Sing fst -> Demote k
forall (a :: k). Sing a -> Demote k
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing fst
sPos') Store (Demote k) r
w

toStore :: (SingKind k) => Travel (Indiscrete @k) r -> Store (Demote k) r
toStore :: forall k r. SingKind k => Travel Indiscrete r -> Store (Demote k) r
toStore (MkTravel Sing a
sp Sigma k (TyCon (Indiscrete a)) -> r
body) =
  let f :: Demote k -> r
f Demote k
v = case Demote k -> SomeSing k
forall k. SingKind k => Demote k -> SomeSing k
toSing Demote k
v of
        SomeSing Sing a
sv -> Sigma k (TyCon (Indiscrete a)) -> r
body (Sing a
sv Sing a
-> (TyCon (Indiscrete a) @@ a) -> Sigma k (TyCon (Indiscrete a))
forall s (a :: s ~> *) (fst :: s).
Sing fst -> (a @@ fst) -> Sigma s a
:&: TyCon (Indiscrete a) @@ a
Indiscrete a a
forall k (a :: k) (b :: k). Indiscrete a b
Indiscrete)
   in (Demote k -> r) -> Demote k -> StoreT (Demote k) Identity r
forall s a. (s -> a) -> s -> Store s a
store Demote k -> r
f (Sing a -> Demote k
forall (a :: k). Sing a -> Demote k
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a
sp)