diff options
Diffstat (limited to 'lib/kernel/validate.mli')
| -rw-r--r-- | lib/kernel/validate.mli | 46 |
1 files changed, 43 insertions, 3 deletions
diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli index d281f9a..511c78f 100644 --- a/lib/kernel/validate.mli +++ b/lib/kernel/validate.mli @@ -5,8 +5,9 @@ type failure = { year : int; date : string; check : string; detail : string } val failure_to_string : failure -> string -(** [run rite ~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. [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 @@ -21,8 +22,47 @@ val failure_to_string : failure -> string 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) Rite.t -> year:int -> failure list +val run : ('s, 'r) Rite.t -> 'r Layer.t -> year:int -> failure list |