module UVMHS.Core.Effects where

import UVMHS.Core.Init
import UVMHS.Core.Classes
import UVMHS.Core.Data

import qualified Prelude as HS

infixl 5 ⊞,⎅

class MonadIO (m ∷ ★ → ★) where io ∷ IO a → m a

class LiftIO t where
  liftIO ∷ ∀ m. (Monad m) ⇒ (∀ a. IO a → m a) → (∀ a. IO a → t m a)

class MonadReader r m | m → r where
  askL ∷ r ⟢ r' → m r'
  localL ∷ ∀ a r'. r ⟢ r' → r' → m a → m a

class LiftReader t where
  liftAskL ∷ ∀ m r. (Monad m) ⇒ (∀ r'. r ⟢ r' → m r') → (∀ r'. r ⟢ r' → t m r')
  liftLocalL ∷ ∀ m r. (Monad m) ⇒ (∀ r' a. r ⟢ r' → r' → m a → m a) → (∀ r' a. r ⟢ r' → r' → t m a → t m a)

class MonadWriter o m | m → o where
  tell ∷ o → m ()
  hijack ∷ ∀ a. m a → m (o ∧ a)

class LiftWriter t where
  liftTell ∷ ∀ m o. (Monad m) ⇒ (o → m ()) → (o → t m ())
  liftHijack ∷ ∀ m o. (Monad m) ⇒ (∀ a. m a → m (o ∧ a)) → (∀ a. t m a → t m (o ∧ a))

class MonadState s m | m → s where
  get ∷ m s
  put ∷ s → m ()

class LiftState t where
  liftGet ∷ ∀ m s. (Monad m) ⇒ m s → t m s
  liftPut ∷ ∀ m s. (Monad m) ⇒ (s → m ()) → (s → t m ())

class MonadFail m where
  abort ∷ ∀ a. m a
  (⎅) ∷ ∀ a. m a → m a → m a

class LiftFail t where
  liftAbort ∷ ∀ m. (Monad m) ⇒ (∀ a. m a) → (∀ a. t m a)
  liftTry ∷ ∀ m. (Monad m) ⇒ (∀ a. m a → m a → m a) → (∀ a. t m a → t m a → t m a)

class MonadError e m | m → e where
  throw ∷ ∀ a. e → m a
  catch ∷ ∀ a. m a → (e → m a) → m a

class LiftError t where
  liftThrow ∷ ∀ m e. (Monad m) ⇒ (∀ a. e → m a) → (∀ a. e → t m a)
  liftCatch ∷ ∀ m e. (Monad m) ⇒ (∀ a. m a → (e → m a) → m a) → (∀ a. t m a → (e → t m a) → t m a)

class MonadDelay m where
  delay ∷ (() → m a) → m a

class LiftDelay t where
  liftDelay ∷ ∀ m. (Monad m) ⇒ (∀ a. (() → m a) → m a) → (∀ a. (() → t m a) → t m a)

class MonadNondet m where
  mzero ∷ ∀ a. m a
  (⊞) ∷ ∀ a. m a → m a → m a

class LiftNondet t where
  liftMzero ∷ ∀ m. (Monad m) ⇒ (∀ a. m a) → (∀ a. t m a)
  liftMplus ∷ ∀ m. (Monad m) ⇒ (∀ a. m a → m a → m a) → (∀ a. t m a → t m a → t m a)

class MonadTop m where
  mtop ∷ ∀ a. m a

class LiftTop t where
  liftMtop ∷ ∀ m. (Monad m) ⇒ (∀ a. m a) → (∀ a. t m a)

class MonadCont r m | m → r where
  callCC ∷ ∀ a. ((a → m r) → m r) → m a 
  withC ∷ ∀ a. (a → m r) → m a → m r 

class LiftCont t where
  liftCallCC ∷ 
    ∀ m r. (Monad m) 
    ⇒ (∀ a. ((a → m r) → m r) → m a) 
    → (∀ a. ((a → t m r) → t m r) → t m a)
  liftWithC ∷ 
    ∀ m r. (Monad m) 
    ⇒ (∀ a. (a → m r) → m a → m r) 
    → (∀ a. (a → t m r) → t m a → t m r)

class MonadUCont m where
  ucallCC ∷ ∀ a. (∀ u. (a → m u) → m u) → m a 
  uwithC ∷ ∀ a u. (a → m u) → m a → m u 

class LiftUCont t where
  liftUCallCC ∷ 
    ∀ m. (Monad m) 
    ⇒ (∀ a. (∀ u. (a → m u) → m u) → m a) 
    → (∀ a. (∀ u. (a → t m u) → t m u) → t m a)
  liftUWithC ∷ 
    ∀ m. (Monad m) 
    ⇒ (∀ a u. (a → m u) → m a → m u) 
    → (∀ a u. (a → t m u) → t m a → t m u)

class MonadBad m where
  bad ∷ ∀ a. m a

------------------------
-- STANDARD INSTANCES --
------------------------

instance MonadReader r ((→) r) where
  askL ∷ r ⟢ r' → r → r'
  askL :: forall r'. (r ⟢ r') -> r -> r'
askL = (r ⟢ r') -> r -> r'
forall r r'. (r ⟢ r') -> r -> r'
access

  localL ∷ ∀ a r'. r ⟢ r' → r' → (r → a) → (r → a)
  localL :: forall a r'. (r ⟢ r') -> r' -> (r -> a) -> r -> a
localL r ⟢ r'
ℓ r'
r' r -> a
f = r -> a
f (r -> a) -> (r -> r) -> r -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (r ⟢ r') -> r' -> r -> r
forall (t :: * -> * -> *) a b. Alter t => t a b -> b -> a -> a
update r ⟢ r'
ℓ r'
r'

instance (Null o) ⇒ MonadWriter o ((∧) o) where
  tell ∷ o → (o ∧ ())
  tell :: o -> o ∧ ()
tell o
o = (o
o o -> () -> o ∧ ()
forall a b. a -> b -> a ∧ b
:* ())

  hijack ∷ ∀ a. o ∧ a → o ∧ (o ∧ a)
  hijack :: forall a. (o ∧ a) -> o ∧ (o ∧ a)
hijack o ∧ a
ox = o
forall a. Null a => a
null o -> (o ∧ a) -> o ∧ (o ∧ a)
forall a b. a -> b -> a ∧ b
:* o ∧ a
ox

instance MonadFail 𝑂 where
  abort ∷ ∀ a. 𝑂 a
  abort :: forall a. 𝑂 a
abort = 𝑂 a
forall a. 𝑂 a
None

  (⎅) ∷ ∀ a. 𝑂 a → 𝑂 a → 𝑂 a
  𝑂 a
None ⎅ :: forall a. 𝑂 a -> 𝑂 a -> 𝑂 a
⎅ 𝑂 a
xM = 𝑂 a
xM
  Some a
x ⎅ 𝑂 a
_ = a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x

instance MonadError e ((∨) e) where
  throw ∷ ∀ a. e → e ∨ a
  throw :: forall a. e -> e ∨ a
throw = e -> e ∨ a
forall e a. e -> e ∨ a
Inl

  catch ∷ ∀ a. e ∨ a → (e → e ∨ a) → e ∨ a
  catch :: forall a. (e ∨ a) -> (e -> e ∨ a) -> e ∨ a
catch (Inl e
e) e -> e ∨ a
k = e -> e ∨ a
k e
e
  catch (Inr a
x) e -> e ∨ a
_ = a -> e ∨ a
forall a b. b -> a ∨ b
Inr a
x

instance MonadNondet 𝐼 where
  mzero ∷ ∀ a. 𝐼 a
  mzero :: forall a. 𝐼 a
mzero = 𝐼 a
forall a. Null a => a
null

  (⊞) ∷ ∀ a. 𝐼 a → 𝐼 a → 𝐼 a
  ⊞ :: forall a. 𝐼 a -> 𝐼 a -> 𝐼 a
(⊞) = 𝐼 a -> 𝐼 a -> 𝐼 a
forall a. Append a => a -> a -> a
(⧺)

instance MonadNondet 𝐿 where
  mzero ∷ ∀ a. 𝐿 a
  mzero :: forall a. 𝐿 a
mzero = 𝐿 a
forall a. Null a => a
null

  (⊞) ∷ ∀ a. 𝐿 a → 𝐿 a → 𝐿 a
  ⊞ :: forall a. 𝐿 a -> 𝐿 a -> 𝐿 a
(⊞) = 𝐿 a -> 𝐿 a -> 𝐿 a
forall a. Append a => a -> a -> a
(⧺)

instance MonadNondet 𝑄 where
  mzero ∷ ∀ a. 𝑄 a
  mzero :: forall a. 𝑄 a
mzero = 𝑄 a
forall a. Null a => a
null

  (⊞) ∷ ∀ a. 𝑄 a → 𝑄 a → 𝑄 a
  ⊞ :: forall a. 𝑄 a -> 𝑄 a -> 𝑄 a
(⊞) = 𝑄 a -> 𝑄 a -> 𝑄 a
forall a. Append a => a -> a -> a
(⧺)

----------------
-- OPERATIONS --
----------------

-- Reader

mapEnvL ∷ (Monad m,MonadReader r₁ m) ⇒ (r₁ ⟢ r₂) → (r₂ → r₂) → m a → m a
mapEnvL :: forall (m :: * -> *) r₁ r₂ a.
(Monad m, MonadReader r₁ m) =>
(r₁ ⟢ r₂) -> (r₂ -> r₂) -> m a -> m a
mapEnvL r₁ ⟢ r₂
ℓ r₂ -> r₂
f m a
xM = do
  r₂
r ← (r₁ ⟢ r₂) -> m r₂
forall r'. (r₁ ⟢ r') -> m r'
forall r (m :: * -> *) r'. MonadReader r m => (r ⟢ r') -> m r'
askL r₁ ⟢ r₂
ℓ
  (r₁ ⟢ r₂) -> r₂ -> m a -> m a
forall a r'. (r₁ ⟢ r') -> r' -> m a -> m a
forall r (m :: * -> *) a r'.
MonadReader r m =>
(r ⟢ r') -> r' -> m a -> m a
localL r₁ ⟢ r₂
ℓ (r₂ -> r₂
f r₂
r) m a
xM

ask ∷ (Monad m,MonadReader r m) ⇒ m r
ask :: forall (m :: * -> *) r. (Monad m, MonadReader r m) => m r
ask = (r ⟢ r) -> m r
forall r'. (r ⟢ r') -> m r'
forall r (m :: * -> *) r'. MonadReader r m => (r ⟢ r') -> m r'
askL r ⟢ r
forall a. a ⟢ a
forall {k} (t :: k -> k -> *) (a :: k). Reflexive t => t a a
refl

local ∷ (Monad m,MonadReader r m) ⇒ r → m a → m a
local :: forall (m :: * -> *) r a.
(Monad m, MonadReader r m) =>
r -> m a -> m a
local = (r ⟢ r) -> r -> m a -> m a
forall a r'. (r ⟢ r') -> r' -> m a -> m a
forall r (m :: * -> *) a r'.
MonadReader r m =>
(r ⟢ r') -> r' -> m a -> m a
localL r ⟢ r
forall a. a ⟢ a
forall {k} (t :: k -> k -> *) (a :: k). Reflexive t => t a a
refl

mapEnv ∷ (Monad m,MonadReader r m) ⇒ (r → r) → m a → m a 
mapEnv :: forall (m :: * -> *) r a.
(Monad m, MonadReader r m) =>
(r -> r) -> m a -> m a
mapEnv = (r ⟢ r) -> (r -> r) -> m a -> m a
forall (m :: * -> *) r₁ r₂ a.
(Monad m, MonadReader r₁ m) =>
(r₁ ⟢ r₂) -> (r₂ -> r₂) -> m a -> m a
mapEnvL r ⟢ r
forall a. a ⟢ a
forall {k} (t :: k -> k -> *) (a :: k). Reflexive t => t a a
refl

-- Writer

tellL ∷ (Monoid o₁,Monad m,MonadWriter o₁ m) ⇒ o₁ ⟢ o₂ → o₂ → m ()
tellL :: forall o₁ (m :: * -> *) o₂.
(Monoid o₁, Monad m, MonadWriter o₁ m) =>
(o₁ ⟢ o₂) -> o₂ -> m ()
tellL o₁ ⟢ o₂
l o₂
o = o₁ -> m ()
forall o (m :: * -> *). MonadWriter o m => o -> m ()
tell (o₁ -> m ()) -> o₁ -> m ()
forall a b. (a -> b) -> a -> b
$ (o₁ ⟢ o₂) -> o₂ -> o₁ -> o₁
forall (t :: * -> * -> *) a b. Alter t => t a b -> b -> a -> a
update o₁ ⟢ o₂
l o₂
o o₁
forall a. Null a => a
null

hijackL ∷ (Monad m,MonadWriter o₁ m,Null o₂) ⇒ o₁ ⟢ o₂ → m a → m (o₂ ∧ a)
hijackL :: forall (m :: * -> *) o₁ o₂ a.
(Monad m, MonadWriter o₁ m, Null o₂) =>
(o₁ ⟢ o₂) -> m a -> m (o₂ ∧ a)
hijackL o₁ ⟢ o₂
ℓ m a
xM = do
  o₁
o₁ :* a
a ← m a -> m (o₁ ∧ a)
forall a. m a -> m (o₁ ∧ a)
forall o (m :: * -> *) a. MonadWriter o m => m a -> m (o ∧ a)
hijack m a
xM
  o₁ -> m ()
forall o (m :: * -> *). MonadWriter o m => o -> m ()
tell (o₁ -> m ()) -> o₁ -> m ()
forall a b. (a -> b) -> a -> b
$ (o₁ ⟢ o₂) -> o₂ -> o₁ -> o₁
forall (t :: * -> * -> *) a b. Alter t => t a b -> b -> a -> a
update o₁ ⟢ o₂
ℓ o₂
forall a. Null a => a
null o₁
o₁
  (o₂ ∧ a) -> m (o₂ ∧ a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ((o₂ ∧ a) -> m (o₂ ∧ a)) -> (o₂ ∧ a) -> m (o₂ ∧ a)
forall a b. (a -> b) -> a -> b
$ (o₁ ⟢ o₂) -> o₁ -> o₂
forall r r'. (r ⟢ r') -> r -> r'
access o₁ ⟢ o₂
ℓ o₁
o₁ o₂ -> a -> o₂ ∧ a
forall a b. a -> b -> a ∧ b
:* a
a

mapOut ∷ (Monad m,MonadWriter o m) ⇒ (o → o) → m a → m a
mapOut :: forall (m :: * -> *) o a.
(Monad m, MonadWriter o m) =>
(o -> o) -> m a -> m a
mapOut o -> o
f m a
aM = do
  (o
o :* a
a) ← m a -> m (o ∧ a)
forall a. m a -> m (o ∧ a)
forall o (m :: * -> *) a. MonadWriter o m => m a -> m (o ∧ a)
hijack m a
aM
  o -> m ()
forall o (m :: * -> *). MonadWriter o m => o -> m ()
tell (o -> m ()) -> o -> m ()
forall a b. (a -> b) -> a -> b
$ o -> o
f o
o
  a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return a
a

retOut ∷ ∀ o m a. (Monad m,MonadWriter o m) ⇒ m a → m o
retOut :: forall o (m :: * -> *) a. (Monad m, MonadWriter o m) => m a -> m o
retOut m a
xM = do
  (o
o :* a
_) ← m a -> m (o ∧ a)
forall a. m a -> m (o ∧ a)
forall o (m :: * -> *) a. MonadWriter o m => m a -> m (o ∧ a)
hijack m a
xM
  o -> m o
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return o
o

-- # State

getL ∷ (Monad m,MonadState s m) ⇒ s ⟢ a → m a 
getL :: forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
(s ⟢ a) -> m a
getL s ⟢ a
l = (s -> a) -> m s -> m a
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((s ⟢ a) -> s -> a
forall r r'. (r ⟢ r') -> r -> r'
access s ⟢ a
l) m s
forall s (m :: * -> *). MonadState s m => m s
get

putL ∷ (Monad m,MonadState s m) ⇒ s ⟢ a → a → m () 
putL :: forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
(s ⟢ a) -> a -> m ()
putL s ⟢ a
𝓁 = (s -> s) -> m ()
forall (m :: * -> *) s.
(Monad m, MonadState s m) =>
(s -> s) -> m ()
modify ((s -> s) -> m ()) -> (a -> s -> s) -> a -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (s ⟢ a) -> a -> s -> s
forall (t :: * -> * -> *) a b. Alter t => t a b -> b -> a -> a
update s ⟢ a
𝓁

modify ∷ (Monad m,MonadState s m) ⇒ (s → s) → m () 
modify :: forall (m :: * -> *) s.
(Monad m, MonadState s m) =>
(s -> s) -> m ()
modify s -> s
f = do
  s
s ← m s
forall s (m :: * -> *). MonadState s m => m s
get
  s -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (s -> m ()) -> s -> m ()
forall a b. (a -> b) -> a -> b
$ s -> s
f s
s

modifyM ∷ (Monad m,MonadState s m) ⇒ (s → m s) → m () 
modifyM :: forall (m :: * -> *) s.
(Monad m, MonadState s m) =>
(s -> m s) -> m ()
modifyM s -> m s
f = do
  s
s ← m s
forall s (m :: * -> *). MonadState s m => m s
get
  s -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (s -> m ()) -> m s -> m ()
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ s -> m s
f s
s

modifyL ∷ (Monad m,MonadState s m) ⇒ s ⟢ a → (a → a) → m () 
modifyL :: forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
(s ⟢ a) -> (a -> a) -> m ()
modifyL s ⟢ a
𝓁 = (s -> s) -> m ()
forall (m :: * -> *) s.
(Monad m, MonadState s m) =>
(s -> s) -> m ()
modify ((s -> s) -> m ()) -> ((a -> a) -> s -> s) -> (a -> a) -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (s ⟢ a) -> (a -> a) -> s -> s
forall a b. (a ⟢ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter s ⟢ a
𝓁

modifyML ∷ (Monad m,MonadState s m) ⇒ s ⟢ a → (a → m a) → m () 
modifyML :: forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
(s ⟢ a) -> (a -> m a) -> m ()
modifyML s ⟢ a
𝓁 = (s -> m s) -> m ()
forall (m :: * -> *) s.
(Monad m, MonadState s m) =>
(s -> m s) -> m ()
modifyM ((s -> m s) -> m ())
-> ((a -> m a) -> s -> m s) -> (a -> m a) -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (s ⟢ a) -> (a -> m a) -> s -> m s
forall (m :: * -> *) a b.
Monad m =>
(a ⟢ b) -> (b -> m b) -> a -> m a
forall (t :: * -> * -> *) (m :: * -> *) a b.
(AlterM t, Monad m) =>
t a b -> (b -> m b) -> a -> m a
alterM s ⟢ a
𝓁

getput ∷ (Monad m,MonadState s m) ⇒ s → m s
getput :: forall (m :: * -> *) s. (Monad m, MonadState s m) => s -> m s
getput s
s = do
  s
s' ← m s
forall s (m :: * -> *). MonadState s m => m s
get
  s -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put s
s
  s -> m s
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return s
s'

getputL ∷ (Monad m,MonadState s₁ m) ⇒ s₁ ⟢ s₂ → s₂ → m s₂
getputL :: forall (m :: * -> *) s₁ s₂.
(Monad m, MonadState s₁ m) =>
(s₁ ⟢ s₂) -> s₂ -> m s₂
getputL s₁ ⟢ s₂
𝓁 s₂
x = do
  s₂
x' ← (s₁ ⟢ s₂) -> m s₂
forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
(s ⟢ a) -> m a
getL s₁ ⟢ s₂
𝓁
  (s₁ ⟢ s₂) -> s₂ -> m ()
forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
(s ⟢ a) -> a -> m ()
putL s₁ ⟢ s₂
𝓁 s₂
x
  s₂ -> m s₂
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return s₂
x'

next ∷ (Monad m,MonadState s m,Multiplicative s) ⇒ m s
next :: forall (m :: * -> *) s.
(Monad m, MonadState s m, Multiplicative s) =>
m s
next = do
  s
i ← m s
forall s (m :: * -> *). MonadState s m => m s
get
  s -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (s -> m ()) -> s -> m ()
forall a b. (a -> b) -> a -> b
$ s -> s
forall a. (One a, Plus a) => a -> a
succ s
i
  s -> m s
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return s
i

nextL ∷ (Monad m,MonadState s m,Multiplicative a) ⇒ s ⟢ a → m a
nextL :: forall (m :: * -> *) s a.
(Monad m, MonadState s m, Multiplicative a) =>
(s ⟢ a) -> m a
nextL s ⟢ a
l = do
  a
i ← (s ⟢ a) -> m a
forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
(s ⟢ a) -> m a
getL s ⟢ a
l
  (s ⟢ a) -> a -> m ()
forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
(s ⟢ a) -> a -> m ()
putL s ⟢ a
l (a -> m ()) -> a -> m ()
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. (One a, Plus a) => a -> a
succ a
i
  a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return a
i

bump ∷ (Monad m,MonadState s m,Multiplicative s) ⇒ m ()
bump :: forall (m :: * -> *) s.
(Monad m, MonadState s m, Multiplicative s) =>
m ()
bump = (s -> s) -> m ()
forall (m :: * -> *) s.
(Monad m, MonadState s m) =>
(s -> s) -> m ()
modify s -> s
forall a. (One a, Plus a) => a -> a
succ

bumpL ∷ (Monad m,MonadState s m,Multiplicative a) ⇒ s ⟢ a → m ()
bumpL :: forall (m :: * -> *) s a.
(Monad m, MonadState s m, Multiplicative a) =>
(s ⟢ a) -> m ()
bumpL s ⟢ a
l = (s ⟢ a) -> (a -> a) -> m ()
forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
(s ⟢ a) -> (a -> a) -> m ()
modifyL s ⟢ a
l a -> a
forall a. (One a, Plus a) => a -> a
succ

localize ∷ (Monad m,MonadState s m) ⇒ s → m a → m (s ∧ a)
localize :: forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
s -> m a -> m (s ∧ a)
localize s
s m a
xM = do
  s
s' ← s -> m s
forall (m :: * -> *) s. (Monad m, MonadState s m) => s -> m s
getput s
s
  a
x ← m a
xM
  s
s'' ← s -> m s
forall (m :: * -> *) s. (Monad m, MonadState s m) => s -> m s
getput s
s'
  (s ∧ a) -> m (s ∧ a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (s
s'' s -> a -> s ∧ a
forall a b. a -> b -> a ∧ b
:* a
x)

localizeL ∷ (Monad m,MonadState s₁ m) ⇒ s₁ ⟢ s₂ → s₂ → m a → m (s₂ ∧ a)
localizeL :: forall (m :: * -> *) s₁ s₂ a.
(Monad m, MonadState s₁ m) =>
(s₁ ⟢ s₂) -> s₂ -> m a -> m (s₂ ∧ a)
localizeL s₁ ⟢ s₂
𝓁 s₂
s₂ m a
aM = do
  s₂
s₂' ← (s₁ ⟢ s₂) -> s₂ -> m s₂
forall (m :: * -> *) s₁ s₂.
(Monad m, MonadState s₁ m) =>
(s₁ ⟢ s₂) -> s₂ -> m s₂
getputL s₁ ⟢ s₂
𝓁 s₂
s₂
  a
x ← m a
aM
  s₂
s₂'' ← (s₁ ⟢ s₂) -> s₂ -> m s₂
forall (m :: * -> *) s₁ s₂.
(Monad m, MonadState s₁ m) =>
(s₁ ⟢ s₂) -> s₂ -> m s₂
getputL s₁ ⟢ s₂
𝓁 s₂
s₂'
  (s₂ ∧ a) -> m (s₂ ∧ a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (s₂
s₂'' s₂ -> a -> s₂ ∧ a
forall a b. a -> b -> a ∧ b
:* a
x)

localState ∷ (Monad m,MonadState s m) ⇒ s → m a → m a
localState :: forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
s -> m a -> m a
localState s
s = ((s ∧ a) -> a) -> m (s ∧ a) -> m a
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (s ∧ a) -> a
forall a b. (a ∧ b) -> b
snd (m (s ∧ a) -> m a) -> (m a -> m (s ∧ a)) -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ s -> m a -> m (s ∧ a)
forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
s -> m a -> m (s ∧ a)
localize s
s

localStateL ∷ (Monad m,MonadState s₁ m) ⇒ s₁ ⟢ s₂ → s₂ → m a → m a
localStateL :: forall (m :: * -> *) s₁ s₂ a.
(Monad m, MonadState s₁ m) =>
(s₁ ⟢ s₂) -> s₂ -> m a -> m a
localStateL s₁ ⟢ s₂
𝓁 s₂
s = ((s₂ ∧ a) -> a) -> m (s₂ ∧ a) -> m a
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (s₂ ∧ a) -> a
forall a b. (a ∧ b) -> b
snd (m (s₂ ∧ a) -> m a) -> (m a -> m (s₂ ∧ a)) -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (s₁ ⟢ s₂) -> s₂ -> m a -> m (s₂ ∧ a)
forall (m :: * -> *) s₁ s₂ a.
(Monad m, MonadState s₁ m) =>
(s₁ ⟢ s₂) -> s₂ -> m a -> m (s₂ ∧ a)
localizeL s₁ ⟢ s₂
𝓁 s₂
s

retState ∷ (Monad m,MonadState s m) ⇒ m a → m s
retState :: forall (m :: * -> *) s a. (Monad m, MonadState s m) => m a -> m s
retState m a
xM = do
  a
_ ← m a
xM
  m s
forall s (m :: * -> *). MonadState s m => m s
get

retStateOut ∷ (Monad m,MonadState s m,MonadWriter o m) ⇒ m a → m (s ∧ o)
retStateOut :: forall (m :: * -> *) s o a.
(Monad m, MonadState s m, MonadWriter o m) =>
m a -> m (s ∧ o)
retStateOut m a
xM = do
  o
o :* a
_ ← m a -> m (o ∧ a)
forall a. m a -> m (o ∧ a)
forall o (m :: * -> *) a. MonadWriter o m => m a -> m (o ∧ a)
hijack m a
xM
  s
s ← m s
forall s (m :: * -> *). MonadState s m => m s
get
  (s ∧ o) -> m (s ∧ o)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ((s ∧ o) -> m (s ∧ o)) -> (s ∧ o) -> m (s ∧ o)
forall a b. (a -> b) -> a -> b
$ s
s s -> o -> s ∧ o
forall a b. a -> b -> a ∧ b
:* o
o

tellStateL ∷ (Monad m,MonadState o₁ m,Append o₂) ⇒ o₁ ⟢ o₂ → o₂ → m ()
tellStateL :: forall (m :: * -> *) o₁ o₂.
(Monad m, MonadState o₁ m, Append o₂) =>
(o₁ ⟢ o₂) -> o₂ -> m ()
tellStateL o₁ ⟢ o₂
𝓁 o₂
o = (o₁ ⟢ o₂) -> (o₂ -> o₂) -> m ()
forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
(s ⟢ a) -> (a -> a) -> m ()
modifyL o₁ ⟢ o₂
𝓁 ((o₂ -> o₂) -> m ()) -> (o₂ -> o₂) -> m ()
forall a b. (a -> b) -> a -> b
$ o₂ -> o₂ -> o₂
forall a. Append a => a -> a -> a
(⧺) o₂
o

hijackStateL ∷ (Monad m,MonadState o₁ m,Null o₂) ⇒ o₁ ⟢ o₂ → m a → m (o₂ ∧ a)
hijackStateL :: forall (m :: * -> *) o₁ o₂ a.
(Monad m, MonadState o₁ m, Null o₂) =>
(o₁ ⟢ o₂) -> m a -> m (o₂ ∧ a)
hijackStateL o₁ ⟢ o₂
𝓁 m a
aM = (o₁ ⟢ o₂) -> o₂ -> m a -> m (o₂ ∧ a)
forall (m :: * -> *) s₁ s₂ a.
(Monad m, MonadState s₁ m) =>
(s₁ ⟢ s₂) -> s₂ -> m a -> m (s₂ ∧ a)
localizeL o₁ ⟢ o₂
𝓁 o₂
forall a. Null a => a
null m a
aM

localMapStateL ∷ (Monad m,MonadState s₁ m) ⇒ s₁ ⟢ s₂ → (s₂ → s₂) → m a → m a
localMapStateL :: forall (m :: * -> *) s₁ s₂ a.
(Monad m, MonadState s₁ m) =>
(s₁ ⟢ s₂) -> (s₂ -> s₂) -> m a -> m a
localMapStateL s₁ ⟢ s₂
ℓ s₂ -> s₂
f m a
xM = do
  s₂
s ← (s₁ ⟢ s₂) -> m s₂
forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
(s ⟢ a) -> m a
getL s₁ ⟢ s₂
ℓ
  (s₂ ∧ a) -> a
forall a b. (a ∧ b) -> b
snd ((s₂ ∧ a) -> a) -> m (s₂ ∧ a) -> m a
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (s₁ ⟢ s₂) -> s₂ -> m a -> m (s₂ ∧ a)
forall (m :: * -> *) s₁ s₂ a.
(Monad m, MonadState s₁ m) =>
(s₁ ⟢ s₂) -> s₂ -> m a -> m (s₂ ∧ a)
localizeL s₁ ⟢ s₂
ℓ (s₂ -> s₂
f s₂
s) m a
xM

localStateEffectsL ∷ (Monad m,MonadState s₁ m) ⇒ s₁ ⟢ s₂ → m a → m a
localStateEffectsL :: forall (m :: * -> *) s₁ s₂ a.
(Monad m, MonadState s₁ m) =>
(s₁ ⟢ s₂) -> m a -> m a
localStateEffectsL s₁ ⟢ s₂
ℓ m a
xM = do
  s₂
s ← (s₁ ⟢ s₂) -> m s₂
forall (m :: * -> *) s a.
(Monad m, MonadState s m) =>
(s ⟢ a) -> m a
getL s₁ ⟢ s₂
ℓ
  (s₁ ⟢ s₂) -> s₂ -> m a -> m a
forall (m :: * -> *) s₁ s₂ a.
(Monad m, MonadState s₁ m) =>
(s₁ ⟢ s₂) -> s₂ -> m a -> m a
localStateL s₁ ⟢ s₂
ℓ s₂
s m a
xM

-- Fail

failEff ∷ (Monad m,MonadFail m) ⇒ 𝑂 a → m a
failEff :: forall (m :: * -> *) a. (Monad m, MonadFail m) => 𝑂 a -> m a
failEff = (() -> m a) -> (a -> m a) -> 𝑂 a -> m a
forall b a. (() -> b) -> (a -> b) -> 𝑂 a -> b
elim𝑂 (m a -> () -> m a
forall a b. a -> b -> a
const m a
forall a. m a
forall {k} (m :: k -> *) (a :: k). MonadFail m => m a
abort) a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return

failObs ∷ (Monad m,MonadFail m) ⇒ m a → m (𝑂 a)
failObs :: forall (m :: * -> *) a. (Monad m, MonadFail m) => m a -> m (𝑂 a)
failObs m a
xM = [m (𝑂 a)] -> m (𝑂 a)
forall (m :: * -> *) a t.
(Monad m, MonadFail m, ToIter (m a) t) =>
t -> m a
tries
  [ a -> 𝑂 a
forall a. a -> 𝑂 a
Some (a -> 𝑂 a) -> m a -> m (𝑂 a)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ m a
xM
  , 𝑂 a -> m (𝑂 a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return 𝑂 a
forall a. 𝑂 a
None
  ]

abort𝑂 ∷ (Monad m,MonadFail m) ⇒ 𝑂 a → m a
abort𝑂 :: forall (m :: * -> *) a. (Monad m, MonadFail m) => 𝑂 a -> m a
abort𝑂 = (() -> m a) -> (a -> m a) -> 𝑂 a -> m a
forall b a. (() -> b) -> (a -> b) -> 𝑂 a -> b
elim𝑂 (m a -> () -> m a
forall a b. a -> b -> a
const m a
forall a. m a
forall {k} (m :: k -> *) (a :: k). MonadFail m => m a
abort) a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return

tries ∷ (Monad m,MonadFail m,ToIter (m a) t) ⇒ t → m a
tries :: forall (m :: * -> *) a t.
(Monad m, MonadFail m, ToIter (m a) t) =>
t -> m a
tries = m a -> (m a -> m a -> m a) -> t -> m a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr m a
forall a. m a
forall {k} (m :: k -> *) (a :: k). MonadFail m => m a
abort m a -> m a -> m a
forall a. m a -> m a -> m a
forall {k} (m :: k -> *) (a :: k). MonadFail m => m a -> m a -> m a
(⎅)

guard ∷ (Monad m,MonadFail m) ⇒ 𝔹 → m ()
guard :: forall (m :: * -> *). (Monad m, MonadFail m) => 𝔹 -> m ()
guard = \case
  𝔹
True → () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ()
  𝔹
False → m ()
forall a. m a
forall {k} (m :: k -> *) (a :: k). MonadFail m => m a
abort

oneOrMoreSplit ∷ (Monad m,MonadFail m) ⇒ m a → m (a ∧ 𝐿 a)
oneOrMoreSplit :: forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
m a -> m (a ∧ 𝐿 a)
oneOrMoreSplit m a
aM = do
  a
x ← m a
aM
  𝐿 a
xs ← m a -> m (𝐿 a)
forall (m :: * -> *) a. (Monad m, MonadFail m) => m a -> m (𝐿 a)
many m a
aM
  (a ∧ 𝐿 a) -> m (a ∧ 𝐿 a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ((a ∧ 𝐿 a) -> m (a ∧ 𝐿 a)) -> (a ∧ 𝐿 a) -> m (a ∧ 𝐿 a)
forall a b. (a -> b) -> a -> b
$ a
x a -> 𝐿 a -> a ∧ 𝐿 a
forall a b. a -> b -> a ∧ b
:* 𝐿 a
xs

oneOrMore ∷ (Monad m,MonadFail m) ⇒ m a → m (𝐿 a)
oneOrMore :: forall (m :: * -> *) a. (Monad m, MonadFail m) => m a -> m (𝐿 a)
oneOrMore m a
xM = do
  (a
x :* 𝐿 a
xs) ← m a -> m (a ∧ 𝐿 a)
forall (m :: * -> *) a.
(Monad m, MonadFail m) =>
m a -> m (a ∧ 𝐿 a)
oneOrMoreSplit m a
xM
  𝐿 a -> m (𝐿 a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐿 a -> m (𝐿 a)) -> 𝐿 a -> m (𝐿 a)
forall a b. (a -> b) -> a -> b
$ a
x a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 a
xs

many ∷ (Monad m,MonadFail m) ⇒ m a → m (𝐿 a)
many :: forall (m :: * -> *) a. (Monad m, MonadFail m) => m a -> m (𝐿 a)
many m a
aM = [m (𝐿 a)] -> m (𝐿 a)
forall (m :: * -> *) a t.
(Monad m, MonadFail m, ToIter (m a) t) =>
t -> m a
tries
  [ m a -> m (𝐿 a)
forall (m :: * -> *) a. (Monad m, MonadFail m) => m a -> m (𝐿 a)
oneOrMore m a
aM
  , 𝐿 a -> m (𝐿 a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return 𝐿 a
forall a. Null a => a
null
  ]

-- Error --

throwEff ∷ (Monad m,MonadError e m) ⇒ m (e ∨ a) → m a
throwEff :: forall (m :: * -> *) e a.
(Monad m, MonadError e m) =>
m (e ∨ a) -> m a
throwEff = ((e ∨ a) -> m a) -> m (e ∨ a) -> m a
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
extend (((e ∨ a) -> m a) -> m (e ∨ a) -> m a)
-> ((e ∨ a) -> m a) -> m (e ∨ a) -> m a
forall a b. (a -> b) -> a -> b
$ (e -> m a) -> (a -> m a) -> (e ∨ a) -> m a
forall a c b. (a -> c) -> (b -> c) -> (a ∨ b) -> c
elimChoice e -> m a
forall a. e -> m a
forall {k} e (m :: k -> *) (a :: k). MonadError e m => e -> m a
throw a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return

throwObs ∷ (Monad m,MonadError e m) ⇒ m a → m (e ∨ a)
throwObs :: forall (m :: * -> *) e a.
(Monad m, MonadError e m) =>
m a -> m (e ∨ a)
throwObs m a
xM = m (e ∨ a) -> (e -> m (e ∨ a)) -> m (e ∨ a)
forall a. m a -> (e -> m a) -> m a
forall {k} e (m :: k -> *) (a :: k).
MonadError e m =>
m a -> (e -> m a) -> m a
catch ((a -> e ∨ a) -> m a -> m (e ∨ a)
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> e ∨ a
forall a b. b -> a ∨ b
Inr m a
xM) ((e -> m (e ∨ a)) -> m (e ∨ a)) -> (e -> m (e ∨ a)) -> m (e ∨ a)
forall a b. (a -> b) -> a -> b
$ (e ∨ a) -> m (e ∨ a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ((e ∨ a) -> m (e ∨ a)) -> (e -> e ∨ a) -> e -> m (e ∨ a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ e -> e ∨ a
forall e a. e -> e ∨ a
Inl

throw𝑂 ∷ (Monad m,MonadError e m) ⇒ e → 𝑂 a → m a 
throw𝑂 :: forall (m :: * -> *) e a.
(Monad m, MonadError e m) =>
e -> 𝑂 a -> m a
throw𝑂 e
e = (() -> m a) -> (a -> m a) -> 𝑂 a -> m a
forall b a. (() -> b) -> (a -> b) -> 𝑂 a -> b
elim𝑂 (m a -> () -> m a
forall a b. a -> b -> a
const (m a -> () -> m a) -> m a -> () -> m a
forall a b. (a -> b) -> a -> b
$ e -> m a
forall a. e -> m a
forall {k} e (m :: k -> *) (a :: k). MonadError e m => e -> m a
throw e
e) a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return

-- Nondet --

mconcat ∷ (MonadNondet m,ToIter (m a) t) ⇒ t → m a
mconcat :: forall {k} (m :: k -> *) (a :: k) t.
(MonadNondet m, ToIter (m a) t) =>
t -> m a
mconcat = m a -> (m a -> m a -> m a) -> t -> m a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr m a
forall (a :: k). m a
forall {k} (m :: k -> *) (a :: k). MonadNondet m => m a
mzero m a -> m a -> m a
forall (a :: k). m a -> m a -> m a
forall {k} (m :: k -> *) (a :: k).
MonadNondet m =>
m a -> m a -> m a
(⊞)

from ∷ (Monad m,MonadNondet m,ToIter a t) ⇒ t → m a
from :: forall (m :: * -> *) a t.
(Monad m, MonadNondet m, ToIter a t) =>
t -> m a
from = 𝐼 (m a) -> m a
forall {k} (m :: k -> *) (a :: k) t.
(MonadNondet m, ToIter (m a) t) =>
t -> m a
mconcat (𝐼 (m a) -> m a) -> (𝐼 a -> 𝐼 (m a)) -> 𝐼 a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (a -> m a) -> 𝐼 a -> 𝐼 (m a)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐼 a -> m a) -> (t -> 𝐼 a) -> t -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter

oneOrMoreSplitNT ∷ (Monad m,MonadNondet m) ⇒ m a → m (a ∧ 𝐿 a)
oneOrMoreSplitNT :: forall (m :: * -> *) a.
(Monad m, MonadNondet m) =>
m a -> m (a ∧ 𝐿 a)
oneOrMoreSplitNT m a
aM = do
  a
x ← m a
aM
  𝐿 a
xs ← m a -> m (𝐿 a)
forall (m :: * -> *) a. (Monad m, MonadNondet m) => m a -> m (𝐿 a)
manyNT m a
aM
  (a ∧ 𝐿 a) -> m (a ∧ 𝐿 a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ((a ∧ 𝐿 a) -> m (a ∧ 𝐿 a)) -> (a ∧ 𝐿 a) -> m (a ∧ 𝐿 a)
forall a b. (a -> b) -> a -> b
$ a
x a -> 𝐿 a -> a ∧ 𝐿 a
forall a b. a -> b -> a ∧ b
:* 𝐿 a
xs

oneOrMoreNT ∷ (Monad m,MonadNondet m) ⇒ m a → m (𝐿 a)
oneOrMoreNT :: forall (m :: * -> *) a. (Monad m, MonadNondet m) => m a -> m (𝐿 a)
oneOrMoreNT m a
xM = do
  (a
x :* 𝐿 a
xs) ← m a -> m (a ∧ 𝐿 a)
forall (m :: * -> *) a.
(Monad m, MonadNondet m) =>
m a -> m (a ∧ 𝐿 a)
oneOrMoreSplitNT m a
xM
  𝐿 a -> m (𝐿 a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐿 a -> m (𝐿 a)) -> 𝐿 a -> m (𝐿 a)
forall a b. (a -> b) -> a -> b
$ a
x a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 a
xs

manyNT ∷ (Monad m,MonadNondet m) ⇒ m a → m (𝐿 a)
manyNT :: forall (m :: * -> *) a. (Monad m, MonadNondet m) => m a -> m (𝐿 a)
manyNT m a
aM = [m (𝐿 a)] -> m (𝐿 a)
forall {k} (m :: k -> *) (a :: k) t.
(MonadNondet m, ToIter (m a) t) =>
t -> m a
mconcat
  [ m a -> m (𝐿 a)
forall (m :: * -> *) a. (Monad m, MonadNondet m) => m a -> m (𝐿 a)
oneOrMoreNT m a
aM
  , 𝐿 a -> m (𝐿 a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return 𝐿 a
forall a. Null a => a
null
  ]

twoOrMoreSplitNT ∷ (Monad m,MonadNondet m) ⇒ m a → m (a ∧ a ∧ 𝐿 a)
twoOrMoreSplitNT :: forall (m :: * -> *) a.
(Monad m, MonadNondet m) =>
m a -> m ((a ∧ a) ∧ 𝐿 a)
twoOrMoreSplitNT m a
aM = do
  a
x₁ ← m a
aM
  (a
x₂ :* 𝐿 a
xs) ← m a -> m (a ∧ 𝐿 a)
forall (m :: * -> *) a.
(Monad m, MonadNondet m) =>
m a -> m (a ∧ 𝐿 a)
oneOrMoreSplitNT m a
aM
  ((a ∧ a) ∧ 𝐿 a) -> m ((a ∧ a) ∧ 𝐿 a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (a
x₁ a -> a -> a ∧ a
forall a b. a -> b -> a ∧ b
:* a
x₂ (a ∧ a) -> 𝐿 a -> (a ∧ a) ∧ 𝐿 a
forall a b. a -> b -> a ∧ b
:* 𝐿 a
xs)

manySepBy ∷ (Monad m,MonadNondet m) ⇒ m () → m a → m (𝐿 a)
manySepBy :: forall (m :: * -> *) a.
(Monad m, MonadNondet m) =>
m () -> m a -> m (𝐿 a)
manySepBy m ()
uM m a
xM = [m (𝐿 a)] -> m (𝐿 a)
forall {k} (m :: k -> *) (a :: k) t.
(MonadNondet m, ToIter (m a) t) =>
t -> m a
mconcat
  [ do
      a
x ← m a
xM
      𝐿 a
xs ← m () -> m a -> m (𝐿 a)
forall (m :: * -> *) a.
(Monad m, MonadNondet m) =>
m () -> m a -> m (𝐿 a)
manyPrefBy m ()
uM m a
xM
      𝐿 a -> m (𝐿 a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐿 a -> m (𝐿 a)) -> 𝐿 a -> m (𝐿 a)
forall a b. (a -> b) -> a -> b
$ a
x a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 a
xs
  , 𝐿 a -> m (𝐿 a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return 𝐿 a
forall a. Null a => a
null
  ]

manyPrefBy ∷ (Monad m,MonadNondet m) ⇒ m () → m a → m (𝐿 a)
manyPrefBy :: forall (m :: * -> *) a.
(Monad m, MonadNondet m) =>
m () -> m a -> m (𝐿 a)
manyPrefBy m ()
uM m a
xM = [m (𝐿 a)] -> m (𝐿 a)
forall {k} (m :: k -> *) (a :: k) t.
(MonadNondet m, ToIter (m a) t) =>
t -> m a
mconcat
  [ do
      m ()
uM
      a
x ← m a
xM
      𝐿 a
xs ← m () -> m a -> m (𝐿 a)
forall (m :: * -> *) a.
(Monad m, MonadNondet m) =>
m () -> m a -> m (𝐿 a)
manyPrefBy m ()
uM m a
xM
      𝐿 a -> m (𝐿 a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐿 a -> m (𝐿 a)) -> 𝐿 a -> m (𝐿 a)
forall a b. (a -> b) -> a -> b
$ a
x a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 a
xs
  , 𝐿 a -> m (𝐿 a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return 𝐿 a
forall a. Null a => a
null
  ]

mzero𝑂 ∷ (Monad m,MonadNondet m) ⇒ 𝑂 a → m a
mzero𝑂 :: forall (m :: * -> *) a. (Monad m, MonadNondet m) => 𝑂 a -> m a
mzero𝑂 = (() -> m a) -> (a -> m a) -> 𝑂 a -> m a
forall b a. (() -> b) -> (a -> b) -> 𝑂 a -> b
elim𝑂 (m a -> () -> m a
forall a b. a -> b -> a
const m a
forall a. m a
forall {k} (m :: k -> *) (a :: k). MonadNondet m => m a
mzero) a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return

return𝑃 ∷ ∀ m a. (Monad m,MonadNondet m) ⇒ 𝑃 a → m a
return𝑃 :: forall (m :: * -> *) a. (Monad m, MonadNondet m) => 𝑃 a -> m a
return𝑃 = m a -> (a -> m a -> m a) -> 𝑃 a -> m a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold m a
forall a. m a
forall {k} (m :: k -> *) (a :: k). MonadNondet m => m a
mzero (\ a
x m a
xM → m a
xM m a -> m a -> m a
forall a. m a -> m a -> m a
forall {k} (m :: k -> *) (a :: k).
MonadNondet m =>
m a -> m a -> m a
⊞ a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return a
x)

-- Cont --

reset ∷ (Monad m,MonadCont u m) ⇒ m u → m u 
reset :: forall (m :: * -> *) u. (Monad m, MonadCont u m) => m u -> m u
reset m u
aM = ((u -> m u) -> m u) -> m u
forall a. ((a -> m u) -> m u) -> m a
forall r (m :: * -> *) a.
MonadCont r m =>
((a -> m r) -> m r) -> m a
callCC (((u -> m u) -> m u) -> m u) -> ((u -> m u) -> m u) -> m u
forall a b. (a -> b) -> a -> b
$ \ u -> m u
k → u -> m u
k (u -> m u) -> m u -> m u
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ (u -> m u) -> m u -> m u
forall a. (a -> m u) -> m a -> m u
forall r (m :: * -> *) a. MonadCont r m => (a -> m r) -> m a -> m r
withC u -> m u
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return m u
aM

modifyC ∷ (Monad m,MonadCont u m) ⇒ (u → m u) → m ()
modifyC :: forall (m :: * -> *) u.
(Monad m, MonadCont u m) =>
(u -> m u) -> m ()
modifyC u -> m u
f = ((() -> m u) -> m u) -> m ()
forall a. ((a -> m u) -> m u) -> m a
forall r (m :: * -> *) a.
MonadCont r m =>
((a -> m r) -> m r) -> m a
callCC (((() -> m u) -> m u) -> m ()) -> ((() -> m u) -> m u) -> m ()
forall a b. (a -> b) -> a -> b
$ \ () -> m u
k → u -> m u
f (u -> m u) -> m u -> m u
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ () -> m u
k ()

withCOn ∷ (Monad m,MonadCont u m) ⇒ m a → (a → m u) → m u
withCOn :: forall (m :: * -> *) u a.
(Monad m, MonadCont u m) =>
m a -> (a -> m u) -> m u
withCOn = ((a -> m u) -> m a -> m u) -> m a -> (a -> m u) -> m u
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> m u) -> m a -> m u
forall a. (a -> m u) -> m a -> m u
forall r (m :: * -> *) a. MonadCont r m => (a -> m r) -> m a -> m r
withC

putEnv ∷ (Monad m,MonadReader r m,MonadCont u m) ⇒ r → m ()
putEnv :: forall (m :: * -> *) r u.
(Monad m, MonadReader r m, MonadCont u m) =>
r -> m ()
putEnv r
r = ((() -> m u) -> m u) -> m ()
forall a. ((a -> m u) -> m u) -> m a
forall r (m :: * -> *) a.
MonadCont r m =>
((a -> m r) -> m r) -> m a
callCC (((() -> m u) -> m u) -> m ()) -> ((() -> m u) -> m u) -> m ()
forall a b. (a -> b) -> a -> b
$ \ () -> m u
𝓀 → r -> m u -> m u
forall (m :: * -> *) r a.
(Monad m, MonadReader r m) =>
r -> m a -> m a
local r
r (m u -> m u) -> m u -> m u
forall a b. (a -> b) -> a -> b
$ () -> m u
𝓀 ()

putEnvL ∷ (Monad m,MonadReader r m,MonadCont u m) ⇒ r ⟢ r' → r' → m ()
putEnvL :: forall (m :: * -> *) r u r'.
(Monad m, MonadReader r m, MonadCont u m) =>
(r ⟢ r') -> r' -> m ()
putEnvL r ⟢ r'
ℓ r'
r = ((() -> m u) -> m u) -> m ()
forall a. ((a -> m u) -> m u) -> m a
forall r (m :: * -> *) a.
MonadCont r m =>
((a -> m r) -> m r) -> m a
callCC (((() -> m u) -> m u) -> m ()) -> ((() -> m u) -> m u) -> m ()
forall a b. (a -> b) -> a -> b
$ \ () -> m u
𝓀 → (r ⟢ r') -> r' -> m u -> m u
forall a r'. (r ⟢ r') -> r' -> m a -> m a
forall r (m :: * -> *) a r'.
MonadReader r m =>
(r ⟢ r') -> r' -> m a -> m a
localL r ⟢ r'
ℓ r'
r (m u -> m u) -> m u -> m u
forall a b. (a -> b) -> a -> b
$ () -> m u
𝓀 ()

modifyEnv ∷ (Monad m,MonadReader r m,MonadCont u m) ⇒ (r → r) → m ()
modifyEnv :: forall (m :: * -> *) r u.
(Monad m, MonadReader r m, MonadCont u m) =>
(r -> r) -> m ()
modifyEnv r -> r
f = do
  r
r ← m r
forall (m :: * -> *) r. (Monad m, MonadReader r m) => m r
ask
  r -> m ()
forall (m :: * -> *) r u.
(Monad m, MonadReader r m, MonadCont u m) =>
r -> m ()
putEnv (r -> m ()) -> r -> m ()
forall a b. (a -> b) -> a -> b
$ r -> r
f r
r

modifyEnvL ∷ (Monad m,MonadReader r m,MonadCont u m) ⇒ r ⟢ r' → (r' → r') → m ()
modifyEnvL :: forall (m :: * -> *) r u r'.
(Monad m, MonadReader r m, MonadCont u m) =>
(r ⟢ r') -> (r' -> r') -> m ()
modifyEnvL r ⟢ r'
ℓ r' -> r'
f = do
  r'
r ← (r ⟢ r') -> m r'
forall r'. (r ⟢ r') -> m r'
forall r (m :: * -> *) r'. MonadReader r m => (r ⟢ r') -> m r'
askL r ⟢ r'
ℓ
  (r ⟢ r') -> r' -> m ()
forall (m :: * -> *) r u r'.
(Monad m, MonadReader r m, MonadCont u m) =>
(r ⟢ r') -> r' -> m ()
putEnvL r ⟢ r'
ℓ (r' -> m ()) -> r' -> m ()
forall a b. (a -> b) -> a -> b
$ r' -> r'
f r'
r

-- UCont --

ureset ∷ (Monad m,MonadUCont m) ⇒ m a → m a 
ureset :: forall (m :: * -> *) a. (Monad m, MonadUCont m) => m a -> m a
ureset m a
aM = (forall u. (a -> m u) -> m u) -> m a
forall a. (forall u. (a -> m u) -> m u) -> m a
forall (m :: * -> *) a.
MonadUCont m =>
(forall u. (a -> m u) -> m u) -> m a
ucallCC ((forall u. (a -> m u) -> m u) -> m a)
-> (forall u. (a -> m u) -> m u) -> m a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> m u
k → a -> m u
k (a -> m u) -> m a -> m u
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ (a -> m a) -> m a -> m a
forall a u. (a -> m u) -> m a -> m u
forall (m :: * -> *) a u. MonadUCont m => (a -> m u) -> m a -> m u
uwithC a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return m a
aM

umodifyC ∷ (Monad m,MonadUCont m) ⇒ (∀ u. u → m u) → m ()
umodifyC :: forall (m :: * -> *).
(Monad m, MonadUCont m) =>
(forall u. u -> m u) -> m ()
umodifyC forall u. u -> m u
f = (forall u. (() -> m u) -> m u) -> m ()
forall a. (forall u. (a -> m u) -> m u) -> m a
forall (m :: * -> *) a.
MonadUCont m =>
(forall u. (a -> m u) -> m u) -> m a
ucallCC ((forall u. (() -> m u) -> m u) -> m ())
-> (forall u. (() -> m u) -> m u) -> m ()
forall a b. (a -> b) -> a -> b
HS.$ \ () -> m u
k → u -> m u
forall u. u -> m u
f (u -> m u) -> m u -> m u
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ () -> m u
k ()

uwithCOn ∷ (Monad m,MonadUCont m) ⇒ m a → (a → m u) → m u
uwithCOn :: forall (m :: * -> *) a u.
(Monad m, MonadUCont m) =>
m a -> (a -> m u) -> m u
uwithCOn = ((a -> m u) -> m a -> m u) -> m a -> (a -> m u) -> m u
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> m u) -> m a -> m u
forall a u. (a -> m u) -> m a -> m u
forall (m :: * -> *) a u. MonadUCont m => (a -> m u) -> m a -> m u
uwithC

uputEnv ∷ (Monad m,MonadReader r m,MonadUCont m) ⇒ r → m ()
uputEnv :: forall (m :: * -> *) r.
(Monad m, MonadReader r m, MonadUCont m) =>
r -> m ()
uputEnv r
r = (forall u. (() -> m u) -> m u) -> m ()
forall a. (forall u. (a -> m u) -> m u) -> m a
forall (m :: * -> *) a.
MonadUCont m =>
(forall u. (a -> m u) -> m u) -> m a
ucallCC ((forall u. (() -> m u) -> m u) -> m ())
-> (forall u. (() -> m u) -> m u) -> m ()
forall a b. (a -> b) -> a -> b
HS.$ \ () -> m u
𝓀 → r -> m u -> m u
forall (m :: * -> *) r a.
(Monad m, MonadReader r m) =>
r -> m a -> m a
local r
r (m u -> m u) -> m u -> m u
forall a b. (a -> b) -> a -> b
$ () -> m u
𝓀 ()

uputEnvL ∷ (Monad m,MonadReader r m,MonadUCont m) ⇒ r ⟢ r' → r' → m ()
uputEnvL :: forall (m :: * -> *) r r'.
(Monad m, MonadReader r m, MonadUCont m) =>
(r ⟢ r') -> r' -> m ()
uputEnvL r ⟢ r'
ℓ r'
r = (forall u. (() -> m u) -> m u) -> m ()
forall a. (forall u. (a -> m u) -> m u) -> m a
forall (m :: * -> *) a.
MonadUCont m =>
(forall u. (a -> m u) -> m u) -> m a
ucallCC ((forall u. (() -> m u) -> m u) -> m ())
-> (forall u. (() -> m u) -> m u) -> m ()
forall a b. (a -> b) -> a -> b
HS.$ \ () -> m u
𝓀 → (r ⟢ r') -> r' -> m u -> m u
forall a r'. (r ⟢ r') -> r' -> m a -> m a
forall r (m :: * -> *) a r'.
MonadReader r m =>
(r ⟢ r') -> r' -> m a -> m a
localL r ⟢ r'
ℓ r'
r (m u -> m u) -> m u -> m u
forall a b. (a -> b) -> a -> b
$ () -> m u
𝓀 ()

umodifyEnv ∷ (Monad m,MonadReader r m,MonadUCont m) ⇒ (r → r) → m ()
umodifyEnv :: forall (m :: * -> *) r.
(Monad m, MonadReader r m, MonadUCont m) =>
(r -> r) -> m ()
umodifyEnv r -> r
f = do
  r
r ← m r
forall (m :: * -> *) r. (Monad m, MonadReader r m) => m r
ask
  r -> m ()
forall (m :: * -> *) r.
(Monad m, MonadReader r m, MonadUCont m) =>
r -> m ()
uputEnv (r -> m ()) -> r -> m ()
forall a b. (a -> b) -> a -> b
$ r -> r
f r
r

umodifyEnvL ∷ (Monad m,MonadReader r m,MonadUCont m) ⇒ r ⟢ r' → (r' → r') → m ()
umodifyEnvL :: forall (m :: * -> *) r r'.
(Monad m, MonadReader r m, MonadUCont m) =>
(r ⟢ r') -> (r' -> r') -> m ()
umodifyEnvL r ⟢ r'
ℓ r' -> r'
f = do
  r'
r ← (r ⟢ r') -> m r'
forall r'. (r ⟢ r') -> m r'
forall r (m :: * -> *) r'. MonadReader r m => (r ⟢ r') -> m r'
askL r ⟢ r'
ℓ
  (r ⟢ r') -> r' -> m ()
forall (m :: * -> *) r r'.
(Monad m, MonadReader r m, MonadUCont m) =>
(r ⟢ r') -> r' -> m ()
uputEnvL r ⟢ r'
ℓ (r' -> m ()) -> r' -> m ()
forall a b. (a -> b) -> a -> b
$ r' -> r'
f r'
r

unextEnvL ∷ (Monad m,MonadReader r m,MonadUCont m,Zero a,One a,Plus a) ⇒ r ⟢ a → m a
unextEnvL :: forall (m :: * -> *) r a.
(Monad m, MonadReader r m, MonadUCont m, Zero a, One a, Plus a) =>
(r ⟢ a) -> m a
unextEnvL r ⟢ a
ℓ = do
  a
x ← (r ⟢ a) -> m a
forall r'. (r ⟢ r') -> m r'
forall r (m :: * -> *) r'. MonadReader r m => (r ⟢ r') -> m r'
askL r ⟢ a
ℓ
  (r ⟢ a) -> a -> m ()
forall (m :: * -> *) r r'.
(Monad m, MonadReader r m, MonadUCont m) =>
(r ⟢ r') -> r' -> m ()
uputEnvL r ⟢ a
ℓ (a -> m ()) -> a -> m ()
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. (One a, Plus a) => a -> a
succ a
x
  a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return a
x

--------------
-- DERIVING --
--------------

deriveAskL ∷ ∀ m₁ m₂ r r'. (m₁ ⇄⁻ m₂,MonadReader r m₂) ⇒ r ⟢ r' → m₁ r'
deriveAskL :: forall (m₁ :: * -> *) (m₂ :: * -> *) r r'.
(m₁ ⇄⁻ m₂, MonadReader r m₂) =>
(r ⟢ r') -> m₁ r'
deriveAskL = m₂ r' -> m₁ r'
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 (m₂ r' -> m₁ r') -> ((r ⟢ r') -> m₂ r') -> (r ⟢ r') -> m₁ r'
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (r ⟢ r') -> m₂ r'
forall r'. (r ⟢ r') -> m₂ r'
forall r (m :: * -> *) r'. MonadReader r m => (r ⟢ r') -> m r'
askL

deriveLocal ∷ ∀ m₁ m₂ r r' a. (m₁ ⇄⁻ m₂,MonadReader r m₂) ⇒ r ⟢ r' → r' → m₁ a → m₁ a
deriveLocal :: forall (m₁ :: * -> *) (m₂ :: * -> *) r r' a.
(m₁ ⇄⁻ m₂, MonadReader r m₂) =>
(r ⟢ r') -> r' -> m₁ a -> m₁ a
deriveLocal r ⟢ r'
ℓ r'
r = m₂ a -> m₁ a
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 (m₂ a -> m₁ a) -> (m₂ a -> m₂ a) -> m₂ a -> m₁ a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (r ⟢ r') -> r' -> m₂ a -> m₂ a
forall a r'. (r ⟢ r') -> r' -> m₂ a -> m₂ a
forall r (m :: * -> *) a r'.
MonadReader r m =>
(r ⟢ r') -> r' -> m a -> m a
localL r ⟢ r'
ℓ r'
r (m₂ a -> m₁ a) -> (m₁ a -> m₂ a) -> m₁ a -> m₁ a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ m₁ a -> m₂ a
m₁ →⁻ m₂
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => t →⁻ u
isoto2

deriveTell ∷ ∀ m₁ m₂ o. (m₁ ⇄⁻ m₂,MonadWriter o m₂) ⇒ o → m₁ ()
deriveTell :: forall (m₁ :: * -> *) (m₂ :: * -> *) o.
(m₁ ⇄⁻ m₂, MonadWriter o m₂) =>
o -> m₁ ()
deriveTell = m₂ () -> m₁ ()
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 (m₂ () -> m₁ ()) -> (o -> m₂ ()) -> o -> m₁ ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ o -> m₂ ()
forall o (m :: * -> *). MonadWriter o m => o -> m ()
tell

deriveHijack ∷ ∀ m₁ m₂ o a. (m₁ ⇄⁻ m₂,MonadWriter o m₂) ⇒ m₁ a → m₁ (o ∧ a)
deriveHijack :: forall (m₁ :: * -> *) (m₂ :: * -> *) o a.
(m₁ ⇄⁻ m₂, MonadWriter o m₂) =>
m₁ a -> m₁ (o ∧ a)
deriveHijack = m₂ (o ∧ a) -> m₁ (o ∧ a)
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 (m₂ (o ∧ a) -> m₁ (o ∧ a))
-> (m₂ a -> m₂ (o ∧ a)) -> m₂ a -> m₁ (o ∧ a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ m₂ a -> m₂ (o ∧ a)
forall a. m₂ a -> m₂ (o ∧ a)
forall o (m :: * -> *) a. MonadWriter o m => m a -> m (o ∧ a)
hijack (m₂ a -> m₁ (o ∧ a)) -> (m₁ a -> m₂ a) -> m₁ a -> m₁ (o ∧ a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ m₁ a -> m₂ a
m₁ →⁻ m₂
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => t →⁻ u
isoto2

deriveGet ∷ ∀ m₁ m₂ s. (m₁ ⇄⁻ m₂,MonadState s m₂) ⇒ m₁ s
deriveGet :: forall (m₁ :: * -> *) (m₂ :: * -> *) s.
(m₁ ⇄⁻ m₂, MonadState s m₂) =>
m₁ s
deriveGet = m₂ s -> m₁ s
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 m₂ s
forall s (m :: * -> *). MonadState s m => m s
get

derivePut ∷ ∀ m₁ m₂ s. (m₁ ⇄⁻ m₂,MonadState s m₂) ⇒ s → m₁ ()
derivePut :: forall (m₁ :: * -> *) (m₂ :: * -> *) s.
(m₁ ⇄⁻ m₂, MonadState s m₂) =>
s -> m₁ ()
derivePut = m₂ () -> m₁ ()
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 (m₂ () -> m₁ ()) -> (s -> m₂ ()) -> s -> m₁ ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ s -> m₂ ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put

deriveAbort ∷ ∀ m₁ m₂ a. (m₁ ⇄⁻ m₂,MonadFail m₂) ⇒ m₁ a
deriveAbort :: forall (m₁ :: * -> *) (m₂ :: * -> *) a.
(m₁ ⇄⁻ m₂, MonadFail m₂) =>
m₁ a
deriveAbort = m₂ a -> m₁ a
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 m₂ a
forall a. m₂ a
forall {k} (m :: k -> *) (a :: k). MonadFail m => m a
abort

deriveTry ∷ ∀ m₁ m₂ a. (m₁ ⇄⁻ m₂,MonadFail m₂) ⇒ m₁ a → m₁ a → m₁ a
deriveTry :: forall (m₁ :: * -> *) (m₂ :: * -> *) a.
(m₁ ⇄⁻ m₂, MonadFail m₂) =>
m₁ a -> m₁ a -> m₁ a
deriveTry m₁ a
xM₁ m₁ a
xM₂ = m₂ a -> m₁ a
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 (m₂ a -> m₁ a) -> m₂ a -> m₁ a
forall a b. (a -> b) -> a -> b
$ m₁ a -> m₂ a
m₁ →⁻ m₂
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => t →⁻ u
isoto2 m₁ a
xM₁ m₂ a -> m₂ a -> m₂ a
forall a. m₂ a -> m₂ a -> m₂ a
forall {k} (m :: k -> *) (a :: k). MonadFail m => m a -> m a -> m a
⎅ m₁ a -> m₂ a
m₁ →⁻ m₂
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => t →⁻ u
isoto2 m₁ a
xM₂

deriveThrow ∷ ∀ m₁ m₂ e a. (m₁ ⇄⁻ m₂,MonadError e m₂) ⇒ e → m₁ a
deriveThrow :: forall (m₁ :: * -> *) (m₂ :: * -> *) e a.
(m₁ ⇄⁻ m₂, MonadError e m₂) =>
e -> m₁ a
deriveThrow e
e = m₂ a -> m₁ a
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 (m₂ a -> m₁ a) -> m₂ a -> m₁ a
forall a b. (a -> b) -> a -> b
$ e -> m₂ a
forall a. e -> m₂ a
forall {k} e (m :: k -> *) (a :: k). MonadError e m => e -> m a
throw e
e

deriveCatch ∷ ∀ m₁ m₂ e a. (m₁ ⇄⁻ m₂,MonadError e m₂) ⇒ m₁ a → (e → m₁ a) → m₁ a
deriveCatch :: forall (m₁ :: * -> *) (m₂ :: * -> *) e a.
(m₁ ⇄⁻ m₂, MonadError e m₂) =>
m₁ a -> (e -> m₁ a) -> m₁ a
deriveCatch m₁ a
xM e -> m₁ a
k = m₂ a -> m₁ a
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 (m₂ a -> m₁ a) -> m₂ a -> m₁ a
forall a b. (a -> b) -> a -> b
$ m₂ a -> (e -> m₂ a) -> m₂ a
forall a. m₂ a -> (e -> m₂ a) -> m₂ a
forall {k} e (m :: k -> *) (a :: k).
MonadError e m =>
m a -> (e -> m a) -> m a
catch (m₁ a -> m₂ a
m₁ →⁻ m₂
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => t →⁻ u
isoto2 m₁ a
xM) (m₁ a -> m₂ a
m₁ →⁻ m₂
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => t →⁻ u
isoto2 (m₁ a -> m₂ a) -> (e -> m₁ a) -> e -> m₂ a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ e -> m₁ a
k)

deriveMzero ∷ ∀ m₁ m₂ a. (m₁ ⇄⁻ m₂,MonadNondet m₂) ⇒ m₁ a
deriveMzero :: forall (m₁ :: * -> *) (m₂ :: * -> *) a.
(m₁ ⇄⁻ m₂, MonadNondet m₂) =>
m₁ a
deriveMzero = m₂ a -> m₁ a
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 m₂ a
forall a. m₂ a
forall {k} (m :: k -> *) (a :: k). MonadNondet m => m a
mzero

deriveMplus ∷ ∀ m₁ m₂ a. (m₁ ⇄⁻ m₂,MonadNondet m₂) ⇒ m₁ a → m₁ a → m₁ a
deriveMplus :: forall (m₁ :: * -> *) (m₂ :: * -> *) a.
(m₁ ⇄⁻ m₂, MonadNondet m₂) =>
m₁ a -> m₁ a -> m₁ a
deriveMplus m₁ a
xM₁ m₁ a
xM₂ = m₂ a -> m₁ a
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 (m₂ a -> m₁ a) -> m₂ a -> m₁ a
forall a b. (a -> b) -> a -> b
$ m₁ a -> m₂ a
m₁ →⁻ m₂
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => t →⁻ u
isoto2 m₁ a
xM₁ m₂ a -> m₂ a -> m₂ a
forall a. m₂ a -> m₂ a -> m₂ a
forall {k} (m :: k -> *) (a :: k).
MonadNondet m =>
m a -> m a -> m a
⊞ m₁ a -> m₂ a
m₁ →⁻ m₂
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => t →⁻ u
isoto2 m₁ a
xM₂

deriveMtop ∷ ∀ m₁ m₂ a. (m₁ ⇄⁻ m₂,MonadTop m₂) ⇒ m₁ a
deriveMtop :: forall (m₁ :: * -> *) (m₂ :: * -> *) a.
(m₁ ⇄⁻ m₂, MonadTop m₂) =>
m₁ a
deriveMtop = m₂ a -> m₁ a
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 m₂ a
forall a. m₂ a
forall {k} (m :: k -> *) (a :: k). MonadTop m => m a
mtop

deriveCallCC ∷ ∀ m₁ m₂ r a. (m₁ ⇄⁻ m₂,MonadCont r m₂) ⇒ ((a → m₁ r) → m₁ r) → m₁ a
deriveCallCC :: forall (m₁ :: * -> *) (m₂ :: * -> *) r a.
(m₁ ⇄⁻ m₂, MonadCont r m₂) =>
((a -> m₁ r) -> m₁ r) -> m₁ a
deriveCallCC (a -> m₁ r) -> m₁ r
ff = m₂ a -> m₁ a
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 (m₂ a -> m₁ a) -> m₂ a -> m₁ a
forall a b. (a -> b) -> a -> b
$ ((a -> m₂ r) -> m₂ r) -> m₂ a
forall a. ((a -> m₂ r) -> m₂ r) -> m₂ a
forall r (m :: * -> *) a.
MonadCont r m =>
((a -> m r) -> m r) -> m a
callCC (((a -> m₂ r) -> m₂ r) -> m₂ a) -> ((a -> m₂ r) -> m₂ r) -> m₂ a
forall a b. (a -> b) -> a -> b
$ \ a -> m₂ r
k → m₁ r -> m₂ r
m₁ →⁻ m₂
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => t →⁻ u
isoto2 (m₁ r -> m₂ r) -> m₁ r -> m₂ r
forall a b. (a -> b) -> a -> b
$ (a -> m₁ r) -> m₁ r
ff (m₂ r -> m₁ r
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 (m₂ r -> m₁ r) -> (a -> m₂ r) -> a -> m₁ r
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> m₂ r
k)

deriveWithC ∷ ∀ m₁ m₂ r a. (m₁ ⇄⁻ m₂,MonadCont r m₂) ⇒ (a → m₁ r) → m₁ a → m₁ r
deriveWithC :: forall (m₁ :: * -> *) (m₂ :: * -> *) r a.
(m₁ ⇄⁻ m₂, MonadCont r m₂) =>
(a -> m₁ r) -> m₁ a -> m₁ r
deriveWithC a -> m₁ r
k m₁ a
xM = m₂ r -> m₁ r
m₂ →⁻ m₁
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => u →⁻ t
isofr2 (m₂ r -> m₁ r) -> m₂ r -> m₁ r
forall a b. (a -> b) -> a -> b
$ (a -> m₂ r) -> m₂ a -> m₂ r
forall a. (a -> m₂ r) -> m₂ a -> m₂ r
forall r (m :: * -> *) a. MonadCont r m => (a -> m r) -> m a -> m r
withC (m₁ r -> m₂ r
m₁ →⁻ m₂
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => t →⁻ u
isoto2 (m₁ r -> m₂ r) -> (a -> m₁ r) -> a -> m₂ r
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> m₁ r
k) (m₁ a -> m₂ a
m₁ →⁻ m₂
forall (t :: * -> *) (u :: * -> *). (t ⇄⁻ u) => t →⁻ u
isoto2 m₁ a
xM)