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.Bounds
import public Text.ParseError
import public Text.ILex.RExp
import public Text.ILex.Lexer
Definitions
interface HasBytes : (Type -> Type) -> Type
  An interface for mutable parser stacks `s` that allows
  the parse loop to register the byte string corresponding to
  the currently parsed token.

  Parameters: s
Constructor: 
MkHB

Methods:
  
bytes : s q -> Ref q ByteString

Implementation: 
HasBytes (DStack s e)
bytes : HasBytes s => s q -> Ref q ByteString
  Totality: total
  Visibility: public export
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 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 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
lastStep : (p : P1 q e a) -> PStep p -> PIx p -> PST p -> F1 q (Either e a)
  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