Refactor pretty printer output functions

Add an mli interface for Pretty_print_sail

Hide attributes in interactive output

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

@@ -702,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
@@ -727,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
@@ -844,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
@@ -868,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
@@ -889,10 +889,7 @@ 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
@@ -952,11 +949,14 @@ 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

src/lib/pretty_print_sail.mli

@@ -0,0 +1,152 @@
+(****************************************************************************)
+(*     Sail                                                                 *)
+(*                                                                          *)
+(*  Sail and the Sail architecture models here, comprising all files and    *)
+(*  directories except the ASL-derived Sail code in the aarch64 directory,  *)
+(*  are subject to the BSD two-clause licence below.                        *)
+(*                                                                          *)
+(*  The ASL derived parts of the ARMv8.3 specification in                   *)
+(*  aarch64/no_vector and aarch64/full are copyright ARM Ltd.               *)
+(*                                                                          *)
+(*  Copyright (c) 2013-2021                                                 *)
+(*    Kathyrn Gray                                                          *)
+(*    Shaked Flur                                                           *)
+(*    Stephen Kell                                                          *)
+(*    Gabriel Kerneis                                                       *)
+(*    Robert Norton-Wright                                                  *)
+(*    Christopher Pulte                                                     *)
+(*    Peter Sewell                                                          *)
+(*    Alasdair Armstrong                                                    *)
+(*    Brian Campbell                                                        *)
+(*    Thomas Bauereiss                                                      *)
+(*    Anthony Fox                                                           *)
+(*    Jon French                                                            *)
+(*    Dominic Mulligan                                                      *)
+(*    Stephen Kell                                                          *)
+(*    Mark Wassell                                                          *)
+(*    Alastair Reid (Arm Ltd)                                               *)
+(*                                                                          *)
+(*  All rights reserved.                                                    *)
+(*                                                                          *)
+(*  This work was partially supported by EPSRC grant EP/K008528/1 <a        *)
+(*  href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous          *)
+(*  Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA   *)
+(*  KTF funding, and donations from Arm.  This project has received         *)
+(*  funding from the European Research Council (ERC) under the European     *)
+(*  Union’s Horizon 2020 research and innovation programme (grant           *)
+(*  agreement No 789108, ELVER).                                            *)
+(*                                                                          *)
+(*  This software was developed by SRI International and the University of  *)
+(*  Cambridge Computer Laboratory (Department of Computer Science and       *)
+(*  Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV")        *)
+(*  and FA8750-10-C-0237 ("CTSRD").                                         *)
+(*                                                                          *)
+(*  Redistribution and use in source and binary forms, with or without      *)
+(*  modification, are permitted provided that the following conditions      *)
+(*  are met:                                                                *)
+(*  1. Redistributions of source code must retain the above copyright       *)
+(*     notice, this list of conditions and the following disclaimer.        *)
+(*  2. Redistributions in binary form must reproduce the above copyright    *)
+(*     notice, this list of conditions and the following disclaimer in      *)
+(*     the documentation and/or other materials provided with the           *)
+(*     distribution.                                                        *)
+(*                                                                          *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''      *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED       *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A         *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR     *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,            *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT        *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF        *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND     *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,      *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT      *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF      *)
+(*  SUCH DAMAGE.                                                            *)
+(****************************************************************************)
+
+open Ast
+open Ast_util
+
+(** The [PRINT_CONFIG] module type can be used to customise the
+    behavior of the pretty-printer *)
+module type PRINT_CONFIG = sig
+  (** If true, then the printer will insert additional braces into the
+      source (essentially creating additional E_block nodes). This
+      will give the code a more normal imperative look, especially
+      after re-writing passes that are on the path to the theorem
+      prover targets that use a more functional style. *)
+  val insert_braces : bool
+
+  (** If true, the printer will attempt to reverse some
+      transformations that are done to the source. It can do this
+      where passes insert attributes into the AST that it can use to
+      revert various changes. It will do the following:
+
+      - Reintroduce [v[n]] for vector_access and [v[n..m]] for vector_subrange
+      - Undo overloading
+      - Turn [operator OP(x, y)] back into [x OP y]
+      - Reintroduce setters [setter(x, y)] into [setter(x) = y]
+  *)
+  val resugar : bool
+
+  (** If true, all attributes [$[attr ...]] will be hidden in the
+      output. Note that [resugar] will remove any attributes it uses
+      as hints for resugaring even when this is false. *)
+  val hide_attributes : bool
+end
+
+(** The [Printer] functor defines the printing function based on the
+    supplied printing configuration *)
+module Printer (Config : PRINT_CONFIG) : sig
+  val doc_id : id -> PPrint.document
+
+  val doc_typ : typ -> PPrint.document
+
+  val doc_binding : typquant * typ -> PPrint.document
+
+  val doc_typschm : typschm -> PPrint.document
+
+  val doc_exp : uannot exp -> PPrint.document
+
+  val doc_block : uannot exp list -> PPrint.document
+
+  val doc_letbind : uannot letbind -> PPrint.document
+
+  val doc_funcl : uannot funcl -> PPrint.document
+
+  val doc_mapcl : uannot mapcl -> PPrint.document
+
+  val doc_spec : uannot val_spec -> PPrint.document
+
+  val doc_type_def : uannot type_def -> PPrint.document
+
+  val doc_register : uannot dec_spec -> PPrint.document
+
+  val doc_def : uannot def -> PPrint.document
+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 code formatter. The output will be dumped as
+    multiple files into the directory argument. *)
+val reformat : into_directory:string -> uannot Ast_defs.ast -> unit
+
+(** The default [PRINT_CONFIG] sets all the options to false, so it
+    prints the AST 'as is' without modifications. *)
+module Default_print_config : PRINT_CONFIG
+
+(** For convenience, other modules can get the default behavior by
+    just importing this module. *)
+include module type of Printer (Default_print_config)
+
+(** This function is primarly used to dump the AST by debug options,
+    such as [--ddump-tc-ast]. *)
+val output_ast : ?line_width:int -> out_channel -> uannot Ast_defs.ast -> unit
+
+(** Some convenience functions for outputting PPrint documents *)
+module Document : sig
+  val to_channel : ?line_width:int -> out_channel -> PPrint.document -> unit
+
+  val to_string : ?line_width:int -> PPrint.document -> string
+end

src/lib/rewrites.ml

@@ -4558,7 +4558,7 @@ let rewrite_step n total (ast, effect_info, env) (name, rewriter) =
     | Some (f, i) ->
         let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in
         let ((ot, _, _, _) as ext_ot) = Util.open_output_with_check_unformatted None filename in
-        Pretty_print_sail.pp_ast ot (strip_ast ast);
+        Pretty_print_sail.output_ast ot (strip_ast ast);
         Util.close_output_with_check ext_ot;
         opt_ddump_rewrite_ast := Some (f, i + 1)
     | _ -> ()

src/lib/specialize.ml

@@ -624,7 +624,7 @@ let specialize_ids spec ids ast effect_info =
     | Some (f, i) ->
         let filename = f ^ "_spec_" ^ string_of_int i ^ ".sail" in
         let out_chan = open_out filename in
-        Pretty_print_sail.pp_ast out_chan (Type_check.strip_ast ast);
+        Pretty_print_sail.output_ast out_chan (Type_check.strip_ast ast);
         close_out out_chan;
         opt_ddump_spec_ast := Some (f, i + 1)
     | None -> ()