Signature:
prove_wc(_decls: Program, env: Env, assumptions: Wcs, goal: Wc,) => Constraints
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 |
|---|
| 33 | N/A | (let (env, subst) = env.universal_substitution(binder)) |
| 34 | N/A | (let p1 = binder.instantiate_with(&subst).unwrap()) |
| 35 | 8 | (prove_wc(decls, env, assumptions, p1) => c) |
| | ──────── ("forall") |
| 37 | 12 | (prove_wc(decls, env, assumptions, Wc::ForAll(binder)) => c.pop_subst(&subst)) |
implies
| Line | Coverage | Source |
|---|
| 41 | 3 | (prove_wc(decls, env, (assumptions, p1), p2) => c) |
| | ──────── ("implies") |
| 43 | 4 | (prove_wc(decls, env, assumptions, Wc::Implies(p1, p2)) => c) |
assumption
| Line | Coverage | Source |
|---|
| 47 | ✗ | (a in assumptions) |
| 48 | 21 | (prove_via(decls, env, assumptions, a, goal) => c) |
| | ──────── ("assumption") |
| 50 | 19 | (prove_wc(decls, env, assumptions, Wc::Predicate(goal)) => c) |
positive impl
| Line | Coverage | Source |
|---|
| 57 | ✗ | (i in decls.impl_decls(&trait_ref.trait_id)) |
| 60 | N/A | (let (env, subst) = env.existential_substitution(&i.binder)) |
| 61 | N/A | (let i = i.binder.instantiate_with(&subst).unwrap()) |
| 65 | N/A | (let t = decls.trait_decl(&i.trait_ref.trait_id).binder.instantiate_with(&i.trait_ref.parameters).unwrap()) |
| 72 | N/A | (let co_assumptions = (assumptions, trait_ref)) |
| 73 | 7 | (prove(decls, env, co_assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c) |
| 74 | 2 | (prove_after(decls, c, co_assumptions, &i.where_clause) => c) |
| 80 | 4 | (prove_after(decls, c, assumptions, &t.where_clause) => c) |
| | ──────── ("positive impl") |
| 82 | 136 | (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst)) |
coherence / remote impl
| Line | Coverage | Source |
|---|
| 86 | ✗ | (if env.bias() == Bias::Completeness) |
| 87 | ✗ | (may_be_remote(decls, env, assumptions, trait_ref) => c) |
| | ──────── ("coherence / remote impl") |
| 89 | ✗ | (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c) |
negative impl
| Line | Coverage | Source |
|---|
| 93 | ✗ | (i in decls.neg_impl_decls(&trait_ref.trait_id)) |
| 94 | N/A | (let (env, subst) = env.existential_substitution(&i.binder)) |
| 95 | N/A | (let i = i.binder.instantiate_with(&subst).unwrap()) |
| 96 | ✗ | (prove(decls, env, assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c) |
| 97 | ✗ | (prove_after(decls, c, assumptions, &i.where_clause) => c) |
| | ──────── ("negative impl") |
| 99 | 3 | (prove_wc(decls, env, assumptions, Predicate::NotImplemented(trait_ref)) => c.pop_subst(&subst)) |
alias eq
| Line | Coverage | Source |
|---|
| 103 | ✗ | (prove_eq(decls, env, assumptions, alias_ty, ty) => c) |
| | ──────── ("alias eq") |
| 105 | 1 | (prove_wc(decls, env, assumptions, Predicate::AliasEq(alias_ty, ty)) => c) |
trait implied bound
| Line | Coverage | Source |
|---|
| 109 | 14 | (ti in decls.trait_invariants()) |
| 110 | N/A | (let (env, subst) = env.existential_substitution(&ti.binder)) |
| 111 | N/A | (let ti = ti.binder.instantiate_with(&subst).unwrap()) |
| 112 | 4 | (prove_via(decls, env, assumptions, &ti.where_clause, trait_ref) => c) |
| 113 | 3 | (prove_after(decls, c, assumptions, &ti.trait_ref) => c) |
| | ──────── ("trait implied bound") |
| 115 | 1 | (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst)) |
eq
| Line | Coverage | Source |
|---|
| 119 | 15 | (prove_eq(decls, env, assumptions, a, b) => c) |
| | ──────── ("eq") |
| 121 | 148 | (prove_wc(decls, env, assumptions, Predicate::Equals(a, b)) => c) |
subtype
| Line | Coverage | Source |
|---|
| 125 | 5 | (prove_sub(decls, env, assumptions, a, b) => c) |
| | ──────── ("subtype") |
| 127 | 82 | (prove_wc(decls, env, assumptions, Predicate::Sub(a, b)) => c) |
trait ref is local
| Line | Coverage | Source |
|---|
| 140 | 7 | (is_local_trait_ref(decls, env, assumptions, trait_ref) => c) |
| | ──────── ("trait ref is local") |
| 142 | 128 | (prove_wc(decls, env, assumptions, Predicate::IsLocal(trait_ref)) => c) |
outlives
| Line | Coverage | Source |
|---|
| 146 | 7 | (prove_outlives(decls, env, assumptions, a, b) => c) |
| | ──────── ("outlives") |
| 148 | 113 | (prove_wc(decls, env, assumptions, Predicate::Outlives(a, b)) => c) |
const has ty
| Line | Coverage | Source |
|---|
| 159 | 1 | (prove_const_has_type(decls, env, assumptions, constant) => (ty_constant, c)) |
| 160 | 1 | (prove_after(decls, c, assumptions, Predicate::equals(ty_constant, ty)) => c) |
| | ──────── ("const has ty") |
| 162 | 3 | (prove_wc(decls, env, assumptions, Predicate::ConstHasType(constant, ty)) => c) |