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 |
|---|
| 35 | N/A | (let (env, subst) = env.universal_substitution(binder)) |
| 36 | N/A | (let p1 = binder.instantiate_with(&subst).unwrap()) |
| 37 | 8 | (prove_wc(decls, env, assumptions, p1) => c) |
| | ──────── ("forall") |
| 39 | 12 | (prove_wc(decls, env, assumptions, WcData::ForAll(binder)) => c.pop_subst(&subst)) |
implies
| Line | Coverage | Source |
|---|
| 43 | 3 | (prove_wc(decls, env, (assumptions, p1), p2) => c) |
| | ──────── ("implies") |
| 45 | 4 | (prove_wc(decls, env, assumptions, WcData::Implies(p1, p2)) => c) |
assumption - predicate
| Line | Coverage | Source |
|---|
| 49 | ✗ | (a in assumptions) |
| 50 | 10 | (prove_via(decls, env, assumptions, a, goal) => c) |
| | ──────── ("assumption - predicate") |
| 52 | 13 | (prove_wc(decls, env, assumptions, WcData::Predicate(goal)) => c) |
assumption - relation
| Line | Coverage | Source |
|---|
| 55 | ✗ | (a in assumptions) |
| 56 | 12 | (prove_via(decls, env, assumptions, a, goal) => c) |
| | ──────── ("assumption - relation") |
| 58 | 4 | (prove_wc(decls, env, assumptions, WcData::Relation(goal)) => c) |
positive impl
| Line | Coverage | Source |
|---|
| 65 | ✗ | (i in decls.impl_decls(&trait_ref.trait_id)) |
| 68 | N/A | (let (env, subst) = env.existential_substitution(&i.binder)) |
| 69 | N/A | (let i = i.binder.instantiate_with(&subst).unwrap()) |
| 73 | N/A | (let t = decls.trait_decl(&i.trait_ref.trait_id).binder.instantiate_with(&i.trait_ref.parameters).unwrap()) |
| 80 | N/A | (let co_assumptions = (assumptions, trait_ref)) |
| 81 | 6 | (prove(decls, env, co_assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c) |
| 82 | 1 | (prove_after(decls, c, co_assumptions, &i.where_clause) => c) |
| 88 | 4 | (prove_after(decls, c, assumptions, &t.where_clause) => c) |
| | ──────── ("positive impl") |
| 90 | 119 | (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst)) |
coherence / remote impl
| Line | Coverage | Source |
|---|
| 94 | ✗ | (if env.bias() == Bias::Completeness) |
| 95 | ✗ | (may_be_remote(decls, env, assumptions, trait_ref) => c) |
| | ──────── ("coherence / remote impl") |
| 97 | ✗ | (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c) |
negative impl
| Line | Coverage | Source |
|---|
| 101 | ✗ | (i in decls.neg_impl_decls(&trait_ref.trait_id)) |
| 102 | N/A | (let (env, subst) = env.existential_substitution(&i.binder)) |
| 103 | N/A | (let i = i.binder.instantiate_with(&subst).unwrap()) |
| 104 | ✗ | (prove(decls, env, assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c) |
| 105 | ✗ | (prove_after(decls, c, assumptions, &i.where_clause) => c) |
| | ──────── ("negative impl") |
| 107 | 3 | (prove_wc(decls, env, assumptions, Predicate::NotImplemented(trait_ref)) => c.pop_subst(&subst)) |
alias eq
| Line | Coverage | Source |
|---|
| 111 | ✗ | (prove_eq(decls, env, assumptions, alias_ty, ty) => c) |
| | ──────── ("alias eq") |
| 113 | 1 | (prove_wc(decls, env, assumptions, Predicate::AliasEq(alias_ty, ty)) => c) |
trait implied bound
| Line | Coverage | Source |
|---|
| 117 | 12 | (ti in decls.trait_invariants()) |
| 118 | N/A | (let (env, subst) = env.existential_substitution(&ti.binder)) |
| 119 | N/A | (let ti = ti.binder.instantiate_with(&subst).unwrap()) |
| 120 | 4 | (prove_via(decls, env, assumptions, &ti.where_clause, trait_ref) => c) |
| 121 | 3 | (prove_after(decls, c, assumptions, &ti.trait_ref) => c) |
| | ──────── ("trait implied bound") |
| 123 | 1 | (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst)) |
eq
| Line | Coverage | Source |
|---|
| 127 | 14 | (prove_eq(decls, env, assumptions, a, b) => c) |
| | ──────── ("eq") |
| 129 | 131 | (prove_wc(decls, env, assumptions, Relation::Equals(a, b)) => c) |
subtype
| Line | Coverage | Source |
|---|
| 133 | 5 | (prove_sub(decls, env, assumptions, a, b) => c) |
| | ──────── ("subtype") |
| 135 | 67 | (prove_wc(decls, env, assumptions, WcData::Relation(Relation::Sub(a, b))) => c) |
trait ref is local
| Line | Coverage | Source |
|---|
| 148 | 6 | (is_local_trait_ref(decls, env, assumptions, trait_ref) => c) |
| | ──────── ("trait ref is local") |
| 150 | 111 | (prove_wc(decls, env, assumptions, Predicate::IsLocal(trait_ref)) => c) |
outlives
| Line | Coverage | Source |
|---|
| 154 | 4 | (prove_outlives(decls, env, assumptions, a, b) => c) |
| | ──────── ("outlives") |
| 156 | 96 | (prove_wc(decls, env, assumptions, Relation::Outlives(a, b)) => c) |
const has ty
| Line | Coverage | Source |
|---|
| 167 | 1 | (prove_const_has_type(decls, env, assumptions, constant) => (ty_constant, c)) |
| 168 | 1 | (prove_after(decls, c, assumptions, Relation::equals(ty_constant, ty)) => c) |
| | ──────── ("const has ty") |
| 170 | 3 | (prove_wc(decls, env, assumptions, Predicate::ConstHasType(constant, ty)) => c) |