aboutsummaryrefslogtreecommitdiff
path: root/lib/kernel/celebration.mli
diff options
context:
space:
mode:
authorLukasz Kasprzak <lukas@labunix.xyz>2026-08-12 02:12:03 +0200
committerLukasz Kasprzak <lukas@labunix.xyz>2026-08-12 02:12:03 +0200
commit633306c8a5ac1854f30749f498498104ebc84edc (patch)
tree7f491a8645c0eb1bf3130ae6ecf51ee18cb8f7cf /lib/kernel/celebration.mli
parent9ce4527550fed24036f6f116474c1f67714f5194 (diff)
downloadcolitur-633306c8a5ac1854f30749f498498104ebc84edc.tar.gz
colitur-633306c8a5ac1854f30749f498498104ebc84edc.zip
kernel(validate): resolution invariants
Widen Validate.run to take the rite's sanctoral layer alongside the rite itself (Calendar.year needs both), and add five checks over the fully resolved liturgical year, on top of the existing temporal-only pass: - observed: a day's observed celebration never also appears among that same day's own commemorations/omissions. - lost: no sanctoral entry is silently dropped. Per slug, the number of times it is actually sighted (observed + commemorations + omitted, summed over the year) must never fall below the number of times its own Date_spec resolves within the year's span -- also fires if resolving the year raises at all, the most total form of loss. - duplicated: the same per-slug count must never exceed the number of Date_spec resolutions either. Deliberately NOT "no slug appears twice": a fixed date can legitimately resolve twice in the ~20% of liturgical years whose 371-day span reaches it on both ends (30 November/St Andrew is the worked example in validate.mli). - unconverged: no day's omitted reason indicates Calendar's placement pass hit its round guard before reaching a fixed point. - admission: the rite's own rules.admit is a fixed point on what it already admitted -- the rite-agnostic form of "the admission limit was not exceeded" available without embedding a rite's own numeric caps (RG 111's, for EF) into kernel code. Each check has a dedicated negative fixture in the synthetic rite (test_validate.ml), hand-traced against Calendar's actual resolution mechanics before writing the assertion, and verified to fail for the right reason against the code before this change. One pair (unconverged/duplicated) is not fully independent: hitting the round guard genuinely also trips duplicated, a real consequence of Calendar's own accounting once a candidate is simultaneously sighted at its permanent natural date and wherever the last placement round left it -- documented in guard_rules's own comment, not papered over. test_validate.ml's ef_rite/run now use the real Rite_ef.context and the real bootstrapped data/ef layer (Precedence_ef and the sanctoral bootstrap did not exist when this scaffolding was first written) rather than the earlier placeholder rules. Validate is clean across the whole 1583..9999 domain against real EF data except the one already-documented year-9999 truncation case (test_year_9999_does_not_raise).
Diffstat (limited to 'lib/kernel/celebration.mli')
0 files changed, 0 insertions, 0 deletions