path: root/test/test_validate.ml

module Val = Colitur_kernel.Validate
module Rite = Colitur_kernel.Rite
module P = Colitur_kernel.Precedence
module V = Rite_ef.Vocab_ef
module T = Rite_ef.Temporal_ef

(* Plan 3's real EF precedence rules (Precedence_ef, Tasks 7-11) don't exist
   yet -- Validate.run doesn't read [rules] at all (nothing does before
   Task 5's Calendar), so a placeholder is enough to assemble a well-typed
   Rite.t here. *)
let ef_rules : (V.season, V.rank) P.rules =
  { P.band = (fun _ _ -> 0);
    disposition = (fun ~winner:_ ~loser:_ -> P.Omit);
    admit = (fun ~observed:_ _ -> []) }

let ef_rite : (V.season, V.rank) Rite.t =
  { Rite.id = T.id; vocab = V.vocab; year_start = T.year_start; temporal = T.temporal;
    anchors = T.anchors; rules = ef_rules; season_runs = V.seasons }

let run year = Val.run ef_rite ~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 ]

(* Register finding 2 / controller finding B: [Validate.run ~year:9999] used
   to raise ([year_start (year + 1)] asks for civil year 10000, out of the
   kernel's domain), even though 9999 is in range and kernel computation must
   never raise on in-range input. [run] now clamps its scan to 31 Dec 9999
   instead. Calling [run 9999] directly (no [try]) is itself part of the
   pin: if the clamp regressed, this call would raise and the test would
   error. The clamped scan only covers Advent and the start of Christmastide,
   so it is *expected* to report the season run as incomplete -- this pins
   that the incompleteness surfaces as an ordinary "seasons" failure, not an
   uncaught exception, and that nothing else broke in the process. *)
let test_year_9999_does_not_raise () =
  let fs = run 9999 in
  Alcotest.(check bool) "no coverage failures (temporal stayed total through the clamp)" true
    (not (List.exists (fun f -> f.Val.check = "coverage") fs));
  Alcotest.(check bool) "seasons check flags the truncated final year as incomplete" true
    (List.exists (fun f -> f.Val.check = "seasons") fs)

(* 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
  (* Both extremes genuinely occur in 1583..2500 (earliest 1818, latest
     2038); requiring just "non-empty" would have passed even if the search
     silently found only one of them (register finding 15). *)
  Alcotest.(check int) "found both extreme years (earliest 22 Mar and latest 25 Apr)" 2 (List.length 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 = [])

(* ---- negative-path fixture (Task 14 review, finding 1) ----

   Everything above only exercises the CLEAN path against real EF data: an
   empty failure list. That leaves nothing committed proving each check can
   actually fire -- a future edit that quietly weakens a check would still
   leave this suite green, since a weaker check only makes more inputs pass.

   This is a small, synthetic two-season, two-rank rite -- not EF -- built so
   each mutation below can violate exactly one invariant directly, rather
   than corrupting real rite data. [Validate] is rite-agnostic by design;
   this is that design's second "rite", proving the abstraction and the
   checks both hold up away from EF specifically. *)
module Synthetic = struct
  module D = Colitur_kernel.Date
  module Vocab = Colitur_kernel.Vocab
  module Cel = Colitur_kernel.Celebration
  module Slug = Colitur_kernel.Slug
  module Colour = Colitur_kernel.Colour
  module Temporal = Colitur_kernel.Temporal
  module P = Colitur_kernel.Precedence
  module Rite = Colitur_kernel.Rite

  type season = A | B
  type rank = R1 | R2

  let season_to_string = function A -> "a" | B -> "b"
  let season_of_string = function "a" -> Some A | "b" -> Some B | _ -> None
  let rank_to_string = function R1 -> "r1" | R2 -> "r2"
  let rank_of_string = function "r1" -> Some R1 | "r2" -> Some R2 | _ -> None

  let vocab : (season, rank) Vocab.t =
    { Vocab.seasons = [ A; B ]; season_to_string; season_of_string;
      ranks = [ R1; R2 ]; rank_to_string; rank_of_string }

  (* A vocab whose declared rank list omits R2 -- a realistic
     documentation/data-drift scenario. (Fabricating an out-of-type rank
     instead would need [Obj.magic] on a two-constructor variant, which is
     undefined behaviour the moment anything pattern-matches it -- see the
     colour mutation below, where that risk is called out explicitly.) *)
  let vocab_missing_rank = { vocab with Vocab.ranks = [ R1 ] }

  (* Register finding 8: rank_to_string collapsing two distinct ranks to the
     same string, and season_to_string doing the same -- a realistic
     documentation/data-drift scenario distinct from [vocab_missing_rank]
     above (that one omits a rank entirely; these make two indistinguishable
     instead). *)
  let vocab_collapsed_ranks = { vocab with Vocab.rank_to_string = (fun _ -> "same") }
  let vocab_collapsed_seasons = { vocab with Vocab.season_to_string = (fun _ -> "same") }

  (* Precedence_ef doesn't exist yet (Tasks 7-11); Validate.run never reads
     [rules], so a placeholder is enough to assemble a well-typed Rite.t. *)
  let rules : (season, rank) P.rules =
    { P.band = (fun _ _ -> 0);
      disposition = (fun ~winner:_ ~loser:_ -> P.Omit);
      admit = (fun ~observed:_ _ -> []) }

  let year_start y = match D.make ~year:y ~month:1 ~day:1 with Ok d -> d | Error e -> failwith e

  let weekday_index d =
    match D.weekday d with
    | D.Sun -> 0 | D.Mon -> 1 | D.Tue -> 2 | D.Wed -> 3 | D.Thu -> 4 | D.Fri -> 5 | D.Sat -> 6

  let sunday_on_or_before d = D.add_days d (-(weekday_index d))

  (* The first Sunday on or after 1 July: where season B and its own week
     origin begin. *)
  let split_date y =
    let jul1 = match D.make ~year:y ~month:7 ~day:1 with Ok d -> d | Error e -> failwith e in
    D.add_days jul1 ((7 - weekday_index jul1) mod 7)

  let floor_div a b = if a >= 0 then a / b else ((a + 1) / b) - 1

  (* The clean baseline: season A from New Year's Day to the Saturday before
     [split_date], season B from [split_date] onward. Both season-run origins
     are Sundays, so weeks are Sunday-aligned and non-decreasing throughout --
     this is what a zero-failure [Validate.run] looks like for a rite that
     actually is clean. *)
  let good d =
    let y = D.year d in
    let s = if D.compare d (split_date y) < 0 then A else B in
    let origin = if s = A then sunday_on_or_before (year_start y) else split_date y in
    let n = floor_div (D.to_rata d - D.to_rata origin) 7 + 1 in
    let slug = Printf.sprintf "syn-%s-%d" (season_to_string s) (D.to_rata d) in
    let rank = if D.weekday d = D.Sun then R1 else R2 in
    { Temporal.season = s; week = Some n; weekday = D.weekday d;
      office = Cel.make ~slug:(Slug.of_string_exn slug) ~rank ~colour:Colour.Green ~layer:"synthetic" () }

  (* The one day each mutation below corrupts. Genuinely mid-week (Tuesday,
     not the Sunday that "2026-03-15" actually is despite the comment this
     replaces having claimed otherwise -- register finding 12): not a
     Sunday, and not New Year's Day or the season split, so it sits safely
     mid-run for every check that cares about run position. *)
  let target = match D.make ~year:2026 ~month:3 ~day:17 with Ok d -> d | Error e -> failwith e

  (* Register finding 3: the rite's own independent restatement of one fixed
     anchor -- [target]'s date, paired with the slug [good] already gives it
     -- so the anchor-agreement check has something non-trivial to check in
     this synthetic rite too, not only in EF. *)
  let anchors _y = [ (Slug.to_string (good target).Temporal.office.Cel.slug, target) ]

  let rite ?(vocab = vocab) ?(anchors = fun _ -> []) ?(season_runs = [ A; B ]) temporal
      : (season, rank) Rite.t =
    { Rite.id = "synthetic"; vocab; year_start; temporal; anchors; rules; season_runs }

  let run ?vocab ?anchors ?season_runs temporal =
    Val.run (rite ?vocab ?anchors ?season_runs temporal) ~year:2026

  let has_check check (fs : Val.failure list) = List.exists (fun f -> f.Val.check = check) fs

  (* A rite whose season B legitimately appears in two separate runs: the
     civil year is split into calendar quarters, seasons alternating A B A B
     -- as the modern form's Ordinary Time does (January-Ash Wednesday, then
     Pentecost-Advent, with Lent/Easter and Advent/Christmas between). Each
     quarter gets its own Sunday-aligned week origin, exactly as [good] does
     for its own two runs, so every other invariant (weekday, week
     numbering, rank, colour, determinism) stays clean and only the season
     check is actually exercised. *)
  let quarter_start y i =
    match D.make ~year:y ~month:(1 + (i * 3)) ~day:1 with Ok d -> d | Error e -> failwith e

  let quarter_index d = (D.month d - 1) / 3

  let two_run_temporal d =
    let y = D.year d in
    let qi = quarter_index d in
    let s = if qi mod 2 = 0 then A else B in
    let origin = sunday_on_or_before (quarter_start y qi) in
    let n = floor_div (D.to_rata d - D.to_rata origin) 7 + 1 in
    let slug = Printf.sprintf "syn2-%s-%d" (season_to_string s) (D.to_rata d) in
    let rank = if D.weekday d = D.Sun then R1 else R2 in
    { Temporal.season = s; week = Some n; weekday = D.weekday d;
      office = Cel.make ~slug:(Slug.of_string_exn slug) ~rank ~colour:Colour.Green ~layer:"synthetic" () }

  let rite_with_two_runs : (season, rank) Rite.t =
    rite ~season_runs:[ A; B; A; B ] two_run_temporal
end

open Synthetic

let test_synthetic_baseline_is_clean () =
  Alcotest.(check bool) "clean synthetic fixture has no failures" true (run good = [])

(* The point of this task: a rite whose season B genuinely appears in two
   separate runs (quarters 0,1,2,3 give season sequence A B A B, not a single
   A-then-B pair) validates clean when [season_runs] says so. Before this
   task, [Validate]'s season check hardcoded "compressed = vocab.seasons"
   ([A; B]) with no way to say otherwise -- against that check this fixture's
   compressed sequence, [A; B; A; B], would never match and every year would
   report a spurious "seasons" failure. *)
let test_two_run_season_is_accepted () =
  let r = Synthetic.rite_with_two_runs in
  Alcotest.(check (list string)) "no failures" []
    (List.map Val.failure_to_string (Val.run r ~year:2026))

let test_coverage_fires () =
  let temporal d = if D.compare d target = 0 then failwith "boom" else good d in
  Alcotest.(check bool) "coverage check fires when temporal raises" true
    (has_check "coverage" (run temporal))

let test_seasons_fires () =
  let temporal d =
    let t = good d in
    let y = D.year d in
    let flip_after = match D.make ~year:y ~month:9 ~day:1 with Ok d -> d | Error e -> failwith e in
    (* Season A reappears after B: breaks the expected [A; B] run sequence. *)
    if D.compare d flip_after >= 0 then { t with Temporal.season = A } else t
  in
  Alcotest.(check bool) "seasons check fires when a season recurs outside season_runs" true
    (has_check "seasons" (run temporal))

let test_week_fires () =
  let temporal d =
    let t = good d in
    (* A single mid-run day's week drops below the day before it. *)
    if D.compare d target = 0 then { t with Temporal.week = Some 1 } else t
  in
  Alcotest.(check bool) "week check fires when a week number decreases mid-run" true
    (has_check "week" (run temporal))

let test_weekday_fires () =
  let temporal d =
    let t = good d in
    if D.compare d target = 0 then
      { t with Temporal.weekday = (if t.Temporal.weekday = D.Sun then D.Mon else D.Sun) }
    else t
  in
  Alcotest.(check bool) "weekday check fires when it disagrees with Date.weekday" true
    (has_check "weekday" (run temporal))

let test_rank_fires () =
  let temporal d =
    let t = good d in
    if D.compare d target = 0 then { t with Temporal.office = { t.Temporal.office with Cel.rank = R2 } }
    else { t with Temporal.office = { t.Temporal.office with Cel.rank = R1 } }
  in
  Alcotest.(check bool) "rank check fires when a rank is absent from the declared vocab" true
    (has_check "rank" (run ~vocab:vocab_missing_rank temporal))

let test_colour_fires () =
  (* Unlike rank, colour isn't rite-parameterised -- [Colour.t] is closed over
     exactly six constructors, all listed in [Colour.all], so no rite's own
     data can ever name a seventh. There is no type-safe way to construct an
     invalid one, so this is the one mutation that reaches for [Obj.magic] --
     safely here, because the colour check compares by structural equality
     ([List.mem], no pattern match), unlike [rank_to_string], which would hit
     undefined behaviour on an out-of-range tag (why the rank mutation above
     goes through an incomplete vocab list instead of doing the same trick). *)
  let bogus_colour : Colour.t = Obj.magic 99 in
  let temporal d =
    let t = good d in
    if D.compare d target = 0 then { t with Temporal.office = { t.Temporal.office with Cel.colour = bogus_colour } }
    else t
  in
  Alcotest.(check bool) "colour check fires when the colour is outside Colour.all" true
    (has_check "colour" (run temporal))

(* Register finding 3 (§5.8 determinism). [target] alternates what it
   returns across successive calls with the same date -- everything else is
   [good], genuinely pure -- so the first call (feeding the season/week/etc.
   checks) and [run]'s own repeated call (the determinism check itself) see
   different results for that one date. *)
let test_determinism_fires () =
  let calls = ref 0 in
  let temporal d =
    if D.compare d target = 0 then begin
      incr calls;
      let t = good d in
      if !calls mod 2 = 0 then { t with Temporal.week = Some 999 } else t
    end
    else good d
  in
  Alcotest.(check bool) "determinism check fires when a repeated call returns a different result" true
    (has_check "determinism" (run temporal))

(* Register finding 3 (§5.7 anchor agreement). *)
let test_anchor_clean () =
  Alcotest.(check bool) "the rite's own anchor list agrees with its own temporal, so no anchor failures"
    true (not (has_check "anchor" (run ~anchors good)))

let test_anchor_fires () =
  let temporal d =
    let t = good d in
    if D.compare d target = 0 then
      { t with Temporal.office = { t.Temporal.office with Cel.slug = Slug.of_string_exn "syn-wrong-anchor" } }
    else t
  in
  Alcotest.(check bool) "anchor check fires when temporal disagrees with the rite's own anchor list" true
    (has_check "anchor" (run ~anchors temporal))

let test_vocab_rank_injectivity_fires () =
  Alcotest.(check bool) "vocab check fires when rank_to_string collapses two ranks to one string" true
    (has_check "vocab" (run ~vocab:vocab_collapsed_ranks good))

let test_vocab_season_injectivity_fires () =
  Alcotest.(check bool) "vocab check fires when season_to_string collapses two seasons to one string" true
    (has_check "vocab" (run ~vocab:vocab_collapsed_seasons good))

let suite =
  ( "Validate",
    [ Alcotest.test_case "landmark years" `Quick test_landmark_years;
      Alcotest.test_case "year 9999 does not raise" `Quick test_year_9999_does_not_raise;
      Alcotest.test_case "easter extremes" `Quick test_easter_extremes;
      Alcotest.test_case "synthetic baseline is clean" `Quick test_synthetic_baseline_is_clean;
      Alcotest.test_case "two-run season is accepted" `Quick test_two_run_season_is_accepted;
      Alcotest.test_case "coverage fires" `Quick test_coverage_fires;
      Alcotest.test_case "seasons fires" `Quick test_seasons_fires;
      Alcotest.test_case "week fires" `Quick test_week_fires;
      Alcotest.test_case "weekday fires" `Quick test_weekday_fires;
      Alcotest.test_case "rank fires" `Quick test_rank_fires;
      Alcotest.test_case "colour fires" `Quick test_colour_fires;
      Alcotest.test_case "determinism fires" `Quick test_determinism_fires;
      Alcotest.test_case "anchor clean" `Quick test_anchor_clean;
      Alcotest.test_case "anchor fires" `Quick test_anchor_fires;
      Alcotest.test_case "vocab rank injectivity fires" `Quick test_vocab_rank_injectivity_fires;
      Alcotest.test_case "vocab season injectivity fires" `Quick test_vocab_season_injectivity_fires ]
    @ List.map QCheck_alcotest.to_alcotest [ prop_invariants ] )