inductive Parser.RegEx : Type u_1 → Type u_1

Type of regular expressions

• set {α : Type u_1} : (α → Bool) → RegEx α

  Character set

• alt {α : Type u_1} : RegEx α → RegEx α → RegEx α

  Alternation

• cat {α : Type u_1} : RegEx α → RegEx α → RegEx α

  Concatenation

• repMany {α : Type u_1} : RegEx α → RegEx α

  Unbounded repetition

• repUpTo {α : Type u_1} : Nat → RegEx α → RegEx α

  Bounded repetition

• group {α : Type u_1} : RegEx α → RegEx α

  Grouping

def Parser.RegEx.depth {α : Type u_1} : RegEx α → Nat

Grouping depth

Equations

• (Parser.RegEx.set a).depth = 0
• (e₁.alt e₂).depth = e₁.depth + e₂.depth
• (e₁.cat e₂).depth = e₁.depth + e₂.depth
• e.repMany.depth = e.depth
• (Parser.RegEx.repUpTo a e).depth = e.depth
• e.group.depth = e.depth + 1

def Parser.RegEx.fail {α : Type u_1} : RegEx α

Empty character set

Equations

• Parser.RegEx.fail = Parser.RegEx.set fun (x : α) => false

instance Parser.RegEx.instInhabited (α : Type u_1) : Inhabited (RegEx α)

Equations

• Parser.RegEx.instInhabited α = { default := Parser.RegEx.fail }

def Parser.RegEx.any {α : Type u_1} : RegEx α

Universal character set

Equations

• Parser.RegEx.any = Parser.RegEx.set fun (x : α) => true

def Parser.RegEx.nil {α : Type u_1} : RegEx α

Nil expression

Equations

• Parser.RegEx.nil = Parser.RegEx.repUpTo 0 default

def Parser.RegEx.opt {α : Type u_1} (e : RegEx α) : RegEx α

Optional

Equations

• e.opt = Parser.RegEx.repUpTo 1 e

def Parser.RegEx.rep {α : Type u_1} (n : Nat) (e : RegEx α) : RegEx α

Repetition

Equations

• Parser.RegEx.rep 0 e = Parser.RegEx.repUpTo 0 e
• Parser.RegEx.rep 1 e = e
• Parser.RegEx.rep n_2.succ e = e.cat (Parser.RegEx.rep n_2 e)

def Parser.RegEx.repMany1 {α : Type u_1} (e : RegEx α) : RegEx α

Unbounded repetition, at least once

Equations

• e.repMany1 = e.cat e.repMany

def Parser.RegEx.repManyN {α : Type u_1} (n : Nat) (e : RegEx α) : RegEx α

Unbounded repetition, at least n times

Equations

• Parser.RegEx.repManyN 0 e = e.repMany
• Parser.RegEx.repManyN n_2.succ e = e.cat (Parser.RegEx.repManyN n_2 e)

partial def Parser.RegEx.foldr {ε σ α β : Type (max u_1 u_2)} [Parser.Stream σ α] [Parser.Error ε σ α] {m : Type (max u_1 u_2) → Type u_3} [Monad m] (f : α → β → β) : RegEx α → ParserT ε σ α m β → ParserT ε σ α m β

Fold over a regex match from the right

def Parser.RegEx.take {ε σ α : Type (max u_1 u_2)} [Parser.Stream σ α] [Parser.Error ε σ α] {m : Type (max u_1 u_2) → Type u_3} [Monad m] (re : RegEx α) : ParserT ε σ α m (List α)

take re parses tokens matching regex re returning the list of tokens, otherwise fails

Equations

• re.take = Parser.RegEx.foldr (fun (x1 : α) (x2 : List α) => x1 :: x2) re (pure [])

def Parser.RegEx.drop {ε σ α : Type} [Parser.Stream σ α] [Parser.Error ε σ α] {m : Type → Type u_1} [Monad m] (re : RegEx α) : ParserT ε σ α m Unit

drop re parses tokens matching regex re, otherwise fails

Equations

• re.drop = Parser.RegEx.foldr (fun (x : α) => id) re (pure ())

def Parser.RegEx.count {ε σ α : Type} [Parser.Stream σ α] [Parser.Error ε σ α] {m : Type → Type u_1} [Monad m] (re : RegEx α) : ParserT ε σ α m Nat

count re parses tokens matching regex re returning the number of tokens, otherwise fails

Equations

• re.count = Parser.RegEx.foldr (fun (x : α) => Nat.succ) re (pure 0)

def Parser.RegEx.match {ε σ α : Type (max u_1 u_2)} [Parser.Stream σ α] [Parser.Error ε σ α] {m : Type (max u_1 u_2) → Type u_3} [Monad m] (re : RegEx α) : ParserT ε σ α m (Array (Option (Stream.Segment σ)))

Parses tokens matching regex re returning all the matching group segments, otherwise fails

Equations

• re.match = Parser.RegEx.match.loop re 0 (mkArray re.depth none)

partial def Parser.RegEx.match.loop {ε σ α : Type (max u_1 u_2)} [Parser.Stream σ α] [Parser.Error ε σ α] {m : Type (max u_1 u_2) → Type u_3} [Monad m] : RegEx α → Nat → Array (Option (Stream.Segment σ)) → ParserT ε σ α m (Array (Option (Stream.Segment σ)))