Data.List.Suffix.Result

Reexports

Definitions

data Result : Bool -> (t : Type) -> List t -> Type -> Type -> Type

  Result of consuming and converting a (possibly strict) prefix
  of a list of tokens.
  
  This comes with a non-erased proof about the number of tokens
  consumed, which can be used to for instance 
  calculate the bounds of a lexeme. Likewise, the error specifies
  a start and end suffix for calculating proper bounds in case
  of an error.
  
  Use this for writing simple, high-performance tokenizers, which
  (in the case of strict results) are guaranteed to terminate.
  See module `Text.Lex.Manual` for
  utilities for consuming and converting prefixes
  of tokens, but for a nicer interface, consider using `Text.Lex.Tokenizer`
  (at the cost of a drop in performance).
  
  @ strict : True if a strict prefix of the list of tokens has
             been consumed.
  @ t      : the type of token consumed.
  @ ts     : the original list of tokens
  @ e      : the error type in case of a failure
  @ a      : the result type

Totality: total
Visibility: public export
Constructors:

Succ : a -> (xs : List t) -> Suffix b xs ts => Result b t ts e a

Fail : Suffix False stopStart ts -> (0 errEnd : List t) -> Suffix False errEnd stopStart => e -> Result b t ts e a

Hint: 

Functor (Result b t ts e)

succ : a -> Suffix b xs ts -> Result b t ts e a

  Alias for `Succ`, which takes the proof as an
  explicit argument

Totality: total
Visibility: public export

swapOr : Result (x || Delay y) t ts e a -> Result (y || Delay x) t ts e a

Totality: total
Visibility: public export

orSame : Result (x || Delay x) t ts e a -> Result x t ts e a

Totality: total
Visibility: public export

orTrue : Result (x || Delay True) t ts e a -> Result True t ts e a

Totality: total
Visibility: public export

orFalse : Result (x || Delay False) t ts e a -> Result x t ts e a

Totality: total
Visibility: public export

swapAnd : Result (x && Delay y) t ts e a -> Result (y && Delay x) t ts e a

Totality: total
Visibility: public export

andSame : Result (x && Delay x) t ts e a -> Result x t ts e a

Totality: total
Visibility: public export

andTrue : Result (x && Delay True) t ts e a -> Result x t ts e a

Totality: total
Visibility: public export

andFalse : Result (x && Delay False) t ts e a -> Result False t ts e a

Totality: total
Visibility: public export

weaken : Result x t ts e a -> Result False t ts e a

Totality: total
Visibility: public export

weakens : Result True t ts e a -> Result x t ts e a

Totality: total
Visibility: public export

and1 : Result x t ts e a -> Result (x && y) t ts e a

Totality: total
Visibility: public export

and2 : Result x t ts e a -> Result (y && Delay x) t ts e a

Totality: total
Visibility: public export

trans : Result b1 t xs e a -> Suffix b2 xs ys -> Result (b1 || Delay b2) t ys e a

Totality: total
Visibility: public export

succT : Result b1 t xs e a -> Suffix True xs ys => Result True t ys e a

Totality: total
Visibility: public export

succF : Result b1 t xs e a -> Suffix True xs ys => Result False t ys e a

Totality: total
Visibility: public export