Add attributes to sail_doc_backend output

Rename _to_json to json_of_ to better match other usages

Refactor Pretty_print_sail, adding a Pretty_print_sail.Printer functor
which can be configured for different use cases. The module contains a

include Printer (Default_print_config)

so other code can just use Pretty_print_sail as before.

The main use for this is in the documentation generation, as we want
to be able to format code slightly differently than when we just dump
the AST for debugging, e.g. re-introduce overloads. This is handled by
the `resugar` flag in the pretty-printer config.

The eventual ideal flow would be:

constant-propagate -> pretty_print w/ resugar -> re-parse -> format_sail

but we don't yet do the last two steps

src/lib/ast_util.ml

@@ -82,13 +82,33 @@ let rec string_of_attribute_data (AD_aux (aux, _)) =
       ^ " }"
   | AD_string s -> "\"" ^ s ^ "\""
   | AD_num n -> Big_int.to_string n
-  | AD_list cs -> "[" ^ Util.string_of_list ", " string_of_attribute_data cs ^ "]"
+  | AD_list vs -> "[" ^ Util.string_of_list ", " string_of_attribute_data vs ^ "]"
   | AD_bool b -> string_of_bool b
 
 let string_of_attribute attr = function
   | None -> Printf.sprintf "$[%s]" attr
   | Some data -> Printf.sprintf "$[%s %s]" attr (string_of_attribute_data data)
 
+let rec json_of_attribute_data (AD_aux (aux, _)) =
+  match aux with
+  | AD_object kvs -> `Assoc (List.map (fun (k, v) -> (k, json_of_attribute_data v)) kvs)
+  | AD_string s -> `String s
+  | AD_num n when Big_int.less_equal (Big_int.of_int min_int) n && Big_int.less_equal n (Big_int.of_int max_int) ->
+      `Int (Big_int.to_int n)
+  | AD_num n -> `String (Big_int.to_string n)
+  | AD_list vs -> `List (List.map json_of_attribute_data vs)
+  | AD_bool b -> `Bool b
+
+let attribute_data_object = function AD_aux (AD_object kvs, _) -> Some kvs | _ -> None
+
+let attribute_data_bool = function AD_aux (AD_bool b, _) -> Some b | _ -> None
+
+let attribute_data_string = function AD_aux (AD_string s, _) -> Some s | _ -> None
+
+let json_of_attribute attr = function
+  | None -> `String attr
+  | Some data -> `List [`String attr; json_of_attribute_data data]
+
 let empty_uannot = { attrs = [] }
 
 let add_attribute l attr arg (annot : uannot) = { attrs = (l, attr, arg) :: annot.attrs }

src/lib/ast_util.mli

@@ -78,12 +78,25 @@ module Big_int = Nat_big_num
    annotations {!Type_check.tannot}. *)
 type uannot
 
+(** The empty annotation *)
 val empty_uannot : uannot
 
+(** {2 Attributes} *)
+
 val string_of_attribute : string -> attribute_data option -> string
 
 val string_of_attribute_data : attribute_data -> string
 
+val json_of_attribute : string -> attribute_data option -> Yojson.Basic.t
+
+val json_of_attribute_data : attribute_data -> Yojson.Basic.t
+
+val attribute_data_object : attribute_data -> (string * attribute_data) list option
+
+val attribute_data_bool : attribute_data -> bool option
+
+val attribute_data_string : attribute_data -> string option
+
 (** Add an attribute to an annotation. Attributes are attached to expressions in Sail  via:
     {@sail[
     $[attribute argument] expression
@@ -118,6 +131,8 @@ val def_annot_map_loc : (l -> l) -> def_annot -> def_annot
    information with the various [locate_] functions in this module. *)
 val no_annot : l * uannot
 
+(** {1 Generated locations} *)
+
 (** [gen_loc l] takes a location l and generates a location which
    means 'generated/derived from location l'. This is useful for debugging
    errors that occur in generated code. *)