diff options
| -rw-r--r-- | lib/kernel/calendar.ml | 157 | ||||
| -rw-r--r-- | lib/kernel/calendar.mli | 31 | ||||
| -rw-r--r-- | lib/kernel/liturgical_day.ml | 9 | ||||
| -rw-r--r-- | lib/kernel/liturgical_day.mli | 9 | ||||
| -rw-r--r-- | test/test_calendar.ml | 207 |
5 files changed, 296 insertions, 117 deletions
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 + 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 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 + (* 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 -> "<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) + 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. 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. *) +(* 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 ] ) |