The regex Plugin

Table of Contents

• Dependencies
• Types
  • RE
• Meta
  • regex.conj
  • regex.disj
• Values
  • regex.range
  • regex.lit
  • regex.not
  • regex.cls.*
  • regex.any
• Quantifiers
  • regex.quant.*
• Passes and Phases
  • Passes

See also

thorin::plug::regex

A normalizing regex plugin

Dependencies

.import compile;
.plugin core;
.plugin mem;
.plugin direct;

Types

RE

Char & String

.let Char = .I8;
.lam Str(n: .Nat): * = %mem.Ptr0 «n; Char»;

A regular expression matcher.

.lam Res (n: .Nat): * = [%mem.M, .Bool, .Idx n];
.let RE = Π.[n: .Nat][%mem.M, Str n, .Idx n] -> Res n;

Meta

%regex.conj

A sequence of RE's, e.g. \d\d\d matching 3 digits: %regex.conj (%regex.cls.d, %regex.cls.d, %regex.cls.d)

.ax %regex.conj: Π[n: .Nat][«n; RE»] -> RE, normalize_conj, 2;

%regex.disj

Match any of the sub expressions: [0123456789]

.ax %regex.disj: Π[n: .Nat][«n; RE»] -> RE, normalize_disj, 2;

Values

%regex.range

Wraps a range of literals. Use: ‘%regex.range ('a’, 'z')` to match all lower case letters.

.ax %regex.range: «2; Char» -> RE, normalize_range, 1;

%regex.lit

Wraps a literal.

.lam %regex.lit(val: Char) = %regex.range (val, val);

%regex.not

Do not match the parameter.

.ax %regex.not_: RE -> RE, normalize_not, 1;

%regex.cls.*

Subtag	Matches
d	digits [0-9]
D	No digits
w	word characters [a-zA-Z_0-9]
W	No word characters
s	whitespace [ \t\r\n]
S	No whitespace

.let %regex.cls.d = %regex.range ('0', '9');
.let %regex.cls.D = %regex.not_ %regex.cls.d;
.let %regex.cls.w = %regex.disj 4 (%regex.range ('0', '9'), %regex.range ('a', 'z'), %regex.range ('A', 'Z'), %regex.lit '_');
.let %regex.cls.W = %regex.not_ %regex.cls.w;
.let %regex.cls.s = %regex.disj 3 (%regex.range ('\t', '\n'), %regex.lit '\r', %regex.lit ' ');
.let %regex.cls.S = %regex.not_ %regex.cls.s;

%regex.any

Match any character.

.ax %regex.any: RE;

Quantifiers

%regex.quant.*

.ax %regex.quant(optional,star,plus): RE -> RE, normalize_quant, 1;

Passes and Phases

Passes

.ax %regex.lower_regex: %compile.Pass;