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
|
(* 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
let run vocab ~year_start ~temporal ~year =
let start = year_start year in
let stop = 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
(* 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 well-formed. Uniqueness *per date* needs no check: [temporal]
returns exactly one office by construction, which is the type
system delivering the invariant. Uniqueness *across the year* is
deliberately NOT asserted -- a resumed Sunday reuses an earlier
Epiphany key on purpose, so the check would be false. *)
(match Slug.of_string (Slug.to_string cel.Celebration.slug) with
| Ok _ -> ()
| Error e -> fail date "slug" e);
(* 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")
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;
List.rev !failures
|
