fix(fstar): print comments only if the item is printed as well

hacspec · Apr 25, 2024 · b1d8788 · b1d8788
1 parent d59f84c
commit b1d8788
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 25 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -796,14 +796,35 @@ struct
         in
         F.mk_e_app effect (if is_lemma then args else typ :: args)
 
+  (** Prints doc comments out of a list of attributes *)
+  let pdoc_comments attrs =
+    attrs
+    |> List.filter_map ~f:(fun (attr : attr) ->
+           match attr.kind with
+           | DocComment { kind; body } -> Some (kind, body)
+           | _ -> None)
+    |> List.map ~f:(fun (kind, string) ->
+           match kind with
+           | DCKLine ->
+               String.split_lines string
+               |> List.map ~f:(fun s -> "///" ^ s)
+               |> String.concat_lines
+           | DCKBlock -> "(**" ^ string ^ "*)")
+    |> List.map ~f:(fun s -> `VerbatimIntf (s, `NoNewline))
+
   let rec pitem (e : item) :
       [> `Impl of F.AST.decl
       | `Intf of F.AST.decl
       | `VerbatimImpl of string * [ `NoNewline | `Newline ]
       | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
-    try pitem_unwrapped e
+    try
+      match pitem_unwrapped e with
+      | [] -> []
+      | printed_items ->
+          (* Print comments only for items that are being printed *)
+          pdoc_comments e.attrs @ printed_items
     with Diagnostics.SpanFreeError.Exn error ->
       let error = Diagnostics.SpanFreeError.payload error in
       let error = [%show: Diagnostics.Context.t * Diagnostics.kind] error in
@@ -820,23 +841,6 @@ struct
       | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
-    let doc_comments =
-      e.attrs
-      |> List.filter_map ~f:(fun (attr : attr) ->
-             match attr.kind with
-             | DocComment { kind; body } -> Some (kind, body)
-             | _ -> None)
-      |> List.map ~f:(fun (kind, string) ->
-             match kind with
-             | DCKLine ->
-                 String.split_lines string
-                 |> List.map ~f:(fun s -> "///" ^ s)
-                 |> String.concat_lines
-             | DCKBlock -> "(**" ^ string ^ "*)")
-      |> List.map ~f:(fun s -> `VerbatimIntf (s, `NoNewline))
-    in
-    doc_comments
-    @
     match e.v with
     | Alias { name; item } ->
         let pat =

diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
@@ -63,7 +63,6 @@ let impl_Foo_for_usize: t_Foo usize =
     f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N
   }
 
-/// Test defaults types and constants
 let dup (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T) (x: v_T)
     : (v_T & v_T) = Core.Clone.f_clone x, Core.Clone.f_clone x <: (v_T & v_T)
 

diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
@@ -32,8 +32,6 @@ module Naming.Ambiguous_names
 open Core
 open FStar.Mul
 
-/// This macro surround a given expression with a let binding for
-/// an identifier `a` and a print of that `a`.
 let debug (label value: u32) : Prims.unit =
   let _:Prims.unit =
     Std.Io.Stdio.v__print (Core.Fmt.impl_2__new_v1 (Rust_primitives.unsize (let list =
@@ -127,10 +125,6 @@ class t_T3_e_for_a (v_Self: Type) = { __marker_trait_t_T3_e_for_a:Prims.unit }
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () }
 
-/// Test for ambiguous local names renaming: when two local vars are
-/// ambiguous by name but not by their internal IDs.
-/// Such situation can occur playing with *hygenic* macros.
-/// Also, this happens with some internal Rustc rewrite. (e.g. assignment of tuples)
 let v_INHERENT_CONSTANT: usize = sz 3
 
 let constants