Pass crate_id instead of all fn item from current crate

tiif · tiif · commit 55388d3ecbdd · 2025-07-29T15:30:04.000+02:00
diff --git a/crates/formality-check/src/fns.rs b/crates/formality-check/src/fns.rs
@@ -3,14 +3,14 @@ use formality_rust::{
     grammar::{Fn, FnBoundData, MaybeFnBody},
     prove::ToWcs,
 };
-use formality_types::grammar::{Fallible, Wcs};
+use formality_types::grammar::{CrateId, Fallible, Wcs};
 
-use crate::{Check, CrateItem};
+use crate::Check;
 
 impl Check<'_> {
     /// A "free function" is a free-standing function that is not part of an impl.
-    pub(crate) fn check_free_fn(&self, f: &Fn, all_fn: &Vec<CrateItem>) -> Fallible<()> {
-        self.check_fn(&Env::default(), Wcs::t(), f, all_fn)
+    pub(crate) fn check_free_fn(&self, f: &Fn, crate_id: &CrateId) -> Fallible<()> {
+        self.check_fn(&Env::default(), Wcs::t(), f, crate_id)
     }
 
     /// Invoked for both free functions and methods.
@@ -25,7 +25,7 @@ impl Check<'_> {
         in_env: &Env,
         in_assumptions: impl ToWcs,
         f: &Fn,
-        all_fn: &Vec<CrateItem>,
+        crate_id: &CrateId
     ) -> Fallible<()> {
         let in_assumptions = in_assumptions.to_wcs();
 
@@ -72,7 +72,7 @@ impl Check<'_> {
                     // A trusted function body is assumed to be valid, all set.
                 }
                 formality_rust::grammar::FnBody::MiniRust(body) => {
-                    self.check_body(&env, &output_ty, &fn_assumptions, body, all_fn, input_tys)?;
+                    self.check_body(&env, &output_ty, &fn_assumptions, body, input_tys, crate_id)?;
                 }
             },
         }
diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs
@@ -1,6 +1,5 @@
 use anyhow::bail;
 
-use crate::CrateItem;
 use fn_error_context::context;
 use formality_core::Downcasted;
 use formality_prove::{Env, Safety};
@@ -13,7 +12,7 @@ use formality_rust::{
     prove::ToWcs,
 };
 use formality_types::{
-    grammar::{Binder, Fallible, Relation, Substitution, Wcs},
+    grammar::{Binder, CrateId, Fallible, Relation, Substitution, Wcs},
     rust::Term,
 };
 
@@ -22,7 +21,7 @@ impl super::Check<'_> {
     pub(super) fn check_trait_impl(
         &self,
         trait_impl: &TraitImpl,
-        all_fn: &Vec<CrateItem>,
+        crate_id: &CrateId
     ) -> Fallible<()> {
         let TraitImpl { binder, safety: _ } = trait_impl;
 
@@ -53,7 +52,7 @@ impl super::Check<'_> {
         self.check_safety_matches(trait_decl, trait_impl)?;
 
         for impl_item in &impl_items {
-            self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item, all_fn)?;
+            self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item, crate_id)?;
         }
 
         Ok(())
@@ -106,15 +105,15 @@ impl super::Check<'_> {
         assumptions: impl ToWcs,
         trait_items: &[TraitItem],
         impl_item: &ImplItem,
-        all_fn: &Vec<CrateItem>,
+        crate_id: &CrateId,
     ) -> Fallible<()> {
         let assumptions: Wcs = assumptions.to_wcs();
         assert!(
             env.only_universal_variables() && env.encloses((&assumptions, trait_items, impl_item))
         );
 
         match impl_item {
-            ImplItem::Fn(v) => self.check_fn_in_impl(env, &assumptions, trait_items, v, all_fn),
+            ImplItem::Fn(v) => self.check_fn_in_impl(env, &assumptions, trait_items, v, crate_id),
             ImplItem::AssociatedTyValue(v) => {
                 self.check_associated_ty_value(env, assumptions, trait_items, v)
             }
@@ -127,7 +126,7 @@ impl super::Check<'_> {
         impl_assumptions: impl ToWcs,
         trait_items: &[TraitItem],
         ii_fn: &Fn,
-        all_fn: &Vec<CrateItem>,
+        crate_id: &CrateId
     ) -> Fallible<()> {
         let impl_assumptions: Wcs = impl_assumptions.to_wcs();
         assert!(
@@ -146,7 +145,7 @@ impl super::Check<'_> {
 
         tracing::debug!(?ti_fn);
 
-        self.check_fn(env, &impl_assumptions, ii_fn, all_fn)?;
+        self.check_fn(env, &impl_assumptions, ii_fn, crate_id)?;
 
         let mut env = env.clone();
         let (
diff --git a/crates/formality-check/src/lib.rs b/crates/formality-check/src/lib.rs
@@ -9,7 +9,7 @@ use formality_rust::{
     grammar::{Crate, CrateItem, Program, Test, TestBoundData},
     prove::ToWcs,
 };
-use formality_types::grammar::{Fallible, Wcs};
+use formality_types::grammar::{CrateId, Fallible, Wcs};
 
 mod mini_rust_check;
 
@@ -60,19 +60,12 @@ impl Check<'_> {
     }
 
     fn check_current_crate(&self, c: &Crate) -> Fallible<()> {
-        let Crate { id: _, items } = c;
-        // Collect Fn item from current crate.
-        let all_fn: Vec<CrateItem> = c
-            .items
-            .clone()
-            .into_iter()
-            .filter(|item| matches!(item, CrateItem::Fn(_)))
-            .collect();
+        let Crate { id, items } = c;
 
         self.check_for_duplicate_items()?;
 
         for item in items {
-            self.check_crate_item(item, &all_fn)?;
+            self.check_crate_item(item, &id)?;
         }
 
         self.check_coherence(c)?;
@@ -116,13 +109,13 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn check_crate_item(&self, c: &CrateItem, all_fn: &Vec<CrateItem>) -> Fallible<()> {
+    fn check_crate_item(&self, c: &CrateItem, crate_id: &CrateId) -> Fallible<()> {
         match c {
-            CrateItem::Trait(v) => self.check_trait(v, all_fn),
-            CrateItem::TraitImpl(v) => self.check_trait_impl(v, all_fn),
+            CrateItem::Trait(v) => self.check_trait(v, crate_id),
+            CrateItem::TraitImpl(v) => self.check_trait_impl(v, crate_id),
             CrateItem::Struct(s) => self.check_adt(&s.to_adt()),
             CrateItem::Enum(e) => self.check_adt(&e.to_adt()),
-            CrateItem::Fn(f) => self.check_free_fn(f, all_fn),
+            CrateItem::Fn(f) => self.check_free_fn(f, crate_id),
             CrateItem::NegTraitImpl(i) => self.check_neg_trait_impl(i),
             CrateItem::Test(t) => self.check_test(t),
         }
diff --git a/crates/formality-check/src/mini_rust_check.rs b/crates/formality-check/src/mini_rust_check.rs
@@ -8,8 +8,8 @@ use formality_rust::grammar::minirust::ValueExpression::{Fn, Load};
 use formality_rust::grammar::minirust::{
     self, ArgumentExpression, BasicBlock, BbId, LocalId, PlaceExpression, ValueExpression,
 };
-use formality_rust::grammar::FnBoundData;
-use formality_types::grammar::FnId;
+use formality_rust::grammar::{FnBoundData};
+use formality_types::grammar::{CrateId, FnId};
 use formality_types::grammar::{Relation, Ty, Wcs};
 
 use crate::{Check, CrateItem};
@@ -22,8 +22,8 @@ impl Check<'_> {
         output_ty: impl Upcast<Ty>,
         fn_assumptions: &Wcs,
         body: minirust::Body,
-        declared_fn: &Vec<CrateItem>,
         declared_input_tys: Vec<Ty>,
+        crate_id: &CrateId
     ) -> Fallible<()> {
         // Type-check:
         //
@@ -91,8 +91,8 @@ impl Check<'_> {
             ret_id: body.ret,
             ret_place_is_initialised: false,
             declared_input_tys,
-            declared_fn: declared_fn.to_vec(),
             callee_input_tys: Map::new(),
+            crate_id: crate_id.clone(),
         };
 
         // (4) Check statements in body are valid
@@ -255,24 +255,34 @@ impl Check<'_> {
             }
             Fn(fn_id) => {
                 // Check if the function called is in declared in current crate.
-                let item = typeck_env.declared_fn.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);
-                                // Store the callee information in typeck_env, we will need this when type checking Terminator::Call.
-                                typeck_env
-                                    .callee_input_tys
-                                    .insert(fn_declared.id.clone(), fn_bound_data);
-                                return true;
+
+                // 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 callee from current crate. 
+                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);
+                                    // Store the callee information in typeck_env, we will need this when type checking Terminator::Call.
+                                    typeck_env
+                                        .callee_input_tys
+                                        .insert(fn_declared.id.clone(), fn_bound_data);
+                                    return true;
+                                }
+                                false
                             }
-                            false
+                            _ => false,
                         }
-                        _ => false,
-                    }
-                });
-                if item == None {
+                    });
+
+                // If the callee is not found, return error.
+                if callee.is_none() {
                     bail!("The function called is not declared in current crate")
                 }
                 value_ty = typeck_env.output_ty.clone();
@@ -329,9 +339,11 @@ struct TypeckEnv {
     /// All declared argument type of current function.
     declared_input_tys: Vec<Ty>,
 
-    /// All declared fn in current crate.
-    declared_fn: Vec<CrateItem>,
-
     /// All information of callee.
     callee_input_tys: Map<FnId, FnBoundData>,
+
+    /// The id of the crate where this function resides.
+    /// We need this to access information about other functions 
+    /// declared in the current crate.
+    crate_id: CrateId,
 }
diff --git a/crates/formality-check/src/traits.rs b/crates/formality-check/src/traits.rs
@@ -1,16 +1,15 @@
-use crate::CrateItem;
 use anyhow::bail;
 use fn_error_context::context;
 use formality_core::Set;
 use formality_prove::Env;
 use formality_rust::grammar::{
     AssociatedTy, AssociatedTyBoundData, Fn, Trait, TraitBoundData, TraitItem, WhereClause,
 };
-use formality_types::grammar::Fallible;
+use formality_types::grammar::{CrateId, Fallible};
 
 impl super::Check<'_> {
     #[context("check_trait({:?})", t.id)]
-    pub(super) fn check_trait(&self, t: &Trait, all_fn: &Vec<CrateItem>) -> Fallible<()> {
+    pub(super) fn check_trait(&self, t: &Trait, crate_id: &CrateId) -> Fallible<()> {
         let Trait {
             safety: _,
             id: _,
@@ -28,7 +27,7 @@ impl super::Check<'_> {
         self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?;
 
         for trait_item in &trait_items {
-            self.check_trait_item(&env, &where_clauses, trait_item, all_fn)?;
+            self.check_trait_item(&env, &where_clauses, trait_item, crate_id)?;
         }
 
         Ok(())
@@ -63,10 +62,10 @@ impl super::Check<'_> {
         env: &Env,
         where_clauses: &[WhereClause],
         trait_item: &TraitItem,
-        all_fn: &Vec<CrateItem>,
+        crate_id: &CrateId,
     ) -> Fallible<()> {
         match trait_item {
-            TraitItem::Fn(v) => self.check_fn_in_trait(env, where_clauses, v, all_fn),
+            TraitItem::Fn(v) => self.check_fn_in_trait(env, where_clauses, v, crate_id),
             TraitItem::AssociatedTy(v) => self.check_associated_ty(env, where_clauses, v),
         }
     }
@@ -76,9 +75,9 @@ impl super::Check<'_> {
         env: &Env,
         where_clauses: &[WhereClause],
         f: &Fn,
-        all_fn: &Vec<CrateItem>,
+        crate_id: &CrateId
     ) -> Fallible<()> {
-        self.check_fn(env, where_clauses, f, all_fn)
+        self.check_fn(env, where_clauses, f, crate_id)
     }
 
     fn check_associated_ty(
