From 9df1aab700ce4454c26c7d0ede5b51c0f0c96c66 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Tue, 11 Aug 2026 19:30:34 +0200 Subject: kernel: the LiturgicalDay result schema Temporal is embedded rather than flattened, so season/week/weekday have one home and cannot disagree with themselves. transferred_in/out make transfers visible in the result -- an ordo must print 'transferred from the 25th', and the nothing-lost invariant reads these fields. citations exists and is empty until Plan 4; adding it later would widen a type every consumer matches on. --- lib/kernel/liturgical_day.ml | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 lib/kernel/liturgical_day.ml (limited to 'lib/kernel/liturgical_day.ml') diff --git a/lib/kernel/liturgical_day.ml b/lib/kernel/liturgical_day.ml new file mode 100644 index 0000000..65e3ba5 --- /dev/null +++ b/lib/kernel/liturgical_day.ml @@ -0,0 +1,19 @@ +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 : Date.t option; + (** this day's celebration went there *) + citations : Citation.t list; (** always empty until Plan 4 *) +} +[@@deriving sexp] -- cgit v1.3 From 953427d8d1e3a34994be53b60e18662ec26fef4e Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Tue, 11 Aug 2026 20:07:55 +0200 Subject: kernel: carry omitted celebrations on Liturgical_day.t, reason and all Precedence.resolution already tracked what happened to every losing candidate -- commemorated, deferred, or omitted with a reason -- but Liturgical_day.t had nowhere for the deferred and omitted buckets to land, so Calendar dropped them at the door. Task 12's no-celebration-lost invariant needs to read that accounting off the day result itself, not re-resolve every day to reconstruct it, so a reason recorded nowhere is not recorded. Add Liturgical_day.omitted : ('r Celebration.t * string) list, after transferred_out and before citations. Calendar.resolve_day now folds resolution.omitted (Precedence's own native omissions, reasons intact) and resolution.deferred (mapped to "deferred: transfer placement not yet implemented (Task 6)") into it. Adds a full-day accounting test against the whole Calendar pipeline: four colliding sanctoral entries plus the day's feria, checked as a slug set (matching test_precedence.ml's own nothing-silently-lost test) so a candidate silently dropped or duplicated into two buckets would fail it, plus an identity check that the deferred and admission-limit reasons don't get swapped. --- lib/kernel/calendar.ml | 21 ++++++++++----- lib/kernel/calendar.mli | 13 ++++++--- lib/kernel/liturgical_day.ml | 3 +++ lib/kernel/liturgical_day.mli | 3 +++ test/test_calendar.ml | 63 ++++++++++++++++++++++++++++++++++++++++--- 5 files changed, 89 insertions(+), 14 deletions(-) (limited to 'lib/kernel/liturgical_day.ml') diff --git a/lib/kernel/calendar.ml b/lib/kernel/calendar.ml index fd23377..1cdd1fa 100644 --- a/lib/kernel/calendar.ml +++ b/lib/kernel/calendar.ml @@ -35,6 +35,15 @@ let year_bounds (rite : ('s, 'r) Rite.t) (y : int) : Date.t * Date.t = in (start, stop) +(* [resolution.deferred] (RG 96-98 transfer candidates) has nowhere to be + PLACED yet -- Task 6 adds the fixed-point pass that does -- but it must + still be accounted for on the day it lost, not silently dropped: Task + 12's no-celebration-lost invariant reads [Liturgical_day.omitted], so a + deferred candidate folds in there too, with its own reason distinct from + Precedence's native omissions ("omitted: yielded to a higher day", + "omitted: admission limit reached"). *) +let deferred_reason = "deferred: transfer placement not yet implemented (Task 6)" + (* RG 91's contest for one date: the temporal office against every sanctoral entry whose Date_spec resolves to it. [Layer.on_date] is keyed on exactly (month, day), which for a [Fixed] spec -- the only form Plan 2 ships -- is @@ -53,13 +62,10 @@ let resolve_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) (date : Date.t 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 in - (* [resolution.deferred] (RG 96-98 transfer candidates) and - [resolution.omitted] (yielded/admission-limit losers) have no field to - land in on Liturgical_day.t yet, so both are simply absent from today's - result -- deliberately incomplete for a deferred candidate, which is - thereby neither observed nor commemorated here, and not yet placed on - any later day either ("deferred: transfer placement not yet implemented - (Task 6)"). Task 6's fixed-point pass closes this gap. *) + let omitted = + List.map (fun (c, reason) -> (c.Precedence.cel, reason)) resolution.Precedence.omitted + @ List.map (fun c -> (c.Precedence.cel, deferred_reason)) resolution.Precedence.deferred + in { Liturgical_day.date; rite = rite.Rite.id; @@ -69,6 +75,7 @@ let resolve_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) (date : Date.t List.map (fun (c, p) -> (c.Precedence.cel, p)) resolution.Precedence.commemorations; transferred_in = None; transferred_out = None; + omitted; citations = []; } diff --git a/lib/kernel/calendar.mli b/lib/kernel/calendar.mli index 50ff8f8..2469f2a 100644 --- a/lib/kernel/calendar.mli +++ b/lib/kernel/calendar.mli @@ -9,10 +9,15 @@ This module resolves each day's temporal-vs-sanctoral contest but does not yet place deferred transfers (RG 96-98): a losing candidate the - rite's rules send to [Precedence.Transfer] is absent from the result - entirely on this pass -- not observed, not commemorated, and - [transferred_in]/[transferred_out] both stay [None] everywhere. Task 6 - adds the fixed-point placement pass that closes this gap. *) + rite's rules send to [Precedence.Transfer] is not observed and not + commemorated on the day it lost, and [transferred_in]/[transferred_out] + both stay [None] everywhere -- but it is not silently dropped either. It + lands in that day's [Liturgical_day.omitted] with the reason ["deferred: + transfer placement not yet implemented (Task 6)"], alongside + [Precedence]'s own native omissions (yielded to a higher day; admission + limit reached), each with its own reason. Task 6 adds the fixed-point + placement pass that actually places these; until then, this is the + day's complete, honest accounting of what happened to every candidate. *) (** [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 diff --git a/lib/kernel/liturgical_day.ml b/lib/kernel/liturgical_day.ml index 65e3ba5..cbaca9c 100644 --- a/lib/kernel/liturgical_day.ml +++ b/lib/kernel/liturgical_day.ml @@ -14,6 +14,9 @@ type ('s, 'r) t = { (** arrived here from an impeded day *) transferred_out : Date.t option; (** this day's celebration went there *) + 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 index 3c331c3..38e7c76 100644 --- a/lib/kernel/liturgical_day.mli +++ b/lib/kernel/liturgical_day.mli @@ -12,6 +12,9 @@ type ('s, 'r) t = { (** arrived here from an impeded day *) transferred_out : Date.t option; (** this day's celebration went there *) + 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/test/test_calendar.ml b/test/test_calendar.ml index a3c4125..d34611a 100644 --- a/test/test_calendar.ml +++ b/test/test_calendar.ml @@ -68,7 +68,12 @@ module Fixture = struct let disposition ~winner:_ ~(loser : rank P.candidate) = match loser.P.cel.Cel.rank with Lo -> P.Commemorate P.Ordinary | Hi -> P.Transfer - let rules : (season, rank) P.rules = { P.band; disposition; admit = (fun ~observed:_ cs -> cs) } + (* Admits at most one commemoration -- mirrors test_precedence.ml's own + example and, unlike "admit everything", actually gives the accounting + test below a genuine Precedence-native omission (distinct from a + deferred one) to exercise. *) + let rules : (season, rank) P.rules = + { P.band; disposition; admit = (fun ~observed:_ cs -> List.filteri (fun i _ -> i < 1) cs) } let rite : (season, rank) Rite.t = { Rite.id = "synthetic-calendar"; vocab; year_start; temporal; anchors = (fun _ -> []); @@ -82,7 +87,23 @@ module Fixture = struct let big_feast = entry ~month:12 ~day:8 ~slug:"big-feast" ~rank:Hi let commem_worthy = entry ~month:12 ~day:15 ~slug:"commem-worthy" ~rank:Lo - let layer = Layer.of_entries ~id:"synthetic" ~name:"Synthetic sanctoral" [ big_feast; commem_worthy ] + (* 20 Dec: four sanctoral entries on one date, for the full-accounting test. + "day-winner" and "eclipsed" tie on band (both Hi, both Sanctoral); ties + break on slug, so "day-winner" wins and "eclipsed" -- a Hi-rank loser -- + is [Transfer]-disposed, landing in [deferred]. "loser-a" and "loser-b" + are both Lo, both [Commemorate]-disposed, but [admit] only keeps one: + the other lands in Precedence's own [omitted] ("admission limit + reached"), distinct from "eclipsed"'s deferred reason. Four candidates, + three different fates -- observed, one specific omission reason, two + more. *) + let day_winner = entry ~month:12 ~day:20 ~slug:"day-winner" ~rank:Hi + let eclipsed = entry ~month:12 ~day:20 ~slug:"eclipsed" ~rank:Hi + let loser_a = entry ~month:12 ~day:20 ~slug:"loser-a" ~rank:Lo + let loser_b = entry ~month:12 ~day:20 ~slug:"loser-b" ~rank:Lo + + let layer = + Layer.of_entries ~id:"synthetic" ~name:"Synthetic sanctoral" + [ big_feast; commem_worthy; day_winner; eclipsed; loser_a; loser_b ] let liturgical_year_of date = let cy = D.year date in @@ -159,6 +180,41 @@ let test_day_near_domain_floor_does_not_raise () = Alcotest.(check string) "observed is the day's own feria" (Sl.to_string (Fixture.office date).Cel.slug) (Sl.to_string d.LD.observed.Cel.slug) +(* Full-day accounting through the whole Calendar pipeline (Layer -> Calendar + -> Liturgical_day), not just Precedence in isolation: every candidate fed + in for 20 Dec 2026 -- the feria plus Fixture's four colliding sanctoral + entries -- appears exactly once across observed/commemorations/omitted. + Checked as a slug SET (Alcotest.slist), matching test_precedence.ml's own + "nothing silently lost" test: a length-only check would pass even if one + slug were duplicated into two buckets and another dropped, which this + project has shipped before (register finding). *) +let test_full_day_accounting () = + let date = mk 2026 12 20 in + let d = C.day Fixture.rite Fixture.layer date in + let feria_slug = Sl.to_string (Fixture.office date).Cel.slug in + let bucketed = + (Sl.to_string d.LD.observed.Cel.slug + :: List.map (fun (c, _) -> Sl.to_string c.Cel.slug) d.LD.commemorations) + @ List.map (fun (c, _) -> Sl.to_string c.Cel.slug) d.LD.omitted + in + Alcotest.(check (slist string compare)) "every candidate appears exactly once" + [ feria_slug; "day-winner"; "eclipsed"; "loser-a"; "loser-b" ] + bucketed; + (* Identity within [omitted], not just membership: "eclipsed" (a deferred + transfer candidate, RG 96-98) must carry the deferred reason, not + Precedence's native "admission limit reached" that "loser-a"/"loser-b" + -- the ones Precedence itself dropped -- carry. Without this, a bug + that folded [resolution.deferred] into [omitted] with the wrong reason, + or dropped [resolution.omitted]'s own reasons, would still pass the + slug-set check above. *) + let reason_of slug = + d.LD.omitted |> List.find (fun (c, _) -> Sl.to_string c.Cel.slug = slug) |> snd + in + Alcotest.(check string) "eclipsed carries the deferred reason" + "deferred: transfer placement not yet implemented (Task 6)" (reason_of "eclipsed"); + Alcotest.(check string) "loser-a carries Precedence's own admission-limit reason" + "omitted: admission limit reached" (reason_of "loser-a") + let suite = ( "Calendar", [ Alcotest.test_case "year covers every day" `Quick test_year_covers_every_day; @@ -169,4 +225,5 @@ let suite = test_lower_ranked_sanctoral_is_commemorated; Alcotest.test_case "year 9999 does not raise" `Quick test_year_9999_does_not_raise; Alcotest.test_case "day near the domain floor does not raise" `Quick - test_day_near_domain_floor_does_not_raise ] ) + test_day_near_domain_floor_does_not_raise; + Alcotest.test_case "full day accounting" `Quick test_full_day_accounting ] ) -- cgit v1.3 From 1d6be4ac281e62accfb905b137b3c6b494183ee4 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Tue, 11 Aug 2026 21:29:13 +0200 Subject: kernel(calendar): fix multi-departure loss, band-order gap, off-array targets Four findings from Task 6 review, addressed on top of f15e44d. 1. transferred_out was a single Date.t option, so when RG 97-98 collides three or more feasts on one date (more than one loser), only the last one Hashtbl.iter happened to visit survived -- a genuinely lost move, and which one survived depended on OCaml's hash seed (OCAMLRUNPARAM=R), an environment read a kernel invariant forbids. RG 97-98 says coinciding feasts transfer "in order" -- plural -- so the type was wrong, not the fixture: transferred_out is now (Celebration.t * Date.t) list. transferred_in stays a single option, deliberately: a day receives at most one arrival (RG 96 sends each departure to the next non-I/II-class day, and the first to arrive occupies it). The per-day list is canonicalised (sorted by target date, then slug) after accumulation, the same fix layer.ml already applies to its own date-bucket index and for the same reason. Verified clean across 15 runs under OCAMLRUNPARAM=R; disabling the canonicalisation step showed the raw order genuinely flip between seeds, confirming the fix is load-bearing. 2. Every deferred candidate in the fixture was the same rank, so compare_deferred's band branch was unreachable and reversing it broke nothing -- the RG 97-98 test was pinning slug order, not band order. The fixture now has three ranks (Hi1 outranks Hi2, both transfer, both outrank Lo), with slugs chosen so band order and slug order disagree. Reversing the band comparison now fails the test on "higher-band loser claims 2 Feb first", received the wrong slug instead. 3. A transfer_target free to name any date could place a candidate outside the liturgical year's own start/stop bounds: invisible to year/build_day, so it would be observed nowhere and, since its origin's re-resolution would report it as settled, omitted nowhere either -- genuinely gone, contradicting calendar.mli's "never silently dropped". place_transfers now checks the range on every placement and routes an out-of-range one to a permanent-exclusion table instead of assignment, with its own cited omitted reason. 4. Precedence.resolve folds Transfer and Repose into one deferred case, and place_transfers routed all of it through transfer_target (RG 96's search), which is only correct for Transfer. Repose is RG 100-102's repositio, a distinct rubric this module does not implement. Documented rather than split into a second mechanism: nothing in the EF ruleset returns Repose (design spec section 1.3, "declared, not exercised"), so the gap is latent, not a live bug. Two new tests (origin records every departure; transfer target outside year is recorded not lost); the RG 97-98 test's fixture and assertions rewritten for finding 2. --- lib/kernel/calendar.ml | 157 +++++++++++++++++++++++-------- lib/kernel/calendar.mli | 31 +++++-- lib/kernel/liturgical_day.ml | 9 +- lib/kernel/liturgical_day.mli | 9 +- test/test_calendar.ml | 211 ++++++++++++++++++++++++++++-------------- 5 files changed, 298 insertions(+), 119 deletions(-) (limited to 'lib/kernel/liturgical_day.ml') diff --git a/lib/kernel/calendar.ml b/lib/kernel/calendar.ml index 1ad45a1..5d3572c 100644 --- a/lib/kernel/calendar.ml +++ b/lib/kernel/calendar.ml @@ -101,6 +101,20 @@ 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 @@ -125,6 +139,22 @@ let injected_index_of_assignment (assignment : (string, Date.t * Date.t) Hashtbl (* 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 @@ -148,11 +178,21 @@ let injected_index_of_assignment (assignment : (string, Date.t * Date.t) Hashtbl 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. *) -let place_transfers (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) (dates : Date.t array) : - (string, Date.t * Date.t) Hashtbl.t * (string, 'r Precedence.candidate) Hashtbl.t = + 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 @@ -185,16 +225,22 @@ let place_transfers (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) (dates : D 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), 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. *) + 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) -> - match Hashtbl.find_opt assignment (Slug.to_string c.Precedence.cel.Celebration.slug) with - | None -> true - | Some (_, target) -> Date.compare date target = 0) + 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 @@ -209,31 +255,30 @@ let place_transfers (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) (dates : D |> 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 - Hashtbl.replace claimed_this_round (Date.to_rata target) c; - Hashtbl.replace assignment slug (origin, target); - Hashtbl.replace candidate_by_slug slug c) + 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) + (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] (some candidate's settled placement - originated here). - - [transferred_out] is a single [Date.t option] (Liturgical_day.mli), so it - cannot represent two different celebrations leaving the same origin day - for two different destinations. [transferred_out_of] is built with - last-write-wins for that (unreached) case; RG 97-98 collisions still - report correctly because what actually matters -- each celebration landing - on its own, correctly-ordered day, exactly once -- is carried by - [observed]/[transferred_in], not by this pointer. *) + 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, Date.t) Hashtbl.t) (date : Date.t) : ('s, 'r) Liturgical_day.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 = @@ -244,7 +289,7 @@ let build_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) |> Option.map (fun c -> c.Precedence.cel) in let transferred_out = - try Some (Hashtbl.find transferred_out_of (Date.to_rata date)) with Not_found -> None + 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 @@ -253,23 +298,30 @@ let build_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) 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. the guard above was hit before this - candidate 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. *) + 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 - 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) + 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, unconverged_reason))) + |> List.map (fun c -> (c.Precedence.cel, reason_for c))) in { Liturgical_day.date; @@ -296,13 +348,36 @@ let year (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) (y : int) : 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 = place_transfers rite idx dates 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, Date.t) Hashtbl.t = Hashtbl.create 16 in + let transferred_out_of : (int, ('r Celebration.t * Date.t) list) Hashtbl.t = Hashtbl.create 16 in Hashtbl.iter - (fun _slug (origin, target) -> Hashtbl.replace transferred_out_of (Date.to_rata origin) target) + (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; - Array.map (build_day rite idx assignment injected transferred_out_of) dates + (* 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 = diff --git a/lib/kernel/calendar.mli b/lib/kernel/calendar.mli index 9fbd7e7..1c0b0ed 100644 --- a/lib/kernel/calendar.mli +++ b/lib/kernel/calendar.mli @@ -11,13 +11,30 @@ 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, - [transferred_out] on the day it left). 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 -- left in [Liturgical_day.omitted] with - a reason that says so, never silently dropped. See [calendar.ml]'s - [place_transfers] for the algorithm and its termination argument. *) + 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 diff --git a/lib/kernel/liturgical_day.ml b/lib/kernel/liturgical_day.ml index cbaca9c..bbb52b8 100644 --- a/lib/kernel/liturgical_day.ml +++ b/lib/kernel/liturgical_day.ml @@ -12,8 +12,13 @@ type ('s, 'r) t = { commemorations : ('r Celebration.t * Precedence.privilege) list; transferred_in : 'r Celebration.t option; (** arrived here from an impeded day *) - transferred_out : Date.t option; - (** this day's celebration went there *) + 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 *) diff --git a/lib/kernel/liturgical_day.mli b/lib/kernel/liturgical_day.mli index 38e7c76..a109251 100644 --- a/lib/kernel/liturgical_day.mli +++ b/lib/kernel/liturgical_day.mli @@ -10,8 +10,13 @@ type ('s, 'r) t = { commemorations : ('r Celebration.t * Precedence.privilege) list; transferred_in : 'r Celebration.t option; (** arrived here from an impeded day *) - transferred_out : Date.t option; - (** this day's celebration went there *) + 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 *) diff --git a/test/test_calendar.ml b/test/test_calendar.ml index 70823a4..505994e 100644 --- a/test/test_calendar.ml +++ b/test/test_calendar.ml @@ -9,8 +9,16 @@ let mk y m d = match D.make ~year:y ~month:m ~day:d with Ok t -> t | Error e -> (* A synthetic rite -- not EF -- so Calendar's behaviour is proven against the abstraction, not against EF's own real (and much larger) data. Two - seasons, two ranks: enough to exercise the type parameters without - dragging in real liturgical logic Calendar itself does not compute. *) + seasons, three ranks: enough to exercise the type parameters without + dragging in real liturgical logic Calendar itself does not compute. + + Three ranks, not two: Task 6 review finding 2. With only one + Transfer-disposed rank, every deferred candidate ties on [band] and + [compare_deferred]'s [b1 <> b2] branch (the one RG 97-98 actually depends + on -- coinciding I-class feasts transfer in TABLE order, not slug order) + was unreachable; reversing it broke no test. [Hi1] outranks [Hi2], both + outrank [Lo], both are [Transfer]-disposed -- so two colliding + transferables can now differ by band, not only by slug. *) module Fixture = struct module Vocab = Colitur_kernel.Vocab module Colour = Colitur_kernel.Colour @@ -20,16 +28,16 @@ module Fixture = struct module Date_spec = Colitur_kernel.Date_spec type season = A | B - type rank = Hi | Lo + type rank = Hi1 | Hi2 | Lo let season_to_string = function A -> "a" | B -> "b" let season_of_string = function "a" -> Some A | "b" -> Some B | _ -> None - let rank_to_string = function Hi -> "hi" | Lo -> "lo" - let rank_of_string = function "hi" -> Some Hi | "lo" -> Some Lo | _ -> None + let rank_to_string = function Hi1 -> "hi1" | Hi2 -> "hi2" | Lo -> "lo" + let rank_of_string = function "hi1" -> Some Hi1 | "hi2" -> Some Hi2 | "lo" -> Some Lo | _ -> None let vocab : (season, rank) Vocab.t = { Vocab.seasons = [ A; B ]; season_to_string; season_of_string; - ranks = [ Hi; Lo ]; rank_to_string; rank_of_string } + ranks = [ Hi1; Hi2; Lo ]; rank_to_string; rank_of_string } let weekday_index d = match D.weekday d with @@ -59,14 +67,15 @@ module Fixture = struct let temporal date : (season, rank) Temporal.t = { Temporal.season = season date; week = None; weekday = D.weekday date; office = office date } - (* Band: Hi beats Lo; Temporal breaks a tie in its own favour -- the same - convention test_precedence.ml uses. *) + (* Band: Hi1 beats Hi2 beats Lo; Temporal breaks a tie against a Lo-rank + Sanctoral entry in its own favour -- the same convention + test_precedence.ml uses. *) let band (_ : season P.context) (c : rank P.candidate) = - (match c.P.cel.Cel.rank with Hi -> 10 | Lo -> 20) + (match c.P.cel.Cel.rank with Hi1 -> 5 | Hi2 -> 10 | Lo -> 20) - (match c.P.origin with P.Temporal -> 1 | P.Sanctoral -> 0) let disposition ~winner:_ ~(loser : rank P.candidate) = - match loser.P.cel.Cel.rank with Lo -> P.Commemorate P.Ordinary | Hi -> P.Transfer + match loser.P.cel.Cel.rank with Lo -> P.Commemorate P.Ordinary | Hi1 | Hi2 -> P.Transfer (* Admits at most one commemoration -- mirrors test_precedence.ml's own example and, unlike "admit everything", actually gives the accounting @@ -77,12 +86,12 @@ module Fixture = struct (* RG 96, generic form: search forward from the day after [origin] for the first day whose occupant is not "blocking" -- in this synthetic - vocabulary Hi stands in for I/II class, Lo for everything else (the same - convention [band] already uses). No Annunciation-style starting-point - override: that exception is EF-specific (RG 96) and belongs to the real - rite (Task 11, pinned by Task 17's golden years), not to this - abstraction-level fixture, which only has to prove Calendar's placement - mechanism, not EF's own rubrics. *) + vocabulary Hi1/Hi2 stand in for I/II class, Lo for everything else (the + same convention [band] already uses). No Annunciation-style + starting-point override: that exception is EF-specific (RG 96) and + belongs to the real rite (Task 11, pinned by Task 17's golden years), + not to this abstraction-level fixture, which only has to prove + Calendar's placement mechanism, not EF's own rubrics. *) let transfer_target (_ : rank P.candidate) (origin : D.t) (occupant : D.t -> rank Cel.t) : D.t = let rec search d = if (occupant d).Cel.rank = Lo then d else search (D.add_days d 1) in search (D.add_days origin 1) @@ -96,20 +105,20 @@ module Fixture = struct cel = Cel.make ~slug:(Sl.of_string_exn slug) ~rank ~colour:Colour.White ~layer:"synthetic-sanctoral" () } - let big_feast = entry ~month:12 ~day:8 ~slug:"big-feast" ~rank:Hi + let big_feast = entry ~month:12 ~day:8 ~slug:"big-feast" ~rank:Hi1 let commem_worthy = entry ~month:12 ~day:15 ~slug:"commem-worthy" ~rank:Lo (* 20 Dec: four sanctoral entries on one date, for the full-accounting test. - "day-winner" and "eclipsed" tie on band (both Hi, both Sanctoral); ties - break on slug, so "day-winner" wins and "eclipsed" -- a Hi-rank loser -- - is [Transfer]-disposed, landing in [deferred]. "loser-a" and "loser-b" - are both Lo, both [Commemorate]-disposed, but [admit] only keeps one: - the other lands in Precedence's own [omitted] ("admission limit - reached"), distinct from "eclipsed"'s deferred reason. Four candidates, - three different fates -- observed, one specific omission reason, two - more. *) - let day_winner = entry ~month:12 ~day:20 ~slug:"day-winner" ~rank:Hi - let eclipsed = entry ~month:12 ~day:20 ~slug:"eclipsed" ~rank:Hi + "day-winner" and "eclipsed" tie on band (both Hi1, both Sanctoral); + ties break on slug, so "day-winner" wins and "eclipsed" -- a Hi1-rank + loser -- is [Transfer]-disposed, landing in [deferred]. "loser-a" and + "loser-b" are both Lo, both [Commemorate]-disposed, but [admit] only + keeps one: the other lands in Precedence's own [omitted] ("admission + limit reached"), distinct from "eclipsed"'s deferred reason. Four + candidates, three different fates -- observed, one specific omission + reason, two more. *) + let day_winner = entry ~month:12 ~day:20 ~slug:"day-winner" ~rank:Hi1 + let eclipsed = entry ~month:12 ~day:20 ~slug:"eclipsed" ~rank:Hi1 let loser_a = entry ~month:12 ~day:20 ~slug:"loser-a" ~rank:Lo let loser_b = entry ~month:12 ~day:20 ~slug:"loser-b" ~rank:Lo @@ -118,33 +127,40 @@ module Fixture = struct [ big_feast; commem_worthy; day_winner; eclipsed; loser_a; loser_b ] (* RG 96 (Task 6): "transferable" is impeded on 10 Jan by "blocker-a" (both - Hi; ties break on slug, "blocker-a" < "transferable", so "blocker-a" + Hi1; ties break on slug, "blocker-a" < "transferable", so "blocker-a" wins and "transferable" is the loser). 11 and 12 Jan are ALSO occupied - by their own uncontested Hi-rank entries, so the placement search must + by their own uncontested Hi1-rank entries, so the placement search must walk past more than one ineligible day, not just try origin+1 and stop. 13 Jan carries nothing, so the feria (Lo) is the first admissible day. *) - let blocker_a = entry ~month:1 ~day:10 ~slug:"blocker-a" ~rank:Hi - let transferable = entry ~month:1 ~day:10 ~slug:"transferable" ~rank:Hi - let blocker_b = entry ~month:1 ~day:11 ~slug:"blocker-b" ~rank:Hi - let blocker_c = entry ~month:1 ~day:12 ~slug:"blocker-c" ~rank:Hi - - (* RG 97-98: three Hi-rank entries coincide on 1 Feb. Sorted by band then - slug (all three tie on band, since Fixture's [band] only reads rank): - "collision-winner" < "transfer-a" < "transfer-b". The winner keeps 1 - Feb; the other two -- both losers, both Hi, both [Transfer]-disposed -- - must transfer in that same order. 2 and 3 Feb carry nothing of their - own, so they are the two admissible days the pair must land on, - consecutively, in that order: "transfer-a" (the higher-precedence - loser) gets first claim on 2 Feb, pushing "transfer-b" to 3 Feb. *) - let collision_winner = entry ~month:2 ~day:1 ~slug:"collision-winner" ~rank:Hi - let transfer_a = entry ~month:2 ~day:1 ~slug:"transfer-a" ~rank:Hi - let transfer_b = entry ~month:2 ~day:1 ~slug:"transfer-b" ~rank:Hi + let blocker_a = entry ~month:1 ~day:10 ~slug:"blocker-a" ~rank:Hi1 + let transferable = entry ~month:1 ~day:10 ~slug:"transferable" ~rank:Hi1 + let blocker_b = entry ~month:1 ~day:11 ~slug:"blocker-b" ~rank:Hi1 + let blocker_c = entry ~month:1 ~day:12 ~slug:"blocker-c" ~rank:Hi1 + + (* RG 97-98: three entries coincide on 1 Feb, spanning both Transfer- + disposed ranks so band order and slug order genuinely disagree (Task 6 + review finding 2). "collision-winner" and "transfer-hi1" both tie at + the BETTER band (Hi1, 5); "transfer-hi2" is at the WORSE band (Hi2, + 10). Within the Hi1 tie, slug decides: "collision-winner" < "transfer- + hi1", so "collision-winner" keeps 1 Feb. Of the two losers, + "transfer-hi1" (band 5) outranks "transfer-hi2" (band 10) -- by BAND, + not by slug: "transfer-b" (transfer-hi2's slug) sorts alphabetically + *before* "transfer-z" (transfer-hi1's slug). A sort that used slug + instead of band, or compared band backwards, would place "transfer-b" + on 2 Feb instead of "transfer-z" -- exactly the wrong-order failure + mode finding 2 flagged as unreachable in the old two-Hi-rank fixture. + 2 and 3 Feb carry nothing of their own, so they are the two admissible + days the pair must land on, consecutively, in band order: + "transfer-hi1" claims 2 Feb, pushing "transfer-hi2" to 3 Feb. *) + let collision_winner = entry ~month:2 ~day:1 ~slug:"collision-winner" ~rank:Hi1 + let transfer_hi1 = entry ~month:2 ~day:1 ~slug:"transfer-z" ~rank:Hi1 + let transfer_hi2 = entry ~month:2 ~day:1 ~slug:"transfer-b" ~rank:Hi2 let layer_with_collision = Layer.of_entries ~id:"synthetic-with-collision" ~name:"Synthetic sanctoral (with collisions)" [ big_feast; commem_worthy; day_winner; eclipsed; loser_a; loser_b; blocker_a; transferable; blocker_b; blocker_c; - collision_winner; transfer_a; transfer_b ] + collision_winner; transfer_hi1; transfer_hi2 ] let liturgical_year_of date = let cy = D.year date in @@ -231,7 +247,7 @@ let test_day_near_domain_floor_does_not_raise () = duplicated into two buckets and another dropped, which this project has shipped before (register finding). - "eclipsed" -- the Hi-rank loser on 20 Dec -- no longer sits in [omitted] + "eclipsed" -- the Hi1-rank loser on 20 Dec -- no longer sits in [omitted] here (that was Task 5's honest placeholder, before Task 6 existed to place it): RG 95 gives an I-class loser the right of translation, so it is genuinely gone from this day's own accounting, and its departure is @@ -265,14 +281,14 @@ let test_full_day_accounting () = not something new. What IS new here: this day positively records that a transfer happened, via a different field entirely. *) Alcotest.(check bool) "20 Dec records that something transferred out" true - (d.LD.transferred_out <> None) + (d.LD.transferred_out <> []) (* Task 6's placement pass (RG 96-98), properties 1 and 2: a transferred celebration appears exactly once in the whole year -- transfer moves, not duplicates -- and [transferred_in]/[transferred_out] are set on the two ends of the move and point at each other. "transferable" is impeded on 10 Jan by "blocker-a" (same band, tie-broken by slug), and 11-12 Jan are also - occupied by their own uncontested Hi entries, so this also proves the + occupied by their own uncontested Hi1 entries, so this also proves the search walks past more than one ineligible day rather than only trying origin+1. *) let test_transfer_moves_and_does_not_duplicate () = @@ -292,22 +308,31 @@ let test_transfer_moves_and_does_not_duplicate () = | Some c -> Sl.to_string c.Cel.slug | None -> ""); (* Located by its own known origin date, not by "the first day with - transferred_out set" -- layer_with_collision has more than one day that - transfers something out (20 Dec's "eclipsed", 1 Feb's "transfer-b"), so - that would silently pick up whichever happens to sort first in the - array rather than proving THIS origin points at THIS landing. *) + transferred_out <> []" -- layer_with_collision has more than one day + that transfers something out (20 Dec's "eclipsed", 1 Feb's two losers), + so that would silently pick up whichever happens to sort first in the + array rather than proving THIS origin points at THIS landing. Its own + origin has exactly one departure -- unlike 1 Feb below -- so a single + pair pins it. *) let origin = Array.to_list days |> List.find (fun d -> D.compare d.LD.date (mk 2027 1 10) = 0) in - Alcotest.(check bool) "origin points at the landing date" true - (origin.LD.transferred_out = Some landed.LD.date) - -(* Property 3: RG 97-98's ordering. Two Hi-rank losers coincide on 1 Feb - (with "collision-winner" keeping the day); band ties, so slug order IS - band order here, same convention Precedence.compare_by uses for real RG - 91 entries that tie within one table slot. Checked by DATE, not by - "b landed one day after a" -- Task 5's review flagged exactly that - style of check as satisfiable by construction (an Array.init built from - add_days would pass it trivially); asserting the literal landing dates - independently is what actually exercises the placement order. *) + Alcotest.(check int) "exactly one departure recorded at the origin" 1 + (List.length origin.LD.transferred_out); + let departed_cel, departed_to = List.hd origin.LD.transferred_out in + Alcotest.(check string) "the departed celebration is \"transferable\"" "transferable" + (Sl.to_string departed_cel.Cel.slug); + Alcotest.(check string) "it points at the landing date" (D.to_iso8601 landed.LD.date) + (D.to_iso8601 departed_to) + +(* Property 3: RG 97-98's ordering, genuinely by band (Task 6 review finding + 2) -- see the [layer_with_collision] comment for how the fixture is built + so band order and slug order actively disagree here: "transfer-hi1" + (slug "transfer-z", band 5) must claim 2 Feb before "transfer-hi2" (slug + "transfer-b", band 10), even though "transfer-b" sorts alphabetically + first. Checked by DATE, not by "b landed one day after a" -- Task 5's + review flagged exactly that style of check as satisfiable by construction + (an Array.init built from add_days would pass it trivially); asserting + the literal landing dates independently is what actually exercises the + placement order. *) let test_two_colliding_transferables_land_in_band_order () = let days = C.year Fixture.rite Fixture.layer_with_collision 2026 in let observed_on date = @@ -317,18 +342,66 @@ let test_two_colliding_transferables_land_in_band_order () = in Alcotest.(check string) "collision-winner keeps 1 Feb" "collision-winner" (observed_on (mk 2027 2 1)); - Alcotest.(check string) "higher-precedence loser (transfer-a) claims 2 Feb first" "transfer-a" + Alcotest.(check string) "higher-band loser (transfer-z, Hi1) claims 2 Feb first" "transfer-z" (observed_on (mk 2027 2 2)); - Alcotest.(check string) "lower-precedence loser (transfer-b) is pushed to 3 Feb" "transfer-b" + Alcotest.(check string) "lower-band loser (transfer-b, Hi2) is pushed to 3 Feb" "transfer-b" (observed_on (mk 2027 2 3)); let count slug = Array.to_list days |> List.filter (fun d -> Sl.to_string d.LD.observed.Cel.slug = slug) |> List.length in - Alcotest.(check int) "transfer-a appears exactly once in the year" 1 (count "transfer-a"); + Alcotest.(check int) "transfer-z appears exactly once in the year" 1 (count "transfer-z"); Alcotest.(check int) "transfer-b appears exactly once in the year" 1 (count "transfer-b") +(* Task 6 review finding 1: RG 97-98 says coinciding I-class feasts transfer + "in order" -- plural -- so 1 Feb's origin must record BOTH departures + ("transfer-z" -> 2 Feb, "transfer-b" -> 3 Feb), not just one. The + original [Date.t option] could only ever hold one; with three entries + colliding on the same date it silently dropped whichever [Hashtbl.iter] + visited last, which depends on OCaml's hash seed (OCAMLRUNPARAM=R) -- an + environment read in a kernel whose invariants forbid one. Sorting both + sides before comparing makes this assertion itself independent of + [transferred_out]'s own (now canonicalised, but not part of the + contract) internal order. *) +let test_origin_records_every_departure () = + let days = C.year Fixture.rite Fixture.layer_with_collision 2026 in + let origin = Array.to_list days |> List.find (fun d -> D.compare d.LD.date (mk 2027 2 1) = 0) in + let departures = + origin.LD.transferred_out + |> List.map (fun (c, target) -> (Sl.to_string c.Cel.slug, D.to_iso8601 target)) + |> List.sort compare + in + Alcotest.(check (list (pair string string))) + "both losers' departures are recorded, order-independently" + (List.sort compare [ ("transfer-z", "2027-02-02"); ("transfer-b", "2027-02-03") ]) + departures + +(* Task 6 review finding 3: a rite whose [transfer_target] names a date + outside the liturgical year's own [start, stop] must not make the + candidate vanish. "eclipsed" is impeded on 20 Dec as usual, but this + rite's search jumps 5000 days forward -- far past [stop] -- instead of + walking to the next admissible day. It must never become [observed] + anywhere in the array (there is nowhere in the array for it to land), + and its origin must record the specific out-of-range reason, not the + generic non-convergence one (this placement decides on round 1; the + round guard is never even approached). *) +let test_transfer_target_outside_year_is_recorded_not_lost () = + let stray_rite = + { Fixture.rite with Rite.transfer_target = (fun _ origin _ -> D.add_days origin 5000) } + in + let days = C.year stray_rite Fixture.layer 2026 in + let observed_anywhere = + Array.to_list days |> List.exists (fun d -> Sl.to_string d.LD.observed.Cel.slug = "eclipsed") + in + Alcotest.(check bool) "never becomes observed anywhere in the year" false observed_anywhere; + let origin = Array.to_list days |> List.find (fun d -> D.compare d.LD.date (mk 2026 12 20) = 0) in + let reason_of slug = + origin.LD.omitted |> List.find (fun (c, _) -> Sl.to_string c.Cel.slug = slug) |> snd + in + Alcotest.(check string) "recorded with the out-of-range reason, not silently dropped" + "omitted: transfer target falls outside the liturgical year (RG 96)" (reason_of "eclipsed") + (* Termination is a correctness requirement (brief): a rite whose [transfer_target] always answers with the impeded day itself (never strictly forward, so the pass can never reach a fixed point) must not @@ -366,5 +439,9 @@ let suite = test_transfer_moves_and_does_not_duplicate; Alcotest.test_case "two colliding transferables land in band order" `Quick test_two_colliding_transferables_land_in_band_order; + Alcotest.test_case "origin records every departure" `Quick + test_origin_records_every_departure; + Alcotest.test_case "transfer target outside year is recorded not lost" `Quick + test_transfer_target_outside_year_is_recorded_not_lost; Alcotest.test_case "transfer guard records failure instead of looping" `Quick test_transfer_guard_records_failure_instead_of_looping ] ) -- cgit v1.3