Idris2Doc : Text.ILex.Runner

Text.ILex.Runner

(source)
Reexports
import public Text.ParseError
import public Text.FC
import public Text.ILex.Parser
Definitions
run : Parser1 e a -> IBuffer n -> Either e a
  Tries to parse a byte vector into a value.

  Totality: total
  Visibility: export
runString : Parser1 e a -> String -> Either e a
  Like `run` but processes a UTF-8 string instead.

  Totality: total
  Visibility: export
runBytes : Parser1 e a -> ByteString -> Either e a
  Like `run` but processes a `ByteString` instead.

  Totality: total
  Visibility: export
runList : Parser1 e a -> List ByteString -> Either e a
  Like `run` but processes a `ByteString` instead.

  Totality: total
  Visibility: export
parse : Parser1 (BBErr e) a -> Origin -> IBuffer n -> Either (ParseError e) a
  Like `run` but fails with a proper parse error
  including error bounds and highlighting of
  the section where an error occurred.

  Totality: total
  Visibility: export
parseString : Parser1 (BBErr e) a -> Origin -> String -> Either (ParseError e) a
  Like `parse` but processes a UTF-8 string instead.

  Totality: total
  Visibility: export
parseBytes : Parser1 (BBErr e) a -> Origin -> ByteString -> Either (ParseError e) a
  Like `parse` but processes a `ByteString` instead.

  Totality: total
  Visibility: export
record LexState : P1 q e a -> Type
  Lexing state.
  
  This encapsulates the current state as well as
  the remainder of the previous chunk that marks
  the beginning of the current token.

  Totality: total
  Visibility: public export
  Constructor: 
LST : PIx p -> PST p -> PStepper sts p -> PByteStep sts p -> PStep p -> LexState p

  Projections:
  
.cur : ({rec:0} : LexState p) -> PByteStep (sts {rec:0}) p
  
.dfa : ({rec:0} : LexState p) -> PStepper (sts {rec:0}) p
  
.stack : LexState p -> PST p
  
.state : LexState p -> PIx p
  
0 .sts : LexState p -> Nat
  
.tok : LexState p -> PStep p
0 .sts : LexState p -> Nat
  Totality: total
  Visibility: public export
0 sts : LexState p -> Nat
  Totality: total
  Visibility: public export
.state : LexState p -> PIx p
  Totality: total
  Visibility: public export
state : LexState p -> PIx p
  Totality: total
  Visibility: public export
.stack : LexState p -> PST p
  Totality: total
  Visibility: public export
stack : LexState p -> PST p
  Totality: total
  Visibility: public export
.dfa : ({rec:0} : LexState p) -> PStepper (sts {rec:0}) p
  Totality: total
  Visibility: public export
dfa : ({rec:0} : LexState p) -> PStepper (sts {rec:0}) p
  Totality: total
  Visibility: public export
.cur : ({rec:0} : LexState p) -> PByteStep (sts {rec:0}) p
  Totality: total
  Visibility: public export
cur : ({rec:0} : LexState p) -> PByteStep (sts {rec:0}) p
  Totality: total
  Visibility: public export
.tok : LexState p -> PStep p
  Totality: total
  Visibility: public export
tok : LexState p -> PStep p
  Totality: total
  Visibility: public export
init : (p : P1 q e a) -> F1 q (LexState p)
  Totality: total
  Visibility: export
0 LoopRes : P1 q e a -> Type
  Result of a partial lexing step: In such a step, we lex
  till the end of a chunk of bytes, allowing for a remainder of
  bytes that could not yet be identified as a tokens.

  Totality: total
  Visibility: public export
lastStep : (p : P1 q e a) -> LexState p -> F1 q (Either e a)
  Totality: total
  Visibility: export
stepState : IBuffer n -> (p : P1 q e a) -> LexState p -> LoopRes p
  Totality: total
  Visibility: export