diff options
| author | Jonathan French | 2017-07-26 11:38:39 +0000 |
|---|---|---|
| committer | Jonathan French | 2017-07-26 11:38:39 +0000 |
| commit | 18cf235fad35a0e06e26ea91ee0e1c673febddb8 (patch) | |
| tree | 60514356175ebfbc0d2d24f70137fffcb8aba0e6 /src/lem_interp/interp_interface.lem | |
| parent | 2e1ca2e6b77b285168223263e747396ad01cb993 (diff) | |
| parent | 24469b4fda9ef14c7717aac415a398da29e8fbd0 (diff) | |
Merged in ojno/sail (pull request #1)
Footprint exhaustive evaluation fixes
Approved-by: Jonathan French <me@jonathanfrench.net>
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 0ce7b43a..937db466 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -162,7 +162,7 @@ end 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 specification = Interp_ast.defs Interp_ast.tannot (*Deem abstract*) type interpreter_mode = Interp.interp_mode (*Deem abstract*) type interp_mode = <| internal_mode: interpreter_mode |> val make_mode : (*eager*) bool -> (*tracking*) bool -> interp_mode @@ -171,12 +171,12 @@ val tracking_dependencies : interp_mode -> bool (*Map between external functions as preceived from a Sail spec and the actual implementation of the function *) -type external_functions = list (string * (Interp.value -> Interp.value)) +type external_functions = list (string * (Interp_ast.value -> Interp_ast.value)) (*Maps between the memory functions as preceived from a Sail spec and the values needed for actions in the memory model*) type barriers = list (string * barrier_kind) -type memory_parameter_transformer = interp_mode -> Interp.value -> (memory_value * nat * maybe (list reg_name)) -type optional_memory_transformer = interp_mode -> Interp.value -> maybe memory_value +type memory_parameter_transformer = interp_mode -> Interp_ast.value -> (memory_value * nat * maybe (list reg_name)) +type optional_memory_transformer = interp_mode -> Interp_ast.value -> maybe memory_value type memory_read = MR of read_kind * memory_parameter_transformer type memory_reads = list (string * memory_read) type memory_read_tagged = MRT of read_kind * memory_parameter_transformer @@ -264,7 +264,7 @@ val initial_instruction_state : context -> string -> list register_value -> inst (* string is a function name, list of value are the parameters to that function *) type instruction_or_decode_error = - | IDE_instr of instruction * Interp.value + | IDE_instr of instruction * Interp_ast.value | IDE_decode_error of decode_error (** propose to remove the following type and use the above instead *) |