Judgment prove_predicate
judgment_fn! {
/// The "heart" of the trait system -- prove that a where-clause holds given a set of declarations, variable environment, and set of assumptions.
/// If successful, returns the constraints under which the where-clause holds.
pub fn prove_predicate(
_decls: Program,
env: Env,
assumptions: Predicates,
goal: Predicate,
) => Constraints {
/* rules omitted */
}
}Source: crates/formality-rust/src/prove/prove_predicate.rs:22
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.
forall| Line | Coverage | Source |
|---|---|---|
| 34 | ✗ | (scope(enter_universally_with_constraints(env, binder) => (env, p1)) with(c) (prove_predicate(decls, env, assumptions, p1) => c)) |
| ──────── ("forall") | ||
| 37 | 14 | (prove_predicate(decls, env, assumptions, Predicate::ForAll(binder)) => c) |
implies| Line | Coverage | Source |
|---|---|---|
| 41 | 3 | (prove_predicate(decls, env, (assumptions, p1), p2) => c) |
| ──────── ("implies") | ||
| 43 | 4 | (prove_predicate(decls, env, assumptions, Predicate::Implies(p1, p2)) => c) |
assumption| Line | Coverage | Source |
|---|---|---|
| 47 | ✗ | (a in assumptions) |
| 48 | 34 | (prove_via(decls, env, assumptions, a, goal) => c) |
| ──────── ("assumption") | ||
| 50 | 23 | (prove_predicate(decls, env, assumptions, Predicate::AtomicPredicate(goal)) => c) |
positive impl| Line | Coverage | Source |
|---|---|---|
| 57 | ✗ | (i in decls.impl_decls(&trait_ref.trait_id)) |
| 60 | ✗ | (scope(enter_existentially_with_constraints(env, &i.binder) => (env, i)) with(c) // Instantiate trait where-clauses from `Foo<?B>`. If we had `trait Foo<X: Debug>`, for example, // this would yield `?B: Debug`. (let t = decls.trait_decl(&i.trait_ref.trait_id).binder.instantiate_with(&i.trait_ref.parameters).unwrap()) // Create a set of assumptions `co_assumptions` that include the predicate the impl itself // is asserting (i.e., `A: Foo<B>`). When proving the impl's where-clauses, we are allowed // to assume this is true (in a coinductive fashion). // // NB: This is actually not what Rust currently does, but it is what "we" (types team) want it to do. (let co_assumptions = (assumptions, trait_ref)) (prove(decls, env, co_assumptions, Predicates::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c) (prove_after(decls, c, co_assumptions, &i.where_clause) => c) // Prove that the well-formedness requirements of the *trait* hold -- for this proof, we cannot // assume that the trait is implemented, because that would allow specious implied bounds // (i.e., we could assume that `B: Debug` based on the trait definition + the existence of an impl, // but actually the impl is responsible for proving that `B: Debug`). (prove_after(decls, c, assumptions, &t.where_clause) => c)) |
| ──────── ("positive impl") | ||
| 80 | 219 | (prove_predicate(decls, env, assumptions, AtomicPredicate::IsImplemented(trait_ref)) => c) |
coherence / remote impl| Line | Coverage | Source |
|---|---|---|
| 84 | ✗ | (if env.bias() == Bias::Completeness) |
| 85 | ✗ | (may_be_remote(decls, env, assumptions, trait_ref) => c) |
| ──────── ("coherence / remote impl") | ||
| 87 | ✗ | (prove_predicate(decls, env, assumptions, AtomicPredicate::IsImplemented(trait_ref)) => c) |
negative impl| Line | Coverage | Source |
|---|---|---|
| 91 | 8 | (i in decls.neg_impl_decls(&trait_ref.trait_id)) |
| 92 | ✗ | (scope(enter_existentially_with_constraints(env, &i.binder) => (env, i)) with(c) (prove(decls, env, assumptions, Predicates::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c) (prove_after(decls, c, assumptions, &i.where_clause) => c)) |
| ──────── ("negative impl") | ||
| 96 | 3 | (prove_predicate(decls, env, assumptions, AtomicPredicate::NotImplemented(trait_ref)) => c) |
alias eq| Line | Coverage | Source |
|---|---|---|
| 100 | ✗ | (prove_eq(decls, env, assumptions, alias_ty, ty) => c) |
| ──────── ("alias eq") | ||
| 102 | 1 | (prove_predicate(decls, env, assumptions, AtomicPredicate::AliasEq(alias_ty, ty)) => c) |
trait implied bound| Line | Coverage | Source |
|---|---|---|
| 106 | 19 | (ti in decls.trait_invariants()) |
| 107 | ✗ | (scope(enter_existentially_with_constraints(env, &ti.binder) => (env, ti)) with(c) (prove_via(decls, env, assumptions, &ti.where_clause, trait_ref) => c) (prove_after(decls, c, assumptions, &ti.trait_ref) => c)) |
| ──────── ("trait implied bound") | ||
| 111 | 1 | (prove_predicate(decls, env, assumptions, AtomicPredicate::IsImplemented(trait_ref)) => c) |
eq| Line | Coverage | Source |
|---|---|---|
| 115 | 17 | (prove_eq(decls, env, assumptions, a, b) => c) |
| ──────── ("eq") | ||
| 117 | 231 | (prove_predicate(decls, env, assumptions, AtomicPredicate::Equals(a, b)) => c) |
subtype| Line | Coverage | Source |
|---|---|---|
| 121 | 11 | (prove_sub(decls, env, assumptions, a, b) => c) |
| ──────── ("subtype") | ||
| 123 | 134 | (prove_predicate(decls, env, assumptions, AtomicPredicate::Sub(a, b)) => c) |
trait well formed| Line | Coverage | Source |
|---|---|---|
| 127 | 1 | (for_all(decls, env, assumptions, &trait_ref.parameters, &prove_wf) => c) |
| 128 | N/A | (let t = decls.trait_decl(&trait_ref.trait_id)) |
| 129 | N/A | (let t = t.binder.instantiate_with(&trait_ref.parameters).unwrap()) |
| 130 | 2 | (prove_after(decls, c, assumptions, &t.where_clause) => c) |
| ──────── ("trait well formed") | ||
| 132 | 30 | (prove_predicate(decls, env, assumptions, AtomicPredicate::WellFormedTraitRef(trait_ref)) => c) |
trait ref is local| Line | Coverage | Source |
|---|---|---|
| 136 | 12 | (is_local_trait_ref(decls, env, assumptions, trait_ref) => c) |
| ──────── ("trait ref is local") | ||
| 138 | 211 | (prove_predicate(decls, env, assumptions, AtomicPredicate::IsLocal(trait_ref)) => c) |
outlives| Line | Coverage | Source |
|---|---|---|
| 142 | 8 | (prove_outlives(decls, env, assumptions, a, b) => c) |
| ──────── ("outlives") | ||
| 144 | 195 | (prove_predicate(decls, env, assumptions, AtomicPredicate::Outlives(a, b)) => c) |
parameter well formed| Line | Coverage | Source |
|---|---|---|
| 149 | 4 | (prove_wf(decls, env, assumptions, p) => c) |
| ──────── ("parameter well formed") | ||
| 151 | 204 | (prove_predicate(decls, env, assumptions, AtomicPredicate::WellFormed(p)) => c) |
const has ty| Line | Coverage | Source |
|---|---|---|
| 155 | 1 | (prove_const_has_type(decls, env, assumptions, constant) => (ty_constant, c)) |
| 156 | 1 | (prove_after(decls, c, assumptions, AtomicPredicate::equals(ty_constant, ty)) => c) |
| ──────── ("const has ty") | ||
| 158 | 4 | (prove_predicate(decls, env, assumptions, AtomicPredicate::ConstHasType(constant, ty)) => c) |