Add more support to mir fn bodies

crates/formality-check/src/mini_rust_check.rs

@@ -1,17 +1,17 @@
 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::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_types::grammar::{Relation, Ty, VariantId, Wcs};
 
 use crate::{Check, CrateItem};
 use anyhow::bail;
@@ -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,22 +268,62 @@ 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
                     )
                 };
                 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")
+                };
+
+                let Some(ty) = env.local_variables.get(&local_id) else {
+                    bail!("The local id used in PlaceExpression::Field is invalid.")
+                };
+
+                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.")
+                }
+
+                place_ty = fields[field_projection.index].ty.clone();
+            }
         }
         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<Ty> {
         let value_ty;
@@ -315,6 +374,52 @@ impl Check<'_> {
                 // it will be rejected by the parser.
                 Ok(constant.get_ty())
             }
+            Struct(value_expressions, ty) => {
+                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 (
+                    _,
+                    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 struct_field_ty: Vec<Ty> =
+                    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")
+                }
+
+                let expression_ty_pair = zip(value_expressions, struct_field_ty);
+
+                // 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::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 struct declared"
+                        )
+                    }
+                }
+                Ok(ty.clone())
+            }
         }
     }
 
@@ -373,4 +478,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<LocalId>,
 }

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]
@@ -285,8 +285,7 @@ pub struct AliasBoundDeclBoundData {
     pub where_clause: Wcs,
 }
 
-/// An "ADT declaration" declares an ADT name, its generics, and its where-clauses.
-/// It doesn't capture the ADT fields, yet.
+/// An "ADT declaration" declares an ADT name, its generics, and its where-clauses, and the field.
 ///
 /// In Rust syntax, it covers the `struct Foo<X> where X: Bar` part of the declaration, but not what appears in the `{...}`.
 #[term(adt $id $binder)]
@@ -299,8 +298,29 @@ pub struct AdtDecl {
 }
 
 /// 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<AdtDeclVariant>,
+}
+
+#[term($name { $,fields })]
+pub struct AdtDeclVariant {
+    pub name: VariantId,
+    pub fields: Vec<AdtDeclField>,
+}
+
+#[term($name : $ty)]
+pub struct AdtDeclField {
+    pub name: AdtDeclFieldName,
+    pub ty: Ty,
+}
+
+#[term]
+pub enum AdtDeclFieldName {
+    #[cast]
+    Id(FieldId),
+    #[cast]
+    Index(usize),
 }

crates/formality-prove/src/prove/minimize/test.rs

@@ -17,12 +17,14 @@ fn minimize_a() {
     let (env, subst) = env.existential_substitution(&term);
     let term = term.instantiate_with(&subst).unwrap();
 
-    expect!["(Env { variables: [?ty_1, ?ty_2, ?ty_3], bias: Soundness }, [?ty_1, ?ty_3])"]
-        .assert_eq(&format!("{:?}", (&env, &term)));
+    expect![
+        "(Env { variables: [?ty_1, ?ty_2, ?ty_3], bias: Soundness, pending: [] }, [?ty_1, ?ty_3])"
+    ]
+    .assert_eq(&format!("{:?}", (&env, &term)));
 
     let (mut env_min, term_min, m) = minimize(env, term);
 
-    expect!["(Env { variables: [?ty_0, ?ty_1], bias: Soundness }, [?ty_0, ?ty_1])"]
+    expect!["(Env { variables: [?ty_0, ?ty_1], bias: Soundness, pending: [] }, [?ty_0, ?ty_1])"]
         .assert_eq(&format!("{:?}", (&env_min, &term_min)));
 
     let ty0 = term_min[0].as_variable().unwrap();
@@ -51,6 +53,7 @@ fn minimize_a() {
                     ?ty_3,
                 ],
                 bias: Soundness,
+                pending: [],
             },
             known_true: true,
             substitution: {

crates/formality-prove/src/test/adt_wf.rs

@@ -11,7 +11,7 @@ fn decls() -> Decls {
     Decls {
         trait_decls: vec![term("trait Foo<ty Self> where {}")],
         impl_decls: vec![term("impl Foo(u32) where {}")],
-        adt_decls: vec![term("adt X<ty T> where {Foo(T)}")],
+        adt_decls: vec![term("adt X<ty T> where {Foo(T)} {}")],
         ..Decls::empty()
     }
 }
@@ -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<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
+        judgment `prove { goal: {@ wf(X<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness, pending: [] }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> 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<u64>)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+            judgment `prove_wc_list { goal: {@ wf(X<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: @ wf(X<u64>), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                judgment `prove_wc { goal: @ wf(X<u64>), 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<u64>, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
+                    judgment `prove_wf { goal: X<u64>, 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 <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> 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 <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> 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()`"#]]);
 }