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.mli | 60 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 lib/kernel/precedence.mli (limited to 'lib/kernel/precedence.mli') 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 -- 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/precedence.mli') 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 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/precedence.mli') 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