Merge pull request #195 from tiif/mir-fn-body

Typeck mir fn bodies

Author: nikomatsakis

crates/formality-check/src/fns.rs

@@ -3,20 +3,20 @@ use formality_rust::{
     grammar::{Fn, FnBoundData, MaybeFnBody},
     prove::ToWcs,
 };
-use formality_types::grammar::{Fallible, Wcs};
+use formality_types::grammar::{CrateId, Fallible, Wcs};
 
-use crate::{mini_rust_check, Check};
+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) -> Fallible<()> {
-        self.check_fn(&Env::default(), Wcs::t(), f)
+    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.
-    /// 
+    ///
     /// # 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 +25,7 @@ impl Check<'_> {
         in_env: &Env,
         in_assumptions: impl ToWcs,
         f: &Fn,
+        crate_id: &CrateId,
     ) -> Fallible<()> {
         let in_assumptions = in_assumptions.to_wcs();
 
@@ -59,7 +60,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 +72,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, input_tys, crate_id)?;
                 }
-            }
+            },
         }
 
         Ok(())

crates/formality-check/src/impls.rs

@@ -12,13 +12,17 @@ use formality_rust::{
     prove::ToWcs,
 };
 use formality_types::{
-    grammar::{Binder, Fallible, Relation, Substitution, Wcs},
+    grammar::{Binder, CrateId, Fallible, Relation, Substitution, Wcs},
     rust::Term,
 };
 
 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,
+        crate_id: &CrateId,
+    ) -> Fallible<()> {
         let TraitImpl { binder, safety: _ } = trait_impl;
 
         let mut env = Env::default();
@@ -48,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)?;
+            self.check_trait_impl_item(&env, &where_clauses, &trait_items, impl_item, crate_id)?;
         }
 
         Ok(())
@@ -101,14 +105,15 @@ impl super::Check<'_> {
         assumptions: impl ToWcs,
         trait_items: &[TraitItem],
         impl_item: &ImplItem,
+        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),
+            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)
             }
@@ -121,6 +126,7 @@ impl super::Check<'_> {
         impl_assumptions: impl ToWcs,
         trait_items: &[TraitItem],
         ii_fn: &Fn,
+        crate_id: &CrateId,
     ) -> Fallible<()> {
         let impl_assumptions: Wcs = impl_assumptions.to_wcs();
         assert!(
@@ -139,7 +145,7 @@ impl super::Check<'_> {
 
         tracing::debug!(?ti_fn);
 
-        self.check_fn(env, &impl_assumptions, ii_fn)?;
+        self.check_fn(env, &impl_assumptions, ii_fn, crate_id)?;
 
         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;
@@ -11,9 +9,9 @@ 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;;
+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.
@@ -62,12 +60,12 @@ impl Check<'_> {
     }
 
     fn check_current_crate(&self, c: &Crate) -> Fallible<()> {
-        let Crate { id: _, items } = c;
+        let Crate { id, items } = c;
 
         self.check_for_duplicate_items()?;
 
         for item in items {
-            self.check_crate_item(item)?;
+            self.check_crate_item(item, &id)?;
         }
 
         self.check_coherence(c)?;
@@ -111,13 +109,13 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn check_crate_item(&self, c: &CrateItem) -> Fallible<()> {
+    fn check_crate_item(&self, c: &CrateItem, crate_id: &CrateId) -> 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, 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),
+            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),
         }