{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE Safe #-}
module MonadLib.Derive (
Iso(Iso),
derive_fmap,
derive_pure, derive_apply,
derive_empty, derive_or,
derive_return, derive_bind, derive_fail,
derive_mzero, derive_mplus,
derive_mfix,
derive_ask,
derive_local,
derive_put,
derive_collect,
derive_get,
derive_set,
derive_raise,
derive_try,
derive_callWithCC,
derive_abort,
derive_lift,
derive_inBase,
derive_runM,
) where
import MonadLib
import Control.Applicative
import Control.Monad.Fix
import Prelude hiding (Ordering(..))
import Control.Monad.Fail as MF
data Iso m n = Iso { forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close :: forall a. m a -> n a,
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open :: forall a. n a -> m a }
derive_fmap :: (Functor m) => Iso m n -> (a -> b) -> n a -> n b
derive_fmap :: forall (m :: * -> *) (n :: * -> *) a b.
Functor m =>
Iso m n -> (a -> b) -> n a -> n b
derive_fmap Iso m n
iso a -> b
f n a
m = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso ((a -> b) -> m a -> m b
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso n a
m))
derive_pure :: (Applicative m) => Iso m n -> a -> n a
derive_pure :: forall (m :: * -> *) (n :: * -> *) a.
Applicative m =>
Iso m n -> a -> n a
derive_pure Iso m n
iso a
a = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a)
derive_apply :: (Applicative m) => Iso m n -> n (a -> b) -> (n a -> n b)
derive_apply :: forall (m :: * -> *) (n :: * -> *) a b.
Applicative m =>
Iso m n -> n (a -> b) -> n a -> n b
derive_apply Iso m n
iso n (a -> b)
f n a
x = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso n (a -> b)
f m (a -> b) -> m a -> m b
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso n a
x)
derive_empty :: (Alternative m) => Iso m n -> n a
derive_empty :: forall (m :: * -> *) (n :: * -> *) a.
Alternative m =>
Iso m n -> n a
derive_empty Iso m n
iso = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso m a
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty
derive_or :: (Alternative m) => Iso m n -> n a -> n a -> n a
derive_or :: forall (m :: * -> *) (n :: * -> *) a.
Alternative m =>
Iso m n -> n a -> n a -> n a
derive_or Iso m n
iso n a
a n a
b = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso n a
a m a -> m a -> m a
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso n a
b)
derive_return :: (Monad m) => Iso m n -> (a -> n a)
derive_return :: forall (m :: * -> *) (n :: * -> *) a.
Monad m =>
Iso m n -> a -> n a
derive_return Iso m n
iso a
a = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a)
derive_bind :: (Monad m) => Iso m n -> n a -> (a -> n b) -> n b
derive_bind :: forall (m :: * -> *) (n :: * -> *) a b.
Monad m =>
Iso m n -> n a -> (a -> n b) -> n b
derive_bind Iso m n
iso n a
m a -> n b
k = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso ((Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso n a
m) m a -> (a -> m b) -> m b
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x -> Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso (a -> n b
k a
x))
derive_fail :: (MF.MonadFail m) => Iso m n -> String -> n a
derive_fail :: forall (m :: * -> *) (n :: * -> *) a.
MonadFail m =>
Iso m n -> String -> n a
derive_fail Iso m n
iso String
a = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
MF.fail String
a)
derive_mfix :: (MonadFix m) => Iso m n -> (a -> n a) -> n a
derive_mfix :: forall (m :: * -> *) (n :: * -> *) a.
MonadFix m =>
Iso m n -> (a -> n a) -> n a
derive_mfix Iso m n
iso a -> n a
f = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso ((a -> m a) -> m a
forall a. (a -> m a) -> m a
forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix (Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso (n a -> m a) -> (a -> n a) -> a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> n a
f))
derive_ask :: (ReaderM m i) => Iso m n -> n i
derive_ask :: forall (m :: * -> *) i (n :: * -> *). ReaderM m i => Iso m n -> n i
derive_ask Iso m n
iso = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso m i
forall (m :: * -> *) i. ReaderM m i => m i
ask
derive_put :: (WriterM m i) => Iso m n -> i -> n ()
derive_put :: forall (m :: * -> *) i (n :: * -> *).
WriterM m i =>
Iso m n -> i -> n ()
derive_put Iso m n
iso i
x = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (i -> m ()
forall (m :: * -> *) i. WriterM m i => i -> m ()
put i
x)
derive_get :: (StateM m i) => Iso m n -> n i
derive_get :: forall (m :: * -> *) i (n :: * -> *). StateM m i => Iso m n -> n i
derive_get Iso m n
iso = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso m i
forall (m :: * -> *) i. StateM m i => m i
get
derive_set :: (StateM m i) => Iso m n -> i -> n ()
derive_set :: forall (m :: * -> *) i (n :: * -> *).
StateM m i =>
Iso m n -> i -> n ()
derive_set Iso m n
iso i
x = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (i -> m ()
forall (m :: * -> *) i. StateM m i => i -> m ()
set i
x)
derive_raise :: (ExceptionM m i) => Iso m n -> i -> n a
derive_raise :: forall (m :: * -> *) i (n :: * -> *) a.
ExceptionM m i =>
Iso m n -> i -> n a
derive_raise Iso m n
iso i
x = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (i -> m a
forall a. i -> m a
forall (m :: * -> *) i a. ExceptionM m i => i -> m a
raise i
x)
derive_callWithCC :: (ContM m) => Iso m n -> ((a -> Label n) -> n a) -> n a
derive_callWithCC :: forall (m :: * -> *) (n :: * -> *) a.
ContM m =>
Iso m n -> ((a -> Label n) -> n a) -> n a
derive_callWithCC Iso m n
iso (a -> Label n) -> n a
f = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (m a -> n a) -> m a -> n a
forall a b. (a -> b) -> a -> b
$ ((a -> Label m) -> m a) -> m a
forall a. ((a -> Label m) -> m a) -> m a
forall (m :: * -> *) a. ContM m => ((a -> Label m) -> m a) -> m a
callWithCC (((a -> Label m) -> m a) -> m a) -> ((a -> Label m) -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso (n a -> m a) -> ((a -> Label m) -> n a) -> (a -> Label m) -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Label n) -> n a
f ((a -> Label n) -> n a)
-> ((a -> Label m) -> a -> Label n) -> (a -> Label m) -> n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Label m) -> a -> Label n
forall {p}. (p -> Label m) -> p -> Label n
relab
where relab :: (p -> Label m) -> p -> Label n
relab p -> Label m
k p
a = (forall b. n b) -> Label n
forall (m :: * -> *). (forall b. m b) -> Label m
labelC (Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (m b -> n b) -> m b -> n b
forall a b. (a -> b) -> a -> b
$ Label m -> m b
forall (m :: * -> *) a. Label m -> m a
jump (Label m -> m b) -> Label m -> m b
forall a b. (a -> b) -> a -> b
$ p -> Label m
k p
a)
derive_abort :: (AbortM m i) => Iso m n -> i -> n a
derive_abort :: forall (m :: * -> *) i (n :: * -> *) a.
AbortM m i =>
Iso m n -> i -> n a
derive_abort Iso m n
iso i
i = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (i -> m a
forall a. i -> m a
forall (m :: * -> *) i a. AbortM m i => i -> m a
abort i
i)
derive_local :: (RunReaderM m i) => Iso m n -> i -> n a -> n a
derive_local :: forall (m :: * -> *) i (n :: * -> *) a.
RunReaderM m i =>
Iso m n -> i -> n a -> n a
derive_local Iso m n
iso i
i = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (m a -> n a) -> (n a -> m a) -> n a -> n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> m a -> m a
forall a. i -> m a -> m a
forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
local i
i (m a -> m a) -> (n a -> m a) -> n a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso
derive_collect :: (RunWriterM m i) => Iso m n -> n a -> n (a,i)
derive_collect :: forall (m :: * -> *) i (n :: * -> *) a.
RunWriterM m i =>
Iso m n -> n a -> n (a, i)
derive_collect Iso m n
iso = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (m (a, i) -> n (a, i)) -> (n a -> m (a, i)) -> n a -> n (a, i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> m (a, i)
forall a. m a -> m (a, i)
forall (m :: * -> *) i a. RunWriterM m i => m a -> m (a, i)
collect (m a -> m (a, i)) -> (n a -> m a) -> n a -> m (a, i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso
derive_try :: (RunExceptionM m i) => Iso m n -> n a -> n (Either i a)
derive_try :: forall (m :: * -> *) i (n :: * -> *) a.
RunExceptionM m i =>
Iso m n -> n a -> n (Either i a)
derive_try Iso m n
iso = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (m (Either i a) -> n (Either i a))
-> (n a -> m (Either i a)) -> n a -> n (Either i a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> m (Either i a)
forall a. m a -> m (Either i a)
forall (m :: * -> *) i a.
RunExceptionM m i =>
m a -> m (Either i a)
try (m a -> m (Either i a)) -> (n a -> m a) -> n a -> m (Either i a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso
derive_mzero :: (MonadPlus m) => Iso m n -> n a
derive_mzero :: forall (m :: * -> *) (n :: * -> *) a. MonadPlus m => Iso m n -> n a
derive_mzero Iso m n
iso = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso m a
forall a. m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
derive_mplus :: (MonadPlus m) => Iso m n -> n a -> n a -> n a
derive_mplus :: forall (m :: * -> *) (n :: * -> *) a.
MonadPlus m =>
Iso m n -> n a -> n a -> n a
derive_mplus Iso m n
iso n a
n1 n a
n2 = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (m a -> m a -> m a
forall a. m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso n a
n1) (Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso n a
n2))
derive_lift :: (MonadT t, Monad m) => Iso (t m) n -> m a -> n a
derive_lift :: forall (t :: (* -> *) -> * -> *) (m :: * -> *) (n :: * -> *) a.
(MonadT t, Monad m) =>
Iso (t m) n -> m a -> n a
derive_lift Iso (t m) n
iso m a
m = Iso (t m) n -> forall a. t m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso (t m) n
iso (m a -> t m a
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift m a
m)
derive_inBase :: (BaseM m x) => Iso m n -> x a -> n a
derive_inBase :: forall (m :: * -> *) (x :: * -> *) (n :: * -> *) a.
BaseM m x =>
Iso m n -> x a -> n a
derive_inBase Iso m n
iso x a
m = Iso m n -> forall a. m a -> n a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. m a -> n a
close Iso m n
iso (x a -> m a
forall a. x a -> m a
forall (m :: * -> *) (n :: * -> *) a. BaseM m n => n a -> m a
inBase x a
m)
derive_runM :: (RunM m a r) => Iso m n -> n a -> r
derive_runM :: forall (m :: * -> *) a r (n :: * -> *).
RunM m a r =>
Iso m n -> n a -> r
derive_runM Iso m n
iso n a
m = m a -> r
forall (m :: * -> *) a r. RunM m a r => m a -> r
runM (Iso m n -> forall a. n a -> m a
forall (m :: * -> *) (n :: * -> *). Iso m n -> forall a. n a -> m a
open Iso m n
iso n a
m)