Regular expressions, typed

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

Between lo and hi repetitions, both included.

Equations

• Cvc.Typed.Term.reLoop lo hi re = Cvc.Untyped.Term.reLoop lo hi re

def Cvc.Typed.Term.reAll [Ω] : Env (Term Regex)

The regular expression matching every string.

Equations

• Cvc.Typed.Term.reAll = Cvc.Untyped.Term.reAll

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

Union.

Equations

• lft.reUnion rgt = Cvc.Untyped.Term.reUnion lft rgt

def Cvc.Typed.Term.reNone [Ω] : Env (Term Regex)

The regular expression matching nothing.

Equations

• Cvc.Typed.Term.reNone = Cvc.Untyped.Term.reNone

def Cvc.Typed.Term.reRange [Ω] (lo hi : Term String) : Env (Term Regex)

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

Equations

• lo.reRange hi = Cvc.Untyped.Term.reRange lo hi

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

One or more repetitions.

Equations

• re.rePlus = Cvc.Untyped.Term.rePlus re

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

Complement.

Equations

• re.reComplement = Cvc.Untyped.Term.reComplement re

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

Zero or one repetition.

Equations

• re.reOpt = Cvc.Untyped.Term.reOpt re

def Cvc.Typed.Term.reAllChar [Ω] : Env (Term Regex)

The regular expression matching every one-character string.

Equations

• Cvc.Typed.Term.reAllChar = Cvc.Untyped.Term.reAllChar

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

Concatenation.

Equations

• lft.reConcat rgt = Cvc.Untyped.Term.reConcat lft rgt

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

reConcat over two or more terms.

Equations

• Cvc.Typed.Term.reConcatN terms atLeastTwoElements = Cvc.Untyped.Term.reConcatN terms atLeastTwoElements

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

Difference: the strings matching lft but not rgt.

Equations

• lft.reDiff rgt = Cvc.Untyped.Term.reDiff lft rgt

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

Exactly the given number of repetitions.

Equations

• Cvc.Typed.Term.reRepeat count re = Cvc.Untyped.Term.reRepeat count re

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

Kleene star.

Equations

• re.reStar = Cvc.Untyped.Term.reStar re

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

Intersection.

Equations

• lft.reInter rgt = Cvc.Untyped.Term.reInter lft rgt

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

reUnion over two or more terms.

Equations

• Cvc.Typed.Term.reUnionN terms atLeastTwoElements = Cvc.Untyped.Term.reUnionN terms atLeastTwoElements

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

reInter over two or more terms.

Equations

• Cvc.Typed.Term.reInterN terms atLeastTwoElements = Cvc.Untyped.Term.reInterN terms atLeastTwoElements

def Cvc.Typed.View.Regex.of [Ω] (τ : Typ) (t : Term τ.Denote) : Env (Option (View.Regex τ))

Takes a term apart one level, at its sort, if Regex owns its operator and the term's sort fits it.

Equations

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

inductive Cvc.Typed.View.Regex [Ω] : Typ → Type

Regex's operators, taken apart one level, indexed by the sort each produces.

• regex [Ω] : OnRegex → View.Regex Typ.regex

  An operator with a result of sort Regex.

inductive Cvc.Typed.View.Regex.OnRegex [Ω] : Type

Regex's operators with a result of sort Regex.

• reConcat [Ω] (kids : Kids Regex) : OnRegex

  Concatenation.

  kids holds every operand, two or more.

• reUnion [Ω] (kids : Kids Regex) : OnRegex

  Union.

  kids holds every operand, two or more.

• reInter [Ω] (kids : Kids Regex) : OnRegex

  Intersection.

  kids holds every operand, two or more.

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

  Difference: the strings matching lft but not rgt.

• reStar [Ω] (re : Term Regex) : OnRegex

  Kleene star.

• rePlus [Ω] (re : Term Regex) : OnRegex

  One or more repetitions.

• reOpt [Ω] (re : Term Regex) : OnRegex

  Zero or one repetition.

• reRange [Ω] (lo hi : Term String) : OnRegex

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

• reComplement [Ω] (re : Term Regex) : OnRegex

  Complement.

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

  Between lo and hi repetitions, both included.

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

  Exactly the given number of repetitions.

• reAll [Ω] : OnRegex

  The regular expression matching every string.

• reAllChar [Ω] : OnRegex

  The regular expression matching every one-character string.

• reNone [Ω] : OnRegex

  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.getValueTerm.

regex!

regex! "ab" ['0'-'9']+ | .* writes a regular expression in the usual notation, as an Env (Term Regex). A regex term in scope, or a ![…] escape, must be a Term Regex.

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

A regular expression in the usual notation, as an Env (Term Regex): regex! "a"+ | .*.

Equations

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