Idris2Doc : Text.Lex.Shift

Text.Lex.Shift

(source)
Reexports
import public Text.Lex.Manual
import public Data.List.Shift
Definitions
shift : Position -> Shift b t sx xs sy ys -> Position
  Shift the position by a number of columns represented by
  a `Shift` value. This assumes, that no line break was "shifted".

  Totality: total
  Visibility: public export
data ShiftRes : Bool -> SnocList Char -> List Char -> Type
  Result of running a lexer once: The lexer either stops, when
  it can no longer consume any characters, or it shifts some characters
  from the head of the list of remaining characters to the tail of the
  snoclist of already recognised characters.
  
  @ st     : the initial snoclist of already recognised characters
  @ ts     : the initial list of remaining characters

  Totality: total
  Visibility: public export
  Constructors:
  
Succ : (post : List Char) -> Shift b Char pre post st ts => ShiftRes b st ts
  
Stop : Shift False Char se errStart st ts -> (0 errEnd : List Char) -> Shift False Char ee errEnd se errStart => InnerError Void -> ShiftRes b st ts
suffix : (SnocList Char -> a) -> ShiftRes True [<] cs -> LexRes True cs e a
  Totality: total
  Visibility: public export
swapOr : ShiftRes (x || Delay y) st ts -> ShiftRes (y || Delay x) st ts
  Totality: total
  Visibility: public export
orSame : ShiftRes (x || Delay x) st ts -> ShiftRes x st ts
  Totality: total
  Visibility: public export
orTrue : ShiftRes (x || Delay True) st ts -> ShiftRes True st ts
  Totality: total
  Visibility: public export
orFalse : ShiftRes (x || Delay False) st ts -> ShiftRes x st ts
  Totality: total
  Visibility: public export
swapAnd : ShiftRes (x && Delay y) st ts -> ShiftRes (y && Delay x) st ts
  Totality: total
  Visibility: public export
andSame : ShiftRes (x && Delay x) st ts -> ShiftRes x st ts
  Totality: total
  Visibility: public export
andTrue : ShiftRes (x && Delay True) st ts -> ShiftRes x st ts
  Totality: total
  Visibility: public export
andFalse : ShiftRes (x && Delay False) st ts -> ShiftRes False st ts
  Totality: total
  Visibility: public export
weaken : ShiftRes x st ts -> ShiftRes False st ts
  Totality: total
  Visibility: public export
weakens : ShiftRes True st ts -> ShiftRes x st ts
  Totality: total
  Visibility: public export
and1 : ShiftRes x st ts -> ShiftRes (x && y) st ts
  Totality: total
  Visibility: public export
and2 : ShiftRes x st ts -> ShiftRes (y && Delay x) st ts
  Totality: total
  Visibility: public export
trans : ShiftRes b1 sx xs -> Shift b2 Char sx xs sy ys -> ShiftRes (b1 || Delay b2) sy ys
  Totality: total
  Visibility: public export
(<|>) : ShiftRes b1 sx xs -> Lazy (ShiftRes b2 sx xs) -> ShiftRes (b1 && Delay b2) sx xs
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 2
0 Shifter : Bool -> Type
  A `Shifter` is a function that moves items from the head of a list
  to the tail of a snoclist.
  
  A lexer is just a fancy wrapper around a `Shifter`, and *running* a
  lexer (via function `run`) leads to the underlying `Shifter`
  (see `Text.Lex.Core`).

  Totality: total
  Visibility: public export
0 AutoShift : Bool -> Type
  Totality: total
  Visibility: public export
range : InnerError Void -> Shift b1 Char ruc cur giro orig -> (0 rest : List Char) -> Shift False Char tser rest ruc cur => ShiftRes b2 giro orig
  Totality: total
  Visibility: public export
invalidEscape : Shift b1 Char ruc cur giro orig -> (0 rest : List Char) -> Shift False Char tser rest ruc cur => ShiftRes b2 giro orig
  Totality: total
  Visibility: public export
unknownRange : Shift b1 Char ruc cur giro orig -> (0 rest : List Char) -> Shift False Char tser rest ruc cur => ShiftRes b2 giro orig
  Totality: total
  Visibility: public export
single : InnerError Void -> Shift b Char ruc (c :: errEnd) giro orig -> ShiftRes bres giro orig
  Totality: total
  Visibility: public export
unknown : Shift b Char ruc (c :: errEnd) giro orig -> ShiftRes bres giro orig
  Totality: total
  Visibility: public export
failCharClass : CharClass -> Shift b Char ruc (c :: errEnd) giro orig -> ShiftRes bres giro orig
  Totality: total
  Visibility: public export
failDigit : DigitType -> Shift b Char ruc (c :: errEnd) giro orig -> ShiftRes bres giro orig
  Totality: total
  Visibility: public export
eoiAt : Shift b1 Char ruc [] giro orig -> ShiftRes b2 giro orig
  Totality: total
  Visibility: public export
eoi : Shifter False
  Shifter that recognises the empty String

  Totality: total
  Visibility: public export
fail : Shifter True
  Shifter that always fails

  Totality: total
  Visibility: public export
one : (Char -> Bool) -> AutoShift True
  A shifter that moves exactly one value, if
  it fulfills the given predicate.

  Totality: total
  Visibility: public export
takeWhile : (Char -> Bool) -> AutoShift False
  A shifter that moves items while the given predicate returns
  `True`

  Totality: total
  Visibility: public export
takeWhile1 : (Char -> Bool) -> AutoShift True
  A strict version of `takeWhile`, which moves at least one item.

  Totality: total
  Visibility: public export
takeUntil : (Char -> Bool) -> AutoShift False
  A shifter that moves items while the give predicate returns
  `False`

  Totality: total
  Visibility: public export
takeUntil1 : (Char -> Bool) -> AutoShift True
  A strict version of `takeUntil`, which moves at least one item.

  Totality: total
  Visibility: public export
digits : AutoShift False
  A shifter that moves digits.

  Totality: total
  Visibility: public export
digits1 : AutoShift True
  A strict version of `digits`.

  Totality: total
  Visibility: public export
int : AutoShift True
  A shifter that moves an integer prefix

  Totality: total
  Visibility: public export
intPlus : AutoShift True
  Like `int` but also allows an optional leading `'+'` character.

  Totality: total
  Visibility: public export
number : Shifter True
  A shifter for recognizing JSON numbers

  Totality: total
  Visibility: public export
double : Tok True e Double
  Totality: total
  Visibility: public export
take : (n : Nat) -> {auto 0 _ : IsSucc n} -> AutoShift True
  Totality: total
  Visibility: public export
tail : AutoShift True
  Totality: total
  Visibility: public export
exact : (ts : List Char) -> {auto 0 _ : NonEmpty ts} -> AutoShift True
  Totality: total
  Visibility: public export
string : Shifter True
  Totality: total
  Visibility: public export