diff options
| -rw-r--r-- | mips/mips_extras.lem | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem index 99487f49..1fbba038 100644 --- a/mips/mips_extras.lem +++ b/mips/mips_extras.lem @@ -7,13 +7,13 @@ import Set_extra let memory_parameter_transformer mode v = match v with - | Interp.V_tuple [location;length] -> + | Interp_ast.V_tuple [location;length] -> let (v,loc_regs) = extern_with_track mode extern_vector_value location in match length with - | Interp.V_lit (L_aux (L_num len) _) -> + | Interp_ast.V_lit (L_aux (L_num len) _) -> (v,(natFromInteger len),loc_regs) - | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs -> + | Interp_ast.V_track (Interp_ast.V_lit (L_aux (L_num len) _)) size_regs -> match loc_regs with | Nothing -> (v,(natFromInteger len),Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))) | Just loc_regs -> (v,(natFromInteger len),Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))) @@ -25,7 +25,7 @@ let memory_parameter_transformer mode v = let memory_parameter_transformer_option_address _mode v = match v with - | Interp.V_tuple [location;_] -> + | Interp_ast.V_tuple [location;_] -> Just (extern_vector_value location) | _ -> Assert_extra.failwith ("memory_parameter_transformer_option_address: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v)) end @@ -54,7 +54,7 @@ let memory_vals : memory_write_vals = ("MEMval_conditional", (MV memory_parameter_transformer_option_address (Just (fun (IState interp context) b -> - let bit = Interp.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in + let bit = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in (IState (Interp.add_answer_to_stack interp bit) context))))); ] @@ -64,7 +64,7 @@ let memory_vals_tagged : memory_write_vals_tagged = ("MEMval_tag_conditional", (MVT memory_parameter_transformer_option_address (Just (fun (IState interp context) b -> - let bit = Interp.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in + let bit = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in (IState (Interp.add_answer_to_stack interp bit) context))))); ] |