From 6436509d6b599b7d7c6467bd39c8090cb9634889 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Tue, 11 Aug 2026 19:39:37 +0200 Subject: kernel(rite): bundle what a rite supplies; make season runs rite-supplied Validate took four loose arguments that had to come from the same rite with nothing enforcing it, and Calendar is about to add more. Bundling makes a mismatched assembly unrepresentable through the normal path. season_runs replaces the hardcoded assumption that every season occupies exactly one unbroken run. That holds for the 1962 rite but is false for the modern form's Ordinary Time, which is one season in two runs -- as written the check would have reported a false failure every year for the second rite. --- lib/kernel/rite.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 lib/kernel/rite.ml (limited to 'lib/kernel/rite.ml') diff --git a/lib/kernel/rite.ml b/lib/kernel/rite.ml new file mode 100644 index 0000000..b948390 --- /dev/null +++ b/lib/kernel/rite.ml @@ -0,0 +1,12 @@ +(* 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; +} -- cgit v1.3 From f15e44dd4c1b871c2daeb952b1c8c848274ea1f1 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Tue, 11 Aug 2026 21:03:00 +0200 Subject: kernel(calendar): place transferred celebrations (RG 96-98) Calendar.year now runs a placement pass after resolving every day: each deferred candidate (RG 95's I-class-only right of translation, via Precedence's Transfer disposition) is placed on the next day the rite's new Rite.t.transfer_target names as admissible, transferred_in/out are set on the two ends of the move, and the whole year is re-resolved to a fixed point, bounded by a hard max_transfer_rounds = 64 guard. transfer_target is rite-supplied rather than a generic search Calendar drives itself: RG 96's 'not I or II class' is not derivable from band or disposition alone (RG 91's own table lets a universal I-class feast outrank an ordinary Sunday in a raw contest, yet RG 96 forbids landing a translation there regardless), and the search's starting point is rite-specific too (the Annunciation exception). It takes an occupant callback exposing what Calendar currently resolves as observed on any date, so the rite never has to re-implement occurrence resolution. Two correctness properties drove most of the design: - A candidate's permanent natural loss at its own origin (the layer entry never moves) is rediscovered every round; left unfiltered this oscillates a placed candidate between two dates forever, since its own rank makes it look 'occupied' to a fresh search from its origin. Both the round loop's gather and the final per-day omitted accounting filter this out, keeping only sightings that are either brand new or losing at a candidate's *current* target (a fresh RG 97-98 bump). - RG 97-98's sort has to actually decide something, not just happen to agree with Precedence.resolve's own tie-break next round: a claimed-this-round overlay lets earlier-processed candidates in one round block later ones in the same pass, so two coinciding I-class feasts land on consecutive admissible days in the one round they collide, in band order. Also folds in Task 5's review finding: year_bounds clamps y to [1582, 9999] once, up front, rather than guarding start and stop independently (each guard only ever covered one of the two rite.year_start calls, leaving year 999 and year 100000 each able to call it out of domain through the other branch). --- lib/kernel/calendar.ml | 256 +++++++++++++++++++++++++++++++++++++++++++----- lib/kernel/calendar.mli | 29 +++--- lib/kernel/rite.ml | 2 + lib/kernel/rite.mli | 24 +++++ test/test_calendar.ml | 177 +++++++++++++++++++++++++++++---- test/test_validate.ml | 13 ++- 6 files changed, 444 insertions(+), 57 deletions(-) (limited to 'lib/kernel/rite.ml') diff --git a/lib/kernel/calendar.ml b/lib/kernel/calendar.ml index 1cdd1fa..1ad45a1 100644 --- a/lib/kernel/calendar.ml +++ b/lib/kernel/calendar.ml @@ -27,44 +27,249 @@ let domain_max_date = 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. *) + 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) -(* [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 - the same test as resolving the spec against [date]'s own year and - comparing, so no separate filter is needed here. *) -let resolve_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) (date : Date.t) : - ('s, 'r) Liturgical_day.t = + 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 sanctoral = + 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 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)" + +(* 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). + + 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. *) +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 = + 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 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), 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) + 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 + 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 + done; + (assignment, candidate_by_slug) + +(* 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. *) +let build_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) + (assignment : (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 = + 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 Some (Hashtbl.find transferred_out_of (Date.to_rata date)) with Not_found -> None + 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. 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. *) + 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) + in 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 + @ (resolution.Precedence.deferred |> List.filter unresolved + |> List.map (fun c -> (c.Precedence.cel, unconverged_reason))) in { Liturgical_day.date; @@ -73,8 +278,8 @@ let resolve_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) (date : Date.t observed = resolution.Precedence.observed.Precedence.cel; commemorations = List.map (fun (c, p) -> (c.Precedence.cel, p)) resolution.Precedence.commemorations; - transferred_in = None; - transferred_out = None; + transferred_in; + transferred_out; omitted; citations = []; } @@ -90,7 +295,14 @@ let year (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) (y : int) : [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 - Array.init n (fun i -> resolve_day rite idx (Date.add_days start i)) + 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 injected = injected_index_of_assignment assignment candidate_by_slug in + let transferred_out_of : (int, Date.t) Hashtbl.t = Hashtbl.create 16 in + Hashtbl.iter + (fun _slug (origin, target) -> Hashtbl.replace transferred_out_of (Date.to_rata origin) target) + assignment; + Array.map (build_day rite idx assignment 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 2469f2a..9fbd7e7 100644 --- a/lib/kernel/calendar.mli +++ b/lib/kernel/calendar.mli @@ -7,23 +7,28 @@ one pass -- and [day] is derived: it finds the liturgical year containing a date and indexes into it. Both are pure; neither caches. - 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 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. *) + 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, + [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. *) (** [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: + 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 diff --git a/lib/kernel/rite.ml b/lib/kernel/rite.ml index b948390..89fceb6 100644 --- a/lib/kernel/rite.ml +++ b/lib/kernel/rite.ml @@ -9,4 +9,6 @@ type ('s, 'r) 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 index db8e86f..6d12dd4 100644 --- a/lib/kernel/rite.mli +++ b/lib/kernel/rite.mli @@ -15,4 +15,28 @@ type ('s, 'r) t = { (** 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". *) } diff --git a/test/test_calendar.ml b/test/test_calendar.ml index d34611a..70823a4 100644 --- a/test/test_calendar.ml +++ b/test/test_calendar.ml @@ -75,9 +75,21 @@ module Fixture = struct let rules : (season, rank) P.rules = { P.band; disposition; admit = (fun ~observed:_ cs -> List.filteri (fun i _ -> i < 1) cs) } + (* 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. *) + 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) + let rite : (season, rank) Rite.t = { Rite.id = "synthetic-calendar"; vocab; year_start; temporal; anchors = (fun _ -> []); - rules; season_runs = [ A; B ] } + rules; season_runs = [ A; B ]; transfer_target } let entry ~month ~day ~slug ~rank = { Layer.date = (match Date_spec.fixed ~month ~day with Ok d -> d | Error e -> failwith e); @@ -105,6 +117,35 @@ module Fixture = struct Layer.of_entries ~id:"synthetic" ~name:"Synthetic sanctoral" [ 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" + 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 + 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 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 ] + let liturgical_year_of date = let cy = D.year date in if D.compare date (year_start cy) >= 0 then cy else cy - 1 @@ -183,11 +224,19 @@ let test_day_near_domain_floor_does_not_raise () = (* 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). *) + entries -- is accounted for exactly once across + observed/commemorations/omitted/transferred_out. 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). + + "eclipsed" -- the Hi-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 + what [transferred_out] records instead. [test_transfer_moves_and_does_not_duplicate] + below is what actually pins where it lands. *) let test_full_day_accounting () = let date = mk 2026 12 20 in let d = C.day Fixture.rite Fixture.layer date in @@ -197,23 +246,109 @@ let test_full_day_accounting () = :: 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" ] + Alcotest.(check (slist string compare)) "every non-transferred candidate appears exactly once" + [ feria_slug; "day-winner"; "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 + (* Identity within [omitted]: "loser-a"/"loser-b" -- the ones Precedence's + own [admit] dropped for exceeding the commemoration limit, not RG 96-98 + translation -- must carry that specific reason. Without this, a bug + that 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") + "omitted: admission limit reached" (reason_of "loser-a"); + (* Not "eclipsed is absent from bucketed" -- the [slist] check just above + already guarantees that (a 5-element set would fail it), so re-asserting + absence from the same list would be checking something already proven, + 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) + +(* 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 + search walks past more than one ineligible day rather than only trying + origin+1. *) +let test_transfer_moves_and_does_not_duplicate () = + let days = C.year Fixture.rite Fixture.layer_with_collision 2026 in + let occurrences = + Array.to_list days + |> List.filter (fun d -> Sl.to_string d.LD.observed.Cel.slug = "transferable") + in + Alcotest.(check int) "appears exactly once" 1 (List.length occurrences); + let landed = List.hd occurrences in + Alcotest.(check string) "lands on the first day past the blocked run (13 Jan 2027)" + "2027-01-13" (D.to_iso8601 landed.LD.date); + Alcotest.(check bool) "marked as transferred in" true (landed.LD.transferred_in <> None); + Alcotest.(check string) "the arriving celebration is itself \"transferable\"" + "transferable" + (match landed.LD.transferred_in with + | 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. *) + 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. *) +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 = + Array.to_list days + |> List.find (fun d -> D.compare d.LD.date date = 0) + |> fun d -> Sl.to_string d.LD.observed.Cel.slug + 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" + (observed_on (mk 2027 2 2)); + Alcotest.(check string) "lower-precedence loser (transfer-b) 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-b appears exactly once in the year" 1 (count "transfer-b") + +(* 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 + hang the computation. It has to hit [max_transfer_rounds] and come back + with the stuck candidate recorded as omitted -- not dropped, not looping + forever. Using plain [Fixture.layer] (20 Dec's "eclipsed" is the stuck + candidate) is enough; this is about the guard firing, not about any + particular collision shape. *) +let test_transfer_guard_records_failure_instead_of_looping () = + let broken_rite = { Fixture.rite with Rite.transfer_target = (fun _ origin _ -> origin) } in + let days = C.year broken_rite Fixture.layer 2026 in + let stuck = + Array.to_list days + |> List.exists (fun d -> + List.exists + (fun (_, reason) -> + reason = "omitted: transfer placement did not converge within max_transfer_rounds (RG 96-98)") + d.LD.omitted) + in + Alcotest.(check bool) "non-convergence is recorded rather than silently dropped or hung" true stuck let suite = ( "Calendar", @@ -226,4 +361,10 @@ let suite = 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; - Alcotest.test_case "full day accounting" `Quick test_full_day_accounting ] ) + Alcotest.test_case "full day accounting" `Quick test_full_day_accounting; + Alcotest.test_case "transfer moves and does not duplicate" `Quick + 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 "transfer guard records failure instead of looping" `Quick + test_transfer_guard_records_failure_instead_of_looping ] ) diff --git a/test/test_validate.ml b/test/test_validate.ml index 31d7a3d..df8c99c 100644 --- a/test/test_validate.ml +++ b/test/test_validate.ml @@ -5,9 +5,9 @@ module V = Rite_ef.Vocab_ef module T = Rite_ef.Temporal_ef (* Plan 3's real EF precedence rules (Precedence_ef, Tasks 7-11) don't exist - yet -- Validate.run doesn't read [rules] at all (nothing does before - Task 5's Calendar), so a placeholder is enough to assemble a well-typed - Rite.t here. *) + yet -- Validate.run doesn't read [rules] or [transfer_target] at all + (nothing does before Task 5's Calendar and Task 6's placement pass), so a + placeholder is enough to assemble a well-typed Rite.t here. *) let ef_rules : (V.season, V.rank) P.rules = { P.band = (fun _ _ -> 0); disposition = (fun ~winner:_ ~loser:_ -> P.Omit); @@ -15,7 +15,8 @@ let ef_rules : (V.season, V.rank) P.rules = let ef_rite : (V.season, V.rank) Rite.t = { Rite.id = T.id; vocab = V.vocab; year_start = T.year_start; temporal = T.temporal; - anchors = T.anchors; rules = ef_rules; season_runs = V.seasons } + anchors = T.anchors; rules = ef_rules; season_runs = V.seasons; + transfer_target = (fun _ origin _ -> origin) } let run year = Val.run ef_rite ~year @@ -174,7 +175,9 @@ module Synthetic = struct let rite ?(vocab = vocab) ?(anchors = fun _ -> []) ?(season_runs = [ A; B ]) temporal : (season, rank) Rite.t = - { Rite.id = "synthetic"; vocab; year_start; temporal; anchors; rules; season_runs } + { Rite.id = "synthetic"; vocab; year_start; temporal; anchors; rules; season_runs; + (* Validate.run doesn't read this either (see [ef_rules] above). *) + transfer_target = (fun _ origin _ -> origin) } let run ?vocab ?anchors ?season_runs temporal = Val.run (rite ?vocab ?anchors ?season_runs temporal) ~year:2026 -- cgit v1.3