majiayu000 Parsing Skill: lean4-parser Library
When parsing structured input (especially for AoC puzzles), use the lean4-parser library instead of manual string splitting.
Installation
Already configured in lakefile.toml:
[[require]]
name = "Parser"
git = "https://github.com/fgdorais/lean4-parser"
rev = "main"
Import
import Parser
open Parser Char
Quick Reference
Parser Types
-- Use SimpleParser for good error messages
abbrev MyParser := SimpleParser Substring Char
Running Parsers
match myParser.run inputString with
| .ok _ result => -- use result
| .error _ e => -- handle error
Common Combinators
| Combinator | Description |
|---|---|
ASCII.parseNat |
Parse natural number |
ASCII.parseInt |
Parse signed integer |
char c |
Match exact character |
string s |
Match exact string |
space, whitespace |
Whitespace matching |
eol |
End of line (LF or CRLF) |
endOfInput |
Assert at end of input |
takeMany p |
Zero or more, collect results |
dropMany p |
Zero or more, discard |
sepBy p sep |
Items separated by delimiter |
first [p1, p2] |
Try alternatives |
test p |
Check without consuming (returns Bool) |
optional p |
Zero or one |
Example: Parse Numbers from Line
def parseLine : SimpleParser Substring Char (List Nat) := do
sepBy ASCII.parseNat (dropMany1 (char ' '))
Example: Parse Coordinates
def parseCoord : SimpleParser Substring Char (Int × Int) := do
let _ ← char '('
let x ← ASCII.parseInt
let _ ← char ','
dropMany space
let y ← ASCII.parseInt
let _ ← char ')'
return (x, y)
Example: Parse Key-Value Pairs
def parseKeyValue : SimpleParser Substring Char (String × Int) := do
let key ← takeMany1 alpha
let _ ← char ':'
dropMany space
let value ← ASCII.parseInt
return (⟨key⟩, value)
Example: Parse with Alternatives
def parseDirection : SimpleParser Substring Char Int := first [
string "up" *> pure 1,
string "down" *> pure (-1),
string "left" *> pure 0,
string "right" *> pure 0
]
Example: Looping Until End
def parseAll : SimpleParser Substring Char (List Int) := do
let mut results := []
while !(← test endOfInput) do
let n ← ASCII.parseInt
results := results ++ [n]
dropMany (char ' ' <|> char '\n')
return results
Documentation
- Full docs: https://www.dorais.org/lean4-parser/doc/
- Repository: https://github.com/fgdorais/lean4-parser