diff options
| author | Peter Sewell | 2014-11-23 00:59:21 +0000 |
|---|---|---|
| committer | Peter Sewell | 2014-11-23 00:59:21 +0000 |
| commit | 40dc7ff0fefce917b1a1a4f2d04514644a3c84cc (patch) | |
| tree | f4794394a7c2a966ccb0bd2af89efdd91da4213f /src | |
| parent | c5dc540e5b2fe0e4ef0ecb0d607cef60ac6d2c66 (diff) | |
fight with interface/impl mismatch. lose.
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 6 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index df47a75e..4cce629c 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -411,18 +411,18 @@ let decode_to_istate top_level orig_value = end -let decode_to_instruction top_level value = +let decode_to_instruction (top_level:context) (value:opcode) : instruction_or_decode_error = match decode_to_istate top_level value with | Instr inst is -> IDE_instr inst | Decode_error de -> IDE_decode_error de end -let instruction_to_istate top_level ((name, parms, _) as instr) = +let instruction_to_istate (top_level:context) (((name, parms, _) as instr):instruction) : instruction_state = let mode = make_mode true false in let get_value (name,typ,v) = let (e,_) = - Interp.to_exp mode Interp.eenv (intern_reg_value (opcode_to_regval v 0 D_increasing)) in e in + Interp.to_exp mode Interp.eenv (intern_reg_value ((* SUSPICIOUS?*) opcode_to_regval v 0 D_increasing)) in e in (* (Instr instr*) (Interp.Thunk_frame (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 6a70990b..da086524 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -350,7 +350,7 @@ val decode_to_istate : context -> opcode -> i_state_or_error val decode_to_instruction : context -> opcode -> instruction_or_decode_error (*Function to generate the state to run from an instruction form; is always an Instr*) -val instruction_to_istate : context -> instruction -> i_state_or_error +val instruction_to_istate : context -> instruction -> instruction_state (*i_state_or_error*) (* Augment an address by the given value *) (*val add_to_address : value -> integer -> value |