diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/kernel/calendar.ml | 46 | ||||
| -rw-r--r-- | lib/kernel/rite.mli | 82 | ||||
| -rw-r--r-- | lib/rites/rite_of/precedence_of.ml | 84 | ||||
| -rw-r--r-- | lib/rites/rite_of/precedence_of.mli | 95 | ||||
| -rw-r--r-- | lib/rites/rite_of/rite_of.mli | 9 |
5 files changed, 219 insertions, 97 deletions
diff --git a/lib/kernel/calendar.ml b/lib/kernel/calendar.ml index a1309f9..a8c4725 100644 --- a/lib/kernel/calendar.ml +++ b/lib/kernel/calendar.ml @@ -113,33 +113,43 @@ let occupant_of (rite : ('s, 'r) Rite.t) (idx : 'r Layer.index) let _, _, resolution = resolve_with_injected rite idx injected date in resolution.Precedence.observed.Precedence.cel -(* Hard guard on the placement fixed point (spec §2.4): every genuine +(* Hard guard on the placement fixed point (spec §2.4): almost every transfer moves a celebration strictly forward and the celebration set is finite, so the round below always empties [deferred] within a handful of rounds in practice (an RG 97-98 collision of N feasts on one date costs at most N-1 extra rounds -- each round resolves the winner of whatever pile-up - occurred and re-defers the rest, one fewer each time). 64 is not tuned to - that bound; it is a defensive ceiling nothing in the 1962 calendar comes - close to, so that a rite/data combination this module has not anticipated - fails as a recorded, inspectable [omitted] reason (below) instead of - hanging the CLI. *) + occurred and re-defers the rest, one fewer each time). CORRECTED + (Normae n. 56(f)/W1, 2026-08-26): "every" no longer holds literally -- a + rite MAY now return a target earlier than origin (rite.mli's own + obligation was relaxed from "strictly later" to "different"; see its + comment for the argument) -- but the bound this guard exists for does + not actually rest on direction: [~start]/[~stop] and this round count + both test the target's own value, never a comparison against [origin], + so a bounded backward jump converges the same way a bounded forward one + does. 64 is not tuned to that bound; it is a defensive ceiling nothing + in either shipped calendar comes close to, so that a rite/data + combination this module has not anticipated fails as a recorded, + inspectable [omitted] reason (below) instead of hanging the CLI. *) let max_transfer_rounds = 64 let unconverged_reason = "omitted: transfer placement did not converge within max_transfer_rounds (RG 96-98)" -(* A rite-supplied [transfer_target] is trusted to search strictly forward - (rite.mli), but nothing stops it naming a date past the end of the - liturgical year it was asked about -- e.g. an I-class feast impeded in - the last days before Advent I, whose first admissible day genuinely - falls in the following liturgical year's own territory (unproven to - occur in the real EF calendar, but not something this module can rule - out by construction). [place_transfers] never injects such a target: the - [dates] array is exactly what [year]/[build_day] walk to produce the - result, so a candidate placed outside it would be [observed]/ - [transferred_in] nowhere in the output at all -- gone, not merely - mis-filed, and silently so, contradicting [calendar.mli]'s "never - silently dropped". This reason makes that failure mode visible instead. *) +(* A rite-supplied [transfer_target] is trusted to return a date genuinely + different from its argument and to terminate on its own (rite.mli), but + nothing stops it naming a date past either end of the liturgical year it + was asked about -- e.g. an I-class feast impeded in the last days before + Advent I, whose first admissible day genuinely falls in the following + liturgical year's own territory (unproven to occur in the real EF + calendar, but not something this module can rule out by construction), + or (since Normae n. 56(f)/W1) a backward-anticipated feast impeded close + enough to the liturgical year's own opening that its target lands before + it. [place_transfers] never injects such a target: the [dates] array is + exactly what [year]/[build_day] walk to produce the result, so a + candidate placed outside it would be [observed]/[transferred_in] nowhere + in the output at all -- gone, not merely mis-filed, and silently so, + contradicting [calendar.mli]'s "never silently dropped". This reason + makes that failure mode visible instead. *) let out_of_range_reason = "omitted: transfer target falls outside the liturgical year (RG 96)" (* RG 33: "Vigilia II aut III classis penitus omittitur... vel si festum cui diff --git a/lib/kernel/rite.mli b/lib/kernel/rite.mli index ec850f8..b0ba7ac 100644 --- a/lib/kernel/rite.mli +++ b/lib/kernel/rite.mli @@ -75,24 +75,70 @@ type ('s, 'r) t = { just to answer "what sits here". OBLIGATIONS (not enforced by the type, and {!Calendar}'s own - termination argument depends on both): the result must be - {b strictly later} than the [Date.t] argument (the date the - candidate was impeded on) -- {!Calendar}'s placement pass treats - [target = origin] or [target < origin] as a legitimate placement, - not an error, so a rite whose search can stand still or go - backward would silently loop candidates in place or resurrect an - already-superseded occupant rather than failing loudly. The call - must also {b terminate} on its own: {!Calendar}'s round guard - (calendar.ml's [max_transfer_rounds]) bounds how many ROUNDS the - whole-year placement pass takes, which is a distinct, outer thing - from whatever internal search a single call to this function runs - -- an implementation that walks forward day by day looking for an - admissible date, without its own bound, can hang the caller - outright on a rite/data shape it does not handle, never reaching - the round guard at all. See rite_ef/precedence_ef.ml's - [transfer_target] for a concrete termination argument (a - structural step bound, not an appeal to the real calendar's own - structure). *) + termination argument depends on both): the result must {b differ + from} the [Date.t] argument (the date the candidate was impeded + on) -- {!Calendar}'s placement pass treats [target = origin] as a + legitimate placement, not an error, and {!Precedence.resolve} + itself never deduplicates by slug, so a rite that can stand still + would hand it the SAME candidate twice at the SAME date in the + SAME contest (once via {!Layer.on_date}'s permanent natural + entry, once via the injection this module's placement pass adds) + -- a genuine self-collision (the candidate disposed of as both + [winner] and [loser] against itself), not merely a docstring + worry: reachable the moment any rite returns its argument + unchanged. The call must also {b terminate} on its own: + {!Calendar}'s round guard (calendar.ml's [max_transfer_rounds]) + bounds how many ROUNDS the whole-year placement pass takes, which + is a distinct, outer thing from whatever internal search a single + call to this function runs -- an implementation that walks day by + day (in EITHER direction) looking for an admissible date, without + its own bound, can hang the caller outright on a rite/data shape + it does not handle, never reaching the round guard at all. See + rite_ef/precedence_ef.ml's [transfer_target] for a concrete + termination argument (a structural step bound, not an appeal to + the real calendar's own structure). + + {b EARLIER targets are permitted} (CORRECTED, + [of-normae-56f]/W1, 2026-08-26: this obligation previously read + "strictly later", full stop, and warned that an earlier target + "would silently loop candidates in place or resurrect an + already-superseded occupant rather than failing loudly" -- traced + against the placement pass actually implemented, not merely + against this comment's own prior claim, and found to overstate + the risk). {!Calendar}'s round loop re-resolves the {b entire} + year fresh from the currently-settled [assignment] every round + (never patched incrementally), and its two safety nets -- + [~start]/[~stop] catching a target outside the liturgical year, + and [max_transfer_rounds] catching non-convergence -- both test + the target's value directly ([target < start || target > stop]; + round count) with no comparison against [origin] anywhere, so + neither depends on which side of [origin] the target falls. + "Resurrecting a superseded occupant" cannot occur either: a day's + occupant is decided fresh each round by the same RG 91/Tabula + contest every other day is, so a backward-placed candidate either + wins that contest or is itself deferred and re-targeted like any + other loser -- there is no stale state to resurrect FROM. A + candidate's own permanent loss at its structural origin is + rediscovered every round regardless of target direction and is + filtered as stale under the identical rule either way (actionable + only if never yet assigned, or if the sighting is at the + candidate's OWN current target -- calendar.ml's [place_transfers], + the [deferred] filter's own comment). + + This is a general property of the mechanism, not a special case + carved out for one rite: it holds for ANY single call that + returns a date [<> origin] and terminates on its own, per the two + obligations above. What it does {b not} license is assuming an + UNBOUNDED backward search is safe merely because a bounded one is + -- the termination obligation still falls entirely on the rite, + exactly as it always did for a forward search. The safest shape, + and the only one exercised so far, is a CONSTANT one-shot + displacement for a specifically-named collision (no internal + search at all, hence trivially terminating) -- see + rite_of/precedence_of.ml's [transfer_target] (Normae n. 56(f), St + Joseph anticipated backward onto Palm Sunday) for the concrete + worked example, the same role rite_ef/precedence_ef.ml's own + [transfer_target] plays for a bounded FORWARD search above. *) readings : observed:'r Celebration.t -> temporal:('s, 'r) Temporal.t -> diff --git a/lib/rites/rite_of/precedence_of.ml b/lib/rites/rite_of/precedence_of.ml index 0587f0a..5344374 100644 --- a/lib/rites/rite_of/precedence_of.ml +++ b/lib/rites/rite_of/precedence_of.ml @@ -300,9 +300,22 @@ let vigil_feast (_ : Vocab_of.rank Precedence.candidate) : Slug.t option = None let rules : (Vocab_of.season, Vocab_of.rank) Precedence.rules = { band; disposition; admit; vigil_feast } -(* Normae n. 60 and Normae n. 5 together. THREE rules, in this priority order - -- n. 60's own text defers to n. 5 explicitly ("servatis iis quae n. 5 - statuuntur"), so the two are one rule set, not two competing ones. +(* Normae n. 56(f), n. 60 and n. 5 together. FOUR rules, in this priority + order -- n. 60's own text defers to n. 5 explicitly ("servatis iis quae + n. 5 statuuntur"), and n. 56(f) names the single collision it overrides + outright, so all three are one rule set, not three competing ones. + + 0. ST JOSEPH ON PALM SUNDAY (Normae n. 56(f)): "Sollemnitas S. Ioseph, + ubi est de praecepto servanda, si cum Dominica in palmis de Passione + Domini occurrit, anticipatur sabbato praecedenti, die 18 martii" -- + ANTICIPATED BACKWARD to the preceding Saturday, 18 March, the one + named exception to every other rule here searching or landing + forward. RESOLVED (of-normae-56f/W1, 2026-08-26; previously KNOWN + UNIMPLEMENTED -- see this value's own .mli for the full history, + including why it was blocked on a kernel contract change and what + that change cost). Checked first, ahead of rule 1, because it names + a more specific collision (one candidate, one date shape) than any + rule below. 1. THE ANNUNCIATION IN HOLY WEEK (Normae n. 60): "Sollemnitas vero Annuntiationis Domini, quotiescumque occurrit aliquo die Hebdomadae @@ -328,15 +341,19 @@ 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 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). *) + rules 1-3's 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). Rule 0 needs no bound of its own: it runs no search at + all, computing [Date.add_days origin (-1)] directly, so it terminates + trivially -- the one shape {!Colitur_kernel.Rite.t.transfer_target}'s own + comment names as always safe regardless of direction. *) let max_search_days = 400 @@ -361,8 +378,26 @@ let max_search_days = 400 let domain_max_date = match Date.make ~year:9999 ~month:12 ~day:31 with Ok d -> d | Error e -> failwith e +(* NOTE, found while adding [st_joseph_slug] below, NOT fixed here -- + out of scope for the W1 task this touches: [annunciation_slug] does not + match the real shipped entry's own slug (data/of/calendar-2002.sexp has + "annunciation-of-the-lord", not "of-annunciation"), so Rule 1 below + never actually fires against real sanctoral data -- only against the + synthetic candidate test_precedence_of.ml's own [annunciation] builds + with the same placeholder slug. Whether this is output-visible on real + data was not established either way here; Rule 3's general forward + search is a plausible fallback that could reach the identical Easter+8 + target by coincidence in the one case tested + ([test_annunciation_in_easter_octave]'s own comment says as much for a + collision NOT in Holy Week), but that is not the same claim as "the two + rules always agree", and this was not checked for Holy Week itself. *) let annunciation_slug = "of-annunciation" +(* The real shipped slug (data/of/calendar-2002.sexp) -- St Joseph's own + Rule 0 below is matched against the actual sanctoral entry, not a + placeholder, precisely because the note above exists. *) +let st_joseph_slug = "joseph-husband-of-the-blessed-virgin-mary" + (* Tabula entries 1-8, scaled: a day is FREE to receive a transfer when its occupant bands strictly above entry 8. *) let entry_8_band = 80 @@ -373,9 +408,27 @@ let transfer_target (c : Vocab_of.rank Precedence.candidate) (origin : Date.t) let easter = Computus.gregorian_easter year in let offset d = Date.to_rata d - Date.to_rata easter in let is_holy_week d = offset d >= -7 && offset d <= -1 in - (* Rule 1. *) - if Slug.to_string c.cel.slug = annunciation_slug && is_holy_week origin then - Date.add_days easter 8 + let is_palm_sunday d = offset d = -7 in + (* Rule 0 (Normae n. 56(f)): "Sollemnitas S. Ioseph, ubi est de praecepto + servanda, si cum Dominica in palmis de Passione Domini occurrit, + anticipatur sabbato praecedenti, die 18 martii" -- St Joseph, impeded + by Palm Sunday, is ANTICIPATED BACKWARD to the preceding Saturday, not + carried forward like every other rule here. A fixed one-day + displacement, not a search: [origin] is Palm Sunday itself whenever + this fires (a Sunday, by construction), so "the preceding Saturday" + and "the day before [origin]" are the same date, and computing it this + way -- rather than via [offset]/[easter] -- makes that identity exact + rather than incidental. This is the rite.mli-documented EARLIER-target + shape (rite.mli's own [transfer_target] comment): a single named + collision, no internal search, hence trivially terminating on its own. + Checked ahead of Rules 1-3, most-specific first, the same order this + whole function already keeps. *) + if Slug.to_string c.cel.slug = st_joseph_slug && is_palm_sunday origin then + Date.add_days origin (-1) + else if + (* Rule 1. *) + Slug.to_string c.cel.slug = annunciation_slug && is_holy_week origin + then Date.add_days easter 8 else let season_of d = (Temporal_of.temporal d).Temporal.season in let privileged_sunday d = @@ -384,7 +437,6 @@ let transfer_target (c : Vocab_of.rank Precedence.candidate) (origin : Date.t) | Vocab_of.Advent | Vocab_of.Lent | Vocab_of.Easter -> true | Vocab_of.Christmas | Vocab_of.Ordinary_time -> false in - let is_palm_sunday d = offset d = -7 in let is_easter_sunday d = offset d = 0 in (* Rule 2. *) if diff --git a/lib/rites/rite_of/precedence_of.mli b/lib/rites/rite_of/precedence_of.mli index 4ef81a5..1b9457b 100644 --- a/lib/rites/rite_of/precedence_of.mli +++ b/lib/rites/rite_of/precedence_of.mli @@ -90,6 +90,9 @@ val rules : (Vocab_of.season, Vocab_of.rank) Precedence.rules Normae n. 60 and Normae n. 5 together -- n. 60 defers to n. 5 explicitly ("servatis iis quae n. 5 statuuntur"), so they are one rule set: + - St Joseph, impeded by falling on Palm Sunday, is ANTICIPATED BACKWARD to + the preceding Saturday, 18 March (n. 56(f), a fixed one-day + displacement, checked first as the most specific collision); - the Annunciation falling anywhere in Holy Week goes to Easter + 8, the Monday after the Second Sunday of Easter (n. 60, a fixed destination); - any other solemnity falling on a Sunday of Advent, Lent or Easter goes to @@ -97,52 +100,62 @@ val rules : (Vocab_of.season, Vocab_of.rank) Precedence.rules which n. 5 excludes and which fall through to the general rule; - otherwise, the nearest later day free of Tabula entries 1-8 (n. 60). - KNOWN UNIMPLEMENTED FOURTH RULE, recorded rather than built (final review - Important #5, ledger ruling R9): Normae n. 56(f) -- - "Sollemnitas S. Ioseph, ubi est de praecepto servanda, si cum Dominica in - palmis de Passione Domini occurrit, anticipatur sabbato praecedenti, die - 18 martii" -- St Joseph, where his solemnity is of precept, falling on - Palm Sunday is ANTICIPATED (a BACKWARD transfer) to the preceding - Saturday, 18 March, not carried forward like every rule above. It is - conditional ("ubi est de praecepto servanda") and the following sentence - gives Episcopal Conferences discretion where it is not, so the universal - calendar legitimately not implementing it is defensible; not citing it at - all was not, hence this note. + FOURTH RULE RESOLVED ([of-normae-56f]/W1, 2026-08-26; previously KNOWN + UNIMPLEMENTED here, final review Important #5, ledger ruling R9). Normae + n. 56(f): "Sollemnitas S. Ioseph, ubi est de praecepto servanda, si cum + Dominica in palmis de Passione Domini occurrit, anticipatur sabbato + praecedenti, die 18 martii" -- St Joseph, where his solemnity is of + precept, falling on Palm Sunday is ANTICIPATED (a BACKWARD transfer) to + the preceding Saturday, 18 March, not carried forward like the other + three rules. It is conditional ("ubi est de praecepto servanda") and the + following sentence gives Episcopal Conferences discretion where it is + not; the universal calendar implements the unconditional reading (the + same discipline every other rule here already applies to a Normae + clause with a conference-discretion escape hatch). - CORRECTED: this note previously said "No sanctoral data exists yet - (Phase 3), so nothing is WRONG today" and located the trigger at - "25 March co-occurring with Palm Sunday". Both are now false and were - already wrong about the date: St Joseph is 19 March, not 25 March (25 - March is the Annunciation, a separate solemnity with its own Holy-Week - handling). Phase 3 shipped sanctoral data on this same branch - (data/of/calendar-2002.sexp), so the defect this note warns about is now - LIVE: 19 March coincides with Palm Sunday in 16 of the 1583-2100 years - (e.g. 2062), and St Joseph lands forward at Easter+9 via rule 3 instead - of anticipated backward to 18 March. Pinned, not silently wrong: see - test_rite_of.ml's [test_joseph_palm_sunday_2062_known_wrong_forward_transfer] - (2062, both grade and identity) and allow-list entries L8/L9 - (data/of/expected-divergences-litcal.sexp, 2035-03-17, a second, distinct - year witnessing the same limitation). + HISTORY (kept for the record; the defect is fixed, not merely + documented, as of this revision). 19 March coincides with Palm Sunday + in 16 of the 1583-2100 years (e.g. 2062), and before this fix St Joseph + landed forward at Easter+9 via rule 3 instead of anticipated backward + to 18 March -- pinned on that shape until this revision, in + test_rite_of.ml's own now-renamed/re-asserted test (previously + [test_joseph_palm_sunday_2062_known_wrong_forward_transfer]; see that + file for its corrected form) and allow-list entries L8/L9 + (data/of/expected-divergences-litcal.sexp) -- L8/L9 name a DIFFERENT + year, 2035-03-17, where St Joseph is impeded by Holy Monday rather than + coinciding with Palm Sunday itself, so n. 56(f)'s own trigger does not + apply there; that instance of the general rule's forward-only reach is + untouched by this fix and remains open on its own terms. - Implementing it would need either a kernel signature change (out of - scope for this rite module and forbidden by this fix wave) or a - deliberate violation of a documented obligation {!Colitur_kernel.Calendar} - depends on: n. 60's own text is "ad proximiorem diem transferatur" -- - the NEAREST day, not "proximiorem diem SEQUENTEM" (the nearest - FOLLOWING one) -- yet every branch above only ever searches or lands - forward. The strictly-LATER reading is not this rite's own choice; it is - imposed by {!Colitur_kernel.Rite.t.transfer_target}'s own contract - (rite.mli:77-84), which is justified there purely by the EF's RG 96. That - is EF-shaped vocabulary constraining rite-agnostic kernel code -- the same - class of item CLAUDE.md already tracks under "EF-shaped things still in - rite-agnostic kernel code" -- so a real fix has to start at the kernel - field, not in this module. + What unblocked it: {!Colitur_kernel.Rite.t.transfer_target}'s own + contract (rite.mli) used to require the result be STRICTLY LATER than + [origin] -- an obligation argued there purely from the EF's RG 96, i.e. + EF-shaped vocabulary constraining rite-agnostic kernel code, the same + class of item CLAUDE.md tracks under "EF-shaped things still in + rite-agnostic kernel code". Traced against {!Colitur_kernel.Calendar}'s + actual placement pass (calendar.ml's [place_transfers]/[year], not + against the obligation's own prior wording) rather than assumed unsafe: + the round loop re-resolves the whole year fresh every round with no + comparison against [origin] anywhere in its two safety nets ([~start]/ + [~stop]; the round-count guard), so a target earlier than [origin] is + handled identically to a later one. The kernel contract was relaxed + (rite.mli, [transfer_target]'s own comment carries the full argument) + from "strictly later" to "different from origin" -- the one requirement + the trace showed is still load-bearing (a same-day target would hand + {!Colitur_kernel.Precedence.resolve} the same candidate twice, which it + does not deduplicate). No change was needed in calendar.ml's actual + logic; two of its comments were corrected for accuracy (the round-guard + rationale and the out-of-range rationale both previously asserted + "every genuine transfer moves forward" as a blanket fact). Shaped to match {!Colitur_kernel.Rite.t.transfer_target} exactly so a later phase wires it with no adaptation, and honours both obligations that field - states: the result is strictly later than [origin], and the search carries - its own step bound rather than relying on {!Colitur_kernel.Calendar}'s - round guard, which bounds rounds rather than one call's internal search. + states: the result differs from [origin] (rule 0's own [Date.add_days + origin (-1)] trivially satisfies this, going backward rather than + forward), and the search carries its own step bound rather than relying + on {!Colitur_kernel.Calendar}'s round guard, which bounds rounds rather + than one call's internal search (rule 0 needs no bound at all -- it runs + no search, so it terminates trivially). Never raises. If no free day is found within 400 days, or the walk would otherwise have to probe past 31 December 9999 (past which diff --git a/lib/rites/rite_of/rite_of.mli b/lib/rites/rite_of/rite_of.mli index 8124467..e537cbd 100644 --- a/lib/rites/rite_of/rite_of.mli +++ b/lib/rites/rite_of/rite_of.mli @@ -34,10 +34,11 @@ module Lectionary_of = Lectionary_of Ordinary Time runs in two separate blocks over one liturgical year (Normae n. 43-44), so the expected run-length-compressed sequence names it twice. - - [transfer_target]: {!Precedence_of.transfer_target}, Normae n. 60/n. 5. - Known incomplete on one named date shape (Normae n. 56(f), St - Joseph's backward anticipation onto Palm Sunday) -- documented on that - value's own .mli, not repeated or silently worked around here. + - [transfer_target]: {!Precedence_of.transfer_target}, Normae n. 56(f)/ + n. 60/n. 5 (St Joseph's backward anticipation onto Palm Sunday, + resolved [of-normae-56f]/W1, 2026-08-26, together with the general + forward search) -- documented on that value's own .mli, not repeated + or silently worked around here. - [readings]: {!Lectionary_of.readings} partially applied to the caller's own [~lectionary] and {!Temporal_of.year_start} (the OF reading-cycle arithmetic's own Advent anchor) -- no [~commons] |