diff options
Diffstat (limited to 'lib/kernel')
| -rw-r--r-- | lib/kernel/liturgical_day.mli | 9 | ||||
| -rw-r--r-- | lib/kernel/validate.ml | 60 | ||||
| -rw-r--r-- | lib/kernel/validate.mli | 23 |
3 files changed, 90 insertions, 2 deletions
diff --git a/lib/kernel/liturgical_day.mli b/lib/kernel/liturgical_day.mli index a109251..f0ea3d9 100644 --- a/lib/kernel/liturgical_day.mli +++ b/lib/kernel/liturgical_day.mli @@ -20,6 +20,13 @@ type ('s, 'r) t = { omitted : ('r Celebration.t * string) list; (** with the reason, never silent -- Task 12's no-celebration-lost invariant reads this *) - citations : Citation.t list; (** always empty until Plan 4 *) + citations : Citation.t list; + (** The day's reading references, resolved by the rite's own + {!Rite.readings}. Empty for a rite whose lectionary is not built; + for EF, exactly one [First] and one [Gospel] on every day of every + year 1583..9999 -- asserted, not assumed, by {!Validate}'s own + ["citations"] / ["citations-unresolved"] checks. (This said "always + empty until Plan 4" until Task 10; the lectionary landed before + Plan 4 did, and the comment outlived its truth.) *) } [@@deriving sexp] diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index ffeb89e..1a0248b 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -388,5 +388,63 @@ let run (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) ~year = "admit is not a fixed point on this day's own commemorations: re-offering %d \ admitted %d back" (List.length offered) (List.length readmitted))) - resolved); + resolved; + (* ---- Citation invariants (the lectionary, Plan 4) ---- + + RITE-AGNOSTIC BY CONSTRUCTION, and this gating is the whole reason + these can live in the kernel beside the temporal checks rather than + in EF's own tests: a rite whose lectionary is not built yet returns + [] from {!Rite.readings} on every day, so [year_has_citations] is + false and not one of these fires. A rite that computes readings AT + ALL is held to all of them, on every day of its year. That is also + why test_validate.ml's own synthetic rite ([readings] a constant + [], "a harmless placeholder" in its own words) stays unaffected -- + checked, not assumed: its negative-path fixtures would otherwise + fail on every day of the year rather than on the one invariant each + is built to violate. + + The single [match] below expresses THREE invariants at once, which + is why it is a match on the sorted part list rather than three + separate tests: + + - zero or two, never one -- an Epistle without a Gospel, or the + reverse, is a malformed Mass, not a partial one; + - only [First] and [Gospel] ever appear -- the chants (Psalm, + Second, Tract, Alleluia, Sequence) are deliberately unbuilt, + with no source and no oracle, so a citation carrying one is a + defect and not a feature arriving early; + - no part appears twice -- two Epistles and no Gospel has length + two and would slip past a bare cardinality test. + + [Citation.part]'s own constructor order puts [First] before + [Gospel], so the sorted well-formed list is literally + [[First; Gospel]] and nothing else. *) + let year_has_citations = + Array.exists + (fun (d : ('s, 'r) Liturgical_day.t) -> d.Liturgical_day.citations <> []) + resolved + in + if year_has_citations then + Array.iter + (fun (d : ('s, 'r) Liturgical_day.t) -> + let date = d.Liturgical_day.date in + let parts = + List.map (fun (c : Citation.t) -> c.Citation.part) d.Liturgical_day.citations + in + match List.sort compare parts with + | [ Citation.First; Citation.Gospel ] -> () + | [] -> + (* Separate check name from the malformed case below on + purpose: this is the lectionary chain falling through + every one of its steps and resolving nothing, a COVERAGE + gap, where the other is a WELL-FORMEDNESS one. They want + different fixes and should be countable apart. *) + fail date "citations-unresolved" + "no reading citations resolved for this day: the lectionary chain fell through \ + every step" + | sorted -> + fail date "citations" + (Printf.sprintf "expected exactly one First and one Gospel, got [%s]" + (String.concat "," (List.map Citation.part_to_string sorted)))) + resolved); List.rev !failures diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli index b46ca30..385e111 100644 --- a/lib/kernel/validate.mli +++ b/lib/kernel/validate.mli @@ -78,6 +78,29 @@ val failure_to_string : failure -> string was not exceeded" available without embedding a rite's specific numeric caps (RG 111's, for EF) into kernel code. + Two further labels (Task 10) check the day's reading {!Citation.t}s. Both + are GATED on the rite producing at least one citation somewhere in the + year: a rite whose lectionary is not built returns [[]] from + {!Rite.readings} on every day and is held to neither, so this stays a + check on rites that HAVE readings rather than a demand that every rite + have them. + - ["citations"]: well-formedness. A day's citation parts, sorted, are + exactly [[First; Gospel]]. This single condition carries three + invariants at once: zero or two but never one (an Epistle without a + Gospel, or the reverse, is a malformed Mass rather than a partial one); + no part outside [First]/[Gospel] (the chants -- Psalm, Second, Tract, + Alleluia, Sequence -- are deliberately unbuilt, so one appearing is a + defect, not a feature arriving early); and no part twice (two Epistles + and no Gospel has length two and would pass a bare cardinality test). + - ["citations-unresolved"]: coverage. A day resolved NO citations at all, + i.e. the rite's own lookup chain fell through every one of its steps. + Deliberately a separate label from ["citations"] above: a coverage gap + and a well-formedness fault want different fixes and should be + countable apart. On the EF data as it stands this label has no live + witness -- every day of every year 1583..9999 resolves exactly one + Epistle and one Gospel -- which is precisely why test_validate.ml + carries a synthetic fixture proving it can fire at all. + Total over the whole 1583..9999 domain, including [year] = 9999: the liturgical year opening there continues into out-of-domain civil year 10000, so the walk is clamped to 31 December 9999 and the checks run |