Add option to generate grouped register state record

... with one field per register *type*, instead of one field per
register.  The fields store functions from register name to value.
This leads to dramatically reduced processing time for the register
state record in HOL4.

1 files changed, 75 insertions, 33 deletions

diff --git a/src/state.ml b/src/state.ml
index 9d79fef0..5af39cd2 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -58,6 +58,8 @@ open PPrint
 open Pretty_print_common
 open Pretty_print_sail
 
+let opt_type_grouped_regstate = ref false
+
 let defs_of_string = ast_of_def_string
 
 let is_defined defs name = IdSet.mem (mk_id name) (ids_of_defs (Defs defs))
@@ -78,11 +80,48 @@ let find_registers defs =
       | _ -> acc
     ) [] defs
 
-let generate_regstate = function
-  | [] -> ["type regstate = unit"]
+let generate_register_id_enum = function
+  | [] -> ["type register_id = unit"]
   | registers ->
-     let reg (typ, id) = Printf.sprintf "%s : %s" (string_of_id id) (to_string (doc_typ typ)) in
-     ["struct regstate = { " ^ (String.concat ", " (List.map reg registers)) ^ " }"]
+     let reg (typ, id) = string_of_id id in
+     ["type register_id = " ^ String.concat " | " (List.map reg registers)]
+
+let rec id_of_regtyp builtins mwords (Typ_aux (t, l) as typ) = match t with
+  | Typ_id id -> id
+  | Typ_app (id, args) ->
+     let name_arg (A_aux (targ, _)) = match targ with
+       | A_typ targ -> string_of_id (id_of_regtyp builtins mwords targ)
+       | A_nexp nexp when is_nexp_constant (nexp_simp nexp) ->
+          string_of_nexp (nexp_simp nexp)
+       | A_order (Ord_aux (Ord_inc, _)) -> "inc"
+       | A_order (Ord_aux (Ord_dec, _)) -> "dec"
+       | _ ->
+          raise (Reporting.err_typ l "Unsupported register type")
+     in
+     if IdSet.mem id builtins && not (mwords && is_bitvector_typ typ) then id else
+     append_id id (String.concat "_" ("" :: List.map name_arg args))
+  | _ -> raise (Reporting.err_typ l "Unsupported register type")
+
+let regstate_field typ = append_id (id_of_regtyp IdSet.empty false typ) "_reg"
+
+let generate_regstate registers =
+  let regstate_def =
+    if registers = [] then
+      TD_abbrev (mk_id "regstate", mk_typquant [], mk_typ_arg (A_typ unit_typ))
+    else
+      let fields =
+        if !opt_type_grouped_regstate then
+          List.map
+            (fun (typ, id) ->
+                 (function_typ [string_typ] typ no_effect,
+                  regstate_field typ))
+            registers
+          |> List.sort_uniq (fun (typ1, id1) (typ2, id2) -> Id.compare id1 id2)
+        else registers
+      in
+      TD_record (mk_id "regstate", mk_typquant [], fields, false)
+  in
+  Defs [DEF_type (TD_aux (regstate_def, (Unknown, ())))]
 
 let generate_initial_regstate defs =
   let registers = find_registers defs in
@@ -181,27 +220,15 @@ let generate_initial_regstate defs =
       | _ -> inits) ([], Bindings.empty) defs
     in
     let init_reg (typ, id) = string_of_id id ^ " = " ^ lookup_init_val init_vals typ in
-    init_defs @
-    ["let initial_regstate : regstate = struct { " ^ (String.concat ", " (List.map init_reg registers)) ^ " }"]
+    List.map defs_of_string
+      (init_defs @
+       ["let initial_regstate : regstate = struct { " ^
+        (String.concat ", " (List.map init_reg registers)) ^
+        " }"])
   with
   | _ -> [] (* Do not generate an initial register state if anything goes wrong *)
 
-let rec regval_constr_id mwords (Typ_aux (t, l) as typ) = match t with
-  | Typ_id id -> id
-  | Typ_app (id, args) ->
-     let name_arg (A_aux (targ, _)) = match targ with
-       | A_typ targ -> string_of_id (regval_constr_id mwords targ)
-       | A_nexp nexp when is_nexp_constant (nexp_simp nexp) ->
-          string_of_nexp (nexp_simp nexp)
-       | A_order (Ord_aux (Ord_inc, _)) -> "inc"
-       | A_order (Ord_aux (Ord_dec, _)) -> "dec"
-       | _ ->
-          raise (Reporting.err_typ l "Unsupported register type")
-     in
-     let builtins = IdSet.of_list (List.map mk_id ["vector"; "bitvector"; "list"; "option"]) in
-     if IdSet.mem id builtins && not (mwords && is_bitvector_typ typ) then id else
-     append_id id (String.concat "_" ("" :: List.map name_arg args))
-  | _ -> raise (Reporting.err_typ l "Unsupported register type")
+let regval_constr_id = id_of_regtyp (IdSet.of_list (List.map mk_id ["vector"; "bitvector"; "list"; "option"]))
 
 let register_base_types mwords typs =
   let rec add_base_typs typs (Typ_aux (t, _) as typ) =
@@ -211,8 +238,8 @@ let register_base_types mwords typs =
         when IdSet.mem id builtins && not (mwords && is_bitvector_typ typ) ->
          let add_typ_arg base_typs (A_aux (targ, _)) =
            match targ with
-             | A_typ typ -> add_base_typs typs typ
-             | _ -> typs
+             | A_typ typ -> add_base_typs base_typs typ
+             | _ -> base_typs
          in
          List.fold_left add_typ_arg typs args
       | _ -> Bindings.add (regval_constr_id mwords typ) typ typs
@@ -227,9 +254,10 @@ let generate_regval_typ typs =
     "Regval_list : list(register_value), " ^
     "Regval_option : option(register_value)"
   in
-  ["union register_value = { " ^
-  (String.concat ", " (builtins :: List.map constr (Bindings.bindings typs))) ^
-  " }"]
+  [defs_of_string
+    ("union register_value = { " ^
+     (String.concat ", " (builtins :: List.map constr (Bindings.bindings typs))) ^
+     " }")]
 
 let add_regval_conv id typ (Defs defs) =
   let id = string_of_id id in
@@ -307,12 +335,20 @@ let register_refs_lem mwords registers =
   in
   let register_ref (typ, id) =
     let idd = string (string_of_id id) in
+    let (read_from, write_to) =
+      if !opt_type_grouped_regstate then
+        let field_idd = string (string_of_id (regstate_field typ)) in
+        (field_idd ^^ space ^^ dquotes idd,
+         doc_op equals field_idd (string "(fun reg -> if reg = \"" ^^ idd ^^ string "\" then v else s." ^^ field_idd ^^ string " reg)"))
+      else
+        (idd, doc_op equals idd (string "v"))
+    in
     (* let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in *)
     let of_regval, regval_of = regval_convs_lem mwords typ in
     concat [string "let "; idd; string "_ref = <|"; hardline;
       string "  name = \""; idd; string "\";"; hardline;
-      string "  read_from = (fun s -> s."; idd; string ");"; hardline;
-      string "  write_to = (fun v s -> (<| s with "; idd; string " = v |>));"; hardline;
+      string "  read_from = (fun s -> s."; read_from; string ");"; hardline;
+      string "  write_to = (fun v s -> (<| s with "; write_to; string " |>));"; hardline;
       string "  of_regval = "; string of_regval; string ";"; hardline;
       string "  regval_of = "; string regval_of; string " |>"; hardline]
   in
@@ -504,14 +540,20 @@ let generate_regstate_defs mwords defs =
   let regtyps = register_base_types mwords (List.map fst registers) in
   let option_typ =
     if is_defined defs "option" then [] else
-      ["union option ('a : Type) = {None : unit, Some : 'a}"]
+      [defs_of_string "union option ('a : Type) = {None : unit, Some : 'a}"]
   in
   let regval_typ = if is_defined defs "register_value" then [] else generate_regval_typ regtyps in
-  let regstate_typ = if is_defined defs "regstate" then [] else generate_regstate registers in
-  let initregstate = if is_defined defs "initial_regstate" then [] else generate_initial_regstate defs in
+  let regstate_typ = if is_defined defs "regstate" then [] else [generate_regstate registers] in
+  let initregstate =
+    (* Don't create initial regstate if it is already defined or if we generated
+       a regstate record with registers grouped per type; the latter would
+       require record fields storing functions, which is not supported in
+       Sail. *)
+    if is_defined defs "initial_regstate" || !opt_type_grouped_regstate then [] else
+    generate_initial_regstate defs
+  in
   let defs =
     option_typ @ regval_typ @ regstate_typ @ initregstate
-    |> List.map defs_of_string
     |> concat_ast
     |> Bindings.fold add_regval_conv regtyps
   in