summaryrefslogtreecommitdiff
path: root/lib/kernel/date_spec.ml
diff options
context:
space:
mode:
authorLukasz Kasprzak <lukas@labunix.xyz>2026-08-17 17:22:43 +0200
committerLukasz Kasprzak <lukas@labunix.xyz>2026-08-17 17:22:43 +0200
commit2b9f8133a22ce6dc309644a98bbe61507f574b38 (patch)
treeedb24a59d092f56f00dcbca654224a0622725d5e /lib/kernel/date_spec.ml
parentf2a0660a9b60b70af32f1157dc78cdfcb298c9f7 (diff)
downloadcolitur-2b9f8133a22ce6dc309644a98bbe61507f574b38.tar.gz
colitur-2b9f8133a22ce6dc309644a98bbe61507f574b38.zip
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.
Diffstat (limited to 'lib/kernel/date_spec.ml')
-rw-r--r--lib/kernel/date_spec.ml120
1 files changed, 104 insertions, 16 deletions
diff --git a/lib/kernel/date_spec.ml b/lib/kernel/date_spec.ml
index 732f6b1..6b328df 100644
--- a/lib/kernel/date_spec.ml
+++ b/lib/kernel/date_spec.ml
@@ -1,14 +1,33 @@
open Sexplib0.Sexp_conv
-(* How a sanctoral entry expresses its date. Plan 2 ships the only form the EF
- sanctoral needs -- a fixed calendar date -- because EF movable feasts come
- from the rite's temporal code, not from data. Sunday-relative and
- Easter-relative forms arrive with the OF sanctoral. *)
+(* How a sanctoral entry expresses its date.
+
+ Plan 2 shipped [Fixed] alone, and this file's own header then said
+ "Sunday-relative and Easter-relative forms arrive with the OF sanctoral".
+ They arrive here instead, ahead of OF, because two things needed them at
+ once: user-supplied overlays carrying LOCAL MOVABLE FEASTS (a patronal
+ feast on "the first Sunday of October" was simply inexpressible), and
+ ROGATION WEDNESDAY's own commemoration (RG 87/88/89), recorded as
+ architecturally blocked since 2026-08-13 for exactly one reason -- its
+ trigger is Easter+38, and there is no (month, day) pair a [Fixed] spec
+ could anchor to.
+
+ Sunday-relative forms ("the Sunday on or after 2 November") are still NOT
+ built: no entry in this repository needs one, and the same mechanism adds
+ them when one does. See
+ docs/superpowers/specs/2026-08-17-colitur-movable-date-specs-design.md. *)
module Repr = struct
- type t = Fixed of { month : int; day : int } [@@deriving sexp]
+ type t =
+ | Fixed of { month : int; day : int }
+ | Easter_offset of int
+ | Nth_weekday of { month : int; nth : int; weekday : Date.weekday }
+ [@@deriving sexp]
end
-type t = Repr.t = Fixed of { month : int; day : int }
+type t = Repr.t =
+ | Fixed of { month : int; day : int }
+ | Easter_offset of int
+ | Nth_weekday of { month : int; nth : int; weekday : Date.weekday }
(* Leap-year maximum, so 29 February is constructible; it simply does not
resolve in a common year. *)
@@ -24,20 +43,89 @@ let fixed ~month ~day =
Error (Printf.sprintf "date_spec: day %d out of range for month %d" day month)
else Ok (Fixed { month; day })
-let resolve t ~year =
+(* Deliberately generous rather than tight. Septuagesima is Easter-63 and Time
+ after Pentecost runs well past Easter+180, so a bound that merely LOOKED
+ precise would reject legitimate specs; a full year either way is the point
+ past which a spec is certainly a data error rather than a calendar. *)
+let easter_offset n =
+ if n < -365 || n > 365 then
+ Error (Printf.sprintf "date_spec: easter offset %d is further than a year from Easter" n)
+ else Ok (Easter_offset n)
+
+(* [nth] is 1-based forward, or negative from the end (-1 = the last). Zero is
+ meaningless, and no month has a sixth of any weekday. *)
+let nth_weekday ~month ~nth ~weekday =
+ if month < 1 || month > 12 then Error (Printf.sprintf "date_spec: month %d out of range 1..12" month)
+ else if nth = 0 then Error "date_spec: nth = 0 is meaningless (1 is the first, -1 the last)"
+ else if nth < -5 || nth > 5 then
+ Error (Printf.sprintf "date_spec: nth %d out of range (no month has six of a weekday)" nth)
+ else Ok (Nth_weekday { month; nth; weekday })
+
+(* The domain check on [Easter_offset] is load-bearing, not defensive
+ decoration: date.mli states plainly that [add_days] is "unbounded total
+ arithmetic (they may denote a date outside the domain)", so Easter+200 in
+ 9999 yields a perfectly well-formed [Date.t] that is nonetheless outside
+ 1583..9999. Returning it would leak an out-of-domain date into a [Layer]
+ index and from there into resolution. [None] is the same answer 29 February
+ already gives in a common year: "this spec does not occur". *)
+let in_domain d = Date.year d >= 1583 && Date.year d <= 9999
+
+let weekday_index = function
+ | Date.Sun -> 0
+ | Date.Mon -> 1
+ | Date.Tue -> 2
+ | Date.Wed -> 3
+ | Date.Thu -> 4
+ | Date.Fri -> 5
+ | Date.Sat -> 6
+
+(* Total: every branch returns [option], and nothing here raises on an in-range
+ year. *)
+let resolve t ~year ~easter =
match t with
| Fixed { month; day } -> Result.to_option (Date.make ~year ~month ~day)
+ | Easter_offset n ->
+ (* [easter] is the caller's Easter for THIS civil year -- the rite
+ supplies it ({!Rite.t}'s own [easter] field), so a Julian-reckoning
+ rite is never silently handed a Gregorian date. *)
+ let d = Date.add_days easter n in
+ if in_domain d then Some d else None
+ | Nth_weekday { month; nth; weekday } -> (
+ match Date.make ~year ~month ~day:1 with
+ | Error _ -> None
+ | Ok first ->
+ (* [Date.make] is the authority on month length, so no leap rule is
+ duplicated here: probe downward from 31 for the last day that
+ actually constructs. Every month has at least 28. *)
+ let rec last_day d =
+ if d <= 28 then d else if Result.is_ok (Date.make ~year ~month ~day:d) then d else last_day (d - 1)
+ in
+ let days_in_month = last_day 31 in
+ let offset_to_first = (weekday_index weekday - weekday_index (Date.weekday first) + 7) mod 7 in
+ let first_occurrence = 1 + offset_to_first in
+ let count = ((days_in_month - first_occurrence) / 7) + 1 in
+ (* Negative [nth] counts back from the end: -1 is the last. *)
+ let index = if nth > 0 then nth else count + nth + 1 in
+ if index < 1 || index > count then None
+ else Result.to_option (Date.make ~year ~month ~day:(first_occurrence + ((index - 1) * 7))))
let sexp_of_t = Repr.sexp_of_t
(* Validating parser, matching Slug and Lang: [ppx_sexp_conv]'s derived
- [t_of_sexp] (relocated to [Repr] above) accepts any in-range int pair, so
- [(Fixed (month 13) (day 40))] would otherwise deserialise into a spec that
- silently never resolves -- a saint quietly vanishing with no diagnostic.
- Re-running the value through [fixed] closes that gap the same way loaders
- already close it for slugs and language codes. *)
+ [t_of_sexp] (relocated to [Repr] above) accepts any in-range int, so
+ [(Fixed (month 13) (day 40))] or [(Nth_weekday (month 10) (nth 0) ...)]
+ would otherwise deserialise into a spec that silently never resolves -- a
+ celebration quietly vanishing with no diagnostic. Re-running the value
+ through the smart constructors closes that gap the same way loaders already
+ close it for slugs and language codes.
+
+ EVERY variant is re-validated here. Adding one without extending this
+ function reopens exactly the hole it exists to close, and the failure mode
+ is invisible: nothing errors, a feast simply never appears. *)
let t_of_sexp sexp =
- let (Fixed { month; day }) = Repr.t_of_sexp sexp in
- match fixed ~month ~day with
- | Ok t -> t
- | Error msg -> Sexplib0.Sexp_conv.of_sexp_error msg sexp
+ let reject msg = Sexplib0.Sexp_conv.of_sexp_error msg sexp in
+ match Repr.t_of_sexp sexp with
+ | Fixed { month; day } -> ( match fixed ~month ~day with Ok t -> t | Error msg -> reject msg)
+ | Easter_offset n -> ( match easter_offset n with Ok t -> t | Error msg -> reject msg)
+ | Nth_weekday { month; nth; weekday } -> (
+ match nth_weekday ~month ~nth ~weekday with Ok t -> t | Error msg -> reject msg)