From bce8290ecf1434983a65e73c13e0c357ea80a638 Mon Sep 17 00:00:00 2001 From: tiif Date: Wed, 30 Jul 2025 16:45:01 +0200 Subject: [PATCH 1/9] Support StorageLive and StorageDead --- crates/formality-check/src/mini_rust_check.rs | 39 ++++++++-- crates/formality-rust/src/grammar/minirust.rs | 6 +- src/test/mir_fn_bodies.rs | 77 +++++++++++++++++++ 3 files changed, 115 insertions(+), 7 deletions(-) diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs index 3baf715b..cbd2da34 100644 --- a/crates/formality-check/src/mini_rust_check.rs +++ b/crates/formality-check/src/mini_rust_check.rs @@ -94,6 +94,7 @@ impl Check<'_> { declared_input_tys, callee_input_tys: Map::new(), crate_id: crate_id.clone(), + fn_args: body.args.clone(), }; // (4) Check statements in body are valid @@ -150,6 +151,24 @@ impl Check<'_> { self.check_place(typeck_env, place_expression)?; // FIXME: check that access the place is allowed per borrowck rules } + minirust::Statement::StorageLive(local_id) => { + // FIXME: We need more checks here after loan is introduced. + if self.find_local_id(&typeck_env, local_id).is_none() { + bail!("Statement::StorageLive: invalid local variable") + } + } + minirust::Statement::StorageDead(local_id) => { + // FIXME: We need more checks here after loan is introduced. + let Some((local_id, _)) = self.find_local_id(&typeck_env, local_id) else { + bail!("Statement::StorageDead: invalid local variable") + }; + // Make sure function arguments and return place are not marked as dead. + if local_id == typeck_env.ret_id + || typeck_env.fn_args.iter().any(|fn_arg| local_id == *fn_arg) + { + bail!("Statement::StorageDead: trying to mark function arguments or return local as dead") + } + } } Ok(()) } @@ -249,11 +268,7 @@ impl Check<'_> { match place { Local(local_id) => { // Check if place id is a valid local id. - let Some((_, ty)) = env - .local_variables - .iter() - .find(|(declared_local_id, _)| *declared_local_id == local_id) - else { + let Some((_, ty)) = self.find_local_id(env, local_id) else { bail!( "PlaceExpression::Local: unknown local name `{:?}`", local_id @@ -265,6 +280,17 @@ impl Check<'_> { Ok(place_ty.clone()) } + fn find_local_id(&self, env: &TypeckEnv, local_id: &LocalId) -> Option<(LocalId, Ty)> { + if let Some((local_id, ty)) = env + .local_variables + .iter() + .find(|(declared_local_id, _)| *declared_local_id == local_id) + { + return Some((local_id.clone(), ty.clone())); + } + return None; + } + // Check if the value expression is well-formed, and return the type of the value expression. fn check_value(&self, typeck_env: &mut TypeckEnv, value: &ValueExpression) -> Fallible { let value_ty; @@ -373,4 +399,7 @@ struct TypeckEnv { /// We need this to access information about other functions /// declared in the current crate. crate_id: CrateId, + + /// LocalId of function argument. + fn_args: Vec, } diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs index 63764ce8..6756a714 100644 --- a/crates/formality-rust/src/grammar/minirust.rs +++ b/crates/formality-rust/src/grammar/minirust.rs @@ -71,8 +71,10 @@ pub enum Statement { // SetDiscriminant // Validate // Deinit - // StorageLive - // StorageDead + #[grammar(StorageLive($v0);)] + StorageLive(LocalId), + #[grammar(StorageDead($v0);)] + StorageDead(LocalId), } /// Based on [MiniRust terminators](https://github.com/minirust/minirust/blob/9ae11cc202d040f08bc13ec5254d3d41d5f3cc25/spec/lang/syntax.md#statements-terminators). diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs index 0ad8ce3a..b0c0d0f8 100644 --- a/src/test/mir_fn_bodies.rs +++ b/src/test/mir_fn_bodies.rs @@ -227,6 +227,33 @@ fn test_place_mention_statement() { ) } +/// Test valid StorageLive and StorageDead statements. +#[test] +fn test_storage_live_dead() { + crate::assert_ok!( + [ + crate Foo { + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + let v2: u32; + + bb0: { + statements { + local(v0) = load(local(v1)); + StorageLive(v2); + StorageDead(v2); + } + return; + } + + }; + } + ] + expect_test::expect![["()"]] + ) +} + // Test what will happen if the next block does not exist for Terminator::Call. #[test] fn test_no_next_bb_for_call_terminator() { @@ -660,3 +687,53 @@ fn test_invalid_value_in_switch_terminator() { expect_test::expect!["The value used for switch must be an int."] ) } + +/// Test the behaviour of having return place in StorageDead. +#[test] +fn test_ret_place_storage_dead() { + crate::assert_err!( + [ + crate Foo { + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements { + StorageDead(v1); + } + return; + } + + }; + } + ] + [] + expect_test::expect!["Statement::StorageDead: trying to mark function arguments or return local as dead"] + ) +} + +/// Test the behaviour of having function argument in StorageDead. +#[test] +fn test_fn_arg_storage_dead() { + crate::assert_err!( + [ + crate Foo { + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + + bb0: { + statements { + StorageDead(v0); + } + return; + } + + }; + } + ] + [] + expect_test::expect!["Statement::StorageDead: trying to mark function arguments or return local as dead"] + ) +} From bc5cb39fc14186623c1b82b33cd8aaf092478fd4 Mon Sep 17 00:00:00 2001 From: tiif Date: Thu, 31 Jul 2025 11:19:10 +0200 Subject: [PATCH 2/9] Add support for struct and field projection --- crates/formality-check/src/mini_rust_check.rs | 118 +++++++++++++++- crates/formality-rust/src/grammar/minirust.rs | 22 ++- src/test/mir_fn_bodies.rs | 126 ++++++++++++++++++ 3 files changed, 258 insertions(+), 8 deletions(-) diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs index cbd2da34..4b97eb0e 100644 --- a/crates/formality-check/src/mini_rust_check.rs +++ b/crates/formality-check/src/mini_rust_check.rs @@ -3,15 +3,15 @@ use std::iter::zip; use formality_core::{Fallible, Map, Upcast}; use formality_prove::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::PlaceExpression::*; +use formality_rust::grammar::minirust::ValueExpression::{Constant, Fn, Load, Struct}; use formality_rust::grammar::minirust::{ self, ty_is_int, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression, }; -use formality_rust::grammar::FnBoundData; -use formality_types::grammar::{CrateId, FnId}; -use formality_types::grammar::{Relation, Ty, Wcs}; +use formality_rust::grammar::{FnBoundData, StructBoundData}; +use formality_types::grammar::{AdtId, Relation, Ty, TyData, Wcs}; +use formality_types::grammar::{CrateId, FnId, RigidName}; use crate::{Check, CrateItem}; use anyhow::bail; @@ -95,6 +95,7 @@ impl Check<'_> { callee_input_tys: Map::new(), crate_id: crate_id.clone(), fn_args: body.args.clone(), + adt_tys: Map::new(), }; // (4) Check statements in body are valid @@ -276,6 +277,38 @@ impl Check<'_> { }; place_ty = ty; } + Field(field_projection) => { + let Local(ref local_id) = *field_projection.root else { + bail!("Only Local is allowed as the root of FieldProjection") + }; + + // Check if the index is valid for the tuple. + // FIXME: use let chain here? + + let Some(ty) = env.local_variables.get(&local_id) else { + bail!("The local id used in PlaceExpression::Field is invalid.") + }; + + // Get the ADT type information. + let TyData::RigidTy(rigid_ty) = ty.data() else { + bail!("The type for field projection must be rigid ty") + }; + + // FIXME: it'd be nice to have the field information in ty data + let RigidName::AdtId(ref adt_id) = rigid_ty.name else { + bail!("The type for field projection must be adt") + }; + + let Some(tys) = env.adt_tys.get(&adt_id) else { + bail!("The ADT used is invalid.") + }; + + if field_projection.index >= tys.len() { + bail!("The field index used in PlaceExpression::Field is invalid.") + } + + place_ty = tys[field_projection.index].clone(); + } } Ok(place_ty.clone()) } @@ -317,6 +350,7 @@ impl Check<'_> { if fn_declared.id == *fn_id { let fn_bound_data = typeck_env.env.instantiate_universally(&fn_declared.binder); + // FIXME: maybe we should store the information somewhere else, like in the value expression? // Store the callee information in typeck_env, we will need this when type checking Terminator::Call. typeck_env .callee_input_tys @@ -341,6 +375,77 @@ impl Check<'_> { // it will be rejected by the parser. Ok(constant.get_ty()) } + Struct(value_expressions, ty) => { + let mut struct_field_ty = Vec::new(); + + // Check if the adt type is valid in current crate. + if let TyData::RigidTy(rigid_ty) = ty.data() { + if let RigidName::AdtId(adt_id) = &rigid_ty.name { + // Find the crate that is currently being typeck. + let curr_crate = self + .program + .crates + .iter() + .find(|c| c.id == typeck_env.crate_id) + .unwrap(); + + // Find the struct from current crate. + let target_struct = curr_crate.items.iter().find(|item| { + match item { + CrateItem::Struct(struct_item) => { + if struct_item.id == *adt_id { + // Get the ty data of the field. + let ( + _, + StructBoundData { + where_clauses: _, + fields, + }, + ) = struct_item.binder.open(); + for field in fields { + struct_field_ty.push(field.ty); + } + return true; + } + false + } + _ => false, + } + }); + + if target_struct.is_none() { + bail!("The type used in Tuple is not declared in current crate") + } + // We will need the adt type information when type checking field projection. + typeck_env + .adt_tys + .insert(adt_id.clone(), struct_field_ty.clone()); + } + } + + // Make sure the length of value expression matches the length of field of adt. + if value_expressions.len() != struct_field_ty.len() { + bail!("The length of ValueExpression::Tuple does not match the type of the ADT declared") + } + + let expression_ty_pair = zip(value_expressions, struct_field_ty); + + // FIXME: we only support const in value expression of tuple for now, we can add support + // more in future. + + for (value_expression, declared_ty) in expression_ty_pair { + let Constant(_) = value_expression else { + bail!("Only Constant is supported in ValueExpression::Tuple for now.") + }; + let ty = self.check_value(typeck_env, value_expression)?; + + // Make sure the type matches the declared adt. + if ty != declared_ty { + bail!("The type in ValueExpression::Tuple does not match the ADT declared") + } + } + Ok(ty.clone()) + } } } @@ -402,4 +507,7 @@ struct TypeckEnv { /// LocalId of function argument. fn_args: Vec, + + /// Type information of adt + adt_tys: Map>, } diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs index 6756a714..73cfde7a 100644 --- a/crates/formality-rust/src/grammar/minirust.rs +++ b/crates/formality-rust/src/grammar/minirust.rs @@ -5,10 +5,13 @@ use formality_types::grammar::{Parameter, RigidName, ScalarId, Ty, TyData}; use crate::grammar::minirust::ConstTypePair::*; use crate::grammar::FnId; +use std::sync::Arc; + // This definition is based on [MiniRust](https://github.com/minirust/minirust/blob/master/spec/lang/syntax.md). id!(BbId); id!(LocalId); +id!(FieldId); // Example: // @@ -138,8 +141,11 @@ pub enum ValueExpression { Constant(ConstTypePair), #[grammar(fn_id $v0)] Fn(FnId), - // #[grammar($(v0) as $v1)] - // Tuple(Vec, Ty), + // FIXME: minirust uses typle to represent arrays, structs, tuples (including unit). + // But I think it will be quite annoying to do typecking when we have all these types + // together, so I added a variant just for struct. + #[grammar(struct ${v0} as $v1)] // FIXME: use comma separated + Struct(Vec, Ty), // Union // Variant // GetDiscriminant @@ -229,7 +235,17 @@ pub enum PlaceExpression { #[grammar(local($v0))] Local(LocalId), // Deref(Arc), - // Field(Arc, FieldId), + // Project to a field. + #[grammar($v0)] + Field(FieldProjection), // Index // Downcast } + +#[term($root.$index)] +pub struct FieldProjection { + /// The place to base the projection on. + pub root: Arc, + /// The field to project to. + pub index: usize, +} diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs index b0c0d0f8..c1597a6e 100644 --- a/src/test/mir_fn_bodies.rs +++ b/src/test/mir_fn_bodies.rs @@ -254,6 +254,37 @@ fn test_storage_live_dead() { ) } +/// Test valid program that uses struct. +#[test] +fn test_struct() { + crate::assert_ok!( + [ + crate Foo { + struct Dummy { + value: u32, + } + + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + let v2: Dummy; + + bb0: { + statements { + local(v0) = load(local(v1)); + local(v2) = struct { constant(1: u32) } as Dummy; + local(v2).0 = constant(2: u32); + } + return; + } + + }; + } + ] + expect_test::expect![["()"]] + ) +} + // Test what will happen if the next block does not exist for Terminator::Call. #[test] fn test_no_next_bb_for_call_terminator() { @@ -737,3 +768,98 @@ fn test_fn_arg_storage_dead() { expect_test::expect!["Statement::StorageDead: trying to mark function arguments or return local as dead"] ) } + +/// Test the behaviour of using invalid index for the struct field. +#[test] +fn test_invalid_struct_field() { + crate::assert_err!( + [ + crate Foo { + struct Dummy { + value: u32, + } + + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + let v2: Dummy; + + bb0: { + statements { + local(v0) = load(local(v1)); + local(v2) = struct { constant(1: u32) } as Dummy; + local(v2).1 = constant(2: u32); + } + return; + } + + }; + } + ] + [] + expect_test::expect!["The field index used in PlaceExpression::Field is invalid."] + ) +} + +/// Test the behaviour of using non-adt local for field projection. +#[test] +fn test_field_projection_root_non_adt() { + crate::assert_err!( + [ + crate Foo { + struct Dummy { + value: u32, + } + + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + let v2: Dummy; + + bb0: { + statements { + local(v0) = load(local(v1)); + local(v2) = struct { constant(1: u32) } as Dummy; + local(v1).1 = constant(2: u32); + } + return; + } + + }; + } + ] + [] + expect_test::expect!["The type for field projection must be adt"] + ) +} + +/// Test the behaviour of initialising the struct with wrong type. +#[test] +fn test_struct_wrong_type_in_initialisation() { + crate::assert_err!( + [ + crate Foo { + struct Dummy { + value: u32, + } + + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + let v2: Dummy; + + bb0: { + statements { + local(v0) = load(local(v1)); + local(v2) = struct { constant(false) } as Dummy; + } + return; + } + + }; + } + ] + [] + expect_test::expect!["The type in ValueExpression::Tuple does not match the ADT declared"] + ) +} From 9ab10894cc36a40c79932e237b9beba3ce63ecd0 Mon Sep 17 00:00:00 2001 From: tiif Date: Mon, 4 Aug 2025 10:36:06 +0200 Subject: [PATCH 3/9] UPDATE_EXPECT=1 for all the tests --- .../src/prove/minimize/test.rs | 5 +- crates/formality-prove/src/test/adt_wf.rs | 17 +-- .../src/test/eq_assumptions.rs | 122 ++++++++-------- .../formality-prove/src/test/eq_partial_eq.rs | 61 ++++---- .../src/test/exists_constraints.rs | 2 +- crates/formality-prove/src/test/expanding.rs | 2 +- crates/formality-prove/src/test/is_local.rs | 12 +- crates/formality-prove/src/test/magic_copy.rs | 132 +++++++++--------- .../formality-prove/src/test/occurs_check.rs | 46 +++--- .../formality-prove/src/test/simple_impl.rs | 4 +- crates/formality-prove/src/test/universes.rs | 16 +-- 11 files changed, 211 insertions(+), 208 deletions(-) diff --git a/crates/formality-prove/src/prove/minimize/test.rs b/crates/formality-prove/src/prove/minimize/test.rs index 8f55e46b..9340a5b9 100644 --- a/crates/formality-prove/src/prove/minimize/test.rs +++ b/crates/formality-prove/src/prove/minimize/test.rs @@ -17,12 +17,12 @@ 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])"] + 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 +51,7 @@ fn minimize_a() { ?ty_3, ], bias: Soundness, + pending: [], }, known_true: true, substitution: { 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: {} }, } "#]]); } From a978bbee93328f8e19aa8229c18092b1992ac7bf Mon Sep 17 00:00:00 2001 From: tiif Date: Mon, 4 Aug 2025 10:37:01 +0200 Subject: [PATCH 4/9] fmt --- crates/formality-prove/src/prove/minimize/test.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/crates/formality-prove/src/prove/minimize/test.rs b/crates/formality-prove/src/prove/minimize/test.rs index 9340a5b9..e50fc86c 100644 --- a/crates/formality-prove/src/prove/minimize/test.rs +++ b/crates/formality-prove/src/prove/minimize/test.rs @@ -17,8 +17,10 @@ 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, pending: [] }, [?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); From bffdf5a4de4747a5e16752deb43d208f7e515896 Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 5 Aug 2025 14:56:36 +0200 Subject: [PATCH 5/9] get field information from decl instead of crate item --- crates/formality-check/src/mini_rust_check.rs | 94 ++++++++----------- crates/formality-prove/src/decls.rs | 30 +++++- crates/formality-rust/src/grammar.rs | 42 +++++++-- crates/formality-rust/src/prove.rs | 6 +- crates/formality-types/src/grammar/ids.rs | 8 ++ 5 files changed, 111 insertions(+), 69 deletions(-) diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs index 4b97eb0e..211cbc7f 100644 --- a/crates/formality-check/src/mini_rust_check.rs +++ b/crates/formality-check/src/mini_rust_check.rs @@ -1,7 +1,7 @@ use std::iter::zip; use formality_core::{Fallible, Map, Upcast}; -use formality_prove::Env; +use formality_prove::{AdtDeclBoundData, AdtDeclVariant, Env}; use formality_rust::grammar::minirust::ArgumentExpression::{ByValue, InPlace}; use formality_rust::grammar::minirust::PlaceExpression::*; use formality_rust::grammar::minirust::ValueExpression::{Constant, Fn, Load, Struct}; @@ -9,9 +9,9 @@ use formality_rust::grammar::minirust::{ self, ty_is_int, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression, }; -use formality_rust::grammar::{FnBoundData, StructBoundData}; -use formality_types::grammar::{AdtId, Relation, Ty, TyData, Wcs}; +use formality_rust::grammar::FnBoundData; use formality_types::grammar::{CrateId, FnId, RigidName}; +use formality_types::grammar::{Relation, Ty, TyData, VariantId, Wcs}; use crate::{Check, CrateItem}; use anyhow::bail; @@ -95,7 +95,6 @@ impl Check<'_> { callee_input_tys: Map::new(), crate_id: crate_id.clone(), fn_args: body.args.clone(), - adt_tys: Map::new(), }; // (4) Check statements in body are valid @@ -294,20 +293,30 @@ impl Check<'_> { bail!("The type for field projection must be rigid ty") }; - // FIXME: it'd be nice to have the field information in ty data + // FIXME: directly get the adt_id information from ty + let RigidName::AdtId(ref adt_id) = rigid_ty.name else { bail!("The type for field projection must be adt") }; - let Some(tys) = env.adt_tys.get(&adt_id) else { - bail!("The ADT used is invalid.") - }; + let ( + _, + AdtDeclBoundData { + where_clause: _, + variants, + }, + ) = self.decls.adt_decl(&adt_id).binder.open(); + let AdtDeclVariant { name, fields } = variants.last().unwrap(); + + if *name != VariantId::for_struct() { + bail!("The local used for field projection must be struct.") + } - if field_projection.index >= tys.len() { + if field_projection.index >= fields.len() { bail!("The field index used in PlaceExpression::Field is invalid.") } - place_ty = tys[field_projection.index].clone(); + place_ty = fields[field_projection.index].ty.clone(); } } Ok(place_ty.clone()) @@ -378,70 +387,46 @@ impl Check<'_> { Struct(value_expressions, ty) => { let mut struct_field_ty = Vec::new(); - // Check if the adt type is valid in current crate. + // Check the validity of the struct. if let TyData::RigidTy(rigid_ty) = ty.data() { if let RigidName::AdtId(adt_id) = &rigid_ty.name { - // Find the crate that is currently being typeck. - let curr_crate = self - .program - .crates - .iter() - .find(|c| c.id == typeck_env.crate_id) - .unwrap(); - - // Find the struct from current crate. - let target_struct = curr_crate.items.iter().find(|item| { - match item { - CrateItem::Struct(struct_item) => { - if struct_item.id == *adt_id { - // Get the ty data of the field. - let ( - _, - StructBoundData { - where_clauses: _, - fields, - }, - ) = struct_item.binder.open(); - for field in fields { - struct_field_ty.push(field.ty); - } - return true; - } - false - } - _ => false, - } - }); - - if target_struct.is_none() { - bail!("The type used in Tuple is not declared in current crate") + let ( + _, + AdtDeclBoundData { + where_clause: _, + variants, + }, + ) = self.decls.adt_decl(&adt_id).binder.open(); + let AdtDeclVariant { name, fields } = variants.last().unwrap(); + + if *name != VariantId::for_struct() { + bail!("This type used in ValueExpression::Struct should be a struct") } - // We will need the adt type information when type checking field projection. - typeck_env - .adt_tys - .insert(adt_id.clone(), struct_field_ty.clone()); + + struct_field_ty = fields.iter().map(|field| field.ty.clone()).collect(); } } - // Make sure the length of value expression matches the length of field of adt. if value_expressions.len() != struct_field_ty.len() { bail!("The length of ValueExpression::Tuple does not match the type of the ADT declared") } let expression_ty_pair = zip(value_expressions, struct_field_ty); - // FIXME: we only support const in value expression of tuple for now, we can add support + // FIXME: we only support const in value expression of struct for now, we can add support // more in future. for (value_expression, declared_ty) in expression_ty_pair { let Constant(_) = value_expression else { - bail!("Only Constant is supported in ValueExpression::Tuple for now.") + bail!("Only Constant is supported in ValueExpression::Struct for now.") }; let ty = self.check_value(typeck_env, value_expression)?; // Make sure the type matches the declared adt. if ty != declared_ty { - bail!("The type in ValueExpression::Tuple does not match the ADT declared") + bail!( + "The type in ValueExpression::Tuple does not match the struct declared" + ) } } Ok(ty.clone()) @@ -507,7 +492,4 @@ struct TypeckEnv { /// LocalId of function argument. fn_args: Vec, - - /// Type information of adt - adt_tys: Map>, } diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 00bd5222..601de3d8 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -1,8 +1,8 @@ use formality_core::{set, Set, Upcast}; use formality_macros::term; use formality_types::grammar::{ - AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, - Wcs, + AdtId, AliasName, AliasTy, Binder, FieldId, Parameter, Predicate, Relation, TraitId, TraitRef, + Ty, VariantId, Wc, Wcs, }; #[term] @@ -286,7 +286,6 @@ pub struct AliasBoundDeclBoundData { } /// An "ADT declaration" declares an ADT name, its generics, and its where-clauses. -/// It doesn't capture the ADT fields, yet. /// /// In Rust syntax, it covers the `struct Foo where X: Bar` part of the declaration, but not what appears in the `{...}`. #[term(adt $id $binder)] @@ -298,9 +297,32 @@ pub struct AdtDecl { pub binder: Binder, } +// FIXME: there is a cyclic dependency if we import from formality-rust, we might be able to fix that. + /// The "bound data" for a [`AdtDecl`][]. -#[term($:where $where_clause)] +#[term($:where $,where_clause { $,variants })] pub struct AdtDeclBoundData { /// The where-clauses declared on the ADT, pub where_clause: Wcs, + pub variants: Vec, +} + +#[term($name { $,fields })] +pub struct AdtDeclVariant { + pub name: VariantId, + pub fields: Vec, +} + +#[term($name : $ty)] +pub struct AdtDeclField { + pub name: AdtDeclFieldName, + pub ty: Ty, +} + +#[term] +pub enum AdtDeclFieldName { + #[cast] + Id(FieldId), + #[cast] + Index(usize), } diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 10e17c28..d7e5263b 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -1,11 +1,11 @@ use std::sync::Arc; use formality_core::{term, Upcast}; -use formality_prove::Safety; +use formality_prove::{AdtDeclField, AdtDeclFieldName, AdtDeclVariant, Safety}; use formality_types::{ grammar::{ AdtId, AliasTy, AssociatedItemId, Binder, Const, ConstData, CrateId, Fallible, FieldId, - FnId, Lt, Parameter, Relation, TraitId, TraitRef, Ty, Wc, Wcs, + FnId, Lt, Parameter, Relation, TraitId, TraitRef, Ty, VariantId, Wc, Wcs, }, rust::Term, }; @@ -120,6 +120,15 @@ pub struct Field { pub ty: Ty, } +impl Field { + pub fn to_adt_decl_field(&self) -> AdtDeclField { + return AdtDeclField { + name: self.name.to_adt_decl_field_name(), + ty: self.ty.clone(), + }; + } +} + #[term] pub enum FieldName { #[cast] @@ -128,12 +137,16 @@ pub enum FieldName { Index(usize), } -formality_core::id!(VariantId); - -impl VariantId { - /// Returns the special variant-id used for the single variant of a struct. - pub fn for_struct() -> Self { - VariantId::new("struct") +impl FieldName { + pub fn to_adt_decl_field_name(&self) -> AdtDeclFieldName { + match self { + FieldName::Id(field_id) => { + return AdtDeclFieldName::Id(field_id.clone()); + } + FieldName::Index(idx) => { + return AdtDeclFieldName::Index(*idx); + } + } } } @@ -172,6 +185,19 @@ pub struct Variant { pub fields: Vec, } +impl Variant { + pub fn to_adt_decl_variant(&self) -> AdtDeclVariant { + AdtDeclVariant { + name: self.name.clone(), + fields: self + .fields + .iter() + .map(|field| field.to_adt_decl_field()) + .collect(), + } + } +} + #[term($?safety trait $id $binder)] pub struct Trait { pub safety: Safety, diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index e62cbd4d..b0062a31 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -300,7 +300,7 @@ impl Crate { vars, AdtBoundData { where_clauses, - variants: _, + variants, }, ) = binder.open(); prove::AdtDecl { @@ -309,6 +309,10 @@ impl Crate { vars, prove::AdtDeclBoundData { where_clause: where_clauses.iter().flat_map(|wc| wc.to_wcs()).collect(), + variants: variants + .iter() + .map(|variant| variant.to_adt_decl_variant()) + .collect(), }, ), } diff --git a/crates/formality-types/src/grammar/ids.rs b/crates/formality-types/src/grammar/ids.rs index b76a5b4c..b1ad8110 100644 --- a/crates/formality-types/src/grammar/ids.rs +++ b/crates/formality-types/src/grammar/ids.rs @@ -6,3 +6,11 @@ id!(TraitId); id!(AssociatedItemId); id!(CrateId); id!(FieldId); +id!(VariantId); + +impl VariantId { + /// Returns the special variant-id used for the single variant of a struct. + pub fn for_struct() -> Self { + VariantId::new("struct") + } +} From a35f3c67f0b3d7ead326b4a6eb512d6ce71a2805 Mon Sep 17 00:00:00 2001 From: tiif Date: Wed, 6 Aug 2025 11:16:16 +0200 Subject: [PATCH 6/9] Make the adt change pass --- crates/formality-prove/src/decls.rs | 6 ++-- crates/formality-prove/src/test/adt_wf.rs | 6 ++-- src/test/coherence_orphan.rs | 34 +++++++++++------------ src/test/mir_fn_bodies.rs | 2 +- src/test/well_formed_trait_ref.rs | 4 +-- 5 files changed, 25 insertions(+), 27 deletions(-) diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 601de3d8..ddd3a74e 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -285,7 +285,7 @@ pub struct AliasBoundDeclBoundData { pub where_clause: Wcs, } -/// An "ADT declaration" declares an ADT name, its generics, and its where-clauses. +/// An "ADT declaration" declares an ADT name, its generics, and its where-clauses, and the field. /// /// In Rust syntax, it covers the `struct Foo where X: Bar` part of the declaration, but not what appears in the `{...}`. #[term(adt $id $binder)] @@ -297,10 +297,8 @@ pub struct AdtDecl { pub binder: Binder, } -// FIXME: there is a cyclic dependency if we import from formality-rust, we might be able to fix that. - /// The "bound data" for a [`AdtDecl`][]. -#[term($:where $,where_clause { $,variants })] +#[term($:where $where_clause { $,variants })] pub struct AdtDeclBoundData { /// The where-clauses declared on the ADT, pub where_clause: Wcs, diff --git a/crates/formality-prove/src/test/adt_wf.rs b/crates/formality-prove/src/test/adt_wf.rs index befdb7bd..f9429d16 100644 --- a/crates/formality-prove/src/test/adt_wf.rs +++ b/crates/formality-prove/src/test/adt_wf.rs @@ -11,7 +11,7 @@ fn decls() -> Decls { Decls { trait_decls: vec![term("trait Foo where {}")], impl_decls: vec![term("impl Foo(u32) where {}")], - adt_decls: vec![term("adt X where {Foo(T)}")], + adt_decls: vec![term("adt X where {Foo(T)} {}")], ..Decls::empty() } } @@ -52,7 +52,7 @@ fn not_well_formed_adt() { assumptions, Relation::WellFormed(goal), ).assert_err(expect![[r#" - 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): + 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, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because @@ -62,7 +62,7 @@ fn not_well_formed_adt() { the rule "ADT" failed at step #3 (src/file.rs:LL:CC) because 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, pending: [] }, 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, pending: [] } }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because diff --git a/src/test/coherence_orphan.rs b/src/test/coherence_orphan.rs index 5037a50f..f8a8b8a6 100644 --- a/src/test/coherence_orphan.rs +++ b/src/test/coherence_orphan.rs @@ -19,7 +19,7 @@ fn neg_CoreTrait_for_CoreStruct_in_Foo() { orphan_check_neg(impl ! CoreTrait for CoreStruct {}) Caused by: - judgment `prove { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct { struct { } }], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, 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 @@ -30,15 +30,15 @@ fn neg_CoreTrait_for_CoreStruct_in_Foo() { judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) + &decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct { struct { } }], {}, {}) &name = (adt CoreStruct) the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `decls.is_local_adt_id(&a)` - decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) + decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct { struct { } }], {}, {}) &a = CoreStruct 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, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) + decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct { struct { } }], {}, {}) &goal.trait_id = CoreTrait"#]] ) } @@ -70,7 +70,7 @@ fn mirror_CoreStruct() { orphan_check(impl CoreTrait for ::Assoc { }) Caused by: - judgment `prove { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct { struct { } }], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, 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 @@ -83,15 +83,15 @@ fn mirror_CoreStruct() { judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) + &decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct { struct { } }], {}, {}) &name = (adt CoreStruct) the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `decls.is_local_adt_id(&a)` - decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) + decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct { struct { } }], {}, {}) &a = CoreStruct 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, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) + decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct { struct { } }], {}, {}) &goal.trait_id = CoreTrait"#]] ) } @@ -158,7 +158,7 @@ fn uncovered_T() { orphan_check(impl CoreTrait for ^ty0_0 { }) Caused by: - judgment `prove { goal: {@ IsLocal(CoreTrait(!ty_0, FooStruct))}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + judgment `prove { goal: {@ IsLocal(CoreTrait(!ty_0, FooStruct))}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct { struct { } }], {}, {FooStruct}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(!ty_0, FooStruct))}, 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 @@ -167,7 +167,7 @@ fn uncovered_T() { judgment `is_local_trait_ref { goal: CoreTrait(!ty_0, FooStruct), assumptions: {}, env: Env { variables: [!ty_0], 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, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) + decls = decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct { struct { } }], {}, {FooStruct}) &goal.trait_id = CoreTrait"#]] ) } @@ -199,7 +199,7 @@ fn alias_to_unit() { orphan_check(impl CoreTrait for ::Assoc { }) Caused by: - judgment `prove { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + judgment `prove { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct { struct { } }], {}, {FooStruct}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, 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 @@ -212,11 +212,11 @@ fn alias_to_unit() { judgment `is_local_parameter { goal: (), assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) + &decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct { struct { } }], {}, {FooStruct}) &name = tuple(0) 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, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) + decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct { struct { } }], {}, {FooStruct}) &goal.trait_id = CoreTrait"#]] ) } @@ -240,7 +240,7 @@ fn CoreTrait_for_CoreStruct_in_Foo() { orphan_check(impl CoreTrait for CoreStruct { }) Caused by: - judgment `prove { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `prove { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct { struct { } }], {}, {}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, 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 @@ -251,15 +251,15 @@ fn CoreTrait_for_CoreStruct_in_Foo() { judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) + &decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct { struct { } }], {}, {}) &name = (adt CoreStruct) the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `decls.is_local_adt_id(&a)` - decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) + decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct { struct { } }], {}, {}) &a = CoreStruct 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, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) + decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct { struct { } }], {}, {}) &goal.trait_id = CoreTrait"#]] ) } diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs index c1597a6e..91002321 100644 --- a/src/test/mir_fn_bodies.rs +++ b/src/test/mir_fn_bodies.rs @@ -860,6 +860,6 @@ fn test_struct_wrong_type_in_initialisation() { } ] [] - expect_test::expect!["The type in ValueExpression::Tuple does not match the ADT declared"] + expect_test::expect!["The type in ValueExpression::Tuple does not match the struct declared"] ) } diff --git a/src/test/well_formed_trait_ref.rs b/src/test/well_formed_trait_ref.rs index ac824b0e..e6b3306c 100644 --- a/src/test/well_formed_trait_ref.rs +++ b/src/test/well_formed_trait_ref.rs @@ -47,7 +47,7 @@ fn missing_dependent_where_clause() { prove_where_clauses_well_formed([S1 : Trait2]) Caused by: - judgment `prove { goal: {@ WellFormedTraitRef(Trait2(S1))}, assumptions: {Trait2(S1)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Trait1 , trait Trait2 ], [], [], [], [], [adt S1 where {Trait1(^ty0_0)}, adt S2 where {Trait2(S1<^ty0_0>)}], {Trait1, Trait2}, {S1, S2}) }` failed at the following rule(s): + judgment `prove { goal: {@ WellFormedTraitRef(Trait2(S1))}, assumptions: {Trait2(S1)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Trait1 , trait Trait2 ], [], [], [], [], [adt S1 where {Trait1(^ty0_0)} { struct { dummy : ^ty0_0 } }, adt S2 where {Trait2(S1<^ty0_0>)} { struct { dummy : ^ty0_0 } }], {Trait1, Trait2}, {S1, S2}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because judgment `prove_wc_list { goal: {@ WellFormedTraitRef(Trait2(S1))}, assumptions: {Trait2(S1)}, 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 @@ -57,7 +57,7 @@ fn missing_dependent_where_clause() { the rule "ADT" failed at step #3 (src/file.rs:LL:CC) because judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, known_true: true, substitution: {} }, goal: {Trait1(!ty_0)}, assumptions: {Trait2(S1)} }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove { goal: {Trait1(!ty_0)}, assumptions: {Trait2(S1)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Trait1 , trait Trait2 ], [], [], [], [], [adt S1 where {Trait1(^ty0_0)}, adt S2 where {Trait2(S1<^ty0_0>)}], {Trait1, Trait2}, {S1, S2}) }` failed at the following rule(s): + judgment `prove { goal: {Trait1(!ty_0)}, assumptions: {Trait2(S1)}, env: Env { variables: [!ty_0], bias: Soundness, pending: [] }, decls: decls(222, [trait Trait1 , trait Trait2 ], [], [], [], [], [adt S1 where {Trait1(^ty0_0)} { struct { dummy : ^ty0_0 } }, adt S2 where {Trait2(S1<^ty0_0>)} { struct { dummy : ^ty0_0 } }], {Trait1, Trait2}, {S1, S2}) }` failed at the following rule(s): failed at (src/file.rs:LL:CC) because judgment `prove_wc_list { goal: {Trait1(!ty_0)}, assumptions: {Trait2(S1)}, 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 From e429d246796e9090c65248ee0a02154dba2b59bd Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 5 Aug 2025 16:26:21 +0200 Subject: [PATCH 7/9] Get the adt id from the type directly --- crates/formality-check/src/mini_rust_check.rs | 52 +++++++------------ crates/formality-types/src/grammar/ty.rs | 9 ++++ 2 files changed, 28 insertions(+), 33 deletions(-) diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs index 211cbc7f..bccae721 100644 --- a/crates/formality-check/src/mini_rust_check.rs +++ b/crates/formality-check/src/mini_rust_check.rs @@ -10,8 +10,8 @@ use formality_rust::grammar::minirust::{ ValueExpression, }; use formality_rust::grammar::FnBoundData; -use formality_types::grammar::{CrateId, FnId, RigidName}; -use formality_types::grammar::{Relation, Ty, TyData, VariantId, Wcs}; +use formality_types::grammar::{CrateId, FnId}; +use formality_types::grammar::{Relation, Ty, VariantId, Wcs}; use crate::{Check, CrateItem}; use anyhow::bail; @@ -281,23 +281,11 @@ impl Check<'_> { bail!("Only Local is allowed as the root of FieldProjection") }; - // Check if the index is valid for the tuple. - // FIXME: use let chain here? - let Some(ty) = env.local_variables.get(&local_id) else { bail!("The local id used in PlaceExpression::Field is invalid.") }; - // Get the ADT type information. - let TyData::RigidTy(rigid_ty) = ty.data() else { - bail!("The type for field projection must be rigid ty") - }; - - // FIXME: directly get the adt_id information from ty - - let RigidName::AdtId(ref adt_id) = rigid_ty.name else { - bail!("The type for field projection must be adt") - }; + let adt_id = ty.get_adt_id().unwrap(); let ( _, @@ -312,6 +300,7 @@ impl Check<'_> { bail!("The local used for field projection must be struct.") } + // Check if the index is valid for the tuple. if field_projection.index >= fields.len() { bail!("The field index used in PlaceExpression::Field is invalid.") } @@ -353,13 +342,13 @@ impl Check<'_> { .unwrap(); // Find the callee from current crate. + // FIXME: get the information from decl too let callee = curr_crate.items.iter().find(|item| { match item { CrateItem::Fn(fn_declared) => { if fn_declared.id == *fn_id { let fn_bound_data = typeck_env.env.instantiate_universally(&fn_declared.binder); - // FIXME: maybe we should store the information somewhere else, like in the value expression? // Store the callee information in typeck_env, we will need this when type checking Terminator::Call. typeck_env .callee_input_tys @@ -385,28 +374,25 @@ impl Check<'_> { Ok(constant.get_ty()) } Struct(value_expressions, ty) => { - let mut struct_field_ty = Vec::new(); + let adt_id = ty.get_adt_id().unwrap(); // Check the validity of the struct. - if let TyData::RigidTy(rigid_ty) = ty.data() { - if let RigidName::AdtId(adt_id) = &rigid_ty.name { - let ( - _, - AdtDeclBoundData { - where_clause: _, - variants, - }, - ) = self.decls.adt_decl(&adt_id).binder.open(); - let AdtDeclVariant { name, fields } = variants.last().unwrap(); - - if *name != VariantId::for_struct() { - bail!("This type used in ValueExpression::Struct should be a struct") - } + let ( + _, + AdtDeclBoundData { + where_clause: _, + variants, + }, + ) = self.decls.adt_decl(&adt_id).binder.open(); + let AdtDeclVariant { name, fields } = variants.last().unwrap(); - struct_field_ty = fields.iter().map(|field| field.ty.clone()).collect(); - } + if *name != VariantId::for_struct() { + bail!("This type used in ValueExpression::Struct should be a struct") } + let struct_field_ty: Vec = + fields.iter().map(|field| field.ty.clone()).collect(); + if value_expressions.len() != struct_field_ty.len() { bail!("The length of ValueExpression::Tuple does not match the type of the ADT declared") } diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs index 8284e10e..3187a6bc 100644 --- a/crates/formality-types/src/grammar/ty.rs +++ b/crates/formality-types/src/grammar/ty.rs @@ -83,6 +83,15 @@ impl Ty { } .upcast() } + + pub fn get_adt_id(&self) -> Option { + if let TyData::RigidTy(rigid_ty) = self.data() { + if let RigidName::AdtId(ref adt_id) = rigid_ty.name { + return Some(adt_id.clone()); + }; + }; + None + } } impl UpcastFrom for Ty { From 321877d3f54e5f32cbc5ca3f7b50acf8b3d36711 Mon Sep 17 00:00:00 2001 From: tiif Date: Wed, 6 Aug 2025 10:52:00 +0200 Subject: [PATCH 8/9] Clean up --- crates/formality-check/src/mini_rust_check.rs | 1 - crates/formality-rust/src/grammar/minirust.rs | 5 +---- src/test/mir_fn_bodies.rs | 3 ++- 3 files changed, 3 insertions(+), 6 deletions(-) diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs index bccae721..83465439 100644 --- a/crates/formality-check/src/mini_rust_check.rs +++ b/crates/formality-check/src/mini_rust_check.rs @@ -342,7 +342,6 @@ impl Check<'_> { .unwrap(); // Find the callee from current crate. - // FIXME: get the information from decl too let callee = curr_crate.items.iter().find(|item| { match item { CrateItem::Fn(fn_declared) => { diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs index 73cfde7a..cbbeaaf3 100644 --- a/crates/formality-rust/src/grammar/minirust.rs +++ b/crates/formality-rust/src/grammar/minirust.rs @@ -141,10 +141,7 @@ pub enum ValueExpression { Constant(ConstTypePair), #[grammar(fn_id $v0)] Fn(FnId), - // FIXME: minirust uses typle to represent arrays, structs, tuples (including unit). - // But I think it will be quite annoying to do typecking when we have all these types - // together, so I added a variant just for struct. - #[grammar(struct ${v0} as $v1)] // FIXME: use comma separated + #[grammar(struct {$,v0} as $v1)] Struct(Vec, Ty), // Union // Variant diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs index 91002321..af845c52 100644 --- a/src/test/mir_fn_bodies.rs +++ b/src/test/mir_fn_bodies.rs @@ -262,6 +262,7 @@ fn test_struct() { crate Foo { struct Dummy { value: u32, + is_true: bool, } fn foo (u32) -> u32 = minirust(v1) -> v0 { @@ -272,7 +273,7 @@ fn test_struct() { bb0: { statements { local(v0) = load(local(v1)); - local(v2) = struct { constant(1: u32) } as Dummy; + local(v2) = struct { constant(1: u32), constant(false)} as Dummy; local(v2).0 = constant(2: u32); } return; From d76e56c47cb17bf353a4d84a189dfc3bad26b4a6 Mon Sep 17 00:00:00 2001 From: tiif Date: Wed, 6 Aug 2025 11:15:56 +0200 Subject: [PATCH 9/9] Add more checks and test --- crates/formality-check/src/mini_rust_check.rs | 8 +++-- src/test/mir_fn_bodies.rs | 30 ++++++++++++++++++- 2 files changed, 35 insertions(+), 3 deletions(-) diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs index 83465439..cbf46d70 100644 --- a/crates/formality-check/src/mini_rust_check.rs +++ b/crates/formality-check/src/mini_rust_check.rs @@ -285,7 +285,9 @@ impl Check<'_> { bail!("The local id used in PlaceExpression::Field is invalid.") }; - let adt_id = ty.get_adt_id().unwrap(); + let Some(adt_id) = ty.get_adt_id() else { + bail!("The local used for field projection is not adt.") + }; let ( _, @@ -373,7 +375,9 @@ impl Check<'_> { Ok(constant.get_ty()) } Struct(value_expressions, ty) => { - let adt_id = ty.get_adt_id().unwrap(); + let Some(adt_id) = ty.get_adt_id() else { + bail!("The type used in ValueExpression::Struct must be adt") + }; // Check the validity of the struct. let ( diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs index af845c52..e02379c4 100644 --- a/src/test/mir_fn_bodies.rs +++ b/src/test/mir_fn_bodies.rs @@ -830,7 +830,7 @@ fn test_field_projection_root_non_adt() { } ] [] - expect_test::expect!["The type for field projection must be adt"] + expect_test::expect!["The local used for field projection is not adt."] ) } @@ -864,3 +864,31 @@ fn test_struct_wrong_type_in_initialisation() { expect_test::expect!["The type in ValueExpression::Tuple does not match the struct declared"] ) } + +/// Test the behaviour of having non-adt as the type for ValueExpression::Struct. +#[test] +fn test_non_adt_ty_for_struct() { + crate::assert_err!( + [ + crate Foo { + + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + let v2: u32; + + bb0: { + statements { + local(v0) = load(local(v1)); + local(v2) = struct { constant(false) } as u32; + } + return; + } + + }; + } + ] + [] + expect_test::expect!["The type used in ValueExpression::Struct must be adt"] + ) +}