diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml index be279f035..576daa42a 100644 --- a/src/lib/ast_util.ml +++ b/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 diff --git a/src/lib/ast_util.mli b/src/lib/ast_util.mli index a35489df3..c372d068b 100644 --- a/src/lib/ast_util.mli +++ b/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 diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml index def89e209..23de56ca0 100644 --- a/src/lib/initial_check.ml +++ b/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 diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll index 82131731d..666ecc36f 100644 --- a/src/lib/lexer.mll +++ b/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 } diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml index 6bfe06a9d..f464f6a17 100644 --- a/src/lib/parse_ast.ml +++ b/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 diff --git a/src/lib/parser.mly b/src/lib/parser.mly index 25ef5ff1b..751b7a369 100644 --- a/src/lib/parser.mly +++ b/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 diff --git a/src/lib/pretty_print_sail.ml b/src/lib/pretty_print_sail.ml index a10473f97..056533ee5 100644 --- a/src/lib/pretty_print_sail.ml +++ b/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 diff --git a/test/lexing/doc_comment_eof.expect b/test/lexing/doc_comment_eof.expect index 1adc89215..61a9e9405 100644 --- a/test/lexing/doc_comment_eof.expect +++ b/test/lexing/doc_comment_eof.expect @@ -2,4 +2,4 @@ doc_comment_eof.sail:3.0-0: 3 |/*! doc  |^ -  | Unbalanced comment +  | Unbalanced documentation comment diff --git a/test/typecheck/pass/scattered_mapping_doc.sail b/test/typecheck/pass/scattered_mapping_doc.sail new file mode 100644 index 000000000..99ebb0653 --- /dev/null +++ b/test/typecheck/pass/scattered_mapping_doc.sail @@ -0,0 +1,25 @@ +default Order dec + +$include + +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