From 8562c8dcaae78909ff089d9900b9bc0f851f71bf Mon Sep 17 00:00:00 2001 From: tiif Date: Fri, 24 Oct 2025 17:35:04 +0800 Subject: [PATCH 1/5] Fix some typo in ValueExpression::Struct --- crates/formality-check/src/mini_rust_check.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs index dd42c345..3e14c26a 100644 --- a/crates/formality-check/src/mini_rust_check.rs +++ b/crates/formality-check/src/mini_rust_check.rs @@ -402,12 +402,12 @@ impl Check<'_> { bail!("This type used in ValueExpression::Struct should be a struct") } - // Check if the number of value provided match the number of field. + // Check if the number of value provided matches the number of field. let struct_field_tys: Vec = fields.iter().map(|field| field.ty.clone()).collect(); if value_expressions.len() != struct_field_tys.len() { - bail!("The length of ValueExpression::Tuple does not match the type of the ADT declared") + bail!("The length of ValueExpression::Struct does not match the type of the ADT declared") } let mut value_tys: Vec = Vec::new(); From a7ccde3f4eae30de61c1f2b465c8371a51f75fda Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 28 Oct 2025 20:52:45 +0800 Subject: [PATCH 2/5] Add tuple expression --- crates/formality-check/src/mini_rust_check.rs | 43 ++++++++++++++++++- 1 file changed, 42 insertions(+), 1 deletion(-) diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs index 3e14c26a..142745a6 100644 --- a/crates/formality-check/src/mini_rust_check.rs +++ b/crates/formality-check/src/mini_rust_check.rs @@ -4,7 +4,7 @@ use formality_core::{judgment_fn, Fallible, Map, Upcast}; use formality_prove::{prove_normalize, AdtDeclBoundData, AdtDeclVariant, Constraints, Decls, 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}; +use formality_rust::grammar::minirust::ValueExpression::*; use formality_rust::grammar::minirust::{ self, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression, }; @@ -432,6 +432,47 @@ impl Check<'_> { Wcs::all_sub(value_tys, struct_field_tys), )?; + Ok(ty.clone()) + } + Tuple(value_expressions, ty) => { + self.prove_goal(&typeck_env.env, &fn_assumptions, ty.well_formed())?; + + if !ty.is_tuple() { + bail!("Non-tuple type provided for tuple expression"); + } + + // Check if the number of value provided matches the number of field. + let tuple_params = ty.get_tuple_parameters().unwrap(); + let value_length = value_expressions.len(); + let declared_tuple_length = tuple_params.len(); + + if value_length != declared_tuple_length { + bail!("The length of tuple declared is {declared_tuple_length}, the number of value provided is {value_length}"); + } + + let mut value_tys: Vec = Vec::new(); + + for value_expression in value_expressions { + // FIXME: we only support const in value expression of tuple for now, we can add support + // more in future. + let Constant(_) = value_expression else { + bail!("Only Constant is supported in ValueExpression::Struct for now.") + }; + + value_tys.push(self.check_value( + typeck_env, + fn_assumptions, + value_expression, + )?); + } + + // Make sure all the types supplied are the subtype of declared types. + self.prove_goal( + &typeck_env.env, + &fn_assumptions, + Wcs::all_sub(value_tys, tuple_params), + )?; + Ok(ty.clone()) } } From 5d5f350947b750030fab712cfd3a5d7bf98b5c5e Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 28 Oct 2025 20:53:12 +0800 Subject: [PATCH 3/5] Support field projection for tuple --- crates/formality-check/src/mini_rust_check.rs | 64 ++++++++++++------- 1 file changed, 42 insertions(+), 22 deletions(-) diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs index 142745a6..24d2ec12 100644 --- a/crates/formality-check/src/mini_rust_check.rs +++ b/crates/formality-check/src/mini_rust_check.rs @@ -281,38 +281,58 @@ impl Check<'_> { place_ty = ty; } Field(field_projection) => { - let ty = self.check_place(env, &field_projection.root).unwrap(); + let ty = self.check_place(env, &field_projection.root)?; // FIXME(tiif): We eventually want to do normalization here, so check_place should be // a judgment fn. - let Some(adt_id) = ty.get_adt_id() else { - bail!("The local used for field projection is not adt.") - }; - - 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.") - } - // 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.") + if ty.is_tuple() { + place_ty = self.check_tuple_projection(ty, field_projection.index)?; + } else { + // TODO: have a ty is struct + place_ty = self.check_struct_projection(ty, field_projection.index)?; } - - place_ty = fields[field_projection.index].ty.clone(); } } Ok(place_ty.clone()) } + fn check_struct_projection(&self, ty: Ty, index: usize) -> Fallible { + let Some(adt_id) = ty.get_adt_id() else { + bail!("The local used for field projection is not adt.") + }; + + 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.") + } + + // Check if the index is valid for the struct. + if index >= fields.len() { + bail!("The field index used in PlaceExpression::Field is invalid.") + } + + return Ok(fields[index].ty.clone()); + } + + fn check_tuple_projection(&self, ty: Ty, index: usize) -> Fallible { + // Check if the index is valid for the struct. + let tuple_params = ty.get_tuple_parameters().unwrap(); + if index >= tuple_params.len() { + bail!("The field index used in PlaceExpression::Field is invalid.") + } + + return Ok(tuple_params[index].as_ty().unwrap().clone()); + } + fn find_local_id(&self, env: &TypeckEnv, local_id: &LocalId) -> Option<(LocalId, Ty)> { if let Some((local_id, ty)) = env .local_variables From 561ad901721f76149cbdf1e93e25b1b382c5daf6 Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 28 Oct 2025 21:54:02 +0800 Subject: [PATCH 4/5] WIP: we can't get the struct parameters from adt parameters yet --- crates/formality-check/src/mini_rust_check.rs | 51 ++++--------------- 1 file changed, 10 insertions(+), 41 deletions(-) diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs index 24d2ec12..a01eb930 100644 --- a/crates/formality-check/src/mini_rust_check.rs +++ b/crates/formality-check/src/mini_rust_check.rs @@ -286,51 +286,20 @@ impl Check<'_> { // FIXME(tiif): We eventually want to do normalization here, so check_place should be // a judgment fn. - if ty.is_tuple() { - place_ty = self.check_tuple_projection(ty, field_projection.index)?; - } else { - // TODO: have a ty is struct - place_ty = self.check_struct_projection(ty, field_projection.index)?; + if !ty.is_tuple() && !ty.is_adt() { + bail!("The local used for field projection must be ADT or Tuple") } - } - } - Ok(place_ty.clone()) - } - - fn check_struct_projection(&self, ty: Ty, index: usize) -> Fallible { - let Some(adt_id) = ty.get_adt_id() else { - bail!("The local used for field projection is not adt.") - }; - - 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.") - } - // Check if the index is valid for the struct. - if index >= fields.len() { - bail!("The field index used in PlaceExpression::Field is invalid.") - } + let parameters = ty.get_rigid_ty_parameters().unwrap(); - return Ok(fields[index].ty.clone()); - } + if field_projection.index >= parameters.len() { + bail!("The field index used in PlaceExpression::Field is invalid.") + } - fn check_tuple_projection(&self, ty: Ty, index: usize) -> Fallible { - // Check if the index is valid for the struct. - let tuple_params = ty.get_tuple_parameters().unwrap(); - if index >= tuple_params.len() { - bail!("The field index used in PlaceExpression::Field is invalid.") + place_ty = parameters[field_projection.index].as_ty().unwrap().clone(); + } } - - return Ok(tuple_params[index].as_ty().unwrap().clone()); + Ok(place_ty.clone()) } fn find_local_id(&self, env: &TypeckEnv, local_id: &LocalId) -> Option<(LocalId, Ty)> { @@ -462,7 +431,7 @@ impl Check<'_> { } // Check if the number of value provided matches the number of field. - let tuple_params = ty.get_tuple_parameters().unwrap(); + let tuple_params = ty.get_rigid_ty_parameters().unwrap(); let value_length = value_expressions.len(); let declared_tuple_length = tuple_params.len(); From 2111b6cb2bea13ebbb3daa31fdeb9623a1b8963a Mon Sep 17 00:00:00 2001 From: tiif Date: Tue, 28 Oct 2025 21:57:09 +0800 Subject: [PATCH 5/5] Change how field projection works to accomodate tuple --- crates/formality-rust/src/grammar/minirust.rs | 2 + crates/formality-types/src/grammar/ty.rs | 20 +++ src/test/mir_fn_bodies.rs | 128 +++++++++++++++++- 3 files changed, 149 insertions(+), 1 deletion(-) diff --git a/crates/formality-rust/src/grammar/minirust.rs b/crates/formality-rust/src/grammar/minirust.rs index d8ecb69b..6a9090df 100644 --- a/crates/formality-rust/src/grammar/minirust.rs +++ b/crates/formality-rust/src/grammar/minirust.rs @@ -145,6 +145,8 @@ pub enum ValueExpression { Fn(FnId), #[grammar(struct {$,v0} as $v1)] Struct(Vec, Ty), + #[grammar(($,v0) as $v1)] + Tuple(Vec, Ty), // Union // Variant // GetDiscriminant diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs index cdb5c042..aa392836 100644 --- a/crates/formality-types/src/grammar/ty.rs +++ b/crates/formality-types/src/grammar/ty.rs @@ -88,6 +88,26 @@ impl Ty { }; None } + + pub fn is_tuple(&self) -> bool { + if let TyData::RigidTy(rigid_ty) = self.data() { + if let RigidName::Tuple(_) = rigid_ty.name { + return true; + } + }; + false + } + + pub fn is_adt(&self) -> bool { + self.get_adt_id().is_some() + } + + pub fn get_rigid_ty_parameters(&self) -> Option> { + if let TyData::RigidTy(rigid_ty) = self.data() { + return Some(rigid_ty.parameters.clone()); + }; + None + } } impl UpcastFrom for Ty { diff --git a/src/test/mir_fn_bodies.rs b/src/test/mir_fn_bodies.rs index 7765672d..d5bc7972 100644 --- a/src/test/mir_fn_bodies.rs +++ b/src/test/mir_fn_bodies.rs @@ -858,7 +858,7 @@ fn test_field_projection_root_non_adt() { } ] [] - expect_test::expect!["The local used for field projection is not adt."] + expect_test::expect!["The local used for field projection must be ADT or Tuple"] ) } @@ -931,3 +931,129 @@ fn test_non_adt_ty_for_struct() { expect_test::expect!["The type used in ValueExpression::Struct must be adt"] ) } + +// Test valid tuple expression +#[test] +fn test_tuple() { + crate::assert_ok!( + [ + crate Foo { + + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + let v2: (u32, u32); + + bb0: { + statements { + local(v0) = load(local(v1)); + local(v2) = (constant(1: u32), constant(2: u32)) as (u32, u32); + } + return; + } + + }; + } + ] + expect_test::expect!["()"] + ) +} + +#[test] +fn test_tuple_length_mismatch() { + crate::assert_err!( + [ + crate Foo { + + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + let v2: (u32, u32); + + bb0: { + statements { + local(v0) = load(local(v1)); + local(v2) = (constant(1: u32), constant(2: u32)) as (u32, u32, u32); + } + return; + } + + }; + } + ] + [] + expect_test::expect!["The length of tuple declared is 3, the number of value provided is 2"] + ) +} + +// Test the behaviour of type mismatch in tuple. +#[test] +fn test_tuple_non_subtype() { + crate::assert_err!( + [ + crate Foo { + + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + let v2: (u32, u32); + + bb0: { + statements { + local(v0) = load(local(v1)); + local(v2) = (constant(1: u32), constant(2: u32)) as (u32, u64); + } + return; + } + + }; + } + ] + [] + expect_test::expect![[r#" + judgment `prove { goal: {u32 <: u32, u32 <: u64}, 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: {u32 <: u32, u32 <: u64}, assumptions: {}, env: Env { variables: [], 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: [], bias: Soundness, pending: [] }, known_true: true, substitution: {} }, goal: {u32 <: 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: {u32 <: u64}, 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: {u32 <: 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: u32 <: u64, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): + the rule "subtype" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_sub { a: u32, b: u64, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` failed at the following rule(s): + the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_normalize { p: u32, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }` + the rule "normalize-r" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_normalize { p: u64, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] } }`"#]] + ) +} + +#[test] +fn test_tuple_projection() { + crate::assert_ok!( + [ + crate Foo { + + fn foo (u32) -> u32 = minirust(v1) -> v0 { + let v0: u32; + let v1: u32; + let v2: (u32, u32); + + bb0: { + statements { + local(v0) = load(local(v1)); + local(v2) = (constant(1: u32), constant(2: u32)) as (u32, u32); + local(v2).0 = constant(1: u32); + } + return; + } + + }; + } + ] + expect_test::expect!["()"] + ) +}