diff options
Diffstat (limited to 'src/lem_interp/interp_inter_imp.lem')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 8199f271..c982a30a 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -48,6 +48,7 @@ import Set_extra open import Pervasives open import Assert_extra open import Interp_ast +open import Interp_utilities open import Sail_impl_base open import Interp_interface @@ -439,7 +440,8 @@ let rec interp_to_value_helper debug arg ivh_mode err_str instr direction regist (Ivh_error (Interp_interface.Internal_error ("Write memory value request in a " ^ errk_str)), events_out) | (Interp.Action (Interp.Write_memv_tagged _ _ _ _) _,_,_) -> (Ivh_error (Interp_interface.Internal_error ("Write memory value tagged request in a " ^ errk_str)), events_out) - | _ -> (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str)), events_out) + | (outcome, _, _) -> + (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str ^ " " ^ Interp.string_of_outcome outcome)), events_out) end let call_external_functions direction outcome = @@ -501,7 +503,7 @@ let value_of_instruction_param direction (name,typ,v) = end in v let intern_instruction direction (name,parms) = - Interp_ast.V_ctor (Interp.id_of_string name) (T_id "ast") Interp_ast.C_Union + Interp_ast.V_ctor (Interp.id_of_string name) (mk_typ_id "ast") Interp_ast.C_Union (Interp_ast.V_tuple (List.map (value_of_instruction_param direction) parms)) let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers (instruction : Interp_ast.value) = @@ -765,7 +767,7 @@ let instr_external_to_interp_value top_level instr = end in (*This type shouldn't be hard-coded*) Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id name) Interp_ast.Unknown) - (T_id "ast") Interp_ast.C_Union parmsV + (mk_typ_id "ast") Interp_ast.C_Union parmsV val instruction_to_istate : context -> Interp_ast.value -> instruction_state let instruction_to_istate (top_level:context) (instr:Interp_ast.value) : instruction_state = |