summaryrefslogtreecommitdiff
path: root/test/test_precedence_ef.ml
diff options
context:
space:
mode:
authorLukasz Kasprzak <lukas@labunix.xyz>2026-08-13 12:44:15 +0200
committerLukasz Kasprzak <lukas@labunix.xyz>2026-08-13 12:44:15 +0200
commitdc00d1f730b23fa99cd15ff142ecba515a9fe0b7 (patch)
treee40f7f003008b33104723a6d8856168bbdea7633 /test/test_precedence_ef.ml
parent59fbda87d565ad9b98c2493e9703390cd988609d (diff)
parente45ec1ccce68d9edb9655004c21861d6bfb33a9d (diff)
downloadcolitur-dc00d1f730b23fa99cd15ff142ecba515a9fe0b7.tar.gz
colitur-dc00d1f730b23fa99cd15ff142ecba515a9fe0b7.zip
Merge branch 'ef-holyname-rg110': the Holy Name of Jesus, RG 110
Builds the Most Holy Name of Jesus with the fallback RG 17(a) and the calendarium both specify -- 'secus die 2 ianuarii', 'vel, ea deficiente, die 2 ianuarii' -- which was unimplemented, so in 3619 of the domain's 8417 years a II-class feast did not exist at all. Also retags it as a feast of the Lord per RG 91 entry 14. Builds RG 110's inseparable Peter/Paul commemoration ('in numero orationum computando, pro unica habeantur') across the three calendarium pairs, and adds the 30 June companion, which was missing from lectio's source and from missalemeum's output alike -- corroborated in both photographic scans plus RG 124(c), and added through adjustments.sexp so the bootstrap's provenance stands. 14627 days change, in four shapes, none unclassified. The register's earlier 852-day estimate for RG 110 reconciles exactly as the Lent Ember subset of one shape: 288 + 284 + 280. RG 110(c)'s ordering was implemented backwards at first and corrected: 'huic orationi additur altera' attaches the companion to the trigger's own oration, so it follows it, where (a) and (b) attach to the day's and so precede everything. The 'ante omnes alias commemorationes' half remains unimplemented and is unreachable by construction -- shape (c) needs the trigger to lose while still being admitted, which only a I-class day or a II-class Sunday allows, and both RG 111 caps are one. Records a fifth way the validation layers can be green while wrong: nothing anywhere compares commemoration order.
Diffstat (limited to 'test/test_precedence_ef.ml')
-rw-r--r--test/test_precedence_ef.ml235
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"