Idris2Doc : Text.ILex.Lexer

Text.ILex.Lexer

(source)
Reexports
import public Data.Array
import public Data.Enum
import public Data.List
import public Data.Prim.Bits32
import public Text.ILex.RExp
Definitions
record Env : Type -> (Type -> Type) -> Type
  Totality: total
  Visibility: public export
  Constructor: 
E : s q -> (1 _ : T1 q) -> Env q s

  Projections:
  
.state : Env q s -> s q
  
.tok : Env q s -> T1 q
.state : Env q s -> s q
  Totality: total
  Visibility: public export
state : Env q s -> s q
  Totality: total
  Visibility: public export
.tok : Env q s -> T1 q
  Totality: total
  Visibility: public export
tok : Env q s -> T1 q
  Totality: total
  Visibility: public export
0 Step1 : Type -> Bits32 -> (Type -> Type) -> Type
  Totality: total
  Visibility: public export
0 Fun1 : Type -> (Type -> Type) -> Type -> Type
  Totality: total
  Visibility: public export
0 Run1 : Type -> Bits32 -> (Type -> Type) -> Type
  Totality: total
  Visibility: public export
data Step : Type -> Bits32 -> (Type -> Type) -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Run : Run1 q r s -> Step q r s
  
Ign : Step q r s
  
Err : Step q r s
toState : Index r -> Step q r s
  Totality: total
  Visibility: export
data Transition : Nat -> Type -> Bits32 -> (Type -> Type) -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Keep : Transition n q r s
  
Done : Run1 q r s -> Transition n q r s
  
Ignore : Transition n q r s
  
Move : Fin (S n) -> Run1 q r s -> Transition n q r s
  
MoveI : Fin (S n) -> Transition n q r s
  
MoveE : Fin (S n) -> Transition n q r s
  
Bottom : Transition n q r s
0 ByteStep : Nat -> Type -> Bits32 -> (Type -> Type) -> Type
  An array of arrays describing a lexer's state machine.

  Totality: total
  Visibility: public export
0 Stepper : Nat -> Type -> Bits32 -> (Type -> Type) -> Type
  An array of arrays describing a lexer's state machine.

  Totality: total
  Visibility: public export
record DFA : Type -> Bits32 -> (Type -> Type) -> Type
  A discrete finite automaton (DFA) encoded as
  an array of state transitions plus an array
  describing the terminal token states.

  Totality: total
  Visibility: public export
  Constructor: 
L : (states : Nat) -> Stepper states q r s -> DFA q r s

  Projections:
  
.next : ({rec:0} : DFA q r s) -> Stepper (states {rec:0}) q r s
  State transitions matrix.
  
  If `cur` is the current state (encoded as a `Fin (S states)`
  and `b` is the current input byte, the next state is determined
  by `next[cur][b]` (in pseudo C-syntax).
  
.states : DFA q r s -> Nat
  Number of non-zero states in the automaton.
.states : DFA q r s -> Nat
  Number of non-zero states in the automaton.

  Totality: total
  Visibility: public export
states : DFA q r s -> Nat
  Number of non-zero states in the automaton.

  Totality: total
  Visibility: public export
.next : ({rec:0} : DFA q r s) -> Stepper (states {rec:0}) q r s
  State transitions matrix.
  
  If `cur` is the current state (encoded as a `Fin (S states)`
  and `b` is the current input byte, the next state is determined
  by `next[cur][b]` (in pseudo C-syntax).

  Totality: total
  Visibility: public export
next : ({rec:0} : DFA q r s) -> Stepper (states {rec:0}) q r s
  State transitions matrix.
  
  If `cur` is the current state (encoded as a `Fin (S states)`
  and `b` is the current input byte, the next state is determined
  by `next[cur][b]` (in pseudo C-syntax).

  Totality: total
  Visibility: public export
0 Steps : Type -> Bits32 -> (Type -> Type) -> Type
  Totality: total
  Visibility: public export
byteDFA : TokenMap8 (Step q r s) -> DFA q r s
  A DFA operating on raw bytes.

  Totality: total
  Visibility: export
dfa : Steps q r s -> DFA q r s
  A utf-8 aware DFA operating on text.

  Totality: total
  Visibility: export