diff options
| author | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-11 21:03:00 +0200 |
|---|---|---|
| committer | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-11 21:03:00 +0200 |
| commit | f15e44dd4c1b871c2daeb952b1c8c848274ea1f1 (patch) | |
| tree | 2e2f73260780f43a9d9a3e38ed9c181f94c9d50b /test | |
| parent | 953427d8d1e3a34994be53b60e18662ec26fef4e (diff) | |
| download | colitur-f15e44dd4c1b871c2daeb952b1c8c848274ea1f1.tar.gz colitur-f15e44dd4c1b871c2daeb952b1c8c848274ea1f1.zip | |
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).
Diffstat (limited to 'test')
| -rw-r--r-- | test/test_calendar.ml | 177 | ||||
| -rw-r--r-- | test/test_validate.ml | 13 |
2 files changed, 167 insertions, 23 deletions
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 -> "<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 |
