From 7c1e6160f89068d7e106a36919806629ca61df04 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Sat, 11 May 2024 23:31:24 +0100 Subject: [PATCH 1/2] Some further documentation improvements 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. --- src/lib/ast_util.ml | 2 ++ src/lib/ast_util.mli | 1 + src/lib/pretty_print_sail.ml | 12 +++++++++++- src/sail_doc_backend/docinfo.ml | 1 + src/sail_doc_backend/wavedrom.ml | 9 ++++++++- 5 files changed, 23 insertions(+), 2 deletions(-) diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml index f6a75552c..8088b85ae 100644 --- a/src/lib/ast_util.ml +++ b/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 diff --git a/src/lib/ast_util.mli b/src/lib/ast_util.mli index e232693a0..d127a0868 100644 --- a/src/lib/ast_util.mli +++ b/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 diff --git a/src/lib/pretty_print_sail.ml b/src/lib/pretty_print_sail.ml index 210567ad3..00025f46a 100644 --- a/src/lib/pretty_print_sail.ml +++ b/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 @@ -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 @@ -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) diff --git a/src/sail_doc_backend/docinfo.ml b/src/sail_doc_backend/docinfo.ml index 3ba72797f..7cdd404aa 100644 --- a/src/sail_doc_backend/docinfo.ml +++ b/src/sail_doc_backend/docinfo.ml @@ -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 diff --git a/src/sail_doc_backend/wavedrom.ml b/src/sail_doc_backend/wavedrom.ml index 799d196a0..6b1686678 100644 --- a/src/sail_doc_backend/wavedrom.ml +++ b/src/sail_doc_backend/wavedrom.ml @@ -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, _)) -> @@ -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 From 4ac6beffc6a67f80b656199a9ed2facea514c0a3 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Sat, 11 May 2024 23:50:27 +0100 Subject: [PATCH 2/2] Refactor pretty printer output functions Add an mli interface for Pretty_print_sail Hide attributes in interactive output --- src/bin/repl.ml | 6 +- src/lib/frontend.ml | 6 +- src/lib/interpreter.ml | 23 ++- src/lib/jib_compile.ml | 7 +- src/lib/jib_util.ml | 3 +- src/lib/pretty_print_sail.ml | 28 ++-- src/lib/pretty_print_sail.mli | 152 ++++++++++++++++++++ src/lib/rewrites.ml | 2 +- src/lib/specialize.ml | 2 +- src/lib/state.ml | 6 +- src/lib/util.ml | 4 + src/lib/util.mli | 5 + src/sail_c_backend/c_backend.ml | 5 +- src/sail_doc_backend/docinfo.ml | 12 +- src/sail_doc_backend/wavedrom.ml | 2 +- src/sail_latex_backend/latex.ml | 2 +- src/sail_latex_backend/sail_plugin_latex.ml | 2 +- src/sail_output/sail_plugin_output.ml | 2 +- src/sail_smt_backend/smtlib.ml | 2 +- src/sail_sv_backend/sail_plugin_sv.ml | 2 +- 20 files changed, 219 insertions(+), 54 deletions(-) create mode 100644 src/lib/pretty_print_sail.mli diff --git a/src/bin/repl.ml b/src/bin/repl.ml index 7ed6569f5..935245dfc 100644 --- a/src/bin/repl.ml +++ b/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" -> diff --git a/src/lib/frontend.ml b/src/lib/frontend.ml index c5abe9898..8eb84c914 100644 --- a/src/lib/frontend.ml +++ b/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; diff --git a/src/lib/interpreter.ml b/src/lib/interpreter.ml index 53d4959f4..4187254c9 100644 --- a/src/lib/interpreter.ml +++ b/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,12 +1008,7 @@ 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 @@ -1014,9 +1016,4 @@ let execute_instruction state ast = 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, []) diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index 1c20c45b5..b75d43cb7 100644 --- a/src/lib/jib_compile.ml +++ b/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 ^ ">") diff --git a/src/lib/jib_util.ml b/src/lib/jib_util.ml index d30af60fd..9fdd9c322 100644 --- a/src/lib/jib_util.ml +++ b/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 diff --git a/src/lib/pretty_print_sail.ml b/src/lib/pretty_print_sail.ml index 00025f46a..06aa8b8bc 100644 --- a/src/lib/pretty_print_sail.ml +++ b/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 diff --git a/src/lib/pretty_print_sail.mli b/src/lib/pretty_print_sail.mli new file mode 100644 index 000000000..0caec118a --- /dev/null +++ b/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 REMS: Rigorous *) +(* Engineering for Mainstream Systems, 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 diff --git a/src/lib/rewrites.ml b/src/lib/rewrites.ml index 8ff5207ff..f0168bb66 100644 --- a/src/lib/rewrites.ml +++ b/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) | _ -> () diff --git a/src/lib/specialize.ml b/src/lib/specialize.ml index e8a3bb71e..7469b20e8 100644 --- a/src/lib/specialize.ml +++ b/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 -> () diff --git a/src/lib/state.ml b/src/lib/state.ml index 38d7fabeb..9af5f509d 100644 --- a/src/lib/state.ml +++ b/src/lib/state.ml @@ -295,7 +295,9 @@ let register_bitfield_types env typs = List.fold_left add_bitfield_typs Bindings.empty typs let generate_regval_typ env typs = - let constr (constr_id, typ) = Printf.sprintf "Regval_%s : %s" (string_of_id constr_id) (to_string (doc_typ typ)) in + let constr (constr_id, typ) = + Printf.sprintf "Regval_%s : %s" (string_of_id constr_id) (Document.to_string (doc_typ typ)) + in let builtins = "Regval_vector : list(register_value), " ^ "Regval_list : list(register_value), " ^ "Regval_option : option(register_value), " ^ "Regval_bool : bool, " ^ "Regval_int : int, " @@ -336,7 +338,7 @@ let regval_base_convs typ = else (id ^ "_of_regval", "regval_of_" ^ id) let add_regval_conv env id typ defs = - let typ_str = to_string (doc_typ typ) in + let typ_str = Document.to_string (doc_typ typ) in let v_exp = mk_exp (E_id (mk_id "v")) in let base_typ = regval_base_typ env typ in (* Create a function that converts from regval to the target type. *) diff --git a/src/lib/util.ml b/src/lib/util.ml index 367f4be0a..dd2d66952 100644 --- a/src/lib/util.ml +++ b/src/lib/util.ml @@ -454,6 +454,10 @@ let list_init len f = let rec list_init' len f acc = if acc >= len then [] else f acc :: list_init' len f (acc + 1) in list_init' len f 0 +let starts_with ~prefix s = + let prefix_len = String.length prefix in + prefix_len <= String.length s && String.sub s 0 prefix_len = prefix + let levenshtein_distance ?(osa = false) str1 str2 = let dist = Array.make_matrix (String.length str1 + 1) (String.length str2 + 1) 0 in diff --git a/src/lib/util.mli b/src/lib/util.mli index 8e3eb7318..e3ef7c334 100644 --- a/src/lib/util.mli +++ b/src/lib/util.mli @@ -224,6 +224,11 @@ val fold_left_index_last : (int -> bool -> 'a -> 'b -> 'a) -> 'a -> 'b list -> ' val list_init : int -> (int -> 'a) -> 'a list +(** {2 String utilities} *) + +(** Alternative to String.starts_with for OCaml < 4.13 *) +val starts_with : prefix:string -> string -> bool + (** Compute the levenshtein distance between two strings using the Wagner–Fischer algorithm. If [~osa] is true computes the optimal string alignment distance, which is similar but allows swaps as a diff --git a/src/sail_c_backend/c_backend.ml b/src/sail_c_backend/c_backend.ml index e1036d3c4..c15d2405a 100644 --- a/src/sail_c_backend/c_backend.ml +++ b/src/sail_c_backend/c_backend.ml @@ -76,6 +76,7 @@ open Jib_visitor open Type_check open PPrint open Value2 +module Document = Pretty_print_sail.Document open Anf @@ -2031,7 +2032,7 @@ let sgen_startup = function | CDEF_aux (CDEF_startup (id, _), _) -> Printf.sprintf " startup_%s();" (sgen_function_id id) | _ -> assert false -let sgen_instr id ctx instr = Pretty_print_sail.to_string (codegen_instr id ctx instr) +let sgen_instr id ctx instr = Document.to_string (codegen_instr id ctx instr) let is_cdef_finish = function CDEF_aux (CDEF_startup _, _) -> true | _ -> false @@ -2191,7 +2192,7 @@ let compile_ast env effect_info output_chan c_includes ast = let end_extern_cpp = separate hardline (List.map string [""; "#ifdef __cplusplus"; "}"; "#endif"]) in let hlhl = hardline ^^ hardline in - Pretty_print_sail.to_string + Document.to_string (preamble ^^ hlhl ^^ docs ^^ hlhl ^^ ( if not !opt_no_rts then model_init ^^ hlhl ^^ model_fini ^^ hlhl ^^ model_pre_exit ^^ hlhl ^^ model_default_main ^^ hlhl diff --git a/src/sail_doc_backend/docinfo.ml b/src/sail_doc_backend/docinfo.ml index 7cdd404aa..78ed403ed 100644 --- a/src/sail_doc_backend/docinfo.ml +++ b/src/sail_doc_backend/docinfo.ml @@ -83,6 +83,8 @@ module Reformatter = Pretty_print_sail.Printer (struct let hide_attributes = true end) +module Document = Pretty_print_sail.Document + (** In the case of latex, we generate files containing a sequence of commands that can simply be included. For other documentation targets with tooling that may consume the json output however, we @@ -447,7 +449,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct | Some (p1, p2) when p1.pos_fname = p2.pos_fname && Filename.is_relative p1.pos_fname && Sys.file_exists p1.pos_fname -> doc_lexing_pos p1 p2 - | _ -> Raw (g x |> f |> Pretty_print_sail.to_string |> encode) + | _ -> Raw (g x |> f |> Document.to_string |> encode) let get_doc_comment def_annot = Option.map @@ -465,11 +467,11 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct } let docinfo_for_type_def (TD_aux (_, annot) as td) = - doc_loc (fst annot) Type_check.strip_typedef Reformatter.doc_typdef td + doc_loc (fst annot) Type_check.strip_typedef Reformatter.doc_type_def td let docinfo_for_register def_annot (DEC_aux (DEC_reg ((Typ_aux (_, typ_l) as typ), _, exp), rd_annot) as rd) = { - source = doc_loc (fst rd_annot) Type_check.strip_register Reformatter.doc_dec rd; + source = doc_loc (fst rd_annot) Type_check.strip_register Reformatter.doc_register rd; type_source = doc_loc typ_l (fun typ -> typ) Reformatter.doc_typ typ; exp_source = Option.map (fun (E_aux (_, (l, _)) as exp) -> doc_loc l Type_check.strip_exp Reformatter.doc_exp exp) exp; @@ -505,7 +507,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct let substs = (Bindings.singleton split_id checked_member, KBindings.empty) in let propagated, _ = Constant_propagation.const_prop "doc" ast IdSet.empty substs Bindings.empty exp in let propagated_doc = - Raw (pretty_printer (Type_check.strip_exp propagated) |> Pretty_print_sail.to_string |> encode) + Raw (pretty_printer (Type_check.strip_exp propagated) |> Document.to_string |> encode) in Bindings.add member propagated_doc splits ) @@ -548,7 +550,7 @@ module Generator (Converter : Markdown.CONVERTER) (Config : CONFIG) = struct doc_lexing_pos { p1 with pos_cnum = p1.pos_bol } p2 | _, _ -> let block = Type_check.strip_exp exp :: List.map Type_check.strip_exp exps in - Raw (Reformatter.doc_block block |> Pretty_print_sail.to_string |> encode) + Raw (Reformatter.doc_block block |> Document.to_string |> encode) end | _ -> doc_loc (exp_loc exp) Type_check.strip_exp Reformatter.doc_exp exp in diff --git a/src/sail_doc_backend/wavedrom.ml b/src/sail_doc_backend/wavedrom.ml index 6b1686678..b4aeeb119 100644 --- a/src/sail_doc_backend/wavedrom.ml +++ b/src/sail_doc_backend/wavedrom.ml @@ -103,7 +103,7 @@ let rec wavedrom_elem_string size label (P_aux (aux, _)) = match aux with | P_id id -> let name = string_of_id id in - if String.starts_with ~prefix:"imm" name then + if Util.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, _)) -> diff --git a/src/sail_latex_backend/latex.ml b/src/sail_latex_backend/latex.ml index 64eaa7886..258263a70 100644 --- a/src/sail_latex_backend/latex.ml +++ b/src/sail_latex_backend/latex.ml @@ -397,7 +397,7 @@ let latex_command ~docstring cat id no_loc l = let code_file = category_name cat ^ Util.file_encode_string (string_of_id id) ^ ".tex" in let chan = open_out (Filename.concat !opt_directory code_file) in let doc = if cat = Val then no_loc else latex_loc ~docstring no_loc l in - output_string chan (Pretty_print_sail.to_string doc); + output_string chan (Pretty_print_sail.Document.to_string doc); close_out chan; let command = sprintf "\\%s" (latex_cat_id cat id) in if StringSet.mem command state.commands then ( diff --git a/src/sail_latex_backend/sail_plugin_latex.ml b/src/sail_latex_backend/sail_plugin_latex.ml index fdd3f76a4..a2e5fe479 100644 --- a/src/sail_latex_backend/sail_plugin_latex.ml +++ b/src/sail_latex_backend/sail_plugin_latex.ml @@ -104,7 +104,7 @@ let latex_target _ _ out_file ast effect_info env = end; Latex.opt_directory := latex_dir; let chan = open_out (Filename.concat latex_dir "commands.tex") in - output_string chan (Pretty_print_sail.to_string (Latex.defs (Type_check.strip_ast ast))); + output_string chan (Pretty_print_sail.Document.to_string (Latex.defs (Type_check.strip_ast ast))); close_out chan let _ = diff --git a/src/sail_output/sail_plugin_output.ml b/src/sail_output/sail_plugin_output.ml index 42a00ff3b..c597d4a39 100644 --- a/src/sail_output/sail_plugin_output.ml +++ b/src/sail_output/sail_plugin_output.ml @@ -77,7 +77,7 @@ let output_sail_options = let sail_target _ _ out_file ast _effect_info _env = let close, output_chan = match out_file with Some f -> (true, open_out (f ^ ".sail")) | None -> (false, stdout) in - Pretty_print_sail.pp_ast output_chan (Type_check.strip_ast ast); + Pretty_print_sail.output_ast output_chan (Type_check.strip_ast ast); if close then close_out output_chan let _ = diff --git a/src/sail_smt_backend/smtlib.ml b/src/sail_smt_backend/smtlib.ml index 89c91dfae..33a0c5601 100644 --- a/src/sail_smt_backend/smtlib.ml +++ b/src/sail_smt_backend/smtlib.ml @@ -581,7 +581,7 @@ let pp_smt_def = ] | Assert exp -> pp_sfun "assert" [pp_smt_exp exp] -let string_of_smt_def def = Pretty_print_sail.to_string (pp_smt_def def) +let string_of_smt_def def = Pretty_print_sail.Document.to_string (pp_smt_def def) let output_smt_defs out_chan smt = List.iter (fun def -> output_string out_chan (string_of_smt_def def ^ "\n")) smt diff --git a/src/sail_sv_backend/sail_plugin_sv.ml b/src/sail_sv_backend/sail_plugin_sv.ml index 081a6f3a9..e2f5cbad3 100644 --- a/src/sail_sv_backend/sail_plugin_sv.ml +++ b/src/sail_sv_backend/sail_plugin_sv.ml @@ -565,7 +565,7 @@ let verilog_target _ default_sail_dir out_opt ast effect_info env = in let sv_output = - Pretty_print_sail.to_string + Pretty_print_sail.Document.to_string (wrap_module out_doc ("sail_" ^ out) (inputs @ outputs @ wire_fun_ports @ module_main_in_out) (in_doc ^^ wire_funs ^^ setup_function ^^ invoke_main)