Idris2Doc : Text.ILex.Parser

Text.ILex.Parser

(source)
Reexports
import public Data.Prim.Bits32
import public Data.ByteString
import public Data.Linear.Ref1
import public Text.ByteBounds
import public Text.ParseError
import public Text.ILex.RExp
import public Text.ILex.Lexer
Definitions
record Arr32 : Bits32 -> Type -> Type
  Totality: total
  Visibility: export
  Constructor: 
A32 : AnyPtr -> Arr32 n a

  Projection: 
.ptr : Arr32 n a -> AnyPtr
at : Arr32 n a -> Index n -> a
  Totality: total
  Visibility: export
record Entry : Bits32 -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
E : Index n -> a -> Entry n a

  Projections:
  
.index : Entry n a -> Index n
  
.value : Entry n a -> a
.index : Entry n a -> Index n
  Totality: total
  Visibility: public export
index : Entry n a -> Index n
  Totality: total
  Visibility: public export
.value : Entry n a -> a
  Totality: total
  Visibility: public export
value : Entry n a -> a
  Totality: total
  Visibility: public export
entry : Cast t (Index n) => t -> a -> Entry n a
  Totality: total
  Visibility: export
arr32 : (n : Bits32) -> a -> List (Entry n a) -> Arr32 n a
  Totality: total
  Visibility: export
0 Lex1 : Type -> Bits32 -> (Type -> Type) -> Type
  Totality: total
  Visibility: public export
interface HasBytes : (Type -> Type) -> Type
  An interface for mutable parser stacks `s` that facilitates
  parsing string tokens containing escape sequences.

  Parameters: s
Constructor: 
MkHB

Methods:
  
prev : s q -> Ref q ByteString
  Returns the remainder of the previous bytestring that should
  be used as the beginning of the current token.
  
cur : s q -> Ref q ByteString
  The byte vector currently being processed.
  
offset : s q -> Ref q Nat
  Absolute start position of the current token from the beginning
  of the whole byte stream processed so far.
  
relpos : s q -> Ref q Integer
  Start position of the current token relative to `cur`.
  
  If this is negative, the current token will also include
  `prev`. Reference `len` will still hold the full length
  of the token.
  
len : s q -> Ref q Nat
  Length of the current token
  
positions : s q -> Ref q (SnocList BytePos)
  Stack of positions used to keep track of the positions of
  opening parentheses and brackets.

Implementation: 
HasBytes (DStack s e)
prev : HasBytes s => s q -> Ref q ByteString
  Returns the remainder of the previous bytestring that should
  be used as the beginning of the current token.

  Totality: total
  Visibility: public export
cur : HasBytes s => s q -> Ref q ByteString
  The byte vector currently being processed.

  Totality: total
  Visibility: public export
offset : HasBytes s => s q -> Ref q Nat
  Absolute start position of the current token from the beginning
  of the whole byte stream processed so far.

  Totality: total
  Visibility: public export
relpos : HasBytes s => s q -> Ref q Integer
  Start position of the current token relative to `cur`.
  
  If this is negative, the current token will also include
  `prev`. Reference `len` will still hold the full length
  of the token.

  Totality: total
  Visibility: public export
len : HasBytes s => s q -> Ref q Nat
  Length of the current token

  Totality: total
  Visibility: public export
positions : HasBytes s => s q -> Ref q (SnocList BytePos)
  Stack of positions used to keep track of the positions of
  opening parentheses and brackets.

  Totality: total
  Visibility: public export
getBytes : HasBytes s => s q => F1 q ByteString
  Returns the current substring of the byte vector
  (corresponding to the position and length of the current
  token).
  
  The remainder of the previous bytestring is prefixed in case
  we are currently at position zero.

  Totality: total
  Visibility: export
record P1 : Type -> Type -> Type -> Type
  A parser is a system of automata, where each
  lexicographic token determines the next automaton
  state plus lexer to use.

  Totality: total
  Visibility: public export
  Constructor: 
P : Index states -> F1 q (state q) -> Lex1 q states state -> (state q -> F1 q (Maybe a)) -> Arr32 states (state q -> F1 q e) -> (Index states -> state q -> F1 q (Either e a)) -> HasBytes state => P1 q e a

  Projections:
  
.chunk : ({rec:0} : P1 q e a) -> state {rec:0} q -> F1 q (Maybe a)
  
.eoi : ({rec:0} : P1 q e a) -> Index (states {rec:0}) -> state {rec:0} q -> F1 q (Either e a)
  
.err : ({rec:0} : P1 q e a) -> Arr32 (states {rec:0}) (state {rec:0} q -> F1 q e)
  
.hasb : ({rec:0} : P1 q e a) -> HasBytes (state {rec:0})
  
.init : ({rec:0} : P1 q e a) -> Index (states {rec:0})
  
.lex : ({rec:0} : P1 q e a) -> Lex1 q (states {rec:0}) (state {rec:0})
  
0 .state : P1 q e a -> Type -> Type
  
.states : P1 q e a -> Bits32
  
.stck : ({rec:0} : P1 q e a) -> F1 q (state {rec:0} q)
.states : P1 q e a -> Bits32
  Totality: total
  Visibility: public export
states : P1 q e a -> Bits32
  Totality: total
  Visibility: public export
0 .state : P1 q e a -> Type -> Type
  Totality: total
  Visibility: public export
0 state : P1 q e a -> Type -> Type
  Totality: total
  Visibility: public export
.init : ({rec:0} : P1 q e a) -> Index (states {rec:0})
  Totality: total
  Visibility: public export
init : ({rec:0} : P1 q e a) -> Index (states {rec:0})
  Totality: total
  Visibility: public export
.stck : ({rec:0} : P1 q e a) -> F1 q (state {rec:0} q)
  Totality: total
  Visibility: public export
stck : ({rec:0} : P1 q e a) -> F1 q (state {rec:0} q)
  Totality: total
  Visibility: public export
.lex : ({rec:0} : P1 q e a) -> Lex1 q (states {rec:0}) (state {rec:0})
  Totality: total
  Visibility: public export
lex : ({rec:0} : P1 q e a) -> Lex1 q (states {rec:0}) (state {rec:0})
  Totality: total
  Visibility: public export
.chunk : ({rec:0} : P1 q e a) -> state {rec:0} q -> F1 q (Maybe a)
  Totality: total
  Visibility: public export
chunk : ({rec:0} : P1 q e a) -> state {rec:0} q -> F1 q (Maybe a)
  Totality: total
  Visibility: public export
.err : ({rec:0} : P1 q e a) -> Arr32 (states {rec:0}) (state {rec:0} q -> F1 q e)
  Totality: total
  Visibility: public export
err : ({rec:0} : P1 q e a) -> Arr32 (states {rec:0}) (state {rec:0} q -> F1 q e)
  Totality: total
  Visibility: public export
.eoi : ({rec:0} : P1 q e a) -> Index (states {rec:0}) -> state {rec:0} q -> F1 q (Either e a)
  Totality: total
  Visibility: public export
eoi : ({rec:0} : P1 q e a) -> Index (states {rec:0}) -> state {rec:0} q -> F1 q (Either e a)
  Totality: total
  Visibility: public export
.hasb : ({rec:0} : P1 q e a) -> HasBytes (state {rec:0})
  Totality: total
  Visibility: public export
hasb : ({rec:0} : P1 q e a) -> HasBytes (state {rec:0})
  Totality: total
  Visibility: public export
0 PST : P1 q e a -> Type
  Totality: total
  Visibility: public export
0 PIx : P1 q e a -> Type
  Totality: total
  Visibility: public export
0 PStep : P1 q e a -> Type
  Totality: total
  Visibility: public export
0 PRun : P1 q e a -> Type
  Totality: total
  Visibility: public export
0 PIgn : P1 q e a -> Type
  Totality: total
  Visibility: public export
0 PByteStep : Nat -> P1 q e a -> Type
  An array of arrays describing a lexer's state machine.

  Totality: total
  Visibility: public export
0 PStepper : Nat -> P1 q e a -> Type
  An array of arrays describing a lexer's state machine.

  Totality: total
  Visibility: public export
arrFail : (0 s : (Type -> Type)) -> Arr32 r (s q -> F1 q e) -> Index r -> s q -> F1 q (Either e x)
  Totality: total
  Visibility: export
fail : (p : P1 q e a) -> PIx p -> PST p -> F1 q (Either e x)
  Totality: total
  Visibility: export
0 Parser1 : Type -> Type -> Type
  Totality: total
  Visibility: public export
lex1 : List (Entry r (DFA q r s)) -> Lex1 q r s
  Totality: total
  Visibility: export