Idris2Doc : Data.Swirl

Data.Swirl

(source)
Reexports
import public Control.MonadRec
import public Language.Implicits.IfUnsolved
Definitions
data Swirl : (Type -> Type) -> Type -> Type -> Type -> Type
  Totality: total
  Visibility: export
  Constructors:
  
Done : r -> Swirl m e r o
  
Fail : e -> Swirl m e r o
  
Yield : o -> Lazy (Swirl m e r o) -> Swirl m e r o
  
Effect : m (assert_total (Swirl m e r o)) -> Swirl m e r o
  
BindR : Lazy (Swirl m e r' o) -> (r' -> Swirl m e r o) -> Swirl m e r o
  
BindE : Lazy (Swirl m e' r o) -> (e' -> Swirl m e r o) -> Swirl m e r o
  
Ensure : Lazy (Swirl m Void r' Void) -> Lazy (Swirl m e r o) -> Swirl m e (r', r) o

  Hints:
  
Functor m => Monoid r => Applicative (Swirl m e r)
  
Functor m => Bifunctor (Swirl m e)
  
Functor m => Functor (Swirl m e r)
  
HasIO io => Monoid r => HasIO (Swirl io e r)
  
Functor m => Monoid r => Monad (Swirl m e r)
  
Functor m => Monoid r => MonadError e (Swirl m e r)
  
Monoid r => MonadTrans (\m => Swirl m e r)
Swirlie : (Type -> Type) -> Type -> Type -> Type
  Totality: total
  Visibility: public export
mapCtx : Functor m => (m a -> n a) -> Swirl m e r o -> Swirl n e r o
  Totality: total
  Visibility: export
mapError : (e -> e') -> Swirl m e r o -> Swirl m e' r o
  Totality: total
  Visibility: export
concat' : Functor m => (rl -> rr -> r) -> Swirl m el rl o -> Lazy (Swirl m er rr o) -> Swirl m (Either el er) r o
  Totality: total
  Visibility: export
concat : Functor m => (rl -> rr -> r) -> Swirl m e rl o -> Lazy (Swirl m e rr o) -> Swirl m e r o
  Totality: total
  Visibility: export
(++) : Functor m => Semigroup r => Swirl m e r o -> Lazy (Swirl m e r o) -> Swirl m e r o
  Totality: total
  Visibility: export
  Fixity Declaration: infixr operator, level 7
andThen : Swirl m e () o -> Lazy (Swirl m e r o) -> Swirl m e r o
  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 1
hasSucceeded : {auto 0 _ : IfUnsolved m' m} -> {auto 0 _ : IfUnsolved e' Void} -> {auto 0 _ : IfUnsolved o' Void} -> Swirl m e r o -> Maybe (Swirl m' e' r o')
  Checks is the only thing left for the given swirl is just to succeed, without any additional actions
  
  Returns the same swirl (with possibly changed parameters) is yes, and `Nothing` if no.

  Totality: total
  Visibility: export
forgetO : Functor m => {auto 0 _ : IfUnsolved o Void} -> Swirl m e r a -> Swirl m e r o
  Totality: total
  Visibility: export
forgetR : Functor m => Monoid r => {auto 0 _ : IfUnsolved r ()} -> Swirl m e r' a -> Swirl m e r a
  Totality: total
  Visibility: export
.by : Functor m => (x -> Swirl m e r o) -> m x -> Swirl m e r o
  A postfix function modifier to create an effected swirl creation.
  E.g. `emit v` emits `v` without any action, and `emit.by mv` emits a value of type `v` from `mv` of type `m v`.

  Totality: total
  Visibility: export
  Fixity Declaration: infix operator, level 0
by : Functor m => (x -> Swirl m e r o) -> m x -> Swirl m e r o
  Totality: total
  Visibility: export
  Fixity Declaration: infix operator, level 0
preEmitTo : {auto 0 _ : IfUnsolved e Void} -> Lazy (Swirl m e r o) -> o -> Swirl m e r o
  Totality: total
  Visibility: export
emit : Monoid r => {auto 0 _ : IfUnsolved e Void} -> {auto 0 _ : IfUnsolved r ()} -> o -> Swirl m e r o
  Totality: total
  Visibility: export
preEmitsTo : {auto 0 _ : IfUnsolved e Void} -> Lazy (Swirl m e r o) -> LazyList o -> Swirl m e r o
  Totality: total
  Visibility: export
emits : Monoid r => {auto 0 _ : IfUnsolved e Void} -> {auto 0 _ : IfUnsolved r ()} -> LazyList o -> Swirl m e r o
  Totality: total
  Visibility: export
preEmitsTo' : Foldable f => {auto 0 _ : IfUnsolved e Void} -> {auto 0 _ : IfUnsolved f List} -> Lazy (Swirl m e r o) -> f o -> Swirl m e r o
  Totality: total
  Visibility: export
emits' : Monoid r => Foldable f => {auto 0 _ : IfUnsolved e Void} -> {auto 0 _ : IfUnsolved f List} -> {auto 0 _ : IfUnsolved r ()} -> f o -> Swirl m e r o
  Totality: total
  Visibility: export
succeed : {auto 0 _ : IfUnsolved e Void} -> {auto 0 _ : IfUnsolved o Void} -> r -> Swirl m e r o
  Totality: total
  Visibility: export
fail : {auto 0 _ : IfUnsolved r ()} -> {auto 0 _ : IfUnsolved o Void} -> e -> Swirl m e r o
  Totality: total
  Visibility: export
succeedOrFail : {auto 0 _ : IfUnsolved o Void} -> Either e r -> Swirl m e r o
  Totality: total
  Visibility: export
emitOrFail : Monoid r => {auto 0 _ : IfUnsolved r ()} -> Either e o -> Swirl m e r o
  Totality: total
  Visibility: export
emitRes' : Functor m => (r -> r') -> Swirl m e r Void -> Swirl m e r' r
  Totality: total
  Visibility: export
emitRes : Functor m => Monoid r => {auto 0 _ : IfUnsolved r ()} -> Swirl m e r' Void -> Swirl m e r r'
  Totality: total
  Visibility: export
swallowM : Functor m => Swirl m e r (m o) -> Swirl m e r o
  Totality: total
  Visibility: export
foldlRO : Functor m => {auto 0 _ : IfUnsolved o'' Void} -> (o' -> o -> o') -> o' -> (o' -> r -> r') -> Swirl m e r o -> Swirl m e r' o''
  Totality: total
  Visibility: export
foldlRO' : Functor m => {auto 0 _ : IfUnsolved o' Void} -> (o -> o -> o) -> (o -> r -> r) -> Swirl m e r o -> Swirl m e r o'
  Totality: total
  Visibility: export
foldRO : Functor m => Semigroup o => {auto 0 _ : IfUnsolved o' Void} -> Swirl m e o o -> Swirl m e o o'
  Totality: total
  Visibility: export
foldlO : Functor m => {auto 0 _ : IfUnsolved o' Void} -> (r -> o -> r) -> r -> Swirl m e () o -> Swirl m e r o'
  Totality: total
  Visibility: export
foldO : Functor m => Monoid o => {auto 0 _ : IfUnsolved o' Void} -> Swirl m e () o -> Swirl m e o o'
  Totality: total
  Visibility: export
outputs : Functor m => {auto 0 _ : IfUnsolved o' Void} -> Swirl m e () o -> Swirl m e (SnocList o) o'
  Totality: total
  Visibility: export
foldlO' : Functor m => (o' -> o -> o') -> o' -> Swirl m e r o -> Swirl m e r o'
  Emits the folded value once before both successful and failing ending.

  Totality: total
  Visibility: export
foldlO : Functor m => (o' -> o -> o') -> o' -> Swirl m e r o -> Swirl m e r o'
  Emits the folded value once and only before the successful ending.

  Totality: total
  Visibility: export
foldO : Functor m => Monoid o => Swirl m e r o -> Swirl m e r o
  Totality: total
  Visibility: export
outputs : Functor m => Swirl m e r o -> Swirl m e r (SnocList o)
  Totality: total
  Visibility: export
mergeCtxs' : Applicative m => Applicative n => (r'' -> r' -> r'') -> r'' -> Swirl m e r (Swirl n e' r' o) -> Swirl (m . n) (Either e e') (r, r'') o
  Totality: total
  Visibility: export
mergeCtxs : Applicative m => Applicative n => Semigroup r => Swirl m e r (Swirl n e r o) -> Swirl (m . n) e r o
  Totality: total
  Visibility: export
squashOuts' : Functor m => (r'' -> r' -> r'') -> r'' -> Swirl m e r (Swirl m e' r' o) -> Swirl m (Either e e') (r, r'') o
  Totality: total
  Visibility: export
squashOuts' : Functor m => Swirl m e r (Swirl m e' () o) -> Swirl m (Either e e') r o
  Totality: total
  Visibility: export
bindR : Swirl m e r' o -> (r' -> Swirl m e r o) -> Swirl m e r o
  Totality: total
  Visibility: export
handleRes : (r' -> Swirl m e r o) -> Swirl m e r' o -> Swirl m e r o
  Totality: total
  Visibility: export
mapEither' : Functor m => {auto 0 _ : IfUnsolved e Void} -> {auto 0 _ : IfUnsolved r ()} -> (o -> Either e' o') -> Swirl m e r o -> Swirl m (Either e e') r o'
  Totality: total
  Visibility: export
mapEither : Functor m => (o -> Either e o') -> Swirl m e r o -> Swirl m e r o'
  Totality: total
  Visibility: export
mapMaybe : Functor m => (o -> Maybe o') -> Swirl m e r o -> Swirl m e r o'
  Totality: total
  Visibility: export
filter : Functor m => (a -> Bool) -> Swirl m e r a -> Swirl m e r a
  Totality: total
  Visibility: export
(=<<:) : Functor m => (o' -> Swirl m e () o) -> Swirl m e r o' -> Swirl m e r o
  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 1
(:>>=) : Functor m => Swirl m e r o' -> (o' -> Swirl m e () o) -> Swirl m e r o
  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 1
(:>>) : Functor m => Swirl m e r () -> Lazy (Swirl m e () o) -> Swirl m e r o
  Totality: total
  Visibility: export
  Fixity Declaration: infixl operator, level 1
handleError : {auto 0 _ : IfUnsolved e' Void} -> (e -> Swirl m e' r o) -> Swirl m e r o -> Swirl m e' r o
  Totality: total
  Visibility: export
withFinally' : Functor m => Swirl m Void r' Void -> Swirl m e r o -> Swirl m e (r', r) o
  Totality: total
  Visibility: export
withFinally : Functor m => Swirl m Void () Void -> Swirl m e r o -> Swirl m e r o
  Totality: total
  Visibility: export
bracket' : Functor m => {auto 0 _ : IfUnsolved e Void} -> {auto 0 _ : IfUnsolved o Void} -> Swirl m e res o -> (res -> Swirl m Void r' Void) -> (res -> Swirl m e r o) -> Swirl m e (r', r) o
  Totality: total
  Visibility: export
bracket : Functor m => {auto 0 _ : IfUnsolved e Void} -> {auto 0 _ : IfUnsolved o Void} -> Swirl m e res o -> (res -> Swirl m Void () Void) -> (res -> Swirl m e r o) -> Swirl m e r o
  Totality: total
  Visibility: export
bracketO : Functor m => Monoid r => {auto 0 _ : IfUnsolved e Void} -> {auto 0 _ : IfUnsolved r ()} -> Swirl m e res Void -> (res -> Swirl m Void r Void) -> Swirl m e r res
  Totality: total
  Visibility: export
repeat : Functor m => {auto 0 _ : IfUnsolved e Void} -> Swirl m e () o -> Swirl m e Void o
  Visibility: export
tickUntil : Functor m => Monoid r => {auto 0 _ : IfUnsolved r ()} -> {auto 0 _ : IfUnsolved e Void} -> Swirl m e Bool Void -> Swirl m e r ()
  Emit units until given effect returns `True` or fails

  Visibility: export
take : Functor m => Nat -> Swirl m e r o -> Swirl m e r o
  Totality: total
  Visibility: export
takeWhile : Functor m => (o -> Bool) -> Swirl m e r o -> Swirl m e r o
  Totality: total
  Visibility: export
drop : Functor m => Nat -> Swirl m e r o -> Swirl m e r o
  Totality: total
  Visibility: export
dropWhile : Functor m => (o -> Bool) -> Swirl m e r o -> Swirl m e r o
  Totality: total
  Visibility: export
intersperseOuts : Functor m => Swirl m e () o -> Swirl m e r o -> Swirl m e r o
  Totality: total
  Visibility: export
iterateAlong : Functor m => (i -> i) -> i -> Swirl m e r o -> Swirl m e r (i, o)
  Totality: total
  Visibility: export
zipWithIndex : Functor m => Swirl m e r o -> Swirl m e r (Nat, o)
  Totality: total
  Visibility: export
toLazyList' : Swirl Identity e r o -> (Either e r, Lazy (LazyList o))
  Totality: total
  Visibility: export
toLazyList : Swirl Identity Void () o -> LazyList o
  Totality: total
  Visibility: export
runSwirlE : MonadRec m => Swirl m e r Void -> m (Either e r)
  Totality: total
  Visibility: export
runSwirl : MonadRec m => Swirl m Void a Void -> m a
  Totality: total
  Visibility: export
data Whirl : (Type -> Type) -> Type -> Type -> Type -> Type
  Totality: total
  Visibility: export
  Constructor: 
MkWhirl : Swirl m e r o -> Whirl m e o r

  Hints:
  
Functor m => Applicative (Whirl m e o)
  
Functor m => Bifunctor (Whirl m e)
  
Functor m => Functor (Whirl m e o)
  
HasIO m => HasIO (Whirl m e o)
  
Functor m => Monad (Whirl m e o)
  
Functor m => MonadError e (Whirl m e o)
  
MonadTrans (\m => Whirl m e o)
Whirlie : (Type -> Type) -> Type -> Type -> Type
  Totality: total
  Visibility: public export
toWhirl : Swirl m e r o -> Whirl m e o r
  Totality: total
  Visibility: export
toSwirl : Whirl m e o r -> Swirl m e r o
  Totality: total
  Visibility: export
mapAsSwirl : (Swirl m e r o -> Swirl m' e' r' o') -> Whirl m e o r -> Whirl m' e' o' r'
  Totality: total
  Visibility: export
apAsSwirl : (Swirl m1 e1 r1 o1 -> Swirl m2 e2 r2 o2 -> Swirl m e r o) -> Whirl m1 e1 o1 r1 -> Whirl m2 e2 o2 r2 -> Whirl m e o r
  Totality: total
  Visibility: export