Lean 4 Regex

A regular expression engine written in Lean 4.

This library is based on the Rust regex crate and extended for compatibility with PCRE2 (see Syntax).

Main restrictions:

• focus on unicode data,
• simple api and few configurations,
• BoundedBacktracker as the single regex engine,
• no optimizations.

Installation

Add the following dependency to lakefile.lean:

require Regex from git
  "https://github.com/bergmannjg/regex" @ "main"

Documentation

The main documentation is in Regex.lean

Example

Get captures of "∀ (n : Nat), 0 ≤ n" :

def Main : IO Unit := do
  let re := regex% r"^\p{Math}\s*.(?<=\()([a-z])[^,]+,\s*(\p{Nd})\s*(\p{Math})\s*\1$"
  let captures := Regex.captures "∀ (n : Nat), 0 ≤ n" re
  IO.println s!"{captures}"

Output is

fullMatch: '∀ (n : Nat), 0 ≤ n', 0, 22
groups: #[(some ('n', 5, 6)), (some ('0', 15, 16)), (some ('≤', 17, 20))]

Api

• regex% : notation to build the regular expression at compile time
• captures : searches for the first match of the regular expression

Components of regular expression:

• \p{Math} : match all characters with the Math property
• (?<=\() : lookbehind of char '('
• (\p{Nd}) : capturing group of numeric characters
• \1 : backreference to first capturing group

Test

The library is tested with the testdata of the PCRE2 library and the testdata of the Rust Regex crate.

The tests are run with

lake test

License

This project is licensed under the MIT license.

The data in Regex/Unicode/data/ is licensed under the Unicode License Agreement (LICENSE-UNICODE).

The .toml files in testdata/rust are licensed under the (LICENSE-RUST-REGEX).