summaryrefslogtreecommitdiff
path: root/lib/kernel
diff options
context:
space:
mode:
authorLukasz Kasprzak <lukas@labunix.xyz>2026-08-12 11:38:35 +0200
committerLukasz Kasprzak <lukas@labunix.xyz>2026-08-12 11:38:35 +0200
commite19adb9c7ea369cafe76e7eff50e9248a4a954d0 (patch)
tree57824e121606286ebdf8fff68439986dd3300eae /lib/kernel
parent0506388da160a15ceddb0cea1a697d737103d5c4 (diff)
parent36df2bd0af9a555a09334e14b0d89118be1dbbc0 (diff)
downloadcolitur-e19adb9c7ea369cafe76e7eff50e9248a4a954d0.tar.gz
colitur-e19adb9c7ea369cafe76e7eff50e9248a4a954d0.zip
Merge branch 'ef-plan3': Plan 3, the EF resolution engine
Adds the rite-parameterised Precedence resolver, Liturgical_day, Rite, and Calendar (year as the primitive, because transfers need whole-year knowledge), the full EF precedence ruleset (RG 91's 28-entry table, occurrence RG 92-95, commemorations RG 108-111, transfers RG 96-98), 322 bootstrapped sanctoral entries, colitur day <year>, and validation layers 3-5. Layer 3 diffs 16801 days against lectio; layer 4 diffs 730 days against missalemeum; layer 5 pins ~30 dates on the known-tricky years. Both comparison layers carry cited allow-lists that name the governing RG paragraph and which engine is right. The oracle layer earned its place immediately: Holy Thursday was violet in colitur and lectio alike, because colitur's data was bootstrapped from lectio and both carried the same error. Only an independent source could see it. RG 128(b) and RG 122 name it white.
Diffstat (limited to 'lib/kernel')
-rw-r--r--lib/kernel/calendar.ml387
-rw-r--r--lib/kernel/calendar.mli72
-rw-r--r--lib/kernel/celebration.ml13
-rw-r--r--lib/kernel/celebration.mli12
-rw-r--r--lib/kernel/liturgical_day.ml27
-rw-r--r--lib/kernel/liturgical_day.mli25
-rw-r--r--lib/kernel/precedence.ml69
-rw-r--r--lib/kernel/precedence.mli78
-rw-r--r--lib/kernel/rite.ml14
-rw-r--r--lib/kernel/rite.mli62
-rw-r--r--lib/kernel/slug.ml8
-rw-r--r--lib/kernel/validate.ml194
-rw-r--r--lib/kernel/validate.mli79
-rw-r--r--lib/kernel/vocab.ml25
-rw-r--r--lib/kernel/vocab.mli25
15 files changed, 1044 insertions, 46 deletions
diff --git a/lib/kernel/calendar.ml b/lib/kernel/calendar.ml
new file mode 100644
index 0000000..5d3572c
--- /dev/null
+++ b/lib/kernel/calendar.ml
@@ -0,0 +1,387 @@
+(* 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.
+
+ [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)
+
+(* RG 91's contest for one date: the temporal office against every sanctoral
+ 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 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:(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)"
+
+(* 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
+ 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).
+
+ 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
+ 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.
+
+ [~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
+ 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, 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) ->
+ 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
+ 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
+ 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, 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] (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, ('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 =
+ 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 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
+ 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. 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
+ 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, reason_for c)))
+ in
+ {
+ 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;
+ transferred_out;
+ omitted;
+ 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
+ let dates = Array.init n (fun i -> Date.add_days start i) 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, ('r Celebration.t * Date.t) list) Hashtbl.t = Hashtbl.create 16 in
+ Hashtbl.iter
+ (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;
+ (* 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 =
+ 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..1c0b0ed
--- /dev/null
+++ b/lib/kernel/calendar.mli
@@ -0,0 +1,72 @@
+(** 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.
+
+ 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
+ (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
+ [rite.year_start (y + 1)], inclusive of both ends.
+
+ 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
+ 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/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
diff --git a/lib/kernel/liturgical_day.ml b/lib/kernel/liturgical_day.ml
new file mode 100644
index 0000000..bbb52b8
--- /dev/null
+++ b/lib/kernel/liturgical_day.ml
@@ -0,0 +1,27 @@
+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 : ('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 *)
+ 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..a109251
--- /dev/null
+++ b/lib/kernel/liturgical_day.mli
@@ -0,0 +1,25 @@
+(** 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 : ('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 *)
+ citations : Citation.t list; (** always empty until Plan 4 *)
+}
+[@@deriving sexp]
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..ae054dd
--- /dev/null
+++ b/lib/kernel/precedence.mli
@@ -0,0 +1,78 @@
+(** 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.
+
+ 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} 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. *)
+}
+
+(** 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/lib/kernel/rite.ml b/lib/kernel/rite.ml
new file mode 100644
index 0000000..89fceb6
--- /dev/null
+++ b/lib/kernel/rite.ml
@@ -0,0 +1,14 @@
+(* 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;
+ 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
new file mode 100644
index 0000000..ffe9471
--- /dev/null
+++ b/lib/kernel/rite.mli
@@ -0,0 +1,62 @@
+(** 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). *)
+ 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".
+
+ 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/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/validate.ml b/lib/kernel/validate.ml
index 7be3425..cc8bdce 100644
--- a/lib/kernel/validate.ml
+++ b/lib/kernel/validate.ml
@@ -20,7 +20,35 @@ 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 =
+(* 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],
+ 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
+ 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
@@ -68,18 +96,16 @@ let run vocab ~year_start ~temporal ~anchors ~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)
@@ -97,9 +123,28 @@ let run vocab ~year_start ~temporal ~anchors ~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 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 +153,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"
@@ -157,4 +202,121 @@ let run vocab ~year_start ~temporal ~anchors ~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 709a711..5e55fc5 100644
--- a/lib/kernel/validate.mli
+++ b/lib/kernel/validate.mli
@@ -5,26 +5,71 @@ 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 layer ~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.
+
+ ["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
+ 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) 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 -> 'r Layer.t -> year:int -> failure list
diff --git a/lib/kernel/vocab.ml b/lib/kernel/vocab.ml
index 78729bb..a4e61a3 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] 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..a4e61a3 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] 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;
}