feat(Parsing): add the chapter from CSwFP/9.1–9.3

Bib.lean

@@ -50,6 +50,12 @@ def love2026 : Article where
   number  := inlines!""
   url     := "https://github.com/lean-forward/logical_verification_2026"
 
+def danielsson2010 : InProceedings where
+  title     := inlines!"Total Parser Combinators"
+  authors   := #[inlines!"Nils Anders Danielsson"]
+  year      := 2010
+  booktitle := inlines!"Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010)"
+
 def FPiL : Article where
   title   := inlines!"Functional Programming in Lean"
   authors := #[inlines!"David Thrane Christiansen"]

Book.lean

@@ -10,6 +10,7 @@ import CSwL.Morphology
 import CSwL.InfEngine
 import CSwL.ModelChecking
 import CSwL.Composition
+import CSwL.Parsing
 
 import VersoManual
 
@@ -37,3 +38,4 @@ set_option verso.code.warnLineLength 80
 {include CSwL.InfEngine}
 {include CSwL.ModelChecking}
 {include CSwL.Composition}
+{include CSwL.Parsing}

CSwFP.yaml

@@ -158,6 +158,25 @@ exercises:
     7.26 (p. 180): deferred with 7.7 (issue 43)
     7.27 (p. 181): deferred with 7.7 (issue 43)
     7.28 (p. 182): deferred with 7.7 (issue 43)
+  CSwFP/9:
+    9.1 (p. 208): imm-dominance
+    9.2 (p. 210): c-command-dominance
+    9.3 (p. 210): mutual-c-command
+    9.4 (p. 211): imm-precedence
+    9.5 (p. 211): command
+    9.6 (p. 214): split-nonempty
+    9.7 (p. 214): absorbed into the cue on termination, which says why left
+      recursion is no trouble for recognition by splitting
+    9.8 (p. 217): symbol-satisfy
+    9.9 (p. 222): absorbed into the closing cue of parser-combinators, which
+      says why left recursion makes a parser loop
+    9.10 (p. 237): TODO
+    9.11 (p. 241): TODO
+    9.12 (p. 244): TODO
+    9.13 (p. 246): TODO
+    9.14 (p. 248): TODO
+    9.15 (p. 257): TODO
+    9.16 (p. 259): TODO
 
 original:
   IntroL.lean: [sum-of-squares, sum-to, sum-list, count-zeros]
@@ -205,6 +224,7 @@ original:
     - left-mon-pattern # from the prose on ↑MON and ↓MON in 7.2, "left to the reader"
     - lang-and-or     # from the prose on quantifier automata in 7.2
     - all-kstar       # from the prose in 7.2, "all corresponds to the regular language 1∗"
+  Parsing/Combinators.lean: [parse-many-as]
 
 depends:
   bangu-proof: bangu-form
@@ -336,7 +356,17 @@ sections:
         reach looked of little use (issue 43).
     7.8 Further Reading: omitted
   CSwFP/8 Extension and Intension: not yet taken up
-  CSwFP/9 Parsing: not yet taken up
+  CSwFP/9:
+    9.1 Talking About Parse Trees: Parsing
+    9.2 Recognizing and Parsing Context-Free Languages: Parsing
+    9.3 Parsers and Parser Combinators: Parsing, without the Mastermind
+      parser, since Mastermind is dropped with 5.4
+    9.4 Features and Categories: Parsing, not yet written
+    9.5 Lexical Lookup and Scanning: Parsing, not yet written
+    9.6 Parsing Categories: Parsing, not yet written
+    9.7 Handling Extractions: Parsing, not yet written
+    9.8 Adding Semantics: Parsing, not yet written
+    9.9 Further Reading: omitted
   CSwFP/10 Handling Relations and Scoping: not yet taken up
   CSwFP/11 Continuation Passing Style Semantics: not yet taken up
   CSwFP/12 Discourse Representation and Context: not yet taken up

CSwL/Parsing.lean

@@ -0,0 +1,50 @@
+import CSwLMeta
+import Bib
+import CSwL.Parsing.ParseTrees
+import CSwL.Parsing.Recognition
+import CSwL.Parsing.Combinators
+
+open Verso.Genre Manual
+open CSwLMeta
+
+#doc (Manual) "Análise sintática" =>
+%%%
+tag := "Parsing"
+file := "Parsing"
+%%%
+
+:::dev NOW
+Plan. The headings follow CSwFP/9.1–9.8 (9.9, further reading, is
+omitted). Sections are written `terse` first (see `STYLE-CODE.md`).
+
+- 9.1: `ParseTree α β`, positions, and the tree relations as lists of
+  pairs; dominance with Lean's `<+:`.
+- 9.2: recognition and parsing by splitting, for the palindrome grammar,
+  total by `termination_by`; agreement with Mathlib's `List.Palindrome`
+  proved for every word over `{a, b, c}`.
+- 9.3: list-of-successes parsers as `StateT (List α) List`, with
+  Mathlib's `Monad`/`Alternative List`; recursive parsers are
+  `partial def`. Lean's `Std.Internal.Parsec` returns one result, not
+  all parses; it can serve the lexer of 9.5.
+- 9.4–9.8: to plan. The representation of `Cat` is tied to issue 42.
+:::
+
+:::terse
+- Até aqui as árvores sintáticas eram construídas à mão. Agora o caminho
+  é o inverso: partir de uma sequência de palavras e encontrar as árvores
+  que a gramática lhe atribui.
+- Primeiro, relações entre os nós de uma árvore. Depois, reconhecer e
+  analisar linguagens livres de contexto.
+:::
+
+::::full
+:::dev BeforeNextRelease
+TODO: translate the CSwFP/9 summary.
+:::
+::::
+
+{include 1 CSwL.Parsing.ParseTrees}
+
+{include 1 CSwL.Parsing.Recognition}
+
+{include 1 CSwL.Parsing.Combinators}