wip with tiif

Author: nikomatsakis

crates/formality-check/src/fns.rs

@@ -1,47 +1,81 @@
 use formality_prove::Env;
 use formality_rust::{
-    grammar::{Fn, FnBoundData},
+    grammar::{Fn, FnBoundData, MaybeFnBody},
     prove::ToWcs,
 };
 use formality_types::grammar::{Fallible, Wcs};
 
-use crate::Check;
+use crate::{mini_rust_check, 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)
     }
 
+    /// 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
     pub(crate) fn check_fn(
         &self,
         in_env: &Env,
         in_assumptions: impl ToWcs,
         f: &Fn,
     ) -> Fallible<()> {
         let in_assumptions = in_assumptions.to_wcs();
+
+        // We do not expect to have any inference variables in the where clauses.
+        //
+        // e.g., `impl<T: Ord> Foo<T> { ... }` would have a reference to a
+        // universal variable `T`, not an existential one.
         assert!(in_env.only_universal_variables() && in_env.encloses((&in_assumptions, f)));
 
+        // Create a mutable copy of the environment which we will extend
+        // with the generic parameters from the function.
         let mut env = in_env.clone();
 
+        // Instantiate the generic parameters declared on the fn
+        // with universal variables (i.e., treat them as fresh,
+        // unknown types).
         let Fn { id: _, binder } = f;
-
         let FnBoundData {
             input_tys,
             output_ty,
             where_clauses,
-            body: _,
+            body,
         } = env.instantiate_universally(binder);
 
+        // The in-scope assumtion are the union of the assumptions from
+        // the impl and the fn.
         let fn_assumptions: Wcs = (in_assumptions, &where_clauses).to_wcs();
 
+        // All of the following must be well-formed:
+        // where-clauses, input parameter types, and output type.
         self.prove_where_clauses_well_formed(&env, &fn_assumptions, &where_clauses)?;
-
         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())?;
 
+        // Type-check the function body, if present.
+        match body {
+            MaybeFnBody::NoFnBody => {
+                // No fn body occurs trait definitions only.
+            }
+            MaybeFnBody::FnBody(fn_body) => match fn_body {
+                formality_rust::grammar::FnBody::TrustedFnBody => {
+                    // 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)?;
+                }
+            }
+        }
+
         Ok(())
     }
 }

crates/formality-check/src/impls.rs

@@ -179,6 +179,32 @@ impl super::Check<'_> {
             )?;
         }
 
+        // Check that the impl's declared return type is a subtype of what the trait declared:
+        //
+        // OK
+        //
+        // ```rust
+        // trait Foo {
+        //     fn bar<'a>(&'a self, input: &u32) -> &'a u32;
+        // }
+        //
+        // impl Foo for MyType {
+        //     fn bar(&self, input: &u32) -> &'static u32 {} // <-- subtype, ok
+        // }
+        // ```
+        //
+        // NOT OK
+        //
+        // ```rust
+        // trait Foo {
+        //     fn bar<'a>(&'a self, input: &u32) -> &'a u32;
+        // }
+        //
+        // impl Foo for MyType {
+        //     fn bar<'b>(&self, input: &'b u32) -> &'b u32 {} // <-- not sutype, not ok
+        // }
+        // ```
+
         self.prove_goal(
             &env,
             (&impl_assumptions, &ii_where_clauses),

crates/formality-check/src/lib.rs

@@ -1,5 +1,7 @@
 #![allow(dead_code)]
 
+use formality_types::rust::FormalityLang;
+
 use std::{collections::VecDeque, fmt::Debug};
 
 use anyhow::bail;
@@ -11,6 +13,8 @@ use formality_rust::{
 };
 use formality_types::grammar::{Fallible, Wcs};
 
+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.
 pub fn check_all_crates(program: &Program) -> Fallible<()> {

crates/formality-check/src/mini_rust_check.rs

@@ -0,0 +1,105 @@
+use formality_core::{term, Fallible, Map, Upcast};
+use formality_prove::Env;
+use formality_rust::grammar::minirust::{self, LocalId};
+use formality_types::grammar::{Ty, Wcs, Relation};
+
+use crate::Check;
+
+impl Check<'_> {
+    pub(crate) fn check_body(
+        &self,
+        env: &Env,
+        output_ty: impl Upcast<Ty>,
+        fn_assumptions: &Wcs,
+        body: minirust::Body,
+    ) -> Fallible<()> {
+        // Type-check:
+        //
+        // (1) Check that all the types declared for each local variable are well-formed
+        // (2) Check that the type of the returned local is compatible with the declared return type
+        // (3) Check that the statements in the body are valid
+
+        let output_ty: Ty = output_ty.upcast();
+
+        // (1) Check that all the types declared for each local variable are well-formed
+        for lv in &body.locals {
+            self.prove_goal(&env, &fn_assumptions, lv.ty.well_formed())?;
+        }
+        let local_variables: Map<LocalId, Ty> = body
+            .locals
+            .iter()
+            .map(|lv| (lv.id.clone(), lv.ty.clone()))
+            .collect();
+
+        // (2) Check if the actual return type is the subtype of the declared return type.
+        self.prove_goal(
+            &env,
+            fn_assumptions,
+            Relation::sub(&local_variables[&body.ret], &output_ty),
+        )?;
+
+        let env = TypeckEnv {
+            env,
+            output_ty,
+            local_variables,
+        };
+
+        // (3) Check statements in body are valid
+        for block in &body.blocks {
+            self.check_block(&env, block)?;
+        }
+
+        Ok(())
+    }
+    
+    fn check_block(&self, env: &TypeckEnv, block: &minirust::BasicBlock) -> Fallible<()> {
+        for statement in  &block.statements {
+            self.check_statement(env, statement)?;
+        }
+
+        self.check_terminator(&block.terminator)?;
+
+        Ok(())
+    }
+
+    fn check_statement(&self, env: &TypeckEnv, statement: &minirust::Statement) -> Fallible<()> {
+        match statement {
+            minirust::Statement::Assign(place_expression, value_expression) => {
+                // FIXME: check that the place and value are well-formed
+                // FIXME: check that the type of the value is a subtype of the place's type
+            }
+            minirust::Statement::PlaceMention(place_expression) => {
+                // FIXME: check that the place is well-formed
+                // FIXME: check that access the place is allowed per borrowck rules
+            }
+        }
+    }
+
+    fn check_terminator(&self, env: &TypeckEnv, terminator: &minirust::Terminator) -> Fallible<()> {
+        match terminator {
+            minirust::Terminator::Goto(bb_id) => {
+                // FIXME: Check that the basic block `bb_id` exists
+            }
+            minirust::Terminator::Call { callee, arguments, ret, next_block } => {
+                // FIXME: check that the callee is something callable
+                // FIXME: check that the arguments are well formed and their types are subtypes of the expected argument types
+                // FIXME: check that the next block is valid
+                // FIXME: check that the fn's declared return type is a subtype of the type of the local variable `ret`
+            }
+            minirust::Terminator::Return => {
+                // FIXME: Check that the return local variable has been initialized
+            }
+        }
+    }
+}
+
+#[term]
+struct TypeckEnv {
+    env: Env,
+
+    /// The declared return type from the function signature.
+    output_ty: Ty,
+
+    /// Type of each local variable, as declared.
+    local_variables: Map<LocalId, Ty>,
+}

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

@@ -1,13 +1,35 @@
 
 use formality_core::id;
 use formality_macros::term;
-use formality_types::grammar::Ty;
+use formality_types::grammar::{Parameter, Ty};
 
 // This definition is based on [MiniRust](https://github.com/minirust/minirust/blob/master/spec/lang/syntax.md).
 
 id!(BbId);
 id!(LocalId);
 
+// Example:
+//
+// fn foo() -> u32 = minirust(v1) -> v0 {
+//   let v0: u32;
+//   let v1: u32;
+//
+//   bb0:
+//     v0 = v1;
+//     return;
+// }
+//
+// fn bar() -> u32 = minirust(v1) -> v0 {
+//   let v0: u32;
+//   let v1: u32;
+//
+//   bb0:
+//     call foo (v1) -> v0 goto bb1;
+//
+//   bb1:
+//     return;
+// }
+
 /// Based on [MiniRust statements](https://github.com/minirust/minirust/blob/9ae11cc202d040f08bc13ec5254d3d41d5f3cc25/spec/lang/syntax.md#statements-terminators).
 #[term(minirust($,args) -> $ret {
     $*locals
@@ -61,10 +83,15 @@ pub enum Terminator {
     // Unreachable
     // Intrinsic
 
-    #[grammar(call $callee$(arguments) -> $ret $:goto $next_block)]
+    // Example:
+    //
+    //    call foo(x, y)
+    //    call foo.add<u32>(x, y)
+    #[grammar(call $callee $<?generic_arguments> $(arguments) -> $ret $:goto $next_block)]
     Call {
         callee: ValueExpression,
         // cc: CallingConvention,
+        generic_arguments: Vec<Parameter>,
         arguments: Vec<ArgumentExpression>,
         ret: PlaceExpression,
         next_block: Option<BbId>,