summaryrefslogtreecommitdiff
path: root/test/test_precedence_ef.ml
diff options
context:
space:
mode:
authorLukasz Kasprzak <lukas@labunix.xyz>2026-08-12 10:18:17 +0200
committerLukasz Kasprzak <lukas@labunix.xyz>2026-08-12 10:18:17 +0200
commitf2b8700f5e9c01bbca219967470a4ed34ad5584f (patch)
treebcdeff232f6d53a9bba3d9a52b9d53248ad2b575 /test/test_precedence_ef.ml
parent37e058066a5f17db6c3d577703c0a39065ea8117 (diff)
downloadcolitur-f2b8700f5e9c01bbca219967470a4ed34ad5584f.tar.gz
colitur-f2b8700f5e9c01bbca219967470a4ed34ad5584f.zip
test(precedence-ef): witness the RG26 Class4 gate and correct a vacuous guard claim
Item 2(a): the RG 26 omission gate (rank = Class4) is extensionally identical, over every candidate this engine actually constructs, to the refuted "privilege_of loser = Ordinary" predicate it replaced -- confirmed by enumerating the whole candidate space over 1583-9999, substituting the old predicate back leaves 257/257 green and byte-identical output. Adds a synthetic row: a temporal-origin, Ordinary-privilege Class3 loser, which the two gates disagree on (RG26: Commemorate; the refuted gate: Omit, since it never looked at rank). Reverting the gate to the old predicate turns exactly this row red: Expected: "Commemorate(Ordinary)" Received: "Omit" Item 2(b): the existing "RG33 boundary" row's comment claimed it proved the RG26 branch's own (not (is_vigil ...)) guard. It does not: the vigil sourced there is Class2, already excluded by the branch's rank = Class4 test alone, with or without the vigil guard -- verified by deleting the guard, which leaves 257/257 green. Corrected the comment to say what the row actually shows (RG31's "if impeded, commemorated" vigil mandate, a real and separate fact worth keeping) and added a genuinely discriminating synthetic row: a temporal-origin Class4 loser whose slug is ALSO vigil-shaped, a combination RG 91 does not describe but Precedence.resolve can still be asked to construct. Deleting the guard turns this row red: Expected: "Commemorate(Ordinary)" Received: "Omit" Both reversions were applied locally to precedence_ef.ml, confirmed, and reverted; the committed .ml is unchanged. Test count 257 -> 259, both new rows green under the current, correct code.
Diffstat (limited to 'test/test_precedence_ef.ml')
-rw-r--r--test/test_precedence_ef.ml71
1 files changed, 65 insertions, 6 deletions
diff --git a/test/test_precedence_ef.ml b/test/test_precedence_ef.ml
index 9bd9b7f..efbdb04 100644
--- a/test/test_precedence_ef.ml
+++ b/test/test_precedence_ef.ml
@@ -376,19 +376,50 @@ let disposition_cases =
"Omit" );
(* RG 33's own boundary, proved from both sides so the rule is shown to
gate on the WINNER too, not "any vigil is always omitted": winner is
- neither a Sunday nor I class, so RG 33's omission does not fire; the
- vigil is temporal-origin ({!of_temporal}, the real Ascension Vigil)
- and would otherwise land in Task 16's new "ordinary temporal loser ->
- Omit" branch too (see the IV-class-feria row further down) -- this
- row is what proves that branch's own [not (is_vigil ...)] guard: a
+ neither a Sunday nor I class, so RG 33's omission does not fire; a
vigil, per RG 31's own text ("si impediuntur, commemorantur"), is
ALWAYS commemorated once RG 33 does not omit it outright, regardless
- of RG 109's closed list. *)
+ of RG 109's closed list.
+
+ CORRECTED comment (final fix wave, item 2b): this row's own comment
+ used to claim it "proves [the RG26 Class4-Omit branch's] own [not
+ (is_vigil ...)] guard" -- that claim does NOT survive under the
+ current [rank = Class4] gate (it may have been true under an earlier
+ predicate). The vigil sourced here ({!of_temporal}, the real
+ Ascension Vigil) is [Class2], not [Class4], so the RG26 branch's own
+ [rank = Class4] test already excludes it on rank alone, with or
+ without the [not (is_vigil ...)] guard -- verified: deleting that
+ guard entirely leaves 257/257 green. This row still genuinely proves
+ RG 31's own "if impeded, commemorated" vigil mandate (a vigil that
+ RG 33 does not omit outright is commemorated, not omitted by some
+ OTHER mechanism), which is real and worth keeping; it just does not
+ discriminate the [not (is_vigil ...)] guard specifically. *)
( "RG33 boundary: vigil loses to an ordinary (non-Sunday, non-I-class) \
II-class day -> Commemorate, NOT Omit (RG31's own vigil mandate)",
cand ~origin:P.Sanctoral ~rank:V.Class2 ~layer:PE.universal_layer "ef-some-other-feast",
of_temporal (off 38),
"Commemorate(Ordinary)" );
+ (* The GENUINE witness for the RG26 branch's [not (is_vigil ...)] guard
+ (final fix wave, item 2b): no REAL vigil this engine constructs can
+ exercise it, since RG 91 has no IV-class vigil at all (this file's own
+ entry-27/28 comments) -- every real vigil is Class2 or Class3, already
+ excluded by [rank = Class4] alone, the exact shape the row above is.
+ This row is therefore deliberately SYNTHETIC: a temporal-origin loser,
+ [Class4], whose slug ALSO carries {!PE.vigil_suffix} -- a shape RG 91
+ itself does not describe, but one {!Precedence.resolve} can still be
+ asked to construct (see precedence_ef.ml's own comment on this guard).
+ With the guard present, [is_vigil] excludes it from the RG26 branch,
+ so it falls through to the ordinary [Commemorate] catch-all (RG 31's
+ "if impeded, commemorated" mandate, the same rule the row above
+ exercises for a realistic Class2 vigil). Deleting [not (is_vigil ...)]
+ from that branch turns this row -- and only this row -- red: the
+ branch would then fire on [rank = Class4] alone and return [Omit]. *)
+ ( "SYNTHETIC (final fix wave, item 2b): a temporal-origin Class4 loser \
+ ALSO vigil-shaped is Commemorate (RG31's vigil mandate via the \
+ not-is_vigil guard), not Omit",
+ an_ordinary_sunday,
+ cand ~rank:V.Class4 "ef-synthetic-class4-vigil",
+ "Commemorate(Ordinary)" );
(* CORRECTED 2026-08-12 (Task 16, primary-source-verified): the register
previously (mis-)transcribed RG 33 as covering only I/II-class
vigils, so this row's own title used to read "outside RG33's
@@ -480,6 +511,34 @@ let disposition_cases =
Commemorate(Ordinary)",
an_ordinary_sunday,
cand ~origin:P.Sanctoral ~rank:V.Class4 ~layer:PE.universal_layer "ef-some-minor-saint",
+ "Commemorate(Ordinary)" );
+ (* Final fix wave, item 2(a): the RG 26 gate above is [rank = Class4],
+ and until this row nothing in the suite discriminated that from the
+ REFUTED predicate it replaced, [privilege_of loser = Ordinary]
+ (precedence_ef.ml's own comment on this branch names that exact
+ predicate as the wrong reading it corrects). The two predicates are
+ extensionally identical over every candidate this engine actually
+ constructs -- confirmed by enumerating the whole candidate space over
+ 1583-9999: substituting the old predicate back leaves 257/257 green
+ and produces byte-identical `colitur day` output for every sampled
+ year. No REALISTIC row can tell them apart, so this one is
+ deliberately SYNTHETIC: a temporal-origin loser, [Class3] (not
+ [Class4]), whose slug matches none of RG 109(a)-(f) -- [privilege_of]
+ therefore returns [Ordinary] for it, the SAME privilege value as the
+ Class4 row above. The two gates now diverge: RG 26 ([rank = Class4])
+ says this loser is NOT a IV-class feria, so it falls through to the
+ ordinary [Commemorate] branch (RG 24/25's mandate for a II/III-class
+ feria); the refuted gate ([privilege_of loser = Ordinary]) tests only
+ the privilege value, which is [Ordinary] here exactly as it is for
+ the Class4 row, so it would wrongly return [Omit]. Reverting the
+ branch's condition to [privilege_of loser = Ordinary] turns this row
+ (and only this row, of the two) red -- see the final-fix-report for
+ the exact Alcotest failure message this produces and its reversion. *)
+ ( "SYNTHETIC (final fix wave, item 2a): a temporal-origin ORDINARY \
+ Class3 loser is Commemorate under RG26 (rank=Class4 gate), would be \
+ Omit under the refuted privilege_of=Ordinary gate",
+ an_ordinary_sunday,
+ cand ~rank:V.Class3 "ef-synthetic-ordinary-class3-feria",
"Commemorate(Ordinary)" )
]