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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
(** 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.
["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] (with [observed]'s own origin reconstructed as
{!Precedence.Sanctoral}; the real EF admit reads only rank and slug
from [observed], never origin, so this reconstruction is exact for
it) must return exactly that same set. Each offered commemoration's
own origin -- CORRECTED, Task B fix round 1 -- is recovered by
comparing its slug against the day's own temporal office, not
reconstructed as [Sanctoral] uniformly: {!Precedence.rules.admit}
(since Task B) is handed each candidate's own {!Precedence.rules.band}
value, computed here exactly as {!Precedence.resolve} computes it, and
[band] DOES read a candidate's origin (temporal- vs sanctoral-keyed
branches) even though EF's own [admit] itself still does not -- a
mislabelled origin would silently score the wrong table entry for a
genuinely temporal-origin commemoration (e.g. a Lent feria) before
this fix. 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.
Two further labels (Task 10) check the day's reading {!Citation.t}s. Both
are GATED on the rite producing at least one citation somewhere in the
year: a rite whose lectionary is not built returns [[]] from
{!Rite.readings} on every day and is held to neither, so this stays a
check on rites that HAVE readings rather than a demand that every rite
have them.
- ["citations"]: well-formedness. A day's citation parts, sorted, are
exactly [[First; Gospel]]. This single condition carries three
invariants at once: zero or two but never one (an Epistle without a
Gospel, or the reverse, is a malformed Mass rather than a partial one);
no part outside [First]/[Gospel] (the chants -- Psalm, Second, Tract,
Alleluia, Sequence -- are deliberately unbuilt, so one appearing is a
defect, not a feature arriving early); and no part twice (two Epistles
and no Gospel has length two and would pass a bare cardinality test).
- ["citations-unresolved"]: coverage. A day resolved NO citations at all,
i.e. the rite's own lookup chain fell through every one of its steps.
Deliberately a separate label from ["citations"] above: a coverage gap
and a well-formedness fault want different fixes and should be
countable apart. On the EF data as it stands this label has no live
witness -- every day of every year 1583..9999 resolves exactly one
Epistle and one Gospel -- which is precisely why test_validate.ml
carries a synthetic fixture proving it can fire at all.
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
|
