diff options
Diffstat (limited to 'lib/kernel/validate.ml')
| -rw-r--r-- | lib/kernel/validate.ml | 194 |
1 files changed, 178 insertions, 16 deletions
diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index 7be3425..cc8bdce 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -20,7 +20,35 @@ let has_duplicate strings = let rec go = function a :: (b :: _ as rest) -> a = b || go rest | _ -> false in go sorted -let run vocab ~year_start ~temporal ~anchors ~year = +(* Like [has_duplicate], but names the offender(s) instead of only reporting + that one exists -- the ["slugs"] check below wants a useful failure + detail, not just a bool. *) +let duplicates strings = + let sorted = List.sort String.compare strings in + let rec go acc = function + | a :: (b :: _ as rest) -> go (if a = b then a :: acc else acc) rest + | _ -> acc + in + List.sort_uniq String.compare (go [] sorted) + +(* Task 12's "unconverged" check has no structural signal to key off -- + Calendar's placement pass records its round-guard reason as a plain + string in [Liturgical_day.omitted] (calendar.ml's own [unconverged_reason], + not exposed as a public constant), and [Liturgical_day.omitted]'s own doc + comment says exactly this check is meant to read it. A short, distinctive + substring rather than the full literal keeps the coupling to calendar.ml's + exact wording as loose as it can be while still being unambiguous: nothing + else this kernel emits into [omitted] talks about "converging". *) +let contains_substring s ~needle = + let ls = String.length s and ln = String.length needle in + let rec at i = i + ln <= ls && (String.sub s i ln = needle || at (i + 1)) in + ln = 0 || at 0 + +let run (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) ~year = + let vocab = rite.Rite.vocab in + let year_start = rite.Rite.year_start in + let temporal = rite.Rite.temporal in + let anchors = rite.Rite.anchors in let start = year_start year in let stop = (* [year_start (year + 1)] needs a date in civil year (year+1); at @@ -68,18 +96,16 @@ let run vocab ~year_start ~temporal ~anchors ~year = (* Weekday agreement. *) if t.Temporal.weekday <> Date.weekday date then fail date "weekday" "temporal weekday disagrees with Date.weekday"; - (* Slug: three properties, none checked here, all delivered - elsewhere. Well-formedness needs no check: [Slug.t] is a private - string validated on every construction path ([of_string], - [of_string_exn], [t_of_sexp]), and [to_string] is the identity, - so round-tripping an existing [Slug.t] can never fail -- a check - here would be structurally incapable of firing, which is worse - than no check, since it would look like coverage that isn't - there. Uniqueness *per date* needs no check either: [temporal] - returns exactly one office by construction. Uniqueness *across - the year* is deliberately NOT asserted -- a resumed Sunday - reuses an earlier Epiphany key on purpose, so the check would be - false. *) + (* Slug: three properties. Well-formedness needs no check: [Slug.t] + is a private string validated on every construction path + ([of_string], [of_string_exn], [t_of_sexp]), and [to_string] is + the identity, so round-tripping an existing [Slug.t] can never + fail -- a check here would be structurally incapable of firing, + which is worse than no check, since it would look like coverage + that isn't there. Uniqueness *per date* needs no check either: + [temporal] returns exactly one office by construction. + Uniqueness *across the year* IS asserted, below, once the whole + walk is in hand -- see the ["slugs"] check after this loop. *) (* Vocabulary closure. *) if not (List.exists (fun r -> vocab.Vocab.rank_to_string r = vocab.Vocab.rank_to_string cel.Celebration.rank) @@ -97,9 +123,28 @@ let run vocab ~year_start ~temporal ~anchors ~year = | None -> fail date "determinism" "a second call to temporal raised where the first succeeded")) days; let observed = List.rev !observed in + (* Slug uniqueness across the year (Plan 2 carried item 4): moved into + [Validate] itself so every consumer gets it, not only a 200-sample + QCheck property scoped to one rite. Asserted OUTRIGHT, no exemption: + Plan 2 verified zero duplicate slugs domain-wide, across all 8 416 + years, for the EF rite's own resumed-Sunday mechanism -- the exemption + the test property used to carry protected nothing real, because a + resumed Sunday only ever backfills a week number Septuagesima cut short + that same liturgical year (so it was never actually used that year to + begin with), never repeats one the year's own January Sundays already + used. If a future rite genuinely needs an exemption, it can supply one + then -- not speculatively here. *) + (match duplicates (List.map (fun (_, t) -> Slug.to_string t.Temporal.office.Celebration.slug) observed) with + | [] -> () + | dups -> + fail start "slugs" + (Printf.sprintf "slug(s) sighted on more than one date this year: %s" (String.concat ", " dups))); (* Season contiguity and completeness: the run-length-compressed sequence must - equal vocab.seasons exactly -- all seasons, each in one unbroken run, in - canonical order. No EF season can be empty in any year. *) + equal the rite's own [season_runs] exactly, in canonical order. This is + NOT necessarily [vocab.seasons] -- most rites have each season in one + unbroken run, but a rite may legitimately have one season appear in two + separate runs (the modern form's Ordinary Time does), so the expected + sequence is rite-supplied rather than derived from the vocabulary. *) let compressed = List.fold_left (fun acc (_, t) -> @@ -108,7 +153,7 @@ let run vocab ~year_start ~temporal ~anchors ~year = [] observed |> List.rev in - let expected = List.map vocab.Vocab.season_to_string vocab.Vocab.seasons in + let expected = List.map vocab.Vocab.season_to_string rite.Rite.season_runs in if compressed <> expected then fail start "seasons" (Printf.sprintf "season runs %s; expected %s" @@ -157,4 +202,121 @@ let run vocab ~year_start ~temporal ~anchors ~year = if actual <> expected_slug then fail date "anchor" (Printf.sprintf "expected slug %S, got %S" expected_slug actual)) anchor_pairs; + (* Resolution invariants (Task 12): everything above only ever asked + [rite.temporal] for a date's office in isolation. From here on the + LITURGICAL YEAR IS ACTUALLY RESOLVED against [layer] -- occurrence, + transfer placement, commemorations, the works (spec ยง2.4) -- and the + result checked for five further properties a temporal-only pass cannot + see at all. [days] (the walk built above) is reused rather than + recomputed: it names exactly the same [start, stop] span + {!Calendar.year} resolves for this [year]. *) + (match Calendar.year rite layer year with + | exception exn -> + (* The kernel contract forbids [run] itself from ever raising on + in-range input, and an exception escaping resolution is the most + total form of "silently lost" there is: nothing about this year's + sanctoral entries could be verified as accounted for at all. *) + fail start "lost" + (Printf.sprintf "resolving the year raised (%s); nothing could be verified as accounted for" + (Printexc.to_string exn)) + | resolved -> + let idx = Layer.index_by_date layer in + let bump tbl slug = Hashtbl.replace tbl slug (1 + (try Hashtbl.find tbl slug with Not_found -> 0)) in + (* Expected: how many times each layer entry's own Date_spec resolves + within [start, stop]. Walking dates and querying [Layer.on_date] + (rather than resolving each entry's Date_spec against candidate + civil years directly) is what naturally counts a fixed late- + November date TWICE in the ~20% of liturgical years whose 371-day + span reaches it on both ends -- see validate.mli's own note on 30 + November / St Andrew. *) + let expected : (string, int) Hashtbl.t = Hashtbl.create 64 in + List.iter + (fun date -> + Layer.on_date idx ~month:(Date.month date) ~day:(Date.day date) + |> List.iter (fun (e : 'r Layer.entry) -> + bump expected (Slug.to_string e.Layer.cel.Celebration.slug))) + days; + (* Actual: how many times each slug is actually sighted across the + resolved year. Deliberately [observed] + [commemorations] + + [omitted] only, NOT [transferred_out]: a successfully transferred + celebration is already counted once, via [observed] (+ + [transferred_in]) on the day it lands; also counting + [transferred_out] at the day it left would double-book every clean + transfer, which is exactly what this check exists to catch, not + cause. *) + let actual : (string, int) Hashtbl.t = Hashtbl.create 64 in + let bump_cel tbl (c : 'r Celebration.t) = bump tbl (Slug.to_string c.Celebration.slug) in + Array.iter + (fun (d : ('s, 'r) Liturgical_day.t) -> + bump_cel actual d.Liturgical_day.observed; + List.iter (fun (c, _) -> bump_cel actual c) d.Liturgical_day.commemorations; + List.iter (fun (c, _) -> bump_cel actual c) d.Liturgical_day.omitted) + resolved; + Hashtbl.fold (fun slug exp acc -> (slug, exp) :: acc) expected [] + |> List.sort compare (* stable failure order: Hashtbl.iter's own order is hash-seed-dependent *) + |> List.iter (fun (slug, exp) -> + let act = try Hashtbl.find actual slug with Not_found -> 0 in + if act < exp then + fail start "lost" + (Printf.sprintf "%s: sighted %d time(s) this year, but its own Date_spec resolves %d" + slug act exp) + else if act > exp then + fail start "duplicated" + (Printf.sprintf "%s: sighted %d time(s) this year, but its own Date_spec resolves only %d" + slug act exp)); + Array.iter + (fun (d : ('s, 'r) Liturgical_day.t) -> + let date = d.Liturgical_day.date in + let observed_slug = Slug.to_string d.Liturgical_day.observed.Celebration.slug in + let has_slug (c, _) = Slug.to_string c.Celebration.slug = observed_slug in + (* "observed": the day's own winner must not ALSO be listed as one + of its own losers -- see validate.mli's own note on why this is + reachable (two distinct layer entries sharing a slug, one + transferred onto the other's natural date, the transferred one + winning) despite {!Precedence.resolve}'s fold never letting the + SAME candidate value appear as both winner and loser. *) + if List.exists has_slug d.Liturgical_day.commemorations + || List.exists has_slug d.Liturgical_day.omitted + then + fail date "observed" + (Printf.sprintf + "%s is this day's observed celebration and also appears among its own \ + commemorations/omissions" + observed_slug); + (* "unconverged": see [contains_substring]'s own comment above. *) + if + List.exists + (fun (_, reason) -> contains_substring reason ~needle:"did not converge") + d.Liturgical_day.omitted + then + fail date "unconverged" + "transfer placement did not reach a fixed point within the round guard (RG 96-98)"; + (* "admission": re-offer this day's own admitted commemorations + back to [rite.rules.admit] and require the exact same set back. + [origin] is reconstructed as [Sanctoral] uniformly: + {!Liturgical_day.t} does not retain a commemoration's original + origin, and the real EF [admit] (precedence_ef.ml) reads only + rank and slug from a candidate, never [origin], so this + reconstruction is exact for it; documented in validate.mli as + the one place a rite whose [admit] DOES consult [origin] could + see a false negative from this check. *) + let observed_candidate : 'r Precedence.candidate = + { Precedence.cel = d.Liturgical_day.observed; origin = Precedence.Sanctoral } + in + let as_candidates comms = + List.map (fun (c, p) -> ({ Precedence.cel = c; origin = Precedence.Sanctoral }, p)) comms + in + let offered = as_candidates d.Liturgical_day.commemorations in + let readmitted = rite.Rite.rules.Precedence.admit ~observed:observed_candidate offered in + let norm l = + List.map (fun (c, p) -> (Slug.to_string c.Precedence.cel.Celebration.slug, p)) l + |> List.sort compare + in + if norm readmitted <> norm offered then + fail date "admission" + (Printf.sprintf + "admit is not a fixed point on this day's own commemorations: re-offering %d \ + admitted %d back" + (List.length offered) (List.length readmitted))) + resolved); List.rev !failures |