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
|
(* The invariant harness: validation layer 2 of the spec's five. Checks run over
a LITURGICAL year (year_start y .. year_start (y+1) - 1), not a civil year:
Christmastide straddles January, so over a civil year it would falsely appear
to recur and break the contiguity check. *)
type failure = { year : int; date : string; check : string; detail : string }
let failure_to_string f =
Printf.sprintf "%d %s [%s] %s" f.year f.date f.check f.detail
(* The kernel's domain ends at year 9999 (Date.make's documented 1583..9999
bound). 31 December 9999 is always constructible: it is in-range by
definition, so this cannot itself raise. *)
let domain_max_date =
match Date.make ~year:9999 ~month:12 ~day:31 with
| Ok d -> d
| Error e -> failwith e
let has_duplicate strings =
let sorted = List.sort String.compare strings in
let rec go = function a :: (b :: _ as rest) -> a = b || go rest | _ -> false in
go sorted
let run vocab ~year_start ~temporal ~anchors ~year =
let start = year_start year in
let stop =
(* [year_start (year + 1)] needs a date in civil year (year+1); at
[year] = 9999, the domain maximum, that lands out of range and would
raise. Clamp to 31 Dec 9999 instead of raising: kernel computation
must never raise on in-range input, and 9999 is in range. This
validates a truncated final liturgical year (through New Year's Eve
9999 only) rather than not being able to run the year at all --
see test_validate.ml's [test_year_9999_does_not_raise]. *)
if year >= 9999 then domain_max_date
else Date.add_days (year_start (year + 1)) (-1)
in
let failures = ref [] in
let fail date check detail =
failures := { year; date = Date.to_iso8601 date; check; detail } :: !failures
in
(* Vocabulary injectivity: the closure checks below compare ranks and
seasons via their _to_string images ([List.mem] has no equality on
function-carrying types), which is only sound if those images are
distinct per value. A rite whose rank_to_string collapses two ranks to
the same string would pass every rank both ranks share -- flag that
directly instead of relying on it silently by construction. *)
if has_duplicate (List.map vocab.Vocab.rank_to_string vocab.Vocab.ranks) then
fail start "vocab" "rank_to_string is not injective over vocab.ranks";
if has_duplicate (List.map vocab.Vocab.season_to_string vocab.Vocab.seasons) then
fail start "vocab" "season_to_string is not injective over vocab.seasons";
(* Walk the liturgical year once, collecting what the checks need. *)
let days = ref [] in
let d = ref start in
while Date.compare !d stop <= 0 do
days := !d :: !days;
d := Date.add_days !d 1
done;
let days = List.rev !days in
let observed = ref [] in
List.iter
(fun date ->
match temporal date with
| exception exn ->
(* Coverage: temporal must be total. *)
fail date "coverage" (Printexc.to_string exn)
| t ->
let cel = t.Temporal.office in
observed := (date, t) :: !observed;
(* Weekday agreement. *)
if t.Temporal.weekday <> Date.weekday date then
fail date "weekday" "temporal weekday disagrees with Date.weekday";
(* Slug: three properties, none checked here, all delivered
elsewhere. Well-formedness needs no check: [Slug.t] is a private
string validated on every construction path ([of_string],
[of_string_exn], [t_of_sexp]), and [to_string] is the identity,
so round-tripping an existing [Slug.t] can never fail -- a check
here would be structurally incapable of firing, which is worse
than no check, since it would look like coverage that isn't
there. Uniqueness *per date* needs no check either: [temporal]
returns exactly one office by construction. Uniqueness *across
the year* is deliberately NOT asserted -- a resumed Sunday
reuses an earlier Epiphany key on purpose, so the check would be
false. *)
(* Vocabulary closure. *)
if not (List.exists (fun r -> vocab.Vocab.rank_to_string r
= vocab.Vocab.rank_to_string cel.Celebration.rank)
vocab.Vocab.ranks)
then fail date "rank" "rank not in the rite vocabulary";
if not (List.mem cel.Celebration.colour Colour.all) then
fail date "colour" "colour not among the six";
(* Determinism: a second, independent call for the same date must
structurally agree with the first. temporal takes no wall-clock,
randomness or environment input, so any difference here is a
purity bug in the rite's own code, not a property of the date. *)
(match (try Some (temporal date) with _ -> None) with
| Some t2 when t2 = t -> ()
| Some _ -> fail date "determinism" "a second call to temporal returned a different result"
| None -> fail date "determinism" "a second call to temporal raised where the first succeeded"))
days;
let observed = List.rev !observed in
(* Season contiguity and completeness: the run-length-compressed sequence must
equal vocab.seasons exactly -- all seasons, each in one unbroken run, in
canonical order. No EF season can be empty in any year. *)
let compressed =
List.fold_left
(fun acc (_, t) ->
let s = vocab.Vocab.season_to_string t.Temporal.season in
match acc with hd :: _ when hd = s -> acc | _ -> s :: acc)
[] observed
|> List.rev
in
let expected = List.map vocab.Vocab.season_to_string vocab.Vocab.seasons in
if compressed <> expected then
fail start "seasons"
(Printf.sprintf "season runs %s; expected %s"
(String.concat "," compressed) (String.concat "," expected));
(* Week numbering: non-decreasing within a season run, and constant across each
Sunday-to-Saturday span inside that run. Deliberately NOT "starts at 1":
the numbering origin is season-specific. *)
let rec check_weeks prev_season prev_week = function
| [] -> ()
| (date, t) :: rest ->
let s = vocab.Vocab.season_to_string t.Temporal.season in
let same_run = prev_season = Some s in
(match (t.Temporal.week, prev_week) with
| Some n, Some p when same_run && n < p ->
fail date "week" (Printf.sprintf "week %d follows %d in the same season run" n p)
| _ -> ());
(* Within a run, a non-Sunday must carry the same week as the day before. *)
(match (t.Temporal.week, prev_week) with
| Some n, Some p when same_run && Date.weekday date <> Date.Sun && n <> p ->
fail date "week" (Printf.sprintf "week changed to %d on a non-Sunday (was %d)" n p)
| _ -> ());
let carry = match t.Temporal.week with Some _ as w -> w | None -> if same_run then prev_week else None in
check_weeks (Some s) carry rest
in
check_weeks None None observed;
(* Anchor agreement: dates the rite itself flags as fixed/Easter-derived
anchors (register/spec §5.7) must land where the rite's own independent
restatement of them says. [anchors] takes a civil year and returns dates
within it; a liturgical year straddles two civil years (most of Advent's
year plus most of the following civil year), so both are consulted and
the result filtered to the dates actually walked above. Guarded with a
safe wrapper: at [year] = 9999, [anchors (year + 1)] asks for civil year
10000, out of the kernel's domain, and must not propagate a raise here
any more than [year_start] may above. *)
let safe_anchors y = try anchors y with _ -> [] in
let anchor_pairs =
safe_anchors year @ safe_anchors (year + 1)
|> List.filter (fun (_, date) -> Date.compare date start >= 0 && Date.compare date stop <= 0)
in
List.iter
(fun (expected_slug, date) ->
match temporal date with
| exception exn -> fail date "anchor" (Printexc.to_string exn)
| t ->
let actual = Slug.to_string t.Temporal.office.Celebration.slug in
if actual <> expected_slug then
fail date "anchor" (Printf.sprintf "expected slug %S, got %S" expected_slug actual))
anchor_pairs;
List.rev !failures
|
