Repository navigation
feat(Parsing): add the chapter from CSwFP/9.1–9.2 - #45
Open
arademaker wants to merge 1 commit into
Open
arademaker wants to merge 1 commit into
arademaker wants to merge 1 commit into
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
| | .leaf a => toString a | ||
| | .branch b ts => | ||
| "[." ++ toString b ++ " " ++ | ||
| toString (ts.map toText) ++ "]" |
| #eval split2 "Jan".toList | ||
|
|
||
| def splitN {α : Type} : Nat → List α → List (List (List α)) | ||
| | 0, _ | 1, _ => [] |
| (x :: us, vs)) | ||
|
|
||
| def splitN' {α : Type} : Nat → List α → List (List (List α)) | ||
| | 0, _ | 1, _ => [] |
| #doc (Manual) "Análise sintática" => | ||
| %%% | ||
| tag := "Parsing" | ||
| htmlSplit := .never |
Comment on lines
+68
to
+70
| - Ela termina: `ys` tem dois elementos a menos. Uma regra recursiva à | ||
| esquerda, V → V T, também não seria problema, porque V recebe um pedaço | ||
| menor da entrada, desde que o pedaço de T não seja vazio. |
This branch has not been deployed
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). Only 9.1 and 9.2 are written,tersefirst; thefulltext is marked with:::dev BeforeNextReleaseTODOs.ParseTree, positions, and the tree relations as lists of pairs; exercises 9.1–9.5.partial def; agreement with Mathlib'sList.Palindromechecked up to length 6 bynative_decide; exercise 9.6 (9.7 is absorbed into the cue onpartial def).CSwFP.yaml,DEVIATIONS.md,STYLE-CODE.mdandcheck-cswfp.pyare updated.Conflicts with the
Compositionpull request inBook.lean,CSwFP.yaml,DEVIATIONS.md,STYLE-CODE.mdandcheck-cswfp.py; they will be resolved by mergingmainhere once that one is in, withParsingplaced afterComposition.🤖 Generated with Claude Code
https://claude.ai/code/session_01UFZtiDzfskeJTJ2ntCt2vh