Register enum defs reachable through ADT fields

[coord-e]

Fixes #221.

Enum registration

basic_block::Analyzer::register_enum_defs discovered the enums a body needs by running a TypeVisitor over the types of its local declarations, and super_visit_with on an Adt descends into that ADT's generic arguments only. An enum occurring solely as the field type of another ADT — struct Wrap { o: Option<i32> }, or enum Outer { X(Inner), Y } — was therefore never registered, while the elaboration of the outer ADT does reach it, so the EnumDefProvider lookup unwrapped a None.

EnumDefCollector (in refine::template, next to the TypeBuilder it mirrors) replaces the inline visitor. It follows the structure TypeBuilder::build follows: an ADT that is not translated as a model type is elaborated into its fields — a struct into the tuple of its fields, an enum into the fields of its variants — so the enums those fields mention are needed as well. Model types keep their fields unvisited, since they are translated directly, and an elaborated_adts set keeps recursive ADTs from looping.

Undeclared sort

Registering Option was not enough to make the by-value reproduction verify: the enum reached chc::System::datatypes, but the emitted SMT-LIB2 still referred to std.option.Option<Int> without declaring it.

FormatContext::from_system monomorphizes a polymorphic datatype only for datatype sorts collected from the clauses, and Option<Int> occurs nowhere in them — the locals have the sort of the tuple Wrap elaborates to, and Option<Int> appears only as that tuple's selector. Sort collection now runs to a fixpoint over the selectors of the datatypes being declared, so a sort reachable only through another datatype's field gets monomorphized and declared too.

Checking

Every program in the issue — both by-value reproductions, the by-reference one, the nested-pattern program, and the two controls — now reports safe. Both directions of the check still hold: with struct Wrap { o: Option<i32> }, a body asserting the wrong value of the field reports Unsat while the correct one passes.

cargo test (316 ui tests, unit and doc tests), cargo clippy -- -D warnings, and cargo fmt --check all pass. No test case is added, per the request.

---

Generated by Claude Code