diff options
Diffstat (limited to 'src/gen_lib/sail_values.lem')
| -rw-r--r-- | src/gen_lib/sail_values.lem | 8 |
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" |
