hacspec / hax

A Rust verification tool

https://hacspec.org/blog

Apache License 2.0

179 stars 19 forks source link

Pull `solve_item_traits` out of mir_traits #637

Open W95Psp opened 5 months ago

W95Psp commented 5 months ago

627 introduces a use of `mir_traits::solve_item_traits` in the extraction of types, which are common to THIR and MIR. Thus `solve_item_traits` should move out of `mir_traits.rs`.

solve_item_traits should anyway be re-written using the traits rustc_utils::SubstBinder and rustc_utils::PredicateToPolyTraitRef.

github-actions[bot] commented 1 month ago

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

W95Psp commented 1 month ago

It's still to be done (https://github.com/hacspec/hax/blob/16db1cc4571cbe1d4818945224f2cd693bb1b32c/frontend/exporter/src/types/mir_traits.rs#L47)

hacspec / hax

Pull `solve_item_traits` out of mir_traits #637

627 introduces a use of mir_traits::solve_item_traits in the extraction of types, which are common to THIR and MIR. Thus solve_item_traits should move out of mir_traits.rs.

627 introduces a use of `mir_traits::solve_item_traits` in the extraction of types, which are common to THIR and MIR. Thus `solve_item_traits` should move out of `mir_traits.rs`.