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
record LTENat : Nat -> Type
  Totality: total
  Visibility: public export
  Constructor: 
LN : (val : Nat) -> {auto 0 _ : LTE val n} -> LTENat n

  Projections:
  
0 .prf : ({rec:0} : LTENat n) -> LTE (val {rec:0}) n
  
.val : LTENat n -> Nat
.val : LTENat n -> Nat
  Totality: total
  Visibility: public export
val : LTENat n -> Nat
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : LTENat n) -> LTE (val {rec:0}) n
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : LTENat n) -> LTE (val {rec:0}) n
  Totality: total
  Visibility: public export
lteNat : (0 m : Nat) -> Ix m n => LTENat n
  Totality: total
  Visibility: export
first : (0 n : Nat) -> LTENat n
  Totality: total
  Visibility: export
last : (n : Nat) -> LTENat n
  Totality: total
  Visibility: export
bytesFromTill : IBuffer n -> LTENat n -> LTENat n -> ByteString
  Totality: total
  Visibility: export
stringFromTill : IBuffer n -> LTENat n -> LTENat n -> String
  Totality: total
  Visibility: 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:
  
copy : (size : Nat) -> Nat -> ByteString -> IBuffer size -> Ref q (LTENat size) -> Ref q (LTENat size) -> s q -> s q
  
bufSize : s q -> Nat
  
prev : s q -> ByteString
  Remainder of the previous bytestring that should
  be used as the beginning of the current token.
  
cur : (v : s q) -> IBuffer (bufSize v)
  The byte vector currently being processed.
  
prevOffset : s q -> Nat
  Absolute position of the first byte of `prev`.
  
curOffset : s q -> Nat
  Absolute position of the first byte of `cur`
  (this equals `prevOffset + prev.size` but should be
  provided as a separate field for reasons of efficiency)
  
from : (v : s q) -> Ref q (LTENat (bufSize v))
  Lower relative token bound (lower position in `cur`)
  
till : (v : s q) -> Ref q (LTENat (bufSize v))
  Next relative token bound (upser position + 1 in `cur`)
  
positions : s q -> Ref q (SnocList BytePos)
  Stack of positions used to keep track of the positions of
  opening parentheses and brackets.

Implementation: 
HasBytes (DState s e)
copy : HasBytes s => (size : Nat) -> Nat -> ByteString -> IBuffer size -> Ref q (LTENat size) -> Ref q (LTENat size) -> s q -> s q
  Totality: total
  Visibility: public export
bufSize : HasBytes s => s q -> Nat
  Totality: total
  Visibility: public export
prev : HasBytes s => s q -> ByteString
  Remainder of the previous bytestring that should
  be used as the beginning of the current token.

  Totality: total
  Visibility: public export
cur : {auto __con : HasBytes s} -> (v : s q) -> IBuffer (bufSize v)
  The byte vector currently being processed.

  Totality: total
  Visibility: public export
prevOffset : HasBytes s => s q -> Nat
  Absolute position of the first byte of `prev`.

  Totality: total
  Visibility: public export
curOffset : HasBytes s => s q -> Nat
  Absolute position of the first byte of `cur`
  (this equals `prevOffset + prev.size` but should be
  provided as a separate field for reasons of efficiency)

  Totality: total
  Visibility: public export
from : {auto __con : HasBytes s} -> (v : s q) -> Ref q (LTENat (bufSize v))
  Lower relative token bound (lower position in `cur`)

  Totality: total
  Visibility: public export
till : {auto __con : HasBytes s} -> (v : s q) -> Ref q (LTENat (bufSize v))
  Next relative token bound (upser position + 1 in `cur`)

  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
getString : HasBytes s => s q => F1 q String
  Totality: total
  Visibility: export
toFinalPos : HasBytes s => s q => F1' q
  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 -> ((size : Nat) -> IBuffer size -> 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) -> (size : Nat) -> IBuffer size -> 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) -> (size : Nat) -> IBuffer size -> F1 q (state {rec:0} q)
  Totality: total
  Visibility: public export
stck : ({rec:0} : P1 q e a) -> (size : Nat) -> IBuffer size -> 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 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
failFun1 : (p : P1 q e a) -> PIx p -> Fun1 q (p .state) (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