diff options
Diffstat (limited to 'lib/kernel')
| -rw-r--r-- | lib/kernel/calendar.ml | 387 | ||||
| -rw-r--r-- | lib/kernel/calendar.mli | 72 | ||||
| -rw-r--r-- | lib/kernel/celebration.ml | 13 | ||||
| -rw-r--r-- | lib/kernel/celebration.mli | 12 | ||||
| -rw-r--r-- | lib/kernel/liturgical_day.ml | 27 | ||||
| -rw-r--r-- | lib/kernel/liturgical_day.mli | 25 | ||||
| -rw-r--r-- | lib/kernel/precedence.ml | 69 | ||||
| -rw-r--r-- | lib/kernel/precedence.mli | 78 | ||||
| -rw-r--r-- | lib/kernel/rite.ml | 14 | ||||
| -rw-r--r-- | lib/kernel/rite.mli | 62 | ||||
| -rw-r--r-- | lib/kernel/slug.ml | 8 | ||||
| -rw-r--r-- | lib/kernel/validate.ml | 194 | ||||
| -rw-r--r-- | lib/kernel/validate.mli | 79 | ||||
| -rw-r--r-- | lib/kernel/vocab.ml | 25 | ||||
| -rw-r--r-- | lib/kernel/vocab.mli | 25 |
15 files changed, 1044 insertions, 46 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) diff --git a/lib/kernel/calendar.mli b/lib/kernel/calendar.mli new file mode 100644 index 0000000..1c0b0ed --- /dev/null +++ b/lib/kernel/calendar.mli @@ -0,0 +1,72 @@ +(** Resolution across a whole liturgical year (spec §2.4). + + Transfers make per-date resolution impossible to do correctly: resolving + 25 March can push a feast onto 26 March, and RG 97-98 has coinciding + I-class feasts transfer in table order, which needs global knowledge of + the whole year. So [year] is the primitive -- it resolves every date in + one pass -- and [day] is derived: it finds the liturgical year containing + a date and indexes into it. Both are pure; neither caches. + + Once every day's temporal-vs-sanctoral contest is resolved, [year] places + every deferred candidate (RG 96-98): a losing I-class candidate the + rite's rules send to [Precedence.Transfer] does not stay put -- it moves + to the next day [rite.transfer_target] names as admissible, and both + ends of the move are recorded: [transferred_in] on the day it arrives + (at most one -- RG 96 sends each departure to the next day that is not I + or II class, and the first to arrive occupies it), [transferred_out] on + the day it left (a list, not an option: RG 97-98 has coinciding I-class + feasts transfer "in order", so one day can lose more than one). Every + deferred candidate is accounted for exactly once: placed, or -- only if + the placement fixed point is not reached within the round guard (which + nothing in the 1962 calendar is expected to trigger), or the rite's own + [transfer_target] names a date outside this liturgical year's own range + (unproven to occur in the real EF calendar, but not ruled out by + construction) -- left in [Liturgical_day.omitted] with a reason that + says which, never silently dropped. See [calendar.ml]'s + [place_transfers] for the algorithm and its termination argument. + + [Precedence.Repose]-disposed losers are gathered the same way + [Precedence.Transfer]-disposed ones are (Precedence folds both into + [deferred] as one case) and are routed through the same RG 96 search. + That is only correct for [Transfer]: [Repose] denotes RG 100-102's + *repositio*, a distinct rubric this module does not implement. Nothing + in the EF ruleset currently returns [Repose] (design spec §1.3: + "declared, not exercised" -- perpetual impediment arises from + proper/diocesan calendars, out of this plan's scope), so the gap is + latent rather than a live bug; documented here rather than given a + second mechanism for a disposition nothing emits. *) + +(** [year rite layer y] resolves every day of the liturgical year that opens + in civil year [y]: from [rite.year_start y] through the day before + [rite.year_start (y + 1)], inclusive of both ends. + + Total over 1583..9999, including the boundary years, and beyond them too: + [y] is clamped to [1582, 9999] before either bound is computed (not just + guarded near the two edges independently -- see [year_bounds] in + [calendar.ml] for why that distinction matters), so [year] never raises + regardless of the [y] it is given, not only for values near the domain + edge. + - At [y] = 9999, [rite.year_start (y + 1)] would ask for civil year + 10000, out of {!Date}'s domain (this is the bug Plan 2 shipped in + [Validate] and later fixed). The end of the walk clamps to 31 December + 9999 instead of computing that call; the returned year comes back + truncated to whatever the rite's own temporal cycle covers between + [rite.year_start 9999] and the last day of that civil year, not + un-computable. + - Symmetrically, [y] < 1583 clamps the start of the walk to 1 January + 1583 instead of calling [rite.year_start y] on an out-of-domain civil + year. [year] is never called this way directly by anything in this + module; {!day} is the only caller that can reach [y] = 1582 (one below + the floor, never lower), when the date it was asked about sits in civil + year 1583 before that year's own [rite.year_start] -- i.e. the sliver + whose true liturgical year opened in civil year 1582, which the domain + cannot represent. Calling [year] with such a [y] directly is also safe: + it returns exactly that truncated sliver. *) +val year : ('s, 'r) Rite.t -> 'r Layer.t -> int -> ('s, 'r) Liturgical_day.t array + +(** [day rite layer date] finds the liturgical year containing [date] -- the + year [y] with [rite.year_start y <= date < rite.year_start (y + 1)] -- + and returns its slot for [date]. Recomputes that whole year on every + call: pure, no cache, no mutable state. Acceptable cost for the natural + usage (dump a year, sweep years for validation), which pays it once. *) +val day : ('s, 'r) Rite.t -> 'r Layer.t -> Date.t -> ('s, 'r) Liturgical_day.t diff --git a/lib/kernel/celebration.ml b/lib/kernel/celebration.ml index 2963366..eb4249e 100644 --- a/lib/kernel/celebration.ml +++ b/lib/kernel/celebration.ml @@ -8,10 +8,17 @@ open Sexplib0.Sexp_conv but would carry no information while forcing every consumer (Layer, Overlay, and later Precedence and Calendar) to thread a variable that means nothing. *) +(* Whether this celebration can be the observed day at all. The 1960 reform + reduced many feasts to a bare commemoration; they retain a rank (RG 111 orders + admitted commemorations by dignity) but can never be observed. NOT a fifth + rank: RG 8 fixes the classes at four. *) +type status = Feast | Commemoration_only [@@deriving sexp] + type 'r t = { slug : Slug.t; names : Names.t; rank : 'r; + status : status; colour : Colour.t; subject : Subject.t; citations : Citation.t list; @@ -19,6 +26,6 @@ type 'r t = { } [@@deriving sexp] -let make ~slug ?(names = Names.empty) ~rank ~colour ?(subject = Subject.Temporal) - ?(citations = []) ~layer () = - { slug; names; rank; colour; subject; citations; layer } +let make ~slug ?(names = Names.empty) ~rank ?(status = Feast) ~colour + ?(subject = Subject.Temporal) ?(citations = []) ~layer () = + { slug; names; rank; status; colour; subject; citations; layer } diff --git a/lib/kernel/celebration.mli b/lib/kernel/celebration.mli index 1c84d35..a3c2960 100644 --- a/lib/kernel/celebration.mli +++ b/lib/kernel/celebration.mli @@ -1,8 +1,15 @@ +(** Whether this celebration can be the observed day at all. The 1960 reform + reduced many feasts to a bare commemoration; they retain a rank (RG 111 + orders admitted commemorations by dignity) but can never be observed. NOT + a fifth rank: RG 8 fixes the classes at four. *) +type status = Feast | Commemoration_only [@@deriving sexp] + (** A celebration. Parameterised by the rite's rank type only. *) type 'r t = { slug : Slug.t; names : Names.t; rank : 'r; + status : status; colour : Colour.t; subject : Subject.t; citations : Citation.t list; @@ -10,7 +17,8 @@ type 'r t = { } [@@deriving sexp] -(** [subject] defaults to [Subject.Temporal], [names] to empty, [citations] to []. *) +(** [status] defaults to [Feast], [subject] to [Subject.Temporal], [names] to + empty, [citations] to []. *) val make : - slug:Slug.t -> ?names:Names.t -> rank:'r -> colour:Colour.t -> + slug:Slug.t -> ?names:Names.t -> rank:'r -> ?status:status -> colour:Colour.t -> ?subject:Subject.t -> ?citations:Citation.t list -> layer:string -> unit -> 'r t diff --git a/lib/kernel/liturgical_day.ml b/lib/kernel/liturgical_day.ml new file mode 100644 index 0000000..bbb52b8 --- /dev/null +++ b/lib/kernel/liturgical_day.ml @@ -0,0 +1,27 @@ +open Sexplib0.Sexp_conv + +(* The single stable result schema (parent spec §2). *) +type ('s, 'r) t = { + date : Date.t; + rite : string; + temporal : ('s, 'r) Temporal.t; + (** embedded, not flattened: it is already a coherent unit with its own + invariants, and re-listing season/week/weekday here would create two + places for them to disagree *) + observed : 'r Celebration.t; + commemorations : ('r Celebration.t * Precedence.privilege) list; + transferred_in : 'r Celebration.t option; + (** arrived here from an impeded day *) + transferred_out : ('r Celebration.t * Date.t) list; + (** celebrations that left this day, and where each one went. A list, + not an option: RG 97-98 has coinciding I-class feasts transfer + "in order" -- plural -- so a day can lose more than one. Asymmetric + with [transferred_in] deliberately: a day receives at most one + arrival, because RG 96 sends each departure to the next day that + is not I or II class, and the first to arrive occupies it. *) + omitted : ('r Celebration.t * string) list; + (** with the reason, never silent -- Task 12's no-celebration-lost + invariant reads this *) + citations : Citation.t list; (** always empty until Plan 4 *) +} +[@@deriving sexp] diff --git a/lib/kernel/liturgical_day.mli b/lib/kernel/liturgical_day.mli new file mode 100644 index 0000000..a109251 --- /dev/null +++ b/lib/kernel/liturgical_day.mli @@ -0,0 +1,25 @@ +(** The single stable result schema (parent spec §2). *) +type ('s, 'r) t = { + date : Date.t; + rite : string; + temporal : ('s, 'r) Temporal.t; + (** embedded, not flattened: it is already a coherent unit with its own + invariants, and re-listing season/week/weekday here would create two + places for them to disagree *) + observed : 'r Celebration.t; + commemorations : ('r Celebration.t * Precedence.privilege) list; + transferred_in : 'r Celebration.t option; + (** arrived here from an impeded day *) + transferred_out : ('r Celebration.t * Date.t) list; + (** celebrations that left this day, and where each one went. A list, + not an option: RG 97-98 has coinciding I-class feasts transfer + "in order" -- plural -- so a day can lose more than one. Asymmetric + with [transferred_in] deliberately: a day receives at most one + arrival, because RG 96 sends each departure to the next day that + is not I or II class, and the first to arrive occupies it. *) + omitted : ('r Celebration.t * string) list; + (** with the reason, never silent -- Task 12's no-celebration-lost + invariant reads this *) + citations : Citation.t list; (** always empty until Plan 4 *) +} +[@@deriving sexp] diff --git a/lib/kernel/precedence.ml b/lib/kernel/precedence.ml new file mode 100644 index 0000000..05ad69f --- /dev/null +++ b/lib/kernel/precedence.ml @@ -0,0 +1,69 @@ +(* The rite-parameterised resolver. RG 91 says who wins; RG 92-95 says what + happens to the loser; RG 108-111 says how many commemorations are admitted. + Three separate functions, because the loser's fate depends on the loser's own + rank, not the winner's. *) +open Sexplib0.Sexp_conv + +type origin = Temporal | Sanctoral [@@deriving sexp] +type privilege = Privileged | Ordinary [@@deriving sexp] +type disposition = Omit | Commemorate of privilege | Transfer | Repose [@@deriving sexp] + +type 'r candidate = { cel : 'r Celebration.t; origin : origin } [@@deriving sexp] + +type 's context = { date : Date.t; season : 's; weekday : Date.weekday } + +type ('s, 'r) rules = { + band : 's context -> 'r candidate -> int; + disposition : winner:'r candidate -> loser:'r candidate -> disposition; + admit : + observed:'r candidate -> + ('r candidate * privilege) list -> + ('r candidate * privilege) list; +} + +type 'r resolution = { + observed : 'r candidate; + commemorations : ('r candidate * privilege) list; + deferred : 'r candidate list; + omitted : ('r candidate * string) list; +} + +(* Ties break on slug so the result never depends on input order. *) +let compare_by rules ctx a b = + let ba = rules.band ctx a and bb = rules.band ctx b in + if ba <> bb then Int.compare ba bb + else Slug.compare a.cel.Celebration.slug b.cel.Celebration.slug + +let resolve rules ctx ~temporal ~sanctoral = + (* A commemoration-only entry can never be observed (see Celebration.status), + so it is held out of the contest entirely rather than relying on its band. *) + let eligible, forced_comm = + List.partition + (fun c -> c.cel.Celebration.status = Celebration.Feast) + sanctoral + in + let sorted = List.stable_sort (compare_by rules ctx) (temporal :: eligible) in + let observed = List.hd sorted in + let losers = List.tl sorted @ forced_comm in + let comms, deferred, omitted = + List.fold_left + (fun (comms, defs, omits) l -> + match rules.disposition ~winner:observed ~loser:l with + | Commemorate p -> ((l, p) :: comms, defs, omits) + | Transfer | Repose -> (comms, l :: defs, omits) + | Omit -> (comms, defs, (l, "omitted: yielded to a higher day") :: omits)) + ([], [], []) losers + in + let comms = List.rev comms and deferred = List.rev deferred in + let admitted = rules.admit ~observed comms in + let dropped = + List.filter (fun c -> not (List.exists (fun a -> fst a == fst c) admitted)) comms + in + { + observed; + commemorations = admitted; + deferred; + omitted = + List.rev omitted + @ List.map (fun (c, _) -> (c, "omitted: admission limit reached")) dropped; + } diff --git a/lib/kernel/precedence.mli b/lib/kernel/precedence.mli new file mode 100644 index 0000000..ae054dd --- /dev/null +++ b/lib/kernel/precedence.mli @@ -0,0 +1,78 @@ +(** The rite-parameterised resolver: RG 91 says who wins, RG 92-95 says what + happens to the loser, RG 108-111 says how many commemorations are admitted. + Three separate rite-supplied functions, because the loser's fate depends on + the loser's own rank, not the winner's -- conflating them would resist + extension to a second rite. *) + +(** Which of the day's two office streams a candidate came from. *) +type origin = Temporal | Sanctoral [@@deriving sexp] + +(** RG 111: an admitted commemoration's own standing, distinct from its rank. *) +type privilege = Privileged | Ordinary [@@deriving sexp] + +(** What becomes of a losing candidate. *) +type disposition = + | Omit (** yields with no trace in the day's celebration *) + | Commemorate of privilege (** kept as a commemoration of the observed day *) + | Transfer (** moved to the next free day (RG 92-95) *) + | Repose (** kept only in a votive/private sense; not commemorated today *) +[@@deriving sexp] + +(** A celebration together with the office stream it was drawn from. Parameterised + by the rite's rank type only, matching {!Celebration.t}. *) +type 'r candidate = { cel : 'r Celebration.t; origin : origin } [@@deriving sexp] + +(** The day a resolution is computed for. Parameterised by the rite's season + type only -- a context has no rank of its own. *) +type 's context = { date : Date.t; season : 's; weekday : Date.weekday } + +(** The rite's three resolution functions. *) +type ('s, 'r) rules = { + band : 's context -> 'r candidate -> int; + (** RG 91: orders candidates for the day; lower wins. *) + disposition : winner:'r candidate -> loser:'r candidate -> disposition; + (** RG 92-95: the loser's fate, which depends on the loser's own rank. *) + admit : + observed:'r candidate -> + ('r candidate * privilege) list -> + ('r candidate * privilege) list; + (** RG 108-111: how many commemorations are admitted, and in what order; + anything filtered out here is recorded in {!resolution.omitted}, not + dropped. + + OBLIGATION ON THE IMPLEMENTATION, not enforced by this type: every + candidate this function returns must be a value taken UNCHANGED + from its input list, never rebuilt (e.g. via a [{ c with ... }] + record update, even one that copies every field back unchanged). + {!resolve}'s own [omitted] accounting distinguishes an admitted + candidate from a dropped one by PHYSICAL equality ([==]) on the + candidate value, not structural equality -- a rebuilt record is + [=] to the original but not [==], so {!resolve} cannot match the + rebuilt copy against the original it was given. The celebration + then surfaces TWICE in the same day's result -- once in + {!resolution.commemorations} (the rebuilt copy, admitted) and once + in {!resolution.omitted} (the original, which nothing in the + admitted set matches). One admission, double-reported, silently + rather than raising. This obligation previously lived only in one rite's + own module documentation (Rite_ef.Precedence_ef.admit); stated + here because this signature -- not any one rite's implementation + of it -- is what an author of the next rite reads. *) +} + +(** The outcome of resolving one day's candidates. *) +type 'r resolution = { + observed : 'r candidate; + commemorations : ('r candidate * privilege) list; + deferred : 'r candidate list; + omitted : ('r candidate * string) list; (** each with a reason *) +} + +(** Total: the temporal candidate is passed separately, so there is no + empty-candidate case. Ties break on slug, so the result never depends on + input order. A [Commemoration_only] celebration is held out of the contest + and can never be [observed]. Every input candidate appears exactly once in + [observed], [commemorations], [deferred] or [omitted] — nothing is dropped + silently. *) +val resolve : + ('s, 'r) rules -> 's context -> temporal:'r candidate -> + sanctoral:'r candidate list -> 'r resolution diff --git a/lib/kernel/rite.ml b/lib/kernel/rite.ml new file mode 100644 index 0000000..89fceb6 --- /dev/null +++ b/lib/kernel/rite.ml @@ -0,0 +1,14 @@ +(* Everything a rite supplies, bundled. Passing these as loose arguments let a + caller pair one rite's vocab with another's temporal; bundling makes that + unrepresentable through the normal path. *) +type ('s, 'r) t = { + id : string; + vocab : ('s, 'r) Vocab.t; + year_start : int -> Date.t; + temporal : Date.t -> ('s, 'r) Temporal.t; + anchors : int -> (string * Date.t) list; + rules : ('s, 'r) Precedence.rules; + season_runs : 's list; + transfer_target : + 'r Precedence.candidate -> Date.t -> (Date.t -> 'r Celebration.t) -> Date.t; +} diff --git a/lib/kernel/rite.mli b/lib/kernel/rite.mli new file mode 100644 index 0000000..ffe9471 --- /dev/null +++ b/lib/kernel/rite.mli @@ -0,0 +1,62 @@ +(** Everything a rite supplies, bundled. Passing these as loose arguments let a + caller pair one rite's vocab with another's temporal; bundling makes that + unrepresentable through the normal path. Carries functions, so it has no + sexp form. *) +type ('s, 'r) t = { + id : string; + vocab : ('s, 'r) Vocab.t; + year_start : int -> Date.t; + (** first day of the liturgical year opening in civil year y *) + temporal : Date.t -> ('s, 'r) Temporal.t; + anchors : int -> (string * Date.t) list; + (** Easter-derived days: (expected slug, date) *) + rules : ('s, 'r) Precedence.rules; + season_runs : 's list; + (** the expected run-length-compressed season sequence over one liturgical + year. NOT necessarily [vocab.seasons]: a rite may have one season + appear in two separate runs (the modern form's Ordinary Time does). *) + transfer_target : + 'r Precedence.candidate -> Date.t -> (Date.t -> 'r Celebration.t) -> Date.t; + (** RG 96: where an impeded I-class feast goes. Given the deferred + candidate, the date it was impeded on, and [occupant] -- a callback + exposing what {!Calendar} currently resolves as observed on any + given date -- returns the date to place it on. + + Deliberately one rite-supplied function, not a generic search Calendar + drives itself: "not I or II class" is not derivable from [band] or + [disposition] alone. RG 91's own table would let a universal I-class + feast (entry 11) numerically outrank an ordinary Sunday (entry 15, + II class) in a raw occurrence contest -- entry 11 comes before entry + 15, and lower wins -- so testing "would the translated feast win + here" is not the same question as "is this day free to receive a + translation": RG 96 forbids landing on the Sunday regardless of + which one would structurally win. Only the rite knows which of its + own ranks are exempt from translation onto them. The rite also + owns the search's starting point, because RG 96's exception is + rite-specific too: the Annunciation does not search forward from + its own impeded date at all, it goes straight to the Monday after + Low Sunday (searching onward from there only if that day is itself + blocked). [occupant] is supplied rather than a raw layer/temporal + pair so the rite never has to re-implement occurrence resolution + 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). *) +} diff --git a/lib/kernel/slug.ml b/lib/kernel/slug.ml index 5139c99..25281f2 100644 --- a/lib/kernel/slug.ml +++ b/lib/kernel/slug.ml @@ -1,6 +1,10 @@ (* Stable celebration identifiers. Also the lectionary key: EF slugs are adopted - verbatim from lectio so the Plan 3 lectionary bootstrap needs no mapping - table (spec §4.4). *) + verbatim from lectio so the Plan 4 lectionary bootstrap needs no mapping + table (spec §4.4). CORRECTED (final fix wave, item 7): this comment said + "Plan 3" -- the SANCTORAL bootstrap (data/ef/sanctoral.sexp) is Plan 3 and + shipped in this branch; the LECTIONARY bootstrap (reading citations, + Liturgical_day.t's own [citations] field) is a separate, later Plan 4, + per that field's own doc comment ("always empty until Plan 4"). *) type t = string let valid_char c = (c >= 'a' && c <= 'z') || (c >= '0' && c <= '9') || c = '-' diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index 7be3425..cc8bdce 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -20,7 +20,35 @@ let has_duplicate strings = let rec go = function a :: (b :: _ as rest) -> a = b || go rest | _ -> false in go sorted -let run vocab ~year_start ~temporal ~anchors ~year = +(* Like [has_duplicate], but names the offender(s) instead of only reporting + that one exists -- the ["slugs"] check below wants a useful failure + detail, not just a bool. *) +let duplicates strings = + let sorted = List.sort String.compare strings in + let rec go acc = function + | a :: (b :: _ as rest) -> go (if a = b then a :: acc else acc) rest + | _ -> acc + in + List.sort_uniq String.compare (go [] sorted) + +(* Task 12's "unconverged" check has no structural signal to key off -- + Calendar's placement pass records its round-guard reason as a plain + string in [Liturgical_day.omitted] (calendar.ml's own [unconverged_reason], + not exposed as a public constant), and [Liturgical_day.omitted]'s own doc + comment says exactly this check is meant to read it. A short, distinctive + substring rather than the full literal keeps the coupling to calendar.ml's + exact wording as loose as it can be while still being unambiguous: nothing + else this kernel emits into [omitted] talks about "converging". *) +let contains_substring s ~needle = + let ls = String.length s and ln = String.length needle in + let rec at i = i + ln <= ls && (String.sub s i ln = needle || at (i + 1)) in + ln = 0 || at 0 + +let run (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) ~year = + let vocab = rite.Rite.vocab in + let year_start = rite.Rite.year_start in + let temporal = rite.Rite.temporal in + let anchors = rite.Rite.anchors in let start = year_start year in let stop = (* [year_start (year + 1)] needs a date in civil year (year+1); at @@ -68,18 +96,16 @@ let run vocab ~year_start ~temporal ~anchors ~year = (* Weekday agreement. *) if t.Temporal.weekday <> Date.weekday date then fail date "weekday" "temporal weekday disagrees with Date.weekday"; - (* Slug: three properties, none checked here, all delivered - elsewhere. Well-formedness needs no check: [Slug.t] is a private - string validated on every construction path ([of_string], - [of_string_exn], [t_of_sexp]), and [to_string] is the identity, - so round-tripping an existing [Slug.t] can never fail -- a check - here would be structurally incapable of firing, which is worse - than no check, since it would look like coverage that isn't - there. Uniqueness *per date* needs no check either: [temporal] - returns exactly one office by construction. Uniqueness *across - the year* is deliberately NOT asserted -- a resumed Sunday - reuses an earlier Epiphany key on purpose, so the check would be - false. *) + (* Slug: three properties. Well-formedness needs no check: [Slug.t] + is a private string validated on every construction path + ([of_string], [of_string_exn], [t_of_sexp]), and [to_string] is + the identity, so round-tripping an existing [Slug.t] can never + fail -- a check here would be structurally incapable of firing, + which is worse than no check, since it would look like coverage + that isn't there. Uniqueness *per date* needs no check either: + [temporal] returns exactly one office by construction. + Uniqueness *across the year* IS asserted, below, once the whole + walk is in hand -- see the ["slugs"] check after this loop. *) (* Vocabulary closure. *) if not (List.exists (fun r -> vocab.Vocab.rank_to_string r = vocab.Vocab.rank_to_string cel.Celebration.rank) @@ -97,9 +123,28 @@ let run vocab ~year_start ~temporal ~anchors ~year = | None -> fail date "determinism" "a second call to temporal raised where the first succeeded")) days; let observed = List.rev !observed in + (* Slug uniqueness across the year (Plan 2 carried item 4): moved into + [Validate] itself so every consumer gets it, not only a 200-sample + QCheck property scoped to one rite. Asserted OUTRIGHT, no exemption: + Plan 2 verified zero duplicate slugs domain-wide, across all 8 416 + years, for the EF rite's own resumed-Sunday mechanism -- the exemption + the test property used to carry protected nothing real, because a + resumed Sunday only ever backfills a week number Septuagesima cut short + that same liturgical year (so it was never actually used that year to + begin with), never repeats one the year's own January Sundays already + used. If a future rite genuinely needs an exemption, it can supply one + then -- not speculatively here. *) + (match duplicates (List.map (fun (_, t) -> Slug.to_string t.Temporal.office.Celebration.slug) observed) with + | [] -> () + | dups -> + fail start "slugs" + (Printf.sprintf "slug(s) sighted on more than one date this year: %s" (String.concat ", " dups))); (* Season contiguity and completeness: the run-length-compressed sequence must - equal vocab.seasons exactly -- all seasons, each in one unbroken run, in - canonical order. No EF season can be empty in any year. *) + equal the rite's own [season_runs] exactly, in canonical order. This is + NOT necessarily [vocab.seasons] -- most rites have each season in one + unbroken run, but a rite may legitimately have one season appear in two + separate runs (the modern form's Ordinary Time does), so the expected + sequence is rite-supplied rather than derived from the vocabulary. *) let compressed = List.fold_left (fun acc (_, t) -> @@ -108,7 +153,7 @@ let run vocab ~year_start ~temporal ~anchors ~year = [] observed |> List.rev in - let expected = List.map vocab.Vocab.season_to_string vocab.Vocab.seasons in + let expected = List.map vocab.Vocab.season_to_string rite.Rite.season_runs in if compressed <> expected then fail start "seasons" (Printf.sprintf "season runs %s; expected %s" @@ -157,4 +202,121 @@ let run vocab ~year_start ~temporal ~anchors ~year = if actual <> expected_slug then fail date "anchor" (Printf.sprintf "expected slug %S, got %S" expected_slug actual)) anchor_pairs; + (* Resolution invariants (Task 12): everything above only ever asked + [rite.temporal] for a date's office in isolation. From here on the + LITURGICAL YEAR IS ACTUALLY RESOLVED against [layer] -- occurrence, + transfer placement, commemorations, the works (spec §2.4) -- and the + result checked for five further properties a temporal-only pass cannot + see at all. [days] (the walk built above) is reused rather than + recomputed: it names exactly the same [start, stop] span + {!Calendar.year} resolves for this [year]. *) + (match Calendar.year rite layer year with + | exception exn -> + (* The kernel contract forbids [run] itself from ever raising on + in-range input, and an exception escaping resolution is the most + total form of "silently lost" there is: nothing about this year's + sanctoral entries could be verified as accounted for at all. *) + fail start "lost" + (Printf.sprintf "resolving the year raised (%s); nothing could be verified as accounted for" + (Printexc.to_string exn)) + | resolved -> + let idx = Layer.index_by_date layer in + let bump tbl slug = Hashtbl.replace tbl slug (1 + (try Hashtbl.find tbl slug with Not_found -> 0)) in + (* Expected: how many times each layer entry's own Date_spec resolves + within [start, stop]. Walking dates and querying [Layer.on_date] + (rather than resolving each entry's Date_spec against candidate + civil years directly) is what naturally counts a fixed late- + November date TWICE in the ~20% of liturgical years whose 371-day + span reaches it on both ends -- see validate.mli's own note on 30 + November / St Andrew. *) + let expected : (string, int) Hashtbl.t = Hashtbl.create 64 in + List.iter + (fun date -> + Layer.on_date idx ~month:(Date.month date) ~day:(Date.day date) + |> List.iter (fun (e : 'r Layer.entry) -> + bump expected (Slug.to_string e.Layer.cel.Celebration.slug))) + days; + (* Actual: how many times each slug is actually sighted across the + resolved year. Deliberately [observed] + [commemorations] + + [omitted] only, NOT [transferred_out]: a successfully transferred + celebration is already counted once, via [observed] (+ + [transferred_in]) on the day it lands; also counting + [transferred_out] at the day it left would double-book every clean + transfer, which is exactly what this check exists to catch, not + cause. *) + let actual : (string, int) Hashtbl.t = Hashtbl.create 64 in + let bump_cel tbl (c : 'r Celebration.t) = bump tbl (Slug.to_string c.Celebration.slug) in + Array.iter + (fun (d : ('s, 'r) Liturgical_day.t) -> + bump_cel actual d.Liturgical_day.observed; + List.iter (fun (c, _) -> bump_cel actual c) d.Liturgical_day.commemorations; + List.iter (fun (c, _) -> bump_cel actual c) d.Liturgical_day.omitted) + resolved; + Hashtbl.fold (fun slug exp acc -> (slug, exp) :: acc) expected [] + |> List.sort compare (* stable failure order: Hashtbl.iter's own order is hash-seed-dependent *) + |> List.iter (fun (slug, exp) -> + let act = try Hashtbl.find actual slug with Not_found -> 0 in + if act < exp then + fail start "lost" + (Printf.sprintf "%s: sighted %d time(s) this year, but its own Date_spec resolves %d" + slug act exp) + else if act > exp then + fail start "duplicated" + (Printf.sprintf "%s: sighted %d time(s) this year, but its own Date_spec resolves only %d" + slug act exp)); + Array.iter + (fun (d : ('s, 'r) Liturgical_day.t) -> + let date = d.Liturgical_day.date in + let observed_slug = Slug.to_string d.Liturgical_day.observed.Celebration.slug in + let has_slug (c, _) = Slug.to_string c.Celebration.slug = observed_slug in + (* "observed": the day's own winner must not ALSO be listed as one + of its own losers -- see validate.mli's own note on why this is + reachable (two distinct layer entries sharing a slug, one + transferred onto the other's natural date, the transferred one + winning) despite {!Precedence.resolve}'s fold never letting the + SAME candidate value appear as both winner and loser. *) + if List.exists has_slug d.Liturgical_day.commemorations + || List.exists has_slug d.Liturgical_day.omitted + then + fail date "observed" + (Printf.sprintf + "%s is this day's observed celebration and also appears among its own \ + commemorations/omissions" + observed_slug); + (* "unconverged": see [contains_substring]'s own comment above. *) + if + List.exists + (fun (_, reason) -> contains_substring reason ~needle:"did not converge") + d.Liturgical_day.omitted + then + fail date "unconverged" + "transfer placement did not reach a fixed point within the round guard (RG 96-98)"; + (* "admission": re-offer this day's own admitted commemorations + back to [rite.rules.admit] and require the exact same set back. + [origin] is reconstructed as [Sanctoral] uniformly: + {!Liturgical_day.t} does not retain a commemoration's original + origin, and the real EF [admit] (precedence_ef.ml) reads only + rank and slug from a candidate, never [origin], so this + reconstruction is exact for it; documented in validate.mli as + the one place a rite whose [admit] DOES consult [origin] could + see a false negative from this check. *) + let observed_candidate : 'r Precedence.candidate = + { Precedence.cel = d.Liturgical_day.observed; origin = Precedence.Sanctoral } + in + let as_candidates comms = + List.map (fun (c, p) -> ({ Precedence.cel = c; origin = Precedence.Sanctoral }, p)) comms + in + let offered = as_candidates d.Liturgical_day.commemorations in + let readmitted = rite.Rite.rules.Precedence.admit ~observed:observed_candidate offered in + let norm l = + List.map (fun (c, p) -> (Slug.to_string c.Precedence.cel.Celebration.slug, p)) l + |> List.sort compare + in + if norm readmitted <> norm offered then + fail date "admission" + (Printf.sprintf + "admit is not a fixed point on this day's own commemorations: re-offering %d \ + admitted %d back" + (List.length offered) (List.length readmitted))) + resolved); List.rev !failures diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli index 709a711..5e55fc5 100644 --- a/lib/kernel/validate.mli +++ b/lib/kernel/validate.mli @@ -5,26 +5,71 @@ type failure = { year : int; date : string; check : string; detail : string } val failure_to_string : failure -> string -(** [run vocab ~year_start ~temporal ~anchors ~year] returns every invariant - violation in the liturgical year opening in civil year [year]. An empty - list means the year is clean. +(** [run rite layer ~year] returns every invariant violation in the + liturgical year opening in civil year [year]. An empty list means the + year is clean. - [anchors y] is the rite's own independent restatement of its fixed and - Easter-derived named days for civil year [y], as (expected slug, date) - pairs -- not derived from [temporal] itself, so a drift between the two - is caught rather than invisible. [run] consults both [anchors year] and - [anchors (year + 1)], since a liturgical year straddles two civil years, - and checks only the pairs whose date actually falls within the year - walked. + [rite.Rite.anchors y] is the rite's own independent restatement of its + fixed and Easter-derived named days for civil year [y], as (expected + slug, date) pairs -- not derived from [rite.Rite.temporal] itself, so a + drift between the two is caught rather than invisible. [run] consults + both [anchors year] and [anchors (year + 1)], since a liturgical year + straddles two civil years, and checks only the pairs whose date actually + falls within the year walked. + + ["slugs"]: no two dates within the walked liturgical year may carry the + same office slug (Plan 2 carried item 4). Asserted outright, with no + exemption for the resumed-Sunday reuse a slug's own name might suggest: + a resumed Sunday only ever backfills a week number Septuagesima cut + short that same year, so by construction it never repeats a number that + year's own January Sundays actually used. + + The season check compares the run-length-compressed season sequence + against [rite.Rite.season_runs], not [rite.Rite.vocab.seasons]: a rite may + have one season appear in two separate runs (the modern form's Ordinary + Time does), so the two are not necessarily the same list. + + [layer] is resolved against [rite] via {!Calendar.year} (spec §2.4's + occurrence/transfer/commemoration pass), and the resulting fully-resolved + liturgical year is checked for five further invariants a temporal-only + pass cannot see (Task 12), each its own ["check"] label: + - ["observed"]: a day's [observed] celebration is never ALSO listed among + that same day's [commemorations] or [omitted] -- a day reports one + winner, not a winner that also lost to itself. + - ["lost"]: no sanctoral entry is silently dropped. Per slug, the number + of times it is actually sighted ([observed] + [commemorations] + + [omitted], summed over the whole year -- NOT [transferred_out], which + would double-count a successfully placed transfer against its own + arrival) must never fall below the number of times its own + {!Date_spec} resolves within the year's span (an entry with two + occurrences, e.g. 30 November in the nine liturgical years where the + 371-day span reaches it twice, must be sighted twice, not once). Also + fires if resolving the year raises at all -- an escaping exception is + the most total form of silent loss, and the kernel contract forbids + [run] itself from propagating it. + - ["duplicated"]: the same per-slug count must never EXCEED the number of + {!Date_spec} resolutions either. Deliberately NOT "no slug appears + twice in the year" -- a fixed date can legitimately resolve twice, per + ["lost"] above -- it is "resolutions and sightings agree", the property + that actually distinguishes a transfer that moved from one that + duplicated. + - ["unconverged"]: no day's [omitted] carries the reason {!Calendar}'s + placement pass records when its round guard (calendar.ml's + [max_transfer_rounds]) is hit before every deferred candidate reaches a + fixed point. + - ["admission"]: the rite's own [rules.admit] is a fixed point on what it + already admitted -- re-offering a day's [commemorations] back to + [admit] (reconstructed with {!Precedence.Sanctoral} origin; the real EF + admit reads only rank and slug, never origin, so this reconstruction is + exact for it) must return exactly that same set. A cap-enforcing + selector that is not idempotent on its own output has, by definition, + admitted something its own rule would not admit if asked again -- the + rite-agnostic form of "the admission limit was not exceeded" available + without embedding a rite's specific numeric caps (RG 111's, for EF) + into kernel code. Total over the whole 1583..9999 domain, including [year] = 9999: the liturgical year opening there continues into out-of-domain civil year 10000, so the walk is clamped to 31 December 9999 and the checks run against that truncated final year rather than raising. *) -val run : - ('s, 'r) Vocab.t -> - year_start:(int -> Date.t) -> - temporal:(Date.t -> ('s, 'r) Temporal.t) -> - anchors:(int -> (string * Date.t) list) -> - year:int -> - failure list +val run : ('s, 'r) Rite.t -> 'r Layer.t -> year:int -> failure list diff --git a/lib/kernel/vocab.ml b/lib/kernel/vocab.ml index 78729bb..a4e61a3 100644 --- a/lib/kernel/vocab.ml +++ b/lib/kernel/vocab.ml @@ -7,13 +7,32 @@ parametric types natively. *) type ('s, 'r) t = { seasons : 's list; - (** canonical liturgical-year order; Validate's contiguity check reads this *) + (** canonical liturgical-year order. CORRECTED (final fix wave, item + 7): this used to say "Validate's contiguity check reads this" -- + false since validate.ml's own "seasons" check switched to + {!Colitur_kernel.Rite.t}.season_runs in this branch (Plan 2 + carried item 1: EF has each season in one run, but the modern + form's Ordinary Time does not, so the expected run sequence had + to become rite-supplied rather than derived from this field). + For EF specifically [Rite_ef.rite] sets season_runs to + this very list, so the two happen to agree there, but Validate + itself no longer reads [seasons] to build its expectation. *) season_to_string : 's -> string; season_of_string : string -> 's option; ranks : 'r list; (** documentation order, highest first. Plan 2 uses it only for the - closure check -- it is not a precedence relation until Plan 3 - defines one. *) + closure check. CORRECTED (final fix wave, item 7): this used to + say "it is not a precedence relation until Plan 3 defines one" -- + Plan 3 did define one (RG 111's dignity ordering, Rite_ef. + Precedence_ef.dignity/compare_dignity), but as its OWN small, + separately-hardcoded function, not one derived from this field: + [admit] needs Vocab_ef.rank's dignity as plain data (RG 8's four + classes), and reusing this field's own [int list] position would + couple that meaning to documentation order the way {!band} is + explicitly NOT allowed to (precedence_ef.ml's own file comment). + This field therefore still carries no precedence relation of its + own; a rite that wanted one derived from it would have to build + it itself. *) rank_to_string : 'r -> string; rank_of_string : string -> 'r option; } diff --git a/lib/kernel/vocab.mli b/lib/kernel/vocab.mli index 78729bb..a4e61a3 100644 --- a/lib/kernel/vocab.mli +++ b/lib/kernel/vocab.mli @@ -7,13 +7,32 @@ parametric types natively. *) type ('s, 'r) t = { seasons : 's list; - (** canonical liturgical-year order; Validate's contiguity check reads this *) + (** canonical liturgical-year order. CORRECTED (final fix wave, item + 7): this used to say "Validate's contiguity check reads this" -- + false since validate.ml's own "seasons" check switched to + {!Colitur_kernel.Rite.t}.season_runs in this branch (Plan 2 + carried item 1: EF has each season in one run, but the modern + form's Ordinary Time does not, so the expected run sequence had + to become rite-supplied rather than derived from this field). + For EF specifically [Rite_ef.rite] sets season_runs to + this very list, so the two happen to agree there, but Validate + itself no longer reads [seasons] to build its expectation. *) season_to_string : 's -> string; season_of_string : string -> 's option; ranks : 'r list; (** documentation order, highest first. Plan 2 uses it only for the - closure check -- it is not a precedence relation until Plan 3 - defines one. *) + closure check. CORRECTED (final fix wave, item 7): this used to + say "it is not a precedence relation until Plan 3 defines one" -- + Plan 3 did define one (RG 111's dignity ordering, Rite_ef. + Precedence_ef.dignity/compare_dignity), but as its OWN small, + separately-hardcoded function, not one derived from this field: + [admit] needs Vocab_ef.rank's dignity as plain data (RG 8's four + classes), and reusing this field's own [int list] position would + couple that meaning to documentation order the way {!band} is + explicitly NOT allowed to (precedence_ef.ml's own file comment). + This field therefore still carries no precedence relation of its + own; a rite that wanted one derived from it would have to build + it itself. *) rank_to_string : 'r -> string; rank_of_string : string -> 'r option; } |
