Make it build successfully and add some comments

Author: tiif

crates/formality-check/src/fns.rs

@@ -5,7 +5,7 @@ use formality_rust::{
 };
 use formality_types::grammar::{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.
@@ -59,7 +59,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,7 +71,7 @@ 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)?;
                 }
             }
         }

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.

crates/formality-check/src/mini_rust_check.rs

@@ -1,4 +1,4 @@
-use formality_core::{term, Fallible, Map, Upcast};
+use formality_core::{Fallible, Map, Upcast};
 use formality_prove::Env;
 use formality_rust::grammar::minirust::{self, LocalId};
 use formality_types::grammar::{Ty, Wcs, Relation};
@@ -39,7 +39,7 @@ impl Check<'_> {
         )?;
 
         let env = TypeckEnv {
-            env,
+            env: env.clone(),
             output_ty,
             local_variables,
         };
@@ -57,43 +57,47 @@ impl Check<'_> {
             self.check_statement(env, statement)?;
         }
 
-        self.check_terminator(&block.terminator)?;
+        self.check_terminator(env, &block.terminator)?;
 
         Ok(())
     }
 
-    fn check_statement(&self, env: &TypeckEnv, statement: &minirust::Statement) -> Fallible<()> {
+    fn check_statement(&self, _env: &TypeckEnv, statement: &minirust::Statement) -> Fallible<()> {
         match statement {
-            minirust::Statement::Assign(place_expression, value_expression) => {
+            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
+                todo!();
             }
-            minirust::Statement::PlaceMention(place_expression) => {
+            minirust::Statement::PlaceMention(_place_expression) => {
                 // FIXME: check that the place is well-formed
                 // FIXME: check that access the place is allowed per borrowck rules
+                todo!();
             }
         }
     }
 
-    fn check_terminator(&self, env: &TypeckEnv, terminator: &minirust::Terminator) -> Fallible<()> {
+    fn check_terminator(&self, _env: &TypeckEnv, terminator: &minirust::Terminator) -> Fallible<()> {
         match terminator {
-            minirust::Terminator::Goto(bb_id) => {
+            minirust::Terminator::Goto(_bb_id) => {
                 // FIXME: Check that the basic block `bb_id` exists
+                todo!();
             }
-            minirust::Terminator::Call { callee, arguments, ret, next_block } => {
+            minirust::Terminator::Call { callee:_, generic_arguments:_, 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`
+                todo!();
             }
             minirust::Terminator::Return => {
                 // FIXME: Check that the return local variable has been initialized
+                todo!();
             }
         }
     }
 }
 
-#[term]
 struct TypeckEnv {
     env: Env,
 

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

@@ -63,6 +63,7 @@ pub enum Statement {
     #[grammar($v0 = $v1;)]
     Assign(PlaceExpression, ValueExpression),
 
+    // Represent let _ = place;
     #[grammar($v0;)]
     PlaceMention(PlaceExpression),
 
@@ -89,14 +90,19 @@ pub enum Terminator {
     //    call foo.add<u32>(x, y)
     #[grammar(call $callee $<?generic_arguments> $(arguments) -> $ret $:goto $next_block)]
     Call {
+        /// What function or method to call.
         callee: ValueExpression,
         // cc: CallingConvention,
         generic_arguments: Vec<Parameter>,
+        /// The function arguments to pass.
         arguments: Vec<ArgumentExpression>,
+        /// The place to put the return value into.
         ret: PlaceExpression,
+        /// The block to jump to when this call returns.
         next_block: Option<BbId>,
     },
 
+    /// Return from the current function.
     #[grammar(return)]
     Return,
 }

src/lib.rs

@@ -1,5 +1,3 @@
-#![feature(control_flow_enum)]
-
 use std::{path::PathBuf, sync::Arc};
 
 use clap::Parser;