From 8ab24da337a10993b98696df5d499706318beb8e Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Tue, 11 Aug 2026 19:02:08 +0200 Subject: kernel(celebration): distinguish a feast from a commemoration-only entry The 1960 reform reduced many feasts to a bare commemoration. They keep a rank, because RG 111 orders admitted commemorations by dignity, but they can never be the observed day. Modelled as a separate status rather than a fifth rank: RG 8 fixes the classes at four. --- lib/kernel/celebration.ml | 13 ++++++++++--- lib/kernel/celebration.mli | 12 ++++++++++-- 2 files changed, 20 insertions(+), 5 deletions(-) (limited to 'lib/kernel') diff --git a/lib/kernel/celebration.ml b/lib/kernel/celebration.ml index 2963366..eb4249e 100644 --- a/lib/kernel/celebration.ml +++ b/lib/kernel/celebration.ml @@ -8,10 +8,17 @@ open Sexplib0.Sexp_conv but would carry no information while forcing every consumer (Layer, Overlay, and later Precedence and Calendar) to thread a variable that means nothing. *) +(* Whether this celebration can be the observed day at all. The 1960 reform + reduced many feasts to a bare commemoration; they retain a rank (RG 111 orders + admitted commemorations by dignity) but can never be observed. NOT a fifth + rank: RG 8 fixes the classes at four. *) +type status = Feast | Commemoration_only [@@deriving sexp] + type 'r t = { slug : Slug.t; names : Names.t; rank : 'r; + status : status; colour : Colour.t; subject : Subject.t; citations : Citation.t list; @@ -19,6 +26,6 @@ type 'r t = { } [@@deriving sexp] -let make ~slug ?(names = Names.empty) ~rank ~colour ?(subject = Subject.Temporal) - ?(citations = []) ~layer () = - { slug; names; rank; colour; subject; citations; layer } +let make ~slug ?(names = Names.empty) ~rank ?(status = Feast) ~colour + ?(subject = Subject.Temporal) ?(citations = []) ~layer () = + { slug; names; rank; status; colour; subject; citations; layer } diff --git a/lib/kernel/celebration.mli b/lib/kernel/celebration.mli index 1c84d35..a3c2960 100644 --- a/lib/kernel/celebration.mli +++ b/lib/kernel/celebration.mli @@ -1,8 +1,15 @@ +(** Whether this celebration can be the observed day at all. The 1960 reform + reduced many feasts to a bare commemoration; they retain a rank (RG 111 + orders admitted commemorations by dignity) but can never be observed. NOT + a fifth rank: RG 8 fixes the classes at four. *) +type status = Feast | Commemoration_only [@@deriving sexp] + (** A celebration. Parameterised by the rite's rank type only. *) type 'r t = { slug : Slug.t; names : Names.t; rank : 'r; + status : status; colour : Colour.t; subject : Subject.t; citations : Citation.t list; @@ -10,7 +17,8 @@ type 'r t = { } [@@deriving sexp] -(** [subject] defaults to [Subject.Temporal], [names] to empty, [citations] to []. *) +(** [status] defaults to [Feast], [subject] to [Subject.Temporal], [names] to + empty, [citations] to []. *) val make : - slug:Slug.t -> ?names:Names.t -> rank:'r -> colour:Colour.t -> + slug:Slug.t -> ?names:Names.t -> rank:'r -> ?status:status -> colour:Colour.t -> ?subject:Subject.t -> ?citations:Citation.t list -> layer:string -> unit -> 'r t -- cgit v1.3 From 19d5bbaab8fbf40f6fa6de8906169e3bb7144e1f Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Tue, 11 Aug 2026 19:07:11 +0200 Subject: kernel(precedence): rite-parameterised resolver Three rite-supplied functions, not one: band (who wins, RG 91), disposition (what happens to the loser, RG 92-95) and admit (how many commemorations are admitted, RG 111). The loser's fate depends on the loser's own rank, so conflating them would resist extension. resolve takes the temporal candidate separately from the sanctoral list, which makes it total by construction. Every candidate lands in exactly one of observed, commemorations, deferred or omitted -- nothing is dropped silently, which is what makes the no-celebration-lost invariant checkable. --- lib/kernel/precedence.ml | 69 ++++++++++++++++++++++++++++++++++++++++++ lib/kernel/precedence.mli | 60 +++++++++++++++++++++++++++++++++++++ test/test_colitur.ml | 2 +- test/test_precedence.ml | 76 +++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 206 insertions(+), 1 deletion(-) create mode 100644 lib/kernel/precedence.ml create mode 100644 lib/kernel/precedence.mli create mode 100644 test/test_precedence.ml (limited to 'lib/kernel') diff --git a/lib/kernel/precedence.ml b/lib/kernel/precedence.ml new file mode 100644 index 0000000..05ad69f --- /dev/null +++ b/lib/kernel/precedence.ml @@ -0,0 +1,69 @@ +(* The rite-parameterised resolver. RG 91 says who wins; RG 92-95 says what + happens to the loser; RG 108-111 says how many commemorations are admitted. + Three separate functions, because the loser's fate depends on the loser's own + rank, not the winner's. *) +open Sexplib0.Sexp_conv + +type origin = Temporal | Sanctoral [@@deriving sexp] +type privilege = Privileged | Ordinary [@@deriving sexp] +type disposition = Omit | Commemorate of privilege | Transfer | Repose [@@deriving sexp] + +type 'r candidate = { cel : 'r Celebration.t; origin : origin } [@@deriving sexp] + +type 's context = { date : Date.t; season : 's; weekday : Date.weekday } + +type ('s, 'r) rules = { + band : 's context -> 'r candidate -> int; + disposition : winner:'r candidate -> loser:'r candidate -> disposition; + admit : + observed:'r candidate -> + ('r candidate * privilege) list -> + ('r candidate * privilege) list; +} + +type 'r resolution = { + observed : 'r candidate; + commemorations : ('r candidate * privilege) list; + deferred : 'r candidate list; + omitted : ('r candidate * string) list; +} + +(* Ties break on slug so the result never depends on input order. *) +let compare_by rules ctx a b = + let ba = rules.band ctx a and bb = rules.band ctx b in + if ba <> bb then Int.compare ba bb + else Slug.compare a.cel.Celebration.slug b.cel.Celebration.slug + +let resolve rules ctx ~temporal ~sanctoral = + (* A commemoration-only entry can never be observed (see Celebration.status), + so it is held out of the contest entirely rather than relying on its band. *) + let eligible, forced_comm = + List.partition + (fun c -> c.cel.Celebration.status = Celebration.Feast) + sanctoral + in + let sorted = List.stable_sort (compare_by rules ctx) (temporal :: eligible) in + let observed = List.hd sorted in + let losers = List.tl sorted @ forced_comm in + let comms, deferred, omitted = + List.fold_left + (fun (comms, defs, omits) l -> + match rules.disposition ~winner:observed ~loser:l with + | Commemorate p -> ((l, p) :: comms, defs, omits) + | Transfer | Repose -> (comms, l :: defs, omits) + | Omit -> (comms, defs, (l, "omitted: yielded to a higher day") :: omits)) + ([], [], []) losers + in + let comms = List.rev comms and deferred = List.rev deferred in + let admitted = rules.admit ~observed comms in + let dropped = + List.filter (fun c -> not (List.exists (fun a -> fst a == fst c) admitted)) comms + in + { + observed; + commemorations = admitted; + deferred; + omitted = + List.rev omitted + @ List.map (fun (c, _) -> (c, "omitted: admission limit reached")) dropped; + } diff --git a/lib/kernel/precedence.mli b/lib/kernel/precedence.mli new file mode 100644 index 0000000..d30e5c3 --- /dev/null +++ b/lib/kernel/precedence.mli @@ -0,0 +1,60 @@ +(** The rite-parameterised resolver: RG 91 says who wins, RG 92-95 says what + happens to the loser, RG 108-111 says how many commemorations are admitted. + Three separate rite-supplied functions, because the loser's fate depends on + the loser's own rank, not the winner's -- conflating them would resist + extension to a second rite. *) + +(** Which of the day's two office streams a candidate came from. *) +type origin = Temporal | Sanctoral [@@deriving sexp] + +(** RG 111: an admitted commemoration's own standing, distinct from its rank. *) +type privilege = Privileged | Ordinary [@@deriving sexp] + +(** What becomes of a losing candidate. *) +type disposition = + | Omit (** yields with no trace in the day's celebration *) + | Commemorate of privilege (** kept as a commemoration of the observed day *) + | Transfer (** moved to the next free day (RG 92-95) *) + | Repose (** kept only in a votive/private sense; not commemorated today *) +[@@deriving sexp] + +(** A celebration together with the office stream it was drawn from. Parameterised + by the rite's rank type only, matching {!Celebration.t}. *) +type 'r candidate = { cel : 'r Celebration.t; origin : origin } [@@deriving sexp] + +(** The day a resolution is computed for. Parameterised by the rite's season + type only -- a context has no rank of its own. *) +type 's context = { date : Date.t; season : 's; weekday : Date.weekday } + +(** The rite's three resolution functions. *) +type ('s, 'r) rules = { + band : 's context -> 'r candidate -> int; + (** RG 91: orders candidates for the day; lower wins. *) + disposition : winner:'r candidate -> loser:'r candidate -> disposition; + (** RG 92-95: the loser's fate, which depends on the loser's own rank. *) + admit : + observed:'r candidate -> + ('r candidate * privilege) list -> + ('r candidate * privilege) list; + (** RG 108-111: how many commemorations are admitted, and in what order; + anything filtered out here is recorded in {!resolution.omitted}, not + dropped. *) +} + +(** The outcome of resolving one day's candidates. *) +type 'r resolution = { + observed : 'r candidate; + commemorations : ('r candidate * privilege) list; + deferred : 'r candidate list; + omitted : ('r candidate * string) list; (** each with a reason *) +} + +(** Total: the temporal candidate is passed separately, so there is no + empty-candidate case. Ties break on slug, so the result never depends on + input order. A [Commemoration_only] celebration is held out of the contest + and can never be [observed]. Every input candidate appears exactly once in + [observed], [commemorations], [deferred] or [omitted] — nothing is dropped + silently. *) +val resolve : + ('s, 'r) rules -> 's context -> temporal:'r candidate -> + sanctoral:'r candidate list -> 'r resolution diff --git a/test/test_colitur.ml b/test/test_colitur.ml index ae58607..08282e6 100644 --- a/test/test_colitur.ml +++ b/test/test_colitur.ml @@ -2,4 +2,4 @@ let () = Alcotest.run "colitur" [ Test_date.suite; Test_computus.suite; Test_colour.suite; Test_slug.suite; Test_names.suite; - Test_overlay.suite; Test_temporal_ef.suite; Test_validate.suite ] + Test_overlay.suite; Test_temporal_ef.suite; Test_validate.suite; Test_precedence.suite ] diff --git a/test/test_precedence.ml b/test/test_precedence.ml new file mode 100644 index 0000000..39be06c --- /dev/null +++ b/test/test_precedence.ml @@ -0,0 +1,76 @@ +module P = Colitur_kernel.Precedence +module Cel = Colitur_kernel.Celebration +module S = Colitur_kernel.Slug +module Col = Colitur_kernel.Colour +module D = Colitur_kernel.Date + +type rank = Hi | Lo [@@deriving sexp] +type season = Green [@@deriving sexp] + +let cand ?(origin = P.Sanctoral) ?(status = Cel.Feast) ~rank slug = + { P.cel = Cel.make ~slug:(S.of_string_exn slug) ~rank ~status ~colour:Col.White + ~layer:"base" (); origin } + +let ctx = + { P.date = (match D.make ~year:2026 ~month:7 ~day:15 with Ok d -> d | Error e -> failwith e); + season = Green; weekday = D.Wed } + +(* Band: Hi beats Lo. Temporal breaks a tie in its own favour. *) +let rules = + { P.band = (fun _ c -> (match c.P.cel.Cel.rank with Hi -> 10 | Lo -> 20) + - (match c.P.origin with P.Temporal -> 1 | P.Sanctoral -> 0)); + disposition = + (fun ~winner:_ ~loser -> + match loser.P.cel.Cel.status with + | Cel.Commemoration_only -> P.Commemorate P.Ordinary + | Cel.Feast -> (match loser.P.cel.Cel.rank with + | Hi -> P.Transfer + | Lo -> P.Commemorate P.Ordinary)); + admit = (fun ~observed:_ cs -> List.filteri (fun i _ -> i < 2) cs) } + +let slug_of c = S.to_string c.P.cel.Cel.slug + +let test_highest_band_wins () = + let r = P.resolve rules ctx ~temporal:(cand ~origin:P.Temporal ~rank:Lo "feria") + ~sanctoral:[ cand ~rank:Hi "big-feast" ] in + Alcotest.(check string) "feast wins" "big-feast" (slug_of r.P.observed) + +let test_temporal_wins_a_tie () = + let r = P.resolve rules ctx ~temporal:(cand ~origin:P.Temporal ~rank:Hi "sunday") + ~sanctoral:[ cand ~rank:Hi "saint" ] in + Alcotest.(check string) "temporal wins tie" "sunday" (slug_of r.P.observed) + +let test_loser_dispositions () = + let r = P.resolve rules ctx ~temporal:(cand ~origin:P.Temporal ~rank:Hi "sunday") + ~sanctoral:[ cand ~rank:Hi "transferable"; cand ~rank:Lo "commemorated" ] in + Alcotest.(check (list string)) "deferred" [ "transferable" ] + (List.map slug_of r.P.deferred); + Alcotest.(check (list string)) "commemorated" [ "commemorated" ] + (List.map (fun (c, _) -> slug_of c) r.P.commemorations) + +(* A commemoration-only entry can never be observed, even at a winning band. *) +let test_commemoration_only_never_observed () = + let r = P.resolve rules ctx ~temporal:(cand ~origin:P.Temporal ~rank:Lo "feria") + ~sanctoral:[ cand ~rank:Hi ~status:Cel.Commemoration_only "suppressed" ] in + Alcotest.(check string) "feria still observed" "feria" (slug_of r.P.observed); + Alcotest.(check (list string)) "suppressed commemorated" [ "suppressed" ] + (List.map (fun (c, _) -> slug_of c) r.P.commemorations) + +(* Anything the admit limit drops is recorded in `omitted`, never dropped silently. *) +let test_nothing_silently_lost () = + let r = P.resolve rules ctx ~temporal:(cand ~origin:P.Temporal ~rank:Hi "sunday") + ~sanctoral:[ cand ~rank:Lo "a"; cand ~rank:Lo "b"; cand ~rank:Lo "c" ] in + Alcotest.(check int) "two admitted" 2 (List.length r.P.commemorations); + Alcotest.(check int) "one recorded as omitted" 1 (List.length r.P.omitted); + let total = 1 + List.length r.P.commemorations + List.length r.P.deferred + + List.length r.P.omitted in + Alcotest.(check int) "every candidate accounted for" 4 total + +let suite = + ( "Precedence", + [ Alcotest.test_case "highest band wins" `Quick test_highest_band_wins; + Alcotest.test_case "temporal wins a tie" `Quick test_temporal_wins_a_tie; + Alcotest.test_case "loser dispositions" `Quick test_loser_dispositions; + Alcotest.test_case "commemoration-only never observed" `Quick + test_commemoration_only_never_observed; + Alcotest.test_case "nothing silently lost" `Quick test_nothing_silently_lost ] ) -- cgit v1.3 From 9df1aab700ce4454c26c7d0ede5b51c0f0c96c66 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Tue, 11 Aug 2026 19:30:34 +0200 Subject: kernel: the LiturgicalDay result schema Temporal is embedded rather than flattened, so season/week/weekday have one home and cannot disagree with themselves. transferred_in/out make transfers visible in the result -- an ordo must print 'transferred from the 25th', and the nothing-lost invariant reads these fields. citations exists and is empty until Plan 4; adding it later would widen a type every consumer matches on. --- lib/kernel/liturgical_day.ml | 19 +++++++++++++++++++ lib/kernel/liturgical_day.mli | 17 +++++++++++++++++ 2 files changed, 36 insertions(+) create mode 100644 lib/kernel/liturgical_day.ml create mode 100644 lib/kernel/liturgical_day.mli (limited to 'lib/kernel') diff --git a/lib/kernel/liturgical_day.ml b/lib/kernel/liturgical_day.ml new file mode 100644 index 0000000..65e3ba5 --- /dev/null +++ b/lib/kernel/liturgical_day.ml @@ -0,0 +1,19 @@ +open Sexplib0.Sexp_conv + +(* The single stable result schema (parent spec §2). *) +type ('s, 'r) t = { + date : Date.t; + rite : string; + temporal : ('s, 'r) Temporal.t; + (** embedded, not flattened: it is already a coherent unit with its own + invariants, and re-listing season/week/weekday here would create two + places for them to disagree *) + observed : 'r Celebration.t; + commemorations : ('r Celebration.t * Precedence.privilege) list; + transferred_in : 'r Celebration.t option; + (** arrived here from an impeded day *) + transferred_out : Date.t option; + (** this day's celebration went there *) + citations : Citation.t list; (** always empty until Plan 4 *) +} +[@@deriving sexp] diff --git a/lib/kernel/liturgical_day.mli b/lib/kernel/liturgical_day.mli new file mode 100644 index 0000000..3c331c3 --- /dev/null +++ b/lib/kernel/liturgical_day.mli @@ -0,0 +1,17 @@ +(** The single stable result schema (parent spec §2). *) +type ('s, 'r) t = { + date : Date.t; + rite : string; + temporal : ('s, 'r) Temporal.t; + (** embedded, not flattened: it is already a coherent unit with its own + invariants, and re-listing season/week/weekday here would create two + places for them to disagree *) + observed : 'r Celebration.t; + commemorations : ('r Celebration.t * Precedence.privilege) list; + transferred_in : 'r Celebration.t option; + (** arrived here from an impeded day *) + transferred_out : Date.t option; + (** this day's celebration went there *) + citations : Citation.t list; (** always empty until Plan 4 *) +} +[@@deriving sexp] -- cgit v1.3 From 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 ++++++++ lib/kernel/rite.mli | 18 +++++++++++ lib/kernel/validate.ml | 15 +++++++--- lib/kernel/validate.mli | 32 ++++++++++---------- test/test_validate.ml | 79 +++++++++++++++++++++++++++++++++++++++++++++---- 5 files changed, 129 insertions(+), 27 deletions(-) create mode 100644 lib/kernel/rite.ml create mode 100644 lib/kernel/rite.mli (limited to 'lib/kernel') 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; +} diff --git a/lib/kernel/rite.mli b/lib/kernel/rite.mli new file mode 100644 index 0000000..db8e86f --- /dev/null +++ b/lib/kernel/rite.mli @@ -0,0 +1,18 @@ +(** Everything a rite supplies, bundled. Passing these as loose arguments let a + caller pair one rite's vocab with another's temporal; bundling makes that + unrepresentable through the normal path. Carries functions, so it has no + sexp form. *) +type ('s, 'r) t = { + id : string; + vocab : ('s, 'r) Vocab.t; + year_start : int -> Date.t; + (** first day of the liturgical year opening in civil year y *) + temporal : Date.t -> ('s, 'r) Temporal.t; + anchors : int -> (string * Date.t) list; + (** Easter-derived days: (expected slug, date) *) + rules : ('s, 'r) Precedence.rules; + season_runs : 's list; + (** the expected run-length-compressed season sequence over one liturgical + year. NOT necessarily [vocab.seasons]: a rite may have one season + appear in two separate runs (the modern form's Ordinary Time does). *) +} diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index 7be3425..c6501a9 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -20,7 +20,11 @@ let has_duplicate strings = let rec go = function a :: (b :: _ as rest) -> a = b || go rest | _ -> false in go sorted -let run vocab ~year_start ~temporal ~anchors ~year = +let run (rite : ('s, 'r) Rite.t) ~year = + let vocab = rite.Rite.vocab in + let year_start = rite.Rite.year_start in + let temporal = rite.Rite.temporal in + let anchors = rite.Rite.anchors in let start = year_start year in let stop = (* [year_start (year + 1)] needs a date in civil year (year+1); at @@ -98,8 +102,11 @@ let run vocab ~year_start ~temporal ~anchors ~year = days; let observed = List.rev !observed in (* Season contiguity and completeness: the run-length-compressed sequence must - equal vocab.seasons exactly -- all seasons, each in one unbroken run, in - canonical order. No EF season can be empty in any year. *) + equal the rite's own [season_runs] exactly, in canonical order. This is + NOT necessarily [vocab.seasons] -- most rites have each season in one + unbroken run, but a rite may legitimately have one season appear in two + separate runs (the modern form's Ordinary Time does), so the expected + sequence is rite-supplied rather than derived from the vocabulary. *) let compressed = List.fold_left (fun acc (_, t) -> @@ -108,7 +115,7 @@ let run vocab ~year_start ~temporal ~anchors ~year = [] observed |> List.rev in - let expected = List.map vocab.Vocab.season_to_string vocab.Vocab.seasons in + let expected = List.map vocab.Vocab.season_to_string rite.Rite.season_runs in if compressed <> expected then fail start "seasons" (Printf.sprintf "season runs %s; expected %s" diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli index 709a711..d281f9a 100644 --- a/lib/kernel/validate.mli +++ b/lib/kernel/validate.mli @@ -5,26 +5,24 @@ type failure = { year : int; date : string; check : string; detail : string } val failure_to_string : failure -> string -(** [run vocab ~year_start ~temporal ~anchors ~year] returns every invariant - violation in the liturgical year opening in civil year [year]. An empty - list means the year is clean. +(** [run rite ~year] returns every invariant violation in the liturgical year + opening in civil year [year]. An empty list means the year is clean. - [anchors y] is the rite's own independent restatement of its fixed and - Easter-derived named days for civil year [y], as (expected slug, date) - pairs -- not derived from [temporal] itself, so a drift between the two - is caught rather than invisible. [run] consults both [anchors year] and - [anchors (year + 1)], since a liturgical year straddles two civil years, - and checks only the pairs whose date actually falls within the year - walked. + [rite.Rite.anchors y] is the rite's own independent restatement of its + fixed and Easter-derived named days for civil year [y], as (expected + slug, date) pairs -- not derived from [rite.Rite.temporal] itself, so a + drift between the two is caught rather than invisible. [run] consults + both [anchors year] and [anchors (year + 1)], since a liturgical year + straddles two civil years, and checks only the pairs whose date actually + falls within the year walked. + + The season check compares the run-length-compressed season sequence + against [rite.Rite.season_runs], not [rite.Rite.vocab.seasons]: a rite may + have one season appear in two separate runs (the modern form's Ordinary + Time does), so the two are not necessarily the same list. Total over the whole 1583..9999 domain, including [year] = 9999: the liturgical year opening there continues into out-of-domain civil year 10000, so the walk is clamped to 31 December 9999 and the checks run against that truncated final year rather than raising. *) -val run : - ('s, 'r) Vocab.t -> - year_start:(int -> Date.t) -> - temporal:(Date.t -> ('s, 'r) Temporal.t) -> - anchors:(int -> (string * Date.t) list) -> - year:int -> - failure list +val run : ('s, 'r) Rite.t -> year:int -> failure list diff --git a/test/test_validate.ml b/test/test_validate.ml index c19957d..31d7a3d 100644 --- a/test/test_validate.ml +++ b/test/test_validate.ml @@ -1,9 +1,23 @@ module Val = Colitur_kernel.Validate +module Rite = Colitur_kernel.Rite +module P = Colitur_kernel.Precedence module V = Rite_ef.Vocab_ef module T = Rite_ef.Temporal_ef -let run year = - Val.run V.vocab ~year_start:T.year_start ~temporal:T.temporal ~anchors:T.anchors ~year +(* 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. *) +let ef_rules : (V.season, V.rank) P.rules = + { P.band = (fun _ _ -> 0); + disposition = (fun ~winner:_ ~loser:_ -> P.Omit); + admit = (fun ~observed:_ _ -> []) } + +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 } + +let run year = Val.run ef_rite ~year let check_year year = match run year with @@ -77,6 +91,8 @@ module Synthetic = struct module Slug = Colitur_kernel.Slug module Colour = Colitur_kernel.Colour module Temporal = Colitur_kernel.Temporal + module P = Colitur_kernel.Precedence + module Rite = Colitur_kernel.Rite type season = A | B type rank = R1 | R2 @@ -105,6 +121,13 @@ module Synthetic = struct let vocab_collapsed_ranks = { vocab with Vocab.rank_to_string = (fun _ -> "same") } let vocab_collapsed_seasons = { vocab with Vocab.season_to_string = (fun _ -> "same") } + (* Precedence_ef doesn't exist yet (Tasks 7-11); Validate.run never reads + [rules], so a placeholder is enough to assemble a well-typed Rite.t. *) + let rules : (season, rank) P.rules = + { P.band = (fun _ _ -> 0); + disposition = (fun ~winner:_ ~loser:_ -> P.Omit); + admit = (fun ~observed:_ _ -> []) } + let year_start y = match D.make ~year:y ~month:1 ~day:1 with Ok d -> d | Error e -> failwith e let weekday_index d = @@ -149,10 +172,41 @@ module Synthetic = struct this synthetic rite too, not only in EF. *) let anchors _y = [ (Slug.to_string (good target).Temporal.office.Cel.slug, target) ] - let run ?(vocab = vocab) ?(anchors = fun _ -> []) temporal = - Val.run vocab ~year_start ~temporal ~anchors ~year:2026 + 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 } + + let run ?vocab ?anchors ?season_runs temporal = + Val.run (rite ?vocab ?anchors ?season_runs temporal) ~year:2026 let has_check check (fs : Val.failure list) = List.exists (fun f -> f.Val.check = check) fs + + (* A rite whose season B legitimately appears in two separate runs: the + civil year is split into calendar quarters, seasons alternating A B A B + -- as the modern form's Ordinary Time does (January-Ash Wednesday, then + Pentecost-Advent, with Lent/Easter and Advent/Christmas between). Each + quarter gets its own Sunday-aligned week origin, exactly as [good] does + for its own two runs, so every other invariant (weekday, week + numbering, rank, colour, determinism) stays clean and only the season + check is actually exercised. *) + let quarter_start y i = + match D.make ~year:y ~month:(1 + (i * 3)) ~day:1 with Ok d -> d | Error e -> failwith e + + let quarter_index d = (D.month d - 1) / 3 + + let two_run_temporal d = + let y = D.year d in + let qi = quarter_index d in + let s = if qi mod 2 = 0 then A else B in + let origin = sunday_on_or_before (quarter_start y qi) in + let n = floor_div (D.to_rata d - D.to_rata origin) 7 + 1 in + let slug = Printf.sprintf "syn2-%s-%d" (season_to_string s) (D.to_rata d) in + let rank = if D.weekday d = D.Sun then R1 else R2 in + { Temporal.season = s; week = Some n; weekday = D.weekday d; + office = Cel.make ~slug:(Slug.of_string_exn slug) ~rank ~colour:Colour.Green ~layer:"synthetic" () } + + let rite_with_two_runs : (season, rank) Rite.t = + rite ~season_runs:[ A; B; A; B ] two_run_temporal end open Synthetic @@ -160,6 +214,18 @@ open Synthetic let test_synthetic_baseline_is_clean () = Alcotest.(check bool) "clean synthetic fixture has no failures" true (run good = []) +(* The point of this task: a rite whose season B genuinely appears in two + separate runs (quarters 0,1,2,3 give season sequence A B A B, not a single + A-then-B pair) validates clean when [season_runs] says so. Before this + task, [Validate]'s season check hardcoded "compressed = vocab.seasons" + ([A; B]) with no way to say otherwise -- against that check this fixture's + compressed sequence, [A; B; A; B], would never match and every year would + report a spurious "seasons" failure. *) +let test_two_run_season_is_accepted () = + let r = Synthetic.rite_with_two_runs in + Alcotest.(check (list string)) "no failures" [] + (List.map Val.failure_to_string (Val.run r ~year:2026)) + let test_coverage_fires () = let temporal d = if D.compare d target = 0 then failwith "boom" else good d in Alcotest.(check bool) "coverage check fires when temporal raises" true @@ -170,10 +236,10 @@ let test_seasons_fires () = let t = good d in let y = D.year d in let flip_after = match D.make ~year:y ~month:9 ~day:1 with Ok d -> d | Error e -> failwith e in - (* Season A reappears after B: breaks "each season, one unbroken run". *) + (* Season A reappears after B: breaks the expected [A; B] run sequence. *) if D.compare d flip_after >= 0 then { t with Temporal.season = A } else t in - Alcotest.(check bool) "seasons check fires when a season recurs" true + Alcotest.(check bool) "seasons check fires when a season recurs outside season_runs" true (has_check "seasons" (run temporal)) let test_week_fires () = @@ -269,6 +335,7 @@ let suite = Alcotest.test_case "year 9999 does not raise" `Quick test_year_9999_does_not_raise; Alcotest.test_case "easter extremes" `Quick test_easter_extremes; Alcotest.test_case "synthetic baseline is clean" `Quick test_synthetic_baseline_is_clean; + Alcotest.test_case "two-run season is accepted" `Quick test_two_run_season_is_accepted; Alcotest.test_case "coverage fires" `Quick test_coverage_fires; Alcotest.test_case "seasons fires" `Quick test_seasons_fires; Alcotest.test_case "week fires" `Quick test_week_fires; -- cgit v1.3 From 8de560db7fb1b7b7d3ca93285068c6a4214e0bff Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Tue, 11 Aug 2026 20:01:31 +0200 Subject: kernel(calendar): the year is the primitive, the day is derived Transfers make per-date resolution impossible to do correctly: resolving 25 March can push a feast onto 26 March, and RG 97-98 has coinciding I-class feasts transfer in table order, which needs global knowledge. So year computes a whole liturgical year in one pass and day indexes into it. Pure, no cache, no mutable state. This commit resolves each day but does not yet place deferred transfers; they are recorded with a reason. Task 6 adds the placement pass. --- lib/kernel/calendar.ml | 93 ++++++++++++++++++++++++++ lib/kernel/calendar.mli | 45 +++++++++++++ test/test_calendar.ml | 172 ++++++++++++++++++++++++++++++++++++++++++++++++ test/test_colitur.ml | 3 +- 4 files changed, 312 insertions(+), 1 deletion(-) create mode 100644 lib/kernel/calendar.ml create mode 100644 lib/kernel/calendar.mli create mode 100644 test/test_calendar.ml (limited to 'lib/kernel') diff --git a/lib/kernel/calendar.ml b/lib/kernel/calendar.ml new file mode 100644 index 0000000..fd23377 --- /dev/null +++ b/lib/kernel/calendar.ml @@ -0,0 +1,93 @@ +(* Resolution across a whole liturgical year. See calendar.mli for the + architectural rationale (why [year] is the primitive and [day] derived). *) + +(* The kernel's domain floor and ceiling (Date.make's documented 1583..9999 + bound). Both are always constructible -- in-range by definition -- so + neither of these can itself raise. *) +let domain_min_date = + match Date.make ~year:1583 ~month:1 ~day:1 with Ok d -> d | Error e -> failwith e + +let domain_max_date = + match Date.make ~year:9999 ~month:12 ~day:31 with Ok d -> d | Error e -> failwith e + +(* [start, stop] for the liturgical year opening in civil year [y], clamped at + both ends of the domain rather than calling [rite.year_start] on a civil + year outside 1583..9999. + + Top: at [y] = 9999, [rite.year_start (y + 1)] would ask for civil year + 10000 -- out of Date's domain (Plan 2 shipped exactly this bug in + Validate). Clamp [stop] to 31 December 9999 instead: the final liturgical + year comes back truncated, not un-computable. + + Bottom: symmetric case, reachable only through [day] below. A date in + civil year 1583 before that year's own [rite.year_start] genuinely belongs + to the liturgical year that opened in civil year 1582 for an + Advent-anchored rite -- but [rite.year_start 1582] is equally out of + domain. [day] only ever decrements a valid date's own (in-domain) civil + year by at most one, so [y] = 1582 is the sole way this branch is reached. + Clamp [start] to 1 January 1583: "year 1582" becomes the truncated + stretch from the domain floor up to the day before [rite.year_start 1583], + which is exactly the sliver a date there needs. *) +let year_bounds (rite : ('s, 'r) Rite.t) (y : int) : Date.t * Date.t = + let start = if y < 1583 then domain_min_date else rite.Rite.year_start y in + let stop = + if y >= 9999 then domain_max_date else Date.add_days (rite.Rite.year_start (y + 1)) (-1) + in + (start, stop) + +(* RG 91's contest for one date: the temporal office against every sanctoral + entry whose Date_spec resolves to it. [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 = + let temporal = rite.Rite.temporal date in + let temporal_candidate = + { Precedence.cel = temporal.Temporal.office; origin = Precedence.Temporal } + in + let sanctoral = + 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 ctx = { Precedence.date; season = temporal.Temporal.season; weekday = temporal.Temporal.weekday } in + let resolution = Precedence.resolve rite.Rite.rules ctx ~temporal:temporal_candidate ~sanctoral in + (* [resolution.deferred] (RG 96-98 transfer candidates) and + [resolution.omitted] (yielded/admission-limit losers) have no field to + land in on Liturgical_day.t yet, so both are simply absent from today's + result -- deliberately incomplete for a deferred candidate, which is + thereby neither observed nor commemorated here, and not yet placed on + any later day either ("deferred: transfer placement not yet implemented + (Task 6)"). Task 6's fixed-point pass closes this gap. *) + { + Liturgical_day.date; + rite = rite.Rite.id; + temporal; + observed = resolution.Precedence.observed.Precedence.cel; + commemorations = + List.map (fun (c, p) -> (c.Precedence.cel, p)) resolution.Precedence.commemorations; + transferred_in = None; + transferred_out = None; + citations = []; + } + +let year (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) (y : int) : + ('s, 'r) Liturgical_day.t array = + let idx = Layer.index_by_date layer in + let start, stop = year_bounds rite y in + (* [max 0]: defends [Array.init] against a negative length, which would + otherwise arise for a rite whose [year_start] lands exactly on the + domain floor (start clamps to the same date, giving [stop] a day + before it). Not reachable through [day] -- see calendar.mli -- but + [year] is public, and a direct out-of-contract call must not raise + either. *) + let n = max 0 (Date.to_rata stop - Date.to_rata start + 1) in + Array.init n (fun i -> resolve_day rite idx (Date.add_days start i)) + +let day (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) (date : Date.t) : + ('s, 'r) Liturgical_day.t = + let cy = Date.year date in + let y = if Date.compare date (rite.Rite.year_start cy) >= 0 then cy else cy - 1 in + let start, _ = year_bounds rite y in + (year rite layer y).(Date.to_rata date - Date.to_rata start) diff --git a/lib/kernel/calendar.mli b/lib/kernel/calendar.mli new file mode 100644 index 0000000..50ff8f8 --- /dev/null +++ b/lib/kernel/calendar.mli @@ -0,0 +1,45 @@ +(** Resolution across a whole liturgical year (spec §2.4). + + Transfers make per-date resolution impossible to do correctly: resolving + 25 March can push a feast onto 26 March, and RG 97-98 has coinciding + I-class feasts transfer in table order, which needs global knowledge of + the whole year. So [year] is the primitive -- it resolves every date in + one pass -- and [day] is derived: it finds the liturgical year containing + a date and indexes into it. Both are pure; neither caches. + + This module resolves each day's temporal-vs-sanctoral contest but does + not yet place deferred transfers (RG 96-98): a losing candidate the + rite's rules send to [Precedence.Transfer] is absent from the result + entirely on this pass -- not observed, not commemorated, and + [transferred_in]/[transferred_out] both stay [None] everywhere. Task 6 + adds the fixed-point placement pass that closes this gap. *) + +(** [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: + - At [y] = 9999, [rite.year_start (y + 1)] would ask for civil year + 10000, out of {!Date}'s domain (this is the bug Plan 2 shipped in + [Validate] and later fixed). The end of the walk clamps to 31 December + 9999 instead of computing that call; the returned year comes back + truncated to whatever the rite's own temporal cycle covers between + [rite.year_start 9999] and the last day of that civil year, not + un-computable. + - Symmetrically, [y] < 1583 clamps the start of the walk to 1 January + 1583 instead of calling [rite.year_start y] on an out-of-domain civil + year. [year] is never called this way directly by anything in this + module; {!day} is the only caller that can reach [y] = 1582 (one below + the floor, never lower), when the date it was asked about sits in civil + year 1583 before that year's own [rite.year_start] -- i.e. the sliver + whose true liturgical year opened in civil year 1582, which the domain + cannot represent. Calling [year] with such a [y] directly is also safe: + it returns exactly that truncated sliver. *) +val year : ('s, 'r) Rite.t -> 'r Layer.t -> int -> ('s, 'r) Liturgical_day.t array + +(** [day rite layer date] finds the liturgical year containing [date] -- the + year [y] with [rite.year_start y <= date < rite.year_start (y + 1)] -- + and returns its slot for [date]. Recomputes that whole year on every + call: pure, no cache, no mutable state. Acceptable cost for the natural + usage (dump a year, sweep years for validation), which pays it once. *) +val day : ('s, 'r) Rite.t -> 'r Layer.t -> Date.t -> ('s, 'r) Liturgical_day.t diff --git a/test/test_calendar.ml b/test/test_calendar.ml new file mode 100644 index 0000000..a3c4125 --- /dev/null +++ b/test/test_calendar.ml @@ -0,0 +1,172 @@ +module C = Colitur_kernel.Calendar +module D = Colitur_kernel.Date +module LD = Colitur_kernel.Liturgical_day +module Cel = Colitur_kernel.Celebration +module Sl = Colitur_kernel.Slug +module Rite = Colitur_kernel.Rite + +let mk y m d = match D.make ~year:y ~month:m ~day:d with Ok t -> t | Error e -> failwith 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. *) +module Fixture = struct + module Vocab = Colitur_kernel.Vocab + module Colour = Colitur_kernel.Colour + module Temporal = Colitur_kernel.Temporal + module P = Colitur_kernel.Precedence + module Layer = Colitur_kernel.Layer + module Date_spec = Colitur_kernel.Date_spec + + type season = A | B + type rank = Hi | 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 vocab : (season, rank) Vocab.t = + { Vocab.seasons = [ A; B ]; season_to_string; season_of_string; + ranks = [ Hi; Lo ]; rank_to_string; rank_of_string } + + let weekday_index d = + match D.weekday d with + | D.Sun -> 0 | D.Mon -> 1 | D.Tue -> 2 | D.Wed -> 3 + | D.Thu -> 4 | D.Fri -> 5 | D.Sat -> 6 + + let sunday_on_or_before d = D.add_days d (-(weekday_index d)) + + (* Advent-anchored, mirroring the real EF rite's own RG-71 "Sunday nearest + 30 November" rule (rite_ef/temporal_ef.ml's [advent_start]) rather than + a Jan-1 year start: that shape is what makes the year-below-the-date's- + own-civil-year case in [Calendar.day] genuinely reachable, so the domain + -floor test below exercises something real. *) + let year_start y = D.add_days (sunday_on_or_before (mk y 12 24)) (-21) + + (* Not liturgically meaningful -- Calendar does not check season + contiguity (that is Validate's job); this just proves the season type + parameter is actually threaded through. *) + let season date = if D.month date < 6 then A else B + + (* One office per day, uniquely named by date so distinct days never + collide on slug. *) + let office date = + let slug = Printf.sprintf "feria-%04d-%02d-%02d" (D.year date) (D.month date) (D.day date) in + Cel.make ~slug:(Sl.of_string_exn slug) ~rank:Lo ~colour:Colour.Green ~layer:"synthetic-temporal" () + + 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. *) + let band (_ : season P.context) (c : rank P.candidate) = + (match c.P.cel.Cel.rank with Hi -> 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 + + let rules : (season, rank) P.rules = { P.band; disposition; admit = (fun ~observed:_ cs -> cs) } + + let rite : (season, rank) Rite.t = + { Rite.id = "synthetic-calendar"; vocab; year_start; temporal; anchors = (fun _ -> []); + rules; season_runs = [ A; B ] } + + let entry ~month ~day ~slug ~rank = + { Layer.date = (match Date_spec.fixed ~month ~day with Ok d -> d | Error e -> failwith e); + 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 commem_worthy = entry ~month:12 ~day:15 ~slug:"commem-worthy" ~rank:Lo + + let layer = Layer.of_entries ~id:"synthetic" ~name:"Synthetic sanctoral" [ big_feast; commem_worthy ] + + let liturgical_year_of date = + let cy = D.year date in + if D.compare date (year_start cy) >= 0 then cy else cy - 1 +end + +let test_year_covers_every_day () = + let days = C.year Fixture.rite Fixture.layer 2026 in + let first = days.(0) and last = days.(Array.length days - 1) in + Alcotest.(check string) "starts at year_start" "2026-11-29" (D.to_iso8601 first.LD.date); + Alcotest.(check bool) "ends the day before next year_start" true + (D.compare last.LD.date (D.add_days (Fixture.rite.Rite.year_start 2027) (-1)) = 0); + (* every consecutive pair is exactly one day apart: no gaps, no duplicates *) + Array.iteri + (fun i d -> + if i > 0 then + Alcotest.(check int) "consecutive" 1 + (D.to_rata d.LD.date - D.to_rata days.(i - 1).LD.date)) + days + +let test_day_agrees_with_year () = + List.iter + (fun (y, m, dd) -> + let date = mk y m dd in + let from_day = C.day Fixture.rite Fixture.layer date in + let ys = C.year Fixture.rite Fixture.layer (Fixture.liturgical_year_of date) in + let from_year = Array.to_list ys |> List.find (fun d -> D.compare d.LD.date date = 0) in + Alcotest.(check string) "same observed" + (Sl.to_string from_year.LD.observed.Cel.slug) + (Sl.to_string from_day.LD.observed.Cel.slug)) + [ (2026, 12, 1); (2027, 3, 15); (2027, 7, 4) ] + +(* Two entries in the layer, per the brief: one that outranks the feria and + one that does not. Both sit on their own date so each assertion below + pins one behaviour without the other candidate muddying it. *) +let test_sanctoral_outranks_feria_becomes_observed () = + let days = C.year Fixture.rite Fixture.layer 2026 in + let date = mk 2026 12 8 in + let d = Array.to_list days |> List.find (fun d -> D.compare d.LD.date date = 0) in + Alcotest.(check string) "big-feast observed" "big-feast" (Sl.to_string d.LD.observed.Cel.slug) + +let test_lower_ranked_sanctoral_is_commemorated () = + let days = C.year Fixture.rite Fixture.layer 2026 in + let date = mk 2026 12 15 in + let d = Array.to_list days |> List.find (fun d -> D.compare d.LD.date date = 0) in + let expected_feria = Sl.to_string (Fixture.office date).Cel.slug in + Alcotest.(check string) "feria still observed" expected_feria (Sl.to_string d.LD.observed.Cel.slug); + Alcotest.(check (list string)) "commem-worthy commemorated" [ "commem-worthy" ] + (List.map (fun (c, _) -> Sl.to_string c.Cel.slug) d.LD.commemorations) + +(* Register/design lesson (Plan 2's Validate 9999 bug): [year_start (y + 1)] + at the top of the domain must not raise. Calling [C.year ... 9999] here + directly (no [try]) is itself part of the pin -- if the clamp regressed, + this call would raise and the test would error rather than fail cleanly. *) +let test_year_9999_does_not_raise () = + let days = C.year Fixture.rite Fixture.layer 9999 in + Alcotest.(check bool) "non-empty" true (Array.length days > 0); + Alcotest.(check string) "starts at year_start 9999" + (D.to_iso8601 (Fixture.rite.Rite.year_start 9999)) + (D.to_iso8601 days.(0).LD.date); + Alcotest.(check string) "ends at the domain ceiling" "9999-12-31" + (D.to_iso8601 days.(Array.length days - 1).LD.date) + +(* The symmetric case at the bottom: 1 January 1583 is the domain's earliest + representable date, and Fixture's Advent-anchored [year_start] puts it + well before that civil year's own year_start -- so [day] must resolve it + via the [y] = 1582 branch without calling [year_start 1582] (out of + domain). Checks identity (the date's own feria), not merely that + something came back. *) +let test_day_near_domain_floor_does_not_raise () = + let date = mk 1583 1 1 in + let d = C.day Fixture.rite Fixture.layer date in + Alcotest.(check string) "returns the queried date" "1583-01-01" (D.to_iso8601 d.LD.date); + Alcotest.(check string) "observed is the day's own feria" + (Sl.to_string (Fixture.office date).Cel.slug) (Sl.to_string d.LD.observed.Cel.slug) + +let suite = + ( "Calendar", + [ Alcotest.test_case "year covers every day" `Quick test_year_covers_every_day; + Alcotest.test_case "day agrees with year" `Quick test_day_agrees_with_year; + Alcotest.test_case "outranking sanctoral becomes observed" `Quick + test_sanctoral_outranks_feria_becomes_observed; + Alcotest.test_case "lower-ranked sanctoral is commemorated" `Quick + test_lower_ranked_sanctoral_is_commemorated; + Alcotest.test_case "year 9999 does not raise" `Quick test_year_9999_does_not_raise; + Alcotest.test_case "day near the domain floor does not raise" `Quick + test_day_near_domain_floor_does_not_raise ] ) diff --git a/test/test_colitur.ml b/test/test_colitur.ml index 08282e6..a97e35c 100644 --- a/test/test_colitur.ml +++ b/test/test_colitur.ml @@ -2,4 +2,5 @@ let () = Alcotest.run "colitur" [ Test_date.suite; Test_computus.suite; Test_colour.suite; Test_slug.suite; Test_names.suite; - Test_overlay.suite; Test_temporal_ef.suite; Test_validate.suite; Test_precedence.suite ] + Test_overlay.suite; Test_temporal_ef.suite; Test_validate.suite; Test_precedence.suite; + Test_calendar.suite ] -- cgit v1.3 From 953427d8d1e3a34994be53b60e18662ec26fef4e Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Tue, 11 Aug 2026 20:07:55 +0200 Subject: kernel: carry omitted celebrations on Liturgical_day.t, reason and all Precedence.resolution already tracked what happened to every losing candidate -- commemorated, deferred, or omitted with a reason -- but Liturgical_day.t had nowhere for the deferred and omitted buckets to land, so Calendar dropped them at the door. Task 12's no-celebration-lost invariant needs to read that accounting off the day result itself, not re-resolve every day to reconstruct it, so a reason recorded nowhere is not recorded. Add Liturgical_day.omitted : ('r Celebration.t * string) list, after transferred_out and before citations. Calendar.resolve_day now folds resolution.omitted (Precedence's own native omissions, reasons intact) and resolution.deferred (mapped to "deferred: transfer placement not yet implemented (Task 6)") into it. Adds a full-day accounting test against the whole Calendar pipeline: four colliding sanctoral entries plus the day's feria, checked as a slug set (matching test_precedence.ml's own nothing-silently-lost test) so a candidate silently dropped or duplicated into two buckets would fail it, plus an identity check that the deferred and admission-limit reasons don't get swapped. --- lib/kernel/calendar.ml | 21 ++++++++++----- lib/kernel/calendar.mli | 13 ++++++--- lib/kernel/liturgical_day.ml | 3 +++ lib/kernel/liturgical_day.mli | 3 +++ test/test_calendar.ml | 63 ++++++++++++++++++++++++++++++++++++++++--- 5 files changed, 89 insertions(+), 14 deletions(-) (limited to 'lib/kernel') diff --git a/lib/kernel/calendar.ml b/lib/kernel/calendar.ml index fd23377..1cdd1fa 100644 --- a/lib/kernel/calendar.ml +++ b/lib/kernel/calendar.ml @@ -35,6 +35,15 @@ let year_bounds (rite : ('s, 'r) Rite.t) (y : int) : Date.t * Date.t = in (start, stop) +(* [resolution.deferred] (RG 96-98 transfer candidates) has nowhere to be + PLACED yet -- Task 6 adds the fixed-point pass that does -- but it must + still be accounted for on the day it lost, not silently dropped: Task + 12's no-celebration-lost invariant reads [Liturgical_day.omitted], so a + deferred candidate folds in there too, with its own reason distinct from + Precedence's native omissions ("omitted: yielded to a higher day", + "omitted: admission limit reached"). *) +let deferred_reason = "deferred: transfer placement not yet implemented (Task 6)" + (* RG 91's contest for one date: the temporal office against every sanctoral entry whose Date_spec resolves to it. [Layer.on_date] is keyed on exactly (month, day), which for a [Fixed] spec -- the only form Plan 2 ships -- is @@ -53,13 +62,10 @@ let resolve_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) (date : Date.t in let ctx = { Precedence.date; season = temporal.Temporal.season; weekday = temporal.Temporal.weekday } in let resolution = Precedence.resolve rite.Rite.rules ctx ~temporal:temporal_candidate ~sanctoral in - (* [resolution.deferred] (RG 96-98 transfer candidates) and - [resolution.omitted] (yielded/admission-limit losers) have no field to - land in on Liturgical_day.t yet, so both are simply absent from today's - result -- deliberately incomplete for a deferred candidate, which is - thereby neither observed nor commemorated here, and not yet placed on - any later day either ("deferred: transfer placement not yet implemented - (Task 6)"). Task 6's fixed-point pass closes this gap. *) + let omitted = + List.map (fun (c, reason) -> (c.Precedence.cel, reason)) resolution.Precedence.omitted + @ List.map (fun c -> (c.Precedence.cel, deferred_reason)) resolution.Precedence.deferred + in { Liturgical_day.date; rite = rite.Rite.id; @@ -69,6 +75,7 @@ let resolve_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) (date : Date.t List.map (fun (c, p) -> (c.Precedence.cel, p)) resolution.Precedence.commemorations; transferred_in = None; transferred_out = None; + omitted; citations = []; } diff --git a/lib/kernel/calendar.mli b/lib/kernel/calendar.mli index 50ff8f8..2469f2a 100644 --- a/lib/kernel/calendar.mli +++ b/lib/kernel/calendar.mli @@ -9,10 +9,15 @@ This module resolves each day's temporal-vs-sanctoral contest but does not yet place deferred transfers (RG 96-98): a losing candidate the - rite's rules send to [Precedence.Transfer] is absent from the result - entirely on this pass -- not observed, not commemorated, and - [transferred_in]/[transferred_out] both stay [None] everywhere. Task 6 - adds the fixed-point placement pass that closes this gap. *) + rite's rules send to [Precedence.Transfer] is not observed and not + commemorated on the day it lost, and [transferred_in]/[transferred_out] + both stay [None] everywhere -- but it is not silently dropped either. It + lands in that day's [Liturgical_day.omitted] with the reason ["deferred: + transfer placement not yet implemented (Task 6)"], alongside + [Precedence]'s own native omissions (yielded to a higher day; admission + limit reached), each with its own reason. Task 6 adds the fixed-point + placement pass that actually places these; until then, this is the + day's complete, honest accounting of what happened to every candidate. *) (** [year rite layer y] resolves every day of the liturgical year that opens in civil year [y]: from [rite.year_start y] through the day before diff --git a/lib/kernel/liturgical_day.ml b/lib/kernel/liturgical_day.ml index 65e3ba5..cbaca9c 100644 --- a/lib/kernel/liturgical_day.ml +++ b/lib/kernel/liturgical_day.ml @@ -14,6 +14,9 @@ type ('s, 'r) t = { (** arrived here from an impeded day *) transferred_out : Date.t option; (** this day's celebration went there *) + omitted : ('r Celebration.t * string) list; + (** with the reason, never silent -- Task 12's no-celebration-lost + invariant reads this *) citations : Citation.t list; (** always empty until Plan 4 *) } [@@deriving sexp] diff --git a/lib/kernel/liturgical_day.mli b/lib/kernel/liturgical_day.mli index 3c331c3..38e7c76 100644 --- a/lib/kernel/liturgical_day.mli +++ b/lib/kernel/liturgical_day.mli @@ -12,6 +12,9 @@ type ('s, 'r) t = { (** arrived here from an impeded day *) transferred_out : Date.t option; (** this day's celebration went there *) + omitted : ('r Celebration.t * string) list; + (** with the reason, never silent -- Task 12's no-celebration-lost + invariant reads this *) citations : Citation.t list; (** always empty until Plan 4 *) } [@@deriving sexp] diff --git a/test/test_calendar.ml b/test/test_calendar.ml index a3c4125..d34611a 100644 --- a/test/test_calendar.ml +++ b/test/test_calendar.ml @@ -68,7 +68,12 @@ module Fixture = struct let disposition ~winner:_ ~(loser : rank P.candidate) = match loser.P.cel.Cel.rank with Lo -> P.Commemorate P.Ordinary | Hi -> P.Transfer - let rules : (season, rank) P.rules = { P.band; disposition; admit = (fun ~observed:_ cs -> cs) } + (* Admits at most one commemoration -- mirrors test_precedence.ml's own + example and, unlike "admit everything", actually gives the accounting + test below a genuine Precedence-native omission (distinct from a + deferred one) to exercise. *) + let rules : (season, rank) P.rules = + { P.band; disposition; admit = (fun ~observed:_ cs -> List.filteri (fun i _ -> i < 1) cs) } let rite : (season, rank) Rite.t = { Rite.id = "synthetic-calendar"; vocab; year_start; temporal; anchors = (fun _ -> []); @@ -82,7 +87,23 @@ module Fixture = struct let big_feast = entry ~month:12 ~day:8 ~slug:"big-feast" ~rank:Hi let commem_worthy = entry ~month:12 ~day:15 ~slug:"commem-worthy" ~rank:Lo - let layer = Layer.of_entries ~id:"synthetic" ~name:"Synthetic sanctoral" [ big_feast; commem_worthy ] + (* 20 Dec: four sanctoral entries on one date, for the full-accounting test. + "day-winner" and "eclipsed" tie on band (both Hi, both Sanctoral); ties + break on slug, so "day-winner" wins and "eclipsed" -- a Hi-rank loser -- + is [Transfer]-disposed, landing in [deferred]. "loser-a" and "loser-b" + are both Lo, both [Commemorate]-disposed, but [admit] only keeps one: + the other lands in Precedence's own [omitted] ("admission limit + reached"), distinct from "eclipsed"'s deferred reason. Four candidates, + three different fates -- observed, one specific omission reason, two + more. *) + let day_winner = entry ~month:12 ~day:20 ~slug:"day-winner" ~rank:Hi + let eclipsed = entry ~month:12 ~day:20 ~slug:"eclipsed" ~rank:Hi + let loser_a = entry ~month:12 ~day:20 ~slug:"loser-a" ~rank:Lo + let loser_b = entry ~month:12 ~day:20 ~slug:"loser-b" ~rank:Lo + + let layer = + Layer.of_entries ~id:"synthetic" ~name:"Synthetic sanctoral" + [ big_feast; commem_worthy; day_winner; eclipsed; loser_a; loser_b ] let liturgical_year_of date = let cy = D.year date in @@ -159,6 +180,41 @@ let test_day_near_domain_floor_does_not_raise () = Alcotest.(check string) "observed is the day's own feria" (Sl.to_string (Fixture.office date).Cel.slug) (Sl.to_string d.LD.observed.Cel.slug) +(* Full-day accounting through the whole Calendar pipeline (Layer -> Calendar + -> Liturgical_day), not just Precedence in isolation: every candidate fed + in for 20 Dec 2026 -- the feria plus Fixture's four colliding sanctoral + entries -- appears exactly once across observed/commemorations/omitted. + Checked as a slug SET (Alcotest.slist), matching test_precedence.ml's own + "nothing silently lost" test: a length-only check would pass even if one + slug were duplicated into two buckets and another dropped, which this + project has shipped before (register finding). *) +let test_full_day_accounting () = + let date = mk 2026 12 20 in + let d = C.day Fixture.rite Fixture.layer date in + let feria_slug = Sl.to_string (Fixture.office date).Cel.slug in + let bucketed = + (Sl.to_string d.LD.observed.Cel.slug + :: List.map (fun (c, _) -> Sl.to_string c.Cel.slug) d.LD.commemorations) + @ List.map (fun (c, _) -> Sl.to_string c.Cel.slug) d.LD.omitted + in + Alcotest.(check (slist string compare)) "every candidate appears exactly once" + [ feria_slug; "day-winner"; "eclipsed"; "loser-a"; "loser-b" ] + bucketed; + (* Identity within [omitted], not just membership: "eclipsed" (a deferred + transfer candidate, RG 96-98) must carry the deferred reason, not + Precedence's native "admission limit reached" that "loser-a"/"loser-b" + -- the ones Precedence itself dropped -- carry. Without this, a bug + that folded [resolution.deferred] into [omitted] with the wrong reason, + or dropped [resolution.omitted]'s own reasons, would still pass the + slug-set check above. *) + let reason_of slug = + d.LD.omitted |> List.find (fun (c, _) -> Sl.to_string c.Cel.slug = slug) |> snd + in + Alcotest.(check string) "eclipsed carries the deferred reason" + "deferred: transfer placement not yet implemented (Task 6)" (reason_of "eclipsed"); + Alcotest.(check string) "loser-a carries Precedence's own admission-limit reason" + "omitted: admission limit reached" (reason_of "loser-a") + let suite = ( "Calendar", [ Alcotest.test_case "year covers every day" `Quick test_year_covers_every_day; @@ -169,4 +225,5 @@ let suite = test_lower_ranked_sanctoral_is_commemorated; Alcotest.test_case "year 9999 does not raise" `Quick test_year_9999_does_not_raise; Alcotest.test_case "day near the domain floor does not raise" `Quick - test_day_near_domain_floor_does_not_raise ] ) + test_day_near_domain_floor_does_not_raise; + Alcotest.test_case "full day accounting" `Quick test_full_day_accounting ] ) -- cgit v1.3 From 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') 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 From 1d6be4ac281e62accfb905b137b3c6b494183ee4 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Tue, 11 Aug 2026 21:29:13 +0200 Subject: kernel(calendar): fix multi-departure loss, band-order gap, off-array targets Four findings from Task 6 review, addressed on top of f15e44d. 1. transferred_out was a single Date.t option, so when RG 97-98 collides three or more feasts on one date (more than one loser), only the last one Hashtbl.iter happened to visit survived -- a genuinely lost move, and which one survived depended on OCaml's hash seed (OCAMLRUNPARAM=R), an environment read a kernel invariant forbids. RG 97-98 says coinciding feasts transfer "in order" -- plural -- so the type was wrong, not the fixture: transferred_out is now (Celebration.t * Date.t) list. transferred_in stays a single option, deliberately: a day receives at most one arrival (RG 96 sends each departure to the next non-I/II-class day, and the first to arrive occupies it). The per-day list is canonicalised (sorted by target date, then slug) after accumulation, the same fix layer.ml already applies to its own date-bucket index and for the same reason. Verified clean across 15 runs under OCAMLRUNPARAM=R; disabling the canonicalisation step showed the raw order genuinely flip between seeds, confirming the fix is load-bearing. 2. Every deferred candidate in the fixture was the same rank, so compare_deferred's band branch was unreachable and reversing it broke nothing -- the RG 97-98 test was pinning slug order, not band order. The fixture now has three ranks (Hi1 outranks Hi2, both transfer, both outrank Lo), with slugs chosen so band order and slug order disagree. Reversing the band comparison now fails the test on "higher-band loser claims 2 Feb first", received the wrong slug instead. 3. A transfer_target free to name any date could place a candidate outside the liturgical year's own start/stop bounds: invisible to year/build_day, so it would be observed nowhere and, since its origin's re-resolution would report it as settled, omitted nowhere either -- genuinely gone, contradicting calendar.mli's "never silently dropped". place_transfers now checks the range on every placement and routes an out-of-range one to a permanent-exclusion table instead of assignment, with its own cited omitted reason. 4. Precedence.resolve folds Transfer and Repose into one deferred case, and place_transfers routed all of it through transfer_target (RG 96's search), which is only correct for Transfer. Repose is RG 100-102's repositio, a distinct rubric this module does not implement. Documented rather than split into a second mechanism: nothing in the EF ruleset returns Repose (design spec section 1.3, "declared, not exercised"), so the gap is latent, not a live bug. Two new tests (origin records every departure; transfer target outside year is recorded not lost); the RG 97-98 test's fixture and assertions rewritten for finding 2. --- lib/kernel/calendar.ml | 157 +++++++++++++++++++++++-------- lib/kernel/calendar.mli | 31 +++++-- lib/kernel/liturgical_day.ml | 9 +- lib/kernel/liturgical_day.mli | 9 +- test/test_calendar.ml | 211 ++++++++++++++++++++++++++++-------------- 5 files changed, 298 insertions(+), 119 deletions(-) (limited to 'lib/kernel') diff --git a/lib/kernel/calendar.ml b/lib/kernel/calendar.ml index 1ad45a1..5d3572c 100644 --- a/lib/kernel/calendar.ml +++ b/lib/kernel/calendar.ml @@ -101,6 +101,20 @@ let max_transfer_rounds = 64 let unconverged_reason = "omitted: transfer placement did not converge within max_transfer_rounds (RG 96-98)" +(* A rite-supplied [transfer_target] is trusted to search strictly forward + (rite.mli), but nothing stops it naming a date past the end of the + liturgical year it was asked about -- e.g. an I-class feast impeded in + the last days before Advent I, whose first admissible day genuinely + falls in the following liturgical year's own territory (unproven to + occur in the real EF calendar, but not something this module can rule + out by construction). [place_transfers] never injects such a target: the + [dates] array is exactly what [year]/[build_day] walk to produce the + result, so a candidate placed outside it would be [observed]/ + [transferred_in] nowhere in the output at all -- gone, not merely + mis-filed, and silently so, contradicting [calendar.mli]'s "never + silently dropped". This reason makes that failure mode visible instead. *) +let out_of_range_reason = "omitted: transfer target falls outside the liturgical year (RG 96)" + (* Rebuilds the per-date injection index from [assignment] (slug -> (origin, target)) fresh each round, rather than accumulating it incrementally as candidates are placed. A candidate re-deferred in a later round (its first @@ -125,6 +139,22 @@ let injected_index_of_assignment (assignment : (string, Date.t * Date.t) Hashtbl (* The placement pass itself (spec §2.4 steps 1-4; step 5, recording transferred_in/out, is [year]'s job once this reaches a fixed point). + Every [Precedence.Transfer]-*and*-[Precedence.Repose]-disposed loser lands + in [resolution.deferred] together -- [Precedence.resolve]'s own fold + matches them as one case, [Transfer | Repose -> ... :: defs ...] -- and + everything gathered below is routed through + [rite.transfer_target], i.e. RG 96's next-admissible-day search. That is + only correct for [Transfer]. [Repose] denotes RG 100-102's *repositio* + (perpetual impediment, reassigned to the next appropriate day and treated + as proper) -- a distinct rubric this module does not implement. It is + documented here rather than split into a second mechanism because nothing + currently produces [Repose]: the design spec records it as "declared, not + exercised" (§1.3) -- the EF ruleset (Tasks 7-9) returns it for nothing; + perpetual impediment arises from proper/diocesan calendars, which are + overlay content, out of this plan's scope. If a future rite's rules ever + do return [Repose], it would silently take the RG 96 path here, which + would be wrong -- worth knowing before that day, not discovering it then. + Each round: gather every currently-deferred candidate across the whole year (fresh, against this round's [injected] state -- a candidate already placed and now winning its target is no longer a loser anywhere and so @@ -148,11 +178,21 @@ let injected_index_of_assignment (assignment : (string, Date.t * Date.t) Hashtbl module's, not because this module's sort ever decided anything. Layering the claims instead means a same-round collision is resolved in the one round it is found, in the sorted order, and the earlier RG 97-98 test - pins exactly that: it fails on "claims 2 Feb first" without this. *) -let place_transfers (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) (dates : Date.t array) : - (string, Date.t * Date.t) Hashtbl.t * (string, 'r Precedence.candidate) Hashtbl.t = + pins exactly that: it fails on "claims 2 Feb first" without this. + + [~start ~stop] bound the [transfer_target] a placement is allowed to + settle on: outside that range it goes into [out_of_range] instead of + [assignment], permanently (never retried -- [transfer_target] is a pure + function of a candidate's own permanent origin and the occupancy state, + so asking it again would only recompute the same out-of-range answer). *) +let place_transfers (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) ~(start : Date.t) + ~(stop : Date.t) (dates : Date.t array) : + (string, Date.t * Date.t) Hashtbl.t + * (string, 'r Precedence.candidate) Hashtbl.t + * (string, Date.t * Date.t) Hashtbl.t = let assignment : (string, Date.t * Date.t) Hashtbl.t = Hashtbl.create 16 in let candidate_by_slug : (string, 'r Precedence.candidate) Hashtbl.t = Hashtbl.create 16 in + let out_of_range : (string, Date.t * Date.t) Hashtbl.t = Hashtbl.create 4 in let compare_deferred (_, ctx1, c1) (_, ctx2, c2) = let b1 = rite.Rite.rules.Precedence.band ctx1 c1 in let b2 = rite.Rite.rules.Precedence.band ctx2 c2 in @@ -185,16 +225,22 @@ let place_transfers (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) (dates : D Jan instead of 13 in test_transfer_moves_and_does_not_duplicate, not merely "doesn't converge" -- the bug is a wrong answer, not only a hang). A sighting is genuinely actionable only if the - candidate has never been placed yet (first time seen), or if it is - losing exactly at the date it is *currently* assigned to (a fresh - RG 97-98 bump: something else also landed there and out-ranked it) - -- any other date is the stale, permanent one and is dropped. *) + candidate has never been placed yet (first time seen, and not + already known unplaceable -- [out_of_range] gets the same + permanent exclusion [assignment] does, for the same reason), or if + it is losing exactly at the date it is *currently* assigned to (a + fresh RG 97-98 bump: something else also landed there and + out-ranked it) -- any other date is the stale, permanent one and is + dropped. *) let deferred = List.filter (fun (date, _ctx, c) -> - match Hashtbl.find_opt assignment (Slug.to_string c.Precedence.cel.Celebration.slug) with - | None -> true - | Some (_, target) -> Date.compare date target = 0) + let slug = Slug.to_string c.Precedence.cel.Celebration.slug in + if Hashtbl.mem out_of_range slug then false + else + match Hashtbl.find_opt assignment slug with + | None -> true + | Some (_, target) -> Date.compare date target = 0) raw in if deferred = [] then converged := true @@ -209,31 +255,30 @@ let place_transfers (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) (dates : D |> List.iter (fun (origin, _ctx, c) -> let target = rite.Rite.transfer_target c origin occupant_with_claims in let slug = Slug.to_string c.Precedence.cel.Celebration.slug in - Hashtbl.replace claimed_this_round (Date.to_rata target) c; - Hashtbl.replace assignment slug (origin, target); - Hashtbl.replace candidate_by_slug slug c) + if Date.compare target start < 0 || Date.compare target stop > 0 then + Hashtbl.replace out_of_range slug (origin, target) + else begin + Hashtbl.replace claimed_this_round (Date.to_rata target) c; + Hashtbl.replace assignment slug (origin, target); + Hashtbl.replace candidate_by_slug slug c + end) end end done; - (assignment, candidate_by_slug) + (assignment, candidate_by_slug, out_of_range) (* The final build of one day, once placement has reached its fixed point (or exhausted the guard): resolve against the settled [injected] state, then layer on [transferred_in] (this date received an injected candidate that - went on to win) and [transferred_out] (some candidate's settled placement - originated here). - - [transferred_out] is a single [Date.t option] (Liturgical_day.mli), so it - cannot represent two different celebrations leaving the same origin day - for two different destinations. [transferred_out_of] is built with - last-write-wins for that (unreached) case; RG 97-98 collisions still - report correctly because what actually matters -- each celebration landing - on its own, correctly-ordered day, exactly once -- is carried by - [observed]/[transferred_in], not by this pointer. *) + went on to win) and [transferred_out] (whichever candidates' settled + placements originated here -- RG 97-98 lets that be more than one; see + [Liturgical_day.transferred_out]). *) let build_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) (assignment : (string, Date.t * Date.t) Hashtbl.t) + (out_of_range : (string, Date.t * Date.t) Hashtbl.t) (injected : (int, 'r Precedence.candidate list) Hashtbl.t) - (transferred_out_of : (int, Date.t) Hashtbl.t) (date : Date.t) : ('s, 'r) Liturgical_day.t = + (transferred_out_of : (int, ('r Celebration.t * Date.t) list) Hashtbl.t) (date : Date.t) : + ('s, 'r) Liturgical_day.t = let temporal, _ctx, resolution = resolve_with_injected rite idx injected date in let arrived = try Hashtbl.find injected (Date.to_rata date) with Not_found -> [] in let transferred_in = @@ -244,7 +289,7 @@ let build_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) |> Option.map (fun c -> c.Precedence.cel) in let transferred_out = - try Some (Hashtbl.find transferred_out_of (Date.to_rata date)) with Not_found -> None + try Hashtbl.find transferred_out_of (Date.to_rata date) with Not_found -> [] in (* [resolution.deferred] here is NOT "the placement pass never got to these": it is the origin day's own permanent, structural loss -- the @@ -253,23 +298,30 @@ let build_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) the exact date it was always going to lose at (this is the same fact [place_transfers]'s round loop has to filter around, see its comment). A [deferred] sighting only belongs in [omitted] if it was never - actually settled anywhere -- i.e. the guard above was hit before this - candidate reached a day it wins. Settled elsewhere means genuinely - accounted for via [observed]/[transferred_in] on the day it landed and - [transferred_out] here, not via [omitted] too -- double-booking it in - both would fail Task 12's "appears exactly once" reading of this day - alone. *) + actually settled anywhere -- i.e. it is stuck in [out_of_range], or the + guard above was hit before it reached a day it wins. Settled elsewhere + means genuinely accounted for via [observed]/[transferred_in] on the + day it landed and [transferred_out] here, not via [omitted] too -- + double-booking it in both would fail Task 12's "appears exactly once" + reading of this day alone. *) let unresolved c = let slug = Slug.to_string c.Precedence.cel.Celebration.slug in - match Hashtbl.find_opt assignment slug with - | None -> true - | Some (_, target) -> - not (Slug.equal (occupant_of rite idx injected target).Celebration.slug c.Precedence.cel.Celebration.slug) + if Hashtbl.mem out_of_range slug then true + else + match Hashtbl.find_opt assignment slug with + | None -> true + | Some (_, target) -> + not (Slug.equal (occupant_of rite idx injected target).Celebration.slug c.Precedence.cel.Celebration.slug) + in + let reason_for c = + if Hashtbl.mem out_of_range (Slug.to_string c.Precedence.cel.Celebration.slug) then + out_of_range_reason + else unconverged_reason in let omitted = List.map (fun (c, reason) -> (c.Precedence.cel, reason)) resolution.Precedence.omitted @ (resolution.Precedence.deferred |> List.filter unresolved - |> List.map (fun c -> (c.Precedence.cel, unconverged_reason))) + |> List.map (fun c -> (c.Precedence.cel, reason_for c))) in { Liturgical_day.date; @@ -296,13 +348,36 @@ let year (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) (y : int) : either. *) let n = max 0 (Date.to_rata stop - Date.to_rata start + 1) in let dates = Array.init n (fun i -> Date.add_days start i) in - let assignment, candidate_by_slug = place_transfers rite idx dates in + let assignment, candidate_by_slug, out_of_range = place_transfers rite idx ~start ~stop dates in let injected = injected_index_of_assignment assignment candidate_by_slug in - let transferred_out_of : (int, Date.t) Hashtbl.t = Hashtbl.create 16 in + let transferred_out_of : (int, ('r Celebration.t * Date.t) list) Hashtbl.t = Hashtbl.create 16 in Hashtbl.iter - (fun _slug (origin, target) -> Hashtbl.replace transferred_out_of (Date.to_rata origin) target) + (fun slug (origin, target) -> + let cel = (Hashtbl.find candidate_by_slug slug).Precedence.cel in + let key = Date.to_rata origin in + Hashtbl.replace transferred_out_of key + ((cel, target) :: (try Hashtbl.find transferred_out_of key with Not_found -> []))) assignment; - Array.map (build_day rite idx assignment injected transferred_out_of) dates + (* Canonicalise each day's departures: the accumulation above walks + [assignment] via [Hashtbl.iter], whose bucket order is not guaranteed + stable across runs (OCaml's hash seed can be randomised via + OCAMLRUNPARAM=R), so a day with more than one departure -- RG 97-98's + coinciding-feasts case -- would otherwise report them in a + run-dependent order: an environment read, in a kernel whose invariants + forbid one. [Layer.index_by_date] guards against exactly this by + re-sorting each date bucket after building it (layer.ml); same fix, + same reason. Sorted by target date -- which, for a correctly-converged + year, is also RG 97-98's own order: the higher-precedence loser claims + the earlier admissible day -- ties (not expected, but not assumed + impossible) broken on slug. *) + let by_target_then_slug (c1, t1) (c2, t2) = + let dc = Date.compare t1 t2 in + if dc <> 0 then dc else Slug.compare c1.Celebration.slug c2.Celebration.slug + in + Hashtbl.iter + (fun k v -> Hashtbl.replace transferred_out_of k (List.sort by_target_then_slug v)) + transferred_out_of; + Array.map (build_day rite idx assignment out_of_range injected transferred_out_of) dates let day (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) (date : Date.t) : ('s, 'r) Liturgical_day.t = diff --git a/lib/kernel/calendar.mli b/lib/kernel/calendar.mli index 9fbd7e7..1c0b0ed 100644 --- a/lib/kernel/calendar.mli +++ b/lib/kernel/calendar.mli @@ -11,13 +11,30 @@ every deferred candidate (RG 96-98): a losing I-class candidate the rite's rules send to [Precedence.Transfer] does not stay put -- it moves to the next day [rite.transfer_target] names as admissible, and both - ends of the move are recorded ([transferred_in] on the day it arrives, - [transferred_out] on the day it left). Every deferred candidate is - accounted for exactly once: placed, or -- only if the placement fixed - point is not reached within the round guard, which nothing in the 1962 - calendar is expected to trigger -- left in [Liturgical_day.omitted] with - a reason that says so, never silently dropped. See [calendar.ml]'s - [place_transfers] for the algorithm and its termination argument. *) + ends of the move are recorded: [transferred_in] on the day it arrives + (at most one -- RG 96 sends each departure to the next day that is not I + or II class, and the first to arrive occupies it), [transferred_out] on + the day it left (a list, not an option: RG 97-98 has coinciding I-class + feasts transfer "in order", so one day can lose more than one). Every + deferred candidate is accounted for exactly once: placed, or -- only if + the placement fixed point is not reached within the round guard (which + nothing in the 1962 calendar is expected to trigger), or the rite's own + [transfer_target] names a date outside this liturgical year's own range + (unproven to occur in the real EF calendar, but not ruled out by + construction) -- left in [Liturgical_day.omitted] with a reason that + says which, never silently dropped. See [calendar.ml]'s + [place_transfers] for the algorithm and its termination argument. + + [Precedence.Repose]-disposed losers are gathered the same way + [Precedence.Transfer]-disposed ones are (Precedence folds both into + [deferred] as one case) and are routed through the same RG 96 search. + That is only correct for [Transfer]: [Repose] denotes RG 100-102's + *repositio*, a distinct rubric this module does not implement. Nothing + in the EF ruleset currently returns [Repose] (design spec §1.3: + "declared, not exercised" -- perpetual impediment arises from + proper/diocesan calendars, out of this plan's scope), so the gap is + latent rather than a live bug; documented here rather than given a + second mechanism for a disposition nothing emits. *) (** [year rite layer y] resolves every day of the liturgical year that opens in civil year [y]: from [rite.year_start y] through the day before diff --git a/lib/kernel/liturgical_day.ml b/lib/kernel/liturgical_day.ml index cbaca9c..bbb52b8 100644 --- a/lib/kernel/liturgical_day.ml +++ b/lib/kernel/liturgical_day.ml @@ -12,8 +12,13 @@ type ('s, 'r) t = { commemorations : ('r Celebration.t * Precedence.privilege) list; transferred_in : 'r Celebration.t option; (** arrived here from an impeded day *) - transferred_out : Date.t option; - (** this day's celebration went there *) + transferred_out : ('r Celebration.t * Date.t) list; + (** celebrations that left this day, and where each one went. A list, + not an option: RG 97-98 has coinciding I-class feasts transfer + "in order" -- plural -- so a day can lose more than one. Asymmetric + with [transferred_in] deliberately: a day receives at most one + arrival, because RG 96 sends each departure to the next day that + is not I or II class, and the first to arrive occupies it. *) omitted : ('r Celebration.t * string) list; (** with the reason, never silent -- Task 12's no-celebration-lost invariant reads this *) diff --git a/lib/kernel/liturgical_day.mli b/lib/kernel/liturgical_day.mli index 38e7c76..a109251 100644 --- a/lib/kernel/liturgical_day.mli +++ b/lib/kernel/liturgical_day.mli @@ -10,8 +10,13 @@ type ('s, 'r) t = { commemorations : ('r Celebration.t * Precedence.privilege) list; transferred_in : 'r Celebration.t option; (** arrived here from an impeded day *) - transferred_out : Date.t option; - (** this day's celebration went there *) + transferred_out : ('r Celebration.t * Date.t) list; + (** celebrations that left this day, and where each one went. A list, + not an option: RG 97-98 has coinciding I-class feasts transfer + "in order" -- plural -- so a day can lose more than one. Asymmetric + with [transferred_in] deliberately: a day receives at most one + arrival, because RG 96 sends each departure to the next day that + is not I or II class, and the first to arrive occupies it. *) omitted : ('r Celebration.t * string) list; (** with the reason, never silent -- Task 12's no-celebration-lost invariant reads this *) diff --git a/test/test_calendar.ml b/test/test_calendar.ml index 70823a4..505994e 100644 --- a/test/test_calendar.ml +++ b/test/test_calendar.ml @@ -9,8 +9,16 @@ let mk y m d = match D.make ~year:y ~month:m ~day:d with Ok t -> t | Error e -> (* A synthetic rite -- not EF -- so Calendar's behaviour is proven against the abstraction, not against EF's own real (and much larger) data. Two - seasons, two ranks: enough to exercise the type parameters without - dragging in real liturgical logic Calendar itself does not compute. *) + seasons, three ranks: enough to exercise the type parameters without + dragging in real liturgical logic Calendar itself does not compute. + + Three ranks, not two: Task 6 review finding 2. With only one + Transfer-disposed rank, every deferred candidate ties on [band] and + [compare_deferred]'s [b1 <> b2] branch (the one RG 97-98 actually depends + on -- coinciding I-class feasts transfer in TABLE order, not slug order) + was unreachable; reversing it broke no test. [Hi1] outranks [Hi2], both + outrank [Lo], both are [Transfer]-disposed -- so two colliding + transferables can now differ by band, not only by slug. *) module Fixture = struct module Vocab = Colitur_kernel.Vocab module Colour = Colitur_kernel.Colour @@ -20,16 +28,16 @@ module Fixture = struct module Date_spec = Colitur_kernel.Date_spec type season = A | B - type rank = Hi | Lo + type rank = Hi1 | Hi2 | Lo let season_to_string = function A -> "a" | B -> "b" let season_of_string = function "a" -> Some A | "b" -> Some B | _ -> None - let rank_to_string = function Hi -> "hi" | Lo -> "lo" - let rank_of_string = function "hi" -> Some Hi | "lo" -> Some Lo | _ -> None + let rank_to_string = function Hi1 -> "hi1" | Hi2 -> "hi2" | Lo -> "lo" + let rank_of_string = function "hi1" -> Some Hi1 | "hi2" -> Some Hi2 | "lo" -> Some Lo | _ -> None let vocab : (season, rank) Vocab.t = { Vocab.seasons = [ A; B ]; season_to_string; season_of_string; - ranks = [ Hi; Lo ]; rank_to_string; rank_of_string } + ranks = [ Hi1; Hi2; Lo ]; rank_to_string; rank_of_string } let weekday_index d = match D.weekday d with @@ -59,14 +67,15 @@ module Fixture = struct let temporal date : (season, rank) Temporal.t = { Temporal.season = season date; week = None; weekday = D.weekday date; office = office date } - (* Band: Hi beats Lo; Temporal breaks a tie in its own favour -- the same - convention test_precedence.ml uses. *) + (* Band: Hi1 beats Hi2 beats Lo; Temporal breaks a tie against a Lo-rank + Sanctoral entry in its own favour -- the same convention + test_precedence.ml uses. *) let band (_ : season P.context) (c : rank P.candidate) = - (match c.P.cel.Cel.rank with Hi -> 10 | Lo -> 20) + (match c.P.cel.Cel.rank with Hi1 -> 5 | Hi2 -> 10 | Lo -> 20) - (match c.P.origin with P.Temporal -> 1 | P.Sanctoral -> 0) let disposition ~winner:_ ~(loser : rank P.candidate) = - match loser.P.cel.Cel.rank with Lo -> P.Commemorate P.Ordinary | Hi -> P.Transfer + match loser.P.cel.Cel.rank with Lo -> P.Commemorate P.Ordinary | Hi1 | Hi2 -> P.Transfer (* Admits at most one commemoration -- mirrors test_precedence.ml's own example and, unlike "admit everything", actually gives the accounting @@ -77,12 +86,12 @@ module Fixture = struct (* RG 96, generic form: search forward from the day after [origin] for the first day whose occupant is not "blocking" -- in this synthetic - vocabulary Hi stands in for I/II class, Lo for everything else (the same - convention [band] already uses). No Annunciation-style starting-point - override: that exception is EF-specific (RG 96) and belongs to the real - rite (Task 11, pinned by Task 17's golden years), not to this - abstraction-level fixture, which only has to prove Calendar's placement - mechanism, not EF's own rubrics. *) + vocabulary Hi1/Hi2 stand in for I/II class, Lo for everything else (the + same convention [band] already uses). No Annunciation-style + starting-point override: that exception is EF-specific (RG 96) and + belongs to the real rite (Task 11, pinned by Task 17's golden years), + not to this abstraction-level fixture, which only has to prove + Calendar's placement mechanism, not EF's own rubrics. *) let transfer_target (_ : rank P.candidate) (origin : D.t) (occupant : D.t -> rank Cel.t) : D.t = let rec search d = if (occupant d).Cel.rank = Lo then d else search (D.add_days d 1) in search (D.add_days origin 1) @@ -96,20 +105,20 @@ module Fixture = struct cel = Cel.make ~slug:(Sl.of_string_exn slug) ~rank ~colour:Colour.White ~layer:"synthetic-sanctoral" () } - let big_feast = entry ~month:12 ~day:8 ~slug:"big-feast" ~rank:Hi + let big_feast = entry ~month:12 ~day:8 ~slug:"big-feast" ~rank:Hi1 let commem_worthy = entry ~month:12 ~day:15 ~slug:"commem-worthy" ~rank:Lo (* 20 Dec: four sanctoral entries on one date, for the full-accounting test. - "day-winner" and "eclipsed" tie on band (both Hi, both Sanctoral); ties - break on slug, so "day-winner" wins and "eclipsed" -- a Hi-rank loser -- - is [Transfer]-disposed, landing in [deferred]. "loser-a" and "loser-b" - are both Lo, both [Commemorate]-disposed, but [admit] only keeps one: - the other lands in Precedence's own [omitted] ("admission limit - reached"), distinct from "eclipsed"'s deferred reason. Four candidates, - three different fates -- observed, one specific omission reason, two - more. *) - let day_winner = entry ~month:12 ~day:20 ~slug:"day-winner" ~rank:Hi - let eclipsed = entry ~month:12 ~day:20 ~slug:"eclipsed" ~rank:Hi + "day-winner" and "eclipsed" tie on band (both Hi1, both Sanctoral); + ties break on slug, so "day-winner" wins and "eclipsed" -- a Hi1-rank + loser -- is [Transfer]-disposed, landing in [deferred]. "loser-a" and + "loser-b" are both Lo, both [Commemorate]-disposed, but [admit] only + keeps one: the other lands in Precedence's own [omitted] ("admission + limit reached"), distinct from "eclipsed"'s deferred reason. Four + candidates, three different fates -- observed, one specific omission + reason, two more. *) + let day_winner = entry ~month:12 ~day:20 ~slug:"day-winner" ~rank:Hi1 + let eclipsed = entry ~month:12 ~day:20 ~slug:"eclipsed" ~rank:Hi1 let loser_a = entry ~month:12 ~day:20 ~slug:"loser-a" ~rank:Lo let loser_b = entry ~month:12 ~day:20 ~slug:"loser-b" ~rank:Lo @@ -118,33 +127,40 @@ module Fixture = struct [ big_feast; commem_worthy; day_winner; eclipsed; loser_a; loser_b ] (* RG 96 (Task 6): "transferable" is impeded on 10 Jan by "blocker-a" (both - Hi; ties break on slug, "blocker-a" < "transferable", so "blocker-a" + Hi1; ties break on slug, "blocker-a" < "transferable", so "blocker-a" wins and "transferable" is the loser). 11 and 12 Jan are ALSO occupied - by their own uncontested Hi-rank entries, so the placement search must + by their own uncontested Hi1-rank entries, so the placement search must walk past more than one ineligible day, not just try origin+1 and stop. 13 Jan carries nothing, so the feria (Lo) is the first admissible day. *) - let blocker_a = entry ~month:1 ~day:10 ~slug:"blocker-a" ~rank:Hi - let transferable = entry ~month:1 ~day:10 ~slug:"transferable" ~rank:Hi - let blocker_b = entry ~month:1 ~day:11 ~slug:"blocker-b" ~rank:Hi - let blocker_c = entry ~month:1 ~day:12 ~slug:"blocker-c" ~rank:Hi - - (* RG 97-98: three Hi-rank entries coincide on 1 Feb. Sorted by band then - slug (all three tie on band, since Fixture's [band] only reads rank): - "collision-winner" < "transfer-a" < "transfer-b". The winner keeps 1 - Feb; the other two -- both losers, both Hi, both [Transfer]-disposed -- - must transfer in that same order. 2 and 3 Feb carry nothing of their - own, so they are the two admissible days the pair must land on, - consecutively, in that order: "transfer-a" (the higher-precedence - loser) gets first claim on 2 Feb, pushing "transfer-b" to 3 Feb. *) - let collision_winner = entry ~month:2 ~day:1 ~slug:"collision-winner" ~rank:Hi - let transfer_a = entry ~month:2 ~day:1 ~slug:"transfer-a" ~rank:Hi - let transfer_b = entry ~month:2 ~day:1 ~slug:"transfer-b" ~rank:Hi + let blocker_a = entry ~month:1 ~day:10 ~slug:"blocker-a" ~rank:Hi1 + let transferable = entry ~month:1 ~day:10 ~slug:"transferable" ~rank:Hi1 + let blocker_b = entry ~month:1 ~day:11 ~slug:"blocker-b" ~rank:Hi1 + let blocker_c = entry ~month:1 ~day:12 ~slug:"blocker-c" ~rank:Hi1 + + (* RG 97-98: three entries coincide on 1 Feb, spanning both Transfer- + disposed ranks so band order and slug order genuinely disagree (Task 6 + review finding 2). "collision-winner" and "transfer-hi1" both tie at + the BETTER band (Hi1, 5); "transfer-hi2" is at the WORSE band (Hi2, + 10). Within the Hi1 tie, slug decides: "collision-winner" < "transfer- + hi1", so "collision-winner" keeps 1 Feb. Of the two losers, + "transfer-hi1" (band 5) outranks "transfer-hi2" (band 10) -- by BAND, + not by slug: "transfer-b" (transfer-hi2's slug) sorts alphabetically + *before* "transfer-z" (transfer-hi1's slug). A sort that used slug + instead of band, or compared band backwards, would place "transfer-b" + on 2 Feb instead of "transfer-z" -- exactly the wrong-order failure + mode finding 2 flagged as unreachable in the old two-Hi-rank fixture. + 2 and 3 Feb carry nothing of their own, so they are the two admissible + days the pair must land on, consecutively, in band order: + "transfer-hi1" claims 2 Feb, pushing "transfer-hi2" to 3 Feb. *) + let collision_winner = entry ~month:2 ~day:1 ~slug:"collision-winner" ~rank:Hi1 + let transfer_hi1 = entry ~month:2 ~day:1 ~slug:"transfer-z" ~rank:Hi1 + let transfer_hi2 = entry ~month:2 ~day:1 ~slug:"transfer-b" ~rank:Hi2 let layer_with_collision = Layer.of_entries ~id:"synthetic-with-collision" ~name:"Synthetic sanctoral (with collisions)" [ big_feast; commem_worthy; day_winner; eclipsed; loser_a; loser_b; blocker_a; transferable; blocker_b; blocker_c; - collision_winner; transfer_a; transfer_b ] + collision_winner; transfer_hi1; transfer_hi2 ] let liturgical_year_of date = let cy = D.year date in @@ -231,7 +247,7 @@ let test_day_near_domain_floor_does_not_raise () = duplicated into two buckets and another dropped, which this project has shipped before (register finding). - "eclipsed" -- the Hi-rank loser on 20 Dec -- no longer sits in [omitted] + "eclipsed" -- the Hi1-rank loser on 20 Dec -- no longer sits in [omitted] here (that was Task 5's honest placeholder, before Task 6 existed to place it): RG 95 gives an I-class loser the right of translation, so it is genuinely gone from this day's own accounting, and its departure is @@ -265,14 +281,14 @@ let test_full_day_accounting () = not something new. What IS new here: this day positively records that a transfer happened, via a different field entirely. *) Alcotest.(check bool) "20 Dec records that something transferred out" true - (d.LD.transferred_out <> None) + (d.LD.transferred_out <> []) (* Task 6's placement pass (RG 96-98), properties 1 and 2: a transferred celebration appears exactly once in the whole year -- transfer moves, not duplicates -- and [transferred_in]/[transferred_out] are set on the two ends of the move and point at each other. "transferable" is impeded on 10 Jan by "blocker-a" (same band, tie-broken by slug), and 11-12 Jan are also - occupied by their own uncontested Hi entries, so this also proves the + occupied by their own uncontested Hi1 entries, so this also proves the search walks past more than one ineligible day rather than only trying origin+1. *) let test_transfer_moves_and_does_not_duplicate () = @@ -292,22 +308,31 @@ let test_transfer_moves_and_does_not_duplicate () = | Some c -> Sl.to_string c.Cel.slug | None -> ""); (* Located by its own known origin date, not by "the first day with - transferred_out set" -- layer_with_collision has more than one day that - transfers something out (20 Dec's "eclipsed", 1 Feb's "transfer-b"), so - that would silently pick up whichever happens to sort first in the - array rather than proving THIS origin points at THIS landing. *) + transferred_out <> []" -- layer_with_collision has more than one day + that transfers something out (20 Dec's "eclipsed", 1 Feb's two losers), + so that would silently pick up whichever happens to sort first in the + array rather than proving THIS origin points at THIS landing. Its own + origin has exactly one departure -- unlike 1 Feb below -- so a single + pair pins it. *) let origin = Array.to_list days |> List.find (fun d -> D.compare d.LD.date (mk 2027 1 10) = 0) in - Alcotest.(check bool) "origin points at the landing date" true - (origin.LD.transferred_out = Some landed.LD.date) - -(* Property 3: RG 97-98's ordering. Two Hi-rank losers coincide on 1 Feb - (with "collision-winner" keeping the day); band ties, so slug order IS - band order here, same convention Precedence.compare_by uses for real RG - 91 entries that tie within one table slot. Checked by DATE, not by - "b landed one day after a" -- Task 5's review flagged exactly that - style of check as satisfiable by construction (an Array.init built from - add_days would pass it trivially); asserting the literal landing dates - independently is what actually exercises the placement order. *) + Alcotest.(check int) "exactly one departure recorded at the origin" 1 + (List.length origin.LD.transferred_out); + let departed_cel, departed_to = List.hd origin.LD.transferred_out in + Alcotest.(check string) "the departed celebration is \"transferable\"" "transferable" + (Sl.to_string departed_cel.Cel.slug); + Alcotest.(check string) "it points at the landing date" (D.to_iso8601 landed.LD.date) + (D.to_iso8601 departed_to) + +(* Property 3: RG 97-98's ordering, genuinely by band (Task 6 review finding + 2) -- see the [layer_with_collision] comment for how the fixture is built + so band order and slug order actively disagree here: "transfer-hi1" + (slug "transfer-z", band 5) must claim 2 Feb before "transfer-hi2" (slug + "transfer-b", band 10), even though "transfer-b" sorts alphabetically + first. Checked by DATE, not by "b landed one day after a" -- Task 5's + review flagged exactly that style of check as satisfiable by construction + (an Array.init built from add_days would pass it trivially); asserting + the literal landing dates independently is what actually exercises the + placement order. *) let test_two_colliding_transferables_land_in_band_order () = let days = C.year Fixture.rite Fixture.layer_with_collision 2026 in let observed_on date = @@ -317,18 +342,66 @@ let test_two_colliding_transferables_land_in_band_order () = in Alcotest.(check string) "collision-winner keeps 1 Feb" "collision-winner" (observed_on (mk 2027 2 1)); - Alcotest.(check string) "higher-precedence loser (transfer-a) claims 2 Feb first" "transfer-a" + Alcotest.(check string) "higher-band loser (transfer-z, Hi1) claims 2 Feb first" "transfer-z" (observed_on (mk 2027 2 2)); - Alcotest.(check string) "lower-precedence loser (transfer-b) is pushed to 3 Feb" "transfer-b" + Alcotest.(check string) "lower-band loser (transfer-b, Hi2) is pushed to 3 Feb" "transfer-b" (observed_on (mk 2027 2 3)); let count slug = Array.to_list days |> List.filter (fun d -> Sl.to_string d.LD.observed.Cel.slug = slug) |> List.length in - Alcotest.(check int) "transfer-a appears exactly once in the year" 1 (count "transfer-a"); + Alcotest.(check int) "transfer-z appears exactly once in the year" 1 (count "transfer-z"); Alcotest.(check int) "transfer-b appears exactly once in the year" 1 (count "transfer-b") +(* Task 6 review finding 1: RG 97-98 says coinciding I-class feasts transfer + "in order" -- plural -- so 1 Feb's origin must record BOTH departures + ("transfer-z" -> 2 Feb, "transfer-b" -> 3 Feb), not just one. The + original [Date.t option] could only ever hold one; with three entries + colliding on the same date it silently dropped whichever [Hashtbl.iter] + visited last, which depends on OCaml's hash seed (OCAMLRUNPARAM=R) -- an + environment read in a kernel whose invariants forbid one. Sorting both + sides before comparing makes this assertion itself independent of + [transferred_out]'s own (now canonicalised, but not part of the + contract) internal order. *) +let test_origin_records_every_departure () = + let days = C.year Fixture.rite Fixture.layer_with_collision 2026 in + let origin = Array.to_list days |> List.find (fun d -> D.compare d.LD.date (mk 2027 2 1) = 0) in + let departures = + origin.LD.transferred_out + |> List.map (fun (c, target) -> (Sl.to_string c.Cel.slug, D.to_iso8601 target)) + |> List.sort compare + in + Alcotest.(check (list (pair string string))) + "both losers' departures are recorded, order-independently" + (List.sort compare [ ("transfer-z", "2027-02-02"); ("transfer-b", "2027-02-03") ]) + departures + +(* Task 6 review finding 3: a rite whose [transfer_target] names a date + outside the liturgical year's own [start, stop] must not make the + candidate vanish. "eclipsed" is impeded on 20 Dec as usual, but this + rite's search jumps 5000 days forward -- far past [stop] -- instead of + walking to the next admissible day. It must never become [observed] + anywhere in the array (there is nowhere in the array for it to land), + and its origin must record the specific out-of-range reason, not the + generic non-convergence one (this placement decides on round 1; the + round guard is never even approached). *) +let test_transfer_target_outside_year_is_recorded_not_lost () = + let stray_rite = + { Fixture.rite with Rite.transfer_target = (fun _ origin _ -> D.add_days origin 5000) } + in + let days = C.year stray_rite Fixture.layer 2026 in + let observed_anywhere = + Array.to_list days |> List.exists (fun d -> Sl.to_string d.LD.observed.Cel.slug = "eclipsed") + in + Alcotest.(check bool) "never becomes observed anywhere in the year" false observed_anywhere; + let origin = Array.to_list days |> List.find (fun d -> D.compare d.LD.date (mk 2026 12 20) = 0) in + let reason_of slug = + origin.LD.omitted |> List.find (fun (c, _) -> Sl.to_string c.Cel.slug = slug) |> snd + in + Alcotest.(check string) "recorded with the out-of-range reason, not silently dropped" + "omitted: transfer target falls outside the liturgical year (RG 96)" (reason_of "eclipsed") + (* Termination is a correctness requirement (brief): a rite whose [transfer_target] always answers with the impeded day itself (never strictly forward, so the pass can never reach a fixed point) must not @@ -366,5 +439,9 @@ let suite = test_transfer_moves_and_does_not_duplicate; Alcotest.test_case "two colliding transferables land in band order" `Quick test_two_colliding_transferables_land_in_band_order; + Alcotest.test_case "origin records every departure" `Quick + test_origin_records_every_departure; + Alcotest.test_case "transfer target outside year is recorded not lost" `Quick + test_transfer_target_outside_year_is_recorded_not_lost; Alcotest.test_case "transfer guard records failure instead of looping" `Quick test_transfer_guard_records_failure_instead_of_looping ] ) -- cgit v1.3 From 7f183c847f8b67c88ad6ea3bf2d635c5c0534651 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Wed, 12 Aug 2026 00:44:36 +0200 Subject: cli: colitur day dumps resolved liturgical days Assembles Rite_ef.context (lib/rites/rite_ef/rite_ef.ml[i]): temporal, anchors and vocab from Temporal_ef; rules from Precedence_ef's band, disposition and admit; season_runs = Vocab_ef.seasons; transfer_target newly implemented here. transfer_target (RG 96): the next following day that is not I or II class, with the Annunciation's own exception (Monday after Low Sunday). Terminates by a structural step bound on its internal search, independent of Calendar's own round guard, which bounds rounds across a year, not one call's walk; documented as an obligation on rite.mli's transfer_target field, which did not previously state it. Fixes the vigil-naming mismatch Task 7's review predicted: the sanctoral bootstrap names its vigils with a vigil-of-X prefix (lectio's own convention), while Precedence_ef's is_vigil only recognised the temporal cycle's own X-vigil suffix. Both are now recognised, fixing RG 91 entries 21/26 and RG 33's vigil omission for the four affected celebrations. Verified by unit test and by mutation-testing the fix (reverting it fails exactly the new rows) and against real output across several years. Suppresses data/ef/sanctoral.sexp's vigil-of-christmas via a new overlay, data/ef/adjustments.sexp: it is the same celebration as the temporal cycle's own ef-nativity-vigil, both dated 24 December. colitur day : one line per civil-year day, temporal and sanctoral fully resolved through Layer, Overlay, Precedence_ef and Calendar -- the first CLI path exercising the whole Plan 3 pipeline against real data. Verified the All Souls transfer chain (Tasks 7-8-11) end to end against real output for both a Sunday year (2025, lands on 3 Nov) and a non-Sunday year (2026, observed directly on 2 Nov). --- bin/main.ml | 137 +++++++++++++++++++++++++++++++++++- data/ef/adjustments.sexp | 13 ++++ lib/kernel/rite.mli | 22 +++++- lib/rites/rite_ef/precedence_ef.ml | 112 +++++++++++++++++++++++++++-- lib/rites/rite_ef/precedence_ef.mli | 68 ++++++++++++++++-- lib/rites/rite_ef/rite_ef.ml | 24 +++++++ lib/rites/rite_ef/rite_ef.mli | 35 +++++++++ test/cli.t | 67 +++++++++++++++++- test/dune | 2 +- test/test_precedence_ef.ml | 130 +++++++++++++++++++++++++++++++++- 10 files changed, 594 insertions(+), 16 deletions(-) create mode 100644 data/ef/adjustments.sexp create mode 100644 lib/rites/rite_ef/rite_ef.ml create mode 100644 lib/rites/rite_ef/rite_ef.mli (limited to 'lib/kernel') diff --git a/bin/main.ml b/bin/main.ml index 896a6bd..53cae87 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -41,8 +41,142 @@ let temporal_report y = d := D.add_days !d 1 done +(* Task 11: the fully resolved EF calendar (temporal AND sanctoral, + occurrence and transfers applied), one line per civil-year day -- + "YYYY-MM-DD weekday season week slug rank colour [+commemoration-slug]...". + [temporal_report] above only ever showed the temporal cycle in isolation + ([Rite_ef.Temporal_ef.temporal] directly, no sanctoral layer, no + [Precedence] contest); this is the first CLI path that runs every piece + Plan 3 built -- [Colitur_kernel.Layer], [Overlay], [Precedence_ef], + [Calendar] -- against real data. *) + +(* [data/ef/sanctoral.sexp] and [data/ef/adjustments.sexp] are located + relative to the BUILD TREE, not the process's own cwd: cwd varies with + how the binary is invoked (a user's shell for `dune exec colitur --`, a + dune cram test's own sandboxed temp directory for `test/cli.t`) and + nothing in this project's build pins it to the repository root. A + build-time constant substituted via dune's [%{workspace_root}] was tried + first and rejected: it is resolved RELATIVE TO THE BUILD ACTION'S OWN + directory (empirically "." here, not an absolute path -- dune keeps + build actions relocatable), so it silently reproduces the same + cwd-dependence this is trying to eliminate, just baked in at build time + instead of read at run time; confirmed by the resulting `colitur day` + failing to find its own data outside the exact directory the build + happened to run in. + + [Sys.executable_name] does not have that problem -- on Linux it resolves + through /proc/self/exe, which the kernel always reports as the + executable's own canonical absolute path, even when the process was + launched through a symlink (verified against dune's own cram sandbox, + which places exactly such a symlink; see the task report). dune's default + ("no [(sandbox ...)] declared") build context mirrors the ENTIRE source + tree under _build/default/, unconditionally, so climbing from + _build/default/bin/main.exe up two directories and back down into data/ + always finds both files, regardless of the caller's own cwd. + + Known limitation, not yet exercised by this project: a `dune install`- + style deployment (executable copied to a prefix with no adjacent _build/ + default/data/) would need a different resolution strategy; there is no + install story yet (README.md: `dune exec` only), so this is not a + regression against anything this project currently supports. *) +let data_dir () = Filename.dirname (Filename.dirname Sys.executable_name) ^ "/data/ef" + +(* Loads the universal sanctoral layer and applies the one hand-authored + overlay over it (data/ef/adjustments.sexp -- see that file's own header): + [Overlay.apply]'s diagnostics are never silently dropped (Overlay.mli), + so any that come back -- expected to be none in the committed data; see + the overlay file's own comment on when one WOULD fire -- are printed to + stderr, loudly, without aborting the run. *) +let load_ef_layer () = + let dir = data_dir () in + let sanctoral_path = Filename.concat dir "sanctoral.sexp" in + let adjustments_path = Filename.concat dir "adjustments.sexp" in + match Colitur_kernel.Layer.load Rite_ef.Vocab_ef.rank_of_sexp sanctoral_path with + | Error e -> Error (Printf.sprintf "failed to load %s: %s" sanctoral_path e) + | Ok layer -> ( + match Colitur_kernel.Overlay.load Rite_ef.Vocab_ef.rank_of_sexp adjustments_path with + | Error e -> Error (Printf.sprintf "failed to load %s: %s" adjustments_path e) + | Ok overlay -> + let layer, diagnostics = Colitur_kernel.Overlay.apply layer overlay in + List.iter + (fun d -> Printf.eprintf "colitur: %s\n" (Colitur_kernel.Overlay.diagnostic_to_string d)) + diagnostics; + Ok layer) + +let day_line (d : (Rite_ef.Vocab_ef.season, Rite_ef.Vocab_ef.rank) Colitur_kernel.Liturgical_day.t) + = + let t = d.Colitur_kernel.Liturgical_day.temporal in + let cel = d.Colitur_kernel.Liturgical_day.observed in + let week = + match t.Colitur_kernel.Temporal.week with Some n -> string_of_int n | None -> "-" + in + let commemoration_suffix (c, _) = + " +" ^ Colitur_kernel.Slug.to_string c.Colitur_kernel.Celebration.slug + in + let commemorations = + String.concat "" (List.map commemoration_suffix d.Colitur_kernel.Liturgical_day.commemorations) + in + Printf.printf "%s %s %s %s %s %s %s%s\n" (D.to_iso8601 d.Colitur_kernel.Liturgical_day.date) + (D.weekday_to_string t.Colitur_kernel.Temporal.weekday) + (Rite_ef.Vocab_ef.season_to_string t.Colitur_kernel.Temporal.season) + week + (Colitur_kernel.Slug.to_string cel.Colitur_kernel.Celebration.slug) + (Rite_ef.Vocab_ef.rank_to_string cel.Colitur_kernel.Celebration.rank) + (Colitur_kernel.Colour.to_string cel.Colitur_kernel.Celebration.colour) + commemorations + +(* One civil year, Jan 1 - Dec 31, matching [temporal_report]'s own scan -- + NOT one liturgical year: [Colitur_kernel.Calendar.year] resolves a single + Advent-anchored liturgical year, which straddles two civil years, so a + civil year's worth of output needs the tail of the liturgical year that + opened the PREVIOUS civil year (covers roughly 1 Jan - 28 Nov) plus the + liturgical year that opens within this one (roughly 29 Nov - 31 Dec). + Both are computed once each -- not once per day via [Calendar.day], which + would recompute the whole (~365-day) placement pass up to 365 times over + for the days sharing one liturgical year (calendar.mli's own "pays it + once" cost model assumes exactly this usage: call [year], not [day] in a + loop). *) +let day_report y = + match load_ef_layer () with + | Error msg -> + Printf.eprintf "colitur: %s\n" msg; + exit 2 + | Ok layer -> + let module Cal = Colitur_kernel.Calendar in + let by_rata : (int, (Rite_ef.Vocab_ef.season, Rite_ef.Vocab_ef.rank) Colitur_kernel.Liturgical_day.t) Hashtbl.t = + Hashtbl.create 400 + in + let index days = + Array.iter + (fun (d : (Rite_ef.Vocab_ef.season, Rite_ef.Vocab_ef.rank) Colitur_kernel.Liturgical_day.t) -> + Hashtbl.replace by_rata (D.to_rata d.Colitur_kernel.Liturgical_day.date) d) + days + in + index (Cal.year Rite_ef.context layer (y - 1)); + index (Cal.year Rite_ef.context layer y); + let jan1 = match D.make ~year:y ~month:1 ~day:1 with Ok t -> t | Error e -> failwith e in + let dec31 = match D.make ~year:y ~month:12 ~day:31 with Ok t -> t | Error e -> failwith e in + let d = ref jan1 in + while D.compare !d dec31 <= 0 do + (match Hashtbl.find_opt by_rata (D.to_rata !d) with + | Some day -> day_line day + | None -> + (* Unreachable for any [y] in 1583..9999: the two indexed + liturgical years jointly cover [year_start (y-1), year_start + (y+1)), which contains all of civil year [y] + (calendar.mli). Not a [failwith] -- an out-of-domain [d] + inside this loop is impossible by construction (jan1/dec31 + are themselves validated in range, and [add_days] only ever + advances within the same civil year here) -- but a silent + skip would violate the same "never silently dropped" + standard the kernel holds itself to, so a gap surfaces + loudly on stderr rather than as a quietly short year. *) + Printf.eprintf "colitur: internal error: no resolved day for %s\n" (D.to_iso8601 !d)); + d := D.add_days !d 1 + done + let usage () = - prerr_endline "colitur: usage: colitur easter | colitur temporal "; + prerr_endline "colitur: usage: colitur easter | colitur temporal | colitur day "; exit 2 let with_year ys f = @@ -57,4 +191,5 @@ let () = match Sys.argv with | [| _; "easter"; ys |] -> with_year ys easter_report | [| _; "temporal"; ys |] -> with_year ys temporal_report + | [| _; "day"; ys |] -> with_year ys day_report | _ -> usage () diff --git a/data/ef/adjustments.sexp b/data/ef/adjustments.sexp new file mode 100644 index 0000000..85d7fa1 --- /dev/null +++ b/data/ef/adjustments.sexp @@ -0,0 +1,13 @@ +; data/ef/adjustments.sexp -- hand-authored overlay over data/ef/sanctoral.sexp +; (Task 11). NOT generated by tools/bootstrap_sanctoral.ml -- edit directly. +; +; Suppresses `vigil-of-christmas` (24 Dec, data/ef/sanctoral.sexp, lectio's +; own bootstrapped entry): it is the SAME celebration as colitur's temporal +; cycle's own `ef-nativity-vigil` (rite_ef/temporal_ef.ml's [named], also 24 +; Dec, RG 91 entry 5), not a second, distinct one. Once the sanctoral layer +; is live, that date would otherwise carry two candidates for one feast. +; Recorded as an Overlay directive rather than filtered out of the bootstrap +; or special-cased in code, per the task brief -- an auditable, diagnosable +; removal (Overlay.apply's own diagnostic fires if this slug is ever absent, +; e.g. after a re-bootstrap that renames it), not a silent drop. +((id ef-adjustments) (directives ((Suppress vigil-of-christmas)))) diff --git a/lib/kernel/rite.mli b/lib/kernel/rite.mli index 6d12dd4..ffe9471 100644 --- a/lib/kernel/rite.mli +++ b/lib/kernel/rite.mli @@ -38,5 +38,25 @@ type ('s, 'r) t = { 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". *) + just to answer "what sits here". + + OBLIGATIONS (not enforced by the type, and {!Calendar}'s own + termination argument depends on both): the result must be + {b strictly later} than the [Date.t] argument (the date the + candidate was impeded on) -- {!Calendar}'s placement pass treats + [target = origin] or [target < origin] as a legitimate placement, + not an error, so a rite whose search can stand still or go + backward would silently loop candidates in place or resurrect an + already-superseded occupant rather than failing loudly. The call + must also {b terminate} on its own: {!Calendar}'s round guard + (calendar.ml's [max_transfer_rounds]) bounds how many ROUNDS the + whole-year placement pass takes, which is a distinct, outer thing + from whatever internal search a single call to this function runs + -- an implementation that walks forward day by day looking for an + admissible date, without its own bound, can hang the caller + outright on a rite/data shape it does not handle, never reaching + the round guard at all. See rite_ef/precedence_ef.ml's + [transfer_target] for a concrete termination argument (a + structural step bound, not an appeal to the real calendar's own + structure). *) } diff --git a/lib/rites/rite_ef/precedence_ef.ml b/lib/rites/rite_ef/precedence_ef.ml index ff6f991..e1c13d1 100644 --- a/lib/rites/rite_ef/precedence_ef.ml +++ b/lib/rites/rite_ef/precedence_ef.ml @@ -55,13 +55,22 @@ let is_universal layer = String.equal layer universal_layer {!Celebration.t} otherwise marks "this is a vigil, not an ordinary office of the same rank" (see the file's top comment), so entries 21/26 read it off the temporal cycle's own slug suffix (rite_ef/temporal_ef.ml's - [named], e.g. "ef-ascension-vigil"). Exposed so a future task naming a - sanctoral vigil (Task 10: Assumption, John Baptist, Peter & Paul, - Lawrence -- only Ascension exists today) uses the same suffix; a - differently-named vigil would band 16/24 instead of 21/26, silently. *) + [named], e.g. "ef-ascension-vigil"). *) let vigil_suffix = "-vigil" -let is_vigil slug = String.ends_with ~suffix:vigil_suffix slug +(* Not an RG citation -- see [universal_layer]. Task 10's sanctoral bootstrap + turned out to name its four real vigils with lectio's OWN convention, a + "vigil-of-X" PREFIX (data/ef/sanctoral.sexp: vigil-of-st-lawrence, + vigil-of-sts-peter-paul, vigil-of-the-assumption, vigil-of-the-nativity- + of-st-john-the-baptist), not [vigil_suffix] -- exactly the mismatch Task + 7's review predicted when it asked for [vigil_suffix] to be exposed. + [is_vigil] below checks both conventions, so a celebration is a "vigil" + for RG 91/33's purposes regardless of which layer (temporal or sanctoral) + produced it. *) +let vigil_prefix = "vigil-of-" + +let is_vigil slug = + String.ends_with ~suffix:vigil_suffix slug || String.starts_with ~prefix:vigil_prefix slug (* Not an RG citation -- see [universal_layer]. Entry 18's Ember days are identified by the temporal cycle's own slug convention (rite_ef/ @@ -519,3 +528,96 @@ let admit ~(observed : Vocab_ef.rank Precedence.candidate) (* RG 111: "III-IV class: at most two" -- by dignity, same as the non-Sunday II-class case, just with room for two. *) take 2 sorted + +(* Task 11: RG 96 -- where an impeded I-class feast lands (docs/research/ + rules-register.md §4, "Transfer/translation"). [band] decides who is + impeded; [disposition] decides that an impeded I-class FEAST (not a + Sunday, not omitted by RG 33) is [Transfer]-disposed; this is the third + and final question RG 96 poses -- WHERE the translation lands -- and is + {!Rite.t.transfer_target} itself, called by {!Calendar}'s placement pass + once per deferred candidate, never re-run once a target is accepted + (calendar.ml's own comment on [~start ~stop]). + + RG 96's own text, register-transcribed: "the next following day that is + not I or II class." [is_blocking] reads that off [Vocab_ef.rank] -- + RG 96 speaks of the day's CLASS (RG 8's four-way dignity), not [band]'s + finer 28-entry occurrence-table row, the same distinction {!admit} above + already draws for RG 111 ({!dignity}, not [band]). *) +let is_blocking (rank : Vocab_ef.rank) = rank = Vocab_ef.Class1 || rank = Vocab_ef.Class2 + +(* RG 96's own named exception, register-transcribed: "(Annunciation + exception): -> Monday after Low Sunday." Identified by slug -- the same + convention this file already uses to pick out one specific celebration + from a rank/status shape shared by many others ({!nativity_octave_prefix}, + [is_ember_18]'s date anchors) -- not an RG citation itself: RG 96 does not + encode how a computer recognises "the Annunciation", only what happens to + it once recognised. data/ef/sanctoral.sexp's own bootstrapped slug (Task + 10), reused verbatim rather than guessed. *) +let annunciation_slug = "annunciation-of-the-blessed-virgin-mary" + +(* Not an RG citation -- a defensive engineering ceiling, the same role + Calendar's own [max_transfer_rounds] plays for the OUTER round loop + (calendar.ml). That guard bounds how many ROUNDS the whole-year placement + pass takes; it does nothing for the walk a single call to this function + makes internally, which is this module's own responsibility (rite.mli + documents the obligation this constant exists to satisfy). Comfortably + longer than the longest real run of consecutive I/II-class days the 1962 + calendar produces -- 24 Dec to 1 Jan (the Nativity vigil through the + Circumcision, both I class, with the intervening octave days II class) is + 9 days; Easter through Low Sunday (the Easter octave, I class, entry 10) + is 8 -- RG 91 entry 28's own unqualified IV-class catch-all guarantees a + non-blocking feria follows any such run in real data. Not tuned to that + bound any more than 64 is tuned to RG 97-98's real collision count: a + ceiling nothing in the 1962 calendar comes close to, so a rite/data shape + this module has not anticipated fails FINITELY (see [search_from]) rather + than hanging the CLI. *) +let max_search_days = 400 + +(* Walks forward from [d], returning the first date [occupant] reports as + NOT [is_blocking]. [steps] is a strictly increasing structural bound on + the recursion, capped at [max_search_days]: the function decreases + [max_search_days - steps] by exactly one on every call and returns as + soon as that reaches zero (whether or not an admissible day was ever + found), so THIS loop terminates by construction, regardless of what + [occupant] reports -- it does not rely on the real EF calendar's own + structure to guarantee termination the way the comment above explains + why the bound is never actually reached in practice. If the bound is + reached, the last date visited is returned WITHOUT probing [occupant] + again -- one more finite (not necessarily admissible) date, not a + further search -- because the val the caller ([transfer_target]) is + still owed is "a date", never an exception; {!Calendar}'s own + [~start ~stop] bound (calendar.ml's [place_transfers]) is what turns an + implausible non-terminating real search into a recorded [omitted], not + this function pretending to have found something admissible. *) +let rec search_from (occupant : Date.t -> Vocab_ef.rank Celebration.t) (steps : int) (d : Date.t) : + Date.t = + if steps >= max_search_days then d + else if is_blocking (occupant d).Celebration.rank then search_from occupant (steps + 1) (Date.add_days d 1) + else d + +(* [transfer_target]'s contract (rite.mli): total, terminating, and its + result is always strictly after [origin]. Terminating: [search_from]'s + own structural bound, above. Strictly after [origin]: the ordinary branch + starts the search at [Date.add_days origin 1] and [search_from] only ever + advances forward from its own starting point, so the result is always >= + origin + 1. The Annunciation branch starts instead at the Monday after + Low Sunday for [origin]'s own civil year -- NOT provably later than + [origin] by the code alone, but true of every representable year: the + Annunciation's [origin] is always 25 March (Date_spec.Fixed in + data/ef/sanctoral.sexp), Easter always falls within that SAME civil year + in [22 March, 25 April] (Computus's own documented range, register §0), + so Low Sunday (Easter + 7) falls in [29 March, 2 May] and the Monday + after it in [30 March, 3 May] -- always after 25 March. *) +let transfer_target (c : Vocab_ef.rank Precedence.candidate) (origin : Date.t) + (occupant : Date.t -> Vocab_ef.rank Celebration.t) : Date.t = + let start = + if Slug.to_string c.Precedence.cel.Celebration.slug = annunciation_slug then + (* Low Sunday = Easter + 7 (register §0, temporal_ef.ml's [off 7]); the + Monday after it = Easter + 8. Searched onward from there exactly + like the general case searches from [origin + 1] -- "only if that + day is itself blocked" (rite.mli) is [search_from]'s ordinary + behaviour, not a second mechanism. *) + Date.add_days (Computus.gregorian_easter (Date.year origin)) 8 + else Date.add_days origin 1 + in + search_from occupant 0 start diff --git a/lib/rites/rite_ef/precedence_ef.mli b/lib/rites/rite_ef/precedence_ef.mli index e1b3638..d06b058 100644 --- a/lib/rites/rite_ef/precedence_ef.mli +++ b/lib/rites/rite_ef/precedence_ef.mli @@ -19,14 +19,31 @@ val universal_layer : string val indult_prefix : string (** Slug suffix marking a celebration as a vigil (RG 91 entries 21, 26), - e.g. "ef-ascension-vigil". Also colitur's own convention, not an RG - citation, exposed for the same reason as {!universal_layer}: only the - Ascension Vigil exists today (rite_ef/temporal_ef.ml); the Assumption, - John Baptist, Peter & Paul and Lawrence vigils arrive as sanctoral data - in a future task, and must use this same suffix or {!band} will band - them 16/24 (an ordinary feast of the same rank) instead of 21/26. *) + e.g. "ef-ascension-vigil" -- colitur's own temporal-cycle convention + (rite_ef/temporal_ef.ml's [named]). Also colitur's own convention, not + an RG citation, exposed for the same reason as {!universal_layer}. See + {!vigil_prefix} for the sanctoral data's own, different convention: a + vigil can arrive named either way, and {!band}/{!disposition} must + recognise both. *) val vigil_suffix : string +(** Slug prefix marking a celebration as a vigil, e.g. "vigil-of-st-lawrence" + -- the sanctoral data's own convention (data/ef/sanctoral.sexp, adopted + verbatim from lectio's naming, per spec §4.4's "slugs are lectionary keys, + not re-derived"). Also colitur's own convention, not an RG citation -- + see {!universal_layer}. Task 10 bootstrapped four real sanctoral vigils + named this way (St Lawrence 08-09, Sts Peter & Paul 06-28, the Assumption + 08-14, the Nativity of St John the Baptist 06-23; a fifth, Christmas, is + suppressed as a duplicate of the temporal cycle's own "ef-nativity-vigil" + -- see data/ef/adjustments.sexp), none of which end in {!vigil_suffix}: + without this prefix also being checked, {!band} would misfile all four at + 16/24 (an ordinary feast of the same rank) instead of RG 91's 21/26, and + RG 33's vigil omission ({!disposition}'s [is_vigil] test, the same + predicate) would never fire for them either -- two rubrics silently + broken for four celebrations, exactly what Task 7's review predicted + when it asked for {!vigil_suffix} to be exposed. *) +val vigil_prefix : string + (** Slug prefixes marking a celebration as one of RG 91 entry 18's three Ember-day sets (Advent, Lent, September -- the Pentecost/Whitsun set is I class and matched by entry 10 before this is ever consulted). Also @@ -153,3 +170,42 @@ val admit : observed:Vocab_ef.rank Precedence.candidate -> (Vocab_ef.rank Precedence.candidate * Precedence.privilege) list -> (Vocab_ef.rank Precedence.candidate * Precedence.privilege) list + +(** The Annunciation's own bootstrapped slug (data/ef/sanctoral.sexp, Task + 10), reused verbatim by {!transfer_target} to recognise RG 96's named + exception. Not an RG citation -- see {!universal_layer} -- exposed so a + future re-bootstrap that renames the slug has somewhere to be caught + other than a silently-wrong transfer target. *) +val annunciation_slug : string + +(** [transfer_target c origin occupant]: RG 96 (docs/research/rules-register + .md §4, "Transfer/translation") -- where an impeded I-class feast, once + {!disposition} has decided it is [Transfer]-disposed, is placed. This + *is* {!Colitur_kernel.Rite.t}.transfer_target; see that field's own + fuller rationale for why the search has to be rite-supplied at all. + + RG 96's own rule: the next following day whose currently-resolved + occupant is not I or II class (read off [Vocab_ef.rank], RG 8's dignity + -- not {!band}'s finer occurrence-table entry, the same distinction + {!admit} draws for RG 111). RG 96's own named exception: the + Annunciation ({!annunciation_slug}) does not search from [origin + 1] at + all -- it starts at the Monday after Low Sunday for [origin]'s own civil + year, searching onward from there only if that day is itself occupied by + a blocking class. + + Total, terminating, and its result is always strictly later than + [origin] -- {!Colitur_kernel.Rite.t}.transfer_target's own obligations, + which {!Colitur_kernel.Calendar}'s placement pass relies on and its own + round guard does not itself enforce (calendar.ml's [place_transfers] + bounds ROUNDS across a whole year, not one call's internal walk). + Terminating by a structural bound on the internal walk (max 400 days, + an engineering ceiling, not an RG citation -- see the .ml), not by an + argument about the real 1962 calendar's own structure, so a rite/data + shape this function has not anticipated fails FINITELY rather than + hanging the caller. Strictly later than [origin]: the ordinary search + starts at [origin + 1] and only ever advances forward from there; the + Annunciation's own starting point is provably later than 25 March for + every representable year (Easter's documented range, register §0) -- + see the .ml for the full argument. *) +val transfer_target : + Vocab_ef.rank Precedence.candidate -> Date.t -> (Date.t -> Vocab_ef.rank Celebration.t) -> Date.t diff --git a/lib/rites/rite_ef/rite_ef.ml b/lib/rites/rite_ef/rite_ef.ml new file mode 100644 index 0000000..7a29421 --- /dev/null +++ b/lib/rites/rite_ef/rite_ef.ml @@ -0,0 +1,24 @@ +(* This module's name matches the library's own name ("rite_ef"), so dune + treats it as the library's top-level module instead of generating one + automatically -- every sibling module this library defines must be + re-exported here explicitly, or external references to e.g. + [Rite_ef.Temporal_ef] (bin/main.ml, every test/ file that opens this + rite) stop resolving. *) +module Vocab_ef = Vocab_ef +module Temporal_ef = Temporal_ef +module Precedence_ef = Precedence_ef + +open Colitur_kernel + +let context : (Vocab_ef.season, Vocab_ef.rank) Rite.t = + { Rite.id = Temporal_ef.id; + vocab = Vocab_ef.vocab; + year_start = Temporal_ef.year_start; + temporal = Temporal_ef.temporal; + anchors = Temporal_ef.anchors; + rules = + { Precedence.band = Precedence_ef.band; + disposition = Precedence_ef.disposition; + admit = Precedence_ef.admit }; + season_runs = Vocab_ef.seasons; + transfer_target = Precedence_ef.transfer_target } diff --git a/lib/rites/rite_ef/rite_ef.mli b/lib/rites/rite_ef/rite_ef.mli new file mode 100644 index 0000000..e2b3e6d --- /dev/null +++ b/lib/rites/rite_ef/rite_ef.mli @@ -0,0 +1,35 @@ +(** The EF (1962) rite module: this library's top-level module (its filename + matches the library's own name "rite_ef", so dune uses it as the + library's entry point directly rather than generating one -- see the + .ml's own comment). Re-exports every sibling module this library + defines, so [Rite_ef.Vocab_ef], [Rite_ef.Temporal_ef] and + [Rite_ef.Precedence_ef] keep resolving exactly as they did before this + module existed. *) + +module Vocab_ef = Vocab_ef +module Temporal_ef = Temporal_ef +module Precedence_ef = Precedence_ef + +(** The EF rite, bundled (design spec's [RITE] signature, realised as a + {!Colitur_kernel.Rite.t} value rather than a functor -- see rite.mli): + - [id], [vocab], [year_start], [temporal], [anchors]: {!Temporal_ef} + unchanged (RG 71-77 seasons, RG 91's named movable days). + - [rules]: {!Precedence_ef}'s three RG 91/92-95/108-111 functions, + wrapped as one {!Colitur_kernel.Precedence.rules} record. + - [season_runs]: {!Vocab_ef.seasons} itself -- the EF liturgical year + visits each of its eight seasons exactly once, in that same order + (Advent-anchored, matching [year_start]), so the expected + run-length-compressed sequence {!Colitur_kernel.Rite.t.season_runs} + wants IS the vocabulary's own canonical list, not a separate one. + - [transfer_target]: {!Precedence_ef.transfer_target}, RG 96 (see that + value's own documentation for the termination and forward-progress + argument {!Colitur_kernel.Rite.t.transfer_target}'s contract requires). + + Deliberately carries no [sanctoral]/[lectionary] fields the way the + original design-doc sketch of [RITE] does: {!Colitur_kernel.Rite.t} (the + type actually shipped, Plan 2) keeps the sanctoral {!Colitur_kernel.Layer.t} + a separate argument to {!Colitur_kernel.Calendar.year}/[day] rather than + embedding it here, so a caller can load data/ef/sanctoral.sexp (plus + data/ef/adjustments.sexp's overlay) however suits it -- bin/main.ml's + [load_ef_layer] is the one this module ships with. *) +val context : (Vocab_ef.season, Vocab_ef.rank) Colitur_kernel.Rite.t diff --git a/test/cli.t b/test/cli.t index feb7c49..77968e6 100644 --- a/test/cli.t +++ b/test/cli.t @@ -17,7 +17,7 @@ A year outside the supported domain is rejected (exit 2): No/garbage arguments give a usage error (exit 2): $ colitur - colitur: usage: colitur easter | colitur temporal + colitur: usage: colitur easter | colitur temporal | colitur day [2] The EF temporal cycle for a year, one line per day: @@ -41,3 +41,68 @@ A year outside the supported domain is rejected (exit 2): $ colitur temporal 1000 colitur: year 1000 out of range 1583..9999 [2] + +The resolved EF calendar for a year (Task 11) -- temporal AND sanctoral, +occurrence and transfers applied: one line per civil-year day, +"YYYY-MM-DD weekday season week slug rank colour [+commemoration-slug]...". + + $ colitur day 2026 | wc -l + 365 + +Easter is the observed day exactly once, and carries no commemoration (an +impeded I class day admits at most one PRIVILEGED commemoration, RG 111, and +nothing outranks Easter to be impeded by it in the first place): + + $ colitur day 2026 | grep -c '^2026-04-05 ' + 1 + $ colitur day 2026 | grep '^2026-04-05 ' + 2026-04-05 sunday paschaltide 1 ef-easter-sunday class-1 white + +Ash Wednesday: I class (RG 91 entry 7), violet, no numbered week (it falls 4 +days before Lent I's own origin -- rite_ef/temporal_ef.ml's [week]): + + $ colitur day 2026 | grep '^2026-02-18 ' + 2026-02-18 wednesday lent - ef-ash-wednesday class-1 violet + +Christmas: I class, white (RG 91 entry 1): + + $ colitur day 2026 | grep '^2026-12-25 ' + 2026-12-25 friday christmastide - ef-nativity class-1 white + +All Souls (2 Nov, RG 91 entry 8) end to end: 2 Nov 2025 is a Sunday (verified +independently -- 1 Jan 2025 is a Wednesday, day-of-year 306, (3+305) mod 7 = +0 = Sunday), so entry 8 yields to it (still an ordinary II-class Sunday, +"sunday" in season time-after-pentecost, colour green -- the week number +itself is not re-asserted here, already covered by test_temporal_ef.ml); RG +95 then transfers All Souls (I class, not a Sunday, not a vigil) and RG 96 +places it on 3 Nov, the next day that is not I or II class: + + $ colitur day 2025 | grep -c 'commemoration-of-all-souls' + 1 + $ colitur day 2025 | grep '^2025-11-02 ' | sed -E 's/ [0-9]+ ef-time-after-pentecost-sunday-[0-9]+ / ef-time-after-pentecost-sunday- /' + 2025-11-02 sunday time-after-pentecost ef-time-after-pentecost-sunday- class-2 green + $ colitur day 2025 | grep '^2025-11-03 ' + 2025-11-03 monday time-after-pentecost 21 commemoration-of-all-souls class-1 black + +(week 21: Pentecost 2025 is 8 June (colitur easter 2025); 8 Jun - 3 Nov is +148 days, floor_div(148, 7) = 21 -- rite_ef/temporal_ef.ml's own [week] +formula, hand-verified before promoting this line, not merely printed and +trusted.) + +All Souls observed directly on 2 Nov in a year where it does not fall on a +Sunday: 2 Nov 2026 is a Monday (1 Jan 2026 is a Thursday, same day-of-year +306 offset, (4+305) mod 7 = 1 = Monday): + + $ colitur day 2026 | grep -c 'commemoration-of-all-souls' + 1 + $ colitur day 2026 | grep '^2026-11-02 ' + 2026-11-02 monday time-after-pentecost 23 commemoration-of-all-souls class-1 black + +(week 23: Pentecost 2026 is 24 May (colitur easter 2026); 24 May - 2 Nov is +162 days, floor_div(162, 7) = 23 -- same formula, same independent check.) + +A year outside the supported domain is rejected (exit 2): + + $ colitur day 1000 + colitur: year 1000 out of range 1583..9999 + [2] diff --git a/test/dune b/test/dune index bb8e474..be24839 100644 --- a/test/dune +++ b/test/dune @@ -6,4 +6,4 @@ (pps ppx_sexp_conv))) (cram - (deps %{bin:colitur})) + (deps %{bin:colitur} ../data/ef/sanctoral.sexp ../data/ef/adjustments.sexp)) diff --git a/test/test_precedence_ef.ml b/test/test_precedence_ef.ml index a95b321..084d708 100644 --- a/test/test_precedence_ef.ml +++ b/test/test_precedence_ef.ml @@ -222,6 +222,22 @@ let cases = ( "26 III-class vigil (non-base layer)", mk 2026 8 10, cand ~origin:P.Sanctoral ~rank:V.Class3 ~layer:"diocese-warsaw" "ef-local-patron-vigil", 26 ); + (* Task 11, issue (a): the sanctoral bootstrap (data/ef/sanctoral.sexp) + names its vigils with lectio's OWN "vigil-of-X" PREFIX convention, not + [PE.vigil_suffix]'s "-vigil" SUFFIX every row above uses -- exactly + the mismatch Task 7's review predicted. These two rows use the real + bootstrapped slugs verbatim (data/ef/sanctoral.sexp: 28 Jun, 9 Aug), + proving [band] recognises the prefix convention too: without it, both + would misfile at 16/24 (an ordinary feast of the same rank) instead + of 21/26. *) + ( "21 II-class vigil via the sanctoral data's own \"vigil-of-X\" prefix", + mk 2026 6 28, + cand ~origin:P.Sanctoral ~rank:V.Class2 ~layer:PE.universal_layer "vigil-of-sts-peter-paul", + 21 ); + ( "26 III-class vigil via the sanctoral data's own \"vigil-of-X\" prefix", + mk 2026 8 9, + cand ~origin:P.Sanctoral ~rank:V.Class3 ~layer:PE.universal_layer "vigil-of-st-lawrence", + 26 ); (* Entry 27 -- register line 352: an otherwise-unoccupied IV-class Saturday. *) ( "27 Office of the BVM on Saturday", off 62, @@ -370,6 +386,21 @@ let disposition_cases = an_ordinary_sunday, cand ~origin:P.Sanctoral ~rank:V.Class3 ~layer:PE.universal_layer "ef-lawrence-vigil", "Commemorate(Ordinary)" ); + (* Task 11, issue (a): [disposition]'s own [is_vigil] check (the RG 33 + omission test) is a SEPARATE call site from [band]'s -- both read the + same private [is_vigil], but each needed its own witness, since a fix + to one call site could in principle miss the other. Real bootstrapped + slug (data/ef/sanctoral.sexp's "vigil-of-the-assumption", 14 Aug), + not a hand-typed one, for the same coupling-safety reason [of_temporal] + rows use real data elsewhere in this file. Before the fix this vigil + was invisible to [is_vigil] entirely, so it would have fallen through + to the ordinary Commemorate branch below instead of Omit -- the exact + failure the task brief describes. *) + ( "RG33 (prefix convention): a \"vigil-of-X\"-named II-class vigil loses \ + to an ordinary Sunday -> Omit", + an_ordinary_sunday, + cand ~origin:P.Sanctoral ~rank:V.Class2 ~layer:PE.universal_layer "vigil-of-the-assumption", + "Omit" ); (* Brief: a Commemoration_only loser is ALWAYS Commemorate -- checked here with a loser that ALSO carries a Class1 rank and a vigil-suffixed slug losing to a Sunday, so this row only passes if the @@ -778,6 +809,94 @@ let test_all_souls_transfers_end_to_end () = Alcotest.(check int) "nothing commemorated" 0 (List.length resolution.P.commemorations); Alcotest.(check int) "nothing omitted" 0 (List.length resolution.P.omitted) +(* Task 11: [PE.transfer_target] -- RG 96 ("the next following day that is + not I or II class") plus its Annunciation exception. [occupant] is a + synthetic callback ({!Colitur_kernel.Rite.t.transfer_target}'s own + [occupant] parameter), not a real [Calendar]-driven one -- the CLI's own + end-to-end proof (colitur day, All Souls landing on 3 Nov 2025 and the + Annunciation landing on 5 Apr 2027, see test/cli.t and the task report) + is what wires this against real data; these rows isolate the search + function itself. *) + +(* [blocked] returns Class1 (blocking) for exactly the listed dates, Class4 + (not blocking) everywhere else -- enough to exercise [is_blocking]'s own + two-way test (RG 96 speaks of I OR II class; Class1 alone is enough to + prove the blocking side, [test_transfer_target_terminates...] below adds + nothing by varying it further). *) +let occupant_blocking_on blocked_dates (d : D.t) : V.rank Cel.t = + let blocking = List.exists (fun bd -> D.compare bd d = 0) blocked_dates in + Cel.make ~slug:(S.of_string_exn "occupant") ~rank:(if blocking then V.Class1 else V.Class4) + ~colour:Col.Green ~layer:"synthetic" () + +let occupant_always_blocking (_ : D.t) : V.rank Cel.t = + Cel.make ~slug:(S.of_string_exn "occupant") ~rank:V.Class1 ~colour:Col.Green ~layer:"synthetic" () + +(* General RG 96 search: two consecutive blocked days past [origin], proving + the search walks past MORE than one ineligible day rather than only + trying [origin + 1] and stopping (the same shape Calendar's own + synthetic fixture pins for the abstraction -- this pins it for the real + EF search function). *) +let test_transfer_target_general_multi_step_search () = + let origin = mk 2026 1 10 in + let occupant = occupant_blocking_on [ mk 2026 1 11; mk 2026 1 12 ] in + let c = cand ~origin:P.Sanctoral ~layer:PE.universal_layer "ef-some-i-class-feast" in + let target = PE.transfer_target c origin occupant in + Alcotest.(check string) "lands on the first day past the blocked run" + "2026-01-13" (D.to_iso8601 target) + +(* RG 96's Annunciation exception: starts the search at the Monday after Low + Sunday, NOT [origin + 1] -- occupant is unconditionally free, so a + general-path implementation would return [origin + 1] (26 March), a date + this test explicitly rules out as well as pinning the real expected one, + so the assertion genuinely discriminates the two starting points rather + than merely checking "some date after origin". *) +let test_transfer_target_annunciation_starts_at_monday_after_low_sunday () = + let origin = mk 2026 3 25 in + let occupant = occupant_blocking_on [] in + let c = cand ~origin:P.Sanctoral ~layer:PE.universal_layer PE.annunciation_slug in + let target = PE.transfer_target c origin occupant in + let monday_after_low_sunday = D.add_days (Comp.gregorian_easter 2026) 8 in + Alcotest.(check string) "lands on the Monday after Low Sunday (Easter + 8)" + (D.to_iso8601 monday_after_low_sunday) (D.to_iso8601 target); + Alcotest.(check bool) "NOT the general path's origin + 1 (discriminates the branch)" true + (D.compare target (D.add_days origin 1) <> 0) + +(* RG 96's own qualifier on the exception -- "searching onward from there + only if that day is itself blocked" (rite.mli) -- is [search_from]'s + ORDINARY behaviour, not a second mechanism: block the Monday after Low + Sunday itself and confirm the search continues exactly one more day. *) +let test_transfer_target_annunciation_searches_onward_if_blocked () = + let origin = mk 2026 3 25 in + let monday_after_low_sunday = D.add_days (Comp.gregorian_easter 2026) 8 in + let occupant = occupant_blocking_on [ monday_after_low_sunday ] in + let c = cand ~origin:P.Sanctoral ~layer:PE.universal_layer PE.annunciation_slug in + let target = PE.transfer_target c origin occupant in + Alcotest.(check string) "searches onward one more day when that Monday is itself blocked" + (D.to_iso8601 (D.add_days monday_after_low_sunday 1)) (D.to_iso8601 target) + +(* rite.mli's own obligations on [transfer_target] (Task 11 brief): the call + must TERMINATE and its result must be STRICTLY AFTER [origin], even for a + rite/data shape this function cannot have anticipated -- an occupant that + reports every single day as blocking, forever. Calendar's own round guard + (max_transfer_rounds) does not cover this: it bounds ROUNDS across a + whole year, not the internal walk one call to this function makes (see + precedence_ef.ml's own comment on [search_from] and [max_search_days]). + Deliberately NOT pinning the exact returned date against the private + [max_search_days] constant -- that would coalesce a behavioural contract + (terminates, makes forward progress) with an internal tuning value this + function is free to change; a generous, test-owned ceiling (1000 days, + comfortably past any realistic bound) is enough to prove termination is + genuine and not merely "didn't hang during this particular run". *) +let test_transfer_target_terminates_under_pathological_occupant () = + let origin = mk 2026 1 1 in + let c = cand ~origin:P.Sanctoral ~layer:PE.universal_layer "ef-pathological-case" in + let target = PE.transfer_target c origin occupant_always_blocking in + Alcotest.(check bool) "strictly after origin" true (D.compare target origin > 0); + Alcotest.(check bool) + "terminates within a generous bound (proves the internal search is bounded, not merely lucky)" + true + (D.compare target (D.add_days origin 1000) <= 0) + let suite = ( "Precedence_ef", List.map @@ -819,4 +938,13 @@ let suite = test_privileged_lent_feria_admitted_end_to_end; Alcotest.test_case "II-class Sunday override: RG109(b) witness admitted over an ordinary saint, end-to-end" - `Quick test_ii_class_sunday_privileged_witness_admitted_end_to_end ] ) + `Quick test_ii_class_sunday_privileged_witness_admitted_end_to_end; + Alcotest.test_case "transfer_target: general RG96 search walks past more than one blocked day" + `Quick test_transfer_target_general_multi_step_search; + Alcotest.test_case "transfer_target: Annunciation exception starts at Monday after Low Sunday" + `Quick test_transfer_target_annunciation_starts_at_monday_after_low_sunday; + Alcotest.test_case + "transfer_target: Annunciation exception searches onward if that Monday is blocked" `Quick + test_transfer_target_annunciation_searches_onward_if_blocked; + Alcotest.test_case "transfer_target: terminates and stays forward under a pathological occupant" + `Quick test_transfer_target_terminates_under_pathological_occupant ] ) -- cgit v1.3 From 633306c8a5ac1854f30749f498498104ebc84edc Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Wed, 12 Aug 2026 02:12:03 +0200 Subject: kernel(validate): resolution invariants Widen Validate.run to take the rite's sanctoral layer alongside the rite itself (Calendar.year needs both), and add five checks over the fully resolved liturgical year, on top of the existing temporal-only pass: - observed: a day's observed celebration never also appears among that same day's own commemorations/omissions. - lost: no sanctoral entry is silently dropped. Per slug, the number of times it is actually sighted (observed + commemorations + omitted, summed over the year) must never fall below the number of times its own Date_spec resolves within the year's span -- also fires if resolving the year raises at all, the most total form of loss. - duplicated: the same per-slug count must never exceed the number of Date_spec resolutions either. Deliberately NOT "no slug appears twice": a fixed date can legitimately resolve twice in the ~20% of liturgical years whose 371-day span reaches it on both ends (30 November/St Andrew is the worked example in validate.mli). - unconverged: no day's omitted reason indicates Calendar's placement pass hit its round guard before reaching a fixed point. - admission: the rite's own rules.admit is a fixed point on what it already admitted -- the rite-agnostic form of "the admission limit was not exceeded" available without embedding a rite's own numeric caps (RG 111's, for EF) into kernel code. Each check has a dedicated negative fixture in the synthetic rite (test_validate.ml), hand-traced against Calendar's actual resolution mechanics before writing the assertion, and verified to fail for the right reason against the code before this change. One pair (unconverged/duplicated) is not fully independent: hitting the round guard genuinely also trips duplicated, a real consequence of Calendar's own accounting once a candidate is simultaneously sighted at its permanent natural date and wherever the last placement round left it -- documented in guard_rules's own comment, not papered over. test_validate.ml's ef_rite/run now use the real Rite_ef.context and the real bootstrapped data/ef layer (Precedence_ef and the sanctoral bootstrap did not exist when this scaffolding was first written) rather than the earlier placeholder rules. Validate is clean across the whole 1583..9999 domain against real EF data except the one already-documented year-9999 truncation case (test_year_9999_does_not_raise). --- lib/kernel/validate.ml | 132 +++++++++++++++++++- lib/kernel/validate.mli | 46 ++++++- test/test_validate.ml | 311 ++++++++++++++++++++++++++++++++++++++++++++---- 3 files changed, 460 insertions(+), 29 deletions(-) (limited to 'lib/kernel') diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index c6501a9..d8de31b 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -20,7 +20,20 @@ let has_duplicate strings = let rec go = function a :: (b :: _ as rest) -> a = b || go rest | _ -> false in go sorted -let run (rite : ('s, 'r) Rite.t) ~year = +(* Task 12's "unconverged" check has no structural signal to key off -- + Calendar's placement pass records its round-guard reason as a plain + string in [Liturgical_day.omitted] (calendar.ml's own [unconverged_reason], + not exposed as a public constant), and [Liturgical_day.omitted]'s own doc + comment says exactly this check is meant to read it. A short, distinctive + substring rather than the full literal keeps the coupling to calendar.ml's + exact wording as loose as it can be while still being unambiguous: nothing + else this kernel emits into [omitted] talks about "converging". *) +let contains_substring s ~needle = + let ls = String.length s and ln = String.length needle in + let rec at i = i + ln <= ls && (String.sub s i ln = needle || at (i + 1)) in + ln = 0 || at 0 + +let run (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) ~year = let vocab = rite.Rite.vocab in let year_start = rite.Rite.year_start in let temporal = rite.Rite.temporal in @@ -164,4 +177,121 @@ let run (rite : ('s, 'r) Rite.t) ~year = if actual <> expected_slug then fail date "anchor" (Printf.sprintf "expected slug %S, got %S" expected_slug actual)) anchor_pairs; + (* Resolution invariants (Task 12): everything above only ever asked + [rite.temporal] for a date's office in isolation. From here on the + LITURGICAL YEAR IS ACTUALLY RESOLVED against [layer] -- occurrence, + transfer placement, commemorations, the works (spec §2.4) -- and the + result checked for five further properties a temporal-only pass cannot + see at all. [days] (the walk built above) is reused rather than + recomputed: it names exactly the same [start, stop] span + {!Calendar.year} resolves for this [year]. *) + (match Calendar.year rite layer year with + | exception exn -> + (* The kernel contract forbids [run] itself from ever raising on + in-range input, and an exception escaping resolution is the most + total form of "silently lost" there is: nothing about this year's + sanctoral entries could be verified as accounted for at all. *) + fail start "lost" + (Printf.sprintf "resolving the year raised (%s); nothing could be verified as accounted for" + (Printexc.to_string exn)) + | resolved -> + let idx = Layer.index_by_date layer in + let bump tbl slug = Hashtbl.replace tbl slug (1 + (try Hashtbl.find tbl slug with Not_found -> 0)) in + (* Expected: how many times each layer entry's own Date_spec resolves + within [start, stop]. Walking dates and querying [Layer.on_date] + (rather than resolving each entry's Date_spec against candidate + civil years directly) is what naturally counts a fixed late- + November date TWICE in the ~20% of liturgical years whose 371-day + span reaches it on both ends -- see validate.mli's own note on 30 + November / St Andrew. *) + let expected : (string, int) Hashtbl.t = Hashtbl.create 64 in + List.iter + (fun date -> + Layer.on_date idx ~month:(Date.month date) ~day:(Date.day date) + |> List.iter (fun (e : 'r Layer.entry) -> + bump expected (Slug.to_string e.Layer.cel.Celebration.slug))) + days; + (* Actual: how many times each slug is actually sighted across the + resolved year. Deliberately [observed] + [commemorations] + + [omitted] only, NOT [transferred_out]: a successfully transferred + celebration is already counted once, via [observed] (+ + [transferred_in]) on the day it lands; also counting + [transferred_out] at the day it left would double-book every clean + transfer, which is exactly what this check exists to catch, not + cause. *) + let actual : (string, int) Hashtbl.t = Hashtbl.create 64 in + let bump_cel tbl (c : 'r Celebration.t) = bump tbl (Slug.to_string c.Celebration.slug) in + Array.iter + (fun (d : ('s, 'r) Liturgical_day.t) -> + bump_cel actual d.Liturgical_day.observed; + List.iter (fun (c, _) -> bump_cel actual c) d.Liturgical_day.commemorations; + List.iter (fun (c, _) -> bump_cel actual c) d.Liturgical_day.omitted) + resolved; + Hashtbl.fold (fun slug exp acc -> (slug, exp) :: acc) expected [] + |> List.sort compare (* stable failure order: Hashtbl.iter's own order is hash-seed-dependent *) + |> List.iter (fun (slug, exp) -> + let act = try Hashtbl.find actual slug with Not_found -> 0 in + if act < exp then + fail start "lost" + (Printf.sprintf "%s: sighted %d time(s) this year, but its own Date_spec resolves %d" + slug act exp) + else if act > exp then + fail start "duplicated" + (Printf.sprintf "%s: sighted %d time(s) this year, but its own Date_spec resolves only %d" + slug act exp)); + Array.iter + (fun (d : ('s, 'r) Liturgical_day.t) -> + let date = d.Liturgical_day.date in + let observed_slug = Slug.to_string d.Liturgical_day.observed.Celebration.slug in + let has_slug (c, _) = Slug.to_string c.Celebration.slug = observed_slug in + (* "observed": the day's own winner must not ALSO be listed as one + of its own losers -- see validate.mli's own note on why this is + reachable (two distinct layer entries sharing a slug, one + transferred onto the other's natural date, the transferred one + winning) despite {!Precedence.resolve}'s fold never letting the + SAME candidate value appear as both winner and loser. *) + if List.exists has_slug d.Liturgical_day.commemorations + || List.exists has_slug d.Liturgical_day.omitted + then + fail date "observed" + (Printf.sprintf + "%s is this day's observed celebration and also appears among its own \ + commemorations/omissions" + observed_slug); + (* "unconverged": see [contains_substring]'s own comment above. *) + if + List.exists + (fun (_, reason) -> contains_substring reason ~needle:"did not converge") + d.Liturgical_day.omitted + then + fail date "unconverged" + "transfer placement did not reach a fixed point within the round guard (RG 96-98)"; + (* "admission": re-offer this day's own admitted commemorations + back to [rite.rules.admit] and require the exact same set back. + [origin] is reconstructed as [Sanctoral] uniformly: + {!Liturgical_day.t} does not retain a commemoration's original + origin, and the real EF [admit] (precedence_ef.ml) reads only + rank and slug from a candidate, never [origin], so this + reconstruction is exact for it; documented in validate.mli as + the one place a rite whose [admit] DOES consult [origin] could + see a false negative from this check. *) + let observed_candidate : 'r Precedence.candidate = + { Precedence.cel = d.Liturgical_day.observed; origin = Precedence.Sanctoral } + in + let as_candidates comms = + List.map (fun (c, p) -> ({ Precedence.cel = c; origin = Precedence.Sanctoral }, p)) comms + in + let offered = as_candidates d.Liturgical_day.commemorations in + let readmitted = rite.Rite.rules.Precedence.admit ~observed:observed_candidate offered in + let norm l = + List.map (fun (c, p) -> (Slug.to_string c.Precedence.cel.Celebration.slug, p)) l + |> List.sort compare + in + if norm readmitted <> norm offered then + fail date "admission" + (Printf.sprintf + "admit is not a fixed point on this day's own commemorations: re-offering %d \ + admitted %d back" + (List.length offered) (List.length readmitted))) + resolved); List.rev !failures diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli index d281f9a..511c78f 100644 --- a/lib/kernel/validate.mli +++ b/lib/kernel/validate.mli @@ -5,8 +5,9 @@ type failure = { year : int; date : string; check : string; detail : string } val failure_to_string : failure -> string -(** [run rite ~year] returns every invariant violation in the liturgical year - opening in civil year [year]. An empty list means the year is clean. +(** [run rite layer ~year] returns every invariant violation in the + liturgical year opening in civil year [year]. An empty list means the + year is clean. [rite.Rite.anchors y] is the rite's own independent restatement of its fixed and Easter-derived named days for civil year [y], as (expected @@ -21,8 +22,47 @@ val failure_to_string : failure -> string have one season appear in two separate runs (the modern form's Ordinary Time does), so the two are not necessarily the same list. + [layer] is resolved against [rite] via {!Calendar.year} (spec §2.4's + occurrence/transfer/commemoration pass), and the resulting fully-resolved + liturgical year is checked for five further invariants a temporal-only + pass cannot see (Task 12), each its own ["check"] label: + - ["observed"]: a day's [observed] celebration is never ALSO listed among + that same day's [commemorations] or [omitted] -- a day reports one + winner, not a winner that also lost to itself. + - ["lost"]: no sanctoral entry is silently dropped. Per slug, the number + of times it is actually sighted ([observed] + [commemorations] + + [omitted], summed over the whole year -- NOT [transferred_out], which + would double-count a successfully placed transfer against its own + arrival) must never fall below the number of times its own + {!Date_spec} resolves within the year's span (an entry with two + occurrences, e.g. 30 November in the nine liturgical years where the + 371-day span reaches it twice, must be sighted twice, not once). Also + fires if resolving the year raises at all -- an escaping exception is + the most total form of silent loss, and the kernel contract forbids + [run] itself from propagating it. + - ["duplicated"]: the same per-slug count must never EXCEED the number of + {!Date_spec} resolutions either. Deliberately NOT "no slug appears + twice in the year" -- a fixed date can legitimately resolve twice, per + ["lost"] above -- it is "resolutions and sightings agree", the property + that actually distinguishes a transfer that moved from one that + duplicated. + - ["unconverged"]: no day's [omitted] carries the reason {!Calendar}'s + placement pass records when its round guard (calendar.ml's + [max_transfer_rounds]) is hit before every deferred candidate reaches a + fixed point. + - ["admission"]: the rite's own [rules.admit] is a fixed point on what it + already admitted -- re-offering a day's [commemorations] back to + [admit] (reconstructed with {!Precedence.Sanctoral} origin; the real EF + admit reads only rank and slug, never origin, so this reconstruction is + exact for it) must return exactly that same set. A cap-enforcing + selector that is not idempotent on its own output has, by definition, + admitted something its own rule would not admit if asked again -- the + rite-agnostic form of "the admission limit was not exceeded" available + without embedding a rite's specific numeric caps (RG 111's, for EF) + into kernel code. + Total over the whole 1583..9999 domain, including [year] = 9999: the liturgical year opening there continues into out-of-domain civil year 10000, so the walk is clamped to 31 December 9999 and the checks run against that truncated final year rather than raising. *) -val run : ('s, 'r) Rite.t -> year:int -> failure list +val run : ('s, 'r) Rite.t -> 'r Layer.t -> year:int -> failure list diff --git a/test/test_validate.ml b/test/test_validate.ml index df8c99c..b2d4f34 100644 --- a/test/test_validate.ml +++ b/test/test_validate.ml @@ -1,24 +1,40 @@ module Val = Colitur_kernel.Validate module Rite = Colitur_kernel.Rite module P = Colitur_kernel.Precedence +module Layer = Colitur_kernel.Layer +module Overlay = Colitur_kernel.Overlay 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] 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); - admit = (fun ~observed:_ _ -> []) } - -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; - transfer_target = (fun _ origin _ -> origin) } - -let run year = Val.run ef_rite ~year +(* Task 12 widens Validate.run to take a resolved layer -- Precedence_ef and + Calendar (Tasks 5-11) now exist, so the REAL EF rite (Rite_ef.context) and + its REAL bootstrapped data replace the earlier placeholder rules/layer-less + Rite.t this module used before Plan 3's resolution engine was built. + Relative to this test's own build directory (_build/default/test/), same + convention test_rite_ef.ml already uses -- test/dune declares both as deps + of the (test ...) stanza. *) +let sanctoral_path = "../data/ef/sanctoral.sexp" +let adjustments_path = "../data/ef/adjustments.sexp" + +(* Loaded once at module init, not per call: [run] below is called by every + test and by the 200-sample property, and Calendar.year's own resolution + cost already dominates -- there is no reason to also re-parse a 322-entry + sexp file on every one of those calls. *) +let real_ef_layer = + match Layer.load V.rank_of_sexp sanctoral_path with + | Error e -> failwith (Printf.sprintf "%s: failed to load: %s" sanctoral_path e) + | Ok layer -> ( + match Overlay.load V.rank_of_sexp adjustments_path with + | Error e -> failwith (Printf.sprintf "%s: failed to load: %s" adjustments_path e) + | Ok overlay -> + let layer, diagnostics = Overlay.apply layer overlay in + if diagnostics <> [] then + failwith + (Printf.sprintf "unexpected overlay diagnostics: %s" + (String.concat "; " (List.map Overlay.diagnostic_to_string diagnostics))); + layer) + +let run year = Val.run Rite_ef.context real_ef_layer ~year let check_year year = match run year with @@ -94,6 +110,8 @@ module Synthetic = struct module Temporal = Colitur_kernel.Temporal module P = Colitur_kernel.Precedence module Rite = Colitur_kernel.Rite + module Layer = Colitur_kernel.Layer + module Date_spec = Colitur_kernel.Date_spec type season = A | B type rank = R1 | R2 @@ -122,8 +140,12 @@ module Synthetic = struct let vocab_collapsed_ranks = { vocab with Vocab.rank_to_string = (fun _ -> "same") } let vocab_collapsed_seasons = { vocab with Vocab.season_to_string = (fun _ -> "same") } - (* Precedence_ef doesn't exist yet (Tasks 7-11); Validate.run never reads - [rules], so a placeholder is enough to assemble a well-typed Rite.t. *) + (* The placeholder ruleset every TEMPORAL-only fixture below still uses: + paired with the default empty [layer] (see [rite] below), there is never + a sanctoral candidate for these three functions to be called against, so + what they return is moot for those tests -- only the Task 12 resolution + fixtures further down override [rules] (and supply a non-empty + [layer]), each with its own small, deliberately-shaped ruleset. *) let rules : (season, rank) P.rules = { P.band = (fun _ _ -> 0); disposition = (fun ~winner:_ ~loser:_ -> P.Omit); @@ -173,14 +195,25 @@ module Synthetic = struct this synthetic rite too, not only in EF. *) let anchors _y = [ (Slug.to_string (good target).Temporal.office.Cel.slug, target) ] - let rite ?(vocab = vocab) ?(anchors = fun _ -> []) ?(season_runs = [ A; B ]) temporal - : (season, rank) Rite.t = + (* Task 12: [rite] now also takes [rules]/[transfer_target] (defaulting to + the placeholder above and to "stand still", respectively -- harmless + defaults against the default empty [layer], since nothing ever contests + the temporal office there) so the resolution fixtures further down can + override them without duplicating every other field. *) + let rite ?(vocab = vocab) ?(anchors = fun _ -> []) ?(season_runs = [ A; B ]) ?(rules = rules) + ?(transfer_target = fun _ origin _ -> origin) temporal : (season, rank) Rite.t = { 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) } + transfer_target } - let run ?vocab ?anchors ?season_runs temporal = - Val.run (rite ?vocab ?anchors ?season_runs temporal) ~year:2026 + (* Empty by default: every check built before Task 12 exercises the + TEMPORAL-only pass, where an empty layer is exactly the fixture that + leaves it unable to affect anything ([Precedence.resolve] against no + sanctoral candidates always just observes the temporal office + unchallenged). Task 12's own resolution fixtures pass their own. *) + let empty_layer = Layer.empty ~id:"synthetic-empty" ~name:"empty" + + let run ?vocab ?anchors ?season_runs ?rules ?transfer_target ?(layer = empty_layer) temporal = + Val.run (rite ?vocab ?anchors ?season_runs ?rules ?transfer_target temporal) layer ~year:2026 let has_check check (fs : Val.failure list) = List.exists (fun f -> f.Val.check = check) fs @@ -210,6 +243,180 @@ module Synthetic = struct let rite_with_two_runs : (season, rank) Rite.t = rite ~season_runs:[ A; B; A; B ] two_run_temporal + + (* ---- Task 12: resolution-level fixtures ---- + + Everything above only ever drives the TEMPORAL-only pass: [run]'s + default [layer] is empty, so [Precedence.resolve] never has a sanctoral + candidate to contest against the temporal office, and [rules]/ + [transfer_target] are never meaningfully exercised. These five fixtures + instead give [Calendar.year] real work -- a non-empty [layer] plus a + small, deliberately-shaped [rules] (and, for two of them, + [transfer_target]) -- each built so its OWN check label fires. Four of + the five fire in clean isolation (the other four Task 12 labels stay + silent); the fifth (["unconverged"]) genuinely also fires + ["duplicated"] alongside it, a real consequence of Calendar's own round- + guard accounting, not a fixture design flaw -- see guard_rules's own + comment. Every fixture's isolation (or lack of it) was verified by + hand-tracing [Calendar]'s resolution mechanics BEFORE writing its + assertion (see the task report), not inferred from what the assertion + happens to require -- the tests below check that trace against the + actual engine output, one fixture at a time. [good] is reused, + unchanged, as every fixture's [temporal]: only [rules]/[layer]/ + [transfer_target] vary, so the temporal-only checks (already proven + clean against [good] by [test_synthetic_baseline_is_clean]) cannot be + what fires here. *) + + let mk_entry ~month ~day ~slug ~rank = + { Layer.date = (match Date_spec.fixed ~month ~day with Ok d -> d | Error e -> failwith e); + cel = Cel.make ~slug:(Slug.of_string_exn slug) ~rank ~colour:Colour.White + ~layer:"synthetic-sanctoral" () } + + let task12_checks = [ "observed"; "lost"; "duplicated"; "unconverged"; "admission" ] + + (* The Task-12-owned subset of a failure list's own check labels, as a + sorted, de-duplicated set -- what each isolation assertion below + compares against, so a fixture that (by mistake) also trips an + unrelated Task-12 check shows up as a wrong set, not a silently-passing + [has_check]. *) + let fired_task12_checks (fs : Val.failure list) = + List.filter_map (fun f -> if List.mem f.Val.check task12_checks then Some f.Val.check else None) fs + |> List.sort_uniq compare + + (* "duplicated": a single ordinary sanctoral entry, always losing to the + temporal office (band: Temporal 0 < Sanctoral 10, unconditionally) and + always Commemorate-disposed. [admit]'s bug is exactly the shape + precedence_ef.mli's own [admit] contract warns against ("a value taken + unchanged from comms, never rebuilt"): it REBUILDS every admitted pair + via a record update, allocating a fresh, structurally-identical-but- + physically-distinct candidate. Precedence.resolve's own [dropped] + computation tells an admitted candidate from a dropped one by PHYSICAL + equality, so the rebuild defeats it -- the one candidate ends up counted + as both admitted (in [commemorations]) and dropped (in [omitted], + "admission limit reached"): two sightings for one Date_spec + resolution. *) + let dup_entry = mk_entry ~month:5 ~day:5 ~slug:"dup-target" ~rank:R2 + let dup_layer = Layer.of_entries ~id:"dup" ~name:"dup" [ dup_entry ] + + let dup_rules : (season, rank) P.rules = + { P.band = (fun _ c -> match c.P.origin with P.Temporal -> 0 | P.Sanctoral -> 10); + disposition = (fun ~winner:_ ~loser:_ -> P.Commemorate P.Ordinary); + admit = (fun ~observed:_ cs -> List.map (fun (c, p) -> ({ c with P.origin = c.P.origin }, p)) cs) } + + (* "unconverged": two entries collide on one date (6 June), both beating + the temporal office and tied with each other, so slug decides: + "guard-aaa" wins the day outright every time, "guard-zzz" is always the + loser there and always Transfer-disposed. Paired with a + [transfer_target] that always answers with the impeded day itself -- + never strictly forward -- this is the exact non-terminating shape + test_calendar.ml's own + [test_transfer_guard_records_failure_instead_of_looping] proves hits + Calendar's round guard: "guard-zzz", re-injected into 6 June every + round, can never win it (it always loses the tie to the natural + "guard-aaa" copy already sitting there), so [deferred] never empties. + + GENUINE FINDING (see the task report): this ALSO fires "duplicated", not + "unconverged" alone. Once the guard is hit, [build_day]'s final resolve + at 6 June sees "guard-zzz" TWICE -- once as the permanent natural entry + (which never stops losing there) and once as whatever the last round's + [injected] state still holds for it -- and [unresolved] is evaluated per + CANDIDATE OBJECT, not per slug, so BOTH copies land in [omitted] with + the unconverged reason. Nothing is lost (both copies carry a recorded + reason), but the slug is sighted twice against one Date_spec resolution, + which is exactly what "duplicated" is for. The same double-recording is + latent in test_calendar.ml's own guard fixture too (day_winner/eclipsed + at 20 Dec, structurally identical) -- untested there only because that + test uses [List.exists], not a count. Calendar's round guard is + documented as "nothing in the 1962 calendar is expected to trigger" + (calendar.ml), so this is a latent accounting quirk in an unreachable + path, not a live bug, and calendar.ml is out of this task's file list -- + reported, not fixed here. *) + let guard_winner_entry = mk_entry ~month:6 ~day:6 ~slug:"guard-aaa" ~rank:R1 + let guard_loser_entry = mk_entry ~month:6 ~day:6 ~slug:"guard-zzz" ~rank:R1 + let guard_layer = Layer.of_entries ~id:"guard" ~name:"guard" [ guard_winner_entry; guard_loser_entry ] + + let guard_rules : (season, rank) P.rules = + { P.band = (fun _ c -> match c.P.origin with P.Temporal -> 50 | P.Sanctoral -> 10); + disposition = + (fun ~winner:_ ~loser -> + match loser.P.cel.Cel.rank with R1 -> P.Transfer | R2 -> P.Commemorate P.Ordinary); + admit = (fun ~observed:_ cs -> cs) } + + let guard_transfer_target (_ : rank P.candidate) (origin : D.t) (_ : D.t -> rank Cel.t) = origin + + (* "admission": three entries collide on one date (9 September), all + losing to the temporal office (band: Temporal 0 < Sanctoral 10) and all + Commemorate-disposed -- a genuine 3-candidate offer to [admit]. The bug: + cap 2 when the offer's length is ODD, cap 1 when EVEN -- a length-keyed + rule with no liturgical meaning, chosen as the simplest function that is + NOT idempotent on its own output (offer 3, admit 2; re-offer those same + 2, admit only 1) while staying idempotent -- and so invisible -- on + every OTHER shape this suite exercises (never offered exactly 2 or 3 + candidates elsewhere), including its own clean 3-candidate day. *) + let adm_a_entry = mk_entry ~month:9 ~day:9 ~slug:"adm-a" ~rank:R2 + let adm_b_entry = mk_entry ~month:9 ~day:9 ~slug:"adm-b" ~rank:R2 + let adm_c_entry = mk_entry ~month:9 ~day:9 ~slug:"adm-c" ~rank:R2 + let adm_layer = Layer.of_entries ~id:"adm" ~name:"adm" [ adm_a_entry; adm_b_entry; adm_c_entry ] + + let adm_compare_slug (c1, _) (c2, _) = Slug.compare c1.P.cel.Cel.slug c2.P.cel.Cel.slug + + let rec adm_take n = function + | [] -> [] + | x :: xs -> if n <= 0 then [] else x :: adm_take (n - 1) xs + + let adm_rules : (season, rank) P.rules = + { P.band = (fun _ c -> match c.P.origin with P.Temporal -> 0 | P.Sanctoral -> 10); + disposition = (fun ~winner:_ ~loser:_ -> P.Commemorate P.Ordinary); + admit = + (fun ~observed:_ cs -> + let sorted = List.stable_sort adm_compare_slug cs in + if List.length sorted mod 2 = 1 then adm_take 2 sorted else adm_take 1 sorted) } + + (* "observed": two DIFFERENT layer entries sharing one slug -- a realistic + data mistake (a renamed or duplicated entry), not prevented by + [Layer.t]'s own type. [collide_a] (1 Feb, rank R1) always loses on its + OWN date: [band] makes the temporal office win there specifically (5, + beating R1's 10) and lose everywhere else (50), so [collide_a] is always + Transfer-disposed at 1 Feb. Its constant [transfer_target] sends it to + 10 Feb -- [collide_b]'s own home date -- where [collide_a]'s rank R1 + (band 10) now beats both the temporal office (50, since the date is no + longer 1 Feb) and [collide_b]'s own rank R2 (band 90): the ARRIVING + [collide_a] wins 10 Feb outright, and [collide_b] -- same slug as the + new winner -- is Commemorate-disposed (R2) right alongside it. One day + ends up reporting the same slug as both its observed celebration and one + of its own commemorations. *) + let collide_d1 = match D.make ~year:2026 ~month:2 ~day:1 with Ok d -> d | Error e -> failwith e + let collide_a_entry = mk_entry ~month:2 ~day:1 ~slug:"collide-x" ~rank:R1 + let collide_b_entry = mk_entry ~month:2 ~day:10 ~slug:"collide-x" ~rank:R2 + let collide_layer = Layer.of_entries ~id:"collide" ~name:"collide" [ collide_a_entry; collide_b_entry ] + + let collide_rules : (season, rank) P.rules = + { P.band = + (fun ctx c -> + match c.P.origin with + | P.Temporal -> if D.compare ctx.P.date collide_d1 = 0 then 5 else 50 + | P.Sanctoral -> ( match c.P.cel.Cel.rank with R1 -> 10 | R2 -> 90)); + disposition = + (fun ~winner:_ ~loser -> + match loser.P.cel.Cel.rank with R1 -> P.Transfer | R2 -> P.Commemorate P.Ordinary); + admit = (fun ~observed:_ cs -> cs) } + + let collide_d2 = match D.make ~year:2026 ~month:2 ~day:10 with Ok d -> d | Error e -> failwith e + let collide_transfer_target (_ : rank P.candidate) (_ : D.t) (_ : D.t -> rank Cel.t) = collide_d2 + + (* A genuinely resolved, well-behaved day (one ordinary sanctoral entry, + cleanly losing and commemorated, nothing transferred) -- proving the + five checks stay silent against REAL resolution machinery, not merely + against the default empty [layer] every fixture above this section + uses. Without this, "no check fires" would only ever have been shown + for a layer with nothing in it. *) + let clean_sanctoral_entry = mk_entry ~month:8 ~day:8 ~slug:"clean-saint" ~rank:R2 + let clean_sanctoral_layer = Layer.of_entries ~id:"clean" ~name:"clean" [ clean_sanctoral_entry ] + + let clean_sanctoral_rules : (season, rank) P.rules = + { P.band = (fun _ c -> match c.P.origin with P.Temporal -> 0 | P.Sanctoral -> 10); + disposition = (fun ~winner:_ ~loser:_ -> P.Commemorate P.Ordinary); + admit = (fun ~observed:_ cs -> cs) } end open Synthetic @@ -227,7 +434,7 @@ let test_synthetic_baseline_is_clean () = let test_two_run_season_is_accepted () = let r = Synthetic.rite_with_two_runs in Alcotest.(check (list string)) "no failures" [] - (List.map Val.failure_to_string (Val.run r ~year:2026)) + (List.map Val.failure_to_string (Val.run r Synthetic.empty_layer ~year:2026)) let test_coverage_fires () = let temporal d = if D.compare d target = 0 then failwith "boom" else good d in @@ -332,6 +539,53 @@ let test_vocab_season_injectivity_fires () = Alcotest.(check bool) "vocab check fires when season_to_string collapses two seasons to one string" true (has_check "vocab" (run ~vocab:vocab_collapsed_seasons good)) +(* ---- Task 12: resolution invariants ---- + + Each test below asserts that exactly one of the five new check labels + fires for its own dedicated fixture (Synthetic's own comments carry the + hand-traced mechanics) -- not merely "at least this one", so a fixture + that turns out to also trip an unrelated Task 12 check would fail loudly + here rather than reading as accidental corroboration. *) + +let test_lost_fires_on_resolution_exception () = + (* Reuses [test_coverage_fires]'s own broken [temporal]: [Calendar.year] + calls [rite.temporal] with no exception guard of its own (unlike the + temporal-only pass above, which wraps every call), so the same raise + that trips "coverage" also makes resolution itself raise -- the most + total form of "silently lost" there is, per validate.mli. *) + let temporal d = if D.compare d target = 0 then failwith "boom" else good d in + Alcotest.(check (list string)) "only the lost check fires" [ "lost" ] (fired_task12_checks (run temporal)) + +let test_duplicated_fires () = + Alcotest.(check (list string)) "only the duplicated check fires" [ "duplicated" ] + (fired_task12_checks (run ~layer:dup_layer ~rules:dup_rules good)) + +let test_unconverged_fires () = + (* Also asserts "duplicated" fires alongside it -- see guard_rules's own + comment for why that is the genuine, hand-verified consequence of + hitting the round guard here, not an isolation failure. *) + Alcotest.(check (list string)) "unconverged fires, and duplicated alongside it" + [ "duplicated"; "unconverged" ] + (fired_task12_checks + (run ~layer:guard_layer ~rules:guard_rules ~transfer_target:guard_transfer_target good)) + +let test_admission_fires () = + Alcotest.(check (list string)) "only the admission check fires" [ "admission" ] + (fired_task12_checks (run ~layer:adm_layer ~rules:adm_rules good)) + +let test_observed_fires () = + Alcotest.(check (list string)) "only the observed check fires" [ "observed" ] + (fired_task12_checks + (run ~layer:collide_layer ~rules:collide_rules ~transfer_target:collide_transfer_target good)) + +(* The positive counterpart: a genuinely resolved, well-behaved day (real + sanctoral entry, real contest, real commemoration) must report none of the + five checks -- proven against actual resolution machinery, not only + against every OTHER fixture's default empty layer. *) +let test_resolution_checks_clean_on_a_well_behaved_layer () = + Alcotest.(check (list string)) "none of the five checks fire" [] + (fired_task12_checks (run ~layer:clean_sanctoral_layer ~rules:clean_sanctoral_rules good)) + let suite = ( "Validate", [ Alcotest.test_case "landmark years" `Quick test_landmark_years; @@ -349,5 +603,12 @@ let suite = Alcotest.test_case "anchor clean" `Quick test_anchor_clean; Alcotest.test_case "anchor fires" `Quick test_anchor_fires; Alcotest.test_case "vocab rank injectivity fires" `Quick test_vocab_rank_injectivity_fires; - Alcotest.test_case "vocab season injectivity fires" `Quick test_vocab_season_injectivity_fires ] + Alcotest.test_case "vocab season injectivity fires" `Quick test_vocab_season_injectivity_fires; + Alcotest.test_case "lost fires on resolution exception" `Quick test_lost_fires_on_resolution_exception; + Alcotest.test_case "duplicated fires" `Quick test_duplicated_fires; + Alcotest.test_case "unconverged fires" `Quick test_unconverged_fires; + Alcotest.test_case "admission fires" `Quick test_admission_fires; + Alcotest.test_case "observed fires" `Quick test_observed_fires; + Alcotest.test_case "resolution checks clean on a well-behaved layer" `Quick + test_resolution_checks_clean_on_a_well_behaved_layer ] @ List.map QCheck_alcotest.to_alcotest [ prop_invariants ] ) -- cgit v1.3 From 4235a6aa18b815c5457a7eb97fd97eb4919dfd4b Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Wed, 12 Aug 2026 02:37:03 +0200 Subject: kernel(validate): fold in Plan 2's carried guards Three carried items from Plan 2's parked rulings, closed: 1. Slug uniqueness moves from a 200-sample QCheck property scoped to one rite (test_temporal_ef.ml) into Validate's own "slugs" check, so every consumer gets it. The resumed-Sunday exemption that property carried is dropped, not weakened elsewhere: Plan 2 verified zero duplicate slugs domain-wide (all 8 416 years), and by construction a resumed Sunday only ever backfills a week number Septuagesima cut short that same liturgical year, so it can never repeat a number that year's own January Sundays already used. The now-redundant property and its is_resumable_sunday_slug helper are removed from test_temporal_ef.ml; test_validate.ml's own domain-wide property covers the same ground for every consumer. 2. The anchors-erosion guard (Plan 2: deleting entries from a rite's anchors list left the whole suite green) is implemented, but not in Validate. Which of a rite's named days are Easter-derived is knowledge only the rite's own `named` function has; Rite.t deliberately exposes only `temporal` and `anchors`, never `named`, so a rite-agnostic Validate has no ground truth to check anchors' completeness against. Hardcoding an Easter offset, or even Easter itself, would smuggle Western/Gregorian-specific knowledge into code meant to also serve a future Julian-reckoning rite; rediscovering "named-ness" structurally from `temporal` alone is unsound for EF, since most ordinary Sunday/feria slugs from Septuagesima onward are also constant-offset-from-Easter by construction. The guard is therefore EF-specific and lives in test_temporal_ef.ml, discovering the Easter-derived slug set mechanically (scanning a window around Easter and keeping whatever `named` answers Some for) rather than hand-copying either named's or anchors' own offset list, then asserting completeness against the real anchors for the domain's Easter extremes (1598, 1666) plus an ordinary year. A negative fixture proves the guard has teeth, matching Plan 2's exact regression (anchors missing "ef-ascension" reports it, and only it, as missing). 3. test_validate.ml's extreme_years comment claimed 1818/2038; verified against Computus.gregorian_easter directly, the domain's actual Easter extremes (1583..2500) are 1598/1666. Corrected. Verification: the full 1583..9999 domain sweep (233 tests via dune test's 200-sample default, plus a manual full sweep) reports exactly one failure -- the known, already-pinned year-9999 season-truncation case -- and zero occurrences of the new "slugs" check anywhere in the domain. Deleting "ef-ascension" from the real anchors list (reproducing Plan 2's regression directly) is caught immediately by the new EF test and, confirmed empirically, invisible to Validate's own full property sweep -- direct evidence for why item 2 cannot live in Validate. --- lib/kernel/validate.ml | 49 +++++++++++++---- lib/kernel/validate.mli | 7 +++ test/test_temporal_ef.ml | 140 ++++++++++++++++++++++++++++++++++++----------- test/test_validate.ml | 24 +++++++- 4 files changed, 174 insertions(+), 46 deletions(-) (limited to 'lib/kernel') diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index d8de31b..cc8bdce 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -20,6 +20,17 @@ let has_duplicate strings = let rec go = function a :: (b :: _ as rest) -> a = b || go rest | _ -> false in go sorted +(* Like [has_duplicate], but names the offender(s) instead of only reporting + that one exists -- the ["slugs"] check below wants a useful failure + detail, not just a bool. *) +let duplicates strings = + let sorted = List.sort String.compare strings in + let rec go acc = function + | a :: (b :: _ as rest) -> go (if a = b then a :: acc else acc) rest + | _ -> acc + in + List.sort_uniq String.compare (go [] sorted) + (* Task 12's "unconverged" check has no structural signal to key off -- Calendar's placement pass records its round-guard reason as a plain string in [Liturgical_day.omitted] (calendar.ml's own [unconverged_reason], @@ -85,18 +96,16 @@ let run (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) ~year = (* Weekday agreement. *) if t.Temporal.weekday <> Date.weekday date then fail date "weekday" "temporal weekday disagrees with Date.weekday"; - (* Slug: three properties, none checked here, all delivered - elsewhere. Well-formedness needs no check: [Slug.t] is a private - string validated on every construction path ([of_string], - [of_string_exn], [t_of_sexp]), and [to_string] is the identity, - so round-tripping an existing [Slug.t] can never fail -- a check - here would be structurally incapable of firing, which is worse - than no check, since it would look like coverage that isn't - there. Uniqueness *per date* needs no check either: [temporal] - returns exactly one office by construction. Uniqueness *across - the year* is deliberately NOT asserted -- a resumed Sunday - reuses an earlier Epiphany key on purpose, so the check would be - false. *) + (* Slug: three properties. Well-formedness needs no check: [Slug.t] + is a private string validated on every construction path + ([of_string], [of_string_exn], [t_of_sexp]), and [to_string] is + the identity, so round-tripping an existing [Slug.t] can never + fail -- a check here would be structurally incapable of firing, + which is worse than no check, since it would look like coverage + that isn't there. Uniqueness *per date* needs no check either: + [temporal] returns exactly one office by construction. + Uniqueness *across the year* IS asserted, below, once the whole + walk is in hand -- see the ["slugs"] check after this loop. *) (* Vocabulary closure. *) if not (List.exists (fun r -> vocab.Vocab.rank_to_string r = vocab.Vocab.rank_to_string cel.Celebration.rank) @@ -114,6 +123,22 @@ let run (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) ~year = | None -> fail date "determinism" "a second call to temporal raised where the first succeeded")) days; let observed = List.rev !observed in + (* Slug uniqueness across the year (Plan 2 carried item 4): moved into + [Validate] itself so every consumer gets it, not only a 200-sample + QCheck property scoped to one rite. Asserted OUTRIGHT, no exemption: + Plan 2 verified zero duplicate slugs domain-wide, across all 8 416 + years, for the EF rite's own resumed-Sunday mechanism -- the exemption + the test property used to carry protected nothing real, because a + resumed Sunday only ever backfills a week number Septuagesima cut short + that same liturgical year (so it was never actually used that year to + begin with), never repeats one the year's own January Sundays already + used. If a future rite genuinely needs an exemption, it can supply one + then -- not speculatively here. *) + (match duplicates (List.map (fun (_, t) -> Slug.to_string t.Temporal.office.Celebration.slug) observed) with + | [] -> () + | dups -> + fail start "slugs" + (Printf.sprintf "slug(s) sighted on more than one date this year: %s" (String.concat ", " dups))); (* Season contiguity and completeness: the run-length-compressed sequence must equal the rite's own [season_runs] exactly, in canonical order. This is NOT necessarily [vocab.seasons] -- most rites have each season in one diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli index 511c78f..5e55fc5 100644 --- a/lib/kernel/validate.mli +++ b/lib/kernel/validate.mli @@ -17,6 +17,13 @@ val failure_to_string : failure -> string straddles two civil years, and checks only the pairs whose date actually falls within the year walked. + ["slugs"]: no two dates within the walked liturgical year may carry the + same office slug (Plan 2 carried item 4). Asserted outright, with no + exemption for the resumed-Sunday reuse a slug's own name might suggest: + a resumed Sunday only ever backfills a week number Septuagesima cut + short that same year, so by construction it never repeats a number that + year's own January Sundays actually used. + The season check compares the run-length-compressed season sequence against [rite.Rite.season_runs], not [rite.Rite.vocab.seasons]: a rite may have one season appear in two separate runs (the modern form's Ordinary diff --git a/test/test_temporal_ef.ml b/test/test_temporal_ef.ml index 2ad93e8..477651c 100644 --- a/test/test_temporal_ef.ml +++ b/test/test_temporal_ef.ml @@ -306,36 +306,112 @@ let test_christmastide_feria_slugs () = Alcotest.(check string) "13 Jan (Tue, on/after the origin)" "ef-time-after-epiphany-1-tuesday" (slug_of (d 2026 1 13)) -(* The general property behind the fix above: no two dates in one liturgical - year may share a slug, except the deliberate resumed-Sunday reuse (see - test_resumed_sundays). Random years across the whole domain, not just - 2026 -- the original bug (controller finding A) was found by grepping one - year's CLI output for duplicates, and other years could hide others. *) -let is_resumable_sunday_slug s = - let prefix = "ef-time-after-epiphany-sunday-" in - String.length s > String.length prefix && String.sub s 0 (String.length prefix) = prefix - -let prop_slugs_unique_within_liturgical_year = - QCheck.Test.make ~count:200 - ~name:"no two dates in one liturgical year share a slug, apart from the resumed-Sunday reuse" - (QCheck.int_range 1583 9998) +(* The general property behind the fix above -- no two dates in one + liturgical year may share a slug -- moved to + [Colitur_kernel.Validate]'s own ["slugs"] check (Plan 2 carried item 4), + asserted outright with no resumed-Sunday exemption: Plan 2 verified zero + duplicate slugs domain-wide, so the exemption this property used to carry + protected nothing real. [Validate]'s own 200-sample property + (test_validate.ml's [prop_invariants]) now covers every consumer, + including this rite, over the same 1583..9998 domain this property used + to sweep alone. *) + +(* ---- Plan 2 carried item 5: the anchors list has no guard against its own + erosion ---- + + [Colitur_kernel.Validate] cannot own this completeness check: which of + [named]'s entries are Easter-derived is knowledge only [named] itself + has. [Rite.t] deliberately exposes just [temporal] (the merged result) + and [anchors] (the independent restatement), never [named] -- so a + rite-agnostic [Validate] has no ground truth to compare [anchors] + against, short of inventing one. Two ways of inventing one were + considered and rejected: + + - Hardcoding a specific Easter offset (Ash Wednesday = Easter-46, say) + inside [Validate] would smuggle Western/Gregorian-Paschal-cycle + knowledge into code the design intends to also serve a future + Julian-reckoning rite (Byzantine, named explicitly as a future module + in this project's own architecture note) -- for which neither that + offset, nor even Gregorian Easter itself as the reference point + ([Computus.gregorian_easter], not [julian_easter]), is the right one. + Even [Computus]'s own [ash_wednesday]/[palm_sunday]/[ascension]/ + [pentecost] helpers are documented "(OF + EF)" -- i.e. already scoped + to the two WESTERN forms, not to "any rite" the way [Validate] must + stay. + - Rediscovering "Easter-derived" structurally from [temporal] alone (scan + near Easter, keep whatever recurs at the same offset across years with + different Easters) is unsound for EF specifically: [Time_after_epiphany] + onward, week numbering itself is computed from Easter-relative origins + ([week_origin]), so almost every ORDINARY Sunday/feria slug in + Septuagesima/Lent/Passiontide/Paschaltide/Time_after_pentecost is ALSO + constant-offset-from-Easter across years -- structurally + indistinguishable from a genuinely named day by that test alone. Rank + does not separate them either: RG 91 entry 10 makes the privileged + Easter/Pentecost octave FERIAS class 1 too, same as many named days. + + This guard is therefore entirely EF-specific and lives here, against + [T.named] and [T.anchors] directly -- both accessible in this file, not + through the [Rite.t] boundary. *) + +(* "Easter-derived" is discovered mechanically from [named] itself, not + hand-copied from either [named]'s or [anchors]'s own source: scan a + window of dates around a year's Easter and keep whatever [named] answers + [Some] for. [named] returns [Some] only for its ~20 genuinely proper/named + days -- ordinary Sundays and ferias are produced by other functions + entirely, in [temporal]'s [None] branch -- so this cannot pick up an + ordinary week's slug by accident regardless of window width. [-60, +75] + safely isolates the Easter-relative half of [named] from its + fixed-calendar half: exhaustively checked over 1583..2500, the nearest + fixed named date to Easter (6 January, Epiphany) is never less than 75 + days before the EARLIEST possible Easter (22 March), so a 60-day backward + reach cannot cross into it even in the closest year, while the window + still comfortably covers [named]'s actual Easter-relative range (Ash + Wednesday at Easter-46 the earliest, Sacred Heart at Easter+68 the + latest). *) +let easter_relative_named_slugs y = + let easter = Colitur_kernel.Computus.gregorian_easter y in + List.filter_map + (fun n -> match T.named (D.add_days easter n) with Some (_, slug, _, _) -> Some slug | None -> None) + (List.init 136 (fun i -> i - 60)) + |> List.sort_uniq compare + +let anchor_slugs y = List.map fst (T.anchors y) |> List.sort_uniq compare + +(* The mechanism both tests below share: which of [named]'s Easter-derived + slugs [anchors] fails to restate. [] means complete. *) +let missing_from_anchors ~named_easter_slugs ~anchors = + List.filter (fun slug -> not (List.mem slug anchors)) named_easter_slugs + +(* The real guard: for the domain's own Easter extremes (1598 earliest, 1666 + latest -- see test_validate.ml's own [extreme_years], corrected by this + same task) plus an ordinary year, nothing [named] produces at an + Easter-relative offset is missing from [anchors]. *) +let test_anchors_cover_easter_derived_named_days () = + List.iter (fun y -> - let start = T.year_start y in - let stop = D.add_days (T.year_start (y + 1)) (-1) in - let n = D.to_rata stop - D.to_rata start + 1 in - let seen = Hashtbl.create 512 in - let rec check i = - i >= n - || - let s = slug_of (D.add_days start i) in - (is_resumable_sunday_slug s - || (not (Hashtbl.mem seen s)) - && ( - Hashtbl.replace seen s (); - true)) - && check (i + 1) + let missing = + missing_from_anchors ~named_easter_slugs:(easter_relative_named_slugs y) ~anchors:(anchor_slugs y) in - check 0) + Alcotest.(check (list string)) + (Printf.sprintf "%d: every Easter-derived named slug is restated in anchors" y) + [] missing) + [ 1598; 1666; 2026 ] + +(* Proves the guard above actually has teeth, per this task's negative-fixture + requirement: [T.anchors]'s real slug set with one genuinely Easter-derived + entry ("ef-ascension") struck out must fail [missing_from_anchors] the same + way the real list passes it -- reproducing, in miniature, exactly what + "deleting four entries leaves the whole suite green" (Plan 2, carried item + 5) looked like before this test existed. *) +let test_anchors_erosion_is_caught () = + let y = 2026 in + let named_easter_slugs = easter_relative_named_slugs y in + Alcotest.(check bool) "sanity: ef-ascension is genuinely in the Easter-derived set" true + (List.mem "ef-ascension" named_easter_slugs); + let eroded_anchors = List.filter (fun s -> s <> "ef-ascension") (anchor_slugs y) in + Alcotest.(check (list string)) "the erosion is caught: the missing entry is reported, and only it" + [ "ef-ascension" ] + (missing_from_anchors ~named_easter_slugs ~anchors:eroded_anchors) let test_totality () = (* Every day of 2026 yields an office without raising. Not a slug @@ -367,12 +443,14 @@ let suite_extra = Alcotest.test_case "colours" `Quick test_colours; Alcotest.test_case "christmastide feria slugs" `Quick test_christmastide_feria_slugs; Alcotest.test_case "named days carry their week" `Quick test_named_days_carry_their_week; - Alcotest.test_case "totality" `Quick test_totality ] + Alcotest.test_case "totality" `Quick test_totality; + Alcotest.test_case "anchors cover easter-derived named days" `Quick + test_anchors_cover_easter_derived_named_days; + Alcotest.test_case "anchors erosion is caught" `Quick test_anchors_erosion_is_caught ] let suite = ( "Rite_ef", [ Alcotest.test_case "vocab roundtrips" `Quick test_vocab_roundtrips; Alcotest.test_case "slug words" `Quick test_slug_words ] @ suite_extra - @ List.map QCheck_alcotest.to_alcotest - [ prop_temporal_week_matches_week; prop_slugs_unique_within_liturgical_year ] ) + @ List.map QCheck_alcotest.to_alcotest [ prop_temporal_week_matches_week ] ) diff --git a/test/test_validate.ml b/test/test_validate.ml index b2d4f34..4b9c3c0 100644 --- a/test/test_validate.ml +++ b/test/test_validate.ml @@ -77,9 +77,10 @@ let extreme_years () = let test_easter_extremes () = let ys = extreme_years () in - (* Both extremes genuinely occur in 1583..2500 (earliest 1818, latest - 2038); requiring just "non-empty" would have passed even if the search - silently found only one of them (register finding 15). *) + (* Both extremes genuinely occur in 1583..2500 (earliest 1598, latest + 1666 -- verified against Computus.gregorian_easter directly, not + transcribed); requiring just "non-empty" would have passed even if the + search silently found only one of them (register finding 15). *) Alcotest.(check int) "found both extreme years (earliest 22 Mar and latest 25 Apr)" 2 (List.length ys); List.iter check_year ys @@ -539,6 +540,22 @@ let test_vocab_season_injectivity_fires () = Alcotest.(check bool) "vocab check fires when season_to_string collapses two seasons to one string" true (has_check "vocab" (run ~vocab:vocab_collapsed_seasons good)) +(* Plan 2 carried item 4: slug uniqueness moves into [Validate] itself, no + exemption. [target] (17 March, mid-run) is given the NEXT day's real slug + verbatim -- a genuine collision between two distinct dates in the same + walked year, touching only the [slug] field so every other check (season, + week, weekday, rank, colour, determinism, anchor) stays silent against it. *) +let test_slugs_fires () = + let colliding_slug = (good (D.add_days target 1)).Temporal.office.Cel.slug in + let temporal d = + let t = good d in + if D.compare d target = 0 then + { t with Temporal.office = { t.Temporal.office with Cel.slug = colliding_slug } } + else t + in + Alcotest.(check bool) "slugs check fires when two dates in the year share a slug" true + (has_check "slugs" (run temporal)) + (* ---- Task 12: resolution invariants ---- Each test below asserts that exactly one of the five new check labels @@ -604,6 +621,7 @@ let suite = Alcotest.test_case "anchor fires" `Quick test_anchor_fires; Alcotest.test_case "vocab rank injectivity fires" `Quick test_vocab_rank_injectivity_fires; Alcotest.test_case "vocab season injectivity fires" `Quick test_vocab_season_injectivity_fires; + Alcotest.test_case "slugs fires" `Quick test_slugs_fires; Alcotest.test_case "lost fires on resolution exception" `Quick test_lost_fires_on_resolution_exception; Alcotest.test_case "duplicated fires" `Quick test_duplicated_fires; Alcotest.test_case "unconverged fires" `Quick test_unconverged_fires; -- cgit v1.3 From ac569e859be08320e47909e496d6e5e8f6057da7 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Wed, 12 Aug 2026 10:40:12 +0200 Subject: docs+test: small factual corrections (item 7, part 1) Six independent, small corrections found during the final review: - dune (workspace root): the comment said the stanza used "(:standard)" to preserve dune's default `default` alias target; the stanza actually spells that out explicitly via (alias_rec install). Comment now matches the code. - test_validate.ml's test_easter_extremes asserted `List.length ys = 2` where an identity check was called for -- the comment already named 1598 and 1666, but nothing confirmed extreme_years() found THOSE two rather than some other pair with the right cardinality. Now asserts the identities directly (the project's "cardinality where identity was required" vacuity flavour, per the review). - test_oracle.ml and expected-divergences-missalemeum.sexp both claimed "one entry (M13) is [verdict open]" -- M11 is open too (its own verdict changed from colitur to open in fix round 1); both now say "two entries (M11 and M13)". - expected-divergences-missalemeum.sexp's M2 note attributed `band` to temporal_ef.ml; `band` is precedence_ef.ml's own function. - lib/kernel/precedence.mli documented `dropped`/`admit`'s physical- equality obligation nowhere -- it lived only in one rite's own module (Rite_ef.Precedence_ef.admit's doc comment), but this signature is what an author of the next rite actually reads. Added the obligation here, cross-referencing the EF instance as precedent, not the only source. - README's opam install line omitted sexplib and ppx_sexp_conv (both in dune-project's own depends; `dune build` fails without them for a contributor following the README verbatim) and documented only `colitur easter`, though `temporal` and `day` both exist and are the more useful entry points. Fixed both. No behaviour change: comment/doc/test-assertion corrections only (the easter-extremes fix strengthens an assertion, it does not change what passes). Verified byte-identical `colitur day` output across 1583, 1900, 1902, 2008, 2011, 2026, 2038, 9999. 259/259 tests green. --- README.md | 6 ++++-- data/ef/expected-divergences-missalemeum.sexp | 9 ++++++--- dune | 7 ++++--- lib/kernel/precedence.mli | 18 +++++++++++++++++- test/test_oracle.ml | 10 +++++++--- test/test_validate.ml | 13 ++++++++++--- 6 files changed, 48 insertions(+), 15 deletions(-) (limited to 'lib/kernel') diff --git a/README.md b/README.md index e5a6c5f..9b11d73 100644 --- a/README.md +++ b/README.md @@ -12,10 +12,12 @@ reading citations, correct to year 9999. See the design and rules research under ```sh opam switch create . 5.2.0 -y # first time: local OCaml switch -opam install -y dune alcotest qcheck qcheck-alcotest +opam install -y dune alcotest qcheck qcheck-alcotest sexplib ppx_sexp_conv dune build dune test -dune exec colitur -- easter 2026 +dune exec colitur -- easter 2026 # Easter and its Easter-relative anchors +dune exec colitur -- temporal 2026 # the EF temporal cycle only, one line per day +dune exec colitur -- day 2026 # the full resolved EF calendar (temporal + sanctoral) ``` ## License diff --git a/data/ef/expected-divergences-missalemeum.sexp b/data/ef/expected-divergences-missalemeum.sexp index 5dbe3ed..f50898b 100644 --- a/data/ef/expected-divergences-missalemeum.sexp +++ b/data/ef/expected-divergences-missalemeum.sexp @@ -16,9 +16,12 @@ ; did not build. Those are honestly verdicted [missalemeum] -- colitur is ; short a feature or a row, not correct -- and each is cross-referenced ; into docs/research/rules-register.md §6 as an open item, not silently -; absorbed as if colitur were right. One entry (M13) is [verdict open]: +; absorbed as if colitur were right. TWO entries (M11 and M13) are +; [verdict open] -- corrected, final fix wave, item 7: this note previously +; said "one entry (M13)", missing M11 (whose own verdict changed from +; [colitur] to [open] in fix round 1, see M11's own entry below). Both are ; adjudicated as UNRESOLVED after real primary-source effort, not defaulted -; past -- see that entry's own note and the task report for the full +; past -- see each entry's own note and the task report for the full ; search. ; ; [expected_rows] is the exact row count this entry accounts for over the @@ -38,7 +41,7 @@ ((id M2) (citation "RG 91 entry 27 (\"Officium sanctae Mariae in sabbato\") -- register §4") (verdict missalemeum) - (note "Every otherwise-unoccupied IV-class Saturday should carry the votive Office of the BVM (white; missalemeum's own titles cycle \"I\"..\"V Mass of the B. V. M. -- Salve, Sancta Parens\"). temporal_ef.ml's [band] already has an entry-27 comment acknowledging this row exists, but [Temporal_ef.temporal] never actually CONSTRUCTS this office -- an unimpeded Time-after-Epiphany/-Pentecost Saturday gets a bare ferial slug and season green instead. A genuine feature gap, not a citation dispute; tracked in register §6, not built in this task.") + (note "Every otherwise-unoccupied IV-class Saturday should carry the votive Office of the BVM (white; missalemeum's own titles cycle \"I\"..\"V Mass of the B. V. M. -- Salve, Sancta Parens\"). precedence_ef.ml's [band] already has an entry-27 comment acknowledging this row exists (corrected attribution, final fix wave: this note previously said temporal_ef.ml, but [band] is precedence_ef.ml's own function), but [Temporal_ef.temporal] never actually CONSTRUCTS this office -- an unimpeded Time-after-Epiphany/-Pentecost Saturday gets a bare ferial slug and season green instead. A genuine feature gap, not a citation dispute; tracked in register §6, not built in this task.") (expected_rows 17)) ((id M3) (citation "RG 87 (Minor Litanies/Rogations, Mon/Tue before Ascension) -- the SAME citation as the lectio allow-list's own C8 (data/ef/expected-divergences.sexp)") diff --git a/dune b/dune index de5051c..8a00001 100644 --- a/dune +++ b/dune @@ -12,9 +12,10 @@ ; test suite could not have caught this on its own -- it took a genuinely ; clean rebuild to surface it. ; -; (:standard) keeps whatever `default` would otherwise resolve to (the -; package's own install artifacts -- executables, libraries) so this ADDS a -; requirement rather than replacing dune's own default behaviour. +; (alias_rec install) keeps whatever `default` would otherwise resolve to +; (the package's own install artifacts -- executables, libraries, reached +; recursively through every subdirectory's own `install` alias) so this +; ADDS a requirement rather than replacing dune's own default behaviour. (alias (name default) (deps diff --git a/lib/kernel/precedence.mli b/lib/kernel/precedence.mli index d30e5c3..4225eb7 100644 --- a/lib/kernel/precedence.mli +++ b/lib/kernel/precedence.mli @@ -38,7 +38,23 @@ type ('s, 'r) rules = { ('r candidate * privilege) list; (** RG 108-111: how many commemorations are admitted, and in what order; anything filtered out here is recorded in {!resolution.omitted}, not - dropped. *) + dropped. + + OBLIGATION ON THE IMPLEMENTATION, not enforced by this type: every + candidate this function returns must be a value taken UNCHANGED + from its input list, never rebuilt (e.g. via a [{ c with ... }] + record update, even one that copies every field back unchanged). + {!resolve}'s own [omitted] accounting distinguishes an admitted + candidate from a dropped one by PHYSICAL equality ([==]) on the + candidate value, not structural equality -- a rebuilt record is + [=] to the original but not [==], so {!resolve} would then count + it as dropped a SECOND time (once because it is genuinely absent + from the admitted set, once because its identity no longer + matches its own admitted copy), silently double-counting rather + than raising. This obligation previously lived only in one rite's + own module documentation (Rite_ef.Precedence_ef.admit); stated + here because this signature -- not any one rite's implementation + of it -- is what an author of the next rite reads. *) } (** The outcome of resolving one day's candidates. *) diff --git a/test/test_oracle.ml b/test/test_oracle.ml index 152464a..ac8d95d 100644 --- a/test/test_oracle.ml +++ b/test/test_oracle.ml @@ -56,9 +56,13 @@ entries; RG 110's inseparable-Peter/Paul commemoration is unimplemented code, a real feature this task did not build) -- honestly verdicted [missalemeum] (colitur is short a feature or a row, not right), never - silently absorbed as if colitur were correct. One entry (M13) is - [verdict open]: adjudicated as unresolved, not resolved either way -- - the brief's own explicit permission ("say so as an open item") used for + silently absorbed as if colitur were correct. TWO entries (M11 and + M13) are [verdict open] -- CORRECTED, final fix wave, item 7: this + comment previously said "one entry (M13)", missing M11, whose own + verdict was changed from [colitur] to [open] in fix round 1 (see M11's + own entry below for why) but this summary was never updated to match. + Both are adjudicated as unresolved, not resolved either way -- the + brief's own explicit permission ("say so as an open item") used for real, not defaulted past. See the task report for every entry's full reasoning and primary-source citation. *) diff --git a/test/test_validate.ml b/test/test_validate.ml index ee7f288..89053c1 100644 --- a/test/test_validate.ml +++ b/test/test_validate.ml @@ -79,9 +79,16 @@ let test_easter_extremes () = let ys = extreme_years () in (* Both extremes genuinely occur in 1583..2500 (earliest 1598, latest 1666 -- verified against Computus.gregorian_easter directly, not - transcribed); requiring just "non-empty" would have passed even if the - search silently found only one of them (register finding 15). *) - Alcotest.(check int) "found both extreme years (earliest 22 Mar and latest 25 Apr)" 2 (List.length ys); + transcribed). CORRECTED (final fix wave, item 7): this used to assert + only [List.length ys = 2], a cardinality check where an identity check + was called for -- the comment already named 1598 and 1666, but nothing + confirmed [ys] actually contained THOSE two years rather than some + other pair the search happened to find first; a version of + [extreme_years] that silently found the wrong two years but still + found exactly two would have passed this unchanged. Asserting the + identities directly is strictly stronger and costs nothing extra. *) + Alcotest.(check (list int)) "found exactly 1598 (earliest 22 Mar) and 1666 (latest 25 Apr)" + [ 1598; 1666 ] ys; List.iter check_year ys (* The confidence-to-9999 core: random years across the whole domain. *) -- cgit v1.3 From 6d6ba502d8022d9e0b8cdc5302f5761d39895192 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Wed, 12 Aug 2026 10:40:27 +0200 Subject: kernel+rite-ef: correct stale plan-relative deferrals (item 7, part 2) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Several comments described work as "arriving with Plan 3" or "waiting for Plan 3" that either shipped without it or refer to the wrong future plan number, all now false in ways that would mislead the next reader: - temporal_ef.ml (two places) and precedence_ef.ml said the Major Litanies (25 April, RG 80) "arrive with Plan 3's sanctoral". Plan 3 shipped, in this branch, without them; register §6 tracks this as a plain open item with no plan committed to build it, and now says so. - temporal_ef.ml said the Sacred Triduum's "own named offices are a Plan 3 sanctoral addition". Wrong on two counts: Plan 3 shipped without adding them, AND a proper office for I-class FERIAS was never a sanctoral matter in the first place (RG 21 defines "feria" to exclude Sundays/feasts, not the reverse). 2026-04-02/03/04 still resolve to the ordinary Passiontide ferial fallback's own generic slugs (ef-passiontide-2-{thursday,friday,saturday}), confirmed against real output; register §6 now records this as its own open item. - temporal_ef.ml said the Rogation-Wednesday commemoration (Ascension Vigil day, entry 21) "waits for RG 108-111" -- both the precedence framework and RG 108-111 exist now; the Wednesday's own commemoration is still never constructed, but for a different, still-real reason (no candidate is wired for it), not a forward dependency. Fixed at both of this comment's two occurrences in the file. - vocab.ml/vocab.mli's `seasons` field doc said "Validate's contiguity check reads this" -- false since validate.ml's "seasons" check switched to Rite.t.season_runs in this branch (rite-supplied, to support a season appearing in more than one run, which the modern form's Ordinary Time needs and EF does not). - vocab.ml/vocab.mli's `ranks` field doc said "it is not a precedence relation until Plan 3 defines one" -- Plan 3 did define one (RG 111's dignity ordering), but as its own small, separately-hardcoded function in precedence_ef.ml, not one derived from this field; corrected to say so precisely rather than leaving a forward-looking claim unresolved. - The lectionary bootstrap (reading citations, Liturgical_day.t's own `citations` field) is called "Plan 3" at slug.ml, vocab_ef.ml, and three places in temporal_ef.ml, but "Plan 4" at liturgical_day.mli (whose own doc comment -- "always empty until Plan 4" -- is the authoritative one: the SANCTORAL bootstrap is Plan 3 and shipped; the LECTIONARY bootstrap is a separate, later Plan 4). All six corrected to say Plan 4, cross-referencing the Plan 3/4 distinction at the first (slug.ml) occurrence so the reasoning is not duplicated six times. No behaviour change: every edit here is a comment/documentation correction. Verified byte-identical `colitur day` output across 1583, 1900, 1902, 2008, 2011, 2026, 2038, 9999. 259/259 tests green. --- lib/kernel/slug.ml | 8 +++- lib/kernel/vocab.ml | 25 +++++++++++-- lib/kernel/vocab.mli | 25 +++++++++++-- lib/rites/rite_ef/precedence_ef.ml | 12 +++--- lib/rites/rite_ef/temporal_ef.ml | 77 +++++++++++++++++++++++++++----------- lib/rites/rite_ef/vocab_ef.ml | 5 ++- 6 files changed, 117 insertions(+), 35 deletions(-) (limited to 'lib/kernel') diff --git a/lib/kernel/slug.ml b/lib/kernel/slug.ml index 5139c99..25281f2 100644 --- a/lib/kernel/slug.ml +++ b/lib/kernel/slug.ml @@ -1,6 +1,10 @@ (* Stable celebration identifiers. Also the lectionary key: EF slugs are adopted - verbatim from lectio so the Plan 3 lectionary bootstrap needs no mapping - table (spec §4.4). *) + verbatim from lectio so the Plan 4 lectionary bootstrap needs no mapping + table (spec §4.4). CORRECTED (final fix wave, item 7): this comment said + "Plan 3" -- the SANCTORAL bootstrap (data/ef/sanctoral.sexp) is Plan 3 and + shipped in this branch; the LECTIONARY bootstrap (reading citations, + Liturgical_day.t's own [citations] field) is a separate, later Plan 4, + per that field's own doc comment ("always empty until Plan 4"). *) type t = string let valid_char c = (c >= 'a' && c <= 'z') || (c >= '0' && c <= '9') || c = '-' diff --git a/lib/kernel/vocab.ml b/lib/kernel/vocab.ml index 78729bb..bcb48b8 100644 --- a/lib/kernel/vocab.ml +++ b/lib/kernel/vocab.ml @@ -7,13 +7,32 @@ parametric types natively. *) type ('s, 'r) t = { seasons : 's list; - (** canonical liturgical-year order; Validate's contiguity check reads this *) + (** canonical liturgical-year order. CORRECTED (final fix wave, item + 7): this used to say "Validate's contiguity check reads this" -- + false since validate.ml's own "seasons" check switched to + {!Colitur_kernel.Rite.t}.season_runs in this branch (Plan 2 + carried item 1: EF has each season in one run, but the modern + form's Ordinary Time does not, so the expected run sequence had + to become rite-supplied rather than derived from this field). + For EF specifically {!Rite_ef.rite_ef.ml} sets season_runs to + this very list, so the two happen to agree there, but Validate + itself no longer reads [seasons] to build its expectation. *) season_to_string : 's -> string; season_of_string : string -> 's option; ranks : 'r list; (** documentation order, highest first. Plan 2 uses it only for the - closure check -- it is not a precedence relation until Plan 3 - defines one. *) + closure check. CORRECTED (final fix wave, item 7): this used to + say "it is not a precedence relation until Plan 3 defines one" -- + Plan 3 did define one (RG 111's dignity ordering, Rite_ef. + Precedence_ef.dignity/compare_dignity), but as its OWN small, + separately-hardcoded function, not one derived from this field: + [admit] needs Vocab_ef.rank's dignity as plain data (RG 8's four + classes), and reusing this field's own [int list] position would + couple that meaning to documentation order the way {!band} is + explicitly NOT allowed to (precedence_ef.ml's own file comment). + This field therefore still carries no precedence relation of its + own; a rite that wanted one derived from it would have to build + it itself. *) rank_to_string : 'r -> string; rank_of_string : string -> 'r option; } diff --git a/lib/kernel/vocab.mli b/lib/kernel/vocab.mli index 78729bb..bcb48b8 100644 --- a/lib/kernel/vocab.mli +++ b/lib/kernel/vocab.mli @@ -7,13 +7,32 @@ parametric types natively. *) type ('s, 'r) t = { seasons : 's list; - (** canonical liturgical-year order; Validate's contiguity check reads this *) + (** canonical liturgical-year order. CORRECTED (final fix wave, item + 7): this used to say "Validate's contiguity check reads this" -- + false since validate.ml's own "seasons" check switched to + {!Colitur_kernel.Rite.t}.season_runs in this branch (Plan 2 + carried item 1: EF has each season in one run, but the modern + form's Ordinary Time does not, so the expected run sequence had + to become rite-supplied rather than derived from this field). + For EF specifically {!Rite_ef.rite_ef.ml} sets season_runs to + this very list, so the two happen to agree there, but Validate + itself no longer reads [seasons] to build its expectation. *) season_to_string : 's -> string; season_of_string : string -> 's option; ranks : 'r list; (** documentation order, highest first. Plan 2 uses it only for the - closure check -- it is not a precedence relation until Plan 3 - defines one. *) + closure check. CORRECTED (final fix wave, item 7): this used to + say "it is not a precedence relation until Plan 3 defines one" -- + Plan 3 did define one (RG 111's dignity ordering, Rite_ef. + Precedence_ef.dignity/compare_dignity), but as its OWN small, + separately-hardcoded function, not one derived from this field: + [admit] needs Vocab_ef.rank's dignity as plain data (RG 8's four + classes), and reusing this field's own [int list] position would + couple that meaning to documentation order the way {!band} is + explicitly NOT allowed to (precedence_ef.ml's own file comment). + This field therefore still carries no precedence relation of its + own; a rite that wanted one derived from it would have to build + it itself. *) rank_to_string : 'r -> string; rank_of_string : string -> 'r option; } diff --git a/lib/rites/rite_ef/precedence_ef.ml b/lib/rites/rite_ef/precedence_ef.ml index 9997bb2..fcd2116 100644 --- a/lib/rites/rite_ef/precedence_ef.ml +++ b/lib/rites/rite_ef/precedence_ef.ml @@ -429,11 +429,13 @@ let privilege_of (c : Vocab_ef.rank Precedence.candidate) : Precedence.privilege else if is_temporal && List.exists (fun p -> String.starts_with ~prefix:p slug) alp_feria_prefixes then Precedence.Privileged (* (f) RG 109(f) (§4): "of the Major Rogations, in Mass" -- the - Major Litanies (25 April, RG 80) are not yet computed anywhere in this - codebase (temporal_ef.ml's own comment on [temporal]'s Rogation branch: - "The Major Litanies... are a fixed date and are not yet computed; they - arrive with Plan 3's sanctoral"), so no candidate this engine can - currently construct represents one. There is no existing slug + Major Litanies (25 April, RG 80) are STILL not computed anywhere in + this codebase (temporal_ef.ml's own comment on [temporal]'s Rogation + branch, CORRECTED final fix wave item 7: they did not, in fact, + "arrive with Plan 3's sanctoral" -- Plan 3 shipped without them, + register §6 tracks this as an open item with no plan yet committed to + build it), so no candidate this engine can currently construct + represents one. There is no existing slug convention to anchor a check to, and guessing one risks silently misclassifying whatever a future task does name it -- a wrong citation is worse than a missing one, so this is left unimplemented and flagged diff --git a/lib/rites/rite_ef/temporal_ef.ml b/lib/rites/rite_ef/temporal_ef.ml index c3db15c..7782876 100644 --- a/lib/rites/rite_ef/temporal_ef.ml +++ b/lib/rites/rite_ef/temporal_ef.ml @@ -90,7 +90,10 @@ let named d = if m = 12 && dd = 25 then Some (Christmastide, "ef-nativity", Colour.White, Class1) else if m = 12 && dd = 24 then (* RG 91 entry 5: the Vigil of the Nativity is I class. lectio has no slug - for it, so this key has no lectionary entry until Plan 3 fills it. *) + for it, so this key has no lectionary entry until Plan 4 fills it + (CORRECTED, final fix wave, item 7 -- this is the lectionary/reading- + citations bootstrap, Plan 4, not the sanctoral one, Plan 3, which + already shipped in this branch). *) Some (Advent, "ef-nativity-vigil", Colour.Violet, Class1) else if m = 12 && (dd = 29 || dd = 30 || dd = 31) then (* Days within the Octave of the Nativity; 26-28 Dec are Stephen, John and @@ -111,9 +114,15 @@ let named d = else if same d (off 7) then Some (Paschaltide, "ef-low-sunday", Colour.White, Class1) (* RG 91 entry 6 *) else if same d (off 38) then - (* RG 91 entry 21: II-class vigil. It is also Rogation Wednesday; with no - precedence framework until Plan 3, temporal emits the higher-ranked - vigil and the Rogation commemoration waits for RG 108-111. *) + (* RG 91 entry 21: II-class vigil. It is also Rogation Wednesday; [named] + emits the higher-ranked vigil (entry 21 outranks any Rogation-day + ferial rank). CORRECTED (final fix wave, item 7): this comment + previously said the Rogation commemoration itself "waits for RG + 108-111" -- the precedence framework and RG 108-111 both exist now + (this branch), but no candidate for the Rogation Wednesday's own + observance is constructed here or anywhere else, so there is nothing + for RG 108-111 to admit; see the fuller comment on the Rogation + branch further down in [temporal] for the current, still-real gap. *) Some (Paschaltide, "ef-ascension-vigil", Colour.White, Class2) else if same d (off 39) then Some (Paschaltide, "ef-ascension", Colour.White, Class1) else if same d (off 48) then Some (Paschaltide, "ef-pentecost-vigil", Colour.Red, Class1) (* RG 91 entry 9 *) @@ -183,8 +192,10 @@ let week d = this to "ef-christmas-0-", indistinguishable from the stretch above in lectio's own data. colitur cannot preserve a distinction lectio doesn't make, so this becomes "ef-christmas-1-" -- a - colitur-only key and a lectionary gap for the Plan 3 bootstrap to fill, - exactly like the Nativity vigil and octave-day keys above. + colitur-only key and a lectionary gap for the Plan 4 bootstrap to fill + (CORRECTED, final fix wave, item 7: the lectionary bootstrap is Plan 4, + not Plan 3 -- see Slug.ml's own corrected comment), exactly like the + Nativity vigil and octave-day keys above. - 7-13 Jan, split in two by the *actual* first-Sunday-after-Epiphany origin ([week_origin Time_after_epiphany], which by construction always falls somewhere in this window -- see that function's own comment): @@ -303,8 +314,10 @@ let third_sunday_of_september y = The September and Advent sets match lectio's own Ember slugs. The Lent and Whitsun (Pentecost) sets do not -- lectio has no Ember slug for either, so "ef-lent-ember-*" and "ef-pentecost-ember-*" are colitur-only keys and a - lectionary gap for the Plan 3 bootstrap to fill (spec §4.4), the same - status as the Nativity vigil and the Rogation days below. *) + lectionary gap for the Plan 4 bootstrap to fill (spec §4.4; CORRECTED, + final fix wave, item 7 -- Plan 4, not Plan 3, is the lectionary + bootstrap), the same status as the Nativity vigil and the Rogation days + below. *) let ember d = let y = Date.year d in let easter = Computus.gregorian_easter y in @@ -327,12 +340,23 @@ let ember d = (* RG 91 entry 7: Ash Wednesday (named above) and Monday-Wednesday of Holy Week are I-class ferias -- the primary text reads "feria IV cinerum et II, - III et IV Hebdomadae sanctae", i.e. explicitly stops at Wednesday. Thursday - to Saturday of Holy Week are the Sacred Triduum, RG 91 entry 2 -- ranked - even above entry 7, not a mere feria -- but their own named offices are a - Plan 3 sanctoral addition; until then this gives them the same I-class rank - via the generic ferial path. RG 91 entry 10: the weekdays within the - privileged Octaves of Easter and Pentecost are I class too. *) + III et IV Hebdomadae sanctae", i.e. explicitly stops at Wednesday + (PRIMARY-SOURCE-VERIFIED, final fix wave: confirmed word for word + against the scan). Thursday to Saturday of Holy Week are the Sacred + Triduum, RG 91 entry 2 -- ranked even above entry 7, not a mere feria -- + but the Sacred Triduum has NO PROPER OFFICE of its own in this codebase + (CORRECTED, final fix wave, item 7: this comment previously said their + "own named offices are a Plan 3 sanctoral addition"; WRONG on two + counts -- Plan 3 shipped, in this branch, without adding them, AND a + proper office for I-class FERIAS was never a sanctoral matter to begin + with, RG 21's own definition of "feria" excludes Sundays/feasts, not the + other way round). `Temporal_ef.temporal 2026-04-02/03/04` (Holy + Thursday/Good Friday/Holy Saturday) still resolve today to the ordinary + Passiontide ferial fallback's own generic slugs, + "ef-passiontide-2-{thursday,friday,saturday}" -- register §6 records + this as its own open item now. This gives them the same I-class rank + via the generic ferial path regardless. RG 91 entry 10: the weekdays + within the privileged Octaves of Easter and Pentecost are I class too. *) let privileged_feria d = let easter = Computus.gregorian_easter (Date.year d) in let n = days_between easter d in @@ -392,16 +416,27 @@ let temporal d = | None -> ( (* Rogations (the Minor Litanies only -- RG 87, Monday and Tuesday before Ascension). The Major Litanies (25 April, RG 80) are a fixed - date and are not yet computed; they arrive with Plan 3's sanctoral - (register §6). The Wednesday here is the Ascension vigil (see Task - 11). RG 88: "de Litaniis minoribus nihil fit in Officio" -- the - Office (hence the day's rank) is unchanged by the Rogation; only the - Mass is proper. No RG 91 table entry elevates these days, so they + date and are STILL not computed (CORRECTED, final fix wave, item 7: + this comment previously said "they arrive with Plan 3's sanctoral" + -- Plan 3 shipped, in this branch, without them; register §6 tracks + this as a plain open item, with no plan committed to build it yet). + The Wednesday here is the Ascension vigil (see Task 11), which + happens to also fall on Rogation Wednesday -- the vigil (higher + RG 91 entry) is what [named] emits for that date; the Rogation + Wednesday's own commemoration is not separately constructed (a real + gap, not a forward dependency: the precedence framework and RG + 108-111 both exist now, but nothing wires a Rogation-Wednesday + candidate into the contest for this specific date the way Monday + and Tuesday get one below). RG 88: "de Litaniis minoribus nihil fit + in Officio" -- the Office (hence the day's rank) is unchanged by + the Rogation; only the Mass is proper. No RG 91 table entry + elevates these days, so they take the ordinary ferial rank of their season via [ferial_rank] rather than a fixed class. lectio has no Rogation slug at all, so "ef-rogation-monday"/"-tuesday" are colitur-only keys and a - lectionary gap for Plan 3, like the Ember and Nativity-vigil keys - above. *) + lectionary gap for Plan 4 (CORRECTED, final fix wave, item 7 -- + the lectionary bootstrap is Plan 4, not Plan 3), like the Ember + and Nativity-vigil keys above. *) let rogation = days_between easter d in if rogation = 36 || rogation = 37 then build ~season:s diff --git a/lib/rites/rite_ef/vocab_ef.ml b/lib/rites/rite_ef/vocab_ef.ml index 13e7309..e5726e8 100644 --- a/lib/rites/rite_ef/vocab_ef.ml +++ b/lib/rites/rite_ef/vocab_ef.ml @@ -45,7 +45,10 @@ let season_of_string = function (* Deliberately NOT season_to_string: slugs are lectionary keys adopted verbatim from lectio, which names these two seasons differently. Changing these words - would silently break the Plan 3 lectionary bootstrap. *) + would silently break the Plan 4 lectionary bootstrap (CORRECTED, final fix + wave, item 7 -- see Slug.ml's own corrected comment for the Plan 3/4 + distinction: the sanctoral bootstrap these slugs already serve is Plan 3 + and shipped; the lectionary/reading-citations bootstrap is Plan 4). *) let season_slug_word = function | Christmastide -> "christmas" | Paschaltide -> "easter" -- cgit v1.3 From d0b78ca2ef533080d4621b22071718bb8d3a6158 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Wed, 12 Aug 2026 11:19:51 +0200 Subject: docs: close the final review's four documentation residues precedence_ef.mli said "there is no fifth, unclassified case" after the same commit renumbered the disposition list from four cases to five; the count is now six. precedence.mli's physical-equality obligation described the failure mode as counting a drop "a SECOND time (once because it is genuinely absent, once because its identity no longer matches)" -- the same condition stated twice. What actually happens to a rebuilt candidate record is that the celebration surfaces in BOTH commemorations (the copy) and omitted (the original), one admission double-reported. precedence_ef.ml carried the same muddled sentence, which is where the kernel's copy came from; both now say it plainly. vocab.ml/.mli referenced {!Rite_ef.rite_ef.ml} -- a filename inside an odoc reference, which is malformed. Now plain [Rite_ef.rite]. README documented only `dune test`, so the exhaustive 1583-9999 Validate sweep was discoverable only by reading test_validate.ml's own comment. With no CI in this repo, that line is what stands between a committed artifact and one anyone runs. No behaviour change: `colitur day` output is byte-identical across 1583, 1900, 1902, 2008, 2011, 2026, 2038 and 9999 (2921 days, both domain edges). 259 tests by default, 260 with the sweep. --- README.md | 3 ++- lib/kernel/precedence.mli | 12 +++++++----- lib/kernel/vocab.ml | 2 +- lib/kernel/vocab.mli | 2 +- lib/rites/rite_ef/precedence_ef.ml | 10 +++++----- lib/rites/rite_ef/precedence_ef.mli | 2 +- 6 files changed, 17 insertions(+), 14 deletions(-) (limited to 'lib/kernel') diff --git a/README.md b/README.md index 9b11d73..6f71f6c 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,8 @@ reading citations, correct to year 9999. See the design and rules research under opam switch create . 5.2.0 -y # first time: local OCaml switch opam install -y dune alcotest qcheck qcheck-alcotest sexplib ppx_sexp_conv dune build -dune test +dune test # fast suite (~3s) +COLITUR_EXHAUSTIVE_SWEEP=1 dune test --force # + every year 1583-9999 (~50s) dune exec colitur -- easter 2026 # Easter and its Easter-relative anchors dune exec colitur -- temporal 2026 # the EF temporal cycle only, one line per day dune exec colitur -- day 2026 # the full resolved EF calendar (temporal + sanctoral) diff --git a/lib/kernel/precedence.mli b/lib/kernel/precedence.mli index 4225eb7..ae054dd 100644 --- a/lib/kernel/precedence.mli +++ b/lib/kernel/precedence.mli @@ -47,11 +47,13 @@ type ('s, 'r) rules = { {!resolve}'s own [omitted] accounting distinguishes an admitted candidate from a dropped one by PHYSICAL equality ([==]) on the candidate value, not structural equality -- a rebuilt record is - [=] to the original but not [==], so {!resolve} would then count - it as dropped a SECOND time (once because it is genuinely absent - from the admitted set, once because its identity no longer - matches its own admitted copy), silently double-counting rather - than raising. This obligation previously lived only in one rite's + [=] to the original but not [==], so {!resolve} cannot match the + rebuilt copy against the original it was given. The celebration + then surfaces TWICE in the same day's result -- once in + {!resolution.commemorations} (the rebuilt copy, admitted) and once + in {!resolution.omitted} (the original, which nothing in the + admitted set matches). One admission, double-reported, silently + rather than raising. This obligation previously lived only in one rite's own module documentation (Rite_ef.Precedence_ef.admit); stated here because this signature -- not any one rite's implementation of it -- is what an author of the next rite reads. *) diff --git a/lib/kernel/vocab.ml b/lib/kernel/vocab.ml index bcb48b8..a4e61a3 100644 --- a/lib/kernel/vocab.ml +++ b/lib/kernel/vocab.ml @@ -14,7 +14,7 @@ type ('s, 'r) t = { carried item 1: EF has each season in one run, but the modern form's Ordinary Time does not, so the expected run sequence had to become rite-supplied rather than derived from this field). - For EF specifically {!Rite_ef.rite_ef.ml} sets season_runs to + For EF specifically [Rite_ef.rite] sets season_runs to this very list, so the two happen to agree there, but Validate itself no longer reads [seasons] to build its expectation. *) season_to_string : 's -> string; diff --git a/lib/kernel/vocab.mli b/lib/kernel/vocab.mli index bcb48b8..a4e61a3 100644 --- a/lib/kernel/vocab.mli +++ b/lib/kernel/vocab.mli @@ -14,7 +14,7 @@ type ('s, 'r) t = { carried item 1: EF has each season in one run, but the modern form's Ordinary Time does not, so the expected run sequence had to become rite-supplied rather than derived from this field). - For EF specifically {!Rite_ef.rite_ef.ml} sets season_runs to + For EF specifically [Rite_ef.rite] sets season_runs to this very list, so the two happen to agree there, but Validate itself no longer reads [seasons] to build its expectation. *) season_to_string : 's -> string; diff --git a/lib/rites/rite_ef/precedence_ef.ml b/lib/rites/rite_ef/precedence_ef.ml index fcd2116..db7e708 100644 --- a/lib/rites/rite_ef/precedence_ef.ml +++ b/lib/rites/rite_ef/precedence_ef.ml @@ -685,11 +685,11 @@ let admit ~(observed : Vocab_ef.rank Precedence.candidate) than rebuilt ones; undocumented for rite authors" -- documented here, now that this is the function that note was about). Building a fresh [{ c with ... }] record anywhere below would silently defeat that - accounting: the dropped candidate would then match nothing in - [admitted], and {!Precedence.resolve} would count it as dropped a - SECOND time (once for real, once because its identity no longer - matches its own admitted copy) without ever raising -- a silent - double-count, not a crash, which is exactly why this comment exists. *) + accounting: the original would then match nothing in [admitted], so the + celebration would surface TWICE in the same day -- once in + [commemorations] (the rebuilt copy) and once in [omitted] (the original, + which nothing admitted matches). One admission, double-reported, and no + crash to announce it, which is exactly why this comment exists. *) let sorted = List.stable_sort compare_dignity comms in let is_privileged (_, p) = p = Precedence.Privileged in let observed_rank = observed.Precedence.cel.Celebration.rank in diff --git a/lib/rites/rite_ef/precedence_ef.mli b/lib/rites/rite_ef/precedence_ef.mli index 161d890..55f947e 100644 --- a/lib/rites/rite_ef/precedence_ef.mli +++ b/lib/rites/rite_ef/precedence_ef.mli @@ -135,7 +135,7 @@ val sunday_marker : string can construct: [Vocab_ef.rank] (RG 8) and {!Celebration.status} are both closed variants, and the five cases above -- an if/else-if chain ending in the unconditional [Commemorate] catch-all -- exhaust every value - those two fields can take between them; there is no fifth, + those two fields can take between them; there is no sixth, "unclassified" case the way {!band} needs one, because this function's own return type has no such slot to fall into by accident. *) val disposition : -- cgit v1.3