From 37e058066a5f17db6c3d577703c0a39065ea8117 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Wed, 12 Aug 2026 10:15:33 +0200 Subject: kernel(precedence-ef): fix precedence_ef.mli's stale RG33/RG26/RG111(b) contract The .mli's disposition doc still said a Class1-or-Class2 vigil is Omit (RG 33) -- the pre-Task-16 mistranscription the register corrects at its RG 33 entry. The .ml has read Class2 || Class3 since commit 079e332; the .mli never caught up. It also named only vigil_suffix, when the vigil test the code actually runs also checks vigil_prefix (the shape the sanctoral bootstrap's four real vigils use); omitted RG 26's Class4 temporal-ferias-are-never-commemorated branch entirely, then asserted the listed cases 'exhaust every representable shape', which was false as written; and omitted RG 111(b)'s 'de festo II classis' rank floor from admit's doc, describing only the privilege-override half of that rule. Fixed all four: the vigil-omission bullet now names Class2/Class3 and both slug conventions; the missing RG 26 branch is now documented, folding the exhaustiveness claim into an accurate five-branch count; admit's Sunday case now states the rank floor as a second, independent condition. The same stale RG 109(e) reading this interface carried ('leaves the Advent and Lent Ember sets ordinary') also survived as the stated reason september_ember_prefix exists, in the .ml, about 330 lines from the already-corrected privilege_of comment it contradicts. Fixed there too: September is broken out because it sits outside RG 109(e)'s three named seasons entirely, not because Advent/Lent Ember needs excluding from (e) -- it does not, per privilege_of's own corrected comment. No behaviour change: both fixes are doc-comment-only edits to already- correct code (precedence_ef.ml's disposition/admit implementations were fixed in an earlier commit; only the .mli's prose and one earlier .ml comment lagged). --- lib/rites/rite_ef/precedence_ef.ml | 16 ++++-- lib/rites/rite_ef/precedence_ef.mli | 110 +++++++++++++++++++++++------------- 2 files changed, 84 insertions(+), 42 deletions(-) (limited to 'lib') diff --git a/lib/rites/rite_ef/precedence_ef.ml b/lib/rites/rite_ef/precedence_ef.ml index 88f1a54..bfd3b93 100644 --- a/lib/rites/rite_ef/precedence_ef.ml +++ b/lib/rites/rite_ef/precedence_ef.ml @@ -87,10 +87,18 @@ let is_vigil slug = [september_ember_prefix] is broken out as its own name (rather than an anonymous list literal) because Task 9's [privilege_of] needs to test the - September set alone, RG 109 privileging it while leaving the Advent and - Lent sets ordinary (register lines 375-376) -- building [ember_prefixes] - from it rather than duplicating the literal keeps the two from silently - drifting apart. *) + September set alone: RG 109(e)'s three named seasons (Advent, Lent, + Passiontide, §4 "Commemorations") never include September, which sits + entirely in time after Pentecost under any reading -- so September Ember + days need their own separate privilege category, (d), regardless of how + (e) itself is read. CORRECTED (fix round 1, F1/F2): this comment + previously justified the split the other way round, claiming RG 109(e) + privileges September specifically "while leaving the Advent and Lent + sets ordinary" -- WRONG; see [privilege_of]'s own (e) comment below for + the full argument. The Advent and Lent Ember sets ARE privileged under + (e), the same as any other Advent/Lent feria; building [ember_prefixes] + from this constant rather than duplicating the literal keeps the two + from silently drifting apart. *) let advent_ember_prefix = "ef-advent-ember-" let lent_ember_prefix = "ef-lent-ember-" let september_ember_prefix = "ef-september-ember-" diff --git a/lib/rites/rite_ef/precedence_ef.mli b/lib/rites/rite_ef/precedence_ef.mli index 8234bf3..161d890 100644 --- a/lib/rites/rite_ef/precedence_ef.mli +++ b/lib/rites/rite_ef/precedence_ef.mli @@ -65,8 +65,8 @@ val unclassified : int (** [band ctx c]: RG 91's Table of Precedence. Returns the table's own entry number -- I class 1-13, II class 14-21, III class 22-26, IV class 27-28; lower wins (see {!Precedence.rules.band}) -- EXCEPT where the table's own - text states an exception: entry 8 (All Souls, register line 334) reads - "yields to an occurring Sunday", so on a Sunday this returns a value that + text states an exception: entry 8 (All Souls) reads "yields to an + occurring Sunday", so on a Sunday this returns a value that loses to entry 15 rather than the literal integer 8 (see the comment on entry 8 in precedence_ef.ml for the exact value and why). Total over every candidate {!Precedence.resolve} or {!Calendar} can construct, @@ -82,39 +82,62 @@ val band : Vocab_ef.season Precedence.context -> Vocab_ef.rank Precedence.candid somewhere to be caught other than a silently-wrong RG 33 disposition. *) val sunday_marker : string -(** [disposition ~winner ~loser]: RG 92-95, 33, 94 (docs/research/ - rules-register.md §4, "Occurrence" and "Vigils"). What becomes of a - losing candidate, decided by the LOSER's own rank and status (RG 95), - except RG 33's vigil omission, which also reads the winner: +(** [disposition ~winner ~loser]: RG 92-95, 33, 21-27, 94 (docs/research/ + rules-register.md §4, "Occurrence", "Vigils" and "Caput IV, 'De + feriis'"). What becomes of a losing candidate, decided by the LOSER's + own rank and status (RG 95), except RG 33's vigil omission, which also + reads the winner: - a {!Celebration.status} of [Commemoration_only] is always [Commemorate] (checked first: it can never win -- see {!Precedence.resolve} -- and, by that same status's own definition, already denotes an office with nothing left to translate, so it never transfers either; not itself a further RG citation beyond RG 93's general four-mechanism statement above); - - a [Class1] or [Class2] loser whose slug marks it a vigil ({!vigil_suffix}) - is [Omit] when the winner is any Sunday ({!sunday_marker}) or itself - [Class1] (RG 33 -- entirely omitted, not merely commemorated); + - a [Class2] or [Class3] loser whose slug marks it a vigil + ({!vigil_suffix} OR {!vigil_prefix} -- both conventions this + codebase's data uses, see {!vigil_prefix}'s own comment) is [Omit] + when the winner is any Sunday ({!sunday_marker}) or itself [Class1] + (RG 33 -- entirely omitted, not merely commemorated). A [Class1] + vigil (Nativity, Pentecost) is outside RG 33 entirely -- RG 30 makes + it preferred to any feast whatsoever, so a real one can never reach + this function as a [loser] in the first place (see the .ml's own + comment on [is_omissible_vigil] for the full argument); - any other [Class1] loser that is NOT a Sunday ({!sunday_marker}) is - [Transfer] (RG 95, register lines 323, 363 -- only I-class FEASTS have - the right of translation; RG 91's own table lists Sundays as a - separate row, entry 6, from feasts, entries 11-13, so a Sunday is - never a "feast" in RG 95's sense and does not transfer even when - impeded by a higher I-class day. This is also what moves All Souls, - register line 334, once it loses to an occurring Sunday -- WHERE it - lands is {!Rite.t.transfer_target}'s job, not this function's); - - everything else -- including an impeded I-class Sunday -- is - [Commemorate], carrying its real RG 109 privilege (see {!admit} - below); RG 109(a) (register line 374) lists "of a Sunday" as a - privileged commemoration category precisely because an impeded Sunday - stays put rather than moving to another day. + [Transfer] (RG 95 -- only I-class FEASTS have the right of + translation; RG 91's own table lists Sundays as a separate row, entry + 6, from feasts, entries 11-13, so a Sunday is never a "feast" in RG + 95's sense and does not transfer even when impeded by a higher + I-class day. This is also what moves All Souls, RG 91 entry 8, once + it loses to an occurring Sunday -- WHERE it lands is + {!Rite.t.transfer_target}'s job, not this function's); + - a TEMPORAL-origin, non-vigil loser of [Class4] is [Omit] (RG 26, + "Caput IV, De feriis" -- "every feria not named in [RG 23-25] is IV + class ... and IV-class ferias are NEVER commemorated." A SEPARATE + rule from RG 109's honour-class one immediately below, keyed on + ferial CLASS rather than on RG 109's privilege letters: RG 109 sorts + commemorations that already exist into honour classes (RG 108's + differing liturgical hours), it does not itself decide which offices + have the right to be commemorated at all -- that is Caput IV's own + business. A SANCTORAL loser of the same rank is unaffected by this + branch (the [is_temporal] guard): RG 21 defines "feria" as any + weekday, never a saint's day, and RG 111(c)/(d) admit an "ordinary" + commemoration of a losing SAINT freely, with no such class-keyed + gate); + - everything else -- including an impeded I-class Sunday, and a + SANCTORAL loser of any rank below I class -- is [Commemorate], + carrying its real RG 109 privilege (see {!admit} below); RG 109(a) + lists "of a Sunday" as a privileged commemoration category precisely + because an impeded Sunday stays put rather than moving to another + day, and RG 24/25 make a losing II- or III-class FERIA's own + commemoration mandatory when impeded, not merely eligible. Total over every winner/loser pair {!Precedence.resolve} or {!Calendar} can construct: [Vocab_ef.rank] (RG 8) and {!Celebration.status} are both - closed variants, so the cases above exhaust every representable shape -- - there is no fifth, "unclassified" case the way {!band} needs one, - because this function's own return type has no such slot to fall into - by accident. *) + closed variants, and the five cases above -- an if/else-if chain ending + in the unconditional [Commemorate] catch-all -- exhaust every value + those two fields can take between them; there is no fifth, + "unclassified" case the way {!band} needs one, because this function's + own return type has no such slot to fall into by accident. *) val disposition : winner:Vocab_ef.rank Precedence.candidate -> loser:Vocab_ef.rank Precedence.candidate -> @@ -130,26 +153,37 @@ val disposition : val nativity_octave_prefix : string (** The September set of {!ember_prefixes}, broken out on its own because RG - 109(d) privileges September Ember days specifically while leaving the - Advent and Lent sets (also {!ember_prefixes}) ordinary -- register lines - 375-376. {!ember_prefixes} is built from this constant, not a duplicated - literal, so the two cannot silently drift apart. *) + 109(d) (§4, "Commemorations") privileges September Ember days under its + own name, and September sits outside RG 109(e)'s three named seasons + (Advent, Lent, Passiontide) under any reading of that clause -- NOT + because the Advent and Lent Ember sets need excluding from (e), which + they do not: (e)'s own bare text privileges them too, the same as any + other Advent/Lent feria (see {!Precedence_ef.privilege_of}'s own (e) + comment in the .ml for the full argument, corrected fix round 1). + {!ember_prefixes} is built from this constant, not a duplicated literal, + so the two cannot silently drift apart. *) val september_ember_prefix : string (** [admit ~observed comms]: RG 108-111 (docs/research/rules-register.md §4, - "Commemorations", register lines 371-379). How many of [comms] -- each - already tagged with its real RG 109 privilege by {!disposition} -- RG - 111 admits, and which, given the day actually observed: + "Commemorations"). How many of [comms] -- each already tagged with its + real RG 109 privilege by {!disposition} -- RG 111 admits, and which, + given the day actually observed: - [observed] a [Class1] day: none, except at most one privileged commemoration (the highest-dignity one, if several are due) -- an ordinary one is never admitted here, no matter how many are due; - - [observed] a [Class2] Sunday (its slug carries {!sunday_marker}): one - -- a privileged commemoration takes the day's one slot over any - ordinary one whenever one is due, not by comparing dignity, so an - ordinary commemoration that would otherwise win on dignity is still - dropped; + - [observed] a [Class2] Sunday (its slug carries {!sunday_marker}): one, + subject to TWO conditions, not one -- (i) a privileged commemoration, + whenever due, categorically takes the day's one slot over any + ordinary one, not by comparing dignity, so an ordinary commemoration + that would otherwise win on dignity is still dropped; (ii) failing + that, the slot is reserved for a [Class2] candidate SPECIFICALLY + ("de festo II classis", RG 111(b)'s own wording -- a RANK FLOOR, not + "whichever ordinary candidate has the best dignity"): a III- or + IV-class ordinary loser has no standing for this slot at all and is + admitted nothing, even when it is the only candidate due; - [observed] any other [Class2] day: one, by dignity alone -- no - privilege override, unlike the Sunday case immediately above; + privilege override and no rank floor, unlike the Sunday case + immediately above; - [observed] a [Class3] or [Class4] day: at most two, by dignity alone. "Dignity" here is [Vocab_ef.rank] (RG 8's four classes), NOT {!band}'s -- cgit v1.3