From 0a85280b0588629a05149e07934759f83f7bd83e Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Tue, 25 Aug 2026 20:51:12 +0200 Subject: fix(of): correct season citation, note All Souls gap, guard transfer search Fix wave from the final whole-branch review of OF Phase 2 (0 Critical, 5 Important, 8 Minor). Applies the five items ruled in-scope and records two more, per the controller's R7/R8/R9 rulings. Fixes: - temporal_of.ml: season-boundary header cited "Normae n. 71-77", a range that does not exist (the Normae end at n. 61) and collides with real IGMR nn. 71-77 (Preparation of the Gifts) in the same PDF -- EF leakage from RG 71-77. Corrected to Normae Titulus II, nn. 17-47, with a note against reintroducing the wrong range. - precedence_of.ml entry 3: added the Tabula's second clause (Commemoratio omnium fidelium defunctorum / All Souls) to the comment, and recorded the Phase 3 hazard -- Vocab_of.rank has no constructor for it yet, and every natural tagging choice gets 2 November's precedence wrong in a different way. No code change; nothing can construct the entity yet. - precedence_of.ml transfer_target's search: added a domain_max_date guard (following Rite_ef.Precedence_ef's existing shape and reasoning) so the walk can no longer probe Computus past 9999-12-31, and it now returns the last date visited on bound exhaustion instead of failwith-ing. .mli updated to drop the @raise Failure clause. - precedence_of.ml is_privileged_sunday: added its own inline Tabula I.2 citation, matching its sibling helpers. - precedence_of.ml entry 10: trimmed the reused "universal or temporal-origin" comment -- Temporal_of never constructs a Memoria_obligatoria candidate, so the temporal-origin half was vacuous there. Recorded without fixing (both comment-only, per explicit scope ruling): - test_precedence_of.ml: corrected the entry-3 Nativity Vigil test's characterisation. The pinned band-30 assertion (2026-12-24, a Thursday) is correct, but is not the value on a 24-December Sunday (e.g. 2028, 2034), where is_privileged_sunday instead bands the same candidate 20. Named the underlying Phase 1 defect this exposes -- named() claims 24 December unconditionally and is matched before sunday_slug, so the Fourth Sunday of Advent gets no office at all in those years, invisible to the litcal layer -- as known and carried to the next task. - precedence_of.mli transfer_target: documented Normae n. 56(f) (St Joseph on Palm Sunday anticipates backward to 18 March) as a known, cited, unimplemented fourth transfer rule, and named the underlying kernel constraint (Rite.t.transfer_target's strictly-later obligation, justified only by the EF's RG 96) as the reason a real fix needs a kernel change. dune test: 799 tests, exit 0. make check (exhaustive sweep): 805 tests, exit 0, 224.7s. No kernel/rite_ef/data changes (git diff empty). --- lib/rites/rite_of/precedence_of.ml | 84 +++++++++++++++++++++++++++++++------- 1 file changed, 70 insertions(+), 14 deletions(-) (limited to 'lib/rites/rite_of/precedence_of.ml') diff --git a/lib/rites/rite_of/precedence_of.ml b/lib/rites/rite_of/precedence_of.ml index 2fab64d..ab5e394 100644 --- a/lib/rites/rite_of/precedence_of.ml +++ b/lib/rites/rite_of/precedence_of.ml @@ -73,6 +73,9 @@ let is_triduum ctx = List.mem (easter_offset ctx) [ -2; -1; 0 ] let entry_2_named = [ "of-nativity"; "of-epiphany"; "of-ascension"; "of-pentecost"; "of-ash-wednesday" ] +(* Tabula I.2's own words for this clause: "Dominicae Adventus, Quadragesimae + et Paschae" -- the same three seasons Normae n. 5 privileges, and the + predicate transfer_target's rule 2 (below) re-uses. *) let is_privileged_sunday (ctx : Vocab_of.season Precedence.context) c = ctx.weekday = Date.Sun && (match ctx.season with @@ -135,7 +138,27 @@ let band (ctx : Vocab_of.season Precedence.context) then 20 (* Tabula I.2 *) else if c.cel.rank = Vocab_of.Sollemnitas && not (is_proper layer) then 30 (* Tabula I.3 -- universal or temporal-origin, never proper; see the - [is_proper] comment above for why this is not [is_universal] *) + [is_proper] comment above for why this is not [is_universal]. + + ENTRY 3 HAS A SECOND CLAUSE THIS BRANCH DOES NOT IMPLEMENT (transcription + line 840, identical in the 1969 Calendarium at OCR line 936): + "Commemoratio omnium fidelium defunctorum" -- All Souls, 2 November. + Nothing constructs it: there is no sanctoral data yet (Phase 3), and + Vocab_of.rank has no constructor for it -- the 2002 Calendarium prints + 2 November UNGRADED ("Omnium Fidelium defunctorum" / "Commemoratio + omnium Fidelium defunctorum"), so the natural rank tag is ambiguous: + Memoria_obligatoria (band 100, loses to a per annum Sunday, WRONG), + Memoria_ad_libitum (band 120, worse), or Sollemnitas (band 30, the + right precedence but a rank word the source never applies to this + day). The 1969 Calendarium's own printing of this clause additionally + carries a qualifier the 2002 text drops -- "quae tamen locum cedit + dominicae occurrenti" -- an edition difference Phase 3 will also need. + PHASE 3 HAZARD: transcribing 2 November with the natural ungraded + rank will silently make it an ordinary weekday whenever it falls on a + Sunday, with every test in this branch still green, because no test + here knows entry 3 has a second clause. Phase 3 must settle how this + day is tagged (or add a dedicated slug test here, mirroring + [entry_2_named]) before shipping OF sanctoral data. *) else if c.cel.rank = Vocab_of.Sollemnitas && is_proper layer then 40 (* Tabula I.4 *) else if c.cel.rank = Vocab_of.Festum && c.cel.subject = Subject.Lord @@ -150,8 +173,11 @@ let band (ctx : Vocab_of.season Precedence.context) && (is_late_advent_feria ctx || is_nativity_octave_day ctx || is_lenten_feria ctx) then 90 (* Tabula II.9 *) else if c.cel.rank = Vocab_of.Memoria_obligatoria && not (is_proper layer) then - 100 (* Tabula III.10 -- universal or temporal-origin, never proper; see the - [is_proper] comment above for why this is not [is_universal] *) + 100 (* Tabula III.10 -- universal or proper; the [layer] test is what + separates entry 10 from entry 11. Unlike entries 3, 5 and 7, "or + temporal-origin" does not apply here: Temporal_of constructs no + Memoria_obligatoria candidate at all (only Sollemnitas, Festum and + Feria), so no temporal candidate ever reaches this branch. *) else if c.cel.rank = Vocab_of.Memoria_obligatoria && is_proper layer then 110 (* Tabula III.11 *) else if c.cel.rank = Vocab_of.Memoria_ad_libitum then @@ -283,14 +309,39 @@ let rules : (Vocab_of.season, Vocab_of.rank) Precedence.rules = whose occupant bands ABOVE 80 (entry 8 x 10). TERMINATION, which Rite.t.transfer_target requires the rite to guarantee: - the search is bounded at [max_search_days] steps and raises if exhausted. - That bound is STRUCTURAL -- it does not appeal to the real calendar's own - shape -- because Calendar's round guard bounds ROUNDS, not the internal - search of a single call, and an unbounded walk would hang the caller - outright before that guard was ever consulted. *) + the search is bounded at [max_search_days] steps AND at {!domain_max_date}, + and returns the last date visited -- never raises -- if either bound is + reached before a free day is found. That bound is STRUCTURAL -- it does + not appeal to the real calendar's own shape -- because Calendar's round + guard bounds ROUNDS, not the internal search of a single call, and an + unbounded walk would hang the caller outright before that guard was ever + consulted; the domain bound additionally prevents the walk from ever + calling [occupant] on a date {!Computus.gregorian_easter} cannot construct + (see {!domain_max_date}'s own comment). *) let max_search_days = 400 +(* The domain's own ceiling ({!Date.make}'s documented 1583..9999 bound, also + duplicated by calendar.ml's own [domain_max_date] for the same reason: + neither module exposes it to the other, and this is a three-line constant, + not worth a new signature just to share it). [search] below must never + call [occupant]/[free] on a date past this: [occupant] chains through the + rite's own [temporal] ([season_of], via [Temporal_of.temporal]), which + calls [Computus.gregorian_easter], NOT total outside 1583..9999 -- it + builds a [Date.t] via [Date.make] and [failwith]s on [Error]. [Date.add_days] + itself has no such limit (documented "unbounded total arithmetic"), so a + walk CAN advance [d] past 31 December 9999 without raising by itself -- the + raise would only happen on the NEXT [occupant]/[free] call, exactly the bug + this guards against: a proper solemnity (band 40) or proper feast (band 80, + NOT > [entry_8_band]) [Add]-ed by an overlay across 26-31 December leaves + only Class2-equivalent Nativity-octave days for the rest of civil year + 9999, so an unguarded walk would reach 1 January 10000 and crash there -- + reachable through the project's own overlay mechanism, the identical shape + Rite_ef.Precedence_ef's own [domain_max_date] documents and fixes + (precedence_ef.ml:1856-1875). *) +let domain_max_date = + match Date.make ~year:9999 ~month:12 ~day:31 with Ok d -> d | Error e -> failwith e + let annunciation_slug = "of-annunciation" (* Tabula entries 1-8, scaled: a day is FREE to receive a transfer when its @@ -333,13 +384,18 @@ let transfer_target (c : Vocab_of.rank Precedence.candidate) (origin : Date.t) in band ctx cand > entry_8_band in + (* Stops, without calling [free] (and so without calling [occupant]) + again, once [d] passes {!domain_max_date} -- see that constant's own + comment for why probing past it can raise. Either way the last date + visited is returned WITHOUT a further [free] probe -- one more finite + (not necessarily free) date, not a further search -- because the + value the caller is still owed is "a date", never an exception; + {!Colitur_kernel.Calendar}'s own [~start ~stop] bound is what turns an + implausible non-terminating real search into a recorded [omitted], + not this function pretending to have found something free. Same + shape as Rite_ef.Precedence_ef.search_from. *) let rec search d steps = - if steps > max_search_days then - failwith - (Printf.sprintf - "Precedence_of.transfer_target: no day free of Tabula entries \ - 1-8 within %d days of %s" - max_search_days (Date.to_iso8601 origin)) + if steps > max_search_days || Date.compare d domain_max_date > 0 then d else if free d then d else search (Date.add_days d 1) (steps + 1) in -- cgit v1.3