Improve handling of inner docstring comments (#103)

This PR fixes #102.  

At a high level, this PR stops treating `///`-prefixed docstring
comments as comments, but as a syntactic structure of their own.

In essence, docstrings can only be used wherever an `attr` can be used
(it might even be a subset of those cases, but handling it wherever
attributes are handled _should_ handle all important cases, since `///`
docstring comments are essentially syntax sugar for the `#[doc(...)]`
attribute).

By removing it from normal comment handling, we gain more control over
them, and can actually place them correctly, touching the actual code
they should be touching; also we don't need to perform any of the normal
comment management/manipulation code on them, since they are already all
in place.

This PR _does_ cause some minor churn around a small handful of
docstring comments in our snapshotted files (see the second commit in
this PR), but reading through all of them, it seems largely either
acceptable, or even welcome changes (e.g., making the docstring
associate with the next item, rather than with the previous item).

CHANGELOG.md

@@ -1,5 +1,7 @@
 # Unreleased
 
+* Improve handling of inner-docstring comments (i.e., `///`-prefixed comments)
+
 # v0.4.3
 
 * Support handling of capturing macros (`macro_pat`) during pattern matches

examples/nr-snapshot/verified-node-replication/src/exec/context.rs

@@ -478,9 +478,9 @@ pub open spec fn inv(&self, v: u64, tid: nat, cell: PCell<PendingOperation<DT>>,
     }
 }
 }  // struct_with_invariants! ContextGhost
-/// Request Enqueue/Dequeue ghost state
 
 
+/// Request Enqueue/Dequeue ghost state
 pub tracked struct FCClientRequestResponseGhost<DT: Dispatch> {
     pub tracked batch_perms: Option<PointsTo<PendingOperation<DT>>>,
     pub tracked cell_id: Ghost<CellId>,

examples/nr-snapshot/verified-node-replication/src/exec/log.rs

@@ -90,6 +90,8 @@ pub open spec fn wf(&self, idx: nat, cb_inst: CyclicBuffer::Instance<DT>) -> boo
     }
 }
 }  // struct_with_invariants
+
+
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // NR Log
 ////////////////////////////////////////////////////////////////////////////////////////////////////

examples/nr-snapshot/verified-node-replication/src/exec/replica.rs

@@ -130,6 +130,8 @@ pub open spec fn wf(&self, nid: NodeId, inst: UnboundedLog::Instance<DT>, cb: Cy
         &&& self.cb_combiner@@.instance == cb
     }
 }}  // struct_with_invariants
+
+
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // Replica
 ////////////////////////////////////////////////////////////////////////////////////////////////////

examples/nr-snapshot/verified-node-replication/src/spec/simple_log.rs

@@ -313,13 +313,13 @@ state_machine! {
     fn no_op_inductive(pre: Self, post: Self, label: Label<DT>) { }
 
 }}  // state_machine! SimpleLog
+
+
 /// constructs the state of the data structure at a specific version given the log
 ///
 /// This function recursively applies the update operations to the initial state of the
 /// data structure and returns the state of the data structure at the given version. The
 /// version must be within the log's range.
-
-
 pub open spec fn compute_nrstate_at_version<DT: Dispatch>(
     log: Seq<DT::WriteOperation>,
     version: LogIdx,

examples/verus-snapshot/source/vstd/cell.rs

@@ -19,6 +19,7 @@ verus! {
 
 broadcast use super::map::group_map_axioms, super::set::group_set_axioms;
 // TODO implement: borrow_mut; figure out Drop, see if we can avoid leaking?
+
 /// `PCell<V>` (which stands for "permissioned call") is the primitive Verus `Cell` type.
 ///
 /// Technically, it is a wrapper around
@@ -55,7 +56,6 @@ broadcast use super::map::group_map_axioms, super::set::group_set_axioms;
 /// to extract data from the cell.
 ///
 /// ### Example (TODO)
-
 #[verifier::external_body]
 #[verifier::accept_recursive_types(V)]
 pub struct PCell<V> {

examples/verus-snapshot/source/vstd/pcm_lib.rs

@@ -8,8 +8,8 @@ use super::seq::*;
 verus! {
 
 broadcast use super::group_vstd_default;
-/// Combines a list of values into one value using P::op().
 
+/// Combines a list of values into one value using P::op().
 pub open spec fn combine_values<P: PCM>(values: Seq<P>) -> P
     decreases values.len(),
 {

examples/verus-snapshot/source/vstd/storage_protocol.rs

@@ -4,6 +4,7 @@ use super::prelude::*;
 verus! {
 
 broadcast use super::set::group_set_axioms, super::map::group_map_axioms;
+
 /// Interface for "storage protocol" ghost state.
 /// This is an extension-slash-variant on the more well-known concept
 /// of "PCM" ghost state, which we also have an interface for [here](crate::pcm::Resource).
@@ -25,7 +26,6 @@ broadcast use super::set::group_set_axioms, super::map::group_map_axioms;
 /// For applications, I generally advise using the
 /// [`tokenized_state_machine!` system](https://verus-lang.github.io/verus/state_machines/),
 /// rather than using this interface directly.
-
 #[verifier::external_body]
 #[verifier::accept_recursive_types(K)]
 #[verifier::accept_recursive_types(P)]

src/lib.rs

@@ -1358,6 +1358,7 @@ fn to_doc<'a>(
         Rule::MULTI_NEWLINE => arena.hardline(),
         Rule::COMMENT => comment_to_doc(ctx, arena, pair, true),
         Rule::multiline_comment => s.append(arena.line()),
+        Rule::inner_docstring_comment => s,
         Rule::verus_macro_body => items_to_doc(ctx, arena, pair, false),
         Rule::file | Rule::non_verus | Rule::verus_macro_use | Rule::EOI => unreachable!(),
     }

src/verus.pest

@@ -53,12 +53,18 @@ MULTI_NEWLINE = @{
 COMMENT = @{
     // Outer docstring
     ("//!" ~ (!NEWLINE ~ ANY)* ~ &NEWLINE)
-    // Inner docstring
-  | ("///" ~ (!NEWLINE ~ ANY)* ~ &NEWLINE)
     // Multiline comment
   | multiline_comment
     // Singleline comment
-  | ("//" ~ (!NEWLINE ~ ANY)* ~ &NEWLINE)
+    //
+    // NOTE: Inner docstrings `/// ...` are _explicitly_ disallowed from being
+    // called a comment, and are handled separately via
+    // `inner_docstring_comment`
+  | (!"///" ~ "//" ~ (!NEWLINE ~ ANY)* ~ &NEWLINE)
+}
+
+inner_docstring_comment = @{
+    ("///" ~ (!NEWLINE ~ ANY)* ~ &NEWLINE)
 }
 
 multiline_comment = @{
@@ -937,7 +943,11 @@ attr_core = {
 }
 // Two aliases for attr_core, so that we can print them differently
 attr = !{
-   attr_core
+    attr_core
+    // Inner docstrings are essentially syntax sugar for `#[doc(...)]` and thus
+    // are usable wherever attributes are usable. This way, docstring comments
+    // can be used anywhere attributes can.
+  | inner_docstring_comment
 }
 
 attr_inner = {

tests/verus-consistency.rs

@@ -2615,3 +2615,32 @@ verus! {
     } // verus!
     "###)
 }
+
+#[test]
+fn verus_handling_of_docstrings() {
+    // Regression test for https://github.com/verus-lang/verusfmt/issues/102
+    let file = r#"
+verus! {
+
+some_macro!{
+}
+
+/// abc
+fn foo() {
+}
+
+} // verus!
+"#;
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    some_macro!{
+    }
+
+    /// abc
+    fn foo() {
+    }
+
+    } // verus!
+    "###)
+}