Idris2Doc : Data.List.Suffix.Result0

Data.List.Suffix.Result0

(source)
Definitions
data Result0 : 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 an erased proof about the number of tokens
  consumed. Consider using `Data.List.Suffix.Result` if you need
  to keep track of the number of tokens consumed at runtime.
  
  Use this for manually writing high-performance parsers, which
  (in the case of strict results) are guaranteed to terminate.
  See module `Text.Parse.Manual` for
  utilities for consuming and converting prefixes
  of tokens, but for a nicer interface, consider using `Text.Parse.Core`
  (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:
  
Succ0 : a -> (xs : List t) -> {auto 0 _ : Suffix b xs ts} -> Result0 b t ts e a
  
Fail0 : e -> Result0 b t ts e a

  Hints:
  
FailParse (Result0 b t ts (Bounded (InnerError y))) y
  
Functor (Result0 b t ts e)
succ : a -> (0 _ : Suffix b xs ts) -> Result0 b t ts e a
  Alias for `Succ`, which takes the proof as an
  explicit argument

  Totality: total
  Visibility: public export
fromEither : (xs : List t) -> {auto 0 _ : Suffix b xs ts} -> Either e a -> Result0 b t ts e a
  Totality: total
  Visibility: public export
swapOr : Result0 (x || Delay y) t ts e a -> Result0 (y || Delay x) t ts e a
  Totality: total
  Visibility: public export
orSame : Result0 (x || Delay x) t ts e a -> Result0 x t ts e a
  Totality: total
  Visibility: public export
orTrue : Result0 (x || Delay True) t ts e a -> Result0 True t ts e a
  Totality: total
  Visibility: public export
orFalse : Result0 (x || Delay False) t ts e a -> Result0 x t ts e a
  Totality: total
  Visibility: public export
swapAnd : Result0 (x && Delay y) t ts e a -> Result0 (y && Delay x) t ts e a
  Totality: total
  Visibility: public export
andSame : Result0 (x && Delay x) t ts e a -> Result0 x t ts e a
  Totality: total
  Visibility: public export
andTrue : Result0 (x && Delay True) t ts e a -> Result0 x t ts e a
  Totality: total
  Visibility: public export
andFalse : Result0 (x && Delay False) t ts e a -> Result0 False t ts e a
  Totality: total
  Visibility: public export
weaken : Result0 x t ts e a -> Result0 False t ts e a
  Totality: total
  Visibility: public export
weakens : Result0 True t ts e a -> Result0 x t ts e a
  Totality: total
  Visibility: public export
and1 : Result0 x t ts e a -> Result0 (x && y) t ts e a
  Totality: total
  Visibility: public export
and2 : Result0 x t ts e a -> Result0 (y && Delay x) t ts e a
  Totality: total
  Visibility: public export
trans : Result0 b1 t xs e a -> (0 _ : Suffix b2 xs ys) -> Result0 (b1 || Delay b2) t ys e a
  Totality: total
  Visibility: public export
succT : Result0 b1 t xs e a -> {auto 0 _ : Suffix True xs ys} -> Result0 True t ys e a
  Totality: total
  Visibility: public export
succF : Result0 b1 t xs e a -> {auto 0 _ : Suffix True xs ys} -> Result0 False t ys e a
  Totality: total
  Visibility: public export
(<|>) : Result0 b1 t ts e a -> Lazy (Result0 b2 t ts e a) -> Result0 (b1 && Delay b2) t ts e a
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 2
run : ((ts : List t) -> Result0 True t ts e a) -> List t -> Either e (List a)
  Repeatedly consumes a strict prefix of a list of items
  until the whole list is consumed.
  
  This is provably total, due to the strictness of the consuming
  function.

  Totality: total
  Visibility: public export
runDropWhitespace : ((cs : List Char) -> Result0 True Char cs e a) -> List Char -> Either e (List a)
  Repeatedly consumes a strict prefix of a list of characters
  until the whole list is consumed. Drops all white space
  it encounters (unsing `Prelude.isSpace` to determine, what is
  a whitespace character).
  
  This is provably total, due to the strictness of the consuming
  function.

  Totality: total
  Visibility: public export
data TokError : Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
EOI : TokError t
  
ExpectedEOI : t -> TokError t
  
Unexpected : t -> TokError t

  Hints:
  
Eq {arg:18277} => Eq (TokError {arg:18277})
  
Interpolation t => Interpolation (TokError t)
  
Show {arg:18277} => Show (TokError {arg:18277})
0 AutoTok0 : Type -> Type -> Type -> Type
  A tokenizing function, which will consume additional characters
  from the input string. This can only be used if already some
  have been consumed.

  Totality: total
  Visibility: public export
0 SafeTok0 : Type -> Type -> Type
  A tokenizing function that cannot fail.

  Totality: total
  Visibility: public export
0 OntoTok0 : Type -> Type -> Type -> Type
  A tokenizing function, which will consume additional items
  from the input.

  Totality: total
  Visibility: public export
head : OntoTok0 t (TokError t) t
  Totality: total
  Visibility: public export
eoi : AutoTok0 t (TokError t) ()
  Totality: total
  Visibility: public export
takeOnto : SnocList t -> Nat -> AutoTok0 t (TokError t) (SnocList t)
  Totality: total
  Visibility: public export
take : Nat -> AutoTok0 t (TokError t) (SnocList t)
  Totality: total
  Visibility: public export
take1 : (n : Nat) -> {auto 0 _ : IsSucc n} -> OntoTok0 t (TokError t) (SnocList t)
  Totality: total
  Visibility: public export
takeWhileOnto : SnocList t -> (t -> Bool) -> SafeTok0 t (SnocList t)
  Totality: total
  Visibility: public export
takeWhile : (t -> Bool) -> SafeTok0 t (SnocList t)
  Totality: total
  Visibility: public export
takeWhile1 : (t -> Bool) -> OntoTok0 t (TokError t) (SnocList t)
  Totality: total
  Visibility: public export
takeUntil : (t -> Bool) -> SafeTok0 t (SnocList t)
  Totality: total
  Visibility: public export
takeUntil1 : (t -> Bool) -> OntoTok0 t (TokError t) (SnocList t)
  Totality: total
  Visibility: public export
takeWhileJustOnto : SnocList s -> (t -> Maybe s) -> SafeTok0 t (SnocList s)
  Totality: total
  Visibility: public export
takeWhileJust : (t -> Maybe s) -> SafeTok0 t (SnocList s)
  Totality: total
  Visibility: public export
takeWhileJust1 : (t -> Maybe s) -> OntoTok0 t (TokError t) (SnocList s)
  Totality: total
  Visibility: public export
accum : s -> (s -> t -> Maybe s) -> SafeTok0 t s
  Totality: total
  Visibility: public export
accum1 : s -> (s -> t -> Maybe s) -> OntoTok0 t (TokError t) s
  Totality: total
  Visibility: public export
data AccumRes : Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Done : AccumRes state err
  
Cont : state -> AccumRes state err
  
Error : err -> AccumRes state err
accumErr : s -> (s -> x) -> (s -> t -> AccumRes s e) -> AutoTok0 t e x
  Totality: total
  Visibility: public export
failInParen : Interpolation t => Bounds -> t -> Result0 b1 (Bounded t) ts (Bounded (InnerError e)) a -> Result0 b2 (Bounded t) ts (Bounded (InnerError e)) x
  General catch-all error generator when parsing within some kind
  of opening token: Will fail with an `Unclosed` error if at the
  end of input, or with an `Unknown` error wrapping the next token.
  Otherwise, will rethrow the current error.
  
  @ b   : Bounds of the opening paren or token
  @ tok : Opening paren or token
  @ res : Current parsing result

  Totality: total
  Visibility: public export
fail : Interpolation t => List (Bounded t) -> Result0 b (Bounded t) ts (Bounded (InnerError y)) a
  Catch-all error generator when no other rule applies.

  Totality: total
  Visibility: public export
result : Interpolation t => Origin -> String -> Result0 b (Bounded t) ts (Bounded (InnerError e)) a -> Either (ParseError e) a
  Totality: total
  Visibility: public export