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, WcData::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, WcData::Implies(p1, p2)) => c) |
assumption - predicate
| Line | Coverage | Source |
|---|
| 47 | ✗ | (a in assumptions) |
| 48 | 11 | (prove_via(decls, env, assumptions, a, goal) => c) |
| | ──────── ("assumption - predicate") |
| 50 | 13 | (prove_wc(decls, env, assumptions, WcData::Predicate(goal)) => c) |
assumption - relation
| Line | Coverage | Source |
|---|
| 53 | ✗ | (a in assumptions) |
| 54 | 18 | (prove_via(decls, env, assumptions, a, goal) => c) |
| | ──────── ("assumption - relation") |
| 56 | 8 | (prove_wc(decls, env, assumptions, WcData::Relation(goal)) => c) |
positive impl
| Line | Coverage | Source |
|---|
| 63 | ✗ | (i in decls.impl_decls(&trait_ref.trait_id)) |
| 66 | N/A | (let (env, subst) = env.existential_substitution(&i.binder)) |
| 67 | N/A | (let i = i.binder.instantiate_with(&subst).unwrap()) |
| 71 | N/A | (let t = decls.trait_decl(&i.trait_ref.trait_id).binder.instantiate_with(&i.trait_ref.parameters).unwrap()) |
| 78 | N/A | (let co_assumptions = (assumptions, trait_ref)) |
| 79 | 7 | (prove(decls, env, co_assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c) |
| 80 | 2 | (prove_after(decls, c, co_assumptions, &i.where_clause) => c) |
| 86 | 4 | (prove_after(decls, c, assumptions, &t.where_clause) => c) |
| | ──────── ("positive impl") |
| 88 | 153 | (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst)) |
coherence / remote impl
| Line | Coverage | Source |
|---|
| 92 | ✗ | (if env.bias() == Bias::Completeness) |
| 93 | ✗ | (may_be_remote(decls, env, assumptions, trait_ref) => c) |
| | ──────── ("coherence / remote impl") |
| 95 | ✗ | (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c) |
negative impl
| Line | Coverage | Source |
|---|
| 99 | ✗ | (i in decls.neg_impl_decls(&trait_ref.trait_id)) |
| 100 | N/A | (let (env, subst) = env.existential_substitution(&i.binder)) |
| 101 | N/A | (let i = i.binder.instantiate_with(&subst).unwrap()) |
| 102 | ✗ | (prove(decls, env, assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c) |
| 103 | ✗ | (prove_after(decls, c, assumptions, &i.where_clause) => c) |
| | ──────── ("negative impl") |
| 105 | 3 | (prove_wc(decls, env, assumptions, Predicate::NotImplemented(trait_ref)) => c.pop_subst(&subst)) |
alias eq
| Line | Coverage | Source |
|---|
| 109 | ✗ | (prove_eq(decls, env, assumptions, alias_ty, ty) => c) |
| | ──────── ("alias eq") |
| 111 | 1 | (prove_wc(decls, env, assumptions, Predicate::AliasEq(alias_ty, ty)) => c) |
trait implied bound
| Line | Coverage | Source |
|---|
| 115 | 14 | (ti in decls.trait_invariants()) |
| 116 | N/A | (let (env, subst) = env.existential_substitution(&ti.binder)) |
| 117 | N/A | (let ti = ti.binder.instantiate_with(&subst).unwrap()) |
| 118 | 4 | (prove_via(decls, env, assumptions, &ti.where_clause, trait_ref) => c) |
| 119 | 3 | (prove_after(decls, c, assumptions, &ti.trait_ref) => c) |
| | ──────── ("trait implied bound") |
| 121 | 1 | (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst)) |
eq
| Line | Coverage | Source |
|---|
| 125 | 15 | (prove_eq(decls, env, assumptions, a, b) => c) |
| | ──────── ("eq") |
| 127 | 165 | (prove_wc(decls, env, assumptions, Relation::Equals(a, b)) => c) |
subtype
| Line | Coverage | Source |
|---|
| 131 | 5 | (prove_sub(decls, env, assumptions, a, b) => c) |
| | ──────── ("subtype") |
| 133 | 99 | (prove_wc(decls, env, assumptions, WcData::Relation(Relation::Sub(a, b))) => c) |
trait ref is local
| Line | Coverage | Source |
|---|
| 146 | 6 | (is_local_trait_ref(decls, env, assumptions, trait_ref) => c) |
| | ──────── ("trait ref is local") |
| 148 | 145 | (prove_wc(decls, env, assumptions, Predicate::IsLocal(trait_ref)) => c) |
outlives
| Line | Coverage | Source |
|---|
| 152 | 10 | (prove_outlives(decls, env, assumptions, a, b) => c) |
| | ──────── ("outlives") |
| 154 | 130 | (prove_wc(decls, env, assumptions, Relation::Outlives(a, b)) => c) |
const has ty
| Line | Coverage | Source |
|---|
| 165 | 1 | (prove_const_has_type(decls, env, assumptions, constant) => (ty_constant, c)) |
| 166 | 1 | (prove_after(decls, c, assumptions, Relation::equals(ty_constant, ty)) => c) |
| | ──────── ("const has ty") |
| 168 | 3 | (prove_wc(decls, env, assumptions, Predicate::ConstHasType(constant, ty)) => c) |