diff options
| author | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-17 14:56:46 +0200 |
|---|---|---|
| committer | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-17 14:56:46 +0200 |
| commit | 947cadfab527829f8e42a896339a0fa6c2e81ad9 (patch) | |
| tree | 4e067c1f03ddc189aa4797fc8a2299dfaf077060 | |
| parent | 1915f3bb9d74998a411bd55ae658cb3f58fd3477 (diff) | |
| download | colitur-947cadfab527829f8e42a896339a0fa6c2e81ad9.tar.gz colitur-947cadfab527829f8e42a896339a0fa6c2e81ad9.zip | |
test: lectionary properties, golden pins, and the blast radius
Layers 2 and 5 for the reading citations, which until now had coverage
from layers 3 and 4 only -- both oracle-bounded, at 2050 and 2027.
test_validate.ml said so in its own words ("No fixture here exercises
citations") and test_golden.ml's describe pinned twelve fields, none of
them a citation. 358 tests -> 369, and 370 under the sweep.
Layer 2 as two Validate checks rather than standalone QCheck properties,
so they ride the existing prop_invariants and the exhaustive sweep
instead of duplicating that machinery. "citations" asserts a day's parts,
sorted, are exactly [First; Gospel] -- one condition carrying three
invariants: zero or two but never one, nothing outside First and Gospel
since the chants are deliberately unbuilt, and no part twice, which a
bare cardinality test would miss. "citations-unresolved" is the separate
coverage half: the chain fell through every step. Both are gated on the
rite producing some citation somewhere, so a rite whose lectionary is not
built is held to neither and the synthetic fixtures stay unaffected.
The result over the whole domain: every day of every liturgical year
1583-9999 resolves exactly one Epistle and one Gospel. Mutation-proved
live rather than merely silent -- treating a well-formed pair as
malformed reddens the suite with real days showing [first,gospel].
citations-unresolved has no live witness at all, which is why
test_validate.ml gains five fixtures driving both checks through a new
?readings override, including the gate itself.
Layer 5 as six pins, one per chain step, so a regression names the step
that broke. Every literal was read out of the scans before being
compared with colitur, per that file's standing rule; scan lines are in
each pin's comment. Two of the six cover step 4, and the plan's own dates
for steps 1 and 4 were wrong: 2030-01-13 is a temporal day (Holy Family
on the generic Sunday slug) and would not have exercised step 1, while
2038-03-08 is John of God, who has a full proper Mass and never routes
through a Common -- so he becomes the step-1 pin instead.
A separate formatter rather than widening describe: widening would
invalidate all thirty existing literals at once and the only practical
way back would be pasting in whatever colitur printed, which is what the
file's header forbids. Restoring them honestly means hand-verifying
thirty more Masses against the scans, a task of its own. Stated rather
than hidden, and defensible because layer 2 now checks the shape of
every day in every year, which is the breadth that widening would have
bought.
Two pins earned their keep immediately. Lent I Monday failed on "Ezek"
against colitur's "Ezech" -- notation only, and colitur matches the
Missal's own abbreviation; layer 3 normalises this away and cannot see
it. The displaced-Sunday feria pins M26 shape 2(b)'s known-wrong
walkback deliberately, labelled as such so a future fix fails loudly,
and established two things M26 had not recorded: both parts come from
the displacing feast, not only the Gospel it cites, and the reference
carries a stray trailing period inherited through the bootstrap.
Blast radius: zero. The CLI never calls Validate, no data file changed,
and 20 years spanning 1583-9998 produce 7301 byte-identical lines
between the pre-change binary and HEAD.
Step 4's blind spot is now measured rather than argued. Corrupting the
Common of Non-Virgins I's Epistle leaves layer 3 (16801 days) and layer
4 (730 days) both green, reddening only one unit test and one new pin.
Both step-4 pins matched the scans on the first attempt -- the first
independent confirmation that route has ever had. It narrows the gap
without closing it: two of five Common-routed saints are witnessed,
isidore-of-seville is not, and gregory-the-great and patrick are
unreachable in any year 2005-2050.
Register: section 6.7 addendum. validate.mli documents both new labels;
liturgical_day.mli's "always empty until Plan 4" was outlived by the
lectionary and is corrected.
| -rw-r--r-- | lib/kernel/liturgical_day.mli | 9 | ||||
| -rw-r--r-- | lib/kernel/validate.ml | 60 | ||||
| -rw-r--r-- | lib/kernel/validate.mli | 23 | ||||
| -rw-r--r-- | test/test_golden.ml | 174 | ||||
| -rw-r--r-- | test/test_validate.ml | 108 |
5 files changed, 366 insertions, 8 deletions
diff --git a/lib/kernel/liturgical_day.mli b/lib/kernel/liturgical_day.mli index a109251..f0ea3d9 100644 --- a/lib/kernel/liturgical_day.mli +++ b/lib/kernel/liturgical_day.mli @@ -20,6 +20,13 @@ type ('s, 'r) t = { omitted : ('r Celebration.t * string) list; (** with the reason, never silent -- Task 12's no-celebration-lost invariant reads this *) - citations : Citation.t list; (** always empty until Plan 4 *) + citations : Citation.t list; + (** The day's reading references, resolved by the rite's own + {!Rite.readings}. Empty for a rite whose lectionary is not built; + for EF, exactly one [First] and one [Gospel] on every day of every + year 1583..9999 -- asserted, not assumed, by {!Validate}'s own + ["citations"] / ["citations-unresolved"] checks. (This said "always + empty until Plan 4" until Task 10; the lectionary landed before + Plan 4 did, and the comment outlived its truth.) *) } [@@deriving sexp] diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index ffeb89e..1a0248b 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -388,5 +388,63 @@ let run (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) ~year = "admit is not a fixed point on this day's own commemorations: re-offering %d \ admitted %d back" (List.length offered) (List.length readmitted))) - resolved); + resolved; + (* ---- Citation invariants (the lectionary, Plan 4) ---- + + RITE-AGNOSTIC BY CONSTRUCTION, and this gating is the whole reason + these can live in the kernel beside the temporal checks rather than + in EF's own tests: a rite whose lectionary is not built yet returns + [] from {!Rite.readings} on every day, so [year_has_citations] is + false and not one of these fires. A rite that computes readings AT + ALL is held to all of them, on every day of its year. That is also + why test_validate.ml's own synthetic rite ([readings] a constant + [], "a harmless placeholder" in its own words) stays unaffected -- + checked, not assumed: its negative-path fixtures would otherwise + fail on every day of the year rather than on the one invariant each + is built to violate. + + The single [match] below expresses THREE invariants at once, which + is why it is a match on the sorted part list rather than three + separate tests: + + - zero or two, never one -- an Epistle without a Gospel, or the + reverse, is a malformed Mass, not a partial one; + - only [First] and [Gospel] ever appear -- the chants (Psalm, + Second, Tract, Alleluia, Sequence) are deliberately unbuilt, + with no source and no oracle, so a citation carrying one is a + defect and not a feature arriving early; + - no part appears twice -- two Epistles and no Gospel has length + two and would slip past a bare cardinality test. + + [Citation.part]'s own constructor order puts [First] before + [Gospel], so the sorted well-formed list is literally + [[First; Gospel]] and nothing else. *) + let year_has_citations = + Array.exists + (fun (d : ('s, 'r) Liturgical_day.t) -> d.Liturgical_day.citations <> []) + resolved + in + if year_has_citations then + Array.iter + (fun (d : ('s, 'r) Liturgical_day.t) -> + let date = d.Liturgical_day.date in + let parts = + List.map (fun (c : Citation.t) -> c.Citation.part) d.Liturgical_day.citations + in + match List.sort compare parts with + | [ Citation.First; Citation.Gospel ] -> () + | [] -> + (* Separate check name from the malformed case below on + purpose: this is the lectionary chain falling through + every one of its steps and resolving nothing, a COVERAGE + gap, where the other is a WELL-FORMEDNESS one. They want + different fixes and should be countable apart. *) + fail date "citations-unresolved" + "no reading citations resolved for this day: the lectionary chain fell through \ + every step" + | sorted -> + fail date "citations" + (Printf.sprintf "expected exactly one First and one Gospel, got [%s]" + (String.concat "," (List.map Citation.part_to_string sorted)))) + resolved); List.rev !failures diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli index b46ca30..385e111 100644 --- a/lib/kernel/validate.mli +++ b/lib/kernel/validate.mli @@ -78,6 +78,29 @@ val failure_to_string : failure -> string was not exceeded" available without embedding a rite's specific numeric caps (RG 111's, for EF) into kernel code. + Two further labels (Task 10) check the day's reading {!Citation.t}s. Both + are GATED on the rite producing at least one citation somewhere in the + year: a rite whose lectionary is not built returns [[]] from + {!Rite.readings} on every day and is held to neither, so this stays a + check on rites that HAVE readings rather than a demand that every rite + have them. + - ["citations"]: well-formedness. A day's citation parts, sorted, are + exactly [[First; Gospel]]. This single condition carries three + invariants at once: zero or two but never one (an Epistle without a + Gospel, or the reverse, is a malformed Mass rather than a partial one); + no part outside [First]/[Gospel] (the chants -- Psalm, Second, Tract, + Alleluia, Sequence -- are deliberately unbuilt, so one appearing is a + defect, not a feature arriving early); and no part twice (two Epistles + and no Gospel has length two and would pass a bare cardinality test). + - ["citations-unresolved"]: coverage. A day resolved NO citations at all, + i.e. the rite's own lookup chain fell through every one of its steps. + Deliberately a separate label from ["citations"] above: a coverage gap + and a well-formedness fault want different fixes and should be + countable apart. On the EF data as it stands this label has no live + witness -- every day of every year 1583..9999 resolves exactly one + Epistle and one Gospel -- which is precisely why test_validate.ml + carries a synthetic fixture proving it can fire at all. + 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 diff --git a/test/test_golden.ml b/test/test_golden.ml index 8d33e29..e9b3ec5 100644 --- a/test/test_golden.ml +++ b/test/test_golden.ml @@ -55,6 +55,7 @@ module Slug = Colitur_kernel.Slug module Date = Colitur_kernel.Date module Cel = Colitur_kernel.Celebration module Colour = Colitur_kernel.Colour +module Citation = Colitur_kernel.Citation module Temporal = Colitur_kernel.Temporal module Prec = Colitur_kernel.Precedence module V = Rite_ef.Vocab_ef @@ -170,6 +171,42 @@ let describe (day : (V.season, V.rank) LD.t) = let check ~msg y m d expected = Alcotest.(check string) msg expected (describe (fetch y m d)) +(* ---- Task 10: the reading citations ---- + + A SEPARATE formatter rather than widening [describe] itself, and the + reason is this file's own opening rule, not convenience. Widening + [describe] would invalidate all ~30 expected literals above at once, and + the only practical way to restore them would be to run the suite and paste + back whatever colitur printed -- "copied from a `colitur day` run and then + rationalised", the exact thing the header forbids. Restoring them + HONESTLY would mean hand-verifying 30 further Masses against the scans, + which is a task of its own and not this one. + + So the trade is stated rather than hidden: the pins above stay + citation-blind, and the pins below carry citations for one day per chain + step, every literal hand-verified against the photographic scans BEFORE + being typed here (each pin's own comment carries its scan line numbers). + That division is defensible because layer 2 now covers what breadth would + have bought: {!Colitur_kernel.Validate}'s own citation checks assert the + SHAPE of every day's citations in every year 1583-9999 -- far more days + than 30 pins could -- so what layer 5 still owes is specific VALUES on the + distinct routes, which is exactly what these six are. *) +let describe_readings (day : (V.season, V.rank) LD.t) = + let part_ref p = + match + List.find_opt (fun (c : Citation.t) -> c.Citation.part = p) day.LD.citations + with + | Some c -> c.Citation.reference + | None -> "-" + in + Printf.sprintf "%s slug=%s first=%s gospel=%s" + (Date.to_iso8601 day.LD.date) + (slug_s day.LD.observed) + (part_ref Citation.First) (part_ref Citation.Gospel) + +let check_readings ~msg y m d expected = + Alcotest.(check string) msg expected (describe_readings (fetch y m d)) + let omitted_has (day : (V.season, V.rank) LD.t) slug = List.exists (fun (c, _) -> slug_s c = slug) day.LD.omitted @@ -1122,6 +1159,128 @@ let test_major_litanies_transfer_2011_easter_monday () = "2011-04-26 tuesday season=paschaltide week=1 slug=ef-easter-1-tuesday rank=class-1 colour=white \ subject=temporal name_la=- comms=[major-litanies:privileged] in=- out=[]" +(* ---- Task 10: one pin per step of the reading-resolution chain ---- + + The chain has four steps, and a citation regression is far easier to + diagnose when the failing pin names WHICH step broke. Every literal below + was read out of the photographic scans first (line numbers given per pin), + then compared with colitur -- not the other way round. + + Step 4 deserves special note: it is the ONE step with no external oracle + witness of any kind (register ยง6.7 -- the five Common-routed saints are + the observed office on just five days in all of 2005-2050, and not one + falls inside layer 4's own 2026-2027 fixture window; layer 3 sees those + days but lectio resolves the literal "-"/"-" sentinel there, which is what + C18 is gated on, so it confirms only that colitur emits SOMETHING). These + two pins are therefore the first independent confirmation that route has + ever had, which is also why step 4 gets two of the six rather than one. *) + +(* STEP 1 -- a sanctoral proper: the citation lives on the Celebration + itself, no walk, no Common. 8 March 1938^H2038, "S. Ioannis a Deo Conf., + III classis": "Lectio libri Sapientiae. Eccli. 31, 8-11" / "Sequentia + sancti Evangelii secundum Matthaeum. Mt. 22, 34-46" (scan1.txt:27732-27734 + + 27769-27770; scan2.txt:30698-30699 + 30733-30736; page image p. 485). + The Missal prints him a FULL Mass with its own assigned Gospel -- the + Epistle happens to coincide with the Common of a Confessor not a Bishop's, + but the Gospel does not (that Common has Luke 12:35-40), which is what + makes this a proper and not a Common, and so a step-1 case rather than a + step-4 one. NOTE the plan named 2030-01-13 for this step; that date is a + TEMPORAL day (Holy Family, carried on the generic Sunday slug per + RG 17(b)) and would not have exercised step 1 at all. *) +let test_readings_step1_sanctoral_proper () = + check_readings ~msg:"step 1: sanctoral proper (John of God, 8 March)" 2038 3 8 + "2038-03-08 slug=john-of-god first=Ecclus 31:8-11 gospel=Matt 22:34-46" + +(* STEP 2 -- a temporal day with its own direct lectionary entry. 23 February + 2026 is "Feria II post dominicam I in Quadragesima" (heading, scan1.txt: + 8137): "Lectio Ezechielis Prophetae. Ezech. 34, 11-16" (scan1.txt:8138- + 8139) / "Sequentia sancti Evangelii secundum Matthaeum. Mt. 25,31-46" + (scan1.txt:8199). A Lenten feria is the right shape here because Lent's + ferias each have their OWN Mass -- they never walk back, so a regression + in step 3 cannot mask a regression in step 2 on this date. + The book abbreviation is "Ezech", not "Ezek": this pin was first written + from the scan as "Ezek 34:11-16" and failed, and the difference turned out + to be notation alone -- colitur's own spelling is in fact the Missal's own + ("Ezech. 34, 11-16", above). Recorded rather than quietly amended, since a + failing pin whose only fault is an abbreviation is exactly the kind of + thing a later reader will otherwise re-litigate. Cross-engine abbreviation + differences are normalised away in layer 3 (test_differential.ml's own A/B + normalisation) and so are invisible there; this layer sees them. *) +let test_readings_step2_temporal_proper () = + check_readings ~msg:"step 2: temporal proper (Lent I Monday)" 2026 2 23 + "2026-02-23 slug=ef-lent-1-monday first=Ezech 34:11-16 gospel=Matt 25:31-46" + +(* STEP 3 -- the ferial resumption: a day with NO Mass of its own, which + therefore repeats its preceding Sunday's. 1 December 2025 is the Monday + after Advent I, and Advent's ferias (unlike Lent's) have no proper Mass, + so the citation must be Advent I Sunday's own: "ad Romanos. Rom. 13, + 11-14" (scan1.txt:4878) / "dum Lucam. Luc. 21, 25-33" (scan1.txt:4912). + That the pinned value equals the SUNDAY's, not the Monday's own, is the + whole point of the pin. *) +let test_readings_step3_ferial_resumption () = + check_readings ~msg:"step 3: ferial resumption (Advent I Monday reads Advent I Sunday)" 2025 12 1 + "2025-12-01 slug=ef-advent-1-monday first=Rom 13:11-14 gospel=Luke 21:25-33" + +(* STEP 4 (a) -- the Common route. 6 March 2038, "Ss. Perpetuae et + Felicitatis Martyrum, III classis", whose own entry directs: "Missa Me + exspectaverunt, de Communi non Virginum I loco [35]" (scan1.txt:27634- + 27635). That Common -- COMMUNE NON VIRGINUM, "Pro Martyre non Virgine" + (scan1.txt:42560 ff) -- reads "Lectio libri Sapientiae. Eccli. 51, 1-8 et + 12" (scan1.txt:42589-42590) and "Sequentia sancti Evangelii secundum + Matthaeum. Mt. 13, 44-52" (scan1.txt:42606). 2038 is the only year in + 2005-2050 in which she is the OBSERVED office at all. *) +let test_readings_step4_common_felicitas () = + check_readings ~msg:"step 4: Common of Non-Virgins I (Perpetua & Felicitas)" 2038 3 6 + "2038-03-06 slug=sts-felicitas-perpetua first=Ecclus 51:1-8, 12 gospel=Matt 13:44-52" + +(* STEP 4 (b) -- the SECOND Common, deliberately a different one, so the pin + pair distinguishes "the Common route works" from "one Common's data is + right". 9 March 2038, "S. Franciscae Romanae Vid., III classis", directed + to "Missa Cognovi, de Communi non Virginum" -- the second Mass of that + same Common, which reads "Lectio libri Sapientiae. Prov. 31, 10-31" + (scan1.txt:42679) and shares the Gospel "Mt. 13, 44-52" (scan1.txt:42720). + The shared Gospel with (a) is the Missal's own doing, not a colitur + collapse -- which is exactly why both Epistles are pinned too. *) +let test_readings_step4_common_frances () = + check_readings ~msg:"step 4: Common of Non-Virgins II (Frances of Rome)" 2038 3 9 + "2038-03-09 slug=frances-rome first=Prov 31:10-31 gospel=Matt 13:44-52" + +(* THE DISPLACED-SUNDAY FERIA -- the case that separates the temporal slug + from the observed one, and the one the plan singles out. It is pinned + here as KNOWN-DIVERGENT OUTPUT, deliberately and with the divergence + named, NOT blessed as correct: this is test_oracle.ml's own M26 shape 2(b) + (verdict open). 26 October 2026 is a feria of the week whose Sunday was + displaced by Christ the King (I class, movable, "Dominica ultima + octobris"). The general mechanism -- a week's ferias follow their OWN + Sunday's temporal identity even when that Sunday is impeded -- is the + shape RG 69 establishes for the Nativity Octave, so the displaced ordinary + Sunday's Mass is what the ferias should read; colitur's step 3 instead + walks back to the DISPLACING feast and emits Christ the King's own Gospel + (John 18:33-37, "Art thou a king?"), which is the literal in this pin. + No Missal-propers rubric specific to Christ the King's own week was found + (checked: scan1.txt:39140-39163, no rubric precedes that Mass heading, + unlike Holy Name's and Holy Family's own), so M26 stays verdict open + rather than being asserted against a citation that does not exist. + WHEN M26 IS FIXED THIS PIN MUST FAIL -- that is its purpose. Update it + deliberately then; do not regenerate it. + + Two things this pin established that M26's own note did not record. First, + BOTH parts come from the displacing feast, not only the Gospel M26 cites: + the Epistle here is Col 1:12-20, which is Christ the King's own, so step 3 + is transplanting the whole Mass rather than half of it. Second, the + reference carries a TRAILING PERIOD ("Col 1:12-20."), a blemish inherited + through the bootstrap from the source data. It is pinned verbatim rather + than tidied, because this pin's job is to state what colitur actually + emits today; the period is noted here as a separate, cosmetic data defect + and is deliberately not fixed under a task about test coverage. Layer 3 + cannot see it (its A/B normalisation strips punctuation before comparing), + which is why it surfaced here first. *) +let test_readings_displaced_sunday_feria_known_divergent () = + check_readings + ~msg:"displaced-Sunday feria: pins M26 shape 2(b)'s KNOWN-WRONG walkback, not correct output" + 2026 10 26 + "2026-10-26 slug=ef-time-after-pentecost-22-monday first=Col 1:12-20. gospel=John 18:33-37" + let suite = ( "golden pins (known-tricky years)", [ Alcotest.test_case "Easter extreme: 1598 earliest (22 Mar, Gauss-verified)" `Quick @@ -1199,5 +1358,18 @@ let suite = `Quick test_major_litanies_displaces_mark_on_ii_class_sunday; Alcotest.test_case "RG80's second trigger: Easter Monday = 25 April, the Litanies transfer to Easter+2 (2011)" `Quick - test_major_litanies_transfer_2011_easter_monday + test_major_litanies_transfer_2011_easter_monday; + Alcotest.test_case "readings step 1: sanctoral proper (John of God, 2038-03-08)" `Quick + test_readings_step1_sanctoral_proper; + Alcotest.test_case "readings step 2: temporal proper (Lent I Monday, 2026-02-23)" `Quick + test_readings_step2_temporal_proper; + Alcotest.test_case "readings step 3: ferial resumption (Advent I Monday, 2025-12-01)" `Quick + test_readings_step3_ferial_resumption; + Alcotest.test_case "readings step 4: Common of Non-Virgins I (2038-03-06)" `Quick + test_readings_step4_common_felicitas; + Alcotest.test_case "readings step 4: Common of Non-Virgins II (2038-03-09)" `Quick + test_readings_step4_common_frances; + Alcotest.test_case + "readings: displaced-Sunday feria pins M26 shape 2(b)'s KNOWN-WRONG walkback (2026-10-26)" `Quick + test_readings_displaced_sunday_feria_known_divergent ] ) 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; |
