Further documentation improvements

src/bin/repl.ml

@@ -430,7 +430,7 @@ let handle_input' istate input =
         | ":n" | ":normal" -> { istate with mode = Normal }
         | ":t" | ":type" ->
             let typq, typ = Type_check.Env.get_val_spec (mk_id arg) istate.env in
-            pretty_sail stdout (doc_binding (typq, typ));
+            Document.to_channel stdout (doc_binding (typq, typ));
             print_newline ();
             istate
         | ":q" | ":quit" ->
@@ -439,7 +439,7 @@ let handle_input' istate input =
         | ":i" | ":infer" ->
             let exp = Initial_check.exp_of_string arg in
             let exp = Type_check.infer_exp istate.env exp in
-            pretty_sail stdout (doc_typ (Type_check.typ_of exp));
+            Document.to_channel stdout (doc_typ (Type_check.typ_of exp));
             print_newline ();
             istate
         | ":prove" ->
@@ -497,7 +497,7 @@ let handle_input' istate input =
            *)
         | ":ast" ->
             let chan = open_out arg in
-            Pretty_print_sail.pp_ast chan (Type_check.strip_ast istate.ast);
+            Pretty_print_sail.output_ast chan (Type_check.strip_ast istate.ast);
             close_out chan;
             istate
         | ":output" ->

src/lib/ast_util.ml

@@ -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

src/lib/ast_util.mli

@@ -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

src/lib/frontend.ml

@@ -81,7 +81,7 @@ let check_ast (asserts_termination : bool) (env : Type_check.Env.t) (ast : uanno
   let ast = Scattered.descatter ast in
   let side_effects = Effects.infer_side_effects asserts_termination ast in
   Effects.check_side_effects side_effects ast;
-  let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_ast stdout (Type_check.strip_ast ast) else () in
+  let () = if !opt_ddump_tc_ast then Pretty_print_sail.output_ast stdout (Type_check.strip_ast ast) else () in
   (ast, env, side_effects)
 
 let instantiate_abstract_types insts ast =
@@ -125,12 +125,12 @@ let wrap_module proj parsed_module =
   |> Util.update_last (fun (f, (comments, defs)) -> (f, (comments, defs @ [bracket_pragma "end_module#"])))
 
 let process_ast target type_envs ast =
-  if !opt_ddump_initial_ast then Pretty_print_sail.pp_ast stdout ast;
+  if !opt_ddump_initial_ast then Pretty_print_sail.output_ast stdout ast;
 
   begin
     match !opt_reformat with
     | Some dir ->
-        Pretty_print_sail.reformat dir ast;
+        Pretty_print_sail.reformat ~into_directory:dir ast;
         exit 0
     | None -> ()
   end;

src/lib/interpreter.ml

@@ -69,6 +69,13 @@ open Ast
 open Ast_defs
 open Ast_util
 open Value
+module Document = Pretty_print_sail.Document
+
+module Printer = Pretty_print_sail.Printer (struct
+  let insert_braces = false
+  let resugar = false
+  let hide_attributes = true
+end)
 
 type gstate = {
   registers : value Bindings.t;
@@ -791,7 +798,7 @@ let rec eval_frame' = function
       | Pure v, head :: stack' when is_value v ->
           Step (stack_string head, (stack_state head, gstate), stack_cont head (Return_ok (value_of_exp v)), stack')
       | Pure exp', _ ->
-          let out' = lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp (Type_check.strip_exp exp'))) in
+          let out' = lazy (Document.to_string (Printer.doc_exp (Type_check.strip_exp exp'))) in
           Step (out', state, step exp', stack)
       | Yield (Call (id, vals, cont)), _ when string_of_id id = "break" -> begin
           let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in
@@ -1001,22 +1008,12 @@ let analyse_instruction state ast =
          [id_typ "regfps"; id_typ "regfps"; id_typ "regfps"; id_typ "niafps"; id_typ "diafp"; id_typ "instruction_kind"]
       )
   in
-  Step
-    ( lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp (Type_check.strip_exp typed))),
-      state,
-      return typed,
-      []
-    )
+  Step (lazy (Document.to_string (Printer.doc_exp (Type_check.strip_exp typed))), state, return typed, [])
 
 let execute_instruction state ast =
   let env = (snd state).typecheck_env in
   let unk = Parse_ast.Unknown in
   let typed =
     annot_exp (E_app (mk_id "execute", [annot_exp (E_internal_value ast) unk env (id_typ "ast")])) unk env unit_typ
   in
-  Step
-    ( lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp (Type_check.strip_exp typed))),
-      state,
-      return typed,
-      []
-    )
+  Step (lazy (Document.to_string (Printer.doc_exp (Type_check.strip_exp typed))), state, return typed, [])

src/lib/jib_compile.ml

@@ -74,6 +74,7 @@ open Jib_util
 open Jib_visitor
 open Type_check
 open Value2
+module Document = Pretty_print_sail.Document
 
 open Anf
 
@@ -553,7 +554,7 @@ module Make (C : CONFIG) = struct
     | AV_vector _ as aval ->
         raise
           (Reporting.err_general l
-             ("Have AVL_vector: " ^ Pretty_print_sail.to_string (pp_aval aval) ^ " which is not a vector type")
+             ("Have AVL_vector: " ^ Document.to_string (pp_aval aval) ^ " which is not a vector type")
           )
     | AV_list (avals, Typ_aux (typ, _)) ->
         let ctyp =
@@ -1464,7 +1465,7 @@ module Make (C : CONFIG) = struct
   let rec compile_def n total ctx (DEF_aux (aux, _) as def) =
     match aux with
     | DEF_fundef (FD_aux (FD_function (_, _, [FCL_aux (FCL_funcl (id, _), _)]), _)) when !opt_memo_cache ->
-        let digest = strip_def def |> Pretty_print_sail.doc_def |> Pretty_print_sail.to_string |> Digest.string in
+        let digest = strip_def def |> Pretty_print_sail.doc_def |> Document.to_string |> Digest.string in
         let cachefile = Filename.concat "_sbuild" ("ccache" ^ Digest.to_hex digest) in
         let cached =
           if Sys.file_exists cachefile then (
@@ -1577,7 +1578,7 @@ module Make (C : CONFIG) = struct
     (* Scattereds, mapdefs, and event related definitions should be removed by this point *)
     | DEF_scattered _ | DEF_mapdef _ | DEF_outcome _ | DEF_impl _ | DEF_instantiation _ ->
         Reporting.unreachable (def_loc def) __POS__
-          ("Could not compile:\n" ^ Pretty_print_sail.to_string (Pretty_print_sail.doc_def (strip_def def)))
+          ("Could not compile:\n" ^ Document.to_string (Pretty_print_sail.doc_def (strip_def def)))
     | DEF_constraint _ -> Reporting.unreachable (def_loc def) __POS__ "Toplevel constraint not supported"
 
   let mangle_mono_id id ctx ctyps = append_id id ("<" ^ Util.string_of_list "," (mangle_string_of_ctyp ctx) ctyps ^ ">")

src/lib/jib_util.ml

@@ -71,6 +71,7 @@ open Jib
 open Jib_visitor
 open Value2
 open PPrint
+module Document = Pretty_print_sail.Document
 
 let symbol_generator str =
   let counter = ref 0 in
@@ -377,7 +378,7 @@ let rec doc_instr (I_aux (aux, _)) =
       ^^ nest 2 (hardline ^^ separate_map hardline doc_instr else_instrs)
       ^^ hardline ^^ twice space ^^ char '}'
 
-let string_of_instr i = Pretty_print_sail.to_string (doc_instr i)
+let string_of_instr i = Document.to_string (doc_instr i)
 
 let rec map_ctyp f = function
   | ( CT_lint | CT_fint _ | CT_constant _ | CT_lbits | CT_fbits _ | CT_sbits _ | CT_float _ | CT_rounding_mode | CT_bit

src/lib/pretty_print_sail.ml

@@ -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
@@ -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
@@ -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
@@ -694,7 +702,7 @@ module Printer (Config : PRINT_CONFIG) = struct
         let clauses = separate_map sep doc_mapcl mapcls in
         string "mapping" ^^ space ^^ doc_id id ^^ space ^^ string "=" ^^ space ^^ surround 2 0 lbrace clauses rbrace
 
-  let doc_dec (DEC_aux (reg, _)) =
+  let doc_register (DEC_aux (reg, _)) =
     match reg with
     | DEC_reg (typ, id, opt_exp) -> (
         match opt_exp with
@@ -719,7 +727,7 @@ module Printer (Config : PRINT_CONFIG) = struct
     | A_bool _ -> space ^^ string sep ^^ space ^^ string "Bool"
     | A_typ _ -> empty
 
-  let doc_typdef (TD_aux (td, _)) =
+  let doc_type_def (TD_aux (td, _)) =
     match td with
     | TD_abstract (id, kind) -> begin doc_op colon (concat [string "type"; space; doc_id id]) (doc_kind kind) end
     | TD_abbrev (id, typq, typ_arg) -> begin
@@ -836,7 +844,7 @@ module Printer (Config : PRINT_CONFIG) = struct
     match aux with
     | DEF_default df -> doc_default df
     | DEF_val v_spec -> doc_spec v_spec
-    | DEF_type t_def -> doc_typdef t_def
+    | DEF_type t_def -> doc_type_def t_def
     | DEF_fundef f_def -> doc_fundef f_def
     | DEF_mapdef m_def -> doc_mapdef m_def
     | DEF_constraint nc -> string "constraint" ^^ space ^^ doc_nc nc
@@ -860,7 +868,7 @@ module Printer (Config : PRINT_CONFIG) = struct
     | DEF_let lbind -> string "let" ^^ space ^^ doc_letbind lbind
     | DEF_internal_mutrec fundefs ->
         (string "mutual {" ^//^ separate_map (hardline ^^ hardline) doc_fundef fundefs) ^^ hardline ^^ string "}"
-    | DEF_register dec -> doc_dec dec
+    | DEF_register dec -> doc_register dec
     | DEF_scattered sdef -> doc_scattered sdef
     | DEF_measure (id, pat, exp) ->
         string "termination_measure" ^^ space ^^ doc_id id ^/^ doc_pat pat ^^ space ^^ equals ^/^ doc_exp exp
@@ -881,13 +889,11 @@ module Printer (Config : PRINT_CONFIG) = struct
   let doc_ast { defs; _ } = separate_map hardline doc_def (List.filter doc_filter defs)
 end
 
-(* This function is intended to reformat machine-generated Sail into
-   something a bit more readable, it is not intended to be used as a
-   general purpose formatter *)
-let reformat dir { defs; _ } =
+let reformat ~into_directory: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
 
@@ -938,15 +944,19 @@ 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)
 
-let pp_ast f d = ToChannel.pretty 1. 80 f (doc_ast d)
+let output_ast ?(line_width = 80) f d = ToChannel.pretty 1. line_width f (doc_ast d)
 
-let pretty_sail f doc = ToChannel.pretty 1. 120 f doc
+module Document = struct
+  let to_channel ?(line_width = 120) f doc = ToChannel.pretty 1. line_width f doc
 
-let to_string doc =
-  let b = Buffer.create 120 in
-  ToBuffer.pretty 1. 120 b doc;
-  Buffer.contents b
+  let to_string ?(line_width = 120) doc =
+    (* Allocate at least one line up front *)
+    let b = Buffer.create line_width in
+    ToBuffer.pretty 1. line_width b doc;
+    Buffer.contents b
+end