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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
(** The Tabula dierum liturgicorum of the 2002 Missale Romanum -- 13 numbered
entries in three parts -- plus Normae n. 60's occurrence and transfer
rules. The OF counterpart of {!Rite_ef.Precedence_ef}, and deliberately
the same shape.
Every citation names its document ("Normae n. N" or "IGMR n. N"): the
2002 Missal carries both, independently numbered from 1. *)
open Colitur_kernel
(** Returned for a candidate shape the Tabula has no row for. [max_int], so an
unclassified candidate always loses. Task 4's property asserts this is
never reached by anything {!Rite_of.Temporal_of} constructs. *)
val unclassified : int
(** The universal (General Roman Calendar) layer id. Not a Normae citation:
the Tabula distinguishes universal entries (3, 7, 10) from proper ones
(4, 8, 11), and [Celebration.t.layer] is the only field carrying that
distinction. *)
val universal_layer : string
(** Prefix marking a candidate as belonging to a PROPER (diocesan, national or
religious) calendar -- Tabula entries 4, 8 and 11.
NO SHIPPED DATA PRODUCES THIS. Phase 3 transcribes the General Roman
Calendar only (the spec's own universal-calendar-only discipline), so
entries 4, 8 and 11 are unreachable on shipped data and are exercised in
tests by synthetic candidates alone. They are transcribed anyway for two
reasons: the transcription of a 13-entry table should be complete rather
than silently 10 entries long, and a user [--overlay] carrying a local
patron becomes correct without a later edit here. *)
val proper_prefix : string
(** [band ctx c]: the Tabula's own entry number for [c], TIMES TEN (entry 1 ->
10, entry 13 -> 130); lower wins. {!unclassified} for a shape with no row.
The ×10 scaling matches {!Rite_ef.Precedence_ef.band} and exists for the
same reason: a future sub-rank fits between neighbours without rescaling
the table. *)
val band : Vocab_of.season Precedence.context -> Vocab_of.rank Precedence.candidate -> int
(** [disposition ~winner ~loser]: Normae n. 60. An impeded SOLEMNITY is
{!Colitur_kernel.Precedence.Transfer}red; every other losing celebration is
{!Colitur_kernel.Precedence.Omit}ted -- "Reliquae celebrationes eo anno
omittuntur".
NEVER RETURNS [Commemorate], AND THAT IS THE RULE RATHER THAN A GAP: the OF
has no commemoration of a losing celebration in the EF's sense. An optional
memorial is an election, not a commemoration. Consequently
{!Colitur_kernel.Liturgical_day.t.commemorations} is permanently empty for
this rite, and {!Colitur_kernel.Precedence.privilege} is meaningless here.
[winner] is unread: n. 60 keys the outcome on the loser's own grade alone,
unlike the EF's RG 92-95. *)
val disposition :
winner:Vocab_of.rank Precedence.candidate ->
loser:Vocab_of.rank Precedence.candidate ->
Precedence.disposition
(** [admit]: always the empty list. The OF admits no commemorations at all --
the direct consequence of {!disposition} never returning [Commemorate], and
argued from the same Normae n. 60. Not a stub: every losing candidate is
still reported in {!Colitur_kernel.Precedence.resolution.omitted} with its
reason, so nothing is dropped silently. All three parameters are unread. *)
val admit :
observed:Vocab_of.rank Precedence.candidate ->
temporal:Vocab_of.rank Precedence.candidate ->
(Vocab_of.rank Precedence.candidate * Precedence.privilege * int) list ->
(Vocab_of.rank Precedence.candidate * Precedence.privilege) list
(** [vigil_feast]: always [None]. RG 33's third omission trigger is EF-only;
the OF has no vigil OFFICE that its feast's movement could orphan --
Normae nn. 11/13 create no such independent celebration for anything
other than "of-nativity-vigil". THAT candidate is not exempt by lacking
standing: {!Rite_of.Temporal_of.named} constructs it as its own
Sollemnitas-rank candidate on 24 December, a genuine contestant in
{!band}/{!Colitur_kernel.Precedence.resolve}. It is exempt structurally
instead -- the Nativity (Tabula entry 2, band 20) can only ever be beaten
by the Triduum (entry 1, band 10), whose window (Easter-2..Easter) is
confined to 20 March-25 April because Gregorian Easter never falls outside
[22 March, 25 April] (measured exhaustively, 1583-9999, not assumed), so
it can never reach 25 December. The Nativity therefore always keeps its
own day, and its vigil can never be orphaned. *)
val vigil_feast : Vocab_of.rank Precedence.candidate -> Slug.t option
(** The four functions assembled for {!Colitur_kernel.Precedence.resolve}. *)
val rules : (Vocab_of.season, Vocab_of.rank) Precedence.rules
(** [transfer_target c origin occupant]: where an impeded solemnity goes.
Normae n. 60 and Normae n. 5 together -- n. 60 defers to n. 5 explicitly
("servatis iis quae n. 5 statuuntur"), so they are one rule set:
- St Joseph, impeded by falling on Palm Sunday, is ANTICIPATED BACKWARD to
the preceding Saturday, 18 March (n. 56(f), a fixed one-day
displacement, checked first as the most specific collision);
- the Annunciation falling anywhere in Holy Week goes to Easter + 8, the
Monday after the Second Sunday of Easter (n. 60, a fixed destination);
- any other solemnity falling on a Sunday of Advent, Lent or Easter goes to
the following Monday (n. 5), except on Palm Sunday or Easter Sunday,
which n. 5 excludes and which fall through to the general rule;
- otherwise, the nearest later day free of Tabula entries 1-8 (n. 60).
FOURTH RULE RESOLVED ([of-normae-56f]/W1, 2026-08-26; previously KNOWN
UNIMPLEMENTED here, final review Important #5, ledger ruling R9). Normae
n. 56(f): "Sollemnitas S. Ioseph, ubi est de praecepto servanda, si cum
Dominica in palmis de Passione Domini occurrit, anticipatur sabbato
praecedenti, die 18 martii" -- St Joseph, where his solemnity is of
precept, falling on Palm Sunday is ANTICIPATED (a BACKWARD transfer) to
the preceding Saturday, 18 March, not carried forward like the other
three rules. It is conditional ("ubi est de praecepto servanda") and the
following sentence gives Episcopal Conferences discretion where it is
not; the universal calendar implements the unconditional reading (the
same discipline every other rule here already applies to a Normae
clause with a conference-discretion escape hatch).
HISTORY (kept for the record; the defect is fixed, not merely
documented, as of this revision). 19 March coincides with Palm Sunday
in 16 of the 1583-2100 years (e.g. 2062), and before this fix St Joseph
landed forward at Easter+9 via rule 3 instead of anticipated backward
to 18 March -- pinned on that shape until this revision, in
test_rite_of.ml's own now-renamed/re-asserted test (previously
[test_joseph_palm_sunday_2062_known_wrong_forward_transfer]; see that
file for its corrected form) and allow-list entries L8/L9
(data/of/expected-divergences-litcal.sexp) -- L8/L9 name a DIFFERENT
year, 2035-03-17, where St Joseph is impeded by Holy Monday rather than
coinciding with Palm Sunday itself, so n. 56(f)'s own trigger does not
apply there; that instance of the general rule's forward-only reach is
untouched by this fix and remains open on its own terms.
What unblocked it: {!Colitur_kernel.Rite.t.transfer_target}'s own
contract (rite.mli) used to require the result be STRICTLY LATER than
[origin] -- an obligation argued there purely from the EF's RG 96, i.e.
EF-shaped vocabulary constraining rite-agnostic kernel code, the same
class of item CLAUDE.md tracks under "EF-shaped things still in
rite-agnostic kernel code". Traced against {!Colitur_kernel.Calendar}'s
actual placement pass (calendar.ml's [place_transfers]/[year], not
against the obligation's own prior wording) rather than assumed unsafe:
the round loop re-resolves the whole year fresh every round with no
comparison against [origin] anywhere in its two safety nets ([~start]/
[~stop]; the round-count guard), so a target earlier than [origin] is
handled identically to a later one. The kernel contract was relaxed
(rite.mli, [transfer_target]'s own comment carries the full argument)
from "strictly later" to "different from origin" -- the one requirement
the trace showed is still load-bearing (a same-day target would hand
{!Colitur_kernel.Precedence.resolve} the same candidate twice, which it
does not deduplicate). No change was needed in calendar.ml's actual
logic; two of its comments were corrected for accuracy (the round-guard
rationale and the out-of-range rationale both previously asserted
"every genuine transfer moves forward" as a blanket fact).
Shaped to match {!Colitur_kernel.Rite.t.transfer_target} exactly so a later
phase wires it with no adaptation, and honours both obligations that field
states: the result differs from [origin] (rule 0's own [Date.add_days
origin (-1)] trivially satisfies this, going backward rather than
forward), and the search carries its own step bound rather than relying
on {!Colitur_kernel.Calendar}'s round guard, which bounds rounds rather
than one call's internal search (rule 0 needs no bound at all -- it runs
no search, so it terminates trivially).
Never raises. If no free day is found within 400 days, or the walk would
otherwise have to probe past 31 December 9999 (past which
{!Colitur_kernel.Computus.gregorian_easter} is not total), the last date
visited is returned instead -- {!Colitur_kernel.Calendar}'s own
[~start]/[~stop] bound turns that into a recorded [omitted], not a crashed
CLI. Same shape as [Rite_ef.Precedence_ef.search_from]
(precedence_ef.ml:1895-1899) -- named in prose, not a doc cross-reference:
[rite_of]'s dune library does not depend on [rite_ef]. *)
val transfer_target :
Vocab_of.rank Precedence.candidate ->
Date.t ->
(Date.t -> Vocab_of.rank Celebration.t) ->
Date.t
|
