Make some methods sin refine_tree private (#959)

flux-rs · Dec 22, 2024 · 19d89f4 · 19d89f4
1 parent 9b3c742
commit 19d89f4
Show file tree

Hide file tree

Showing 2 changed files with 39 additions and 34 deletions.
diff --git a/crates/flux-infer/src/infer.rs b/crates/flux-infer/src/infer.rs
@@ -222,26 +222,6 @@ impl InferCtxtInner {
 }
 
 impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> {
-    pub fn clean_subtree(&mut self, snapshot: &Snapshot) {
-        self.rcx.clear_children(snapshot);
-    }
-
-    pub fn change_item<'a>(
-        &'a mut self,
-        def_id: LocalDefId,
-        region_infcx: &'a rustc_infer::infer::InferCtxt<'tcx>,
-    ) -> InferCtxt<'a, 'genv, 'tcx> {
-        InferCtxt { def_id: def_id.to_def_id(), rcx: self.rcx.branch(), region_infcx, ..*self }
-    }
-
-    pub fn change_root(&mut self, snapshot: &Snapshot) -> InferCtxt<'_, 'genv, 'tcx> {
-        InferCtxt { rcx: self.rcx.change_root(snapshot).unwrap(), ..*self }
-    }
-
-    pub fn branch(&mut self) -> InferCtxt<'_, 'genv, 'tcx> {
-        InferCtxt { rcx: self.rcx.branch(), ..*self }
-    }
-
     pub fn at(&mut self, span: Span) -> InferCtxtAt<'_, 'infcx, 'genv, 'tcx> {
         InferCtxtAt { infcx: self, span }
     }
@@ -361,8 +341,28 @@ impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> {
     }
 }
 
-/// Delegate methods to [`RefineCtxt`]
-impl<'infcx> InferCtxt<'infcx, '_, '_> {
+/// Methods that modify or advance the [`RefineTree`] cursor
+impl<'infcx, 'genv, 'tcx> InferCtxt<'infcx, 'genv, 'tcx> {
+    pub fn clean_subtree(&mut self, snapshot: &Snapshot) {
+        self.rcx.clear_children(snapshot);
+    }
+
+    pub fn change_item<'a>(
+        &'a mut self,
+        def_id: LocalDefId,
+        region_infcx: &'a rustc_infer::infer::InferCtxt<'tcx>,
+    ) -> InferCtxt<'a, 'genv, 'tcx> {
+        InferCtxt { def_id: def_id.to_def_id(), rcx: self.rcx.branch(), region_infcx, ..*self }
+    }
+
+    pub fn change_root(&mut self, snapshot: &Snapshot) -> InferCtxt<'_, 'genv, 'tcx> {
+        InferCtxt { rcx: self.rcx.change_root(snapshot).unwrap(), ..*self }
+    }
+
+    pub fn branch(&mut self) -> InferCtxt<'_, 'genv, 'tcx> {
+        InferCtxt { rcx: self.rcx.branch(), ..*self }
+    }
+
     pub fn define_vars(&mut self, sort: &Sort) -> Expr {
         self.rcx.define_vars(sort)
     }

diff --git a/crates/flux-infer/src/refine_tree.rs b/crates/flux-infer/src/refine_tree.rs
@@ -114,7 +114,7 @@ pub struct Scope {
 }
 
 impl Scope {
-    pub fn iter(&self) -> impl Iterator<Item = (Var, Sort)> + '_ {
+    pub(crate) fn iter(&self) -> impl Iterator<Item = (Var, Sort)> + '_ {
         itertools::chain(
             self.params.iter().cloned(),
             self.bindings
@@ -193,33 +193,38 @@ enum NodeKind {
 }
 
 impl RefineTree {
-    pub fn new(params: Vec<(Var, Sort)>) -> RefineTree {
+    pub(crate) fn new(params: Vec<(Var, Sort)>) -> RefineTree {
         let root =
             Node { kind: NodeKind::Root(params), nbindings: 0, parent: None, children: vec![] };
         let root = NodePtr(Rc::new(RefCell::new(root)));
         RefineTree { root }
     }
 
-    pub fn simplify(&mut self, defns: &SpecFuncDefns) {
+    pub(crate) fn simplify(&mut self, defns: &SpecFuncDefns) {
         self.root.borrow_mut().simplify(defns);
     }
 
-    pub fn into_fixpoint(self, cx: &mut FixpointCtxt<Tag>) -> QueryResult<fixpoint::Constraint> {
+    pub(crate) fn into_fixpoint(
+        self,
+        cx: &mut FixpointCtxt<Tag>,
+    ) -> QueryResult<fixpoint::Constraint> {
         Ok(self
             .root
             .borrow()
             .to_fixpoint(cx)?
             .unwrap_or(fixpoint::Constraint::TRUE))
     }
 
-    pub fn refine_ctxt_at_root(&mut self) -> RefineCtxt {
+    pub(crate) fn refine_ctxt_at_root(&mut self) -> RefineCtxt {
         RefineCtxt { ptr: NodePtr(Rc::clone(&self.root)), tree: self }
     }
 }
 
 impl<'rcx> RefineCtxt<'rcx> {
-    #[expect(clippy::unused_self, reason = "we want to explicit borrow self mutably")]
-    // We take a mutable reference to the subtree to prove statically that there's only one writer.
+    #[expect(
+        clippy::unused_self,
+        reason = "we want to explicitly borrow `self` mutably to prove there's only one writer"
+    )]
     pub(crate) fn clear_children(&mut self, snapshot: &Snapshot) {
         if let Some(ptr) = snapshot.ptr.upgrade() {
             ptr.borrow_mut().children.clear();
@@ -250,7 +255,7 @@ impl<'rcx> RefineCtxt<'rcx> {
 
     /// Defines a fresh refinement variable with the given `sort`. It returns the freshly generated
     /// name for the variable.
-    pub fn define_var(&mut self, sort: &Sort) -> Name {
+    pub(crate) fn define_var(&mut self, sort: &Sort) -> Name {
         let fresh = Name::from_usize(self.ptr.next_name_idx());
         self.ptr = self.ptr.push_node(NodeKind::ForAll(fresh, sort.clone()));
         fresh
@@ -267,7 +272,7 @@ impl<'rcx> RefineCtxt<'rcx> {
     /// [`sort`]: Sort
     /// [tuple]: Sort::Tuple
     /// [adt]: flux_middle::rty::SortCtor::Adt
-    pub fn define_vars(&mut self, sort: &Sort) -> Expr {
+    pub(crate) fn define_vars(&mut self, sort: &Sort) -> Expr {
         Expr::fold_sort(sort, |sort| Expr::fvar(self.define_var(sort)))
     }
 
@@ -298,7 +303,7 @@ impl<'rcx> RefineCtxt<'rcx> {
         Hoister::with_delegate(Unpacker { rcx: self, assume_invariants }).transparent()
     }
 
-    pub fn assume_invariants(&mut self, ty: &Ty, overflow_checking: bool) {
+    pub(crate) fn assume_invariants(&mut self, ty: &Ty, overflow_checking: bool) {
         struct Visitor<'a, 'rcx> {
             rcx: &'a mut RefineCtxt<'rcx>,
             overflow_checking: bool,
@@ -333,13 +338,13 @@ impl<'rcx> RefineCtxt<'rcx> {
     }
 }
 
-pub enum AssumeInvariants {
+pub(crate) enum AssumeInvariants {
     Yes { check_overflow: bool },
     No,
 }
 
 impl AssumeInvariants {
-    pub fn yes(check_overflow: bool) -> Self {
+    pub(crate) fn yes(check_overflow: bool) -> Self {
         Self::Yes { check_overflow }
     }
 }