diff --git a/crates/formality-check/src/lib.rs b/crates/formality-check/src/lib.rs index 4a56b505..eb8dafab 100644 --- a/crates/formality-check/src/lib.rs +++ b/crates/formality-check/src/lib.rs @@ -3,13 +3,16 @@ use std::{collections::VecDeque, fmt::Debug}; use anyhow::bail; -use formality_core::Set; -use formality_prove::{is_definitely_not_proveable, Decls, Env}; +use formality_core::{ProvenSet, Set}; +use formality_prove::{is_definitely_not_proveable, Constraints, Decls, Env}; use formality_rust::{ grammar::{Crate, CrateItem, Program, Test, TestBoundData}, prove::ToWcs, }; -use formality_types::grammar::{CrateId, Fallible, Wcs}; +use formality_types::{ + grammar::{CrateId, Fallible, Wcs}, + rust::Visit, +}; mod mini_rust_check; @@ -134,18 +137,36 @@ impl Check<'_> { goal: impl ToWcs + Debug, ) -> Fallible<()> { let goal: Wcs = goal.to_wcs(); + self.prove_judgment(env, assumptions, goal.to_wcs(), formality_prove::prove) + } + + fn prove_judgment( + &self, + env: &Env, + assumptions: impl ToWcs, + goal: G, + judgment_fn: impl FnOnce(Decls, Env, Wcs, G) -> ProvenSet, + ) -> Fallible<()> + where + G: Debug + Visit + Clone, + { let assumptions: Wcs = assumptions.to_wcs(); assert!(env.only_universal_variables()); assert!(env.encloses((&assumptions, &goal))); - let cs = formality_prove::prove(self.decls, env, &assumptions, &goal); + let cs = judgment_fn( + self.decls.clone(), + env.clone(), + assumptions.clone(), + goal.clone(), + ); let cs = cs.into_set()?; if cs.iter().any(|c| c.unconditionally_true()) { return Ok(()); } - bail!("failed to prove {goal:?} given {assumptions:?}, got {cs:?}") + bail!("failed to prove `{goal:?}` given `{assumptions:?}`: got {cs:?}") } #[tracing::instrument(level = "Debug", skip(self, assumptions, goal))] diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs index 3baf715b..3c6da3f9 100644 --- a/crates/formality-check/src/mini_rust_check.rs +++ b/crates/formality-check/src/mini_rust_check.rs @@ -1,16 +1,15 @@ use std::iter::zip; -use formality_core::{Fallible, Map, Upcast}; -use formality_prove::Env; +use formality_core::{judgment_fn, Fallible, Map, Upcast}; +use formality_prove::{prove_normalize, Constraints, Decls, Env}; use formality_rust::grammar::minirust::ArgumentExpression::{ByValue, InPlace}; use formality_rust::grammar::minirust::PlaceExpression::Local; use formality_rust::grammar::minirust::ValueExpression::{Constant, Fn, Load}; use formality_rust::grammar::minirust::{ - self, ty_is_int, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, - ValueExpression, + self, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression, }; use formality_rust::grammar::FnBoundData; -use formality_types::grammar::{CrateId, FnId}; +use formality_types::grammar::{CrateId, FnId, Parameter, RigidName, RigidTy}; use formality_types::grammar::{Relation, Ty, Wcs}; use crate::{Check, CrateItem}; @@ -229,9 +228,7 @@ impl Check<'_> { // Check if the value is well-formed. let value_ty = self.check_value(typeck_env, switch_value).unwrap(); - if !ty_is_int(value_ty) { - bail!("The value used for switch must be an int."); - } + self.prove_judgment(&typeck_env.env, &fn_assumptions, value_ty, ty_is_int)?; // Ensure all bbid are valid. for switch_target in switch_targets { @@ -374,3 +371,34 @@ struct TypeckEnv { /// declared in the current crate. crate_id: CrateId, } + +judgment_fn! { + fn ty_is_int( + _decls: Decls, + env: Env, + assumptions: Wcs, + ty: Parameter, + ) => Constraints { + debug(assumptions, ty, env) + // If the type that we are currently checking is rigid, check if it is an int. + // If the type can be normalized, normalize until rigid then check if it is an int. + // For the rest of the case, it should fail. + + ( + (prove_normalize(&decl, &env, &assumptions, ty) => (c1, p))! + (let assumptions = c1.substitution().apply(&assumptions)) + (ty_is_int(&decl, &env, assumptions, p) => c2) + ----------------------------- ("alias_ty is int") + (ty_is_int(decl, env, assumptions, ty) => c2) + ) + + ( + (if id.is_int()) + ----------------------------- ("rigid_ty is int") + (ty_is_int(_decls, _env, _assumptions, RigidTy {name: RigidName::ScalarId(id), parameters: _}) => Constraints::none(env)) + ) + + } +} + +mod test; diff --git a/crates/formality-check/src/mini_rust_check/test.rs b/crates/formality-check/src/mini_rust_check/test.rs new file mode 100644 index 00000000..30d53da2 --- /dev/null +++ b/crates/formality-check/src/mini_rust_check/test.rs @@ -0,0 +1,29 @@ +// Decide how to do this test -- should it be a unit test? +// Can it be an integration test? + +// const TEST_TY_IS_INT: &str = "[ +// crate test { +// trait Id { +// type This: []; +// } + +// impl Id for T { +// type This = T; +// } +// } +// ]"; + +// #[test] +// fn test_ty_is_int() { +// test_where_clause( +// TEST_TY_IS_INT, +// "{} => { ::This = u16 }", +// ) +// .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }}"]); + +// test_where_clause( +// TEST_TY_IS_INT, +// "{} => { @is_int(::This) }", +// ) +// .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }}"]); +// } diff --git a/crates/formality-prove/src/lib.rs b/crates/formality-prove/src/lib.rs index 65a2745d..e29f4d20 100644 --- a/crates/formality-prove/src/lib.rs +++ b/crates/formality-prove/src/lib.rs @@ -1,3 +1,12 @@ +//! This crate contains the trait proving + type inference logic. +//! It correpsonds loosely to the `InferenceContext` and trait solving (fulfillment context, etc) +//! in the Rust compiler. +//! +//! The base operations we export are: +//! +//! * [`prove`][] -- prove a set of where-clauses to be true +//! * [`prove_normalize`][] -- normalize a type one step (typically used in a recursive setup) + // Defines the language used by derive(term) and friends. use formality_types::rust::FormalityLang; @@ -7,6 +16,7 @@ mod prove; pub use decls::*; pub use prove::prove; +pub use prove::prove_normalize::prove_normalize; pub use prove::Constraints; pub use prove::{is_definitely_not_proveable, may_not_be_provable, negation_via_failure}; pub use prove::{Bias, Env}; diff --git a/crates/formality-prove/src/prove.rs b/crates/formality-prove/src/prove.rs index 315d7e1e..ccbafa9a 100644 --- a/crates/formality-prove/src/prove.rs +++ b/crates/formality-prove/src/prove.rs @@ -6,7 +6,7 @@ mod minimize; mod negation; mod prove_after; mod prove_eq; -mod prove_normalize; +pub mod prove_normalize; mod prove_via; mod prove_wc; mod prove_wc_list; diff --git a/crates/formality-prove/src/prove/minimize/test.rs b/crates/formality-prove/src/prove/minimize/test.rs index 8f55e46b..e50fc86c 100644 --- a/crates/formality-prove/src/prove/minimize/test.rs +++ b/crates/formality-prove/src/prove/minimize/test.rs @@ -17,12 +17,14 @@ fn minimize_a() { let (env, subst) = env.existential_substitution(&term); let term = term.instantiate_with(&subst).unwrap(); - expect!["(Env { variables: [?ty_1, ?ty_2, ?ty_3], bias: Soundness }, [?ty_1, ?ty_3])"] - .assert_eq(&format!("{:?}", (&env, &term))); + expect![ + "(Env { variables: [?ty_1, ?ty_2, ?ty_3], bias: Soundness, pending: [] }, [?ty_1, ?ty_3])" + ] + .assert_eq(&format!("{:?}", (&env, &term))); let (mut env_min, term_min, m) = minimize(env, term); - expect!["(Env { variables: [?ty_0, ?ty_1], bias: Soundness }, [?ty_0, ?ty_1])"] + expect!["(Env { variables: [?ty_0, ?ty_1], bias: Soundness, pending: [] }, [?ty_0, ?ty_1])"] .assert_eq(&format!("{:?}", (&env_min, &term_min))); let ty0 = term_min[0].as_variable().unwrap(); @@ -51,6 +53,7 @@ fn minimize_a() { ?ty_3, ], bias: Soundness, + pending: [], }, known_true: true, substitution: { diff --git a/crates/formality-prove/src/prove/prove_normalize.rs b/crates/formality-prove/src/prove/prove_normalize.rs index 55bdbc06..7bc0c7fe 100644 --- a/crates/formality-prove/src/prove/prove_normalize.rs +++ b/crates/formality-prove/src/prove/prove_normalize.rs @@ -14,6 +14,9 @@ use crate::{ use super::constraints::Constraints; judgment_fn! { + /// Normalize `p` one step, returning a set of constraints and a new parameter `q` that is + /// semantically equivalent to `p`. e.g., if p is ` as IntoIterator>::Item`, this would + /// return `T`. pub fn prove_normalize( _decls: Decls, env: Env, diff --git a/crates/formality-prove/src/test/adt_wf.rs b/crates/formality-prove/src/test/adt_wf.rs index 98b86604..befdb7bd 100644 --- a/crates/formality-prove/src/test/adt_wf.rs +++ b/crates/formality-prove/src/test/adt_wf.rs @@ -32,6 +32,7 @@ fn well_formed_adt() { env: Env { variables: [], bias: Soundness, + pending: [], }, known_true: true, substitution: {}, @@ -51,21 +52,21 @@ fn not_well_formed_adt() { assumptions, Relation::WellFormed(goal), ).assert_err(expect![[r#" - judgment `prove { goal: {@ wf(X)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {@ wf(X)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {@ wf(X)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {@ wf(X)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ wf(X), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: @ wf(X), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wf { goal: X, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wf { goal: X, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "ADT" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }, goal: {Foo(u64)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo ], [impl Foo(u32)], [], [], [], [adt X where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Foo(u64)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because expression evaluated to an empty collection: `decls.trait_invariants()`"#]]); } diff --git a/crates/formality-prove/src/test/eq_assumptions.rs b/crates/formality-prove/src/test/eq_assumptions.rs index 0c3e332e..0baa39c5 100644 --- a/crates/formality-prove/src/test/eq_assumptions.rs +++ b/crates/formality-prove/src/test/eq_assumptions.rs @@ -14,7 +14,7 @@ fn test_a() { ) .assert_ok(expect![[r#" { - Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, + Constraints { env: Env { variables: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }, } "#]]); } @@ -27,7 +27,7 @@ fn test_b() { ) .assert_ok(expect![[r#" { - Constraints { env: Env { variables: [?ty_2, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => Vec, ?ty_2 => u32} }, + Constraints { env: Env { variables: [?ty_2, ?ty_1], bias: Soundness, pending: [] }, known_true: true, substitution: {?ty_1 => Vec, ?ty_2 => u32} }, } "#]]); } @@ -40,7 +40,7 @@ fn test_normalize_assoc_ty() { ) .assert_ok(expect![[r#" { - Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, + Constraints { env: Env { variables: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }, } "#]]); } @@ -52,39 +52,39 @@ fn test_normalize_assoc_ty_existential0() { term("exists {} => {for if { ::Item = u32 } ::Item = u32}"), ).assert_err( expect![[r#" - judgment `prove { goal: {for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: for if {<^ty0_0 as Iterator>::Item = u32} ::Item = u32, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: if {::Item = u32} ::Item = u32, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: if {::Item = u32} ::Item = u32, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "implies" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ::Item, b: u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: ::Item, b: u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_normalize { p: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "axiom-l" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: !ty_1, b: ?ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: !ty_1, b: ?ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_1)` the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `env.universe(p) < env.universe(v)` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_1)` the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because @@ -92,67 +92,67 @@ fn test_normalize_assoc_ty_existential0() { the rule "normalize-via-impl" failed at step #0 (src/file.rs:LL:CC) because expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: u32, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-l" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_0, !ty_1], bias: Soundness }, known_true: true, substitution: {} }, goal: {::Item = ::Item}, assumptions: {::Item = u32} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] }, known_true: true, substitution: {} }, goal: {::Item = ::Item}, assumptions: {::Item = u32} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {::Item = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {::Item = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {::Item = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {::Item = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: ::Item = ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: ::Item = ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove { goal: {!ty_0 = ?ty_1}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {!ty_0 = ?ty_1}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {!ty_0 = ?ty_1}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {!ty_0 = ?ty_1}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: !ty_0 = ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: !ty_0 = ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_0)` the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `env.universe(p) < env.universe(v)` the rule "normalize-l" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, known_true: true, substitution: {} }, goal: {u32 = ::Item}, assumptions: {::Item = u32} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] }, known_true: true, substitution: {} }, goal: {u32 = ::Item}, assumptions: {::Item = u32} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {u32 = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {u32 = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {u32 = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {u32 = ::Item}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: u32 = ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: u32 = ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: u32, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ::Item, b: u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: ::Item, b: u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_normalize { p: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "axiom-l" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_0)` the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `env.universe(p) < env.universe(v)` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_0)` the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because @@ -160,43 +160,43 @@ fn test_normalize_assoc_ty_existential0() { the rule "normalize-via-impl" failed at step #0 (src/file.rs:LL:CC) because expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove { goal: {?ty_1 = !ty_0}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {?ty_1 = !ty_0}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {?ty_1 = !ty_0}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {?ty_1 = !ty_0}, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: ?ty_1 = !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: ?ty_1 = !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_0)` the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `env.universe(p) < env.universe(v)` the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_normalize { p: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_normalize_via { goal: ::Item, via: ::Item = u32, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "axiom-l" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: !ty_0, b: ?ty_1, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_0)` the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `env.universe(p) < env.universe(v)` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ::Item, b: ::Item, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "alias" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_syntactically_eq { a: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_1, b: !ty_0, assumptions: {::Item = u32}, env: Env { variables: [?ty_1, !ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_0)` the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because @@ -218,7 +218,7 @@ fn test_normalize_assoc_ty_existential1() { ) .assert_ok(expect![[r#" { - Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, + Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [] }, known_true: true, substitution: {?ty_2 => !ty_1} }, } "#]]); } diff --git a/crates/formality-prove/src/test/eq_partial_eq.rs b/crates/formality-prove/src/test/eq_partial_eq.rs index 7216d505..c9267bf2 100644 --- a/crates/formality-prove/src/test/eq_partial_eq.rs +++ b/crates/formality-prove/src/test/eq_partial_eq.rs @@ -29,6 +29,7 @@ fn eq_implies_partial_eq() { env: Env { variables: [], bias: Soundness, + pending: [], }, known_true: true, substitution: {}, @@ -44,19 +45,19 @@ fn not_partial_eq_implies_eq() { prove(decls(), (), (), goal) .assert_err( expect![[r#" - judgment `prove { goal: {for if {PartialEq(^ty0_0)} Eq(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {for if {PartialEq(^ty0_0)} Eq(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {for if {PartialEq(^ty0_0)} Eq(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {for if {PartialEq(^ty0_0)} Eq(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for if {PartialEq(^ty0_0)} Eq(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: for if {PartialEq(^ty0_0)} Eq(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: if {PartialEq(!ty_1)} Eq(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: if {PartialEq(!ty_1)} Eq(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "implies" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Eq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: Eq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "assumption - predicate" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], bias: Soundness } }` + judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], bias: Soundness, pending: [] } }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1, ?ty_2], bias: Soundness } }`"#]]); + judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [] } }`"#]]); } #[test] @@ -65,49 +66,49 @@ fn universals_not_eq() { prove(decls(), (), (), goal) .assert_err( expect![[r#" - judgment `prove { goal: {for if {Eq(^ty0_0)} PartialEq(^ty0_1)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {for if {Eq(^ty0_0)} PartialEq(^ty0_1)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {for if {Eq(^ty0_0)} PartialEq(^ty0_1)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {for if {Eq(^ty0_0)} PartialEq(^ty0_1)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for if {Eq(^ty0_0)} PartialEq(^ty0_1), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: for if {Eq(^ty0_0)} PartialEq(^ty0_1), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: if {Eq(!ty_1)} PartialEq(!ty_2), assumptions: {}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: if {Eq(!ty_1)} PartialEq(!ty_2), assumptions: {}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "implies" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: PartialEq(!ty_2), assumptions: {Eq(!ty_1)}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: PartialEq(!ty_2), assumptions: {Eq(!ty_1)}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "assumption - predicate" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: PartialEq(!ty_2), via: Eq(!ty_1), assumptions: {Eq(!ty_1)}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness } }` + judgment had no applicable rules: `prove_via { goal: PartialEq(!ty_2), via: Eq(!ty_1), assumptions: {Eq(!ty_1)}, env: Env { variables: [!ty_1, !ty_2], bias: Soundness, pending: [] } }` the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, !ty_2, ?ty_3], bias: Soundness }, known_true: true, substitution: {?ty_3 => !ty_2} }, goal: {Eq(?ty_3)}, assumptions: {Eq(!ty_1)} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, !ty_2, ?ty_3], bias: Soundness, pending: [] }, known_true: true, substitution: {?ty_3 => !ty_2} }, goal: {Eq(?ty_3)}, assumptions: {Eq(!ty_1)} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Eq(!ty_1)}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Eq(!ty_1), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: Eq(!ty_1), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "assumption - predicate" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_via { goal: Eq(!ty_1), via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_via { goal: Eq(!ty_1), via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "predicate-congruence-axiom" failed at step #3 (src/file.rs:LL:CC) because - judgment `prove { goal: {!ty_0 = !ty_1}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {!ty_0 = !ty_1}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] }, decls: decls(222, [trait Eq where {PartialEq(^ty0_0)}, trait PartialEq ], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {!ty_0 = !ty_1}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {!ty_0 = !ty_1}, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: !ty_0 = !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: !ty_0 = !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "assumption - relation" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: !ty_0 = !ty_1, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` + judgment had no applicable rules: `prove_via { goal: !ty_0 = !ty_1, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] } }` the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: !ty_0, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_normalize { p: !ty_0, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` + judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] } }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_1, b: !ty_0, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: !ty_1, b: !ty_0, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_normalize { p: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: !ty_1, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` + judgment had no applicable rules: `prove_normalize_via { goal: !ty_1, via: Eq(!ty_0), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] } }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness } }` + cyclic proof attempt: `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], bias: Soundness, pending: [] } }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], bias: Soundness } }`"#]]); + judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], bias: Soundness, pending: [] } }`"#]]); } diff --git a/crates/formality-prove/src/test/exists_constraints.rs b/crates/formality-prove/src/test/exists_constraints.rs index 17c71fab..465bfcd5 100644 --- a/crates/formality-prove/src/test/exists_constraints.rs +++ b/crates/formality-prove/src/test/exists_constraints.rs @@ -20,7 +20,7 @@ fn decls() -> Decls { fn exists_u_for_t() { test_prove(decls(), term("exists {} => {Foo(U)}")).assert_ok(expect![[r#" { - Constraints { env: Env { variables: [?ty_2, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => Vec} }, + Constraints { env: Env { variables: [?ty_2, ?ty_1], bias: Soundness, pending: [] }, known_true: true, substitution: {?ty_1 => Vec} }, } "#]]); } diff --git a/crates/formality-prove/src/test/expanding.rs b/crates/formality-prove/src/test/expanding.rs index 4c3426ea..4439cc82 100644 --- a/crates/formality-prove/src/test/expanding.rs +++ b/crates/formality-prove/src/test/expanding.rs @@ -19,7 +19,7 @@ fn decls() -> Decls { fn expanding() { test_prove(decls(), term("exists {} => {Debug(T)}")).assert_ok(expect![[r#" { - Constraints { env: Env { variables: [?ty_0], bias: Soundness }, known_true: false, substitution: {} }, + Constraints { env: Env { variables: [?ty_0], bias: Soundness, pending: [] }, known_true: false, substitution: {} }, } "#]]); } diff --git a/crates/formality-prove/src/test/is_local.rs b/crates/formality-prove/src/test/is_local.rs index ed56bbcf..9108b76b 100644 --- a/crates/formality-prove/src/test/is_local.rs +++ b/crates/formality-prove/src/test/is_local.rs @@ -13,15 +13,15 @@ fn test_forall_not_local() { term("{} => {for @IsLocal(Debug(T))}"), ).assert_err( expect![[r#" - judgment `prove { goal: {for @ IsLocal(Debug(^ty0_0))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {for @ IsLocal(Debug(^ty0_0))}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {for @ IsLocal(Debug(^ty0_0))}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {for @ IsLocal(Debug(^ty0_0))}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for @ IsLocal(Debug(^ty0_0)), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: for @ IsLocal(Debug(^ty0_0)), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ IsLocal(Debug(!ty_1)), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: @ IsLocal(Debug(!ty_1)), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because - judgment `is_local_trait_ref { goal: Debug(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `is_local_trait_ref { goal: Debug(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` decls = decls(222, [], [], [], [], [], [], {}, {}) @@ -36,7 +36,7 @@ fn test_exists_not_local() { ) .assert_ok(expect![[r#" { - Constraints { env: Env { variables: [?ty_1], bias: Soundness }, known_true: false, substitution: {} }, + Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [] }, known_true: false, substitution: {} }, } "#]]) } diff --git a/crates/formality-prove/src/test/magic_copy.rs b/crates/formality-prove/src/test/magic_copy.rs index 4ab17a3c..96eb9b8f 100644 --- a/crates/formality-prove/src/test/magic_copy.rs +++ b/crates/formality-prove/src/test/magic_copy.rs @@ -25,140 +25,140 @@ fn decls() -> Decls { fn all_t_not_magic() { test_prove(decls(), term("{} => {for Magic(T)}")).assert_err( expect![[r#" - judgment `prove { goal: {for Magic(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {for Magic(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {for Magic(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {for Magic(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for Magic(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: for Magic(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Magic(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: Magic(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "positive impl" failed at step #7 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {Copy(?ty_2)}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [] }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {Copy(?ty_2)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Copy(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: Copy(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "positive impl" failed at step #5 (src/file.rs:LL:CC) because - judgment `prove { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "assumption - relation" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_normalize { p: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_normalize { p: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + judgment had no applicable rules: `prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness, pending: [] }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "positive impl" failed at step #7 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness, pending: [] }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` + cyclic proof attempt: `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness } }` + judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness, pending: [] } }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Magic(!ty_1), via: Copy(?ty_2), assumptions: {}, env: Env { variables: [!ty_1, ?ty_2], bias: Soundness } }`"#]]); + judgment had no applicable rules: `prove_via { goal: Magic(!ty_1), via: Copy(?ty_2), assumptions: {}, env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [] } }`"#]]); } #[test] fn all_t_not_copy() { test_prove(decls(), term("{} => {for Copy(T)}")).assert_err( expect![[r#" - judgment `prove { goal: {for Copy(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {for Copy(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {for Copy(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {for Copy(^ty0_0)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for Copy(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: for Copy(^ty0_0), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Copy(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: Copy(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "positive impl" failed at step #5 (src/file.rs:LL:CC) because - judgment `prove { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "assumption - relation" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_normalize { p: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_normalize { p: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + judgment had no applicable rules: `prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {Magic(?ty_2)}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [] }, known_true: true, substitution: {?ty_2 => !ty_1} }, goal: {Magic(?ty_2)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: Magic(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "positive impl" failed at step #7 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness, pending: [] }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Copy(?ty_1)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Copy(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Copy(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: Copy(!ty_0), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "positive impl" failed at step #5 (src/file.rs:LL:CC) because - judgment `prove { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {!ty_0 = u32}, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: !ty_0 = u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "assumption - relation" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + judgment had no applicable rules: `prove_via { goal: !ty_0 = u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_normalize { p: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + judgment had no applicable rules: `prove_normalize_via { goal: !ty_0, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: u32, b: !ty_0, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_normalize { p: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + judgment had no applicable rules: `prove_normalize_via { goal: u32, via: Copy(!ty_0), assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` + cyclic proof attempt: `prove_eq { a: !ty_0, b: u32, assumptions: {Copy(!ty_0)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` the rule "trait implied bound" failed at step #4 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0, ?ty_1], bias: Soundness, pending: [] }, known_true: true, substitution: {?ty_1 => !ty_0} }, goal: {Magic(?ty_1)}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Copy , trait Magic where {Copy(^ty0_0)}], [impl Magic(^ty0_0) where {Magic(^ty0_0)}, impl Copy(u32)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness } }` + cyclic proof attempt: `prove_wc_list { goal: {Magic(!ty_0)}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] } }` the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness } }`"#]]); + judgment had no applicable rules: `prove_via { goal: Magic(!ty_0), via: Copy(?ty_1), assumptions: {}, env: Env { variables: [!ty_0, ?ty_1], bias: Soundness, pending: [] } }`"#]]); } diff --git a/crates/formality-prove/src/test/occurs_check.rs b/crates/formality-prove/src/test/occurs_check.rs index 5b9012aa..9454ac82 100644 --- a/crates/formality-prove/src/test/occurs_check.rs +++ b/crates/formality-prove/src/test/occurs_check.rs @@ -20,15 +20,15 @@ fn decls() -> Decls { fn direct_cycle() { test_prove(decls(), term("exists {} => {A = Vec}")).assert_err( expect![[r#" - judgment `prove { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: ?ty_0 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: ?ty_0 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because judgment `equate_variable` failed at the following rule(s): failed at (src/file.rs:LL:CC) because @@ -40,7 +40,7 @@ fn direct_cycle() { fn eq_variable_to_rigid() { test_prove(decls(), term("exists {} => {X = Vec}")).assert_ok(expect![[r#" { - Constraints { env: Env { variables: [?ty_3, ?ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_1 => Vec, ?ty_2 => ?ty_3} }, + Constraints { env: Env { variables: [?ty_3, ?ty_1, ?ty_2], bias: Soundness, pending: [] }, known_true: true, substitution: {?ty_1 => Vec, ?ty_2 => ?ty_3} }, } "#]]); } @@ -50,7 +50,7 @@ fn eq_variable_to_rigid() { fn eq_rigid_to_variable() { test_prove(decls(), term("exists {} => {Vec = X}")).assert_ok(expect![[r#" { - Constraints { env: Env { variables: [?ty_3, ?ty_1, ?ty_2], bias: Soundness }, known_true: true, substitution: {?ty_1 => Vec, ?ty_2 => ?ty_3} }, + Constraints { env: Env { variables: [?ty_3, ?ty_1, ?ty_2], bias: Soundness, pending: [] }, known_true: true, substitution: {?ty_1 => Vec, ?ty_2 => ?ty_3} }, } "#]]); } @@ -63,21 +63,21 @@ fn indirect_cycle_1() { term("exists {} => {A = Vec, B = A}"), ).assert_err( expect![[r#" - judgment `prove { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_2, ?ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_0 => Vec, ?ty_1 => ?ty_2} }, goal: {?ty_1 = ?ty_0}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_2, ?ty_0, ?ty_1], bias: Soundness, pending: [] }, known_true: true, substitution: {?ty_0 => Vec, ?ty_1 => ?ty_2} }, goal: {?ty_1 = ?ty_0}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: ?ty_0 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: ?ty_0 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because judgment `equate_variable` failed at the following rule(s): failed at (src/file.rs:LL:CC) because @@ -92,21 +92,21 @@ fn indirect_cycle_2() { term("exists {} => {B = A, A = Vec}"), ).assert_err( expect![[r#" - judgment `prove { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {?ty_0 = Vec, ?ty_1 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0, ?ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_2, ?ty_0, ?ty_1], bias: Soundness }, known_true: true, substitution: {?ty_0 => Vec, ?ty_1 => ?ty_2} }, goal: {?ty_1 = ?ty_0}, assumptions: {} }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [?ty_2, ?ty_0, ?ty_1], bias: Soundness, pending: [] }, known_true: true, substitution: {?ty_0 => Vec, ?ty_1 => ?ty_2} }, goal: {?ty_1 = ?ty_0}, assumptions: {} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo ], [impl Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {?ty_0 = Vec}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: ?ty_0 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: ?ty_0 = Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_0, b: Vec, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #1 (src/file.rs:LL:CC) because judgment `equate_variable` failed at the following rule(s): failed at (src/file.rs:LL:CC) because diff --git a/crates/formality-prove/src/test/simple_impl.rs b/crates/formality-prove/src/test/simple_impl.rs index 3c2a66a0..8445aa1b 100644 --- a/crates/formality-prove/src/test/simple_impl.rs +++ b/crates/formality-prove/src/test/simple_impl.rs @@ -22,7 +22,7 @@ fn vec_u32_debug() { let goal: Wc = term("Debug(Vec)"); prove(decls(), (), (), goal).assert_ok(expect![[r#" { - Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, + Constraints { env: Env { variables: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }, } "#]]); } @@ -32,7 +32,7 @@ fn vec_vec_u32_debug() { let goal: Wc = term("Debug(Vec>)"); prove(decls(), (), (), goal).assert_ok(expect![[r#" { - Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, + Constraints { env: Env { variables: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }, } "#]]); } diff --git a/crates/formality-prove/src/test/universes.rs b/crates/formality-prove/src/test/universes.rs index 2686ff03..866acf95 100644 --- a/crates/formality-prove/src/test/universes.rs +++ b/crates/formality-prove/src/test/universes.rs @@ -12,19 +12,19 @@ fn exists_u_for_t() { let decls = Decls::empty(); test_prove(decls, term("exists {} => {for T = U}")).assert_err( expect![[r#" - judgment `prove { goal: {for ^ty0_0 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {for ^ty0_0 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {for ^ty0_0 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc_list { goal: {for ^ty0_0 = ?ty_0}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for ^ty0_0 = ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: for ^ty0_0 = ?ty_0, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: !ty_1 = ?ty_0, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_wc { goal: !ty_1 = ?ty_0, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: !ty_1, b: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: !ty_1, b: ?ty_0, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: ?ty_0, b: !ty_1, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_eq { a: ?ty_0, b: !ty_1, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness } }` failed at the following rule(s): + judgment `prove_existential_var_eq { v: ?ty_0, b: !ty_1, assumptions: {}, env: Env { variables: [?ty_0, !ty_1], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "existential-nonvar" failed at step #0 (src/file.rs:LL:CC) because pattern `None` did not match value `Some(!ty_1)` the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because @@ -42,7 +42,7 @@ fn for_t_exists_u() { test_prove(decls, term("{} => {for Test(T, T)}")).assert_ok(expect![[r#" { - Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }, + Constraints { env: Env { variables: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }, } "#]]); } diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs index 63764ce8..57114cfa 100644 --- a/crates/formality-rust/src/grammar/minirust.rs +++ b/crates/formality-rust/src/grammar/minirust.rs @@ -1,6 +1,6 @@ use formality_core::{id, UpcastFrom}; use formality_macros::term; -use formality_types::grammar::{Parameter, RigidName, ScalarId, Ty, TyData}; +use formality_types::grammar::{Parameter, ScalarId, Ty}; use crate::grammar::minirust::ConstTypePair::*; use crate::grammar::FnId; @@ -198,30 +198,6 @@ impl ConstTypePair { } } -pub fn ty_is_int(ty: Ty) -> bool { - // integer is rigidty - let TyData::RigidTy(rigid_ty) = ty.data() else { - return false; - }; - let RigidName::ScalarId(ref scalar_id) = rigid_ty.name else { - return false; - }; - - match scalar_id { - ScalarId::U8 - | ScalarId::U16 - | ScalarId::U32 - | ScalarId::U64 - | ScalarId::I8 - | ScalarId::I16 - | ScalarId::I32 - | ScalarId::I64 - | ScalarId::Usize - | ScalarId::Isize => true, - ScalarId::Bool => false, - } -} - #[term] pub enum PlaceExpression { #[grammar(local($v0))] diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index d9522c21..4e49436c 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -101,6 +101,7 @@ pub enum Skeleton { Equals, Sub, Outlives, + IsInt, } impl Predicate { diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs index 8284e10e..ed7292a3 100644 --- a/crates/formality-types/src/grammar/ty.rs +++ b/crates/formality-types/src/grammar/ty.rs @@ -40,10 +40,6 @@ impl Ty { } } - pub fn is_rigid(&self) -> bool { - matches!(self.data(), TyData::RigidTy(_)) - } - pub fn rigid(name: impl Upcast, parameters: impl Upcast>) -> Self { RigidTy { name: name.upcast(), @@ -189,6 +185,24 @@ pub enum ScalarId { Isize, } +impl ScalarId { + pub fn is_int(&self) -> bool { + match self { + ScalarId::U8 + | ScalarId::U16 + | ScalarId::U32 + | ScalarId::U64 + | ScalarId::I8 + | ScalarId::I16 + | ScalarId::I32 + | ScalarId::I64 + | ScalarId::Usize + | ScalarId::Isize => true, + ScalarId::Bool => false, + } + } +} + #[term((alias $name $*parameters))] #[customize(parse, debug)] pub struct AliasTy { diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs index 0ad8ce3a..40f8016d 100644 --- a/src/test/mir_fn_bodies.rs +++ b/src/test/mir_fn_bodies.rs @@ -657,6 +657,10 @@ fn test_invalid_value_in_switch_terminator() { } ] [] - expect_test::expect!["The value used for switch must be an int."] + expect_test::expect![[r#" + judgment `ty_is_int { assumptions: {}, ty: bool, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): + the rule "rigid_ty is int" failed at step #0 (src/file.rs:LL:CC) because + condition evaluted to false: `id.is_int()` + id = bool"#]] ) }