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
|
(** The OF (post-1970) temporal cycle, per the Missale Romanum editio typica
tertia (2002) "Normae universales de anno liturgico et de calendario"
("Normae n. N") and the Institutio Generalis Missalis Romani ("IGMR
n. N") -- the same PDF carries both documents, independently numbered
from 1, so every citation in this rite module names which one it is.
OPEN QUESTION, deliberately NOT settled here (design
2026-08-24-colitur-of-rite-module-design.md §8.1): the OF calendar has
no meaning before 1970, but colitur's kernel domain is 1583..9999, and
this module is computable -- and computed -- across the WHOLE of it,
exactly as {!Rite_ef.Temporal_ef} is. Phase 1 takes no position on
whether a pre-1970 (or, symmetrically, a far-future) answer from this
module means anything liturgically; it only guarantees the arithmetic is
total and the properties below hold everywhere the kernel itself is
total. Refusing, extrapolating, or flagging pre-1970 output specially is
a decision for the phase that wires this module into a {!Colitur_kernel
.Rite.t} and a validation layer with a real oracle to check it
against -- not this one. *)
open Colitur_kernel
(** Normae n. 40: "Tempus Adventus incipit a I Vesperis dominicae quae
incidit in diem 30 novembris vel est huic vicinior" -- Advent begins with
First Vespers of the Sunday falling on 30 November or nearest to it.
Worded identically in substance to EF's own RG 20 ({!Rite_ef.Temporal_ef
.advent_start}), so the same closed-form identity applies: the Sunday
nearest 30 November is, equivalently, three weeks before the last Sunday
on or before 24 December -- see that function's own citation for why
that identity holds for every civil year with no case split. *)
val advent_start : int -> Date.t
(** First day of the liturgical year opening in civil year [y]. Same as
{!advent_start}. *)
val year_start : int -> Date.t
val season : Date.t -> Vocab_of.season
(** Normae n. 38 and the Calendarium Romanum Generale's own January table
(extracted line ~4033: "Dominica post diem 6 ianuarii: In baptismate
Domini Festum"): the Sunday falling AFTER 6 January (never 6 January
itself, even in a year 6 January IS a Sunday -- "post", not "on or
after") carries the feast of the Baptism of the Lord. The January
table's own further note ("Ubi sollemnitas Epiphaniae ad dominicam
transfertur... festum Baptismatis Domini celebratur feria secunda
sequenti") only concerns places that exercise Normae n. 37's LOCAL
option to move Epiphany itself off 6 January -- inapplicable to the
universal calendar this module computes, which keeps Epiphany fixed at
6 January (spec's own EF-precedented "universal calendar only"
discipline), so that Monday-shift clause is never reached here. *)
val baptism_of_the_lord : int -> Date.t
(** Normae n. 35(a) and the December calendarium table's own closing line
(extracted line ~4459: "Dominica infra octavam Nativitatis, vel, ea
deficiente, die 30 decembris: Sanctae Familiae ... Festum"): the Sunday
falling within the Octave of the Nativity (26-31 December), or, that
lacking, 30 December. Movable-with-a-fixed-fallback, the same shape as
EF's own Holy Family/Holy Name ({!Rite_ef.Temporal_ef.holy_family_sunday}
/[holy_name_sunday]) -- CODE for that reason, not sanctoral DATA, unlike
the plain fixed-date entries this window also contains (Stephen 26 Dec,
John 27 Dec, the Holy Innocents 28 Dec), which carry no such fallback
logic and are deferred to Phase 3's calendar data instead (see this
file's own top-of-module comment for the full CODE-vs-DATA argument).
UNLIKE EF's 7-13 January window, which can never be empty of a Sunday,
this 6-day window (26-31 December) CAN be -- confirmed by the fallback
clause's own existence in the primary text, not merely inferred. *)
val holy_family : int -> Date.t
(** Normae n. 36: "Dominica a die 2 ad diem 5 ianuarii occurrens est
Dominica II post Nativitatem" -- the Sunday falling 2-5 January, if any,
is the Second Sunday after the Nativity. [None] when no such Sunday
exists that year (the SAME 2-5 January window as EF's own Holy Name of
Jesus, {!Rite_ef.Temporal_ef.holy_name_sunday} -- a real structural
coincidence between the two rites' calendars, not a shared computation:
OF's Normae carries no "otherwise, on a fixed date" fallback for this
Sunday at all, unlike EF's RG 17(a) -- a year without one simply has no
"Second Sunday after the Nativity" office; {!temporal}'s own dispatch
falls through to an ordinary Christmas-time feria for every day of that
window in such a year). *)
val second_sunday_of_christmas : int -> Date.t option
(** Normae n. 43-44 and the Missale's own "HEBDOMADA XXXIV 'PER ANNUM'"
heading (extracted line 13099: "Dominica ultima 'per annum' fit
sollemnitas ... universorum Regis"): the LAST Sunday before Advent I,
always the Solemnity of Christ the King, always week XXXIV. See
{!temporal}'s own citation on the two-block week arithmetic for the full
derivation this anchors. *)
val christ_the_king : int -> Date.t
(** The named temporal days: the Nativity and its Vigil, Mary Mother of God
(the Nativity's own Octave Day, 1 January), Epiphany, Ash Wednesday,
Palm/Passion Sunday, Easter and the days of its Octave, Ascension,
Pentecost, Trinity Sunday, Corpus Christi, and Christ the King. Returns
(season, slug, colour, rank). Carries no week of its own, for the same
reason {!Rite_ef.Temporal_ef.named} does not: {!temporal} computes it
uniformly via {!week} for every day, named or not, so a named day inside
a numbered season run always carries that run's week.
Deliberately EXCLUDES {!holy_family}, {!second_sunday_of_christmas} and
{!baptism_of_the_lord}: each needs a per-year conditional ([holy_family]
on whether 26-31 December has a Sunday at all; the other two on which
Sunday, if any, actually falls in their own window) that this function's
bare [Date.t -> ... option] shape has no way to express without
threading extra state through every other branch too -- the exact
reason EF's own [named] excludes its structurally identical Holy
Family/Holy Name. {!temporal} applies all three as its own targeted
dispatch instead.
24 December is ALSO conditional, not unconditional like the rest of this
function's fixed dates: it yields [of-nativity-vigil] only when that date
is not itself a Sunday. On a Sunday, [None] is returned so {!temporal}'s
dispatch falls through to {!sunday_slug}'s own [of-advent-sunday-4] --
Tabula I.2/Normae n. 5's Sundays of Advent outrank the Vigil (Tabula
I.3), the same evening-Mass-inside-the-civil-day reasoning already
applied to Holy Thursday (see [named]'s own implementation comment for
the full argument). *)
val named : Date.t -> (Vocab_of.season * string * Colour.t * Vocab_of.rank) option
(** Week within the season, 1-indexed, Sunday-aligned (constant across a
Sunday-to-Saturday span). [None] outside every numbered run -- Christmas
has none at all (Normae's own Christmas-season structure is date-keyed,
never week-keyed: contrast n. 36's "the Sunday falling 2-5 January", a
date range, against n. 30's own "Sundays I, II, III..." for Lent) -- and
Ordinary Time's own numbering is total over both of its runs (Normae
n. 43-44): see {!temporal}'s own citation for the two-block arithmetic
that makes the second run's numbers land correctly on 1..34 with the
final week always 34, INCLUDING the "in some years a week is skipped
entirely" case Normae n. 43's own "thirty-three OR thirty-four" already
names. *)
val week : Date.t -> int option
(** The slug for a Sunday, or [None] if [d] is not a Sunday. *)
val sunday_slug : Date.t -> string option
val id : string
(** Total over 1583..9999: every date yields exactly one temporal identity
(subject to this file's own top-of-module note on what "yields" means
before 1970). *)
val temporal : Date.t -> (Vocab_of.season, Vocab_of.rank) Temporal.t
(** Independent restatement of {!named}'s fixed and Easter-relative dates,
plus {!holy_family}, {!second_sunday_of_christmas} and
{!baptism_of_the_lord}, for civil year [y], paired with the slug each
should carry -- the same anchor-agreement discipline
{!Rite_ef.Temporal_ef.anchors} follows, for the same reason: catches an
accidental single-site drift in an offset rather than leaving it
invisible. Not wired into {!Colitur_kernel.Validate.run} in this phase
(that needs a full {!Colitur_kernel.Rite.t}, Phase 2's own deliverable),
but kept in the same shape so that wiring is a straight reuse. *)
val anchors : int -> (string * Date.t) list
|
