Repository navigation
feat(Parsing): add the chapter from CSwFP/9.1–9.3 - #45
Merged
Merged
Conversation
Start the parsing chapter with CSwFP 9.1 and 9.2, skipping CSwFP 8. Parse trees carry positions and the tree relations of dominance, sisterhood, c-command and precedence, as lists of pairs. Recognition and parsing by splitting the input are shown on the palindrome grammar, with `partial def`, and checked against Mathlib's `List.Palindrome` up to length 6. Exercises 9.1-9.6 are ported; 9.7 goes into the cue on `partial def`. Claude Code (Opus 5.5) drafted these changes and this message under the author's direction; the author reviewed them.
Contributor
There was a problem hiding this comment.
🟡 Changes recommended
The split helpers mishandle unary and zero-piece cases, tree output uses incorrect brackets, and the left-recursion guidance omits a necessary guard.
5 open issues
What changed in this PR
Adds the first two sections of the Parsing chapter, bringing parse-tree relations and palindrome recognition into the Lean textbook. The chapter is written for the terse variant first, with full-prose translations left as explicit TODOs.
Changes:
- Introduces parse trees, positions, tree relations, and exercises.
- Adds splitting-based recognition and parsing, with a bounded check against Mathlib’s palindrome predicate.
- Integrates the chapter into the book and updates coverage tracking and style documentation.
| File | Description |
|---|---|
STYLE-CODE.md |
Records newly introduced Lean features. |
scripts/check-cswfp.py |
Adds the exercise count for CSwFP chapter 9. |
README.md |
Marks Parsing as partially implemented. |
DEVIATIONS.md |
Documents adaptations and omitted material. |
CSwL/Parsing/Recognition.lean |
Adds palindrome recognition, parsing, generation, and splitting exercises. |
CSwL/Parsing/ParseTrees.lean |
Defines trees, position relations, and related exercises. |
CSwL/Parsing.lean |
Assembles the chapter and records remaining plans. |
CSwFP.yaml |
Maps chapter 9 sections and exercises to the port. |
Book.lean |
Imports and includes the Parsing chapter. |
Review effort: Balanced
recognize and parse no longer need partial def. They recurse over
(splitN 3 xs).attach, which pairs each split with a proof that it
belongs to splitN 3 xs, and decreasing_by uses flatten_of_mem_splitN,
the fact that the pieces of a split concatenate to the input, to show
that the middle piece is shorter. Its converse, mem_splitN_flatten,
states that every split is produced; both hold for any n.
With recognize total, the bounded check by native_decide on words up
to length 6 gives way to a proof, in a details block, that recognize
agrees with Mathlib's List.Palindrome on every word over {a, b, c}.
The cues follow: the one on termination keeps exercise 9.7, and the one
before parse says why the trees of all rules are concatenated.
STYLE-CODE.md records the features the chapter now uses for the first
time: termination_by, decreasing_by, List.attach, and rcases and Or.inr
outside a solution. DEVIATIONS.md, CSwFP.yaml and the chapter overview
no longer mention partial def.
AI-usage disclosure: these changes were drafted with the assistance of
Claude Opus 5.5 (Anthropic, via Claude Code), under the author's
direction. The assistant wrote the termination argument and the proofs,
drafted the Portuguese cues, and updated the project's records; the
author reviewed them and takes full responsibility for the final
content.
splitN now covers every number of pieces: one piece is the input itself, and the empty input has the split into zero pieces. CSwFP's version stops with an error below two. The recursion becomes uniform, splitN serves unary rules, and mem_splitN_flatten holds for every list of pieces. The base cases of splitN' in exercise 9.6 sit outside the solution, so they follow suit there. ParseTree.toText separates the daughters of a node by spaces, as in the bracket notation of qtree, instead of printing them as a list. Nothing reads the text back. Parsing is a glue chapter, so it drops htmlSplit := .never and each section gets its file key, as STYLE-CODE.md asks: each section is now its own page and its own generated module. The cue on left recursion says what goes wrong when the piece of T may be empty, and that Lean would then refuse the definition. AI-usage disclosure: these changes were drafted with the assistance of Claude Opus 5.5 (Anthropic, via Claude Code), under the author's direction, in response to an automated review of the pull request. The author reviewed them and takes full responsibility for the final content.
arademaker
changed the title
Section from CSwFP/9.3. A parser is StateT (List α) List β, which unfolds by definition to a function from the input to the list of (result, remainder) pairs; Mathlib's Monad and Alternative instances for List give pure, failure, <|>, <$> and do-notation with the meaning the section needs. Recursive parsers are partial def. Exercise 9.8 becomes symbol-satisfy; 9.9 is answered in the closing cue, with a left-recursive parser that is defined but never run. The Mastermind parser is dropped with Mastermind; parseManyAs, which only it used, becomes the exercise parse-many-as. AI usage: Claude Code (Claude Opus 5.5) drafted the Lean code, the terse cues and the documentation updates under the author's direction; the author reviewed and approved the changes.
Terse cues in ParseTrees and Recognition no longer open a sentence with a lowercase Lean identifier, as STYLE-WRITING.md asks. The cue on pos now says it uses a local let rec helper, not a mutual block. AI usage: Claude Code (Claude Opus 5.5) rewrote the sentences at the author's request; the author reviewed the changes.
AI usage: Claude Code (Claude Opus 5.5) found and fixed the stale references; the author reviewed the change.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds the
Parsingchapter, ported from CSwFP/9 (CSwFP/8 is skipped for now). Sections 9.1–9.3 are written,tersefirst; thefulltext is marked with:::dev BeforeNextReleaseTODOs. Each section is its own page and its own generated module.ParseTrees):ParseTree, positions, and the tree relations as lists of pairs; exercises 9.1–9.5.Recognition): recognition and parsing of palindromes by splitting.recognizeandparseare total (termination_byoversplitN 3 xs |>.attach); a theorem in a:::detailsblock proves thatrecognizeagrees with Mathlib'sList.Palindromeon every word over{a, b, c}. Exercise 9.6; 9.7 is absorbed into the cue on termination.Combinators): list-of-successes parsers asStateT (List α) List β, with Mathlib'sMonad/Alternative Listgivingpure,failure,<|>,<$>anddo. Recursive parsers (palindrome,many) arepartial def. Exercise 9.8 becomessymbol-satisfy;parseManyAsbecomes the new exerciseparse-many-as; 9.9 is answered in the closing cue, with a left-recursive parser that is defined but never run. The Mastermind parser is dropped with Mastermind.CSwFP.yaml,DEVIATIONS.md,STYLE-CODE.md,Bib.leanandcheck-cswfp.pyare updated.Up to date with main, which now has Composition; Parsing comes after it in the book.
🤖 Generated with Claude Code
https://claude.ai/code/session_01UFZtiDzfskeJTJ2ntCt2vh