Documentation

Regex.NFA.Basic

inductive Regex.NFA.Node :

done : Node
fail : Node
epsilon (next : Nat) : Node
anchor (anchor : Data.Anchor) (next : Nat) : Node
char (c : Char) (next : Nat) : Node
split (next₁ next₂ : Nat) : Node
save (offset next : Nat) : Node
sparse (cs : Data.Classes) (next : Nat) : Node

Instances For

instance Regex.NFA.instReprNode :

Equations

Regex.NFA.instReprNode = { reprPrec := Regex.NFA.instReprNode.repr }

def Regex.NFA.instReprNode.repr :

Node → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
Regex.NFA.instReprNode.repr Regex.NFA.Node.done prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Regex.NFA.Node.done")).group prec✝
Regex.NFA.instReprNode.repr Regex.NFA.Node.fail prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Regex.NFA.Node.fail")).group prec✝

Instances For

def Regex.NFA.instDecidableEqNode.decEq (x✝ x✝¹ : Node) :

Decidable (x✝ = x✝¹)

Equations

Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.done Regex.NFA.Node.done = isTrue ⋯
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.done Regex.NFA.Node.fail = isFalse Regex.NFA.instDecidableEqNode.decEq._proof_1✝
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.done (Regex.NFA.Node.epsilon next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.done (Regex.NFA.Node.anchor anchor next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.done (Regex.NFA.Node.char c next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.done (Regex.NFA.Node.split next₁ next₂) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.done (Regex.NFA.Node.save offset next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.done (Regex.NFA.Node.sparse cs next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.fail Regex.NFA.Node.done = isFalse Regex.NFA.instDecidableEqNode.decEq._proof_8✝
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.fail Regex.NFA.Node.fail = isTrue ⋯
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.fail (Regex.NFA.Node.epsilon next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.fail (Regex.NFA.Node.anchor anchor next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.fail (Regex.NFA.Node.char c next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.fail (Regex.NFA.Node.split next₁ next₂) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.fail (Regex.NFA.Node.save offset next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq Regex.NFA.Node.fail (Regex.NFA.Node.sparse cs next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.epsilon next) Regex.NFA.Node.done = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.epsilon next) Regex.NFA.Node.fail = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.epsilon a) (Regex.NFA.Node.epsilon b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.epsilon next) (Regex.NFA.Node.anchor anchor next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.epsilon next) (Regex.NFA.Node.char c next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.epsilon next) (Regex.NFA.Node.split next₁ next₂) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.epsilon next) (Regex.NFA.Node.save offset next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.epsilon next) (Regex.NFA.Node.sparse cs next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.anchor anchor next) Regex.NFA.Node.done = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.anchor anchor next) Regex.NFA.Node.fail = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.anchor anchor next) (Regex.NFA.Node.epsilon next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.anchor a a_1) (Regex.NFA.Node.anchor b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.anchor anchor next) (Regex.NFA.Node.char c next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.anchor anchor next) (Regex.NFA.Node.split next₁ next₂) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.anchor anchor next) (Regex.NFA.Node.save offset next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.anchor anchor next) (Regex.NFA.Node.sparse cs next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.char c next) Regex.NFA.Node.done = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.char c next) Regex.NFA.Node.fail = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.char c next) (Regex.NFA.Node.epsilon next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.char c next) (Regex.NFA.Node.anchor anchor next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.char a a_1) (Regex.NFA.Node.char b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.char c next) (Regex.NFA.Node.split next₁ next₂) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.char c next) (Regex.NFA.Node.save offset next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.char c next) (Regex.NFA.Node.sparse cs next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.split next₁ next₂) Regex.NFA.Node.done = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.split next₁ next₂) Regex.NFA.Node.fail = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.split next₁ next₂) (Regex.NFA.Node.epsilon next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.split next₁ next₂) (Regex.NFA.Node.anchor anchor next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.split next₁ next₂) (Regex.NFA.Node.char c next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.split a a_1) (Regex.NFA.Node.split b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.split next₁ next₂) (Regex.NFA.Node.save offset next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.split next₁ next₂) (Regex.NFA.Node.sparse cs next) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.save offset next) Regex.NFA.Node.done = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.save offset next) Regex.NFA.Node.fail = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.save offset next) (Regex.NFA.Node.epsilon next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.save offset next) (Regex.NFA.Node.anchor anchor next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.save offset next) (Regex.NFA.Node.char c next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.save offset next) (Regex.NFA.Node.split next₁ next₂) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.save a a_1) (Regex.NFA.Node.save b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.save offset next) (Regex.NFA.Node.sparse cs next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.sparse cs next) Regex.NFA.Node.done = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.sparse cs next) Regex.NFA.Node.fail = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.sparse cs next) (Regex.NFA.Node.epsilon next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.sparse cs next) (Regex.NFA.Node.anchor anchor next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.sparse cs next) (Regex.NFA.Node.char c next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.sparse cs next) (Regex.NFA.Node.split next₁ next₂) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.sparse cs next) (Regex.NFA.Node.save offset next_1) = isFalse ⋯
Regex.NFA.instDecidableEqNode.decEq (Regex.NFA.Node.sparse a a_1) (Regex.NFA.Node.sparse b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

instance Regex.NFA.instDecidableEqNode :

DecidableEq Node

Equations

Regex.NFA.instDecidableEqNode = Regex.NFA.instDecidableEqNode.decEq

instance Regex.NFA.instInhabitedNode :

Equations

Regex.NFA.instInhabitedNode = { default := Regex.NFA.instInhabitedNode.default }

def Regex.NFA.instInhabitedNode.default :

Equations

Regex.NFA.instInhabitedNode.default = Regex.NFA.Node.done

Instances For

instance Regex.NFA.instToExprNode :

Lean.ToExpr Node

Equations

Regex.NFA.instToExprNode = { toExpr := Regex.NFA.instToExprNode.toExpr, toTypeExpr := Lean.Expr.const `Regex.NFA.Node [] }

def Regex.NFA.instToExprNode.toExpr :

Node → Lean.Expr

Equations

Regex.NFA.instToExprNode.toExpr Regex.NFA.Node.done = Lean.Expr.const `Regex.NFA.Node.done []
Regex.NFA.instToExprNode.toExpr Regex.NFA.Node.fail = Lean.Expr.const `Regex.NFA.Node.fail []
Regex.NFA.instToExprNode.toExpr (Regex.NFA.Node.epsilon a) = (Lean.Expr.const `Regex.NFA.Node.epsilon []).app (Lean.toExpr a)
Regex.NFA.instToExprNode.toExpr (Regex.NFA.Node.anchor a a_1) = ((Lean.Expr.const `Regex.NFA.Node.anchor []).app (Lean.toExpr a)).app (Lean.toExpr a_1)
Regex.NFA.instToExprNode.toExpr (Regex.NFA.Node.char a a_1) = ((Lean.Expr.const `Regex.NFA.Node.char []).app (Lean.toExpr a)).app (Lean.toExpr a_1)
Regex.NFA.instToExprNode.toExpr (Regex.NFA.Node.split a a_1) = ((Lean.Expr.const `Regex.NFA.Node.split []).app (Lean.toExpr a)).app (Lean.toExpr a_1)
Regex.NFA.instToExprNode.toExpr (Regex.NFA.Node.save a a_1) = ((Lean.Expr.const `Regex.NFA.Node.save []).app (Lean.toExpr a)).app (Lean.toExpr a_1)
Regex.NFA.instToExprNode.toExpr (Regex.NFA.Node.sparse a a_1) = ((Lean.Expr.const `Regex.NFA.Node.sparse []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

Instances For

@[always_inline]

def Regex.NFA.Node.isDone (n : Node) :

Equations

Regex.NFA.Node.done.isDone = true
n.isDone = false

Instances For

@[simp]

theorem Regex.NFA.Node.isDone_def {n : Node} :

n.isDone = decide (n = done)

def Regex.NFA.Node.inBounds (n : Node) (size : Nat) :

Equations

Regex.NFA.Node.done.inBounds size = True
Regex.NFA.Node.fail.inBounds size = True
(Regex.NFA.Node.epsilon next).inBounds size = (next < size)
(Regex.NFA.Node.anchor anchor next).inBounds size = (next < size)
(Regex.NFA.Node.char c next).inBounds size = (next < size)
(Regex.NFA.Node.split next₁ next₂).inBounds size = (next₁ < size ∧ next₂ < size)
(Regex.NFA.Node.save offset next).inBounds size = (next < size)
(Regex.NFA.Node.sparse cs next).inBounds size = (next < size)

Instances For

@[simp]

theorem Regex.NFA.Node.inBounds.done {size : Nat} :

Node.done.inBounds size

@[simp]

theorem Regex.NFA.Node.inBounds.fail {size : Nat} :

Node.fail.inBounds size

@[simp]

theorem Regex.NFA.Node.inBounds.epsilon_iff {size next : Nat} :

(epsilon next).inBounds size ↔ next < size

@[simp]

theorem Regex.NFA.Node.inBounds.anchor_iff {size next : Nat} {a : Data.Anchor} :

(anchor a next).inBounds size ↔ next < size

@[simp]

theorem Regex.NFA.Node.inBounds.char_iff {size next : Nat} {c : Char} :

(char c next).inBounds size ↔ next < size

@[simp]

theorem Regex.NFA.Node.inBounds.split_iff {size next₁ next₂ : Nat} :

(split next₁ next₂).inBounds size ↔ next₁ < size ∧ next₂ < size

@[simp]

theorem Regex.NFA.Node.inBounds.save_iff {size offset next : Nat} :

(save offset next).inBounds size ↔ next < size

@[simp]

theorem Regex.NFA.Node.inBounds.sparse_iff {size next : Nat} {cs : Data.Classes} :

(sparse cs next).inBounds size ↔ next < size

theorem Regex.NFA.Node.inBounds_of_inBounds_of_le {n : Node} {size size' : Nat} (h : n.inBounds size) (le : size ≤ size') :

n.inBounds size'

structure Regex.NFA :

A NFA consists of an array of nodes. The starting node is the last node.

The transition relation and accept nodes are embedded in the nodes themselves.

nodes : Array Node

Instances For

theorem Regex.NFA.ext_iff {x y : NFA} :

x = y ↔ x.nodes = y.nodes

theorem Regex.NFA.ext {x y : NFA} (nodes : x.nodes = y.nodes) :

x = y

instance Regex.instReprNFA :

Equations

Regex.instReprNFA = { reprPrec := Regex.instReprNFA.repr }

def Regex.instReprNFA.repr :

NFA → Nat → Std.Format

Equations

Regex.instReprNFA.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "nodes" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.nodes)).group) " }"

Instances For

def Regex.instDecidableEqNFA.decEq (x✝ x✝¹ : NFA) :

Decidable (x✝ = x✝¹)

Equations

Regex.instDecidableEqNFA.decEq { nodes := a } { nodes := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

instance Regex.instDecidableEqNFA :

DecidableEq NFA

Equations

Regex.instDecidableEqNFA = Regex.instDecidableEqNFA.decEq

def Regex.instInhabitedNFA.default :

Equations

Regex.instInhabitedNFA.default = { nodes := default }

Instances For

instance Regex.instInhabitedNFA :

Equations

Regex.instInhabitedNFA = { default := Regex.instInhabitedNFA.default }

def Regex.instToExprNFA.toExpr :

NFA → Lean.Expr

Equations

Regex.instToExprNFA.toExpr { nodes := a } = (Lean.Expr.const `Regex.NFA.mk []).app (Lean.toExpr a)

Instances For

instance Regex.instToExprNFA :

Lean.ToExpr NFA

Equations

Regex.instToExprNFA = { toExpr := Regex.instToExprNFA.toExpr, toTypeExpr := Lean.Expr.const `Regex.NFA [] }

instance Regex.instToStringNFA :

Equations

Regex.instToStringNFA = { toString := fun (nfa : Regex.NFA) => reprStr nfa }

def Regex.NFA.done :

Equations

Regex.NFA.done = { nodes := #[Regex.NFA.Node.done ] }

Instances For

def Regex.NFA.size (nfa : NFA) :

Equations

nfa.size = nfa.nodes.size

Instances For

def Regex.NFA.start (nfa : NFA) :

Equations

nfa.start = nfa.size - 1

Instances For

def Regex.NFA.get (nfa : NFA) (i : Nat) (h : i < nfa.size) :

Equations

nfa.get i h = nfa.nodes[i]

Instances For

instance Regex.NFA.instGetElemNatNodeLtSize :

GetElem NFA Nat Node fun (nfa : NFA) (i : Nat) => i < nfa.size

Equations

Regex.NFA.instGetElemNatNodeLtSize = { getElem := fun (nfa : Regex.NFA) (i : Nat) (h : i < nfa.size) => nfa.get i h }

theorem Regex.NFA.get_eq_nodes_get (nfa : NFA) (i : Nat) (h : i < nfa.size) :

nfa[i] = nfa.nodes[i]

def Regex.NFA.maxTag (nfa : NFA) :

Equations

nfa.maxTag = Array.foldl (fun (accum : Nat) (node : Regex.NFA.Node) => match node with | Regex.NFA.Node.save tag next => accum.max tag | x => accum) 0 nfa.nodes

Instances For

theorem Regex.NFA.le_maxTag {tag next : Nat} (nfa : NFA) (i : Fin nfa.size) (eq : nfa[i] = Node.save tag next) :

tag ≤ nfa.maxTag

structure Regex.NFA.WellFormed (nfa : NFA) :

size_lt : 0 < nfa.size
inBounds (i : Nat) (h : i < nfa.size) : nfa[i].inBounds nfa.size

Instances For

theorem Regex.NFA.WellFormed.iff {nfa : NFA} :

nfa.WellFormed ↔ 0 < nfa.size ∧ ∀ (i : Nat) (h : i < nfa.size), nfa[i].inBounds nfa.size

theorem Regex.NFA.WellFormed.inBounds' {nfa : NFA} {node : Node} (wf : nfa.WellFormed) (i : Nat) (h : i < nfa.size) (hn : nfa[i] = node) :

node.inBounds nfa.size

theorem Regex.NFA.WellFormed.start_lt {nfa : NFA} (wf : nfa.WellFormed) :

nfa.start < nfa.size

instance Regex.NFA.decWellFormed (nfa : NFA) :

Decidable nfa.WellFormed

Equations

nfa.decWellFormed = decidable_of_decidable_of_iff ⋯

theorem Regex.NFA.done_WellFormed :

done.WellFormed