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

Positive coverage: is_local_trait_ref / local parameter

local parameter
LineCoverageSource
214✗(i in 0 .. goal.parameters.len())
2157(is_local_parameter(decls, env, assumptions, &goal.parameters[*i]) => c1)
218N/A(let assumptions = c1.substitution().apply(assumptions))
219N/A(let goal = c1.substitution().apply(goal))
2201(for_all(decls, env, assumptions, &goal.parameters[..*i], &is_not_downstream) => c2)
──────── ("local parameter")
22211(is_local_trait_ref(decls, env, assumptions, goal) => c1.seq(c2))

11 tests exercised this rule:

Source location: crates/formality-rust/src/prove/test/is_local.rs:26 (all coverage from this test)

#[test]
fn test_exists_not_local() {
    test_prove(
        Program::empty(),
        term("exists<T> {} => {@IsLocal(Debug(T))}"),
    )
    .assert_ok(expect!["{Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: false, substitution: {} }}"])
}
Proof tree

Source location: tests/coherence_orphan.rs:85 (all coverage from this test)

#[test]
fn mirror_FooStruct() {
    FormalityTest::new(crates![crate core {
        trait CoreTrait {}

        trait Mirror {
            type Assoc : [];
        }

        impl<T> Mirror for T {
            type Assoc = T;
        }
    },
    crate foo {
        struct FooStruct {}
        impl CoreTrait for <FooStruct as Mirror>::Assoc {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/coherence_orphan.rs:99 (all coverage from this test)

#[test]
fn covered_VecT() {
    FormalityTest::new(crates![crate core {
        trait CoreTrait<T> {}
        struct Vec<T> {}
    },
    crate foo {
        struct FooStruct {}
        impl<T> CoreTrait<FooStruct> for Vec<T> {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/coherence_orphan.rs:221 (all coverage from this test)

#[test]
fn CoreTraitLocal_for_AliasToKnown_in_Foo() {
    // TODO: see comment in `orphan_check` from prev commit
    FormalityTest::new(crates![crate core {
        trait CoreTrait<T> {}

        trait Unit {
            type Assoc : [];
        }

        impl<T> Unit for T {
            type Assoc = ();
        }
    },
    crate foo {
        struct FooStruct {}
        impl CoreTrait<FooStruct> for <() as Unit>::Assoc {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/drop.rs:20 (all coverage from this test)

#[test]
fn drop_impl_simple_struct() {
    FormalityTest::new(crates![
        crate Foo {
            struct MyStruct {
                value: u32,
            }

            impl Drop for MyStruct {}
        }
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1058 nodes shown)

Source location: tests/drop.rs:38 (all coverage from this test)

#[test]
fn drop_impl_generic_struct() {
    FormalityTest::new(crates![
        crate Foo {
            trait Clone {}

            struct MyStruct<T> where T: Clone {
                value: T,
            }

            impl<T> Drop for MyStruct<T> where T: Clone {}
        }
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1108 nodes shown)

Source location: tests/drop.rs:54 (all coverage from this test)

#[test]
fn drop_impl_generic_no_where_clauses() {
    FormalityTest::new(crates![
        crate Foo {
            struct Wrapper<T> {
                value: T,
            }

            impl<T> Drop for Wrapper<T> {}
        }
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1074 nodes shown)

Source location: tests/drop.rs:78 (all coverage from this test)

#[test]
fn drop_impl_subset_where_clauses() {
    FormalityTest::new(crates![
        crate Foo {
            trait Clone {}
            trait Debug {}

            struct MyStruct<T> where T: Clone, T: Debug {
                value: T,
            }

            // Impl has no where-clauses — but the struct requires them.
            impl<T> Drop for MyStruct<T> {}
        }
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1096 nodes shown)

Source location: tests/drop.rs:94 (all coverage from this test)

#[test]
fn drop_impl_enum() {
    FormalityTest::new(crates![
        crate Foo {
            enum MyEnum {
                Variant{},
            }

            impl Drop for MyEnum {}
        }
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1049 nodes shown)

Source location: tests/drop.rs:111 (all coverage from this test)

#[test]
fn drop_impl_cross_crate_local() {
    FormalityTest::new(crates![
        crate a {
            struct MyStruct {
                value: u32,
            }

            impl Drop for MyStruct {}
        },
        crate b {}
    ])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1061 nodes shown)

Source location: tests/field_projections.rs:17 (all coverage from this test)

fn test(ptr: Ptr) -> () {
    let x: () = *ptr;
}

Proof trees omitted for the remaining 1 tests; each one is on its test’s page in Coverage by test.