Parse doc comments on mapping clauses

Allows round-tripping mapping doc comments through the pretty-printer

Previously, some doc comments would be silently stripped by descattering
as there is nowhere for them to go. While this patch and previous ones
address some of these issues there are still a few places where this is
unavoidable, so warn when that occurs.

Adjust the syntax of doc comments slightly to address formatting issues:

* Nested comments are now preserved in the documentation string

* We allow doc comments to be written with leading asterisks, i.e.

  /*!
   * Some doc comment
   * with leading asterisks
   */

  These asterisks (and a space on each side)  will be stripped out, so the above is equivalent to:

  /*!
  Some doc comment
  with leading asterisks
  */

  In order for an asterisk to be recognized, it must now be preceded
  by a newline, then 1 or more whitespace characters, and followed by exactly 1
  whitespace character, before the comment continues. This sequence will
  be replaced by a newline followed by the whitespace with the final
  " * " sequence removed.

  Previously it was 0 or more whitespace characters before the asterisk,
  and the whitespace after was optional.

src/lib/ast_util.ml

@@ -87,7 +87,7 @@ let get_attributes annot = annot.attrs
 let find_attribute_opt attr1 attrs =
   List.find_opt (fun (_, attr2, _) -> attr1 = attr2) attrs |> Option.map (fun (_, _, arg) -> arg)
 
-let mk_def_annot l = { doc_comment = None; attrs = []; loc = l }
+let mk_def_annot ?doc ?(attrs = []) l = { doc_comment = doc; attrs; loc = l }
 
 let map_clause_annot f (def_annot, annot) =
   let l, annot' = f (def_annot.loc, annot) in

src/lib/ast_util.mli

@@ -97,7 +97,7 @@ val get_attributes : uannot -> (l * string * string) list
 
 val find_attribute_opt : string -> (l * string * string) list -> string option
 
-val mk_def_annot : l -> def_annot
+val mk_def_annot : ?doc:string -> ?attrs:(l * string * string) list -> l -> def_annot
 
 val add_def_attribute : l -> string -> string -> def_annot -> def_annot
 

src/lib/initial_check.ml

@@ -862,12 +862,10 @@ let rec to_ast_type_union doc attrs ctx = function
       | Some _ -> raise (Reporting.err_general l "Union constructor has multiple documentation comments")
       | None -> to_ast_type_union (Some doc_comment) attrs ctx tu
     end
-  | P.Tu_aux (P.Tu_attribute (attr, arg, tu), l) -> to_ast_type_union doc ((attr, arg, l) :: attrs) ctx tu
+  | P.Tu_aux (P.Tu_attribute (attr, arg, tu), l) -> to_ast_type_union doc (attrs @ [(l, attr, arg)]) ctx tu
   | P.Tu_aux (P.Tu_ty_id (atyp, id), l) ->
-      let annot = List.fold_left (fun a (attr, arg, l) -> add_def_attribute l attr arg a) (mk_def_annot l) attrs in
-      let annot = { annot with doc_comment = doc } in
       let typ = to_ast_typ ctx atyp in
-      Tu_aux (Tu_ty_id (typ, to_ast_id ctx id), annot)
+      Tu_aux (Tu_ty_id (typ, to_ast_id ctx id), mk_def_annot ?doc ~attrs l)
   | P.Tu_aux (_, l) ->
       raise (Reporting.err_unreachable l __POS__ "Anonymous record type should have been rewritten by now")
 
@@ -1083,14 +1081,14 @@ let to_ast_typschm_opt ctx (P.TypSchm_opt_aux (aux, l)) : tannot_opt ctx_out =
 
 let rec to_ast_funcl doc attrs ctx (P.FCL_aux (fcl, l) : P.funcl) : uannot funcl =
   match fcl with
-  | P.FCL_attribute (attr, arg, fcl) -> to_ast_funcl doc ((attr, arg, l) :: attrs) ctx fcl
+  | P.FCL_attribute (attr, arg, fcl) -> to_ast_funcl doc (attrs @ [(l, attr, arg)]) ctx fcl
   | P.FCL_doc (doc_comment, fcl) -> begin
       match doc with
       | Some _ -> raise (Reporting.err_general l "Function clause has multiple documentation comments")
       | None -> to_ast_funcl (Some doc_comment) attrs ctx fcl
     end
   | P.FCL_funcl (id, pexp) ->
-      FCL_aux (FCL_funcl (to_ast_id ctx id, to_ast_case ctx pexp), (mk_def_annot l, empty_uannot))
+      FCL_aux (FCL_funcl (to_ast_id ctx id, to_ast_case ctx pexp), (mk_def_annot ?doc ~attrs l, empty_uannot))
 
 let to_ast_impl_funcls ctx (P.FCL_aux (fcl, l) : P.funcl) : uannot funcl list =
   match fcl with
@@ -1141,21 +1139,26 @@ let to_ast_mpexp ctx (P.MPat_aux (mpexp, l)) =
   | P.MPat_pat mpat -> MPat_aux (MPat_pat (to_ast_mpat ctx mpat), (l, empty_uannot))
   | P.MPat_when (mpat, exp) -> MPat_aux (MPat_when (to_ast_mpat ctx mpat, to_ast_exp ctx exp), (l, empty_uannot))
 
-let to_ast_mapcl ctx (P.MCL_aux (mapcl, l)) =
-  let def_annot = mk_def_annot l in
+let rec to_ast_mapcl doc attrs ctx (P.MCL_aux (mapcl, l)) =
   match mapcl with
+  | P.MCL_attribute (attr, arg, mcl) -> to_ast_mapcl doc (attrs @ [(l, attr, arg)]) ctx mcl
+  | P.MCL_doc (doc_comment, mcl) -> begin
+      match doc with
+      | Some _ -> raise (Reporting.err_general l "Function clause has multiple documentation comments")
+      | None -> to_ast_mapcl (Some doc_comment) attrs ctx mcl
+    end
   | P.MCL_bidir (mpexp1, mpexp2) ->
-      MCL_aux (MCL_bidir (to_ast_mpexp ctx mpexp1, to_ast_mpexp ctx mpexp2), (def_annot, empty_uannot))
+      MCL_aux (MCL_bidir (to_ast_mpexp ctx mpexp1, to_ast_mpexp ctx mpexp2), (mk_def_annot ?doc ~attrs l, empty_uannot))
   | P.MCL_forwards (mpexp, exp) ->
-      MCL_aux (MCL_forwards (to_ast_mpexp ctx mpexp, to_ast_exp ctx exp), (def_annot, empty_uannot))
+      MCL_aux (MCL_forwards (to_ast_mpexp ctx mpexp, to_ast_exp ctx exp), (mk_def_annot ?doc ~attrs l, empty_uannot))
   | P.MCL_backwards (mpexp, exp) ->
-      MCL_aux (MCL_backwards (to_ast_mpexp ctx mpexp, to_ast_exp ctx exp), (def_annot, empty_uannot))
+      MCL_aux (MCL_backwards (to_ast_mpexp ctx mpexp, to_ast_exp ctx exp), (mk_def_annot ?doc ~attrs l, empty_uannot))
 
 let to_ast_mapdef ctx (P.MD_aux (md, l) : P.mapdef) : uannot mapdef =
   match md with
   | P.MD_mapping (id, typschm_opt, mapcls) ->
       let tannot_opt, ctx = to_ast_typschm_opt ctx typschm_opt in
-      MD_aux (MD_mapping (to_ast_id ctx id, tannot_opt, List.map (to_ast_mapcl ctx) mapcls), (l, empty_uannot))
+      MD_aux (MD_mapping (to_ast_id ctx id, tannot_opt, List.map (to_ast_mapcl None [] ctx) mapcls), (l, empty_uannot))
 
 let to_ast_dec ctx (P.DEC_aux (regdec, l)) =
   DEC_aux
@@ -1214,7 +1217,7 @@ let to_ast_scattered ctx (P.SD_aux (aux, l)) =
         (None, SD_mapping (id, tannot_opt), ctx)
     | P.SD_mapcl (id, mapcl) ->
         let id = to_ast_id ctx id in
-        let mapcl = to_ast_mapcl ctx mapcl in
+        let mapcl = to_ast_mapcl None [] ctx mapcl in
         (None, SD_mapcl (id, mapcl), ctx)
     | P.SD_enum id ->
         let id = to_ast_id ctx id in
@@ -1236,11 +1239,19 @@ let to_ast_loop_measure ctx = function
   | P.Loop (P.While, exp) -> Loop (While, to_ast_exp ctx exp)
   | P.Loop (P.Until, exp) -> Loop (Until, to_ast_exp ctx exp)
 
+(* Annotations on some scattered constructs will not be preserved after de-scattering, so warn about this *)
+let check_annotation (DEF_aux (aux, def_annot)) =
+  if Option.is_some def_annot.doc_comment || not (Util.list_empty def_annot.attrs) then (
+    match aux with
+    | DEF_scattered (SD_aux ((SD_function _ | SD_mapping _ | SD_end _), _)) ->
+        Reporting.warn "" def_annot.loc "Documentation comments and attributes will not be preserved on this definition"
+    | _ -> ()
+  )
+
 let rec to_ast_def doc attrs ctx (P.DEF_aux (def, l)) : uannot def list ctx_out =
-  let annot = List.fold_left (fun a (attr, arg, l) -> add_def_attribute l attr arg a) (mk_def_annot l) attrs in
-  let annot = { annot with doc_comment = doc } in
+  let annot = mk_def_annot ?doc ~attrs l in
   match def with
-  | P.DEF_attribute (attr, arg, def) -> to_ast_def doc ((attr, arg, l) :: attrs) ctx def
+  | P.DEF_attribute (attr, arg, def) -> to_ast_def doc (attrs @ [(l, attr, arg)]) ctx def
   | P.DEF_doc (doc_comment, def) -> begin
       match doc with
       | Some _ -> raise (Reporting.err_general l "Toplevel definition has multiple documentation comments")
@@ -1336,8 +1347,9 @@ let to_ast ctx (P.Defs files) =
     let defs, ctx =
       List.fold_left
         (fun (defs, ctx) def ->
-          let def, ctx = to_ast_def None [] ctx def in
-          (def @ defs, ctx)
+          let new_defs, ctx = to_ast_def None [] ctx def in
+          List.iter check_annotation new_defs;
+          (new_defs @ defs, ctx)
         )
         ([], ctx) defs
     in

src/lib/lexer.mll

@@ -232,7 +232,7 @@ rule token = parse
   | "-"                                 { Minus }
   | "<->"                               { Bidir }
   | "=>"                                { EqGt "=>" }
-  | "/*!" wsc*  { Doc (doc_comment (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) 0 false lexbuf) }
+  | "/*!"       { Doc (doc_comment (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) 0 false lexbuf) }
   | "//"        { line_comment (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf; token lexbuf }
   | "/*"        { comment (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) 0 lexbuf; token lexbuf }
   | "*/"        { raise (Reporting.err_lex (Lexing.lexeme_start_p lexbuf) "Unbalanced comment") }
@@ -302,19 +302,22 @@ and line_comment pos b = parse
   | eof                                 { raise (Reporting.err_lex pos "File ended before newline in comment") }
 
 and doc_comment pos b depth lstart = parse
-  | "/*!"                               { doc_comment pos b (depth + 1) false lexbuf }
-  | "/*"                                { doc_comment pos b (depth + 1) false lexbuf }
-  | wsc* "*/"                           { if depth = 0 then Buffer.contents b
-					  else if depth > 0 then doc_comment pos b (depth - 1) false lexbuf
-					  else assert false }
-  | eof                                 { raise (Reporting.err_lex pos "Unbalanced comment") }
+  | "/*!"                               { Buffer.add_string b "/*!"; doc_comment pos b (depth + 1) false lexbuf }
+  | "/*"                                { Buffer.add_string b "/*"; doc_comment pos b (depth + 1) false lexbuf }
+  | "*/"                                { if depth = 0 then Buffer.contents b
+					  else (
+                                            Buffer.add_string b "*/";
+                                            doc_comment pos b (depth - 1) false lexbuf
+					  ) }
   | "\n"                                { Buffer.add_string b "\n"; Lexing.new_line lexbuf; doc_comment pos b depth true lexbuf }
-  | wsc* "*" wsc? as prefix             { if lstart then (
+  | wsc+ "*" wsc as prefix              { if lstart then (
+                                            Buffer.add_string b (String.make (String.length prefix - 3) ' ');
                                             doc_comment pos b depth false lexbuf
                                           ) else (
                                             Buffer.add_string b prefix; doc_comment pos b depth false lexbuf
                                           ) }
   | _ as c                              { Buffer.add_string b (String.make 1 c); doc_comment pos b depth false lexbuf }
+  | eof                                 { raise (Reporting.err_lex pos "Unbalanced documentation comment") }
 
 and comment pos b depth = parse
   | "/*"                                { comment pos b (depth + 1) lexbuf }

src/lib/parse_ast.ml

@@ -372,14 +372,16 @@ type mpexp_aux = MPat_pat of mpat | MPat_when of mpat * exp
 
 type mpexp = MPat_aux of mpexp_aux * l
 
-type mapcl_aux =
+type mapcl = MCL_aux of mapcl_aux * l
+
+and mapcl_aux =
   (* mapping clause (bidirectional pattern-match) *)
+  | MCL_attribute of string * string * mapcl
+  | MCL_doc of string * mapcl
   | MCL_bidir of mpexp * mpexp
   | MCL_forwards of mpexp * exp
   | MCL_backwards of mpexp * exp
 
-type mapcl = MCL_aux of mapcl_aux * l
-
 type mapdef_aux =
   (* mapping definition (bidirectional pattern-match function) *)
   | MD_mapping of id * typschm_opt * mapcl list

src/lib/parser.mly

@@ -1166,6 +1166,10 @@ fmpat:
     { mk_mpexp (MPat_when ($1, $3)) $startpos $endpos }
 
 mapcl:
+  | attr = Attribute; mcl = mapcl
+    { MCL_aux (MCL_attribute (fst attr, snd attr, mcl), loc $startpos(attr) $endpos(attr)) }
+  | doc = Doc; mcl = mapcl
+    { MCL_aux (MCL_doc (doc, mcl), loc $startpos(doc) $endpos(doc)) }
   | mpexp Bidir mpexp
     { mk_bidir_mapcl $1 $3 $startpos $endpos }
   | mpexp EqGt exp

src/lib/pretty_print_sail.ml

@@ -84,8 +84,6 @@ let doc_kid kid = string (Ast_util.string_of_kid kid)
 let doc_attr attr arg =
   if arg = "" then Printf.ksprintf string "$[%s]" attr ^^ space else Printf.ksprintf string "$[%s %s]" attr arg ^^ space
 
-let get_column l = match Reporting.simp_loc l with Some (l1, _) -> Some (l1.pos_cnum - l1.pos_bol) | None -> None
-
 let doc_def_annot def_annot =
   (match def_annot.doc_comment with Some str -> string "/*!" ^^ string str ^^ string "*/" ^^ hardline | _ -> empty)
   ^^
@@ -202,7 +200,7 @@ and doc_typ ?(simple = false) (Typ_aux (typ_aux, l)) =
         Typ_aux (Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var kid2, _)), _)]), _)
       )
     when Kid.compare (kopt_kid kopt) kid1 == 0 && Kid.compare kid1 kid2 == 0 && Id.compare (mk_id "atom") id == 0 ->
-      enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints)
+      enclose (char '{') (char '}') (separate_map (string ", ") doc_int ints)
   | Typ_exist (kopts, nc, typ) ->
       braces (separate_map space doc_kopt kopts ^^ comma ^^ space ^^ doc_nc nc ^^ dot ^^ space ^^ doc_typ typ)
   | Typ_fn ([Typ_aux (Typ_tuple typs, _)], typ) ->
@@ -626,7 +624,9 @@ let doc_mpexp (MPat_aux (mpexp, _)) =
   | MPat_pat mpat -> doc_mpat mpat
   | MPat_when (mpat, guard) -> doc_mpat mpat ^^ space ^^ string "if" ^^ space ^^ doc_exp guard
 
-let doc_mapcl (MCL_aux (cl, _)) =
+let doc_mapcl (MCL_aux (cl, (def_annot, _))) =
+  doc_def_annot def_annot
+  ^^
   match cl with
   | MCL_bidir (mpexp1, mpexp2) ->
       let left = doc_mpexp mpexp1 in

test/lexing/doc_comment_eof.expect

@@ -2,4 +2,4 @@
 doc_comment_eof.sail:3.0-0:
 3 |/*! doc
   |^
-  | Unbalanced comment
+  | Unbalanced documentation comment

test/typecheck/pass/scattered_mapping_doc.sail

@@ -0,0 +1,25 @@
+default Order dec
+
+$include <prelude.sail>
+
+enum E = A | B | C
+
+/*! Documentation
+ * comment
+ * with
+ * asterisks
+ */
+val foo : E <-> int
+
+scattered mapping foo
+
+/*! Mapping clause doc comment /* nested */ */
+mapping clause foo = A <-> 3
+
+/*! Mapping clause
+ * box style
+ * comment */
+mapping clause foo = B <-> 2
+
+$[some_attribute]
+mapping clause foo = C <-> 1