Fix docs

crates/flux-infer/src/infer.rs

@@ -239,21 +239,18 @@ impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> {
         t
     }
 
-    // [NOTE:INFCX-SCOPE] (see https://github.com/flux-rs/flux/pull/900#discussion_r1853052650)
-    // The InferCtxt is a cursor into a tree. Some functions like define_var, assume_pred and
-    // by extension unpack advance the cursor. For example, defining a variable pushes a node
-    // as a child of the current node and then moves the cursor into that new node.
-    // Other functions, like subtyping or check_pred (typically the ones defined in InferCtxtAt)
-    // do not advance the cursor (from the caller's perspective). For example, if you call
-    // subtyping a subtree is pushed under the current node, and the cursor is returned
-    // to where it was. That's the purpose of infcx.branch: to "clone" the cursor such
-    // that the original one doesn't get modified.
-    // `infcx.pop_scope()` and `infcx.replace_evars(...)` are supposed to be called when
-    // the `infcx`` is on the same node where the push_scope was called, because
-    // `replace_evars`` only replaces evars below that node.
-    // If `pop_scope` is called at a node further down (e.g. after calling unpack),
-    // the evars above that cursor will not be replaced.
-
+    /// The `InferCtxt` is a cursor into a tree. Some functions like `define_var`, `assume_pred` and
+    /// by extension `unpack` advance the cursor. For example, defining a variable pushes a node
+    /// as a child of the current node and then moves the cursor into that new node. Other functions,
+    /// like `subtyping` or `check_pred` (typically the ones defined in `InferCtxtAt`) do not advance
+    /// the cursor (from the caller's perspective). For example, if you call subtyping a subtree is
+    /// pushed under the current node, and the cursor is returned to where it was. That's the purpose
+    /// of infcx.branch: to "clone" the cursor such that the original one doesn't get modified.
+    /// `infcx.pop_scope()` and `infcx.replace_evars(...)` are supposed to be called when the `infcx`
+    /// is on the same node where the `push_scope` was called, because `replace_evars` only replaces
+    /// evars below that node. If `pop_scope` is called at a node further down (e.g. after calling
+    /// `unpack`), the evars above that cursor will not be replaced.
+    /// (see <https://github.com/flux-rs/flux/pull/900#discussion_r1853052650>)
     pub fn push_scope(&mut self) {
         let scope = self.scope();
         self.inner.borrow_mut().evars.enter_context(scope);
@@ -459,6 +456,7 @@ pub trait LocEnv {
     ) -> InferResult<Ty>;
 
     fn unfold_strg_ref(&mut self, infcx: &mut InferCtxt, path: &Path, ty: &Ty) -> InferResult<Loc>;
+
     fn get(&self, path: &Path) -> Ty;
 }
 
@@ -472,19 +470,6 @@ struct Sub {
     obligations: Vec<Binder<rty::CoroutineObligPredicate>>,
 }
 
-/// [NOTE:unfold_strg_ref] We use this function to unfold a strong reference prior to a subtyping check.
-/// Normally, when checking a function body, a `StrgRef` is automatically unfolded
-/// i.e. `x:&strg T` is turned into turned into a `x:Ptr(l); l: T` where `l` is some
-/// fresh location. However, we need the below to do a similar unfolding in `check_fn_subtyping`
-/// where we just have the super-type signature that needs to be unfolded.
-/// We also add the binding to the environment so that we can:
-/// (1) UPDATE the location after the call, and
-/// (2) CHECK the relevant `ensures` clauses of the super-sig.
-/// Nico: More importantly, we are assuming functions always give back the "ownership"
-/// of the location so even though we should technically "consume" the ownership and
-/// remove the location from the environment, the type is always going to be overwritten.
-/// (there's a check for this btw, if you write an &strg we require an ensures for that
-/// location for the signature to be well-formed)
 impl Sub {
     fn new(reason: ConstrReason, span: Span) -> Self {
         Self { reason, span, obligations: vec![] }
@@ -503,6 +488,7 @@ impl Sub {
     ) -> InferResult {
         let infcx = &mut infcx.branch();
         // infcx.push_trace(TypeTrace::tys(a, b));
+
         match (a.kind(), b.kind()) {
             (_, TyKind::Exists(ctor_b)) => {
                 infcx.enter_exists(ctor_b, |infcx, ty_b| self.fun_args(infcx, env, a, &ty_b))
@@ -512,12 +498,26 @@ impl Sub {
                 self.fun_args(infcx, env, a, ty_b)
             }
             (TyKind::Ptr(PtrKind::Mut(_), path1), TyKind::StrgRef(_, path2, ty2)) => {
+                // We should technically remove `path1` from `env`, but we are assuming that functions
+                // always give back ownership of the location so `path1` is going to be overwritten
+                // after the call anyways.
                 let ty1 = env.get(path1);
                 infcx.unify_exprs(&path1.to_expr(), &path2.to_expr());
                 self.tys(infcx, &ty1, ty2)
             }
             (TyKind::StrgRef(_, path1, ty1), TyKind::StrgRef(_, path2, ty2)) => {
-                env.unfold_strg_ref(infcx, path1, ty1)?; // see [NOTE:unfold_strg_ref]
+                // We has to unfold strong references prior to a subtyping check. Normally, when
+                // checking a function body, a `StrgRef` is automatically unfolded i.e. `x:&strg T`
+                // is turned into a `x:ptr(l); l: T` where `l` is some fresh location. However, we
+                // need the below to do a similar unfolding in `check_fn_subtyping` where we just
+                // have the super-type signature that needs to be unfolded. We also add the binding
+                // to the environment so that we can:
+                // (1) UPDATE the location after the call, and
+                // (2) CHECK the relevant `ensures` clauses of the super-sig.
+                // Same as the `Ptr` case above we should remove the location from the environment
+                // after unfolding to consume it, but we are assuming functions always give back
+                // ownership.
+                env.unfold_strg_ref(infcx, path1, ty1)?;
                 let ty1 = env.get(path1);
                 infcx.unify_exprs(&path1.to_expr(), &path2.to_expr());
                 self.tys(infcx, &ty1, ty2)

crates/flux-middle/src/rty/region_matching.rs

@@ -22,8 +22,9 @@ pub fn rty_match_regions(a: &rty::Ty, b: &rty::Ty) -> rty::Ty {
     subst.apply(&a)
 }
 
-/// Replace all regions with a [`ReVar`] assigning each a unique [`RegionVid`]. This is used
-/// to have a unique identifier for each position such that we can infer a region substitution.
+/// Replace all non-bound regions with a [`rty::ReVar`] assigning each a unique [`rty::RegionVid`].
+/// This is used to have a unique identifier for each position such that we can infer a region
+/// substitution.
 fn replace_regions_with_unique_vars(ty: &rty::Ty) -> rty::Ty {
     struct Replacer {
         next_rvid: u32,

crates/flux-refineck/src/checker.rs

@@ -285,7 +285,7 @@ fn check_fn_subtyping(
         infcx.check_pred(requires, reason);
     }
 
-    // 4. Plug in the EVAR solution / replace evars -- see [NOTE:INFCX-SCOPE]
+    // 4. Plug in the EVAR solution / replace evars -- see [`InferCtxt::push_scope`]
     let evars_sol = infcx.pop_scope().with_span(span)?;
     infcx.replace_evars(&evars_sol);
     let output = sub_sig
@@ -384,13 +384,13 @@ fn find_trait_item(
     Ok(None)
 }
 
-/// [NOTE:Unfold-Local-Pointers] temporarily (at a call-site) convert an &mut to an &strg
-/// to allow for the call to be checked. This is done by unfolding the &mut into a local pointer
-/// at the call-site and then folding the pointer back into the &mut upon return.
-/// See [NOTE:Fold-Local-Pointers]
+/// Temporarily (around a function call) convert an `&mut` to an `&strg` to allow for the call to be
+/// checked. This is done by unfolding the `&mut` into a local pointer at the call-site and then
+/// folding the pointer back into the `&mut` upon return.
+/// See also [`fold_local_ptrs`].
 ///
 /// ```text
-/// unpack(T) = T'
+///             unpack(T) = T'
 /// ---------------------------------------[local-unfold]
 /// Γ ; &mut T => Γ, l:[<: T] T' ; ptr(l)
 /// ```
@@ -421,12 +421,11 @@ fn unfold_local_ptrs(
     Ok(tys)
 }
 
-/// [NOTE:Fold-Local-Pointers] Fold local pointers implements roughly a rule like this (for all the
-/// local pointers) that converts the local pointers created via [NOTE:Unfold-Local-Pointers] back
-/// into &mut.
+/// Fold local pointers implements roughly a rule like the following (for all local pointers)
+/// that converts the local pointers created via [`unfold_local_ptrs`] back into `&mut`.
 ///
 /// ```text
-/// T1 <: T2
+///       T1 <: T2
 /// --------------------- [local-fold]
 /// Γ, l:[<: T2] T1 => Γ
 /// ```
@@ -956,8 +955,8 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> {
         Ok(Guard::Pred(pred))
     }
 
-    /// Checks conditional branching as in a `match` statement. [`SwitchTargets`] (https://doc.rust-lang.org/nightly/nightly-rustc/stable_mir/mir/struct.SwitchTargets.html) contains a list of branches - the exact bit value which is being compared and the block to jump to. Using the conditionals, each branch can be checked using the new control flow information.
-    /// See https://github.com/flux-rs/flux/pull/840#discussion_r1786543174
+    /// Checks conditional branching as in a `match` statement. [`SwitchTargets`](https://doc.rust-lang.org/nightly/nightly-rustc/stable_mir/mir/struct.SwitchTargets.html) contains a list of branches - the exact bit value which is being compared and the block to jump to. Using the conditionals, each branch can be checked using the new control flow information.
+    /// See <https://github.com/flux-rs/flux/pull/840#discussion_r1786543174>
     fn check_if(discr_ty: &Ty, targets: &SwitchTargets) -> Vec<(BasicBlock, Guard)> {
         let mk = |bits| {
             match discr_ty.kind() {

crates/flux-refineck/src/type_env.rs

@@ -334,7 +334,7 @@ impl<'a> TypeEnv<'a> {
         Ok(loc)
     }
 
-    /// ```
+    /// ```text
     /// -----------------------------------
     /// Γ ; &strg <ℓ: t> => Γ,ℓ: t ; ptr(ℓ)
     /// ```