Idris2Doc : Text.ILex.RExp

Text.ILex.RExp

(source)
Reexports
import public Text.ILex.Char.Set
Definitions
data RExpOf : Bool -> Type -> Type
  A data type for regular expressions.
  
  The `Bool` flag indicates, if the regular expression consumes
  at least one character of input or not.

  Totality: total
  Visibility: public export
  Constructors:
  
Eps : RExpOf False t
  
Ch : SetOf t -> RExpOf True t
  
And : RExpOf b1 t -> RExpOf b2 t -> RExpOf (b1 || Delay b2) t
  
Or : RExpOf b1 t -> RExpOf b2 t -> RExpOf (b1 && Delay b2) t
  
Star : RExpOf True t -> RExpOf False t

  Hint: 
Show {arg:12279} => Show (RExpOf {arg:12276} {arg:12279})
0 RExp : Bool -> Type
  Totality: total
  Visibility: public export
0 RExp8 : Bool -> Type
  Totality: total
  Visibility: public export
data IsCh : RExpOf b t -> Type
  Totality: total
  Visibility: public export
  Constructor: 
ItIsCh : IsCh (Ch s)
adjRanges : (SetOf t -> RExpOf True s) -> RExpOf b t -> RExpOf b s
  Totality: total
  Visibility: export
0 TokenMap : Type -> Type
  Totality: total
  Visibility: public export
0 TokenMap8 : Type -> Type
  Totality: total
  Visibility: public export
orF : RExpOf (b || Delay False) t -> RExpOf b t
  Totality: total
  Visibility: public export
orT : RExpOf (b || Delay True) t -> RExpOf True t
  Totality: total
  Visibility: public export
toOrF : RExpOf b t -> RExpOf (b || Delay False) t
  Totality: total
  Visibility: public export
chr : Char -> RExp True
  Accepts the given single character

  Totality: total
  Visibility: public export
fromChar : Char -> RExp True
  Totality: total
  Visibility: public export
charLike : Char -> RExp True
  Case insensitive version of `chr`.

  Totality: total
  Visibility: public export
not : WithBounds t => Neg t => (r : RExpOf b t) -> {auto 0 _ : IsCh r} -> RExpOf True t
  Totality: total
  Visibility: public export
(&&) : WithBounds t => Neg t => (x : RExpOf b t) -> (y : RExpOf b t) -> {auto 0 _ : IsCh x} -> {auto 0 _ : IsCh y} -> RExpOf True t
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 5
(||) : WithBounds t => Neg t => (x : RExpOf b t) -> (y : RExpOf b t) -> {auto 0 _ : IsCh x} -> {auto 0 _ : IsCh y} -> RExpOf True t
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 4
(<|>) : WithBounds t => Neg t => RExpOf b1 t -> RExpOf b2 t -> RExpOf (b1 && Delay b2) t
  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 2
oneof : WithBounds t => Neg t => (rs : List (RExpOf True t)) -> {auto 0 _ : NonEmpty rs} -> RExpOf True t
  Totality: total
  Visibility: public export
(>>) : RExpOf b1 t -> RExpOf b2 t -> RExpOf (b1 || Delay b2) t
  Totality: total
  Visibility: public export
  Fixity Declaration: infixl operator, level 1
eps : RExpOf False t
  Totality: total
  Visibility: public export
opt : RExpOf True t -> RExpOf False t
  Totality: total
  Visibility: public export
chars : (cs : List Char) -> {auto 0 _ : NonEmpty cs} -> RExp True
  Exactly matches the given sequence of characters

  Totality: total
  Visibility: public export
charsLike : (cs : List Char) -> {auto 0 _ : NonEmpty cs} -> RExp True
  Case-insensitive version of `chars`

  Totality: total
  Visibility: public export
str : (s : String) -> {auto 0 _ : NonEmpty (unpack s)} -> RExp True
  Exactly matches the given string.

  Totality: total
  Visibility: public export
fromString : (s : String) -> {auto 0 _ : NonEmpty (unpack s)} -> RExp True
  Utility for using string literals with regular expressions.

  Totality: total
  Visibility: public export
like : (s : String) -> {auto 0 _ : NonEmpty (unpack s)} -> RExp True
  Case-insensitive version of `str`

  Totality: total
  Visibility: public export
pre : (s : String) -> {auto 0 _ : NonEmpty (unpack s)} -> RExp b -> RExp True
  Totality: total
  Visibility: public export
star : RExpOf True t -> RExpOf False t
  Totality: total
  Visibility: public export
plus : RExpOf True t -> RExpOf True t
  Totality: total
  Visibility: public export
sep1 : RExpOf True t -> RExpOf True t -> RExpOf True t
  Totality: total
  Visibility: public export
sep : RExpOf True t -> RExpOf True t -> RExpOf False t
  Totality: total
  Visibility: public export
rep : Nat -> Bool
  Totality: total
  Visibility: public export
repeat : (n : Nat) -> RExpOf True t -> RExpOf (rep n) t
  Repeats the given expression exactly `n` times

  Totality: total
  Visibility: export
atmost : Nat -> RExpOf True t -> RExpOf False t
  Repeats the given expression exactly at most `n` times

  Totality: total
  Visibility: export
repeatRange : (m : Nat) -> Nat -> RExpOf True t -> RExpOf (rep m) t
  Repeats the given expression between `m` and `n`  times

  Totality: total
  Visibility: export
atleast : (n : Nat) -> RExpOf True t -> RExpOf (rep n) t
  Repeats the given expression at least `n` times

  Totality: total
  Visibility: export
nl : RExp True
  Accepts only the newline character

  Totality: total
  Visibility: public export
range32 : Bits32 -> Bits32 -> RExp True
  Accepts any character in the given range of unicode
  code points.
  
  Please note that even if the given range exceeds the given
  set of valid codepoints (0x000 - 0xD7FF || 0xE000 - 0x10FFFF),
  it will be intersected with the valid set during generation
  of the state machine.

  Totality: total
  Visibility: public export
range : Char -> Char -> RExp True
  Accepts any character in the given range

  Totality: total
  Visibility: public export
digit : RExp True
  Accepts any character in the given range

  Totality: total
  Visibility: public export
posdigit : RExp True
  Totality: total
  Visibility: public export
upper : RExp True
  Accepts any upper case character

  Totality: total
  Visibility: public export
lower : RExp True
  Accepts any lower case character

  Totality: total
  Visibility: public export
alpha : RExp True
  Accepts any alphabetic character

  Totality: total
  Visibility: public export
alphaNum : RExp True
  Accepts any alpha-numeric character

  Totality: total
  Visibility: public export
bindigit : RExp True
  Accepts a binary digit ('0' or '1').

  Totality: total
  Visibility: public export
octdigit : RExp True
  Accepts an octal digit.

  Totality: total
  Visibility: public export
hexdigit : RExp True
  Accepts a hexadecimal digit.
  
  Letters can be upper or lower case.

  Totality: total
  Visibility: public export
control : RExp True
  Accepts a single unicode control codepoint.
  
  Control characters are unicode codepoints in the ranges
  0x00 to 0x1f (`'\NUL'` to `'\US'`) and
  0x71 to 0x9f (`'\DEL'` to `'\159'`).
  
  Among these, the most commonly used are tab (`'\t'`, 0x09),
  line feed (`'\r'`, 0x0d) and carriage return (`'\n'`, 0x0a).

  Totality: total
  Visibility: public export
dot : RExp True
  Accepts a non-control unicode codepoint.

  Totality: total
  Visibility: public export
dots : RExp False
  Accepts an arbitrary number of printable unicode codepoints.

  Totality: total
  Visibility: public export
dots1 : RExp True
  Accepts a non-empty number of printable unicode codepoints.

  Totality: total
  Visibility: public export
binary : RExp True
  Recognizes a non-empty string of binary digits.

  Totality: total
  Visibility: public export
octal : RExp True
  Recognizes a non-empty string of octal digits.

  Totality: total
  Visibility: public export
decimal : RExp True
  Recognizes a non-empty string of decimal digits.
  
  In this case, no leading zeroes are allowed: "0" is recognized
  but "01" is not.

  Totality: total
  Visibility: public export
hexadecimal : RExp True
  Recognizes a non-empty string of hexadecimal digits.
  
  Letters can be upper or lower case.

  Totality: total
  Visibility: public export
integer : RExp True
  Accepts a decimal number (like `decimal`: no leading zeroes)
  prefixed with an optional "minus" sign.

  Totality: total
  Visibility: public export
natural : RExp True
  Accepts a natural number in binary, octal, decimal (no leading zeroes),
  or hexadecimal form.
  
  Non-decimal forms must be prefixed with "0b" (binary), "0o" (octal), or
  "0x" (hexadecimal), just like in Idris.

  Totality: total
  Visibility: public export
data ConstSize : Nat -> RExpOf b t -> Type
  Proof that regular expression `x` consists of a constant number
  (`n`) of characters.

  Totality: total
  Visibility: public export
  Constructors:
  
CS0 : ConstSize 0 Eps
  The epsilon expression trivially matches zero characters.
  
CSC : ConstSize 1 (Ch x)
  A single character trivially matches one character.
  
CSAnd : ConstSize m x -> ConstSize n y -> ConstSize (m + n) (And x y)
  Sequencing two constant size expressions of `m` and `n` characters
  yields an expression matching `m+n` characters.
  
CSOr : ConstSize n x -> ConstSize n y -> ConstSize n (Or x y)
  A choice of constant size expressions all matching the same number of
  characters yields again an expression matching the same number of
  characters.
constSize : (x : RExpOf b t) -> Maybe (Subset Nat (\{arg:0} => ConstSize {arg:0} x))
  Decides if the given expression matches a constant number of
  characters.

  Totality: total
  Visibility: export
0 charsConstSize : (cs : List Char) -> {auto 0 prf : NonEmpty cs} -> ConstSize (length cs) (chars cs)
  Proof that the `chars cs` combinator returns an expression
  that matches a constant number of `length cs` characters.

  Totality: total
  Visibility: export