diff options
| author | Alasdair Armstrong | 2017-07-27 17:42:04 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-07-27 17:42:04 +0100 |
| commit | e8efda851a54e3a658b0168c916204e1eef83802 (patch) | |
| tree | 9e01f9e429c1c79f9f4f36356cf917df8753a7b9 /mips/mips_extras.lem | |
| parent | c0ef2c3ea1ce7fc2c0b2ba970de27c3a1a5f6591 (diff) | |
| parent | 2b8ab9a1d1438ee8462e5140711fa5f6f4074aef (diff) | |
Merge branch 'master' into sail_new_tc
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))))); ] |