Repository navigation
Tags
Tags
feat(Parsing): add the chapter from CSwFP/9.1–9.3 (#45) 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`. 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. 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. 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. 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.