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: prove_wc / assumption

assumption
LineCoverageSource
47✗(a in assumptions)
4821(prove_via(decls, env, assumptions, a, goal) => c)
──────── ("assumption")
5019(prove_wc(decls, env, assumptions, Wc::Predicate(goal)) => c)

19 tests exercised this rule:

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

#[test]
fn test_a() {
    test_prove(
        Program::empty(),
        term("{} => {for<T, U> if {T = u32, U = Vec<T>} U = Vec<u32>}"),
    )
    .assert_ok(expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}
Proof tree

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

#[test]
fn test_normalize_assoc_ty() {
    test_prove(
        Program::empty(),
        term("{} => {for<T> if { <T as Iterator>::Item = u32 } <T as Iterator>::Item = u32}"),
    )
    .assert_ok(expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}
Proof tree

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

#[test]
fn eq_implies_partial_eq() {
    let assumptions: Wcs = Wcs::t();
    let goal: Wc = term("for<T> if {Eq(T)} PartialEq(T)");
    let constraints = prove(decls(), (), assumptions, goal);
    constraints.assert_ok(
    expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}
Proof tree

Source location: tests/basic_tests.rs:58 (all coverage from this test)

#[test]
fn hello_world() {
    FormalityTest::new(crates![crate Foo {
        trait Foo<T> where T: Bar<Self>, Self: Baz {}

        trait Bar<T> where T: Baz {}

        trait Baz {}

        impl Baz for u32 {}

        impl Bar<u32> for u32 {}
        impl<T> Bar<T> for () where T: Baz {}
    }])
    .skip_execute()
    .ok()
}
Proof tree
… (200 of 1245 nodes shown)

Source location: tests/basic_tests.rs:149 (all coverage from this test)

#[test]
fn non_lifetime_binder_in_trait_impl_where_clause_pass() {
    FormalityTest::new(crates![crate core {
        #![feature(non_lifetime_binders)]
        trait A<T> where T: B { }

        trait B { }

        impl<T> B for T where for<U> u32: A<U> { }
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/basic_tests.rs:179 (all coverage from this test)

#[test]
fn non_lifetime_binder_in_neg_trait_impl_where_clause_pass() {
    FormalityTest::new(crates![crate core {
        #![feature(non_lifetime_binders)]
        trait A<T> where T: B { }

        trait B { }

        impl<T> !A<T> for u32 where for<U> u32: A<U> { }

        impl <T> B for T {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/borrowck.rs:4472 (all coverage from this test)

fn use_it<'a, 'b>() -> u32 {
    exists<'r0> {
        let v: Invariant<'r0> = create_invariant::<'r0>();
        if true {
            return sink::<'a, 'r0>(v);
        } else {
            return sink::<'b, 'r0>(v);
        }
    }
}
Proof tree
… (200 of 1182 nodes shown)

Source location: tests/borrowck.rs:4537 (all coverage from this test)

fn use_it_but_its_the_same_region<'a, 'b>() -> u32 where 'a: 'b, 'b: 'a {
    exists<'r0> {
        let v: Invariant<'r0> = create_invariant::<'r0>();
        if true {
            return sink::<'a, 'r0>(v);
        } else {
            return sink::<'b, 'r0>(v);
        }
    }
}
Proof tree
… (200 of 1190 nodes shown)

Source location: tests/coherence_overlap.rs:148 (all coverage from this test)

#[test]
fn neg_CoreTrait_for_CoreStruct_implies_no_overlap() {
    FormalityTest::new(crates![crate core {
        #![feature(negative_impls)]
        trait CoreTrait {}
        struct CoreStruct {}
        impl !CoreTrait for CoreStruct {}
    },
    crate foo {
        trait FooTrait {}
        impl<T> FooTrait for T where T: CoreTrait {}
        impl FooTrait for CoreStruct {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/coherence_overlap.rs:207 (all coverage from this test)

#[test]
fn u32_T_where_T_Not_impls() {
    FormalityTest::new(crates![crate core {
        trait Foo {}
        impl Foo for u32 {}
        impl<T> Foo for T where T: Not {}

        trait Not {}
    }])
    .skip_execute()
    .ok()
}
Proof tree

Source location: tests/coherence_overlap.rs:308 (all coverage from this test)

#[test]
fn is_local_unknowable_trait_ref() {
    FormalityTest::new(crates![crate core {
        trait Project {
            type Assoc: [];
        }

        impl<T> Project for T {
            type Assoc = T;
        }

        trait Foo<U> { }
    },
    crate foo {
        struct LocalType {}

        trait Overlap<U> {}
        impl<T, U> Overlap<U> for T
        where
            <T as Project>::Assoc: Foo<U> {}
        impl<T> Overlap<LocalType> for () {}
    }])
    .skip_execute()
    .ok()
}

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

Source location: tests/consts.rs:23 (all coverage from this test)

#[test]
fn ok() {
    FormalityTest::new(crates![crate Foo {
        trait Foo<const C> where type_of_const C is bool {}
        trait Bar<const C> where type_of_const C is u32 {}

        impl<const C> Foo<C> for u32 where type_of_const C is bool {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/consts.rs:92 (all coverage from this test)

#[test]
fn generic_match() {
    FormalityTest::new(crates![crate Foo {
        trait Foo<const C> where type_of_const C is bool {}

        // Here, the impl matches the trait bound.
        impl<const C> Foo<C> for u32 where type_of_const C is bool {}
    }])
    .skip_execute()
    .ok()
}

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()
}

Source location: tests/mir_typeck.rs:961 (all coverage from this test)

fn foo<'a, T>(v1: &'a T) -> T
where
    T: Copy,
    T: 'a,
{
    exists<'r0> {
        let v2: T = *v1;
        return v2;
    }
}

Source location: tests/projection.rs:36 (all coverage from this test)

#[test]
fn normalize_basic() {
    test_where_clause(
        NORMALIZE_BASIC,
        "forall<T> exists<U> {} => { <Vec<T> as Iterator>::Item = U }",
    )
    .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => <Vec<!ty_1> as Iterator>::Item} }, Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => !ty_1} }}"]);

    test_where_clause(
        NORMALIZE_BASIC,
        "forall<T> {} => { Iterator(Vec<T>), <Vec<T> as Iterator>::Item = T }",
    )
    .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);

    test_where_clause(
        NORMALIZE_BASIC,
        "forall<T> { Iterator(T), <T as Iterator>::Item = Foo } => { <T as Iterator>::Item = Foo }",
    ).assert_ok(
        expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]
    );

    test_where_clause(
        NORMALIZE_BASIC,
        "forall<T> exists<U> { Iterator(T) } => { <T as Iterator>::Item = U }",
    )
    .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => <!ty_1 as Iterator>::Item} }}"]);

    test_where_clause(
        NORMALIZE_BASIC,
        "forall<T> { Iterator(T) } => { <T as Iterator>::Item = <T as Iterator>::Item }",
    )
    .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);

    test_where_clause(
        NORMALIZE_BASIC,
        "forall<T> exists<U> { Iterator(T) } => { <T as Iterator>::Item = <U as Iterator>::Item }",
    ).assert_ok(
    expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => !ty_1} }, Constraints { env: Env { variables: [!ty_1, ?ty_3, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => Vec<<!ty_1 as Iterator>::Item>, ?ty_3 => <!ty_1 as Iterator>::Item} }}"]);
}

Source location: tests/references.rs:36 (all coverage from this test)

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

fn main() -> () {
    exists<'y> {
        let a: u32 = 22_u32;
        let f: Foo<'y> = Foo::<'y> { y: &'y a };
    }
}

Source location: tests/well_formed_trait_ref.rs:19 (all coverage from this test)

#[test]
fn dependent_where_clause() {
    FormalityTest::new(crates![crate foo {
        trait Trait1 {}

        trait Trait2 {}

        struct S1<T> where T: Trait1 {
            dummy: T,
        }

        struct S2<T> where T: Trait1, S1<T> : Trait2 {
            dummy: T,
        }
    }])
    .skip_execute()
    .ok()
}