Extend mir fn bodies

crates/formality-check/src/fns.rs

@@ -5,18 +5,19 @@ use formality_rust::{
 };
 use formality_types::grammar::{Fallible, Wcs};
 
-use crate::{mini_rust_check, Check};
+use crate::Check;
+use crate::CrateItem;
 
 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) -> Fallible<()> {
-        self.check_fn(&Env::default(), Wcs::t(), f)
+    pub(crate) fn check_free_fn(&self, f: &Fn, all_fn: &Vec<CrateItem>) -> Fallible<()> {
+        self.check_fn(&Env::default(), Wcs::t(), f, all_fn)
     }
 
     /// Invoked for both free functions and methods.
-    /// 
+    ///
     /// # Parameters
-    /// 
+    ///
     /// * `in_env` -- the environment from the enclosing impl (if any)
     /// * `in_assumptions` -- where-clauses from the enclosing impl (if any)
     /// * `f` -- the function definition
@@ -25,6 +26,7 @@ impl Check<'_> {
         in_env: &Env,
         in_assumptions: impl ToWcs,
         f: &Fn,
+        all_fn: &Vec<CrateItem>,
     ) -> Fallible<()> {
         let in_assumptions = in_assumptions.to_wcs();
 
@@ -59,7 +61,7 @@ impl Check<'_> {
         for input_ty in &input_tys {
             self.prove_goal(&env, &fn_assumptions, input_ty.well_formed())?;
         }
-        self.prove_goal(&env, &fn_assumptions, output_ty.well_formed())?;
+        self.prove_goal(&env, &fn_assumptions, &output_ty.well_formed())?;
 
         // Type-check the function body, if present.
         match body {
@@ -71,9 +73,9 @@ impl Check<'_> {
                     // A trusted function body is assumed to be valid, all set.
                 }
                 formality_rust::grammar::FnBody::MiniRust(body) => {
-                    mini_rust_check::check_body(&env, &fn_assumptions, body)?;
+                    self.check_body(&env, &output_ty, &fn_assumptions, body, all_fn, input_tys)?;
                 }
-            }
+            },
         }
 
         Ok(())

crates/formality-check/src/impls.rs

@@ -1,5 +1,6 @@
 use anyhow::bail;
 
+use crate::CrateItem;
 use fn_error_context::context;
 use formality_core::Downcasted;
 use formality_prove::{Env, Safety};
@@ -18,7 +19,11 @@ use formality_types::{
 
 impl super::Check<'_> {
     #[context("check_trait_impl({trait_impl:?})")]
-    pub(super) fn check_trait_impl(&self, trait_impl: &TraitImpl) -> Fallible<()> {
+    pub(super) fn check_trait_impl(
+        &self,
+        trait_impl: &TraitImpl,
+        all_fn: &Vec<CrateItem>,
+    ) -> Fallible<()> {
         let TraitImpl { binder, safety: _ } = trait_impl;
 
         let mut env = Env::default();
@@ -48,7 +53,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)?;
+            self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item, all_fn)?;
         }
 
         Ok(())
@@ -101,14 +106,15 @@ impl super::Check<'_> {
         assumptions: impl ToWcs,
         trait_items: &[TraitItem],
         impl_item: &ImplItem,
+        all_fn: &Vec<CrateItem>,
     ) -> 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),
+            ImplItem::Fn(v) => self.check_fn_in_impl(env, &assumptions, trait_items, v, all_fn),
             ImplItem::AssociatedTyValue(v) => {
                 self.check_associated_ty_value(env, assumptions, trait_items, v)
             }
@@ -121,6 +127,7 @@ impl super::Check<'_> {
         impl_assumptions: impl ToWcs,
         trait_items: &[TraitItem],
         ii_fn: &Fn,
+        all_fn: &Vec<CrateItem>,
     ) -> Fallible<()> {
         let impl_assumptions: Wcs = impl_assumptions.to_wcs();
         assert!(
@@ -139,7 +146,7 @@ impl super::Check<'_> {
 
         tracing::debug!(?ti_fn);
 
-        self.check_fn(env, &impl_assumptions, ii_fn)?;
+        self.check_fn(env, &impl_assumptions, ii_fn, all_fn)?;
 
         let mut env = env.clone();
         let (

crates/formality-check/src/lib.rs

@@ -1,7 +1,5 @@
 #![allow(dead_code)]
 
-use formality_types::rust::FormalityLang;
-
 use std::{collections::VecDeque, fmt::Debug};
 
 use anyhow::bail;
@@ -13,7 +11,7 @@ use formality_rust::{
 };
 use formality_types::grammar::{Fallible, Wcs};
 
-mod mini_rust_check;;
+mod mini_rust_check;
 
 /// Check all crates in the program. The crates must be in dependency order
 /// such that any prefix of the crates is a complete program.
@@ -63,11 +61,18 @@ impl Check<'_> {
 
     fn check_current_crate(&self, c: &Crate) -> Fallible<()> {
         let Crate { id: _, items } = c;
+        // Collect all fn informatiion from current crate.
+        let all_fn: Vec<CrateItem> = c
+            .items
+            .clone()
+            .into_iter()
+            .filter(|item| matches!(item, CrateItem::Fn(_)))
+            .collect();
 
         self.check_for_duplicate_items()?;
 
         for item in items {
-            self.check_crate_item(item)?;
+            self.check_crate_item(item, &all_fn)?;
         }
 
         self.check_coherence(c)?;
@@ -111,13 +116,13 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn check_crate_item(&self, c: &CrateItem) -> Fallible<()> {
+    fn check_crate_item(&self, c: &CrateItem, all_fn: &Vec<CrateItem>) -> Fallible<()> {
         match c {
-            CrateItem::Trait(v) => self.check_trait(v),
-            CrateItem::TraitImpl(v) => self.check_trait_impl(v),
+            CrateItem::Trait(v) => self.check_trait(v, all_fn),
+            CrateItem::TraitImpl(v) => self.check_trait_impl(v, all_fn),
             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),
+            CrateItem::Fn(f) => self.check_free_fn(f, all_fn),
             CrateItem::NegTraitImpl(i) => self.check_neg_trait_impl(i),
             CrateItem::Test(t) => self.check_test(t),
         }