Judgment borrow_check_place_expr
judgment_fn! {
/// Borrow-check a place expression, returning its type.
pub fn borrow_check_place_expr(
env: TypeckEnv,
assumptions: Predicates,
state: FlowState,
place: PlaceExpr,
) => (TypedPlaceExpr, FlowState) {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/borrow_check/nll.rs:668
The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.
local| Line | Coverage | Source |
|---|---|---|
| 679 | 2 | (let ty = state.local_variable(&local_id)?) |
| ──────── ("local") | ||
| 681 | 103 | (borrow_check_place_expr(_env, _assumptions, state, PlaceExpr::Var(local_id)) => ( TypedPlaceExpr::new(ty, TypedPlaceExpressionData::local(local_id)), state, )) |
struct field| Line | Coverage | Source |
|---|---|---|
| 688 | ✗ | (borrow_check_place_expr(env, assumptions, state, prefix) => (prefix_typed, state)) |
| 689 | 1 | (prove_ty_is_rigid(env, assumptions, state, &prefix_typed.ty) => (RigidTy { name: RigidName::AdtId(adt_id), parameters }, state)) |
| 690 | ✗ | (let Struct { id: _, binder } = env.crates().struct_named(&adt_id)?) |
| 691 | ✗ | (let StructBoundData { where_clauses, fields } = binder.instantiate_with(¶meters)?) |
| 692 | ✗ | (prove_where_clauses(env, assumptions, state, where_clauses) => state) |
| 693 | ✗ | (field in fields) |
| 694 | 1 | (if field.name == *field_name) |
| ──────── ("struct field") | ||
| 696 | 19 | (borrow_check_place_expr(env, assumptions, state, PlaceExpr::Field { prefix, field_name }) => ( TypedPlaceExpr::new(&field.ty, TypedPlaceExpressionData::field(prefix_typed, field_name, adt_id, VariantId::for_struct())), state, )) |
tuple field| Line | Coverage | Source |
|---|---|---|
| 703 | ✗ | (borrow_check_place_expr(env, assumptions, state, prefix) => (prefix_typed, state)) |
| 704 | ✗ | (prove_ty_is_rigid(env, assumptions, state, &prefix_typed.ty) => (RigidTy { name: RigidName::Tuple(arity), parameters }, state)) |
| 705 | ✗ | (if field_index < arity) |
| 706 | ✗ | (if let Parameter::Ty(field_ty) = ¶meters[*field_index]) |
| ──────── ("tuple field") | ||
| 708 | ✗ | (borrow_check_place_expr(env, assumptions, state, PlaceExpr::Field { prefix, field_name: FieldName::Index(field_index) }) => ( TypedPlaceExpr::new(field_ty, TypedPlaceExpressionData::tuple_field(prefix_typed, field_index)), state, )) |
parens| Line | Coverage | Source |
|---|---|---|
| 715 | ✗ | (borrow_check_place_expr(env, assumptions, state, place) => (place_typed, state)) |
| ──────── ("parens") | ||
| 717 | 8 | (borrow_check_place_expr(env, assumptions, state, PlaceExpr::Parens(place)) => (place_typed, state)) |
deref-ref| Line | Coverage | Source |
|---|---|---|
| 721 | ✗ | (borrow_check_place_expr(env, assumptions, state, prefix) => (prefix_typed, state)) |
| 722 | ✗ | (prove_is_implemented(env, assumptions, state, TraitId::new("Derefable").with_self(&prefix_typed.ty)) => state) |
| 723 | N/A | (let referent_ty = AliasTy::associated_ty( TraitId::new("Derefable"), AssociatedItemId::new("Target"), 0, vec![&prefix_typed.ty], )) |
| ──────── ("deref-ref") | ||
| 730 | 42 | (borrow_check_place_expr(env, assumptions, state, PlaceExpr::Deref { prefix }) => ( TypedPlaceExpr::new(referent_ty, TypedPlaceExpressionData::deref(prefix_typed)), state, )) |