Register EnumDatatypeDef on-demand

[coord-e]

• To support externally-defined ADTs, register ADTs with the Analyzer on-demand, rather than processing the current crate's initially
  • Env needs to lookup enum_defs. We previously passed the copy of enum_defs when Env is built at the start of BB analysis. However in the current situation Env needs to catch up with the enum_defs changes during BB analysis. So, Env and Analyzer shares Rc<RefCell<EnumDefs>> now.
• Include some minor bug fixes that was found by new test cases

[Copilot]

Pull request overview

This PR refactors enum datatype definition registration from an upfront, crate-wide approach to an on-demand registration strategy. This enables support for externally-defined ADTs by registering enum definitions during basic block analysis when they are first encountered. The key architectural change involves sharing Rc<RefCell<EnumDefs>> between Env and Analyzer to allow dynamic updates during analysis, replacing the previous static copy approach.

• Introduces EnumDefProvider trait to abstract enum definition lookup
• Replaces upfront enum registration in crate analysis with on-demand registration in basic block analysis
• Includes bug fixes in the CHC unboxing pass for proper handling of datatype sorts and matcher predicates
• Adds comprehensive test coverage for Result and Option enum types with both passing and failing cases

Reviewed changes

Copilot reviewed 16 out of 16 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
src/analyze.rs	Adds EnumDefs structure with on-demand get_or_register_enum_def method; refactors to share enum definitions via Rc<RefCell<EnumDefs>>
src/analyze/crate_.rs	Removes upfront register_enum_defs function that processed all enum definitions at crate initialization
src/analyze/basic_block.rs	Adds register_enum_defs to register enums found in local declarations before BB analysis; updates aggregate handling to use on-demand registration
src/refine/env.rs	Introduces EnumDefProvider trait and makes Env generic over it; updates to use trait for enum definition lookups
src/refine.rs	Exports new EnumDefProvider trait
src/chc/unbox.rs	Fixes bugs by adding unbox_datatype_sort call for DatatypeCtor and unbox_pred call for atom predicates
tests/ui/pass/result_struct.rs	Test case verifying Result enum handling with struct fields
tests/ui/pass/result_mut.rs	Test case for mutable Result enum operations
tests/ui/pass/option_mut.rs	Test case for mutable Option enum operations
tests/ui/pass/option_loop.rs	Test case for Option enum in loop contexts
tests/ui/pass/option_inc.rs	Test case for Option enum with increment operations
tests/ui/fail/result_struct.rs	Negative test case expecting failure with incorrect Result assertion
tests/ui/fail/result_mut.rs	Negative test case expecting failure with incorrect mutation assertion
tests/ui/fail/option_mut.rs	Negative test case expecting failure with incorrect Option mutation assertion
tests/ui/fail/option_loop.rs	Negative test case expecting failure with incorrect loop termination assertion
tests/ui/fail/option_inc.rs	Negative test case expecting failure with incorrect increment assertion

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.