Skip to content

Commit

Permalink
Some further documentation improvements
Browse files Browse the repository at this point in the history
We will now resugar `v[n]` and `v[n..m]` after splitting. Non overloaded
operators are handled better.

Wavedrom generation now handles submappings in a somewhat sensible way.
  • Loading branch information
Alasdair committed May 11, 2024
1 parent 2725bc8 commit bbd46b8
Show file tree
Hide file tree
Showing 5 changed files with 23 additions and 2 deletions.
2 changes: 2 additions & 0 deletions src/lib/ast_util.ml
Original file line number Diff line number Diff line change
Expand Up @@ -997,6 +997,8 @@ let def_loc (DEF_aux (_, annot)) = annot.loc

let deinfix = function Id_aux (Id v, l) -> Id_aux (Operator v, l) | Id_aux (Operator v, l) -> Id_aux (Operator v, l)

let infix_swap = function Id_aux (Id v, l) -> Id_aux (Operator v, l) | Id_aux (Operator v, l) -> Id_aux (Id v, l)

let id_of_kid = function Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)

let kid_of_id = function Id_aux (Id v, l) -> Kid_aux (Var ("'" ^ v), l) | Id_aux (Operator _, _) -> assert false
Expand Down
1 change: 1 addition & 0 deletions src/lib/ast_util.mli
Original file line number Diff line number Diff line change
Expand Up @@ -498,6 +498,7 @@ val id_of_dec_spec : 'a dec_spec -> id
(** {2 Functions for manipulating identifiers} *)

val deinfix : id -> id
val infix_swap : id -> id

val id_of_kid : kid -> id
val kid_of_id : id -> kid
Expand Down
12 changes: 11 additions & 1 deletion src/lib/pretty_print_sail.ml
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,7 @@ module Big_int = Nat_big_num
module type PRINT_CONFIG = sig
val insert_braces : bool
val resugar : bool
val hide_attributes : bool
end

module Printer (Config : PRINT_CONFIG) = struct
Expand Down Expand Up @@ -401,6 +402,7 @@ module Printer (Config : PRINT_CONFIG) = struct
if Config.resugar && Option.is_some (get_attribute "setter" uannot) then (remove_attribute "setter" uannot, true)
else (uannot, false)
in
let uannot = if Config.hide_attributes then empty_uannot else uannot in
concat_map (fun (_, attr, arg) -> doc_attr attr arg) (get_attributes uannot)
^^
match e_aux with
Expand Down Expand Up @@ -503,7 +505,13 @@ module Printer (Config : PRINT_CONFIG) = struct
match (overloaded, exps) with
| Some (name, true), [x; y] -> doc_exp (E_aux (E_app_infix (x, mk_id name, y), (l, uannot)))
| Some (name, false), _ ->
handle_setter (mk_id name) (lazy (doc_atomic_exp (E_aux (E_app (mk_id name, exps), (l, uannot)))))
handle_setter (mk_id name) (lazy (doc_exp (E_aux (E_app (mk_id name, exps), (l, uannot)))))
| None, [x; y] when Config.resugar && match id with Id_aux (Operator _, _) -> true | _ -> false ->
doc_exp (E_aux (E_app_infix (x, infix_swap id, y), (l, uannot)))
| None, [v; n] when Config.resugar && Id.compare id (mk_id "vector_access") = 0 ->
doc_atomic_exp v ^^ char '[' ^^ doc_exp n ^^ char ']'
| None, [v; n; m] when Config.resugar && Id.compare id (mk_id "vector_subrange") = 0 ->
doc_atomic_exp v ^^ char '[' ^^ doc_exp n ^^ space ^^ string ".." ^^ space ^^ doc_exp m ^^ char ']'
| _, _ -> handle_setter id (lazy (doc_atomic_exp exp))
end
| _ -> doc_atomic_exp exp
Expand Down Expand Up @@ -888,6 +896,7 @@ let reformat dir { defs; _ } =
let module Reformatter = Printer (struct
let insert_braces = true
let resugar = true
let hide_attributes = false
end) in
let file_stack = ref [] in

Expand Down Expand Up @@ -938,6 +947,7 @@ let reformat dir { defs; _ } =
module Default_print_config : PRINT_CONFIG = struct
let insert_braces = false
let resugar = false
let hide_attributes = false
end

include Printer (Default_print_config)
Expand Down
1 change: 1 addition & 0 deletions src/sail_doc_backend/docinfo.ml
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,7 @@ open Parse_ast.Attribute_data
module Reformatter = Pretty_print_sail.Printer (struct
let insert_braces = true
let resugar = true
let hide_attributes = true
end)

(** In the case of latex, we generate files containing a sequence of
Expand Down
9 changes: 8 additions & 1 deletion src/sail_doc_backend/wavedrom.ml
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,10 @@ let binary_to_hex str =
let rec wavedrom_elem_string size label (P_aux (aux, _)) =
match aux with
| P_id id ->
Printf.sprintf " { bits: %d, name: '%s'%s, type: 2 }" size (string_of_id id) (wavedrom_label size label)
let name = string_of_id id in
if String.starts_with ~prefix:"imm" name then
Printf.sprintf " { bits: %d, name: '%s'%s, type: 6 }" size (string_of_id id) (wavedrom_label size label)
else Printf.sprintf " { bits: %d, name: '%s'%s, type: 2 }" size (string_of_id id) (wavedrom_label size label)
| P_lit (L_aux (L_bin bin, _)) ->
Printf.sprintf " { bits: %d, name: 0x%s%s, type: 8 }" size (binary_to_hex bin) (wavedrom_label size label)
| P_lit (L_aux (L_hex hex, _)) ->
Expand All @@ -112,6 +115,10 @@ let rec wavedrom_elem_string size label (P_aux (aux, _)) =
| P_vector_subrange (id, n, m) ->
Printf.sprintf " { bits: %d, name: '%s[%s..%s]'%s, type: 3 }" size (string_of_id id) (Big_int.to_string n)
(Big_int.to_string m) (wavedrom_label size label)
| P_app (id, [P_aux (P_id arg, _)]) ->
Printf.sprintf " { bits: %d, name: '%s'%s, type: 4 }" size (string_of_id arg) (wavedrom_label size label)
| P_app (id, _) ->
Printf.sprintf " { bits: %d, name: '%s'%s, type: 7 }" size (string_of_id id) (wavedrom_label size label)
| P_as (pat, _) | P_typ (_, pat) -> wavedrom_elem_string size label pat
| _ -> raise Invalid_wavedrom

Expand Down

0 comments on commit bbd46b8

Please sign in to comment.