Data.Swirl.Parsing

Reexports

Definitions

data WhetherConsumeLast : Type -> Type

Totality: total
Visibility: public export
Constructors:

ConsumeLast : a -> WhetherConsumeLast a

DoNotConsumeLast : a -> WhetherConsumeLast a

Hint: 

Functor WhetherConsumeLast

.val : WhetherConsumeLast a -> a

Totality: total
Visibility: export

ifConsumes : WhetherConsumeLast a -> Lazy b -> Lazy b -> b

Totality: total
Visibility: export

record RawParser : (Type -> Type) -> Type -> Type -> Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

RP : st -> (o -> st -> Either st (WhetherConsumeLast (Swirl m e' () o'))) -> (st -> r -> Swirl m e' r' o') -> RawParser m st e' r r' o o'

Projections:

.initSeed : RawParser m st e' r r' o o' -> st

.manageFin : RawParser m st e' r r' o o' -> st -> r -> Swirl m e' r' o'

.parseStep : RawParser m st e' r r' o o' -> o -> st -> Either st (WhetherConsumeLast (Swirl m e' () o'))

Hint: 

Functor m => Functor (RawParser m st e' r r' o)

.initSeed : RawParser m st e' r r' o o' -> st

Totality: total
Visibility: public export

initSeed : RawParser m st e' r r' o o' -> st

Totality: total
Visibility: public export

.parseStep : RawParser m st e' r r' o o' -> o -> st -> Either st (WhetherConsumeLast (Swirl m e' () o'))

Totality: total
Visibility: public export

parseStep : RawParser m st e' r r' o o' -> o -> st -> Either st (WhetherConsumeLast (Swirl m e' () o'))

Totality: total
Visibility: public export

.manageFin : RawParser m st e' r r' o o' -> st -> r -> Swirl m e' r' o'

Totality: total
Visibility: public export

manageFin : RawParser m st e' r r' o o' -> st -> r -> Swirl m e' r' o'

Totality: total
Visibility: public export

rawParseOnce : Functor m => {auto 0 _ : IfUnsolved r' ()} -> {auto 0 _ : IfUnsolved o' Void} -> RawParser m st e'' r r' o o' -> Swirl m e r o -> Swirl m (Either e e'') (Either r' (Swirl m e r o)) o'

Totality: total
Visibility: export

rawParseAll : Functor m => {auto 0 _ : IfUnsolved r' ()} -> {auto 0 _ : IfUnsolved o' Void} -> RawParser m st e' r r' o o' -> Swirl m e r o -> Swirl m (Either e e') r' o'

Totality: total
Visibility: export