Support tuple in mir fn body

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,
 };
@@ -281,33 +281,22 @@ 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.")
+                if !ty.is_tuple() && !ty.is_adt() {
+                    bail!("The local used for field projection must be ADT or Tuple")
                 }
 
-                // Check if the index is valid for the tuple.
-                if field_projection.index >= fields.len() {
+                let parameters = ty.get_rigid_ty_parameters().unwrap();
+
+                if field_projection.index >= parameters.len() {
                     bail!("The field index used in PlaceExpression::Field is invalid.")
                 }
 
-                place_ty = fields[field_projection.index].ty.clone();
+                place_ty = parameters[field_projection.index].as_ty().unwrap().clone();
             }
         }
         Ok(place_ty.clone())
@@ -402,12 +391,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<Ty> =
                     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<Ty> = Vec::new();
@@ -432,6 +421,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_rigid_ty_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<Ty> = 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())
             }
         }

crates/formality-rust/src/grammar/minirust.rs

@@ -145,6 +145,8 @@ pub enum ValueExpression {
     Fn(FnId),
     #[grammar(struct {$,v0} as $v1)]
     Struct(Vec<ValueExpression>, Ty),
+    #[grammar(($,v0) as $v1)]
+    Tuple(Vec<ValueExpression>, Ty),
     // Union
     // Variant
     // GetDiscriminant

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<Vec<Parameter>> {
+        if let TyData::RigidTy(rigid_ty) = self.data() {
+            return Some(rigid_ty.parameters.clone());
+        };
+        None
+    }
 }
 
 impl UpcastFrom<TyData> for Ty {

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!["()"]
+    )
+}