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

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

instance Regex.NFA.instReprNode :

Equations

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

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 [] }

@[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 a).inBounds size = (a < size)
(Regex.NFA.Node.anchor a a_1).inBounds size = (a_1 < size)
(Regex.NFA.Node.char a a_1).inBounds size = (a_1 < size)
(Regex.NFA.Node.split a a_1).inBounds size = (a < size ∧ a_1 < size)
(Regex.NFA.Node.save a a_1).inBounds size = (a_1 < size)
(Regex.NFA.Node.sparse a a_1).inBounds size = (a_1 < 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 {size next : Nat} (h : next < size) :

(Node.epsilon next).inBounds size

@[simp]

theorem Regex.NFA.Node.inBounds.anchor {size next : Nat} {a : Data.Anchor} (h : next < size) :

(Node.anchor a next).inBounds size

@[simp]

theorem Regex.NFA.Node.inBounds.char {size next : Nat} {c : Char} (h : next < size) :

(Node.char c next).inBounds size

@[simp]

theorem Regex.NFA.Node.inBounds.split {size next₁ next₂ : Nat} (h₁ : next₁ < size) (h₂ : next₂ < size) :

(Node.split next₁ next₂).inBounds size

@[simp]

theorem Regex.NFA.Node.inBounds.save {size offset next : Nat} (h : next < size) :

(Node.save offset next).inBounds size

theorem Regex.NFA.Node.lt_of_inBounds.epsilon {size next : Nat} (h : (Node.epsilon next).inBounds size) :

next < size

theorem Regex.NFA.Node.lt_of_inBounds.char {size next : Nat} {c : Char} (h : (Node.char c next).inBounds size) :

next < size

theorem Regex.NFA.Node.lt_of_inBounds.split {size next₁ next₂ : Nat} (h : (Node.split next₁ next₂).inBounds size) :

next₁ < size ∧ next₂ < size

theorem Regex.NFA.Node.lt_of_inBounds.split_left {size next₁ next₂ : Nat} (h : (Node.split next₁ next₂).inBounds size) :

next₁ < size

theorem Regex.NFA.Node.lt_of_inBounds.split_right {size next₁ next₂ : Nat} (h : (Node.split next₁ next₂).inBounds size) :

next₂ < size

theorem Regex.NFA.Node.lt_of_inBounds.save {size offset next : Nat} (h : (Node.save offset 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'

instance Regex.NFA.Node.decInBounds {node : Node} {size : Nat} :

Decidable (node.inBounds size)

Equations

Regex.NFA.Node.decInBounds = isTrue trivial
Regex.NFA.Node.decInBounds = isTrue trivial
Regex.NFA.Node.decInBounds = inferInstanceAs (Decidable (next < size))
Regex.NFA.Node.decInBounds = inferInstanceAs (Decidable (next < size))
Regex.NFA.Node.decInBounds = inferInstanceAs (Decidable (next < size))
Regex.NFA.Node.decInBounds = inferInstanceAs (Decidable (next < size))
Regex.NFA.Node.decInBounds = inferInstanceAs (Decidable (next₁ < size ∧ next₂ < size))
Regex.NFA.Node.decInBounds = inferInstanceAs (Decidable (next < size))

structure Regex.NFA :

A NFA consists an array of nodes and a designated start node.

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

nodes : Array Node
start : Nat

Instances For

instance Regex.instReprNFA :

Equations

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

def Regex.instReprNFA.repr :

NFA → Nat → Std.Format

Equations

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

Instances For

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

Decidable (x✝ = x✝¹)

Equations

Regex.instDecidableEqNFA.decEq { nodes := a, start := a_1 } { nodes := b, start := 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.instDecidableEqNFA :

DecidableEq NFA

Equations

Regex.instDecidableEqNFA = Regex.instDecidableEqNFA.decEq

instance Regex.instInhabitedNFA :

Equations

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

def Regex.instInhabitedNFA.default :

Equations

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

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 ], start := 0 }

Instances For

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

Equations

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

Instances For

instance Regex.NFA.instGetElemNatNodeLtSizeNodes :

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

Equations

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

theorem Regex.NFA.get_eq_nodes_get (nfa : NFA) (i : Nat) (h : i < nfa.nodes.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.nodes.size) (eq : nfa[i] = Node.save tag next) :

tag ≤ nfa.maxTag

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

start_lt : nfa.start < nfa.nodes.size
inBounds (i : Fin nfa.nodes.size) : nfa[i].inBounds nfa.nodes.size

Instances For

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

nfa.WellFormed ↔ nfa.start < nfa.nodes.size ∧ ∀ (i : Fin nfa.nodes.size), nfa[i].inBounds nfa.nodes.size

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

node.inBounds nfa.nodes.size

theorem Regex.NFA.done_WellFormed :

done.WellFormed

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

Decidable nfa.WellFormed

Equations

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