diff options
| -rw-r--r-- | lib/kernel/rite.ml | 12 | ||||
| -rw-r--r-- | lib/kernel/rite.mli | 18 | ||||
| -rw-r--r-- | lib/kernel/validate.ml | 15 | ||||
| -rw-r--r-- | lib/kernel/validate.mli | 32 | ||||
| -rw-r--r-- | test/test_validate.ml | 79 |
5 files changed, 129 insertions, 27 deletions
diff --git a/lib/kernel/rite.ml b/lib/kernel/rite.ml new file mode 100644 index 0000000..b948390 --- /dev/null +++ b/lib/kernel/rite.ml @@ -0,0 +1,12 @@ +(* Everything a rite supplies, bundled. Passing these as loose arguments let a + caller pair one rite's vocab with another's temporal; bundling makes that + unrepresentable through the normal path. *) +type ('s, 'r) t = { + id : string; + vocab : ('s, 'r) Vocab.t; + year_start : int -> Date.t; + temporal : Date.t -> ('s, 'r) Temporal.t; + anchors : int -> (string * Date.t) list; + rules : ('s, 'r) Precedence.rules; + season_runs : 's list; +} diff --git a/lib/kernel/rite.mli b/lib/kernel/rite.mli new file mode 100644 index 0000000..db8e86f --- /dev/null +++ b/lib/kernel/rite.mli @@ -0,0 +1,18 @@ +(** Everything a rite supplies, bundled. Passing these as loose arguments let a + caller pair one rite's vocab with another's temporal; bundling makes that + unrepresentable through the normal path. Carries functions, so it has no + sexp form. *) +type ('s, 'r) t = { + id : string; + vocab : ('s, 'r) Vocab.t; + year_start : int -> Date.t; + (** first day of the liturgical year opening in civil year y *) + temporal : Date.t -> ('s, 'r) Temporal.t; + anchors : int -> (string * Date.t) list; + (** Easter-derived days: (expected slug, date) *) + rules : ('s, 'r) Precedence.rules; + season_runs : 's list; + (** the expected run-length-compressed season sequence over one liturgical + year. NOT necessarily [vocab.seasons]: a rite may have one season + appear in two separate runs (the modern form's Ordinary Time does). *) +} diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index 7be3425..c6501a9 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -20,7 +20,11 @@ let has_duplicate strings = 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 run (rite : ('s, 'r) Rite.t) ~year = + let vocab = rite.Rite.vocab in + let year_start = rite.Rite.year_start in + let temporal = rite.Rite.temporal in + let anchors = rite.Rite.anchors in let start = year_start year in let stop = (* [year_start (year + 1)] needs a date in civil year (year+1); at @@ -98,8 +102,11 @@ let run vocab ~year_start ~temporal ~anchors ~year = 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. *) + equal the rite's own [season_runs] exactly, in canonical order. This is + NOT necessarily [vocab.seasons] -- most rites have each season in one + unbroken run, but a rite may legitimately have one season appear in two + separate runs (the modern form's Ordinary Time does), so the expected + sequence is rite-supplied rather than derived from the vocabulary. *) let compressed = List.fold_left (fun acc (_, t) -> @@ -108,7 +115,7 @@ let run vocab ~year_start ~temporal ~anchors ~year = [] observed |> List.rev in - let expected = List.map vocab.Vocab.season_to_string vocab.Vocab.seasons in + let expected = List.map vocab.Vocab.season_to_string rite.Rite.season_runs in if compressed <> expected then fail start "seasons" (Printf.sprintf "season runs %s; expected %s" diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli index 709a711..d281f9a 100644 --- a/lib/kernel/validate.mli +++ b/lib/kernel/validate.mli @@ -5,26 +5,24 @@ type failure = { year : int; date : string; check : string; detail : string } val failure_to_string : failure -> string -(** [run vocab ~year_start ~temporal ~anchors ~year] returns every invariant - violation in the liturgical year opening in civil year [year]. An empty - list means the year is clean. +(** [run rite ~year] returns every invariant violation in the liturgical year + opening in civil year [year]. An empty list means the year is clean. - [anchors y] is the rite's own independent restatement of its fixed and - Easter-derived named days for civil year [y], as (expected slug, date) - pairs -- not derived from [temporal] itself, so a drift between the two - is caught rather than invisible. [run] consults both [anchors year] and - [anchors (year + 1)], since a liturgical year straddles two civil years, - and checks only the pairs whose date actually falls within the year - walked. + [rite.Rite.anchors y] is the rite's own independent restatement of its + fixed and Easter-derived named days for civil year [y], as (expected + slug, date) pairs -- not derived from [rite.Rite.temporal] itself, so a + drift between the two is caught rather than invisible. [run] consults + both [anchors year] and [anchors (year + 1)], since a liturgical year + straddles two civil years, and checks only the pairs whose date actually + falls within the year walked. + + The season check compares the run-length-compressed season sequence + against [rite.Rite.season_runs], not [rite.Rite.vocab.seasons]: a rite may + have one season appear in two separate runs (the modern form's Ordinary + Time does), so the two are not necessarily the same list. Total over the whole 1583..9999 domain, including [year] = 9999: the liturgical year opening there continues into out-of-domain civil year 10000, so the walk is clamped to 31 December 9999 and the checks run against that truncated final year rather than raising. *) -val run : - ('s, 'r) Vocab.t -> - year_start:(int -> Date.t) -> - temporal:(Date.t -> ('s, 'r) Temporal.t) -> - anchors:(int -> (string * Date.t) list) -> - year:int -> - failure list +val run : ('s, 'r) Rite.t -> year:int -> failure list diff --git a/test/test_validate.ml b/test/test_validate.ml index c19957d..31d7a3d 100644 --- a/test/test_validate.ml +++ b/test/test_validate.ml @@ -1,9 +1,23 @@ 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 -let run year = - Val.run V.vocab ~year_start:T.year_start ~temporal:T.temporal ~anchors:T.anchors ~year +(* 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 @@ -77,6 +91,8 @@ module Synthetic = struct 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 @@ -105,6 +121,13 @@ module Synthetic = struct 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 = @@ -149,10 +172,41 @@ module Synthetic = struct this synthetic rite too, not only in EF. *) let anchors _y = [ (Slug.to_string (good target).Temporal.office.Cel.slug, target) ] - let run ?(vocab = vocab) ?(anchors = fun _ -> []) temporal = - Val.run vocab ~year_start ~temporal ~anchors ~year:2026 + 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 @@ -160,6 +214,18 @@ 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 @@ -170,10 +236,10 @@ let test_seasons_fires () = 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 "each season, one unbroken run". *) + (* 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" true + Alcotest.(check bool) "seasons check fires when a season recurs outside season_runs" true (has_check "seasons" (run temporal)) let test_week_fires () = @@ -269,6 +335,7 @@ let suite = 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; |