Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Judgment borrow_check_place_expr at crates/formality-rust/src/check/borrow_check/nll.rs:563

Signature:

borrow_check_place_expr(env: TypeckEnv, assumptions: Wcs, state: FlowState, place: PlaceExpr,) => (TypedPlaceExpr, FlowState)

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
LineCoverageSource
5742(let ty = state.local_variable(&local_id)?)
──────── ("local")
57658(borrow_check_place_expr(_env, _assumptions, state, PlaceExpr::Var(local_id)) => (
TypedPlaceExpr::new(ty, TypedPlaceExpressionData::local(local_id)),
state,
))
struct field
LineCoverageSource
583(borrow_check_place_expr(env, assumptions, state, prefix) => (prefix_typed, state))
5841(prove_ty_is_rigid(env, assumptions, state, &prefix_typed.ty) => (RigidTy { name: RigidName::AdtId(adt_id), parameters }, state))
585(let Struct { id: _, binder } = env.crates().struct_named(&adt_id)?)
586(let StructBoundData { where_clauses, fields } = binder.instantiate_with(&parameters)?)
587(prove_where_clauses(env, assumptions, state, where_clauses) => state)
588(field in fields)
5891(if field.name == *field_name)
──────── ("struct field")
5917(borrow_check_place_expr(env, assumptions, state, PlaceExpr::Field { prefix, field_name }) => (
TypedPlaceExpr::new(&field.ty, TypedPlaceExpressionData::field(prefix_typed, field_name)),
state,
))
tuple field
LineCoverageSource
598(borrow_check_place_expr(env, assumptions, state, prefix) => (prefix_typed, state))
599(prove_ty_is_rigid(env, assumptions, state, &prefix_typed.ty) => (RigidTy { name: RigidName::Tuple(arity), parameters }, state))
600(if field_index < arity)
601(if let Parameter::Ty(field_ty) = &parameters[*field_index])
──────── ("tuple field")
603(borrow_check_place_expr(env, assumptions, state, PlaceExpr::Field { prefix, field_name: FieldName::Index(field_index) }) => (
TypedPlaceExpr::new(field_ty, TypedPlaceExpressionData::field(prefix_typed, field_index)),
state,
))
parens
LineCoverageSource
610(borrow_check_place_expr(env, assumptions, state, place) => (place_typed, state))
──────── ("parens")
6122(borrow_check_place_expr(env, assumptions, state, PlaceExpr::Parens(place)) => (place_typed, state))
deref-ref
LineCoverageSource
616(borrow_check_place_expr(env, assumptions, state, prefix) => (prefix_typed, state))
617(prove_is_implemented(env, assumptions, state, TraitId::new("Derefable").with_self(&prefix_typed.ty)) => state)
618N/A(let referent_ty = AliasTy::associated_ty(
TraitId::new("Derefable"),
AssociatedItemId::new("Target"),
0,
vec![&prefix_typed.ty],
))
──────── ("deref-ref")
62518(borrow_check_place_expr(env, assumptions, state, PlaceExpr::Deref { prefix }) => (
TypedPlaceExpr::new(referent_ty, TypedPlaceExpressionData::deref(prefix_typed)),
state,
))