Idris2Doc : Text.ILex.Internal.Types

Text.ILex.Internal.Types

(source)
Reexports
import public Text.ILex.RExp
import public Data.Linear.Ref1
Definitions
record NatMap1 : Type -> Type -> Type
  A mutable map from natural numbers to values (backed by a mutable array).
  
  Note: Since we might need to dynamically regrow the internal array,
        it has to be stored as a dependent pair in a mutable reference.

  Totality: total
  Visibility: export
  Constructor: 
NM1 : Ref s (n : Nat ** MArray s n (Maybe a)) -> NatMap1 s a

  Projection: 
.ref : NatMap1 s a -> Ref s (n : Nat ** MArray s n (Maybe a))
empty : {default 256 size : Nat} -> {auto 0 _ : IsSucc size} -> F1 s (NatMap1 s a)
  Totality: total
  Visibility: export
lookup1 : Nat -> NatMap1 s a -> F1 s (Maybe a)
  Totality: total
  Visibility: export
lookupDflt1 : Nat -> Lazy a -> NatMap1 s a -> F1 s a
  Totality: total
  Visibility: export
delete1 : Nat -> NatMap1 s a -> F1' s
  Totality: total
  Visibility: export
insert1 : Nat -> a -> NatMap1 s a -> F1' s
  Totality: total
  Visibility: export
fromList1 : List (Nat, a) -> F1 s (NatMap1 s a)
  Totality: total
  Visibility: export
pairs1 : NatMap1 s a -> F1 s (List (Nat, a))
  Totality: total
  Visibility: export
keys1 : NatMap1 s a -> F1 s (List Nat)
  Totality: total
  Visibility: export
values1 : NatMap1 s a -> F1 s (List a)
  Totality: total
  Visibility: export
connectedComponent : (a -> List Nat) -> Nat -> NatMap1 s a -> F1' s
  Totality: total
  Visibility: export
0 NSet : Type
  Totality: total
  Visibility: public export
sunion : NSet -> NSet -> NSet
  Totality: total
  Visibility: export
record Edge : Type
  A transformation pointing from one node to another

  Totality: total
  Visibility: public export
  Constructor: 
E : Range8 -> Nat -> Edge

  Projections:
  
.rule : Edge -> Range8
  The characters that triggers thi conversion
  
.tgt : Edge -> Nat
  The target of the given rule

  Hints:
  
Eq Edge
  
Show Edge
.rule : Edge -> Range8
  The characters that triggers thi conversion

  Totality: total
  Visibility: public export
rule : Edge -> Range8
  The characters that triggers thi conversion

  Totality: total
  Visibility: public export
.tgt : Edge -> Nat
  The target of the given rule

  Totality: total
  Visibility: public export
tgt : Edge -> Nat
  The target of the given rule

  Totality: total
  Visibility: public export
transitions : Edge -> List (Bits8, Nat)
  Totality: total
  Visibility: export
0 Edges : Type
  State transitions in a finite, discrete automaton

  Totality: total
  Visibility: public export
record ENode : Type
  Totality: total
  Visibility: public export
  Constructor: 
EN : List Nat -> List Nat -> Edges -> ENode

  Projections:
  
.acc : ENode -> List Nat
  
.eps : ENode -> List Nat
  
.out : ENode -> Edges

  Hint: 
Show ENode
.acc : ENode -> List Nat
  Totality: total
  Visibility: public export
acc : ENode -> List Nat
  Totality: total
  Visibility: public export
.eps : ENode -> List Nat
  Totality: total
  Visibility: public export
eps : ENode -> List Nat
  Totality: total
  Visibility: public export
.out : ENode -> Edges
  Totality: total
  Visibility: public export
out : ENode -> Edges
  Totality: total
  Visibility: public export
0 EGraph : Type -> Type
  Totality: total
  Visibility: public export
record NEdge : Type
  A transformation pointing from one node to a set
  of others

  Totality: total
  Visibility: public export
  Constructor: 
NE : Range8 -> NSet -> NEdge

  Projections:
  
.rule : NEdge -> Range8
  The characters that trigger this conversion
  
.tgts : NEdge -> NSet
  The list of targets of the given rule

  Hints:
  
Eq NEdge
  
Show NEdge
.rule : NEdge -> Range8
  The characters that trigger this conversion

  Totality: total
  Visibility: public export
rule : NEdge -> Range8
  The characters that trigger this conversion

  Totality: total
  Visibility: public export
.tgts : NEdge -> NSet
  The list of targets of the given rule

  Totality: total
  Visibility: public export
tgts : NEdge -> NSet
  The list of targets of the given rule

  Totality: total
  Visibility: public export
0 NEdges : Type
  State transitions in a finite, non-discrete automaton

  Totality: total
  Visibility: public export
record NNode : Type
  Totality: total
  Visibility: public export
  Constructor: 
NN : Nat -> List Nat -> NEdges -> NNode

  Projections:
  
.acc : NNode -> List Nat
  
.out : NNode -> NEdges
  
.pos : NNode -> Nat

  Hint: 
Show NNode
.pos : NNode -> Nat
  Totality: total
  Visibility: public export
pos : NNode -> Nat
  Totality: total
  Visibility: public export
.acc : NNode -> List Nat
  Totality: total
  Visibility: public export
acc : NNode -> List Nat
  Totality: total
  Visibility: public export
.out : NNode -> NEdges
  Totality: total
  Visibility: public export
out : NNode -> NEdges
  Totality: total
  Visibility: public export
nchildren : NNode -> List Nat
  Totality: total
  Visibility: export
0 NGraph : Type -> Type
  Totality: total
  Visibility: public export
record Node : Type
  Totality: total
  Visibility: public export
  Constructor: 
N : Nat -> List Nat -> Edges -> Node

  Projections:
  
.acc : Node -> List Nat
  
.out : Node -> Edges
  
.pos : Node -> Nat

  Hint: 
Show Node
.pos : Node -> Nat
  Totality: total
  Visibility: public export
pos : Node -> Nat
  Totality: total
  Visibility: public export
.acc : Node -> List Nat
  Totality: total
  Visibility: public export
acc : Node -> List Nat
  Totality: total
  Visibility: public export
.out : Node -> Edges
  Totality: total
  Visibility: public export
out : Node -> Edges
  Totality: total
  Visibility: public export
children : Node -> List Nat
  Totality: total
  Visibility: export
0 Graph : Type -> Type
  Totality: total
  Visibility: public export
record DFAState : Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
ST : NatMap1 s a -> Ref s (SortedMap NSet Nat) -> EGraph s -> NGraph s -> Graph s -> Ref s Nat -> DFAState s a

  Projections:
  
.accs : DFAState s a -> NatMap1 s a
  
.cur : DFAState s a -> Ref s Nat
  
.egraph : DFAState s a -> EGraph s
  
.graph : DFAState s a -> Graph s
  
.ngraph : DFAState s a -> NGraph s
  
.sets : DFAState s a -> Ref s (SortedMap NSet Nat)
.accs : DFAState s a -> NatMap1 s a
  Totality: total
  Visibility: public export
accs : DFAState s a -> NatMap1 s a
  Totality: total
  Visibility: public export
.sets : DFAState s a -> Ref s (SortedMap NSet Nat)
  Totality: total
  Visibility: public export
sets : DFAState s a -> Ref s (SortedMap NSet Nat)
  Totality: total
  Visibility: public export
.egraph : DFAState s a -> EGraph s
  Totality: total
  Visibility: public export
egraph : DFAState s a -> EGraph s
  Totality: total
  Visibility: public export
.ngraph : DFAState s a -> NGraph s
  Totality: total
  Visibility: public export
ngraph : DFAState s a -> NGraph s
  Totality: total
  Visibility: public export
.graph : DFAState s a -> Graph s
  Totality: total
  Visibility: public export
graph : DFAState s a -> Graph s
  Totality: total
  Visibility: public export
.cur : DFAState s a -> Ref s Nat
  Totality: total
  Visibility: public export
cur : DFAState s a -> Ref s Nat
  Totality: total
  Visibility: public export
init : F1 s (DFAState s a)
  Totality: total
  Visibility: export
inc : DFAState s a => F1 s Nat
  Totality: total
  Visibility: export
addSet : DFAState s a => NSet -> F1 s Nat
  Totality: total
  Visibility: export
lookupSet : DFAState s a => NSet -> F1 s (Maybe Nat)
  Totality: total
  Visibility: export
insertENode : DFAState s a => Nat -> ENode -> F1 s Nat
  Totality: total
  Visibility: export
insertTerminal : DFAState s a => (Nat, (t, a)) -> F1' s
  Totality: total
  Visibility: export
createENode : DFAState s a => ENode -> F1 s Nat
  Totality: total
  Visibility: export
lookupENode : DFAState s a => Nat -> F1 s (Maybe ENode)
  Totality: total
  Visibility: export
getENode : DFAState s a => Nat -> F1 s ENode
  Totality: total
  Visibility: export
insertNNode : DFAState s a => Nat -> NNode -> F1' s
  Totality: total
  Visibility: export
lookupNNode : DFAState s a => Nat -> F1 s (Maybe NNode)
  Totality: total
  Visibility: export
getNNode : DFAState s a => Nat -> F1 s NNode
  Totality: total
  Visibility: export
insertNode : DFAState s a => Nat -> Node -> F1' s
  Totality: total
  Visibility: export
lookupNode : DFAState s a => Nat -> F1 s (Maybe Node)
  Totality: total
  Visibility: export
getNode : DFAState s a => Nat -> F1 s Node
  Totality: total
  Visibility: export
evalST : DFAState s a => (DFAState s a => F1 s b) -> b
  Totality: total
  Visibility: export
normalizeGraph : DFAState s a => F1' s
  Totality: total
  Visibility: export
record Machine : Type -> Type -> Type
  A finite state machine with terminal states and
  a graph representation for the state transitions.
  
  State 0 is the initial state.

  Totality: total
  Visibility: public export
  Constructor: 
M : SortedMap Nat a -> b -> Machine a b

  Projections:
  
.graph : Machine a b -> b
  
.terminals : Machine a b -> SortedMap Nat a
.terminals : Machine a b -> SortedMap Nat a
  Totality: total
  Visibility: public export
terminals : Machine a b -> SortedMap Nat a
  Totality: total
  Visibility: public export
.graph : Machine a b -> b
  Totality: total
  Visibility: public export
graph : Machine a b -> b
  Totality: total
  Visibility: public export
machine : (DFAState s a => F1 s b) -> Machine a b
  Evaluate a state normalizer and return the resulting
  machine.

  Totality: total
  Visibility: export