diff --git a/CHANGELOG.md b/CHANGELOG.md index aa61fd1..d0fa06f 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/examples/nr-snapshot/verified-node-replication/src/exec/context.rs b/examples/nr-snapshot/verified-node-replication/src/exec/context.rs index 5b96dd5..9796e54 100644 --- a/examples/nr-snapshot/verified-node-replication/src/exec/context.rs +++ b/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>, } } } // struct_with_invariants! ContextGhost -/// Request Enqueue/Dequeue ghost state +/// Request Enqueue/Dequeue ghost state pub tracked struct FCClientRequestResponseGhost { pub tracked batch_perms: Option>>, pub tracked cell_id: Ghost, diff --git a/examples/nr-snapshot/verified-node-replication/src/exec/log.rs b/examples/nr-snapshot/verified-node-replication/src/exec/log.rs index bf2ad23..a86e652 100644 --- a/examples/nr-snapshot/verified-node-replication/src/exec/log.rs +++ b/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
) -> boo } } } // struct_with_invariants + + //////////////////////////////////////////////////////////////////////////////////////////////////// // NR Log //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/examples/nr-snapshot/verified-node-replication/src/exec/replica.rs b/examples/nr-snapshot/verified-node-replication/src/exec/replica.rs index 0791671..b88cc0f 100644 --- a/examples/nr-snapshot/verified-node-replication/src/exec/replica.rs +++ b/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
, cb: Cy &&& self.cb_combiner@@.instance == cb } }} // struct_with_invariants + + //////////////////////////////////////////////////////////////////////////////////////////////////// // Replica //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/examples/nr-snapshot/verified-node-replication/src/spec/simple_log.rs b/examples/nr-snapshot/verified-node-replication/src/spec/simple_log.rs index 1d2a528..6c29241 100644 --- a/examples/nr-snapshot/verified-node-replication/src/spec/simple_log.rs +++ b/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
) { } }} // 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( log: Seq, version: LogIdx, diff --git a/examples/verus-snapshot/source/vstd/cell.rs b/examples/verus-snapshot/source/vstd/cell.rs index fd037b6..95fe252 100644 --- a/examples/verus-snapshot/source/vstd/cell.rs +++ b/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` (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 { diff --git a/examples/verus-snapshot/source/vstd/pcm_lib.rs b/examples/verus-snapshot/source/vstd/pcm_lib.rs index d8551d1..f68f8fc 100644 --- a/examples/verus-snapshot/source/vstd/pcm_lib.rs +++ b/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(values: Seq

) -> P decreases values.len(), { diff --git a/examples/verus-snapshot/source/vstd/storage_protocol.rs b/examples/verus-snapshot/source/vstd/storage_protocol.rs index 415a4b7..20901f1 100644 --- a/examples/verus-snapshot/source/vstd/storage_protocol.rs +++ b/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)] diff --git a/src/lib.rs b/src/lib.rs index 47055da..180d849 100644 --- a/src/lib.rs +++ b/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!(), } diff --git a/src/verus.pest b/src/verus.pest index cb33fe8..fda124f 100644 --- a/src/verus.pest +++ b/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 = { diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index 929732f..8cb8852 100644 --- a/tests/verus-consistency.rs +++ b/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! + "###) +}