diff options
| author | Thomas Bauereiss | 2017-12-06 17:18:36 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-12-06 17:18:36 +0000 |
| commit | 2bc281428a3a1d608d56f69e71b50056a25e3da0 (patch) | |
| tree | dfd8e8a13702696fd9daef64315952b9652f95e8 /src/lem_interp/interp_interface.lem | |
| parent | c3c3c40a1d4f81448d8356317e88be2b04363df7 (diff) | |
| parent | 44e9396fa90ab68ee4c8d9674c6bbad6fc851c6d (diff) | |
Merge remote branch 'experiments' into experiments
Diffstat (limited to 'src/lem_interp/interp_interface.lem')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index dcc9f537..32744da2 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -9,6 +9,14 @@ (* Robert Norton-Wright *) (* Christopher Pulte *) (* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) (* *) (* All rights reserved. *) (* *) @@ -104,6 +112,10 @@ end and the potential static effects from the funcl clause for this instruction Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values *) + + +type instruction_field_value = list bit + type instruction = (string * list (string * instr_parm_typ * instruction_field_value)) let {coq} instructionEqual i1 i2 = match (i1,i2) with @@ -117,7 +129,7 @@ let inline ~{coq} instructionInequal = unsafe_structural_inequality type v_kind = Bitv | Bytev type decode_error = - | Unsupported_instruction_error of instruction + | Unsupported_instruction_error of Interp_ast.value | Not_an_instruction_error of opcode | Internal_error of string @@ -264,12 +276,12 @@ 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_ast.value + | IDE_instr of Interp_ast.value | IDE_decode_error of decode_error (** propose to remove the following type and use the above instead *) type i_state_or_error = - | Instr of instruction * instruction_state + | Instr of Interp_ast.value * instruction_state | Decode_error of decode_error |