diff options
Diffstat (limited to 'lib/kernel/validate.ml')
| -rw-r--r-- | lib/kernel/validate.ml | 132 |
1 files changed, 131 insertions, 1 deletions
diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index c6501a9..d8de31b 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -20,7 +20,20 @@ let has_duplicate strings = let rec go = function a :: (b :: _ as rest) -> a = b || go rest | _ -> false in go sorted -let run (rite : ('s, 'r) Rite.t) ~year = +(* 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 @@ -164,4 +177,121 @@ let run (rite : ('s, 'r) Rite.t) ~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 |