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
|
(** 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:
- 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).
KNOWN UNIMPLEMENTED FOURTH RULE, recorded rather than built (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 every rule above. It is
conditional ("ubi est de praecepto servanda") and the following sentence
gives Episcopal Conferences discretion where it is not, so the universal
calendar legitimately not implementing it is defensible; not citing it at
all was not, hence this note.
CORRECTED: this note previously said "No sanctoral data exists yet
(Phase 3), so nothing is WRONG today" and located the trigger at
"25 March co-occurring with Palm Sunday". Both are now false and were
already wrong about the date: St Joseph is 19 March, not 25 March (25
March is the Annunciation, a separate solemnity with its own Holy-Week
handling). Phase 3 shipped sanctoral data on this same branch
(data/of/calendar-2002.sexp), so the defect this note warns about is now
LIVE: 19 March coincides with Palm Sunday in 16 of the 1583-2100 years
(e.g. 2062), and St Joseph lands forward at Easter+9 via rule 3 instead
of anticipated backward to 18 March. Pinned, not silently wrong: see
test_rite_of.ml's [test_joseph_palm_sunday_2062_known_wrong_forward_transfer]
(2062, both grade and identity) and allow-list entries L8/L9
(data/of/expected-divergences-litcal.sexp, 2035-03-17, a second, distinct
year witnessing the same limitation).
Implementing it would need either a kernel signature change (out of
scope for this rite module and forbidden by this fix wave) or a
deliberate violation of a documented obligation {!Colitur_kernel.Calendar}
depends on: n. 60's own text is "ad proximiorem diem transferatur" --
the NEAREST day, not "proximiorem diem SEQUENTEM" (the nearest
FOLLOWING one) -- yet every branch above only ever searches or lands
forward. The strictly-LATER reading is not this rite's own choice; it is
imposed by {!Colitur_kernel.Rite.t.transfer_target}'s own contract
(rite.mli:77-84), which is justified there purely by the EF's RG 96. That
is EF-shaped vocabulary constraining rite-agnostic kernel code -- the same
class of item CLAUDE.md already tracks under "EF-shaped things still in
rite-agnostic kernel code" -- so a real fix has to start at the kernel
field, not in this module.
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 is strictly later than [origin], 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.
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
|