diff options
| -rw-r--r-- | lib/kernel/validate.ml | 92 | ||||
| -rw-r--r-- | lib/kernel/validate.mli | 16 | ||||
| -rw-r--r-- | test/test_colitur.ml | 2 | ||||
| -rw-r--r-- | test/test_validate.ml | 45 |
4 files changed, 154 insertions, 1 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 diff --git a/test/test_colitur.ml b/test/test_colitur.ml index 293e439..ae58607 100644 --- a/test/test_colitur.ml +++ b/test/test_colitur.ml @@ -2,4 +2,4 @@ let () = Alcotest.run "colitur" [ Test_date.suite; Test_computus.suite; Test_colour.suite; Test_slug.suite; Test_names.suite; - Test_overlay.suite; Test_temporal_ef.suite ] + Test_overlay.suite; Test_temporal_ef.suite; Test_validate.suite ] diff --git a/test/test_validate.ml b/test/test_validate.ml new file mode 100644 index 0000000..e293dfd --- /dev/null +++ b/test/test_validate.ml @@ -0,0 +1,45 @@ +module Val = Colitur_kernel.Validate +module V = Rite_ef.Vocab_ef +module T = Rite_ef.Temporal_ef + +let run year = + Val.run V.vocab ~year_start:T.year_start ~temporal:T.temporal ~year + +let check_year year = + match run year with + | [] -> () + | fs -> + Alcotest.failf "%d: %s" year + (String.concat "; " (List.map Val.failure_to_string (List.filteri (fun i _ -> i < 5) fs))) + +let test_landmark_years () = List.iter check_year [ 1583; 2026; 2035; 9998 ] + +(* Easter extremes: the earliest possible date is 22 March and the latest is + 25 April. Find one of each inside the domain and validate those years. *) +let extreme_years () = + let module C = Colitur_kernel.Computus in + let module D = Colitur_kernel.Date in + let earliest = ref None and latest = ref None in + for y = 1583 to 2500 do + let e = C.gregorian_easter y in + if D.month e = 3 && D.day e = 22 && !earliest = None then earliest := Some y; + if D.month e = 4 && D.day e = 25 && !latest = None then latest := Some y + done; + List.filter_map Fun.id [ !earliest; !latest ] + +let test_easter_extremes () = + let ys = extreme_years () in + Alcotest.(check bool) "found at least one extreme year" true (ys <> []); + List.iter check_year ys + +(* The confidence-to-9999 core: random years across the whole domain. *) +let prop_invariants = + QCheck.Test.make ~count:200 ~name:"EF temporal invariants hold across 1583..9998" + (QCheck.int_range 1583 9998) + (fun y -> run y = []) + +let suite = + ( "Validate", + [ Alcotest.test_case "landmark years" `Quick test_landmark_years; + Alcotest.test_case "easter extremes" `Quick test_easter_extremes ] + @ List.map QCheck_alcotest.to_alcotest [ prop_invariants ] ) |