From 2b9f8133a22ce6dc309644a98bbe61507f574b38 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Mon, 17 Aug 2026 17:22:43 +0200 Subject: feat(kernel): movable Date_spec variants, and Rogation Wednesday Date_spec carried one variant, Fixed(month, day), and its own header said Sunday- and Easter-relative forms would arrive with the OF sanctoral. They arrive early because two things needed them at once: a user-supplied overlay carrying a local movable feast had no way to express "the first Sunday of October", and Rogation Wednesday's commemoration has been recorded as architecturally blocked since 2026-08-13. That blockage turns out to have been a premise, not a fact. The register concluded the Rogation "is not Commemoration_only sanctoral data by nature... it needs a genuinely THIRD kind of thing this architecture has no name for" -- but the reasoning rested on there being "no civil (month, day) pair to anchor a Fixed entry to". That is a statement about Date_spec's expressiveness. With Easter_offset the entity is ordinary sanctoral data, the identical shape Add major-litanies already ships, differing only in how the date is written. No third channel was needed. The register is corrected rather than left contradicting the code. Two variants: Easter_offset of int, and Nth_weekday of {month; nth; weekday} with negative nth counting from the end. Fixed's sexp representation is untouched, so all 327 sanctoral entries and the whole overlay parse unchanged. Both are re-validated in t_of_sexp through their smart constructors, extending the idiom Fixed already used -- the failure that guards against is invisible, a spec deserialising into something that silently never resolves and a celebration vanishing with no diagnostic. Easter is supplied by the rite, not computed in the kernel. Computus ships Gregorian and Julian both, and picking one here would hard-code a Roman assumption into rite-agnostic code and be silently wrong for a Julian-reckoning rite. Rite.t gains an easter field; Rite_ef supplies the Gregorian one. Layer keeps a split index. Fixed entries stay in the year-independent (month, day) table, which preserves the fast path and the "30 November counted twice in a 371-day span" behaviour validate.mli documents for St Andrew. Movable entries have no year-independent key by construction -- the same spec lands on a different (month, day) each year -- so they resolve per civil year into a rata-die table. index_by_date is removed rather than kept as an alias: two ways to index a layer, one of which silently ignores movable entries, is the trap this change exists to avoid. Two domain-edge defects, both found by the suite rather than reasoning. A liturgical year is Advent-anchored, so resolving civil year y names y +/- 1, and at the edges those are 1582 and 10000, which Computus correctly refuses by raising. The ceiling surfaced through the domain-ceiling test, the floor through `colitur day 1583` failing outright. Fixed once, in Layer.index, the single point that calls the rite's easter -- a clamp repeated per caller would have been two places to get wrong a third time. Rogation Wednesday: RG 87 assigns the Litaniae minores to the Monday, Tuesday AND Wednesday before Ascension (scan1:691); colitur built the first two from the start and never the third. RG 88 keeps it out of the Office, so the Ascension Vigil remains observed. RG 89 routes it through the Major Litanies' rules, but RG 109's closed list names only maiores, so by RG 107 it is an ORDINARY commemoration -- confirmed in the output, not assumed. Name from the Missal's own "feria IV" (scan1:20495-20497), violet to match the Monday and Tuesday offices. Blast radius, full 1583-9999 sweep against the pre-change binary: 2257 days, every one the same shape, zero unclassified, line counts equal both sides. The complement is the informative half -- in the other 6160 years the Rogation does not appear at all, because RG 111 admits one commemoration on a II-class day and an impeded feast takes it under RG 113, a Commemoration_only candidate having no row in RG 91's table. Both shapes are pinned. Allow-lists unmoved: layer 3 compares no commemorations and is blind by construction, and layer 4's 2026-2027 window has a competing feast on both Wednesdays, so the Rogation is capped out in exactly the years the oracle can see. C8 is unchanged, asserted by its own count pin. Not built: Sunday-relative specs, which nothing needs yet, and the --overlay plumbing that would let a user actually supply a local movable feast. Nth_weekday therefore ships with synthetic and property coverage only; inventing a shipped entry to exercise it would be fabricating calendar data. Register: section 6.10. --- lib/kernel/date_spec.mli | 46 +++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 41 insertions(+), 5 deletions(-) (limited to 'lib/kernel/date_spec.mli') diff --git a/lib/kernel/date_spec.mli b/lib/kernel/date_spec.mli index 3fe9625..70a3030 100644 --- a/lib/kernel/date_spec.mli +++ b/lib/kernel/date_spec.mli @@ -1,9 +1,45 @@ -(** A sanctoral entry's date expression. *) -type t = Fixed of { month : int; day : int } [@@deriving sexp] +(** A sanctoral entry's date expression. + + [Fixed] is a civil (month, day) that recurs every year. The other two move: + [Easter_offset] is a signed day count from the rite's own Easter, and + [Nth_weekday] is the nth (or nth-from-last) given weekday of a month. + + Sunday-relative forms ("the Sunday on or after 2 November") are + deliberately absent: nothing in this repository needs one yet, and the same + mechanism admits them when something does. *) +type t = + | Fixed of { month : int; day : int } + | Easter_offset of int + | Nth_weekday of { month : int; nth : int; weekday : Date.weekday } +[@@deriving sexp] (** Validates against the leap-year maximum, so 29 February is constructible. *) val fixed : month:int -> day:int -> (t, string) result -(** [None] when the spec does not occur in that year (29 February in a common - year) or falls outside the supported domain. *) -val resolve : t -> year:int -> Date.t option +(** Rejects an offset further than a year from Easter in either direction -- + past that, a spec is a data error rather than a calendar. Deliberately + generous: Septuagesima is Easter-63 and Time after Pentecost runs well past + Easter+180. *) +val easter_offset : int -> (t, string) result + +(** [nth] is 1-based forward, or negative from the end ([-1] is the last). + Rejects [nth = 0] (meaningless), [|nth| > 5] (no month has six of any + weekday), and a month outside 1..12. *) +val nth_weekday : month:int -> nth:int -> weekday:Date.weekday -> (t, string) result + +(** [resolve spec ~year ~easter] is the civil date [spec] denotes in [year], + where [easter] is that year's Easter as the RITE reckons it -- supplied by + the caller, never computed here, since {!Computus} ships both Gregorian and + Julian and choosing one in the kernel would be silently wrong for a + Julian-reckoning rite. + + [None] means "this spec does not occur in that year", per variant: + - [Fixed]: 29 February in a common year, or a date outside 1583..9999. + - [Easter_offset]: the resolved date falls outside 1583..9999. This is + reachable at the domain edges -- {!Date.add_days} is unbounded total + arithmetic and will happily denote a date outside the domain. + - [Nth_weekday]: the month has no such occurrence (a fifth Sunday it + lacks). + + Total: never raises on any in-range year, for any constructible spec. *) +val resolve : t -> year:int -> easter:Date.t -> Date.t option -- cgit v1.3