diff options
Diffstat (limited to 'test/test_precedence_ef.ml')
| -rw-r--r-- | test/test_precedence_ef.ml | 235 |
1 files changed, 234 insertions, 1 deletions
diff --git a/test/test_precedence_ef.ml b/test/test_precedence_ef.ml index 4ee2fd8..ed9a933 100644 --- a/test/test_precedence_ef.ml +++ b/test/test_precedence_ef.ml @@ -1016,6 +1016,43 @@ let sixtus = UNIVERSALLY), so the two values coinciding is the faithful shape, not a simplification that dodges the new parameter. The last two rows are where they genuinely differ -- see their own comment. *) +(* RG 110 (§4, Caput XIV): candidates built with the REAL trigger/companion + slugs {!PE.rg110_companion_slug} matches on -- unlike every other + [admit_cases] candidate above, which is deliberately built with a + SYNTHETIC slug {!PE.band}'s 28 branches (and this file's own RG 110 + lookup) cannot recognise, these three rows need [PE.admit] to recognise + the slug itself, so the real ones are used directly. [~status: + Cel.Commemoration_only] on the companions matches the real data shape + (data/ef/sanctoral.sexp's own [peter]/[paul]; + data/ef/adjustments.sexp's own [commemoration-of-st-peter]) even though + [admit] itself never reads [status] -- only [Precedence.resolve]'s own + partition does, upstream of [admit] -- kept for a reader's sake, not a + test requirement. *) +let chair_of_st_peter_synth = cand ~rank:V.Class2 "chair-of-st-peter" +let paul_companion_synth = cand ~rank:V.Class3 ~status:Cel.Commemoration_only "paul" + +(* An unrelated third commemoration, sorting AFTER both members of the RG110 + pair, so that "spliced immediately after its trigger" and "appended at the + end" give different answers. Added by the fix-round re-review (G1): with + only the pair present the two are indistinguishable, and the re-review + proved an append-at-end variant passed the whole suite green. Class3 + Commemoration_only so it cannot win the day; its slug is deliberately not + one {!PE.rg110_companion_slug} recognises. *) +let unrelated_comm_synth = + cand ~rank:V.Class3 ~status:Cel.Commemoration_only "zzz-unrelated-commemoration" + +(* Any real Lent/Ember feria's own shape (a Class3, PRIVILEGED, temporal- + origin candidate) -- {!PE.rg110_companion_slug} does not match this slug, + so it is a neutral bystander in [admit]'s own normal (pre-RG110) contest, + exactly like [privileged_lo] elsewhere in this table, just kept + separately named so this block's own rows are self-contained and do not + depend on a binding declared for an unrelated purpose above. Given the + WORSE (higher) precedence int than [paul_companion_synth] would need to + win the day's one "other II class" slot on its own dignity ALONE -- the + whole point of the row below is that RG 110 does not care who wins that + contest; it adds Paul regardless. *) +let lent_feria_synth = (cand ~origin:P.Temporal ~rank:V.Class3 "ef-lent-2-monday-synth", P.Privileged, 180) + let admit_cases = [ (* RG 111 (§4): "I class: none save one privileged." *) ( "I-class day, only an ordinary commemoration due -> none admitted", @@ -1109,7 +1146,98 @@ let admit_cases = admitted", lord_winner, lord_winner, [ po sixtus P.Ordinary ], - [ "pope-sixtus-ii-felicissimus-and-agapitus-martyrs" ] ) + [ "pope-sixtus-ii-felicissimus-and-agapitus-martyrs" ] ); + (* RG 110, shape (a)/(b): [chair-of-st-peter] observed, a competing + PRIVILEGED Lent feria also due for the day's single "other II class" + slot (RG 111(c) itself has no privilege-override clause -- unlike the + Sunday branch above -- so pure precedence order decides that slot on + its own, and [lent_feria_synth]'s own 180 beats + [paul_companion_synth]'s 999). Without RG 110, this is exactly + precedence_ef.ml's own measured defect (3,533 of 8,417 domain-wide + years, this task's own report): Paul loses the slot outright and is + never admitted at all. With RG 110, Paul is added ADDITIONALLY, + PREPENDED ahead of the feria -- RG 110(a)/(b)'s own text ("oratio + alterius Apostoli additur ... orationi diei", the companion's oration + added to the DAY's own oration) governs here, not (c)'s "ante omnes + alias commemorationes" (CORRECTED, fix round 1, coordinator finding + F1: this comment previously cited (c) for both shapes uniformly -- + see [rg110_additions]'s own comment in precedence_ef.ml for why the + two shapes need, and get, DIFFERENT orderings, not the same one for + different reasons) -- both admitted, not one displacing the other. *) + ( "RG110 (a)/(b): chair-of-st-peter observed, Paul rides alongside a \ + competing privileged Lent feria, uncapped and prepended", + chair_of_st_peter_synth, chair_of_st_peter_synth, + [ (paul_companion_synth, P.Ordinary, 999); lent_feria_synth ], + [ "paul"; "ef-lent-2-monday-synth" ] ); + (* RG 110, shape (c): [chair-of-st-peter] itself LOSES the day outright + (observed is some unrelated II-class Sunday) but is admitted, on its + OWN Class2 dignity, as RG 111(b)'s single ordinary commemoration -- + exactly the domain-wide 593-year pattern this task's own report + measures. RG 110(c)'s own text, word for word ("quoties vero oratio + unius Apostoli addenda est ad modum commemorationis, HUIC ORATIONI + ADDITUR ALTERA immediate, ante omnes alias commemorationes"): the + companion (Paul, Class3, no standing of its OWN for this Sunday's + rank-floored slot) rides along anyway, uncapped -- ADDED TO THE + TRIGGER'S own oration ("huic orationi additur altera"), i.e. + FOLLOWING it, not preceding it. CORRECTED, fix round 1 (coordinator + finding F1): this row originally asserted `["paul"; + "chair-of-st-peter"]` -- the companion BEFORE the trigger -- citing + the SAME "ante omnes alias commemorationes" clause that actually + governs the PAIR's position relative to OTHER, unrelated + commemorations, not the pair's own internal order. "Huic orationi" + (dative, "to THIS oration") refers back to "oratio unius Apostoli", + the trigger's own oration -- so the companion is added TO it, + following, not leading. Reproduced by mutation: reverting + [rg110_additions]'s shape-(c) branch back to a uniform prepend + reddens exactly this row's own expected order, nothing else. *) + ( "RG110 (c): chair-of-st-peter admitted merely AS a commemoration \ + (loses the day to an ordinary II-class Sunday), Paul rides along \ + AFTER it (RG110(c): \"huic orationi additur altera\")", + cand ~rank:V.Class2 "ef-some-other-sunday", cand ~rank:V.Class2 "ef-some-other-sunday", + (* A third, unrelated candidate is OFFERED here deliberately, and is + correctly NOT admitted -- which is itself the point. + + The fix-round re-review asked for a third commemoration so that + "spliced IMMEDIATELY after its own trigger" (RG110(c)'s own word) + could be told apart from "appended at the end of the list": with a + single-member result the two coincide, and it proved an + append-at-end variant passed the whole suite green. + + Attempting it establishes something better than the test it asked + for: on this day-shape a third commemoration is RUBRICALLY + IMPOSSIBLE, so the distinction is unobservable BY CONSTRUCTION, not + merely unobserved. Shape (c) requires the trigger to LOSE the day + while still being admitted -- and a Class2 trigger can only lose to + a I-class day (RG 111(a): one privileged commemoration) or a + II-class Sunday (RG 111(b): one, and "scilicet de festo II + classis"). Both caps are ONE. Anything a third candidate could be + is either outranked by the trigger or excluded by the rank floor; + here [zzz-unrelated-commemoration] is Class3 and RG 111(b) drops + it, leaving the pair alone. + That is why the re-review's own domain sweep found shape (c) never + co-occurring with a third commemoration in 8 417 years: not an + accident of the data, a consequence of the rubric. + + So RG110(c)'s "ante omnes alias commemorationes" half has no + reachable witness in the EF's real rubrical space, and the + adjacency this row asserts is exercised only against the pair + itself. The append-at-end variant therefore remains + indistinguishable from the splice on any input the engine can + actually construct -- recorded in the register rather than papered + over with a synthetic row that proves a shape no rubric permits. *) + [ po chair_of_st_peter_synth P.Ordinary; + (paul_companion_synth, P.Ordinary, 999); + po unrelated_comm_synth P.Ordinary ], + [ "chair-of-st-peter"; "paul" ] ); + (* Defensive: a trigger slug is [observed], but its companion is simply + not present among [comms] at all (a data gap, or -- as this exact + shape was for 30 June before this task's own [Add + commemoration-of-st-peter] directive -- an upstream omission). + {!PE.rg110_find_companion} must return [None] gracefully, not raise; + the day's own (empty, here) normal result is unaffected. *) + ( "RG110 defensive: chair-of-st-peter observed, no companion present in \ + comms at all -> no crash, nothing added", + chair_of_st_peter_synth, chair_of_st_peter_synth, [], [] ) ] (* Order independence (brief: "the admitted set must not depend on input @@ -1426,6 +1554,103 @@ let test_class1_feast_inside_holy_familys_window_end_to_end () = Alcotest.failf "expected exactly one Privileged commemoration (Holy Family), got %d" (List.length other)) +(* Most Holy Name of Jesus (RG 17(a)) -- the SAME two proofs immediately + above, restated for Holy Name instead of Holy Family. UNLIKE Holy Family, + there is no LIVE collision to exercise here (this file's own [cases]/ + [disposition_cases] rows never construct one, because + data/ef/sanctoral.sexp has nothing fixed-date 2-5 January besides + [telesphorus-pope-and-martyr] (5 Jan, Commemoration_only, so it can never + contest [observed] at all -- {!P.resolve}'s own partition holds it out of + the band contest entirely) -- register §6.2's own account: "no live + collision exists for it in this codebase's current data". These two + tests are the SYNTHETIC proof the task brief asked for instead: that + {!band}'s [entry_14_movable_band]/RG 112(a) mechanism, ALREADY proved + above for Holy Family, governs Holy Name identically, since neither + {!band} nor {!disposition} key on anything Holy-Family-specific (only on + [subject]/[rank]/[origin], which [temporal_ef.ml]'s fix now sets + identically for both feasts) -- not a live-data regression test, a + mechanism-generalises-correctly one, the same distinction this file's own + header draws between a table row and an end-to-end proof. + + Run against BOTH of RG 17(a)'s own shapes -- the Sunday (2026-01-04) and + the 2 January fallback (2029-01-02, {!T.holy_name_fallback_date}) -- + because [temporal_ef.ml]'s own fallback-branch comment claims both band + identically at {!PE.entry_14_movable_band} (ONE feast, not two + differently-classified ones); a table proving the SAME two outcomes hold + for both dates is direct evidence for that specific claim, not merely + for the Sunday shape colitur already had a name for before this task. *) +let holy_name_probe_dates = + [ ("Sunday shape (2026-01-04)", mk 2026 1 4); ("fallback shape (2029-01-02)", T.holy_name_fallback_date 2029) ] + +let test_holy_name_excludes_synthetic_lord_end_to_end () = + List.iter + (fun (label, date) -> + let holy_name = of_temporal date in + Alcotest.(check bool) (label ^ ": sanity -- temporal_ef really did tag this Lord") true + (holy_name.P.cel.Cel.subject = Sub.Lord); + let day_ctx = ctx date in + let synthetic_lord = + cand ~origin:P.Sanctoral ~rank:V.Class2 ~subject:Sub.Lord ~layer:PE.universal_layer + "ef-synthetic-fixed-lord-probe" + in + let resolution = P.resolve real_rules day_ctx ~temporal:holy_name ~sanctoral:[ synthetic_lord ] in + Alcotest.(check string) (label ^ ": Holy Name is observed (RG91 e14: movable first)") + (S.to_string holy_name.P.cel.Cel.slug) (S.to_string resolution.P.observed.P.cel.Cel.slug); + Alcotest.(check int) (label ^ ": no commemorations at all -- RG112(a)'s own exclusion") 0 + (List.length resolution.P.commemorations); + Alcotest.(check (list string)) (label ^ ": the synthetic Lord candidate is OMITTED, not commemorated") + [ "ef-synthetic-fixed-lord-probe" ] + (List.map (fun (c, _) -> S.to_string c.P.cel.Cel.slug) resolution.P.omitted)) + holy_name_probe_dates + +(* A REAL asymmetry this test found between the two shapes, kept explicit + rather than papered over by forcing one uniform expectation on both -- + RG 109(a)'s privilege is textually "of a SUNDAY" (docs/research/rules- + register.md §4), read here via {!PE.is_sunday_slug}'s own substring test: + the Sunday shape's slug ("ef-holy-name-sunday") carries the marker and + the fallback shape's ("ef-holy-name") genuinely does not, because 2 + January genuinely is not a Sunday. So a losing Holy-Name-Sunday is + PRIVILEGED (RG109(a)) and survives RG111(a)'s "I class: none save one + privileged" cap when it loses to a higher day; a losing Holy-Name- + fallback has no RG109(a)-(f) category to claim (not a Sunday, not I + class, none of (c)-(f) either) and so is only ORDINARY -- which + RG111(a)'s own cap admits NONE of on a I-class day. Both outcomes are + individually correct readings of RG 109/111's own closed lists, not a + defect in either shape -- first observed as a test failure while writing + this pair (the original version of this test asserted one Privileged + commemoration for BOTH shapes uniformly and reddened here), traced to + this citation rather than forced to pass. *) +let test_class1_feast_inside_holy_name_window_end_to_end () = + List.iter + (fun (label, date, expect_privileged_commemoration) -> + let holy_name = of_temporal date in + let day_ctx = ctx date in + let synthetic_class1 = + cand ~origin:P.Sanctoral ~subject:Sub.Saint ~layer:PE.universal_layer "ef-synthetic-class1-probe-hn" + in + let resolution = P.resolve real_rules day_ctx ~temporal:holy_name ~sanctoral:[ synthetic_class1 ] in + Alcotest.(check string) (label ^ ": the I-class candidate is observed, NOT Holy Name (RG91 e11 beats e14-movable)") + "ef-synthetic-class1-probe-hn" (S.to_string resolution.P.observed.P.cel.Cel.slug); + Alcotest.(check (list string)) (label ^ ": nothing transfers") [] + (List.map (fun c -> S.to_string c.P.cel.Cel.slug) resolution.P.deferred); + if expect_privileged_commemoration then + match resolution.P.commemorations with + | [ (c, P.Privileged) ] -> + Alcotest.(check string) + (label ^ ": Holy Name itself is privileged-commemorated (RG109(a)), neither omitted nor transferred") + (S.to_string holy_name.P.cel.Cel.slug) (S.to_string c.P.cel.Cel.slug) + | other -> + Alcotest.failf "%s: expected exactly one Privileged commemoration (Holy Name), got %d" label + (List.length other) + else + Alcotest.(check int) + (label ^ ": RG111(a) admits none -- Holy Name's own commemoration here is Ordinary \ + (no RG109(a)-(f) category applies to a non-Sunday loser), and a I-class day admits \ + only a Privileged one") + 0 (List.length resolution.P.commemorations)) + [ ("Sunday shape (2026-01-04)", mk 2026 1 4, true); + ("fallback shape (2029-01-02)", T.holy_name_fallback_date 2029, false) ] + (* Completes Task 7's carried fix (RG 91 entry 8, §4): on a real Sunday landing on 2 November, All Souls does not merely lose (that was Task 7's [band] fix, proved by [test_all_souls_yields_to_sunday] above) -- it must @@ -1681,6 +1906,14 @@ let suite = "fix round 1, finding 1: a synthetic I-class candidate inside Holy Family's own window is \ observed and does not transfer (2026-01-11)" `Quick test_class1_feast_inside_holy_familys_window_end_to_end; + Alcotest.test_case + "RG112(a) + RG91 e14 \"primum mobilia\": Holy Name of Jesus excludes a synthetic fixed Lord \ + candidate entirely, both shapes (Sunday + fallback)" + `Quick test_holy_name_excludes_synthetic_lord_end_to_end; + Alcotest.test_case + "a synthetic I-class candidate inside Holy Name's own window is observed and does not \ + transfer, both shapes (Sunday + fallback)" + `Quick test_class1_feast_inside_holy_name_window_end_to_end; Alcotest.test_case "transfer_target: general RG96 search walks past more than one blocked day" `Quick test_transfer_target_general_multi_step_search; Alcotest.test_case "transfer_target: Annunciation exception starts at Monday after Low Sunday" |