Merge branch 'experiments' into mono-experiments

1 files changed, 8 insertions, 0 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 3616897a..f994ae22 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -887,6 +887,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"