Module traits

Re-exports

pub use utils::ToPolyTraitRef;

pub use utils::erase_and_norm;

pub use utils::implied_predicates;

pub use utils::is_sized_related_trait;

pub use utils::predicates_defined_on;

pub use utils::required_predicates;

pub use utils::self_predicate;

pub use resolution::PredicateSearcher;

Modules

resolution 🔒

Trait resolution: given a trait reference, we track which local clause caused it to be true. This module is independent from the rest of hax, in particular it doesn’t use its state-tracking machinery.

utils 🔒

Each item can involve three kinds of predicates:

Structs

ImplExpr

An ImplExpr describes the full data of a trait implementation. Because of generics, this may need to combine several concrete trait implementation items. For example, ((1u8, 2u8), "hello").clone() combines the generic implementation of Clone for (A, B) with the concrete implementations for u8 and &str, represented as a tree.

Enums

DropData

ImplExprAtom

The source of a particular trait implementation. Most often this is either Concrete for a concrete impl Trait for Type {} item, or LocalBound for a context-bound where T: Trait.

ImplExprPathChunk

Functions

self_clause_for_item

Retrieve the Self: Trait clause for a trait associated item.

solve_item_implied_traits

Solve the trait obligations for implementing a trait (or for trait associated type bounds) in the current context.

solve_item_required_traits

Solve the trait obligations for a specific item use (for example, a method call, an ADT, etc.) in the current context. Just like generic args include generics of parent items, this includes impl exprs for parent items.

solve_item_traits_inner 🔒

Apply the given generics to the provided clauses and resolve the trait references in the current context.

solve_trait

This is the entrypoint of the solving.

super_clause_to_clause_and_impl_expr

Given a clause clause in the context of some impl block impl_did, susbts correctly Self from clause and (1) derive a Clause and (2) resolve an ImplExpr.

translate_item_ref

Translate a reference to an item, resolving the appropriate trait clauses as needed.