diff options
Diffstat (limited to 'lib/kernel/calendar.ml')
| -rw-r--r-- | lib/kernel/calendar.ml | 46 |
1 files changed, 28 insertions, 18 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 |