diff options
Diffstat (limited to 'test/test_validate.ml')
| -rw-r--r-- | test/test_validate.ml | 108 |
1 files changed, 103 insertions, 5 deletions
diff --git a/test/test_validate.ml b/test/test_validate.ml index 8c96f26..1a960df 100644 --- a/test/test_validate.ml +++ b/test/test_validate.ml @@ -3,6 +3,7 @@ module Rite = Colitur_kernel.Rite module P = Colitur_kernel.Precedence module Layer = Colitur_kernel.Layer module Overlay = Colitur_kernel.Overlay +module Citation = Colitur_kernel.Citation module V = Rite_ef.Vocab_ef module T = Rite_ef.Temporal_ef @@ -299,12 +300,26 @@ module Synthetic = struct defaults against the default empty [layer], since nothing ever contests the temporal office there) so the resolution fixtures further down can override them without duplicating every other field. *) - (* No fixture here exercises citations -- readings is a harmless constant - [], the same role the other placeholder defaults above play. *) + (* Most fixtures here exercise no citations -- [readings] is a harmless + constant [], the same role the other placeholder defaults above play, + and {!Validate}'s own citation checks are gated on a rite producing SOME + citation somewhere, so a constant [] leaves them entirely dormant. Task + 10 makes it overridable ([?readings] below) so the citation fixtures at + the end of this file can drive those checks directly, exactly as every + other check here is driven -- rather than leaving two kernel checks with + no committed proof that they can fire at all. *) let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = [] + (* The shape {!Validate} accepts: exactly one First and one Gospel. The + references are deliberately nonsense -- these fixtures assert SHAPE, + never content. *) + let well_formed_citations = + [ { Citation.part = Citation.First; reference = "Synth 1:1" }; + { Citation.part = Citation.Gospel; reference = "Synth 2:2" } ] + let rite ?(vocab = vocab) ?(anchors = fun _ -> []) ?(season_runs = [ A; B ]) ?(rules = rules) - ?(transfer_target = fun _ origin _ -> origin) temporal : (season, rank) Rite.t = + ?(transfer_target = fun _ origin _ -> origin) ?(readings = readings) temporal : + (season, rank) Rite.t = { Rite.id = "synthetic"; vocab; year_start; temporal; anchors; rules; season_runs; transfer_target; readings } @@ -315,8 +330,11 @@ module Synthetic = struct unchallenged). Task 12's own resolution fixtures pass their own. *) let empty_layer = Layer.empty ~id:"synthetic-empty" ~name:"empty" - let run ?vocab ?anchors ?season_runs ?rules ?transfer_target ?(layer = empty_layer) temporal = - Val.run (rite ?vocab ?anchors ?season_runs ?rules ?transfer_target temporal) layer ~year:2026 + let run ?vocab ?anchors ?season_runs ?rules ?transfer_target ?readings ?(layer = empty_layer) + temporal = + Val.run + (rite ?vocab ?anchors ?season_runs ?rules ?transfer_target ?readings temporal) + layer ~year:2026 let has_check check (fs : Val.failure list) = List.exists (fun f -> f.Val.check = check) fs @@ -708,6 +726,76 @@ let test_resolution_checks_clean_on_a_well_behaved_layer () = Alcotest.(check (list string)) "none of the five checks fire" [] (fired_task12_checks (run ~layer:clean_sanctoral_layer ~rules:clean_sanctoral_rules good)) +(* ---- Task 10: the citation invariants ---- + + Two new kernel checks, and on real EF data NEITHER can fire: every day of + every liturgical year 1583-9999 resolves exactly one Epistle and one + Gospel (measured, not assumed -- the exhaustive sweep is clean, and the + check was mutation-proved live rather than merely silent). That is the + good outcome and precisely why these fixtures are needed: a check with no + live witness and no negative-path test is indistinguishable from a check + that does nothing, which is the trap this whole section of the file exists + to avoid. + + All four drive the checks through [?readings], the same way every fixture + above drives its own check through [?vocab]/[temporal]/[?rules]. *) + +(* The gate itself, and the most load-bearing of the four: a rite that + computes no readings AT ALL (the default constant [], every other fixture + in this file, and any rite whose lectionary is simply not built yet) must + report neither check -- not "usually", not "on this year". Without this, + the natural implementation ("a day with no citations is a failure") would + turn every unrelated fixture here red and, worse, would make [Validate] + demand a lectionary of any rite that has none. *) +let test_citations_silent_without_a_lectionary () = + let fs = run good in + Alcotest.(check bool) "no citation check fires for a rite with no readings at all" false + (has_check "citations" fs || has_check "citations-unresolved" fs) + +(* The positive: well-formed citations on every day report nothing. *) +let test_citations_clean_when_well_formed () = + let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = well_formed_citations in + let fs = run ~readings good in + Alcotest.(check bool) "neither citation check fires when every day carries First + Gospel" false + (has_check "citations" fs || has_check "citations-unresolved" fs) + +(* Zero or two, never one: a lone Epistle is a malformed Mass. This is the + invariant the plan names first, and the one a bootstrap bug would most + plausibly produce -- half a lookup succeeding. *) +let test_citations_fires_on_a_lone_epistle () = + let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = + [ { Citation.part = Citation.First; reference = "Synth 1:1" } ] + in + Alcotest.(check bool) "citations check fires when a day carries an Epistle but no Gospel" true + (has_check "citations" (run ~readings good)) + +(* A part outside this plan's scope. The chants (Psalm/Second/Tract/Alleluia/ + Sequence) are deliberately unbuilt -- no source, no oracle -- so one + appearing is a defect, not a feature arriving early, and must be caught + even though the day is otherwise a well-formed pair. *) +let test_citations_fires_on_an_out_of_scope_part () = + let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = + { Citation.part = Citation.Tract; reference = "Synth 3:3" } :: well_formed_citations + in + Alcotest.(check bool) "citations check fires when a part outside First/Gospel appears" true + (has_check "citations" (run ~readings good)) + +(* The coverage half, kept a SEPARATE check name from the three above: a rite + that resolves readings on most days but falls through on one. On real EF + data this has no witness at all, so this fixture is the only thing that + holds it honest. [target] is the same mid-run day every other fixture in + this file singles out. *) +let test_citations_unresolved_fires_on_a_gap () = + let readings ~observed:_ ~temporal:_ ~date ~temporal_at:_ = + if D.compare date target = 0 then [] else well_formed_citations + in + Alcotest.(check bool) "citations-unresolved fires when one day of the year resolves nothing" true + (has_check "citations-unresolved" (run ~readings good)); + (* ...and the well-formedness check must stay silent on that same run: the + two are different faults and must not be reported as one. *) + Alcotest.(check bool) "the well-formedness check stays silent on a pure coverage gap" false + (has_check "citations" (run ~readings good)) + let suite = ( "Validate", [ Alcotest.test_case "landmark years" `Quick test_landmark_years; @@ -727,6 +815,16 @@ let suite = 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; Alcotest.test_case "slugs fires" `Quick test_slugs_fires; + Alcotest.test_case "citations silent without a lectionary" `Quick + test_citations_silent_without_a_lectionary; + Alcotest.test_case "citations clean when well formed" `Quick + test_citations_clean_when_well_formed; + Alcotest.test_case "citations fires on a lone epistle" `Quick + test_citations_fires_on_a_lone_epistle; + Alcotest.test_case "citations fires on an out-of-scope part" `Quick + test_citations_fires_on_an_out_of_scope_part; + Alcotest.test_case "citations-unresolved fires on a gap" `Quick + test_citations_unresolved_fires_on_a_gap; Alcotest.test_case "lost fires on resolution exception" `Quick test_lost_fires_on_resolution_exception; Alcotest.test_case "duplicated fires" `Quick test_duplicated_fires; Alcotest.test_case "unconverged fires" `Quick test_unconverged_fires; |