Text.ILex.Shunting

Definitions

data Assoc : Type

  Infix operator associativity

Totality: total
Visibility: public export
Constructors:

None : Assoc

InfixR : Assoc

InfixL : Assoc

Hints:

Eq Assoc

Interpolation Assoc

Ord Assoc

Show Assoc

data Precedence : Type

  Infix operator associativity and precedence

Totality: total
Visibility: public export
Constructors:

Prefix : Nat -> Precedence

Postfix : Nat -> Precedence

Infix : Nat -> Assoc -> Precedence

Hints:

Cast a Precedence => Cast (ByteBounded a) Precedence

Cast (Tok t p i o) Precedence

Eq Precedence

Interpolation Precedence

Show Precedence

toPrec : Cast o Precedence => o -> Precedence

Totality: total
Visibility: export

prec : Cast o Precedence => o -> Nat

Totality: total
Visibility: export

data ShuntingErr : Type -> Type

Totality: total
Visibility: public export
Constructor: 

AssocNone : o -> Precedence -> ShuntingErr o

Hints:

Eq {arg:12675} => Eq (ShuntingErr {arg:12675})

Interpolation o => Interpolation (ShuntingErr o)

Show {arg:12675} => Show (ShuntingErr {arg:12675})

data Tok : Type -> Type -> Type -> Type -> Type

  Shunting yard algorithm input token.
  A token is either a term followed by an infix operator
  or a single prefix operator

Totality: total
Visibility: public export
Constructors:

TPre : ByteBounded p -> Nat -> Tok t p i o

TInf : t -> ByteBounded i -> Nat -> Assoc -> Tok t p i o

TPst : ByteBounded o -> Nat -> Tok t p i o

Hints:

Cast (Tok t p i o) Precedence

Eq p => Eq t => Eq i => Eq o => Eq (Tok t p i o)

Show p => Show t => Show i => Show o => Show (Tok t p i o)

0 Toks : Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: public export

0 Skot : Type -> Type -> Type -> Type -> Type

Totality: total
Visibility: public export

shuntingYard : Cast (ShuntingErr i) e => (ByteBounded p -> t -> t) -> (t -> ByteBounded i -> t -> t) -> (ByteBounded o -> t -> t) -> Skot t p i o -> t -> Either (ByteBounded e) t

  An implementation of the
  [shunting yard algorithm](https://en.wikipedia.org/wiki/Shunting_yard_algorithm)
  used to convert term-operator chains such as `1 + 2 * 3 ^ 4` to proper
  syntax trees based on the operators' associativity and precedence.

Totality: total
Visibility: export