diff options
| -rw-r--r-- | lib/rites/rite_ef/rubrics_ef.ml | 70 | ||||
| -rw-r--r-- | test/test_rubrics_ef.ml | 156 |
2 files changed, 215 insertions, 11 deletions
diff --git a/lib/rites/rite_ef/rubrics_ef.ml b/lib/rites/rite_ef/rubrics_ef.ml index eef86cb..6345399 100644 --- a/lib/rites/rite_ef/rubrics_ef.ml +++ b/lib/rites/rite_ef/rubrics_ef.ml @@ -160,7 +160,48 @@ let creed ~(temporal : (Vocab_ef.season, Vocab_ef.rank) Temporal.t) liturgical action has no Mass in the 1955-restored Holy Week to begin with, so the question is moot there independent of this check -- but this structural test correctly excludes it too, since - it is also named in RG 23(b).) *) + it is also named in RG 23(b).) + + RG 24-25 (immediately following, same Caput IV) name TWO MORE + ferial classes this branch does not reach: feriae II classis (RG + 24 -- the Advent ferias 17-23 December, and the Quatuor Temporum + sets of Advent, Lent and September) and feriae III classis (RG 25 + -- the numbered Lenten/Passiontide ferias from the Thursday after + Ash Wednesday to the Saturday before Passion Sunday II, and the + un-Embered Advent ferias to 16 December). NEITHER is excluded by a + check anywhere in this module -- this branch and RG 33's vigil + branch immediately below are the whole of what [creed] tests + before falling through to 475(b)/(c)/(e)'s own rank/subject/slug + guards. They do not need an explicit exclusion of their own for + 475(b): temporal_ef.ml's own [ferial_rank] never returns [Class1] + for them (only Ash Wednesday and Holy Week do, RG 23's own population, + already excluded above), so that branch is unreachable for them + regardless of anything checked here. But RG 24's own II-class set + DOES reach 475(c)'s [Class2] guard below, and 475(e)'s + apostle-slug guard carries no rank floor at all, so both classes + genuinely reach a live branch of this function. Getting [false] + there is NOT established by this exclusion, or by any check in + this file: it rests on an unstated property of {!Temporal_ef} -- + every ferial-origin office it builds carries [subject = Temporal] + and an "ef-"-prefixed slug, never [Lord]/[Bvm] or a name on + {!creed_apostle_slugs}. Verified directly in temporal_ef.ml: the + Ember/Rogation/generic-ferial branches all go through [build]'s + own default [subject = Temporal], with exactly two documented + exceptions, neither able to reach a live branch below -- the + Sacred Triduum ([subject = Lord], but [Class1], already excluded + above) and the votive Office of the BVM on Saturday, RG 91 entry + 27 ([subject = Bvm], but [Class4], never satisfying 475(c)'s own + [Class2] guard). + + (CORRECTED, review fix: this comment, and 475(b)'s own immediately + below, previously read as though "the two exclusions immediately + above" disposed of ferias in general -- they dispose of feria I + classis only. RG 24/25's own higher classes were excluded by NO + check, an unstated-invariant gap now named here rather than + silently relied on: test/test_rubrics_ef.ml's own ferial-invariant + sweep now asserts the Temporal_ef property above directly against + real output, so a future change that broke it would fail that + test rather than silently changing the Creed.) *) n = -46 || (n >= -6 && n <= -1) then false else if @@ -183,13 +224,17 @@ let creed ~(temporal : (Vocab_ef.season, Vocab_ef.rank) Temporal.t) then false else if (* RG 475(b): "in festis I classis". Genuine feasts only, by - construction of the two exclusions immediately above (feriae, - vigils) -- every remaining [Class1] candidate reaching this branch - is a real festum: the Nativity, Epiphany, Ascension, Corpus Christi, - the Sacred Heart, Christ the King, a I-class sanctoral feast (the - Assumption, the Immaculate Conception...), or a I-class Sunday - (already [true] above via 475(a), so this branch is never the FIRST - to grant those a [true], only ever redundant with it). *) + construction of the two exclusions immediately above (feria I + classis -- Ash Wednesday and Holy Week, the only feriae that are + ever [Class1]; RG 24/25's II- and III-class feriae are a different + population and never reach this rank at all, see the RG 23 + comment's own note above -- and vigils) -- every remaining + [Class1] candidate reaching this branch is a real festum: the + Nativity, Epiphany, Ascension, Corpus Christi, the Sacred Heart, + Christ the King, a I-class sanctoral feast (the Assumption, the + Immaculate Conception...), or a I-class Sunday (already [true] + above via 475(a), so this branch is never the FIRST to grant those + a [true], only ever redundant with it). *) observed.Celebration.rank = Vocab_ef.Class1 then true else if @@ -207,7 +252,14 @@ let creed ~(temporal : (Vocab_ef.season, Vocab_ef.rank) Temporal.t) ships [subject = Saint] instead -- {!Precedence_ef.marian_slugs} is the list built (and, here, reused rather than re-derived) precisely because the [subject] field cannot be trusted alone for this - question; see its own citation in precedence_ef.mli. *) + question; see its own citation in precedence_ef.mli. + + This [Class2] guard is also the one live branch RG 24's own + II-class feriae (Advent 17-23, the Advent/Lent/September Ember + sets) genuinely reach -- the RG 23 comment above (this file, the + [n = -46 ...] branch) has the full account of why they still come + out [false] here: an unstated Temporal_ef property, checked by a + test, not a guard in this file. *) observed.Celebration.rank = Vocab_ef.Class2 && (observed.Celebration.subject = Subject.Lord || observed.Celebration.subject = Subject.Bvm diff --git a/test/test_rubrics_ef.ml b/test/test_rubrics_ef.ml index 2000d61..5109c69 100644 --- a/test/test_rubrics_ef.ml +++ b/test/test_rubrics_ef.ml @@ -9,7 +9,14 @@ this module existed, never read off [Rubrics_ef.creed]'s own answer. Two synthetic unit tests isolate Trap One (RG 475(a) reads [temporal], never [observed]) directly, without depending on finding a real-calendar - coincidence. *) + coincidence. + + One further test (celebrant-rubrics-phase1 review, finding 1) is + different in kind from the rest: not an end-to-end [creed] check + against a single real date, but a direct sweep of {!Rite_ef.Temporal_ef} + output across a century, asserting the unstated invariant [creed]'s own + RG 24/25 ferial branches rely on rather than leaving it asserted only + in prose -- see its own header comment for the full account. *) module Cal = Colitur_kernel.Calendar module LD = Colitur_kernel.Liturgical_day @@ -21,6 +28,7 @@ module Slug = Colitur_kernel.Slug module Temporal = Colitur_kernel.Temporal module V = Rite_ef.Vocab_ef module RE = Rite_ef.Rubrics_ef +module TE = Rite_ef.Temporal_ef let mk y m d = match Date.make ~year:y ~month:m ~day:d with Ok t -> t | Error e -> failwith e @@ -208,6 +216,148 @@ let test_every_sunday_in_2026_says_the_creed () = true d.LD.creed) days +(* ---- Review finding 1 (celebrant-rubrics-phase1 fix task): RG 24/25's + feriae II and III classis (the Advent ferias 17-23 December, the + Advent/Lent/September Ember sets, and the numbered Lenten/Passiontide + ferias) are excluded from the Creed by NO check in rubrics_ef.ml -- see + that file's own RG 23 comment (the [n = -46 ...] branch) for the full + account. [creed]'s correct [false] answer for them rests entirely on an + unstated property of {!Rite_ef.Temporal_ef}: no ferial-origin office it + ever builds carries [subject = Lord] or [subject = Bvm] at [Class2] + (RG 475(c)'s own rank guard), and none carries a slug on + [RE.creed_apostle_slugs] (RG 475(e), which has no rank guard at all). + This test asserts that property directly against real Temporal_ef + output, rather than leaving it asserted only in prose, so a future + Temporal_ef change that breaks it fails HERE loudly instead of silently + changing the Creed. + + Two real, harmless, already-documented exceptions are excluded from the + [subject] checks rather than papered over: the Sacred Triduum + ([subject = Lord], [Class1] -- verified in temporal_ef.ml's own + [triduum_names] branch) and the votive Office of the BVM on Saturday, + RG 91 entry 27 ([subject = Bvm], [Class4] -- {!TE}'s own [is_bvm_saturday] + citation). Neither can ever reach [creed]'s 475(c) branch: the Triduum + is caught earlier by the explicit feria-I-classis check (its own + [Class1] is not [Class2]), and the BVM Saturday Office is [Class4], not + [Class2], so 475(c)'s own rank guard excludes it regardless of subject. + Excluding them here is not a loophole in the test -- it is the precise + boundary of what RG 475(c) actually reads, confirmed rather than + assumed by restricting the [Lord]/[Bvm] checks to exactly [Class2] (RG + 24's own II-class population) and [Class3] (RG 25's III-class + population), the two ranks a real feria can carry that are NOT already + handled by an explicit branch or a rank mismatch. The apostle-slug + check has no such carve-out: it is asserted for every ferial-origin day + of every rank, matching 475(e)'s own unguarded text. + + A THIRD exception -- not anticipated when this test was first written, + found by actually running it, not by inspection -- had to be excluded + from the POPULATION itself, not from the subject checks: RG 17(a)'s own + "secus die 2 ianuarii" fallback (2 January, only in a civil year with + no 2-5 January Sunday) is a genuine FEAST, [subject = Lord], [Class2], + sitting outside {!TE.named}'s table for a purely architectural reason + (temporal_ef.ml's own citation: that table's shape cannot express a + fallback conditional on a per-year fact) and not always a Sunday + either, so neither of [is_ferial_origin]'s two filters caught it on the + first run -- it failed on 1584-01-02 before {!is_holy_name_fallback} + below was added. Left in as evidence the sweep has real teeth rather + than trimmed from the span: excluding a genuine mistaken positive by + name, once found, is the correct fix; narrowing the span to dodge it + would not have been. + + A day is "ferial-origin" here iff {!TE.named} returns [None] for it + (nothing in the fixed/movable table of named feasts, vigils and octave + days claims it), it is not a Sunday (RG 21's own definition: "Nomine + feriae intelleguntur singuli dies hebdomadae, praeter dominicam" -- + every day of the week EXCEPT Sunday), and it is not the RG 17(a) + fallback date just above. *) +let contains_substring ~needle haystack = + let nl = String.length needle and hl = String.length haystack in + let rec loop i = (i + nl <= hl) && (String.sub haystack i nl = needle || loop (i + 1)) in + nl = 0 || loop 0 + +(* RG 17(a)'s own "secus die 2 ianuarii" fallback (temporal_ef.ml's own + citation on [holy_name_fallback_date]): a genuine FEAST, [subject = + Lord], [Class2] -- legitimately outside {!TE.named}'s table only for an + architectural reason (that table's bare [Date.t -> ... option] shape + cannot express a fallback conditional on a per-year fact, + [holy_name_sunday y = None]), never a ferial one, and it is not always + a Sunday, so the weekday filter below does not catch it either. Found + by running this test before this exclusion existed: it failed on + 1584-01-02, a real year with no 2-5 January Sunday. *) +let is_holy_name_fallback (d : Date.t) = + let y = Date.year d in + Date.compare d (TE.holy_name_fallback_date y) = 0 && TE.holy_name_sunday y = None + +let is_ferial_origin (d : Date.t) = + TE.named d = None && Date.weekday d <> Date.Sun && not (is_holy_name_fallback d) + +(* Span: civil years 1583-1682, the domain's own opening century -- every + RG 24/25 population recurs every civil year (Advent 17-23, all three + non-Whitsun Ember sets, and Lenten/Passiontide ferias are none of them + rare or conditional), so one year already gives full COVERAGE; a + century instead of one is for confidence the invariant is not an + accident of a single Easter date, at a cost (day-by-day calls to the + pure {!TE.temporal}, no Calendar/Precedence resolution) cheap enough to + stay in the default, unsampled suite. 1583 is also the domain's own + lower bound, and this span contains 1598, the earliest possible Easter + (22 March) in [1583, 2500] per {!test_easter_extremes} above -- a real, + not merely nominal, edge case. Coverage is VERIFIED below via counters, + not assumed: a test that never actually walks an Ember day would prove + nothing about Ember days. *) +let test_ferial_origin_never_carries_lord_bvm_or_apostle_slug () = + let total = ref 0 + and advent_ember = ref 0 + and lent_ember = ref 0 + and september_ember = ref 0 + and advent_17_23 = ref 0 + and lenten_passiontide_class3 = ref 0 in + for y = 1583 to 1682 do + let dec31 = mk y 12 31 in + let d = ref (mk y 1 1) in + while Date.compare !d dec31 <= 0 do + (if is_ferial_origin !d then begin + let t = TE.temporal !d in + incr total; + let office = t.Temporal.office in + let slug = Slug.to_string office.Cel.slug in + let label = Printf.sprintf "%s (%s, rank=%s)" (Date.to_iso8601 !d) slug + (match office.Cel.rank with + | V.Class1 -> "1" + | V.Class2 -> "2" + | V.Class3 -> "3" + | V.Class4 -> "4") + in + (* Coverage tallies -- checked against zero below. *) + if contains_substring ~needle:"advent-ember" slug then incr advent_ember; + if contains_substring ~needle:"lent-ember" slug then incr lent_ember; + if contains_substring ~needle:"september-ember" slug then incr september_ember; + if Date.month !d = 12 && Date.day !d >= 17 && Date.day !d <= 23 then incr advent_17_23; + if + office.Cel.rank = V.Class3 + && (t.Temporal.season = V.Lent || t.Temporal.season = V.Passiontide) + then incr lenten_passiontide_class3; + (* The invariant itself. Apostle slugs: every rank, no carve-out. *) + Alcotest.(check bool) (label ^ ": not on the apostle-natalicium slug list") false + (List.mem slug RE.creed_apostle_slugs); + (* Lord/Bvm subject: only at the two ranks a real RG 24/25 feria + can carry -- see this test's own header for why Class1 + (Triduum) and Class4 (BVM Saturday) are deliberately excluded. *) + if office.Cel.rank = V.Class2 || office.Cel.rank = V.Class3 then begin + Alcotest.(check bool) (label ^ ": not subject Lord") false (office.Cel.subject = Subject.Lord); + Alcotest.(check bool) (label ^ ": not subject Bvm") false (office.Cel.subject = Subject.Bvm) + end + end); + d := Date.add_days !d 1 + done + done; + Alcotest.(check bool) "span examined a real number of ferial-origin days" true (!total > 10_000); + Alcotest.(check bool) "span reached Advent Ember days" true (!advent_ember > 0); + Alcotest.(check bool) "span reached Lent Ember days" true (!lent_ember > 0); + Alcotest.(check bool) "span reached September Ember days" true (!september_ember > 0); + Alcotest.(check bool) "span reached Advent 17-23 ferias" true (!advent_17_23 > 0); + Alcotest.(check bool) "span reached Lenten/Passiontide III-class ferias" true + (!lenten_passiontide_class3 > 0) + let suite = ( "Rubrics_ef", [ Alcotest.test_case "475(a): ordinary Sunday" `Quick test_475a_ordinary_sunday; @@ -237,4 +387,6 @@ let suite = test_vigil_excluded_even_when_class2_and_marian; Alcotest.test_case "476(d): BVM Saturday Office, IV class" `Quick test_476d_bvm_saturday_office; Alcotest.test_case "every Sunday in 2026 says the Creed" `Quick - test_every_sunday_in_2026_says_the_creed ] ) + test_every_sunday_in_2026_says_the_creed; + Alcotest.test_case "RG 24/25: no ferial-origin office carries Lord/Bvm or an apostle slug" `Quick + test_ferial_origin_never_carries_lord_bvm_or_apostle_slug ] ) |