Fixed a bug where sizeof re-writing fail for aliased type arguments

Also: Merge remote-tracking branch 'origin/sail_new_tc' into 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 53a74d05..eb5cdef5 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"