Skip to content

Commit

Permalink
fix: make hyphen special in regex classes
Browse files Browse the repository at this point in the history
  • Loading branch information
fgdorais committed Dec 23, 2023
1 parent 885d929 commit 5be007a
Showing 1 changed file with 4 additions and 11 deletions.
15 changes: 4 additions & 11 deletions Parser/RegEx/Compile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,8 @@ import Parser.RegEx.Basic
* `[c]` matches one character from the class `c`.
* `[^c]` matches one character not in the class `c`.
Character classes support single characters and character ranges. The special characters `\`,
`[`, `]` must be preceded by an escape character `\` within a class.
Character classes support single characters and character ranges. The special characters `-`,
`[`, `\`, `]` must be preceded by an escape character `\` within a class.
-/


Expand Down Expand Up @@ -116,20 +116,13 @@ where
let _ ← char ')'
return if n then e else .group e

-- setLoop (cs : List Char) := do
-- match ← option? <| tokenFilter (!['[', ']'].elem .) with
-- | some c =>
-- let c ← if c == '\\' then esc else pure c
-- setLoop (c :: cs)
-- | none => return cs

setLoop (filter : Char → Bool) : REParser (Char → Bool) := do
match ← option? <| tokenFilter (!['[', ']'].elem .) with
match ← option? <| tokenFilter (!['-', '[', ']'].elem .) with
| some c =>
let c ← if c == '\\' then esc else pure c
let f ← try withBacktracking do
let _ ← char '-'
let c' ← tokenFilter (!['[', ']'].elem .)
let c' ← tokenFilter (!['-', '[', ']'].elem .)
let c' ← if c' == '\\' then esc else pure c'
pure <| fun x => c ≤ x && x ≤ c'
catch _ =>
Expand Down

0 comments on commit 5be007a

Please sign in to comment.