Text.Regex.Interface

Reexports

Definitions

data EdgeSide : Type

Totality: total
Visibility: public export
Constructors:

Start : EdgeSide

End : EdgeSide

Hint: 

Show EdgeSide

data LineMode : Type

  `Line` line mode means "depends on the matching mode", `Text` means "literally, independent on matching mode".

Totality: total
Visibility: public export
Constructors:

Line : LineMode

Text : LineMode

Hint: 

Show LineMode

ShowEdgeSide : Show EdgeSide

Totality: total
Visibility: export

ShowLineMode : Show LineMode

Totality: total
Visibility: export

interface Regex : (Type -> Type) -> Type

Parameters: rx
Constraints: Alternative rx
Methods:

sym' : (Char -> Maybe a) -> rx a

  Matches a symbol if the given function returns `Just`, and returns the contents of this `Just`.

sym : (Char -> Bool) -> rx Char

  Matches a symbol satisfying the given predicate, and returns the matched char, or fails.

char : Char -> rx Char

  Matches the given symbol and returns it, or fails.

anyChar : LineMode -> rx Char

  Matches any single char in line (i.e. without newlines depending on the mode) or in text (i.e. literally any character).

edge : LineMode -> EdgeSide -> rx ()

  Matches the start/end of the line/text.

wordBoundary : Bool -> Bool -> rx ()

  Zero-width boundary between a word-class char and a non-word class char or an edge.
  
  For left or right boundary, set corresponding bool parameter to `True`,
  for any set both to `True`, for non-boundary set both to `False`.

string : String -> rx String

  Matches the given string.

withMatch : rx a -> rx (String, a)

  Regex having an original matched string along with the original value.

matchOf : rx a -> rx String

  Regex having only the original matched string as a contained resulting value.

all : All rx tys -> rx (HList tys)

  Matches all of given sub-regexes, sequentially.

exists : All rx tys -> rx (Any id tys)

  Matches is there exists at least one sub-regex that matches.

opt : rx a -> rx (Maybe a)

  Optional application of a given regex.

rep1 : rx a -> rx (List1 a)

rep : rx a -> rx (List a)

repeatN : (n : Nat) -> rx a -> rx (Vect n a)

repeatNOrMore : Nat -> rx a -> rx (List a)

repeatNOrLess : Nat -> rx a -> rx (List a)

repeatNM : (n : Nat) -> (m : Nat) -> {auto 0 _ : LTE n m} -> rx a -> rx (List a)

Implementation: 

Regex RegExp

sym' : Regex rx => (Char -> Maybe a) -> rx a

  Matches a symbol if the given function returns `Just`, and returns the contents of this `Just`.

Totality: total
Visibility: public export

sym : Regex rx => (Char -> Bool) -> rx Char

  Matches a symbol satisfying the given predicate, and returns the matched char, or fails.

Totality: total
Visibility: public export

char : Regex rx => Char -> rx Char

  Matches the given symbol and returns it, or fails.

Totality: total
Visibility: public export

anyChar : Regex rx => LineMode -> rx Char

  Matches any single char in line (i.e. without newlines depending on the mode) or in text (i.e. literally any character).

Totality: total
Visibility: public export

edge : Regex rx => LineMode -> EdgeSide -> rx ()

  Matches the start/end of the line/text.

Totality: total
Visibility: public export

wordBoundary : Regex rx => Bool -> Bool -> rx ()

  Zero-width boundary between a word-class char and a non-word class char or an edge.
  
  For left or right boundary, set corresponding bool parameter to `True`,
  for any set both to `True`, for non-boundary set both to `False`.

Totality: total
Visibility: public export

string : Regex rx => String -> rx String

  Matches the given string.

Totality: total
Visibility: public export

withMatch : Regex rx => rx a -> rx (String, a)

  Regex having an original matched string along with the original value.

Totality: total
Visibility: public export

matchOf : Regex rx => rx a -> rx String

  Regex having only the original matched string as a contained resulting value.

Totality: total
Visibility: public export

all : Regex rx => All rx tys -> rx (HList tys)

  Matches all of given sub-regexes, sequentially.

Totality: total
Visibility: public export

exists : Regex rx => All rx tys -> rx (Any id tys)

  Matches is there exists at least one sub-regex that matches.

Totality: total
Visibility: public export

opt : Regex rx => rx a -> rx (Maybe a)

  Optional application of a given regex.

Totality: total
Visibility: public export

rep1 : Regex rx => rx a -> rx (List1 a)

Totality: total
Visibility: public export

rep : Regex rx => rx a -> rx (List a)

Totality: total
Visibility: public export

repeatN : Regex rx => (n : Nat) -> rx a -> rx (Vect n a)

Totality: total
Visibility: public export

repeatNOrMore : Regex rx => Nat -> rx a -> rx (List a)

Totality: total
Visibility: public export

repeatNOrLess : Regex rx => Nat -> rx a -> rx (List a)

Totality: total
Visibility: public export

repeatNM : Regex rx => (n : Nat) -> (m : Nat) -> {auto 0 _ : LTE n m} -> rx a -> rx (List a)

Totality: total
Visibility: public export

omega : Regex rx => rx ()

  Always matches without consuming any symbol.

Totality: total
Visibility: public export

thenGoes : Regex rx => rx a -> rx b -> rx (a, b)

  Simple consequent composition

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

anyOf : Regex rx => List Char -> rx Char

Totality: total
Visibility: public export

noneOf : Regex rx => List Char -> rx Char

Totality: total
Visibility: public export

between : Regex rx => Char -> Char -> rx Char

Totality: total
Visibility: public export

genericNL : Regex rx => rx String

  Either "\r\n" or any of '\n', '\r' or '\v'

Totality: total
Visibility: public export

data CharClass : Type

Totality: total
Visibility: public export
Constructors:

Alpha : CharClass

Digit : CharClass

XDigit : CharClass

Alnum : CharClass

Upper : CharClass

Lower : CharClass

Word : CharClass

Cntrl : CharClass

Space : CharClass

Blank : CharClass

Graph : CharClass

Print : CharClass

Ascii : CharClass

Punct : CharClass

charClass : CharClass -> Char -> Bool

Totality: total
Visibility: public export

parseDigit : (base : Nat) -> {auto 0 _ : So ((2 <= base) && Delay (base <= 36))} -> Char -> Maybe (Fin base)

Totality: total
Visibility: public export

digit' : Regex rx => (base : Nat) -> {auto 0 _ : So ((2 <= base) && Delay (base <= 36))} -> rx (Fin base)

  A digit of given base

Totality: total
Visibility: public export

digit : Regex rx => rx (Fin 10)

  A 10-base digit

Totality: total
Visibility: public export

naturalNumber' : Regex rx => (base : Nat) -> {auto 0 _ : So ((2 <= base) && Delay (base <= 36))} -> rx Nat

  A natural number regex without any sign

Totality: total
Visibility: public export

naturalNumber : Regex rx => rx Nat

Totality: total
Visibility: public export