a bit of docs

crates/ide-assists/src/assist_context.rs

@@ -16,6 +16,12 @@ use crate::{
 
 pub(crate) use ide_db::source_change::{SourceChangeBuilder, TreeMutator};
 
+///
+/// Majority of Proof action APIs are associated with AssistContext as its `impl`,
+/// as those need broader information (e.g., info for the whole project)
+/// 
+/// 
+/// 
 /// `AssistContext` allows to apply an assist or check if it could be applied.
 ///
 /// Assists use a somewhat over-engineered approach, given the current needs.
@@ -46,7 +52,7 @@ pub(crate) use ide_db::source_change::{SourceChangeBuilder, TreeMutator};
 /// Note, however, that we don't actually use such two-phase logic at the
 /// moment, because the LSP API is pretty awkward in this place, and it's much
 /// easier to just compute the edit eagerly :-)
-pub(crate) struct AssistContext<'a> {
+pub struct AssistContext<'a> {
     pub(crate) config: &'a AssistConfig,
     pub(crate) sema: Semantics<'a, RootDatabase>,
     frange: FileRange,

crates/ide-assists/src/lib.rs

@@ -66,7 +66,7 @@ macro_rules! eprintln {
 }
 
 pub(crate) mod assist_config;
-mod assist_context;
+pub mod assist_context;
 // #[cfg(test)]
 pub(crate) mod tests;
 pub mod utils;

crates/ide-assists/src/proof_plumber_api.rs

@@ -1,12 +1,38 @@
 //! ProofPlumber APIs
 //! 
-//! ProofPlumber APIs include functions inside this module
+//! ProofPlumber APIs include functions inside each module.
+//! 
+//! These APIs provide ways to utilize functionalities
+//! for a developer to write proof actions
+//! 
+//! See [`crate::AssistContext`] for APIs that utilize context information 
+//! For the rest, see [`verus_error`] and [`vst_ext`].
+//! 
+//! Aside from above APIs, there are several traits already implemented for TOST nodes
+//! 
+//! TOST nodes (aka VST node) implement various traits including `TryFrom` and `Display`
+//! `TryFrom` is used to convert CST node into a TOST Node
+//! `Display` is used to convert a TOST node into a concrete code text.
+//! 
+//! 
+//! `new` function is implemented for all TOST nodes.
+//! `From` is implemented between various TOST nodes to make it easy to convert between those.
+//! For example,
+//! ```rust
+//! for e in split_exprs {
+//!     let split_assert = AssertExpr::new(e);
+//!     stmts.statements.push(split_assert.into()); // convert AssertExpr into Stmt
+//! }
+//! ```
+//! 
+//! 
+//! For Verus syntax definition, read `ungram` file at `syntax` crate.
+//!  
+//! We use 
+//! `syntax/src/tests/sourcegen_vst.rs` to auto-generate `syntax/src/ast/generated/vst_nodes.rs`
+//! hand-written pars are at `syntax/src/vst.rs`
+//! 
 //! 
-//! For further referece, see 
-//! `syntax/src/vst`, 
-//! `syntax/src/tests/sourcegen_vst.rs`,
-//! and `ungram` file at `syntax` crate.
-//!
 pub mod proof_action_context;
 pub mod verus_error;
 pub mod run_fmt;

crates/ide-assists/src/proof_plumber_api/inline_function_api.rs

@@ -15,9 +15,9 @@ use syntax::{
 impl<'a> AssistContext<'a> {
     /// inline function call
     /// for now, assume one file only
-    /// TODO: handle Verus builtin types -- for example, `type_of_expr` panics for `int`
-    /// TODO: properly register req/ens/etc in semantics db
-    /// TODO: currently inline can panic when the inlining expr does not fully use all the parameters
+    // TODO: handle Verus builtin types -- for example, `type_of_expr` panics for `int`
+    // TODO: properly register req/ens/etc in semantics db
+    // TODO: currently inline can panic when the inlining expr does not fully use all the parameters
     pub fn vst_inline_call(
         &self,
         name_ref: vst::NameRef,     // the name of the function to inline **at the callsite**. from `name_ref`, we get its arguments

crates/ide-assists/src/proof_plumber_api/proof_action_context.rs

@@ -13,7 +13,7 @@ impl<'a> AssistContext<'a> {
     /// Get TOST node(VST node) from the current cursor position
     /// This is a wrapper around `find_node_at_offset` that returns a TOST node(VST node)
     // REVIEW: to remove type annotation, consider auto-generating all sorts of this function
-    pub(crate) fn vst_find_node_at_offset<VSTT, CSTT>(&self) -> Option<VSTT>
+    pub fn vst_find_node_at_offset<VSTT, CSTT>(&self) -> Option<VSTT>
     where
         VSTT: TryFrom<CSTT>,
         CSTT: AstNode,
@@ -22,15 +22,15 @@ impl<'a> AssistContext<'a> {
         VSTT::try_from(cst_node).ok()
     }
 
-    pub(crate) fn verus_errors(&self) -> Vec<VerusError> {
+    pub fn verus_errors(&self) -> Vec<VerusError> {
         self.verus_errors.clone()
     }
 
     /// get verus errors generated inside this function
     // note that `pre` uses `pre.callsite` instead of `pre.failing_pre`.
     // technically, the failing pre condition is not the error of that function.
     // it is error of the callsite
-    pub(crate) fn verus_errors_inside_fn(&self, func: &vst::Fn) -> Option<Vec<VerusError>> {
+    pub fn verus_errors_inside_fn(&self, func: &vst::Fn) -> Option<Vec<VerusError>> {
         let surrounding_fn: &ast::Fn = func.cst.as_ref()?;
         let surrounding_range = surrounding_fn.syntax().text_range();
         let filtered_verus_errs = self
@@ -46,7 +46,7 @@ impl<'a> AssistContext<'a> {
     }
 
     /// Get precondition failures that was generated by calling this function
-    pub(crate) fn pre_failures_by_calling_this_fn(&self, func: &vst::Fn) -> Option<Vec<PreFailure>> {
+    pub fn pre_failures_by_calling_this_fn(&self, func: &vst::Fn) -> Option<Vec<PreFailure>> {
         let surrounding_fn: &ast::Fn = func.cst.as_ref()?;
         let surrounding_range: text_edit::TextRange = surrounding_fn.syntax().text_range();
         let filtered_verus_errs: Vec<VerusError> = self
@@ -61,27 +61,27 @@ impl<'a> AssistContext<'a> {
     }
 
     /// Gather every precondition failures
-    pub(crate) fn pre_failures(&self) -> Vec<PreFailure> {
+    pub fn pre_failures(&self) -> Vec<PreFailure> {
         filter_pre_failuires(&self.verus_errors)
     }
 
     /// Gather every postcondition failrues
-    pub(crate) fn post_failures(&self) -> Vec<PostFailure> {
+    pub fn post_failures(&self) -> Vec<PostFailure> {
         filter_post_failuires(&self.verus_errors)
     }
 
     /// From a Precondition Failure, retreive the TOST expression of the failing predicate
-    pub(crate) fn expr_from_pre_failure(&self, pre: PreFailure) -> Option<vst::Expr> {
+    pub fn expr_from_pre_failure(&self, pre: PreFailure) -> Option<vst::Expr> {
         self.find_node_at_given_range::<syntax::ast::Expr>(pre.failing_pre)?.try_into().ok()
     }
 
     /// From a Postcondition Failure, retreive the TOST expression of the failing predicate
-    pub(crate) fn expr_from_post_failure(&self, post: PostFailure) -> Option<vst::Expr> {
+    pub fn expr_from_post_failure(&self, post: PostFailure) -> Option<vst::Expr> {
         self.find_node_at_given_range::<syntax::ast::Expr>(post.failing_post)?.try_into().ok()
     }
 
     /// Specify the syntax token to invoke a proof action
-    pub(crate) fn at_this_token(&self, token: SyntaxKind) -> Option<()> {
+    pub fn at_this_token(&self, token: SyntaxKind) -> Option<()> {
         let assert_keyword = self.find_token_syntax_at_offset(token)?;
         let cursor_in_range = assert_keyword.text_range().contains_range(self.selection_trimmed());
         if !cursor_in_range {
@@ -91,7 +91,7 @@ impl<'a> AssistContext<'a> {
     }
 
     /// helper routine to replace statement
-    pub(crate) fn replace_statement<ST0, ST1>(&self, func: &vst::Fn, old: ST0, new: ST1) -> Option<vst::Fn> 
+    pub fn replace_statement<ST0, ST1>(&self, func: &vst::Fn, old: ST0, new: ST1) -> Option<vst::Fn> 
     where
         ST0: Into<vst::Stmt> + std::clone::Clone,
         ST1: Into<vst::Stmt> + std::clone::Clone,
@@ -131,7 +131,7 @@ impl<'a> AssistContext<'a> {
     }
 
     /// helper routine to reduce a list of predicate into &&-ed predicate
-    pub(crate) fn reduce_exprs(&self, es: Vec<vst::Expr>) -> Option<vst::Expr> {
+    pub fn reduce_exprs(&self, es: Vec<vst::Expr>) -> Option<vst::Expr> {
         es.into_iter().reduce(|acc, e| {
             vst::Expr::BinExpr(Box::new(vst::BinExpr::new(
                 acc,

crates/ide-assists/src/proof_plumber_api/run_fmt.rs

@@ -1,6 +1,6 @@
 //! ProofPlumber API for formatting
 //! 
-//! Uses verusfmt at https://github.com/verus-lang/verusfmt
+//! Uses verusfmt at <https://github.com/verus-lang/verusfmt>
 //! 
 //! Since TOST node (VST node) abstracts away whitespace, indentation, newline and stuff
 //! for easier manipulation, we need to restore those
@@ -36,7 +36,7 @@ impl<'a> AssistContext<'a> {
     /// 1) print the function into a temporary file (ugly, but syntactically correct one)
     /// 2) run verusfmt on the temporary file
     /// 3) return the formatted function as a string
-    pub(crate) fn fmt<N: AstNode>(
+    pub fn fmt<N: AstNode>(
         &self,
         sth_to_remove: N,        // old
         text_to_replace: String, // new

crates/ide-assists/src/proof_plumber_api/run_verus.rs

@@ -1,3 +1,6 @@
+//! Run Verus and return the verification result
+
+
 use std::{process::Command, collections::hash_map::DefaultHasher, time::Instant, env, path::Path, hash::{Hasher, Hash}, fs::File, io::Write};
 use crate::AssistContext;
 use syntax::ast::{self, vst, HasModuleItem, HasName};
@@ -12,23 +15,15 @@ impl<'a> AssistContext<'a> {
     // TODO: pass the whole project to verus, instead of this single file
     // TODO: projects with multiple file/module -- `verify-module` flag --verify-function flag
     // output: None -> compile error
+    /// We only replace the function in the input
+    /// we use the remaining codebase when invoking Verus
+    /// Output None when Verus fails to start (e.g., compile error on the modified function)
     pub(crate) fn try_verus(
         &self,
         vst_fn: &vst::Fn, // only replace this function and run 
     ) -> Option<VerifResult> {
         let source_file = &self.source_file;
-        // let verus_exec_path = &self.config.verus_path;
-        // if verus_exec_path.len() == 0 {
-        //     dbg!("verus path not set");
-        // }
-        // #[cfg(test)] // We get verus path from config of editor. In test, we use a hardcoded path
-        // let verus_exec_path = HARDCODED_VERUS_PATH_FOR_TEST.to_string(); // TODO: maybe move this to test config
         let verus_exec_path = std::env::var("VERUS_BINARY_PATH").expect("please set VERUS_BINARY_PATH environment variable");
-        // if verus_exec_path.len() == 0 {
-        //     dbg!("verus path not set");
-        // }
-
-
         let mut text_string  = String::new();
         // in VST, we should also be able to "print" and verify
         // display for VST should be correct modulo whitespace

crates/ide-assists/src/proof_plumber_api/semantic_info.rs

@@ -1,6 +1,5 @@
 //! Various helper functions related to type resolution to work with TOST Nodes (VST Nodes)
 //! 
-//! 
 //! Utilizes Rust-analyzer's type `hir` implementation
 //! 
 #![allow(dead_code)]
@@ -35,6 +34,7 @@ impl<'a> AssistContext<'a> {
         None
     }
 
+    /// From a pattern, get the Enum definition of that pat.
     pub fn type_of_pat_enum(&self, pat: &vst::Pat) -> Option<vst::Enum> {
         let sema: &Semantics<'_, ide_db::RootDatabase> = &self.sema;
         let hir_ty: Vec<hir::Type> =
@@ -50,6 +50,7 @@ impl<'a> AssistContext<'a> {
         None
     }
 
+    /// Get the Struct definition of an expression
     pub fn type_of_expr_struct(&self, expr: &vst::Expr) -> Option<vst::Struct> {
         let typename = self.type_of_expr_adt(expr)?;
         if let vst::Adt::Struct(e) = typename {
@@ -58,6 +59,7 @@ impl<'a> AssistContext<'a> {
         None
     }
 
+    /// Get the struct deinition of a pat
     pub fn type_of_pat_struct(&self, pat: &vst::Pat) -> Option<vst::Struct> {
         let sema: &Semantics<'_, ide_db::RootDatabase> = &self.sema;
         let hir_ty: Vec<hir::Type> =
@@ -73,6 +75,7 @@ impl<'a> AssistContext<'a> {
         None
     }
 
+    /// From a Type usage, get the definition of the enum
     pub fn resolve_type_enum(&self, ty: &vst::Type) ->  Option<vst::Enum> {
         let sema: &Semantics<'_, ide_db::RootDatabase> = &self.sema;
         let hir_ty: Vec<hir::Type> =
@@ -93,6 +96,7 @@ impl<'a> AssistContext<'a> {
         None
     }
 
+    /// Get the NameRef at the callsite
     pub fn name_ref_from_call_expr(&self, call: &vst::CallExpr) -> Option<vst::NameRef> {
         let path = match &*call.expr {
             vst::Expr::PathExpr(path) => &path.path,
@@ -102,7 +106,8 @@ impl<'a> AssistContext<'a> {
         Some(*name_ref.clone())
     }
 
-    pub(crate) fn vst_find_fn(&self, call: &vst::CallExpr) -> Option<vst::Fn> {
+    /// Get function definition from the callsite
+    pub fn vst_find_fn(&self, call: &vst::CallExpr) -> Option<vst::Fn> {
         for item in self.source_file.items() {
             let v_item: ast::generated::vst_nodes::Item = 
                 match item.try_into() {
@@ -124,7 +129,8 @@ impl<'a> AssistContext<'a> {
         return None;
     }
 
-    pub(crate) fn is_opaque(&self, func: &vst::Fn) -> bool {
+    /// Query if this function is opaque (non-visible to the solver)
+    pub fn is_opaque(&self, func: &vst::Fn) -> bool {
         for attr in &func.attrs {
             if attr.to_string().contains("opaque") {
                 return true;
@@ -133,10 +139,4 @@ impl<'a> AssistContext<'a> {
         return false;
     }
 
-    // fn type_of_pat(&self, pat: &vst::Pat) -> Option<String> {
-    //     let sema: &Semantics<'_, ide_db::RootDatabase> = &self.sema;
-    //     let hir_ty: Vec<hir::Type> =
-    //         sema.type_of_pat(&pat.cst()?)?.adjusted().autoderef(sema.db).collect::<Vec<_>>();
-    //     let hir_ty = hir_ty.first()?.hir_fmt()
-    // }
 }

crates/ide-assists/src/proof_plumber_api/vst_ext.rs

@@ -14,6 +14,7 @@ pub fn vst_walk_expr(expr: &vst::Expr, cb: &mut dyn FnMut(vst::Expr)) {
     })
 }
 
+/// Map a VST Node recursively
 pub fn vst_map_expr_visitor<EE, FF>(exp: EE, cb: &FF) -> Result<vst::Expr, String>
 where
     EE: Into<vst::Expr>,
@@ -132,9 +133,10 @@ pub fn vst_preorder_expr(exp: &vst::Expr, cb: &mut dyn FnMut(vst::Expr) -> bool)
     }
 }
 
+/// Map each tail expressions
 // For now, just gather each returning expression 
 // TODO: `match` 
-// TODO: `return`
+// TODO: `return` 
 pub fn vst_map_each_tail_expr<EE, FF>(exp: EE, cb: &FF) -> Result<vst::Expr, String>
 where
     EE: Into<vst::Expr>,

crates/ide-assists/src/proof_plumber_api/vst_from_text.rs

@@ -1,26 +1,35 @@
+//! It can be cumbersom to generate a new TOST node using `new`
+//! Below are some helper functions in this case.
+//! We can generate commonly used TOST nodes from text using the following APIs.
+//! 
+
 use crate::AssistContext;
 use syntax::ast::{self, vst};
 
 impl<'a> AssistContext<'a> {
+    /// Generate Path from text
     pub fn vst_path_from_text(&self, text: &str) -> Option<vst::Path> {
         let path = ast::make::path_from_text(text);
         let vst_path = vst::Path::try_from(path).ok()?;
         return Some(vst_path);
     }
 
+    /// Generate CallExpr from Text and ArgList
     pub fn vst_call_expr_from_text(&self, fn_name: &str, arglist: vst::ArgList) -> Option<vst::CallExpr> {
         let fn_name_as_path: vst::Path = self.vst_path_from_text(fn_name)?;
         let fn_name_as_pathexpr: vst::PathExpr = vst::PathExpr::new(fn_name_as_path);
         let vst_call_expr = vst::CallExpr::new(fn_name_as_pathexpr, arglist);
         return Some(vst_call_expr);
     }
 
+    /// Generate NameRef from text
     pub fn vst_nameref_from_text(&self, s: &str) -> Option<vst::NameRef> {
         let mut name = vst::NameRef::new();
         name.ident_token = Some(String::from(s));
         Some(name)
     }
 
+    /// Generate Expr from text
     pub fn vst_expr_from_text(&self, s: &str) -> Option<vst::Expr> {
         let ret: vst::Expr = vst::Literal::new(s.to_string()).into();
         Some(ret)