Idris2Doc : Text.Parse.Core

Text.Parse.Core

(source)
Definitions
data Res : Bool -> (t : Type) -> List (Bounded t) -> Type -> Type -> Type -> Type
  Result of running a parser.

  Totality: total
  Visibility: public export
  Constructors:
  
Fail : Bool -> List1 (Bounded (InnerError e)) -> Res b t ts state e a
  
Succ : state -> Bounded a -> (toks : List (Bounded t)) -> Suffix b toks ts -> Res b t ts state e a

  Hint: 
FailParse (Res b t ts state e) e
merge : Bounded z -> Res b t ts s e a -> Res b t ts s e a
  Totality: total
  Visibility: public export
succ : Res b t ts s e a -> Suffix True ts ts' -> Res b1 t ts' s e a
  Totality: total
  Visibility: export
0 inf : Bool -> Type -> Type
  Totality: total
  Visibility: public export
data Grammar : Bool -> Type -> Type -> Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Lift : (state -> (ts : List (Bounded t)) -> Res b t ts state e a) -> Grammar b state t e a
  
AppEat : Grammar True state t e (a -> b) -> Inf (Grammar b2 state t e a) -> Grammar True state t e b
  
App : Grammar b1 state t e (a -> b) -> Grammar b2 state t e a -> Grammar (b1 || Delay b2) state t e b
  
BindEat : Grammar True state t e a -> Inf (a -> Grammar b2 state t e b) -> Grammar True state t e b
  
(>>=) : Grammar b1 state t e a -> (a -> Grammar b2 state t e b) -> Grammar (b1 || Delay b2) state t e b
  
ThenEat : Grammar True state t e a -> Inf (Grammar b2 state t e b) -> Grammar True state t e b
  
(>>) : Grammar b1 state t e a -> Grammar b2 state t e b -> Grammar (b1 || Delay b2) state t e b
  
Alt : Grammar b1 state t e a -> Lazy (Grammar b2 state t e a) -> Grammar (b1 && Delay b2) state t e a
  
Bounds : Grammar b state t e a -> Grammar b state t e (Bounded a)
  
Try : Grammar b state t e a -> Grammar b state t e a

  Hints:
  
FailParse (Grammar b state t e) e
  
Functor (Grammar b s t e)
(<|>) : Grammar b1 state t e a -> Lazy (Grammar b2 state t e a) -> Grammar (b1 && Delay b2) state t e a
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 2
pure : a -> Grammar False state t e a
  Totality: total
  Visibility: public export
(<*>) : Grammar b1 state t e (a -> b) -> inf b1 (Grammar b2 state t e a) -> Grammar (b1 || Delay b2) state t e b
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 3
(*>) : Grammar b1 state t e a -> Grammar b2 state t e b -> Grammar (b1 || Delay b2) state t e b
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 3
(<*) : Grammar b1 state t e a -> Grammar b2 state t e b -> Grammar (b1 || Delay b2) state t e a
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 3
nextIs : Lazy e -> (t -> Bool) -> Grammar False s t e t
  Check whether the next token satisfies a predicate

  Totality: total
  Visibility: public export
peek : Grammar False s t e t
  Look at the next token in the input

  Totality: total
  Visibility: public export
readHead : (t -> Either (InnerError e) a) -> Grammar True s t e a
  Look at the next token in the input

  Totality: total
  Visibility: public export
terminal : Interpolation t => (t -> Maybe a) -> Grammar True s t e a
  Look at the next token in the input

  Totality: total
  Visibility: public export
is : Interpolation t => Eq t => t -> Grammar True s t e ()
  Look at the next token in the input

  Totality: total
  Visibility: public export
option : a -> Grammar b state t e a -> Grammar False state t e a
  Optionally parse a thing, with a default value if the grammar doesn't
  match. May match the empty input.

  Totality: total
  Visibility: export
optional : Grammar b state t e a -> Grammar False state t e (Maybe a)
  Optionally parse a thing, with a default value if the grammar doesn't
  match. May match the empty input.

  Totality: total
  Visibility: export
some : Grammar True s t e a -> Grammar True s t e (List1 a)
  Totality: total
  Visibility: public export
many : Grammar True s t e a -> Grammar False s t e (List a)
  Totality: total
  Visibility: public export
someTill : Grammar b s t e x -> Grammar True s t e a -> Grammar True s t e (List1 a)
  Parse one or more instances of `p` until `end` succeeds, returning the
  list of values from `p`. Guaranteed to consume input.

  Totality: total
  Visibility: export
manyTill : Grammar b s t e x -> Grammar True s t e a -> Grammar b s t e (List a)
  Parse zero or more instances of `p` until `end` succeeds, returning the
  list of values from `p`. Guaranteed to consume input if `end` consumes.

  Totality: total
  Visibility: export
afterSome : Grammar True s t e x -> Grammar b s t e a -> Grammar True s t e a
  Parse one or more instance of `skip` until `p` is encountered,
  returning its value.

  Totality: total
  Visibility: export
afterMany : Grammar True s t e x -> Grammar b s t e a -> Grammar b s t e a
  Parse zero or more instance of `skip` until `p` is encountered,
  returning its value.

  Totality: total
  Visibility: export
sepBy1 : Grammar True s t e s -> Grammar b s t e a -> Grammar b s t e (List1 a)
  Parse one or more things, each separated by another thing.

  Totality: total
  Visibility: export
sepBy : Grammar True s t e s -> Grammar b s t e a -> Grammar False s t e (List a)
  Parse zero or more things, each separated by another thing. May
  match the empty input.

  Totality: total
  Visibility: export
sepEndBy1 : Grammar True s t e s -> Grammar b s t e a -> Grammar b s t e (List1 a)
  Parse one or more instances of `p` separated by and optionally terminated by
  `sep`.

  Totality: total
  Visibility: export
sepEndBy : Grammar True s t e s -> Grammar b s t e a -> Grammar False s t e (List a)
  Parse zero or more instances of `p`, separated by and optionally terminated
  by `sep`. Will not match a separator by itself.

  Totality: total
  Visibility: export
endBy1 : Grammar True s t e s -> Grammar b s t e a -> Grammar True s t e (List1 a)
  Parse one or more instances of `p`, separated and terminated by `sep`.

  Totality: total
  Visibility: export
endBy : Grammar True s t e s -> Grammar b s t e a -> Grammar False s t e (List a)
  Totality: total
  Visibility: export
between : Grammar True s t e l -> Grammar True s t e r -> Grammar b s t e a -> Grammar True s t e a
  Parse an instance of `p` that is between `left` and `right`.

  Totality: total
  Visibility: export
parse : Grammar b state t e a -> state -> List (Bounded t) -> Either (List1 (Bounded (InnerError e))) (state, (a, List (Bounded t)))
  Totality: total
  Visibility: export
lexFull : Interpolation t => Origin -> Tokenizer e t -> (t -> Bool) -> String -> Either (Bounded (InnerError e)) (List (Bounded t))
  Given a tokenizer and an input string, return a list of recognised tokens.
  
  This fails with an error if not the whole input is consumed.

  Totality: total
  Visibility: export
lexAndParse : Interpolation t => Origin -> Tokenizer e t -> (t -> Bool) -> Grammar b state t e a -> state -> String -> Either (List1 (FileContext, InnerError e)) (state, a)
  Totality: total
  Visibility: export