{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
-- |
-- Module: Language.KURE.Injection
-- Copyright: (c) 2012--2021 The University of Kansas
-- License: BSD3
--
-- Maintainer: Neil Sculthorpe <neil.sculthorpe@ntu.ac.uk>
-- Stability: beta
-- Portability: ghc
--
-- This module provides a type class for injective functions (and their projections),
-- and some useful interactions with 'Transform'.
--
module Language.KURE.Injection
       ( -- * Injection Class
         Injection(..)
       -- * Monad Injections
       , injectM
       , projectM
       , projectWithFailMsgM
       -- * Transformation Injections
       , injectT
       , projectT
       , extractT
       , promoteT
       , projectWithFailMsgT
       , promoteWithFailMsgT
       -- * Rewrite Injections
       , extractR
       , promoteR
       , extractWithFailMsgR
       , promoteWithFailMsgR
) where

import Control.Arrow

#if !MIN_VERSION_base(4,13,0)
import Control.Monad.Fail (MonadFail)
#endif

import Language.KURE.Transform

-------------------------------------------------------------------------------

-- | A class of injective functions from @a@ to @b@, and their projections.
--   The following law is expected to hold:
--
-- > project (inject a) == Just a

class Injection a u where
  inject  :: a -> u
  project :: u -> Maybe a

-- | There is an identity injection for all types.
instance Injection a a where
  inject :: a -> a
  inject :: a -> a
inject = a -> a
forall a. a -> a
id
  {-# INLINE inject #-}

  project :: a -> Maybe a
  project :: a -> Maybe a
project = a -> Maybe a
forall a. a -> Maybe a
Just
  {-# INLINE project #-}

instance Injection a (Maybe a) where
  inject :: a -> Maybe a
  inject :: a -> Maybe a
inject  = a -> Maybe a
forall a. a -> Maybe a
Just
  {-# INLINE inject #-}

  project :: Maybe a -> Maybe a
  project :: Maybe a -> Maybe a
project = Maybe a -> Maybe a
forall a. a -> a
id
  {-# INLINE project #-}

-------------------------------------------------------------------------------

-- | Injects a value and lifts it into a 'Monad'.
injectM :: (Monad m, Injection a u) => a -> m u
injectM :: a -> m u
injectM = u -> m u
forall (m :: * -> *) a. Monad m => a -> m a
return (u -> m u) -> (a -> u) -> a -> m u
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> u
forall a u. Injection a u => a -> u
inject
{-# INLINE injectM #-}

-- | As 'projectM', but takes a custom error message to use if projection fails.
projectWithFailMsgM :: (MonadFail m, Injection a u) => String -> u -> m a
projectWithFailMsgM :: String -> u -> m a
projectWithFailMsgM String
msg = m a -> (a -> m a) -> Maybe a -> m a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
msg) a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m a) -> (u -> Maybe a) -> u -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. u -> Maybe a
forall a u. Injection a u => u -> Maybe a
project
{-# INLINE projectWithFailMsgM #-}

-- | Projects a value and lifts it into a 'Monad', with the possibility of failure.
projectM :: (MonadFail m, Injection a u) => u -> m a
projectM :: u -> m a
projectM = String -> u -> m a
forall (m :: * -> *) a u.
(MonadFail m, Injection a u) =>
String -> u -> m a
projectWithFailMsgM String
"projectM failed"
{-# INLINE projectM #-}

-------------------------------------------------------------------------------

-- | Lifted 'inject'.
injectT :: (Monad m, Injection a u) => Transform c m a u
injectT :: Transform c m a u
injectT = (a -> u) -> Transform c m a u
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr a -> u
forall a u. Injection a u => a -> u
inject
{-# INLINE injectT #-}

projectWithFailMsgT :: (MonadFail m, Injection a u) => String -> Transform c m u a
projectWithFailMsgT :: String -> Transform c m u a
projectWithFailMsgT = (u -> m a) -> Transform c m u a
forall k a (m :: k -> *) (b :: k) c.
(a -> m b) -> Transform c m a b
contextfreeT ((u -> m a) -> Transform c m u a)
-> (String -> u -> m a) -> String -> Transform c m u a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> u -> m a
forall (m :: * -> *) a u.
(MonadFail m, Injection a u) =>
String -> u -> m a
projectWithFailMsgM
{-# INLINE projectWithFailMsgT #-}

-- | Lifted 'project', the transformation fails if the projection fails.
projectT :: (MonadFail m, Injection a u) => Transform c m u a
projectT :: Transform c m u a
projectT = String -> Transform c m u a
forall (m :: * -> *) a u c.
(MonadFail m, Injection a u) =>
String -> Transform c m u a
projectWithFailMsgT String
"projectT failed"
{-# INLINE projectT #-}

-- | Convert a transformation over an injected value into a transformation over a non-injected value.
extractT :: (Monad m, Injection a u) => Transform c m u b -> Transform c m a b
extractT :: Transform c m u b -> Transform c m a b
extractT Transform c m u b
t = Transform c m a u
forall (m :: * -> *) a u c.
(Monad m, Injection a u) =>
Transform c m a u
injectT Transform c m a u -> Transform c m u b -> Transform c m a b
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Transform c m u b
t
{-# INLINE extractT #-}

-- | As 'promoteT', but takes a custom error message to use if promotion fails.
promoteWithFailMsgT  :: (MonadFail m, Injection a u) => String -> Transform c m a b -> Transform c m u b
promoteWithFailMsgT :: String -> Transform c m a b -> Transform c m u b
promoteWithFailMsgT String
msg Transform c m a b
t = String -> Transform c m u a
forall (m :: * -> *) a u c.
(MonadFail m, Injection a u) =>
String -> Transform c m u a
projectWithFailMsgT String
msg Transform c m u a -> Transform c m a b -> Transform c m u b
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Transform c m a b
t
{-# INLINE promoteWithFailMsgT #-}

-- | Promote a transformation over a value into a transformation over an injection of that value,
--   (failing if that injected value cannot be projected).
promoteT  :: (MonadFail m, Injection a u) => Transform c m a b -> Transform c m u b
promoteT :: Transform c m a b -> Transform c m u b
promoteT = String -> Transform c m a b -> Transform c m u b
forall (m :: * -> *) a u c b.
(MonadFail m, Injection a u) =>
String -> Transform c m a b -> Transform c m u b
promoteWithFailMsgT String
"promoteT failed"
{-# INLINE promoteT #-}

-- | As 'extractR', but takes a custom error message to use if extraction fails.
extractWithFailMsgR :: (MonadFail m, Injection a u) => String -> Rewrite c m u -> Rewrite c m a
extractWithFailMsgR :: String -> Rewrite c m u -> Rewrite c m a
extractWithFailMsgR String
msg Rewrite c m u
r = Transform c m a u
forall (m :: * -> *) a u c.
(Monad m, Injection a u) =>
Transform c m a u
injectT Transform c m a u -> Transform c m u a -> Rewrite c m a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Rewrite c m u
r Rewrite c m u -> Transform c m u a -> Transform c m u a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> String -> Transform c m u a
forall (m :: * -> *) a u c.
(MonadFail m, Injection a u) =>
String -> Transform c m u a
projectWithFailMsgT String
msg
{-# INLINE extractWithFailMsgR #-}

-- | Convert a rewrite over an injected value into a rewrite over a projection of that value,
--   (failing if that injected value cannot be projected).
extractR :: (MonadFail m, Injection a u) => Rewrite c m u -> Rewrite c m a
extractR :: Rewrite c m u -> Rewrite c m a
extractR = String -> Rewrite c m u -> Rewrite c m a
forall (m :: * -> *) a u c.
(MonadFail m, Injection a u) =>
String -> Rewrite c m u -> Rewrite c m a
extractWithFailMsgR String
"extractR failed"
{-# INLINE extractR #-}

-- | As 'promoteR', but takes a custom error message to use if promotion fails.
promoteWithFailMsgR :: (MonadFail m, Injection a u) => String -> Rewrite c m a -> Rewrite c m u
promoteWithFailMsgR :: String -> Rewrite c m a -> Rewrite c m u
promoteWithFailMsgR String
msg Rewrite c m a
r = String -> Transform c m u a
forall (m :: * -> *) a u c.
(MonadFail m, Injection a u) =>
String -> Transform c m u a
projectWithFailMsgT String
msg Transform c m u a -> Transform c m a u -> Rewrite c m u
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Rewrite c m a
r Rewrite c m a -> Transform c m a u -> Transform c m a u
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Transform c m a u
forall (m :: * -> *) a u c.
(Monad m, Injection a u) =>
Transform c m a u
injectT
{-# INLINE promoteWithFailMsgR #-}

-- | Promote a rewrite over a value into a rewrite over an injection of that value,
--   (failing if that injected value cannot be projected).
promoteR  :: (MonadFail m, Injection a u) => Rewrite c m a -> Rewrite c m u
promoteR :: Rewrite c m a -> Rewrite c m u
promoteR = String -> Rewrite c m a -> Rewrite c m u
forall (m :: * -> *) a u c.
(MonadFail m, Injection a u) =>
String -> Rewrite c m a -> Rewrite c m u
promoteWithFailMsgR String
"promoteR failed"
{-# INLINE promoteR #-}

-------------------------------------------------------------------------------