diff options
Diffstat (limited to 'lib/kernel')
| -rw-r--r-- | lib/kernel/calendar.ml | 46 | ||||
| -rw-r--r-- | lib/kernel/rite.mli | 82 |
2 files changed, 92 insertions, 36 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 -> |