diff options
| author | Alasdair Armstrong | 2017-07-28 15:39:52 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-07-28 15:39:52 +0100 |
| commit | 3c18efc6153c340517d7b229fe64b38e4d3e5f33 (patch) | |
| tree | 34f7ed3cce7bf6a3b35b94e117e0c6690ae73399 /mips | |
| parent | 34c27ada18e9e36a0224e2ff9999559ed2899157 (diff) | |
| parent | f951a1712fe88eadc812643175ea8f3d31a558cf (diff) | |
Merge remote-tracking branch 'origin/sail_new_tc' into experiments
Diffstat (limited to 'mips')
| -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))))); ] |