Add documentation of src/analyze/{annot,crate_,did_cache,local_def}.rs

Author: coord-e

src/analyze/annot.rs

@@ -1,3 +1,5 @@
+//! Supporting implementation for parsing Thrust annotations.
+
 use rustc_ast::ast::Attribute;
 use rustc_ast::tokenstream::TokenStream;
 use rustc_index::IndexVec;
@@ -31,6 +33,10 @@ pub fn callable_path() -> [Symbol; 2] {
     [Symbol::intern("thrust"), Symbol::intern("callable")]
 }
 
+/// A [`Resolver`] implementation for resolving function parameters.
+///
+/// The parameter names and their sorts needs to be configured via
+/// [`ParamResolver::push_param`] before use.
 #[derive(Debug, Clone, Default)]
 pub struct ParamResolver {
     params: IndexVec<rty::FunctionParamIdx, (Symbol, chc::Sort)>,
@@ -52,6 +58,10 @@ impl ParamResolver {
     }
 }
 
+/// A [`Resolver`] implementation for resolving the special identifier `result`.
+///
+/// The `result` identifier is used to refer to [`rty::RefinedTypeVar::Value`] in postconditions, denoting
+/// the return value of a function.
 #[derive(Debug, Clone)]
 pub struct ResultResolver {
     result_symbol: Symbol,

src/analyze/crate_.rs

@@ -1,3 +1,5 @@
+//! Analyze a local crate.
+
 use std::collections::HashSet;
 
 use rustc_hir::def::DefKind;
@@ -12,6 +14,16 @@ use crate::chc;
 use crate::refine::{self, TemplateTypeGenerator, UnrefinedTypeGenerator};
 use crate::rty::{self, ClauseBuilderExt as _};
 
+/// An implementation of local crate analysis.
+///
+/// The entry point is [`Analyzer::run`], which performs the following steps in order:
+///
+/// 1. Register enum definitions found in the crate.
+/// 2. Give initial refinement types to local function definitions based on their signatures and
+///    annotations. This generates template refinement types with predicate variables for parameters and
+///    return types that are not known via annotations.
+/// 3. Type local function definition bodies via [`local_def::Analyzer`] using the refinement types
+///    generated in the previous step.
 pub struct Analyzer<'tcx, 'ctx> {
     tcx: TyCtxt<'tcx>,
     ctx: &'ctx mut analyze::Analyzer<'tcx>,

src/analyze/did_cache.rs

@@ -1,3 +1,5 @@
+//! Retrieves and caches well-known [`DefId`]s.
+
 use std::cell::OnceCell;
 
 use rustc_middle::ty::TyCtxt;
@@ -10,6 +12,10 @@ struct DefIds {
     nonnull: OnceCell<Option<DefId>>,
 }
 
+/// Retrieves and caches well-known [`DefId`]s.
+///
+/// [`DefId`]s of some well-known types can be retrieved as lang items or via the definition of
+/// lang items. This struct implements that logic and caches the results.
 #[derive(Clone)]
 pub struct DefIdCache<'tcx> {
     tcx: TyCtxt<'tcx>,

src/analyze/local_def.rs

@@ -1,3 +1,5 @@
+//! Analyze a local definition.
+
 use std::collections::{HashMap, HashSet};
 
 use rustc_index::bit_set::BitSet;
@@ -12,6 +14,10 @@ use crate::pretty::PrettyDisplayExt as _;
 use crate::refine::{BasicBlockType, TemplateTypeGenerator};
 use crate::rty;
 
+/// An implementation of the typing of local definitions.
+///
+/// The current implementation only applies to function definitions. The entry point is
+/// [`Analyzer::run`], which generates constraints during typing, given the expected type of the function.
 pub struct Analyzer<'tcx, 'ctx> {
     ctx: &'ctx mut analyze::Analyzer<'tcx>,
     tcx: TyCtxt<'tcx>,