diff options
| author | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-12 11:38:35 +0200 |
|---|---|---|
| committer | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-12 11:38:35 +0200 |
| commit | e19adb9c7ea369cafe76e7eff50e9248a4a954d0 (patch) | |
| tree | 57824e121606286ebdf8fff68439986dd3300eae /lib/kernel/calendar.ml | |
| parent | 0506388da160a15ceddb0cea1a697d737103d5c4 (diff) | |
| parent | 36df2bd0af9a555a09334e14b0d89118be1dbbc0 (diff) | |
| download | colitur-e19adb9c7ea369cafe76e7eff50e9248a4a954d0.tar.gz colitur-e19adb9c7ea369cafe76e7eff50e9248a4a954d0.zip | |
Merge branch 'ef-plan3': Plan 3, the EF resolution engine
Adds the rite-parameterised Precedence resolver, Liturgical_day, Rite,
and Calendar (year as the primitive, because transfers need whole-year
knowledge), the full EF precedence ruleset (RG 91's 28-entry table,
occurrence RG 92-95, commemorations RG 108-111, transfers RG 96-98),
322 bootstrapped sanctoral entries, colitur day <year>, and validation
layers 3-5.
Layer 3 diffs 16801 days against lectio; layer 4 diffs 730 days against
missalemeum; layer 5 pins ~30 dates on the known-tricky years. Both
comparison layers carry cited allow-lists that name the governing RG
paragraph and which engine is right.
The oracle layer earned its place immediately: Holy Thursday was violet
in colitur and lectio alike, because colitur's data was bootstrapped
from lectio and both carried the same error. Only an independent source
could see it. RG 128(b) and RG 122 name it white.
Diffstat (limited to 'lib/kernel/calendar.ml')
| -rw-r--r-- | lib/kernel/calendar.ml | 387 |
1 files changed, 387 insertions, 0 deletions
diff --git a/lib/kernel/calendar.ml b/lib/kernel/calendar.ml new file mode 100644 index 0000000..5d3572c --- /dev/null +++ b/lib/kernel/calendar.ml @@ -0,0 +1,387 @@ +(* Resolution across a whole liturgical year. See calendar.mli for the + architectural rationale (why [year] is the primitive and [day] derived). *) + +(* The kernel's domain floor and ceiling (Date.make's documented 1583..9999 + bound). Both are always constructible -- in-range by definition -- so + neither of these can itself raise. *) +let domain_min_date = + match Date.make ~year:1583 ~month:1 ~day:1 with Ok d -> d | Error e -> failwith e + +let domain_max_date = + match Date.make ~year:9999 ~month:12 ~day:31 with Ok d -> d | Error e -> failwith e + +(* [start, stop] for the liturgical year opening in civil year [y], clamped at + both ends of the domain rather than calling [rite.year_start] on a civil + year outside 1583..9999. + + Top: at [y] = 9999, [rite.year_start (y + 1)] would ask for civil year + 10000 -- out of Date's domain (Plan 2 shipped exactly this bug in + Validate). Clamp [stop] to 31 December 9999 instead: the final liturgical + year comes back truncated, not un-computable. + + Bottom: symmetric case, reachable only through [day] below. A date in + civil year 1583 before that year's own [rite.year_start] genuinely belongs + to the liturgical year that opened in civil year 1582 for an + Advent-anchored rite -- but [rite.year_start 1582] is equally out of + domain. [day] only ever decrements a valid date's own (in-domain) civil + year by at most one, so [y] = 1582 is the sole way this branch is reached. + Clamp [start] to 1 January 1583: "year 1582" becomes the truncated + stretch from the domain floor up to the day before [rite.year_start 1583], + which is exactly the sliver a date there needs. + + [y] itself is clamped once, up front, to [1582, 9999] -- not left to each + branch's own guard. Task 5's review found that guarding [start] and [stop] + independently protected only one of their two [rite.year_start] calls + each: [start]'s guard (["y < 1583"]) leaves [stop]'s "y + 1" call + unguarded at the bottom (["year 999"] still called [year_start 1000], out + of domain), and [stop]'s guard (["y >= 9999"]) leaves [start]'s call + unguarded at the top (["year 100000"] still called [year_start 100000]). + Neither is reachable through [day] (see calendar.mli), but [year] is + public, and a direct out-of-contract call must not raise either. Clamping + [y] once closes both gaps with one check instead of two. *) +let year_bounds (rite : ('s, 'r) Rite.t) (y : int) : Date.t * Date.t = + let y = max 1582 (min 9999 y) in + let start = if y < 1583 then domain_min_date else rite.Rite.year_start y in + let stop = + if y >= 9999 then domain_max_date else Date.add_days (rite.Rite.year_start (y + 1)) (-1) + in + (start, stop) + +(* RG 91's contest for one date: the temporal office against every sanctoral + entry whose Date_spec resolves to it, plus whatever the placement pass + below has [injected] there so far (a celebration transferred in from an + impeded day elsewhere). [Layer.on_date] is keyed on exactly (month, day), + which for a [Fixed] spec -- the only form Plan 2 ships -- is the same test + as resolving the spec against [date]'s own year and comparing, so no + separate filter is needed here. + + [injected] is keyed by [Date.to_rata] rather than [Date.t] directly: + [Date.t] carries no [compare]-respecting hash, and rata-die is already the + canonical total order this module uses for date arithmetic. *) +let resolve_with_injected (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) + (injected : (int, 'r Precedence.candidate list) Hashtbl.t) (date : Date.t) : + ('s, 'r) Temporal.t * 's Precedence.context * 'r Precedence.resolution = + let temporal = rite.Rite.temporal date in + let temporal_candidate = + { Precedence.cel = temporal.Temporal.office; origin = Precedence.Temporal } + in + let natural = + Layer.on_date idx ~month:(Date.month date) ~day:(Date.day date) + |> List.map (fun (e : 'r Layer.entry) -> + { Precedence.cel = e.Layer.cel; origin = Precedence.Sanctoral }) + in + let arrived = try Hashtbl.find injected (Date.to_rata date) with Not_found -> [] in + let ctx = { Precedence.date; season = temporal.Temporal.season; weekday = temporal.Temporal.weekday } in + let resolution = + Precedence.resolve rite.Rite.rules ctx ~temporal:temporal_candidate ~sanctoral:(natural @ arrived) + in + (temporal, ctx, resolution) + +(* What Precedence.resolve currently reports as observed on [date], given the + placements decided so far -- this is exactly the [occupant] callback + Rite.transfer_target's search walks forward with (rite.mli explains why + that judgement has to come from the rite, not from here). *) +let occupant_of (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) + (injected : (int, 'r Precedence.candidate list) Hashtbl.t) (date : Date.t) : 'r Celebration.t = + 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 + 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. *) +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. *) +let out_of_range_reason = "omitted: transfer target falls outside the liturgical year (RG 96)" + +(* Rebuilds the per-date injection index from [assignment] (slug -> (origin, + target)) fresh each round, rather than accumulating it incrementally as + candidates are placed. A candidate re-deferred in a later round (its first + target turned out to already be claimed by a higher-band rival, see + [place_transfers]) must vacate its old target date entirely, not merely + gain a second one; rebuilding from a slug-keyed map, which holds exactly + one entry per candidate, gives that for free. An append-only structure + would instead leave the stale placement behind forever, and the round + loop would never see [deferred] empty out. *) +let injected_index_of_assignment (assignment : (string, Date.t * Date.t) Hashtbl.t) + (candidate_by_slug : (string, 'r Precedence.candidate) Hashtbl.t) : + (int, 'r Precedence.candidate list) Hashtbl.t = + let tbl : (int, 'r Precedence.candidate list) Hashtbl.t = Hashtbl.create 16 in + Hashtbl.iter + (fun slug (_origin, target) -> + let key = Date.to_rata target in + let c = Hashtbl.find candidate_by_slug slug in + Hashtbl.replace tbl key (c :: (try Hashtbl.find tbl key with Not_found -> []))) + assignment; + tbl + +(* The placement pass itself (spec §2.4 steps 1-4; step 5, recording + transferred_in/out, is [year]'s job once this reaches a fixed point). + + Every [Precedence.Transfer]-*and*-[Precedence.Repose]-disposed loser lands + in [resolution.deferred] together -- [Precedence.resolve]'s own fold + matches them as one case, [Transfer | Repose -> ... :: defs ...] -- and + everything gathered below is routed through + [rite.transfer_target], i.e. RG 96's next-admissible-day search. That is + only correct for [Transfer]. [Repose] denotes RG 100-102's *repositio* + (perpetual impediment, reassigned to the next appropriate day and treated + as proper) -- a distinct rubric this module does not implement. It is + documented here rather than split into a second mechanism because nothing + currently produces [Repose]: the design spec records it as "declared, not + exercised" (§1.3) -- the EF ruleset (Tasks 7-9) returns it for nothing; + perpetual impediment arises from proper/diocesan calendars, which are + overlay content, out of this plan's scope. If a future rite's rules ever + do return [Repose], it would silently take the RG 96 path here, which + would be wrong -- worth knowing before that day, not discovering it then. + + Each round: gather every currently-deferred candidate across the whole + year (fresh, against this round's [injected] state -- a candidate already + placed and now winning its target is no longer a loser anywhere and so + will not reappear here); if none, the fixed point is reached. Otherwise + sort ALL of them by band -- RG 97-98: this is the global ordering that + decides who transfers first when I-class feasts coincide -- ties break on + slug, same convention as Precedence.compare_by, so placement never depends + on the layer's own entry order. Then place each in turn, in that order. + + [claimed_this_round] is what makes the sort actually decide anything: it + starts empty every round and gains one entry per candidate placed so far + THIS round, and [occupant_with_claims] reports a claimed date as occupied + by whoever claimed it, layered on top of [injected] (last round's settled + state, frozen for the round -- see [injected_index_of_assignment] for why + that has to stay frozen rather than being updated in place). Without it, + every candidate in a round would search against the exact same snapshot + and a same-date collision would only be caught (and only one side of it + corrected) on re-resolution next round, one collision layer per round -- + RG 97-98's own ordering would still come out right in the end, but only + by accident of Precedence.resolve's own internal tie-break repeating this + module's, not because this module's sort ever decided anything. Layering + the claims instead means a same-round collision is resolved in the one + round it is found, in the sorted order, and the earlier RG 97-98 test + pins exactly that: it fails on "claims 2 Feb first" without this. + + [~start ~stop] bound the [transfer_target] a placement is allowed to + settle on: outside that range it goes into [out_of_range] instead of + [assignment], permanently (never retried -- [transfer_target] is a pure + function of a candidate's own permanent origin and the occupancy state, + so asking it again would only recompute the same out-of-range answer). *) +let place_transfers (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) ~(start : Date.t) + ~(stop : Date.t) (dates : Date.t array) : + (string, Date.t * Date.t) Hashtbl.t + * (string, 'r Precedence.candidate) Hashtbl.t + * (string, Date.t * Date.t) Hashtbl.t = + let assignment : (string, Date.t * Date.t) Hashtbl.t = Hashtbl.create 16 in + let candidate_by_slug : (string, 'r Precedence.candidate) Hashtbl.t = Hashtbl.create 16 in + let out_of_range : (string, Date.t * Date.t) Hashtbl.t = Hashtbl.create 4 in + let compare_deferred (_, ctx1, c1) (_, ctx2, c2) = + let b1 = rite.Rite.rules.Precedence.band ctx1 c1 in + let b2 = rite.Rite.rules.Precedence.band ctx2 c2 in + if b1 <> b2 then Int.compare b1 b2 + else Slug.compare c1.Precedence.cel.Celebration.slug c2.Precedence.cel.Celebration.slug + in + let round = ref 0 in + let converged = ref false in + let guard_hit = ref false in + while (not !converged) && not !guard_hit do + incr round; + if !round > max_transfer_rounds then guard_hit := true + else begin + let injected = injected_index_of_assignment assignment candidate_by_slug in + let raw = + Array.to_list dates + |> List.concat_map (fun date -> + let _, ctx, resolution = resolve_with_injected rite idx injected date in + List.map (fun c -> (date, ctx, c)) resolution.Precedence.deferred) + in + (* [raw] rediscovers every candidate's *permanent* natural loss at its + origin every round -- the layer entry never moves, so a candidate + already settled elsewhere still shows up losing at the date it was + always going to lose at. Left unfiltered, that stale sighting gets + placed again right next to the candidate's own already-settled + self, which -- because a placed candidate's own rank makes it look + "occupied" to a fresh search starting from its original origin -- + oscillates between two dates forever, never reaching [deferred = + []] (confirmed by removing this filter: "transferable" lands on 14 + Jan instead of 13 in test_transfer_moves_and_does_not_duplicate, + not merely "doesn't converge" -- the bug is a wrong answer, not + only a hang). A sighting is genuinely actionable only if the + candidate has never been placed yet (first time seen, and not + already known unplaceable -- [out_of_range] gets the same + permanent exclusion [assignment] does, for the same reason), or if + it is losing exactly at the date it is *currently* assigned to (a + fresh RG 97-98 bump: something else also landed there and + out-ranked it) -- any other date is the stale, permanent one and is + dropped. *) + let deferred = + List.filter + (fun (date, _ctx, c) -> + let slug = Slug.to_string c.Precedence.cel.Celebration.slug in + if Hashtbl.mem out_of_range slug then false + else + match Hashtbl.find_opt assignment slug with + | None -> true + | Some (_, target) -> Date.compare date target = 0) + raw + in + if deferred = [] then converged := true + else begin + let claimed_this_round : (int, 'r Precedence.candidate) Hashtbl.t = Hashtbl.create 4 in + let occupant_with_claims d = + match Hashtbl.find_opt claimed_this_round (Date.to_rata d) with + | Some c -> c.Precedence.cel + | None -> occupant_of rite idx injected d + in + List.stable_sort compare_deferred deferred + |> List.iter (fun (origin, _ctx, c) -> + let target = rite.Rite.transfer_target c origin occupant_with_claims in + let slug = Slug.to_string c.Precedence.cel.Celebration.slug in + if Date.compare target start < 0 || Date.compare target stop > 0 then + Hashtbl.replace out_of_range slug (origin, target) + else begin + Hashtbl.replace claimed_this_round (Date.to_rata target) c; + Hashtbl.replace assignment slug (origin, target); + Hashtbl.replace candidate_by_slug slug c + end) + end + end + done; + (assignment, candidate_by_slug, out_of_range) + +(* The final build of one day, once placement has reached its fixed point (or + exhausted the guard): resolve against the settled [injected] state, then + layer on [transferred_in] (this date received an injected candidate that + went on to win) and [transferred_out] (whichever candidates' settled + placements originated here -- RG 97-98 lets that be more than one; see + [Liturgical_day.transferred_out]). *) +let build_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) + (assignment : (string, Date.t * Date.t) Hashtbl.t) + (out_of_range : (string, Date.t * Date.t) Hashtbl.t) + (injected : (int, 'r Precedence.candidate list) Hashtbl.t) + (transferred_out_of : (int, ('r Celebration.t * Date.t) list) Hashtbl.t) (date : Date.t) : + ('s, 'r) Liturgical_day.t = + let temporal, _ctx, resolution = resolve_with_injected rite idx injected date in + let arrived = try Hashtbl.find injected (Date.to_rata date) with Not_found -> [] in + let transferred_in = + arrived + |> List.find_opt (fun c -> + Slug.equal c.Precedence.cel.Celebration.slug + resolution.Precedence.observed.Precedence.cel.Celebration.slug) + |> Option.map (fun c -> c.Precedence.cel) + in + let transferred_out = + try Hashtbl.find transferred_out_of (Date.to_rata date) with Not_found -> [] + in + (* [resolution.deferred] here is NOT "the placement pass never got to + these": it is the origin day's own permanent, structural loss -- the + layer entry that lost the RG 91 contest here never moves, so a + candidate successfully placed somewhere else still shows up losing at + the exact date it was always going to lose at (this is the same fact + [place_transfers]'s round loop has to filter around, see its comment). + A [deferred] sighting only belongs in [omitted] if it was never + actually settled anywhere -- i.e. it is stuck in [out_of_range], or the + guard above was hit before it reached a day it wins. Settled elsewhere + means genuinely accounted for via [observed]/[transferred_in] on the + day it landed and [transferred_out] here, not via [omitted] too -- + double-booking it in both would fail Task 12's "appears exactly once" + reading of this day alone. *) + let unresolved c = + let slug = Slug.to_string c.Precedence.cel.Celebration.slug in + if Hashtbl.mem out_of_range slug then true + else + match Hashtbl.find_opt assignment slug with + | None -> true + | Some (_, target) -> + not (Slug.equal (occupant_of rite idx injected target).Celebration.slug c.Precedence.cel.Celebration.slug) + in + let reason_for c = + if Hashtbl.mem out_of_range (Slug.to_string c.Precedence.cel.Celebration.slug) then + out_of_range_reason + else unconverged_reason + in + let omitted = + List.map (fun (c, reason) -> (c.Precedence.cel, reason)) resolution.Precedence.omitted + @ (resolution.Precedence.deferred |> List.filter unresolved + |> List.map (fun c -> (c.Precedence.cel, reason_for c))) + in + { + Liturgical_day.date; + rite = rite.Rite.id; + temporal; + observed = resolution.Precedence.observed.Precedence.cel; + commemorations = + List.map (fun (c, p) -> (c.Precedence.cel, p)) resolution.Precedence.commemorations; + transferred_in; + transferred_out; + omitted; + citations = []; + } + +let year (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) (y : int) : + ('s, 'r) Liturgical_day.t array = + let idx = Layer.index_by_date layer in + let start, stop = year_bounds rite y in + (* [max 0]: defends [Array.init] against a negative length, which would + otherwise arise for a rite whose [year_start] lands exactly on the + domain floor (start clamps to the same date, giving [stop] a day + before it). Not reachable through [day] -- see calendar.mli -- but + [year] is public, and a direct out-of-contract call must not raise + either. *) + let n = max 0 (Date.to_rata stop - Date.to_rata start + 1) in + let dates = Array.init n (fun i -> Date.add_days start i) in + let assignment, candidate_by_slug, out_of_range = place_transfers rite idx ~start ~stop dates in + let injected = injected_index_of_assignment assignment candidate_by_slug in + let transferred_out_of : (int, ('r Celebration.t * Date.t) list) Hashtbl.t = Hashtbl.create 16 in + Hashtbl.iter + (fun slug (origin, target) -> + let cel = (Hashtbl.find candidate_by_slug slug).Precedence.cel in + let key = Date.to_rata origin in + Hashtbl.replace transferred_out_of key + ((cel, target) :: (try Hashtbl.find transferred_out_of key with Not_found -> []))) + assignment; + (* Canonicalise each day's departures: the accumulation above walks + [assignment] via [Hashtbl.iter], whose bucket order is not guaranteed + stable across runs (OCaml's hash seed can be randomised via + OCAMLRUNPARAM=R), so a day with more than one departure -- RG 97-98's + coinciding-feasts case -- would otherwise report them in a + run-dependent order: an environment read, in a kernel whose invariants + forbid one. [Layer.index_by_date] guards against exactly this by + re-sorting each date bucket after building it (layer.ml); same fix, + same reason. Sorted by target date -- which, for a correctly-converged + year, is also RG 97-98's own order: the higher-precedence loser claims + the earlier admissible day -- ties (not expected, but not assumed + impossible) broken on slug. *) + let by_target_then_slug (c1, t1) (c2, t2) = + let dc = Date.compare t1 t2 in + if dc <> 0 then dc else Slug.compare c1.Celebration.slug c2.Celebration.slug + in + Hashtbl.iter + (fun k v -> Hashtbl.replace transferred_out_of k (List.sort by_target_then_slug v)) + transferred_out_of; + Array.map (build_day rite idx assignment out_of_range injected transferred_out_of) dates + +let day (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) (date : Date.t) : + ('s, 'r) Liturgical_day.t = + let cy = Date.year date in + let y = if Date.compare date (rite.Rite.year_start cy) >= 0 then cy else cy - 1 in + let start, _ = year_bounds rite y in + (year rite layer y).(Date.to_rata date - Date.to_rata start) |
