Add support for register types other than bitvector to state monad

Make state monad parametric in register state, and generate a record with
registers from the Sail spec

1 files changed, 8 insertions, 0 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index b4a15432..b5019df6 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -884,6 +884,14 @@ type register =
   | UndefinedRegister of integer (* length *)
   | RegisterPair of register * register
 
+type register_ref 'regstate 'a =
+  <| read_from : 'regstate -> 'a;
+     write_to : 'regstate -> 'a -> 'regstate |>
+
+type field_ref 'regtype 'a =
+  <| get_field : 'regtype -> 'a;
+     set_field : 'regtype -> 'a -> 'regtype |>
+
 let name_of_reg = function
   | Register name _ _ _ _ -> name
   | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister"