feat: add support for #[doc="..."] attributes

engine/backends/fstar/fstar_backend.ml

@@ -799,8 +799,8 @@ struct
   let rec pitem (e : item) :
       [> `Impl of F.AST.decl
       | `Intf of F.AST.decl
-      | `VerbatimImpl of string
-      | `VerbatimIntf of string
+      | `VerbatimImpl of string * [ `NoNewline | `Newline ]
+      | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
     try pitem_unwrapped e
@@ -816,10 +816,27 @@ struct
   and pitem_unwrapped (e : item) :
       [> `Impl of F.AST.decl
       | `Intf of F.AST.decl
-      | `VerbatimImpl of string
-      | `VerbatimIntf of string
+      | `VerbatimImpl of string * [ `NoNewline | `Newline ]
+      | `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 =
@@ -1272,10 +1289,13 @@ struct
                    "Malformed `Quote` item: could not find a ItemQuote payload")
           |> Option.value ~default:Types.{ intf = true; impl = false }
         in
-        (if fstar_opts.intf then [ `VerbatimIntf (pquote e.span quote) ]
+        (if fstar_opts.intf then
+         [ `VerbatimIntf (pquote e.span quote, `Newline) ]
         else [])
         @
-        if fstar_opts.impl then [ `VerbatimImpl (pquote e.span quote) ] else []
+        if fstar_opts.impl then
+          [ `VerbatimImpl (pquote e.span quote, `Newline) ]
+        else []
     | HaxError details ->
         [
           `Comment
@@ -1291,8 +1311,8 @@ module type S = sig
     item ->
     [> `Impl of F.AST.decl
     | `Intf of F.AST.decl
-    | `VerbatimImpl of string
-    | `VerbatimIntf of string
+    | `VerbatimImpl of string * [ `NoNewline | `Newline ]
+    | `VerbatimIntf of string * [ `NoNewline | `Newline ]
     | `Comment of string ]
     list
 end
@@ -1305,7 +1325,8 @@ let make (module M : Attrs.WITH_ITEMS) ctx =
             end) : S)
 
 let strings_of_item ~signature_only (bo : BackendOptions.t) m items
-    (item : item) : [> `Impl of string | `Intf of string ] list =
+    (item : item) :
+    ([> `Impl of string | `Intf of string ] * [ `NoNewline | `Newline ]) list =
   let interface_mode' : Types.inclusion_kind =
     List.rev bo.interfaces
     |> List.find ~f:(fun (clause : Types.inclusion_clause) ->
@@ -1342,26 +1363,44 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
   Print.pitem item
   |> List.filter ~f:(function `Impl _ when no_impl -> false | _ -> true)
   |> List.concat_map ~f:(function
-       | `Impl i -> [ mk_impl (decl_to_string i) ]
-       | `Intf i -> [ mk_intf (decl_to_string i) ]
-       | `VerbatimIntf s -> if interface_mode then [ `Intf s ] else [ `Impl s ]
-       | `VerbatimImpl s -> if interface_mode then [ `Impl s ] else [ `Impl s ]
+       | `Impl i -> [ (mk_impl (decl_to_string i), `Newline) ]
+       | `Intf i -> [ (mk_intf (decl_to_string i), `Newline) ]
+       | `VerbatimIntf (s, nl) ->
+           [ ((if interface_mode then `Intf s else `Impl s), nl) ]
+       | `VerbatimImpl (s, nl) ->
+           [ ((if interface_mode then `Impl s else `Impl s), nl) ]
        | `Comment s ->
            let s = "(* " ^ s ^ " *)" in
-           if interface_mode then [ `Impl s; `Intf s ] else [ `Impl s ])
+           if interface_mode then [ (`Impl s, `Newline); (`Intf s, `Newline) ]
+           else [ (`Impl s, `Newline) ])
 
 let string_of_items ~signature_only (bo : BackendOptions.t) m items :
     string * string =
   let strings =
     List.concat_map ~f:(strings_of_item ~signature_only bo m items) items
-    |> List.map ~f:(function
-         | `Impl s -> `Impl (String.strip s)
-         | `Intf s -> `Intf (String.strip s))
+    |> List.map
+         ~f:
+           ((function
+              | `Impl s -> `Impl (String.strip s)
+              | `Intf s -> `Intf (String.strip s))
+           *** Fn.id)
     |> List.filter
-         ~f:((function `Impl s | `Intf s -> String.is_empty s) >> not)
+         ~f:(fst >> (function `Impl s | `Intf s -> String.is_empty s) >> not)
   in
   let string_for filter =
-    List.filter_map ~f:filter strings |> String.concat ~sep:"\n\n"
+    let l =
+      List.filter_map
+        ~f:(fun (s, space) ->
+          let* s = filter s in
+          Some (s, space))
+        strings
+    in
+    let n = List.length l - 1 in
+    List.mapi
+      ~f:(fun i (s, space) ->
+        s ^ if [%matches? `NoNewline] space || [%eq: int] i n then "" else "\n")
+      l
+    |> String.concat ~sep:"\n"
   in
   ( string_for (function `Impl s -> Some s | _ -> None),
     string_for (function `Intf s -> Some s | _ -> None) )

engine/lib/import_thir.ml

@@ -101,6 +101,19 @@ let c_logical_op : Thir.logical_op -> logical_op = function
 let c_attr (attr : Thir.attribute) : attr =
   let kind =
     match attr.kind with
+    | DocComment (kind, body) ->
+        let kind =
+          match kind with Thir.Line -> DCKLine | Thir.Block -> DCKBlock
+        in
+        DocComment { kind; body }
+    | Normal
+        {
+          item =
+            { args = Eq (_, Hir { symbol; _ }); path = "doc"; tokens = None };
+          tokens = None;
+        } ->
+        DocComment { kind = DCKLine; body = symbol }
+        (* Looks for `#[doc = "something"]` *)
     | Normal { item = { args; path; tokens = subtokens }; tokens } ->
         let args_tokens =
           match args with Delimited { tokens; _ } -> Some tokens | _ -> None
@@ -110,11 +123,6 @@ let c_attr (attr : Thir.attribute) : attr =
           Option.value ~default:"" (args_tokens || tokens || subtokens)
         in
         Tool { path; tokens }
-    | DocComment (kind, body) ->
-        let kind =
-          match kind with Thir.Line -> DCKLine | Thir.Block -> DCKBlock
-        in
-        DocComment { kind; body }
   in
   { kind; span = Span.of_thir attr.span }
 
@@ -125,15 +133,14 @@ let c_item_attrs (attrs : Thir.item_attributes) : attrs =
      that parent/self structure in our AST. See
      https://github.com/hacspec/hax/issues/123. *)
   let self = c_attrs attrs.attributes in
-  let parent = c_attrs attrs.parent_attributes in
   let parent =
-    (* Repeating associateditem or uid is harmful *)
-    List.filter
-      ~f:(fun payload ->
+    c_attrs attrs.parent_attributes
+    |> List.filter ~f:([%matches? ({ kind = DocComment _; _ } : attr)] >> not)
+    |> (* Repeating associateditem or uid is harmful, same for comments *)
+    List.filter ~f:(fun payload ->
         match Attr_payloads.payloads [ payload ] with
         | [ ((Uid _ | AssociatedItem _), _) ] -> false
         | _ -> true)
-      parent
   in
   self @ parent
 

frontend/exporter/src/types/copied.rs

@@ -2008,9 +2008,35 @@ pub enum AttrArgs {
     Empty,
     Delimited(DelimArgs),
 
+    Eq(Span, AttrArgsEq),
+    // #[todo]
+    // Todo(String),
+}
+
+/// Reflects [`rustc_ast::ast::AttrArgsEq`]
+#[derive(AdtInto)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::AttrArgsEq, state: S as tcx)]
+#[derive(
+    Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
+)]
+pub enum AttrArgsEq {
+    Hir(MetaItemLit),
     #[todo]
-    Todo(String),
-    // Eq(Span, AttrArgsEq),
+    Ast(String),
+    // Ast(P<Expr>),
+}
+
+/// Reflects [`rustc_ast::ast::MetaItemLit`]
+#[derive(AdtInto)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::MetaItemLit, state: S as tcx)]
+#[derive(
+    Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
+)]
+pub struct MetaItemLit {
+    pub symbol: Symbol,
+    pub suffix: Option<Symbol>,
+    pub kind: LitKind,
+    pub span: Span,
 }
 
 /// Reflects [`rustc_ast::ast::AttrItem`]

test-harness/src/snapshots/toolchain__attributes into-fstar.snap

@@ -108,6 +108,10 @@ let v_MAX: usize = sz 10
 
 type t_MyArray = | MyArray : t_Array u8 (sz 10) -> t_MyArray
 
+/// Triple dash comment
+(** Multiline double star comment Maecenas blandit accumsan feugiat.
+    Done vitae ullamcorper est.
+    Curabitur id dui eget sem viverra interdum. *)
 let mutation_example
       (use_generic_update_at: t_MyArray)
       (use_specialized_update_at: t_Slice u8)
@@ -153,6 +157,8 @@ let u32_max: u32 = 90000ul
 
 unfold let some_function _ = "hello from F*"
 
+/// A doc comment on `add3`
+///another doc comment on add3
 let add3 (x y z: u32)
     : Prims.Pure u32
       (requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max)

test-harness/src/snapshots/toolchain__generics into-fstar.snap

@@ -63,6 +63,7 @@ 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)
 

test-harness/src/snapshots/toolchain__include-flag into-fstar.snap

@@ -34,12 +34,14 @@ open FStar.Mul
 
 class t_Trait (v_Self: Type) = { __marker_trait_t_Trait:Prims.unit }
 
+/// Indirect dependencies
 let main_a_a (_: Prims.unit) : Prims.unit = ()
 
 let main_a_b (_: Prims.unit) : Prims.unit = ()
 
 let main_a_c (_: Prims.unit) : Prims.unit = ()
 
+/// Direct dependencies
 let main_a (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T)
     : Prims.unit =
   let _:Prims.unit = main_a_a () in
@@ -76,6 +78,7 @@ type t_Foo = | Foo : t_Foo
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () }
 
+/// Entrypoint
 let main (_: Prims.unit) : Prims.unit =
   let _:Prims.unit = main_a (Foo <: t_Foo) in
   let _:Prims.unit = main_b () in

test-harness/src/snapshots/toolchain__interface-only into-fstar.snap

@@ -35,6 +35,11 @@ module Interface_only
 open Core
 open FStar.Mul
 
+/// This item contains unsafe blocks and raw references, two features
+/// not supported by hax. Thanks to the `-i` flag and the `+:`
+/// modifier, `f` is still extractable as an interface.
+/// Expressions within type are still extracted, as well as pre- and
+/// post-conditions.
 val f (x: u8)
     : Prims.Pure (t_Array u8 (sz 4))
       (requires x <. 254uy)
@@ -45,6 +50,9 @@ val f (x: u8)
 
 type t_Bar = | Bar : t_Bar
 
+/// Non-inherent implementations are extracted, their bodies are not
+/// dropped. This might be a bit surprising: see
+/// https://github.com/hacspec/hax/issues/616.
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl: Core.Convert.t_From t_Bar Prims.unit =
   {
@@ -55,6 +63,7 @@ let impl: Core.Convert.t_From t_Bar Prims.unit =
 
 val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True)
 
+/// If you need to drop the body of a method, please hoist it:
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_1: Core.Convert.t_From t_Bar u8 =
   {

test-harness/src/snapshots/toolchain__naming into-fstar.snap

@@ -32,6 +32,8 @@ 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 =
@@ -56,6 +58,7 @@ let debug (label value: u32) : Prims.unit =
   in
   ()
 
+/// `f` stacks mutliple let bindings declaring different `a`s.
 let f (_: Prims.unit) : Prims.unit =
   let a_1_:u32 = 104ul in
   let a_2_:u32 = 205ul in
@@ -66,6 +69,13 @@ let f (_: Prims.unit) : Prims.unit =
   let _:Prims.unit = debug 1ul a_1_ in
   debug 4ul a
 
+/// `f` is expanded into `f_expand` below, while the execution of `f` gives:
+/// ```plaintext
+///  [3] a=306
+///  [2] a=205
+///  [1] a=104
+///  [last] a=123
+/// ```
 let ff_expand (_: Prims.unit) : Prims.unit =
   let a:i32 = 104l in
   let a:i32 = 205l in
@@ -117,6 +127,10 @@ 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