diff options
Diffstat (limited to 'lib/kernel')
| -rw-r--r-- | lib/kernel/validate.ml | 92 | ||||
| -rw-r--r-- | lib/kernel/validate.mli | 16 |
2 files changed, 108 insertions, 0 deletions
diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml new file mode 100644 index 0000000..9be030a --- /dev/null +++ b/lib/kernel/validate.ml @@ -0,0 +1,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 diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli new file mode 100644 index 0000000..b557731 --- /dev/null +++ b/lib/kernel/validate.mli @@ -0,0 +1,16 @@ +(** The invariant harness -- validation layer 2. Checks run over a *liturgical* + year, not a civil year: a season that straddles January would otherwise look + as though it recurs. *) +type failure = { year : int; date : string; check : string; detail : string } + +val failure_to_string : failure -> string + +(** [run vocab ~year_start ~temporal ~year] returns every invariant violation in + the liturgical year opening in civil year [year]. An empty list means the + year is clean. *) +val run : + ('s, 'r) Vocab.t -> + year_start:(int -> Date.t) -> + temporal:(Date.t -> ('s, 'r) Temporal.t) -> + year:int -> + failure list |