ch:indexed-inductive-families: ch:indexed-inductive-families
Problem and result. Implement the format-indexed decimal parser in Kappa. For widths 427105 as 427105. The five-digit input 42715 must be rejected at the final field with expected width three and actual width two.
Representation. Use Format for widths. Keep the checked-field and parsed-format types private. Their only constructor path first consumes exactly the declared number of decimal digits. Printing consumes only checked fields, so it cannot silently change a field’s width.
Text boundary. Import graphemes from std.unicode. Its specified type is String -> Query Grapheme; materialize the query with a Kappa list comprehension, map the ten decimal grapheme literals to natural numbers, and reject the first other grapheme. This is the only path from the surface string to the digit stream consumed by the width checker.
First complete version. Define takeExact by structural recursion on a field width. Its Took branch returns the field and unconsumed suffix; its Short branch returns every digit that was available. Parse the field only after takeExact succeeds.
Remaining cases. Thread a zero-based field index through the parser. Reject a digit outside zero through nine, and reject trailing input after all widths are consumed. Extract field values for the accepted oracle. Concatenate the checked digit segments for the printer oracle.
A failing version. In the Short partial branch, return an accepted empty suffix instead of FieldRejected. The program still checks, but the final-field rejection line changes to FAIL.
Acceptance test. Run the four appendix E commands and require the exact three PASS lines, the final summary All 3 Chapter 78 corpus cases passed., and the empty audit [].
Mathematical boundary. The run illustrates a vector of widths controlling construction of a private parsed representation. It does not prove the vector eliminator, coverage, or elimination of case trees without K.