1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
(** The invariant harness -- validation layer 2. Checks run over a *liturgical*
year, not a civil year: a season that straddles January would otherwise look
as though it recurs. *)
type failure = { year : int; date : string; check : string; detail : string }
val failure_to_string : failure -> string
(** [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
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.
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) Rite.t -> 'r Layer.t -> year:int -> failure list
|
