Add documentation to src/{analyze,refine,refine/basic_block}.rs

Author: coord-e

src/analyze.rs

@@ -1,3 +1,11 @@
+//! Analysis of Rust MIR to generate a CHC system.
+//!
+//! The [`Analyzer`] generates subtyping constraints in the form of CHCs ([`chc::System`]).
+//! The entry point is [`crate_::Analyzer::run`], followed by [`local_def::Analyzer::run`]
+//! and [`basic_block::Analyzer::run`], while accumulating the necessary information in
+//! [`Analyzer`]. Once [`chc::System`] is collected for the entire input, it invokes an external
+//! CHC solver with the [`Analyzer::solve`] and subsequently reports the result.
+
 use std::cell::RefCell;
 use std::collections::HashMap;
 use std::rc::Rc;

src/refine.rs

@@ -1,3 +1,12 @@
+//! Core logic of refinement typing.
+//!
+//! This module includes the definition of the refinement typing environment along with the template
+//! type generation from MIR types.
+//!
+//! This module is used by the [`crate::analyze`] module. There is currently no clear boundary between
+//! the `analyze` and `refine` modules, so it is a TODO to integrate this into the `analyze`
+//! module and remove this one.
+
 mod template;
 pub use template::{TemplateScope, TemplateTypeGenerator, UnrefinedTypeGenerator};
 

src/refine/basic_block.rs

@@ -1,12 +1,18 @@
+//! The refinement type for a basic block.
+
 use pretty::{termcolor, Pretty};
 use rustc_index::IndexVec;
 use rustc_middle::mir::Local;
 use rustc_middle::ty as mir_ty;
 
 use crate::rty;
 
-/// `BasicBlockType` is a special case of `FunctionType` whose parameters are
-/// associated with `Local`s.
+/// A special case of [`rty::FunctionType`] whose parameters are
+/// associated with [`Local`]s.
+///
+/// Thrust essentially handles basic blocks as functions, but it needs to associate function
+/// parameters with MIR [`Local`]s during its analysis. [`BasicBlockType`] includes the mapping
+/// from function parameters to [`Local`]s along with the underlying function type.
 #[derive(Debug, Clone)]
 pub struct BasicBlockType {
     // TODO: make this completely private by exposing appropriate ctor