diff options
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 374f633e..396f0f5c 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -30,11 +30,16 @@ end type word8 = nat (* bounded at a byte, for when lem supports it*) +type end_flag = + | E_big_endian + | E_little_endian + type interpreter_state = Interp.stack (*Deem abstract*) (* Will come from a .lem file generated by Sail, bound to a 'defs' identifier *) type specification = Interp_ast.defs Interp.tannot (*Deem abstract*) -type interp_mode = Interp.interp_mode (*Deem abstract*) -val make_mode : bool -> bool -> interp_mode +type interpreter_mode = Interp.interp_mode (*Deem abstract*) +type interp_mode = <| internal_mode: interpreter_mode; endian: end_flag |> +val make_mode : (*eager*) bool -> (*tracking*) bool -> end_flag -> interp_mode val tracking_dependencies : interp_mode -> bool (** basic values *) @@ -53,10 +58,6 @@ type direction = | D_increasing | D_decreasing -type end_flag = - | E_big_endian - | E_little_endian - type register_value = <| rv_bits: list bit_lifted (* MSB first, smallest index number *); rv_dir: direction; @@ -73,8 +74,9 @@ type instruction_field_value = list bit type byte = Byte of list bit (* of length 8 *) (*MSB first everywhere*) type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*) * maybe integer +(* for both values of end_flag, MSBy first *) -type memory_byte = byte_lifted +type memory_byte = byte_lifted (* of length 8 *) (*MSB first everywhere*) type memory_value = list memory_byte (* the list is of length >=1 *) |