Idris2Doc : Text.ILex.Lexer

Text.ILex.Lexer

(source)
Reexports
import public Data.Array
import public Data.List
import public Data.Prim.Bits32
import public Text.ILex.RExp
Definitions
record Index : Bits32 -> Type
  Totality: total
  Visibility: public export
  Constructor: 
I : (val : Bits32) -> {auto 0 _ : val < n} -> Index n

  Projections:
  
0 .prf : ({rec:0} : Index n) -> val {rec:0} < n
  
.val : Index n -> Bits32

  Hints:
  
Eq (Index n)
  
Ord (Index n)
  
Show (Index n)
.val : Index n -> Bits32
  Totality: total
  Visibility: public export
val : Index n -> Bits32
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : Index n) -> val {rec:0} < n
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : Index n) -> val {rec:0} < n
  Totality: total
  Visibility: public export
toIndex : Bits32 -> Maybe (Index r)
  Totality: total
  Visibility: export
fromInteger : (n : Integer) -> {auto 0 _ : cast n < r} -> Index r
  Totality: total
  Visibility: public export
Ini : {auto 0 _ : 0 < n} -> Index n
  Totality: total
  Visibility: public export
0 Step1 : Type -> Bits32 -> (Type -> Type) -> Type
  Totality: total
  Visibility: public export
toState : Index r -> Step1 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 : Step1 q r s -> Transition n q r s
  
DoneBS : Step1 q r s -> Transition n q r s
  
Move : Fin (S n) -> Step1 q r s -> 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
data Step : Type -> Bits32 -> (Type -> Type) -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Go : Step1 q r s -> Step q r s
  
Rd : Step1 q r s -> Step q r s
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