diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/kernel/validate.ml | 33 | ||||
| -rw-r--r-- | lib/kernel/validate.mli | 26 | ||||
| -rw-r--r-- | lib/rites/rite_ef/precedence_ef.ml | 86 | ||||
| -rw-r--r-- | lib/rites/rite_ef/precedence_ef.mli | 44 |
4 files changed, 159 insertions, 30 deletions
diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index 433dc99..24adcd8 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -330,12 +330,41 @@ let run (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) ~year = season = d.Liturgical_day.temporal.Temporal.season; weekday = d.Liturgical_day.temporal.Temporal.weekday } in + (* CORRECTED (Task B fix round 1, coordinator finding 5): [origin] + used to be reconstructed as [Sanctoral] UNCONDITIONALLY, which + was harmless while nothing here called [band] on the result + (the comment this replaces was correct about [PE.admit] itself: + it never reads [origin]) -- but this function ALSO now calls + [rite.rules.Precedence.band day_ctx cand] on every one of these + reconstructed candidates (the line just below), and [band] DOES + read [origin] (its own [is_temporal] test) to choose between its + temporal- and sanctoral-keyed branches. A genuinely + TEMPORAL-origin commemoration (a privileged Advent/Lent/ + Passiontide feria, an Ember day, an impeded Sunday) mislabelled + [Sanctoral] would score the WRONG band entry (e.g. a Lent feria + scoring entry 23, "III-class feasts in particular calendars", + instead of its real entry 22) -- inert today only because + nothing currently asserts on the SCORE [band] returns here, only + on whether re-offering [admit] the same values round-trips + (which happens not to depend on getting [origin] right for any + case this codebase's data reaches -- unverified in general). + [Liturgical_day.t] itself still does not retain a + commemoration's original origin, so it is recovered the only + way available: a commemoration whose SLUG matches the day's own + temporal office is temporal-origin; every other commemoration + is sanctoral-origin. This is exact whenever slugs cannot + collide across the two streams (Task 12's own "observed" check + already assumes this for a different purpose), which is the + same assumption the rest of this codebase already leans on. *) + let temporal_office_slug = d.Liturgical_day.temporal.Temporal.office.Celebration.slug in let as_candidates comms = List.map (fun (c, p) -> - let cand : 'r Precedence.candidate = - { Precedence.cel = c; origin = Precedence.Sanctoral } + let origin = + if Slug.equal c.Celebration.slug temporal_office_slug then Precedence.Temporal + else Precedence.Sanctoral in + let cand : 'r Precedence.candidate = { Precedence.cel = c; origin } in (cand, p, rite.Rite.rules.Precedence.band day_ctx cand)) comms in diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli index 5e55fc5..b46ca30 100644 --- a/lib/kernel/validate.mli +++ b/lib/kernel/validate.mli @@ -59,14 +59,24 @@ val failure_to_string : failure -> string fixed point. - ["admission"]: the rite's own [rules.admit] is a fixed point on what it already admitted -- re-offering a day's [commemorations] back to - [admit] (reconstructed with {!Precedence.Sanctoral} origin; the real EF - admit reads only rank and slug, never origin, so this reconstruction is - exact for it) must return exactly that same set. A cap-enforcing - selector that is not idempotent on its own output has, by definition, - admitted something its own rule would not admit if asked again -- the - rite-agnostic form of "the admission limit was not exceeded" available - without embedding a rite's specific numeric caps (RG 111's, for EF) - into kernel code. + [admit] (with [observed]'s own origin reconstructed as + {!Precedence.Sanctoral}; the real EF admit reads only rank and slug + from [observed], never origin, so this reconstruction is exact for + it) must return exactly that same set. Each offered commemoration's + own origin -- CORRECTED, Task B fix round 1 -- is recovered by + comparing its slug against the day's own temporal office, not + reconstructed as [Sanctoral] uniformly: {!Precedence.rules.admit} + (since Task B) is handed each candidate's own {!Precedence.rules.band} + value, computed here exactly as {!Precedence.resolve} computes it, and + [band] DOES read a candidate's origin (temporal- vs sanctoral-keyed + branches) even though EF's own [admit] itself still does not -- a + mislabelled origin would silently score the wrong table entry for a + genuinely temporal-origin commemoration (e.g. a Lent feria) before + this fix. A cap-enforcing selector that is not idempotent on its own + output has, by definition, admitted something its own rule would not + admit if asked again -- the rite-agnostic form of "the admission limit + was not exceeded" available without embedding a rite's specific + numeric caps (RG 111's, for EF) into kernel code. Total over the whole 1583..9999 domain, including [year] = 9999: the liturgical year opening there continues into out-of-domain civil year diff --git a/lib/rites/rite_ef/precedence_ef.ml b/lib/rites/rite_ef/precedence_ef.ml index 861bb1a..8452e69 100644 --- a/lib/rites/rite_ef/precedence_ef.ml +++ b/lib/rites/rite_ef/precedence_ef.ml @@ -110,6 +110,7 @@ let band (ctx : Vocab_ef.season Precedence.context) (c : Vocab_ef.rank Precedenc int = let cel = c.Precedence.cel in let rank = cel.Celebration.rank in + let status = cel.Celebration.status in let subject = cel.Celebration.subject in let layer = cel.Celebration.layer in let slug = Slug.to_string cel.Celebration.slug in @@ -129,8 +130,41 @@ let band (ctx : Vocab_ef.season Precedence.context) (c : Vocab_ef.rank Precedenc binding, not a second literal, so the two can never drift apart. *) let entry_15_band = 15 in let open Vocab_ef in - (* 1: Nativity, Easter Sunday, Pentecost Sunday (I class w/ octave). *) - if is_temporal && rank = Class1 && ((m = 12 && d = 25) || off = 0 || off = 49) then 1 + (* CORRECTED (Task B fix round 1, ef-rg16a): a [Commemoration_only] + celebration has NO row in RG 91's table at all, checked FIRST, ahead of + every rank-keyed branch below -- RG 91's own text enumerates only "dies + liturgici" (entry 24's own wording, e.g., "Festa III classis, in + calendario Ecclesiae universae inscripta" -- FEASTS, inscribed in the + calendar), and the calendarium itself marks the difference in its own + notation: 22 September's row reads "S. Thomae de Villanova Ep. et + Conf., III classis. / Commemoratio Ss. Mauritii et Soc. Mm." -- Thomas + gets a class number (a "festum"); Maurice gets "Commemoratio" and NO + class number at all, because he never had a row in the table for that + occasion to begin with. Before this fix, [band] read [rank] alone, so + a [Commemoration_only] entry silently borrowed the SAME entry number + as a genuine [Feast] of its own rank (a Class3 Commemoration_only + entry banded to 24, indistinguishable from a real Class3 universal + feast) -- manufacturing a "tie" at {!compare_precedence}/RG 113's own + admission ordering that the primary text never creates: RG 113 does + not run out of instruction between two same-rank commemorations; + [band] ran out of fidelity, handing out a table row that does not + exist for one of them. [unclassified] (worse than every real entry) is + the same value already used for a candidate this table's 28 branches + otherwise fail to describe, which is exactly the right answer here + too: "not in this table" for a different reason, same table-position + consequence. Confirmed by the oracle: missalemeum's own commemoration + id embeds a rank that AGREES with the demoted status this represents + (e.g. sancti:09-22o:4:r for Maurice, rank 4, against Thomas's own + sancti:09-22:3:w, rank 3, on the day Thomas is observed -- test_oracle + .ml's own [test_identity_rank_corroboration]). Restricted to [status]; + [rank] itself is untouched, since {!Celebration.status}'s own doc + comment is explicit that a demoted feast "retains a rank" for RG 111's + admission-COUNT purposes (I/II/III/IV class thresholds), which this + guard does not touch -- only ORDERING among candidates already offered + to {!admit} changes. *) + if status = Celebration.Commemoration_only then unclassified + (* 1: Nativity, Easter Sunday, Pentecost Sunday (I class w/ octave). *) + else if is_temporal && rank = Class1 && ((m = 12 && d = 25) || off = 0 || off = 49) then 1 (* 2: Sacred Triduum (Thu-Sat of Holy Week). *) else if is_temporal && rank = Class1 && off >= -3 && off <= -1 then 2 (* 3: Epiphany, Ascension, Holy Trinity, Corpus Christi, Sacred Heart, @@ -769,16 +803,44 @@ let disposition ~(winner : Vocab_ef.rank Precedence.candidate) This REPLACES a previous [compare_dignity], which sorted by RG 8's coarse four-class [rank] ("dignity") and broke same-rank ties alphabetically by - slug -- an engineering convention with no rubrical warrant, silently - deciding 66 days over 2005-2050 (e.g. 22 Sept 2027, an Ember Wednesday: - the alphabetical rule admitted "maurice-and-companions-martyrs" over - "thomas-of-villanova", both Class3/{!band} entry 24 -- missalemeum shows - Thomas). {!band} needs a [context] this function itself does not have - (date/season/weekday) -- unlike [dignity], which read [rank] alone -- - so {!Precedence.resolve} now computes each candidate's own [band] value - once, generically, and hands it to [admit] as the trailing [int] on each - input triple (see {!Precedence.rules.admit}'s own doc). [comms] below is - [(candidate * privilege * int) list], not the pair it used to be. *) + slug -- an engineering convention with no rubrical warrant. Measured, + fix round 1 (2005-2050, a temporary pre-fix [git worktree]): a + same-[rank] tie existed on 599 days, most never reaching a real + decision; reversing the slug tie-break alone changed the ADMITTED SET on + 65 of them and the printed ORDER of an already-admitted pair on a + further 149 (docs/research/rules-register.md §6.1's full account, + correcting this comment's own earlier, unreproduced "66 days" claim). + + CORRECTED, fix round 1 (coordinator finding 1): checking every one of + those 65+149 real decisions against data/ef/sanctoral.sexp found the + SAME underlying shape in all of them, no exceptions -- one candidate is + always [Cel.Commemoration_only] (e.g. "maurice-and-companions-martyrs", + 22 September) and the other always a genuine [Cel.Feast] or a temporal + office of the SAME [rank] (e.g. "thomas-of-villanova", same day; or a + Lent feria, {!band} entry 22, against "paul", 22 February). That is + {!band}'s OWN fidelity bug, fixed separately at its source (see [band]'s + own top-of-branch guard, RG 91's table has no row for a bare + commemoration at all) -- NOT a case RG 113's table-order alone resolves, + since a [Commemoration_only] candidate never had a real table entry to + compare in the first place. With that fixed, none of these 599 days' + real decisions any longer depend on THIS function's own slug fallback: + {!band} alone (a real entry vs {!unclassified}) already decides every + one. What remains genuinely open -- two DIFFERENT candidates landing on + the IDENTICAL real table entry, e.g. two different Class3 universal + feasts both at entry 24 -- was checked and found EMPTY across + 2005-2050 (register §6.1): RG 113's own table-order, once {!band} is + accurate, already decides every real case this codebase's current data + produces; the slug fallback below is exercised only between two + [Commemoration_only] candidates tied at {!unclassified} (138 of the 599, + all order/count-invisible -- RG 91 has no table position for either of + them to compare, so there is nothing more specific RG 113 could supply + here either). {!band} needs a [context] this function itself does not + have (date/season/weekday) -- unlike [dignity], which read [rank] alone + -- so {!Precedence.resolve} now computes each candidate's own [band] + value once, generically, and hands it to [admit] as the trailing [int] + on each input triple (see {!Precedence.rules.admit}'s own doc). [comms] + below is [(candidate * privilege * int) list], not the pair it used to + be. *) let compare_precedence (a, _, ba) (b, _, bb) = if ba <> bb then Int.compare (ba : int) bb else Slug.compare a.Precedence.cel.Celebration.slug b.Precedence.cel.Celebration.slug diff --git a/lib/rites/rite_ef/precedence_ef.mli b/lib/rites/rite_ef/precedence_ef.mli index 49195f9..b283a17 100644 --- a/lib/rites/rite_ef/precedence_ef.mli +++ b/lib/rites/rite_ef/precedence_ef.mli @@ -68,10 +68,21 @@ val unclassified : int 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, - including shapes the 1962 table itself does not describe (see - {!unclassified}). *) + entry 8 in precedence_ef.ml for the exact value and why). ALSO + {!unclassified} for any [Cel.Commemoration_only] candidate, checked + first, ahead of every rank-keyed branch -- CORRECTED, Task B fix round + 1 (coordinator finding 1): RG 91's own table enumerates only "dies + liturgici" (entry 24's own text, "Festa III classis..." -- FEASTS), so + a celebration reduced to a bare commemoration was never a row in the + table to begin with, confirmed by the calendarium's own notation (a + genuine feast carries a class number on its occurrence line; a bare + "Commemoratio" carries none). Before this fix, a [Commemoration_only] + candidate silently borrowed the SAME entry number as a genuine [Feast] + of its own [rank] -- manufacturing ties {!Precedence.compare_by} and + {!compare_precedence} both then had to break some other way, that RG 91 + itself never created. Total over every candidate {!Precedence.resolve} + or {!Calendar} can construct, including shapes the 1962 table itself + does not describe (see {!unclassified}). *) val band : Vocab_ef.season Precedence.context -> Vocab_ef.rank Precedence.candidate -> int (** RG 33's marker: every Sunday slug this rite's temporal cycle produces @@ -195,8 +206,16 @@ val september_ember_prefix : string CORRECTED, Task B (branch ef-rg16a): this used to sort by [Vocab_ef.rank] (RG 8's coarse four-class "dignity") and break same-rank ties alphabetically by slug -- an engineering convention with no - rubrical warrant, cited nowhere, silently deciding 66 days over - 2005-2050. RG 113's own second sentence, previously uncited + rubrical warrant, cited nowhere. Measured, fix round 1 (2005-2050, + reproducible via a temporary [git worktree] at the pre-fix commit): + a same-[rank] tie existed in the candidate pool offered to [admit] on + 599 days, most never reaching a real decision (RG 111's own admission + count often has room for both, e.g. a III-class day admits two); of + those, reversing the slug tie-break ALONE actually changed the ADMITTED + SET on 65 days and only the printed ORDER of an already-admitted pair + on a further 149 (docs/research/rules-register.md §6.1's own full + account, superseding this comment's earlier, unreproduced "66 days" + claim). RG 113's own second sentence, previously uncited (docs/research/rules-register.md §4's RG 113 entry), is the real rule: *"in admittendis et ordinandis aliis commemorationibus, servetur ordo tabellae praecedentiae"* -- admitting and ordering commemorations both @@ -205,8 +224,17 @@ val september_ember_prefix : string receive on its own, so {!Precedence.resolve} computes it once, generically, and hands each candidate its own value as the trailing [int] on [comms]'s triples (see {!Precedence.rules.admit}). Ties break - on slug ONLY within one identical [band] value (RG 113 gives no further - instruction there; still an uncited engineering convention, register §6 + on slug ONLY within one identical [band] value -- CORRECTED, fix round + 1 (coordinator finding 1): [band] itself used to hand a + [Cel.Commemoration_only] candidate the same table entry as a genuine + [Cel.Feast] of its own rank (RG 91's table has no row for a bare + commemoration at all), manufacturing most of the "identical [band] + value" ties this comment used to describe as RG 113's own residual. + Fixed in [band] itself; checked afterward (2005-2050 and the full + 1583-9999 domain, register §6.1) and found EMPTY of any remaining + "two different real table entries tied" case -- the slug fallback below + is exercised only between two [Commemoration_only] candidates both at + {!unclassified}, still an uncited engineering convention (register §6 "RG 113 tie-break"), matching {!Precedence.compare_by}'s own fallback, so the result never depends on the order [comms] arrives in. |