Generated Regex constructors, sort-erased

def Cvc.Untyped.Term.reInter [Ω] (lft rgt : Term) : Env Term

Intersection.

Equations

• lft.reInter rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.REGEXP_INTER #[lft, rgt]

def Cvc.Untyped.Term.reComplement [Ω] (re : Term) : Env Term

Complement.

Equations

• re.reComplement = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.REGEXP_COMPLEMENT #[re]

def Cvc.Untyped.Term.reInterN [Ω] (terms : Terms) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env Term

reInter over two or more terms.

Equations

• Cvc.Untyped.Term.reInterN terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.REGEXP_INTER terms

def Cvc.Untyped.Term.reLoop [Ω] (lo hi : Nat) (re : Term) : Env Term

Between lo and hi repetitions, both included.

Equations

• Cvc.Untyped.Term.reLoop lo hi re = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => do let __do_lift ← tm.mkOpOfIndices cvc5.Kind.REGEXP_LOOP #[lo, hi] tm.mkTermOfOp __do_lift #[re]

def Cvc.Untyped.Term.reUnionN [Ω] (terms : Terms) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env Term

reUnion over two or more terms.

Equations

• Cvc.Untyped.Term.reUnionN terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.REGEXP_UNION terms

def Cvc.Untyped.Term.reConcat [Ω] (lft rgt : Term) : Env Term

Concatenation.

Equations

• lft.reConcat rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.REGEXP_CONCAT #[lft, rgt]

def Cvc.Untyped.Term.reAll [Ω] : Env Term

The regular expression matching every string.

Equations

• Cvc.Untyped.Term.reAll = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkRegexpAll

def Cvc.Untyped.Term.reNone [Ω] : Env Term

The regular expression matching nothing.

Equations

• Cvc.Untyped.Term.reNone = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkRegexpNone

def Cvc.Untyped.Term.reOpt [Ω] (re : Term) : Env Term

Zero or one repetition.

Equations

• re.reOpt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.REGEXP_OPT #[re]

def Cvc.Untyped.Term.reConcatN [Ω] (terms : Terms) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env Term

reConcat over two or more terms.

Equations

• Cvc.Untyped.Term.reConcatN terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.REGEXP_CONCAT terms

def Cvc.Untyped.Term.reDiff [Ω] (lft rgt : Term) : Env Term

Difference: the strings matching lft but not rgt.

Equations

• lft.reDiff rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.REGEXP_DIFF #[lft, rgt]

def Cvc.Untyped.Term.reRange [Ω] (lo hi : Term) : Env Term

Any one character from lo to hi included; matches nothing unless both are one character.

Equations

• lo.reRange hi = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.REGEXP_RANGE #[lo, hi]

def Cvc.Untyped.Term.reStar [Ω] (re : Term) : Env Term

Kleene star.

Equations

• re.reStar = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.REGEXP_STAR #[re]

def Cvc.Untyped.Term.rePlus [Ω] (re : Term) : Env Term

One or more repetitions.

Equations

• re.rePlus = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.REGEXP_PLUS #[re]

def Cvc.Untyped.Term.reRepeat [Ω] (count : Nat) (re : Term) : Env Term

Exactly the given number of repetitions.

Equations

• Cvc.Untyped.Term.reRepeat count re = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => do let __do_lift ← tm.mkOpOfIndices cvc5.Kind.REGEXP_REPEAT #[count] tm.mkTermOfOp __do_lift #[re]

def Cvc.Untyped.Term.reUnion [Ω] (lft rgt : Term) : Env Term

Union.

Equations

• lft.reUnion rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.REGEXP_UNION #[lft, rgt]

def Cvc.Untyped.Term.reAllChar [Ω] : Env Term

The regular expression matching every one-character string.

Equations

• Cvc.Untyped.Term.reAllChar = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkRegexpAllchar

def Cvc.Untyped.View.Regex.of? [Ω] (viewed : Term) : Option View.Regex

Takes a term apart one level, if Regex owns its operator.

Equations

• One or more equations did not get rendered due to their size.

inductive Cvc.Untyped.View.Regex [Ω] : Type

Regex's operators, taken apart one level, sort-erased.

• reConcat [Ω] (kids : Kids) : View.Regex

  Concatenation.

  kids holds every operand, two or more.

• reUnion [Ω] (kids : Kids) : View.Regex

  Union.

  kids holds every operand, two or more.

• reInter [Ω] (kids : Kids) : View.Regex

  Intersection.

  kids holds every operand, two or more.

• reDiff [Ω] (lft rgt : Term) : View.Regex

  Difference: the strings matching lft but not rgt.

• reStar [Ω] (re : Term) : View.Regex

  Kleene star.

• rePlus [Ω] (re : Term) : View.Regex

  One or more repetitions.

• reOpt [Ω] (re : Term) : View.Regex

  Zero or one repetition.

• reRange [Ω] (lo hi : Term) : View.Regex

  Any one character from lo to hi included; matches nothing unless both are one character.

• reComplement [Ω] (re : Term) : View.Regex

  Complement.

• reLoop [Ω] (lo hi : Nat) (re : Term) : View.Regex

  Between lo and hi repetitions, both included.

• reRepeat [Ω] (count : Nat) (re : Term) : View.Regex

  Exactly the given number of repetitions.

• reAll [Ω] : View.Regex

  The regular expression matching every string.

• reAllChar [Ω] : View.Regex

  The regular expression matching every one-character string.

• reNone [Ω] : View.Regex

  The regular expression matching nothing.

Values

A regular expression has no Lean value: cvc5 exposes no accessor for the language a constant regex denotes, so Regex has no value conversions. Read a model's regex as a term, with Solver.getValue.

regex!

Regular expressions in the notation they are usually written in, building the same terms as the re… constructors:

regex! ['a'-'z' '_'] ['a'-'z' '0'-'9' '_']*     -- an identifier
regex! digit+ ("." digit+)?                       -- `digit` a regex term in scope
regex! ("ab" | "cd"){2,3} ∖ "abab"

form	meaning
"abc", 'a'	the literal string, the literal character
x, ![e]	a regex term in scope, any Lean term of type Env Term
., ∅	any single character, the empty language (.* is every string)
['a'-'z' '_'], [^ …]	a character class: ranges and characters; its complement in .
r*, r+, r?, r{n}, r{n,m}	star, plus, option, exactly n, between n and m
r s	concatenation
¬ r	complement
r ∩ s, r ∖ s	intersection, difference
r \| s	union

Postfix operators bind tightest, then complement, then concatenation, then ∩/∖, then |, as in the usual notation. A literal string is Lean's, so escapes are Lean's and a "." is a dot, never "any character". No token is added that Lean does not already have.

regex! is scoped in each layer, as smt! is: open Cvc.Untyped selects this one, which answers an Env Term; the typed one answers an Env (Term Regex).

def Cvc.smtRegex.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.smtRegex : Category

A regular expression, as regex! writes one.

Equations

• Lean.Parser.Category.smtRegex = { }

def Lean.Parser.Category.smtRegexClassItem : Category

An item of a character class: a character, or a range of them.

Equations

• Lean.Parser.Category.smtRegexClassItem = { }

def Cvc.smtRegexClassItem.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Cvc.smtRegexClassChar : Lean.ParserDescr

A single character.

Equations

• Cvc.smtRegexClassChar = Lean.ParserDescr.node `Cvc.smtRegexClassChar 1022 (Lean.ParserDescr.const `char)

def Cvc.smtRegexClassRange : Lean.ParserDescr

The characters from the first to the second, inclusive.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.smtRegexStr : Lean.ParserDescr

A literal string.

Equations

• Cvc.smtRegexStr = Lean.ParserDescr.node `Cvc.smtRegexStr 1024 (Lean.ParserDescr.const `str)

def Cvc.smtRegexChar : Lean.ParserDescr

A literal character.

Equations

• Cvc.smtRegexChar = Lean.ParserDescr.node `Cvc.smtRegexChar 1024 (Lean.ParserDescr.const `char)

def Cvc.smtRegexIdent : Lean.ParserDescr

A regex term in scope.

Equations

• Cvc.smtRegexIdent = Lean.ParserDescr.node `Cvc.smtRegexIdent 1024 (Lean.ParserDescr.const `ident)

def Cvc.smtRegexEscape : Lean.ParserDescr

Any Lean term building a regex: Env Term, Env (Term Regex) typed.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.smtRegexParen : Lean.ParserDescr

Grouping.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.smtRegexAny : Lean.ParserDescr

Any single character.

Equations

• Cvc.smtRegexAny = Lean.ParserDescr.node `Cvc.smtRegexAny 1024 (Lean.ParserDescr.nonReservedSymbol "." false)

def Cvc.smtRegexNone : Lean.ParserDescr

The empty language.

Equations

• Cvc.smtRegexNone = Lean.ParserDescr.node `Cvc.smtRegexNone 1024 (Lean.ParserDescr.nonReservedSymbol "∅" false)

def Cvc.smtRegexClass : Lean.ParserDescr

A character class.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.smtRegexNotClass : Lean.ParserDescr

A negated character class: any single character not in it.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.smtRegexStar : Lean.TrailingParserDescr

Zero or more.

Equations

• Cvc.smtRegexStar = Lean.ParserDescr.trailingNode `Cvc.smtRegexStar 1024 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `noWs) (Lean.ParserDescr.symbol "*"))

def Cvc.smtRegexPlus : Lean.TrailingParserDescr

One or more.

Equations

• Cvc.smtRegexPlus = Lean.ParserDescr.trailingNode `Cvc.smtRegexPlus 1024 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `noWs) (Lean.ParserDescr.symbol "+"))

def Cvc.smtRegexOpt : Lean.TrailingParserDescr

Zero or one.

Equations

• Cvc.smtRegexOpt = Lean.ParserDescr.trailingNode `Cvc.smtRegexOpt 1024 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `noWs) (Lean.ParserDescr.symbol "?"))

def Cvc.smtRegexRepeat : Lean.TrailingParserDescr

Exactly n.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.smtRegexLoop : Lean.TrailingParserDescr

Between n and m, inclusive.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.smtRegexComp : Lean.ParserDescr

Complement.

Equations

• Cvc.smtRegexComp = Lean.ParserDescr.node `Cvc.smtRegexComp 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "¬" false) (Lean.ParserDescr.cat `smtRegex 1024))

def Cvc.smtRegexSeq : Lean.TrailingParserDescr

Concatenation, by juxtaposition: flat, as application is in smt!.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.smtRegexInter : Lean.TrailingParserDescr

Intersection.

Equations

• Cvc.smtRegexInter = Lean.ParserDescr.trailingNode `Cvc.smtRegexInter 20 20 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∩ ") (Lean.ParserDescr.cat `smtRegex 21))

def Cvc.smtRegexDiff : Lean.TrailingParserDescr

Difference.

Equations

• Cvc.smtRegexDiff = Lean.ParserDescr.trailingNode `Cvc.smtRegexDiff 20 20 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∖ ") (Lean.ParserDescr.cat `smtRegex 21))

def Cvc.smtRegexUnion : Lean.TrailingParserDescr

Union.

Equations

• Cvc.smtRegexUnion = Lean.ParserDescr.trailingNode `Cvc.smtRegexUnion 10 10 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " | ") (Lean.ParserDescr.cat `smtRegex 11))

def Cvc.regexU : Lean.ParserDescr

A sort-erased regex; regex! under open Cvc.Untyped.

Equations

• Cvc.regexU = Lean.ParserDescr.node `Cvc.regexU 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "regexU! ") (Lean.ParserDescr.cat `smtRegex 0))

def Cvc.regexT : Lean.ParserDescr

A typed regex; regex! under open Cvc.Typed.

Equations

• Cvc.regexT = Lean.ParserDescr.node `Cvc.regexT 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "regexT! ") (Lean.ParserDescr.cat `smtRegex 0))

def Cvc.Untyped.termRegex!_ : Lean.ParserDescr

A sort-erased regex term, in Env, in the usual notation: regex! ['a'-'z']+ ("." | "_")?.

Equations

• Cvc.Untyped.termRegex!_ = Lean.ParserDescr.node `Cvc.Untyped.termRegex!_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "regex! ") (Lean.ParserDescr.cat `smtRegex 0))

partial def Cvc.Ext.expandRegex (layer : Layer) (stx : Lean.Syntax) : Lean.MacroM (Lean.TSyntax `term)

Expands a regex! node into a term of the given layer, in Env.