name	parsing
description	Use the lean4-parser library for parsing structured input. Invoke when implementing parsers for AoC puzzles or other text processing tasks in Lean.
allowed-tools	Read, Edit, Write

Parsing Skill: lean4-parser Library

Name: parsing
Author: kim-em

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

parsing

Install Skill

SKILL.md