diff options
| author | Jon French | 2017-07-26 14:23:34 +0100 |
|---|---|---|
| committer | Jon French | 2017-07-26 14:23:34 +0100 |
| commit | e472553a0bc8c1c59d2e1e460cbd9395727a0279 (patch) | |
| tree | 8a5ca0d34b705f12aa98d4510598428868df2656 /mips/mips_extras.lem | |
| parent | 18cf235fad35a0e06e26ea91ee0e1c673febddb8 (diff) | |
mips_extras.lem: fix references to Interp.V_foo
Diffstat (limited to 'mips/mips_extras.lem')
| -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))))); ] |