The regex Plugin

See also

mim::plug::regex

A normalizing regex plugin.

Dependencies

import compile;
plugin core;
plugin mem;
plugin cps;

Types

RE

A position in a mem.Str n; position n is the end of the string.

anx lam Pos (n: Nat): * = Idx (core.nat.add (n, 1));

The i-th position in a mem.Str n.

anx lam pos (n: Nat) (i: Nat): Pos n = core.idx 0 (core.nat.add (n, 1)) i;

Res n is a match result: the memory, a success flag, and the new position.

anx lam Res (n: Nat): * = [mem.M 0, Bool, Pos n];

RE is the matcher itself: it takes the memory, the string, and the current position.

anx let RE = {n: Nat} → [mem.M 0, mem.Str n, Pos n] → Res n;

Meta

conj

A sequence of REs.
E.g., \d\d\d matches 3 digits: regex.conj (regex.cls.d, regex.cls.d, regex.cls.d).

axm conj: {n: Nat} → «n; RE» → RE, normalize_conj, 2;

disj

Matches any of the sub-expressions, e.g. [0123456789].

axm disj: {n: Nat} → «n; RE» → RE, normalize_disj, 2;

Values

range

Wraps a range of literals. E.g., use regex.range ('a', 'z') to match all lower-case letters.

axm range: «2; mem.Char» → RE, normalize_range, 1;

lit

Wraps a literal.

anx lam lit (val: mem.Char): RE = range (val, val);

not

Matches anything but the ranges in the parameter - the parameter must only contain regex.disjs and regex.ranges.

axm not: RE → RE, normalize_not, 1;

neg_lookahead

Succeeds iff the parameter does not match, without consuming input.

axm neg_lookahead: RE → RE, 1;

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

pub mod cls
    anx let d = range ('0', '9');
    anx let D = not d;
    anx let w = disj (range ('0', '9'), range ('a', 'z'), range ('A', 'Z'), lit '_');
    anx let W = not w;
    anx let s = disj (range ('\t', '\n'), lit '\r', lit ' ');
    anx let S = not s;
end

any

Matches any character.

axm any: RE, 0;

empty

Matches the empty string.

axm empty: RE, 0;

Quantifiers

quant.*

The usual quantifiers:

• optional: ? - zero or one
• star: * - zero or more
• plus: + - one or more

axm quant.(optional, star, plus): RE → RE, normalize_quant, 1;

Phases

lower_regex

Compiles the regex combinators into an executable matcher (via a DFA).

axm lower_regex: compile.Phase;