TyRE.Parser.SM

Definitions

data Instruction : SnocList Type -> SnocList Type -> Type

Totality: total
Visibility: public export
Constructors:

Push : x -> Instruction tps (tps :< x)

  Pushes chosen symbol on the stack

PushChar : Instruction tps (tps :< Char)

  Pushes currently consumed character on the stack

ReducePair : (x -> y -> z) -> Instruction ((tps :< x) :< y) (tps :< z)

  Reduces two last symbols from the stack accoring to the given funciton

Transform : (x -> y) -> Instruction (tps :< x) (tps :< y)

  Maps the top element of stack

EmitString : Instruction tps (tps :< String)

  Pushes collected string on the stack

Record : Instruction tps tps

  Raises record flag and starts collecting characters

liftInst : Instruction tps tps' -> Instruction (pcds ++ tps) (pcds ++ tps')

Totality: total
Visibility: public export

data RoutineSnoc : SnocList Type -> SnocList Type -> Type

Totality: total
Visibility: public export
Constructors:

Lin : RoutineSnoc tps tps

  Identity

(:<) : RoutineSnoc tps tps' -> Instruction tps' tps'' -> RoutineSnoc tps tps''

  Sequences routines

data Routine : SnocList Type -> SnocList Type -> Type

Totality: total
Visibility: public export
Constructors:

Nil : Routine tps tps

  Identity

(::) : Instruction tps tps' -> Routine tps' tps'' -> Routine tps tps''

  Sequences routines

(++) : RoutineSnoc tps tps' -> RoutineSnoc tps' tps'' -> RoutineSnoc tps tps''

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

lift : RoutineSnoc tps tps' -> RoutineSnoc (pcds ++ tps) (pcds ++ tps')

Totality: total
Visibility: public export

data EitherErased : Type -> Type -> Type

  Like Data.Either, but argument to `Right` variant is erased

Totality: total
Visibility: public export
Constructors:

Left : a -> EitherErased a b

Right : (0 _ : b) -> EitherErased a b

data IsInitInstruction : Instruction t t' -> Type

Totality: total
Visibility: public export
Constructors:

InitRecord : IsInitInstruction Record

InitPush : IsInitInstruction (Push elem)

InitReducePair : IsInitInstruction (ReducePair f)

InitTransform : IsInitInstruction (Transform f)

InitEmitString : IsInitInstruction EmitString

data IsInitRoutine : Routine t t' -> Type

Totality: total
Visibility: public export
Constructors:

Nil : IsInitRoutine []

(::) : IsInitInstruction x -> IsInitRoutine xs -> IsInitRoutine (x :: xs)

head : IsInitRoutine (x :: xs) -> IsInitInstruction x

Totality: total
Visibility: public export

tail : IsInitRoutine (x :: xs) -> IsInitRoutine xs

Totality: total
Visibility: public export

data IsInitRoutineSnoc : RoutineSnoc t t' -> Type

Totality: total
Visibility: public export
Constructors:

Lin : IsInitRoutineSnoc [<]

(:<) : IsInitRoutineSnoc xs -> IsInitInstruction x -> IsInitRoutineSnoc (xs :< x)

(++) : IsInitRoutineSnoc xs -> IsInitRoutineSnoc xs' -> IsInitRoutineSnoc (xs ++ xs')

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

reverse : IsInitRoutineSnoc sx -> IsInitRoutine (reverse sx)

Totality: total
Visibility: export

lift : IsInitRoutineSnoc xs -> IsInitRoutineSnoc (lift xs)

Totality: total
Visibility: public export

mlookup : (s -> SnocList Type) -> Type -> Maybe s -> SnocList Type

Totality: total
Visibility: public export

InitStatesType : Type -> (state : Type) -> (state -> SnocList Type) -> Type

Totality: total
Visibility: public export

TransitionRelation : Type -> (state : Type) -> (state -> SnocList Type) -> Type

Totality: total
Visibility: public export

record SM : Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkSM : (0 s : Type) -> (0 lookup : (s -> SnocList Type)) -> Eq s => InitStatesType t s lookup -> TransitionRelation t s lookup -> SM t

Projections:

.init : ({rec:0} : SM t) -> InitStatesType t (s {rec:0}) (lookup {rec:0})

.isEq : ({rec:0} : SM t) -> Eq (s {rec:0})

0 .lookup : ({rec:0} : SM t) -> s {rec:0} -> SnocList Type

.next : ({rec:0} : SM t) -> TransitionRelation t (s {rec:0}) (lookup {rec:0})

0 .s : SM t -> Type

0 .s : SM t -> Type

Totality: total
Visibility: public export

0 s : SM t -> Type

Totality: total
Visibility: public export

0 .lookup : ({rec:0} : SM t) -> s {rec:0} -> SnocList Type

Totality: total
Visibility: public export

0 lookup : ({rec:0} : SM t) -> s {rec:0} -> SnocList Type

Totality: total
Visibility: public export

.isEq : ({rec:0} : SM t) -> Eq (s {rec:0})

Totality: total
Visibility: public export

isEq : ({rec:0} : SM t) -> Eq (s {rec:0})

Totality: total
Visibility: public export

.init : ({rec:0} : SM t) -> InitStatesType t (s {rec:0}) (lookup {rec:0})

Totality: total
Visibility: public export

init : ({rec:0} : SM t) -> InitStatesType t (s {rec:0}) (lookup {rec:0})

Totality: total
Visibility: public export

.next : ({rec:0} : SM t) -> TransitionRelation t (s {rec:0}) (lookup {rec:0})

Totality: total
Visibility: public export

next : ({rec:0} : SM t) -> TransitionRelation t (s {rec:0}) (lookup {rec:0})

Totality: total
Visibility: public export

data Stack : SnocList Type -> Type

Totality: total
Visibility: public export
Constructors:

Lin : Stack [<]

(:<) : Stack tps -> t -> Stack (tps :< t)

runTillStrEnd : {auto sm : SM t} -> List Char -> List (Thread sm) -> Maybe t

  Run the state machine matching the whole string

Totality: total
Visibility: export

runTillFirstAccept : {auto sm : SM t} -> List Char -> List (Thread sm) -> (Maybe t, List Char)

  Run the state machine looking for a first matching prefix (non-greedy)

Totality: total
Visibility: export

runTillLastAccept : {auto sm : SM t} -> List Char -> Maybe (t, List Char) -> List (Thread sm) -> (Maybe t, List Char)

  Run the state machine looking for the last matching prefix (greedy)

Totality: total
Visibility: export

runTillFirstAccept : {auto sm : SM t} -> Stream Char -> List (Thread sm) -> (Maybe t, Stream Char)

  Run the state machine looking for a first matching prefix (non-greedy)
  re return also the leftover stream

Visibility: export

runTillLastAccept : {auto sm : SM t} -> Stream Char -> Maybe (t, Stream Char) -> List (Thread sm) -> (Maybe t, Stream Char)

  Run the state machine looking for the last matching prefix (greedy)

Visibility: export

runFromInit : {auto sm : SM t} -> (List (Thread sm) -> a) -> a

Totality: total
Visibility: export