diff options
Diffstat (limited to 'mips_new_tc')
| -rw-r--r-- | mips_new_tc/mips_extras_embed.lem | 24 | ||||
| -rw-r--r-- | mips_new_tc/mips_extras_embed_sequential.lem | 56 |
2 files changed, 40 insertions, 40 deletions
diff --git a/mips_new_tc/mips_extras_embed.lem b/mips_new_tc/mips_extras_embed.lem index 74bec64b..82f208f6 100644 --- a/mips_new_tc/mips_extras_embed.lem +++ b/mips_new_tc/mips_extras_embed.lem @@ -4,10 +4,10 @@ open import Sail_impl_base open import Sail_values open import Prompt -val MEMr : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserve : (vector bitU * integer) -> M (vector bitU) -val MEMr_tag : (vector bitU * integer) -> M (vector bitU) -val MEMr_tag_reserve : (vector bitU * integer) -> M (vector bitU) +val MEMr : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b +val MEMr_reserve : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b +val MEMr_tag : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b +val MEMr_tag_reserve : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'b let MEMr (addr,size) = read_mem false Read_plain addr size let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size @@ -16,10 +16,10 @@ let MEMr_tag (addr,size) = read_mem false Read_plain addr size let MEMr_tag_reserve (addr,size) = read_mem false Read_reserve addr size -val MEMea : (vector bitU * integer) -> M unit -val MEMea_conditional : (vector bitU * integer) -> M unit -val MEMea_tag : (vector bitU * integer) -> M unit -val MEMea_tag_conditional : (vector bitU * integer) -> M unit +val MEMea : forall 'a. Bitvector 'a => ('a * integer) -> M unit +val MEMea_conditional : forall 'a. Bitvector 'a => ('a * integer) -> M unit +val MEMea_tag : forall 'a. Bitvector 'a => ('a * integer) -> M unit +val MEMea_tag_conditional : forall 'a. Bitvector 'a => ('a * integer) -> M unit let MEMea (addr,size) = write_mem_ea Write_plain addr size let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size @@ -28,10 +28,10 @@ let MEMea_tag (addr,size) = write_mem_ea Write_plain addr size let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size -val MEMval : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bool -val MEMval_tag : (vector bitU * integer * vector bitU) -> M unit -val MEMval_tag_conditional : (vector bitU * integer * vector bitU) -> M bool +val MEMval : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M unit +val MEMval_conditional : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M bool +val MEMval_tag : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M unit +val MEMval_tag_conditional : forall 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M bool let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then true else false) diff --git a/mips_new_tc/mips_extras_embed_sequential.lem b/mips_new_tc/mips_extras_embed_sequential.lem index 4f690e5b..c32f297e 100644 --- a/mips_new_tc/mips_extras_embed_sequential.lem +++ b/mips_new_tc/mips_extras_embed_sequential.lem @@ -5,46 +5,46 @@ open import Sail_values open import Sail_operators_mwords open import State -val MEMr : forall 'regs 'a 'b. Size 'a, Size 'b => (bitvector 'a * integer) -> M 'regs (bitvector 'b) -val MEMr_reserve : forall 'regs 'a 'b. Size 'a, Size 'b => (bitvector 'a * integer) -> M 'regs (bitvector 'b) -val MEMr_tag : forall 'regs 'a 'b. Size 'a, Size 'b => (bitvector 'a * integer) -> M 'regs (bool * bitvector 'b) -val MEMr_tag_reserve : forall 'regs 'a 'b. Size 'a, Size 'b => (bitvector 'a * integer) -> M 'regs (bool * bitvector 'b) +val MEMr : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs 'b +val MEMr_reserve : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs 'b +val MEMr_tag : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs (bool * 'b) +val MEMr_tag_reserve : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs (bool * 'b) -let MEMr (addr,size) = read_mem false Read_plain (unsigned addr) size >>= fun v -> return (vec_to_bvec v) -let MEMr_reserve (addr,size) = read_mem false Read_reserve (unsigned addr) size >>= fun v -> return (vec_to_bvec v) +let MEMr (addr,size) = read_mem false Read_plain addr size +let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size let MEMr_tag (addr,size) = - read_mem false Read_plain (unsigned addr) size >>= fun v -> - read_tag false Read_plain (unsigned addr) >>= fun t -> - return (bitU_to_bool t, vec_to_bvec v) + read_mem false Read_plain addr size >>= fun v -> + read_tag false Read_plain addr >>= fun t -> + return (bitU_to_bool t, v) let MEMr_tag_reserve (addr,size) = - read_mem false Read_plain (unsigned addr) size >>= fun v -> - read_tag false Read_plain (unsigned addr) >>= fun t -> - return (bitU_to_bool t, vec_to_bvec v) + read_mem false Read_plain addr size >>= fun v -> + read_tag false Read_plain addr >>= fun t -> + return (bitU_to_bool t, v) -val MEMea : forall 'regs 'a. (bitvector 'a * integer) -> M 'regs unit -val MEMea_conditional : forall 'regs 'a. (bitvector 'a * integer) -> M 'regs unit -val MEMea_tag : forall 'regs 'a. (bitvector 'a * integer) -> M 'regs unit -val MEMea_tag_conditional : forall 'regs 'a. (bitvector 'a * integer) -> M 'regs unit +val MEMea : forall 'regs 'a. Bitvector 'a => ('a * integer) -> M 'regs unit +val MEMea_conditional : forall 'regs 'a. Bitvector 'a => ('a * integer) -> M 'regs unit +val MEMea_tag : forall 'regs 'a. Bitvector 'a => ('a * integer) -> M 'regs unit +val MEMea_tag_conditional : forall 'regs 'a. Bitvector 'a => ('a * integer) -> M 'regs unit -let MEMea (addr,size) = write_mem_ea Write_plain (unsigned addr) size -let MEMea_conditional (addr,size) = write_mem_ea Write_conditional (unsigned addr) size +let MEMea (addr,size) = write_mem_ea Write_plain addr size +let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size -let MEMea_tag (addr,size) = write_mem_ea Write_plain (unsigned addr) size -let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional (unsigned addr) size +let MEMea_tag (addr,size) = write_mem_ea Write_plain addr size +let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size -val MEMval : forall 'regs 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M 'regs unit -val MEMval_conditional : forall 'regs 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M 'regs bool -val MEMval_tag : forall 'regs 'a 'b. (bitvector 'a * integer * bool * bitvector 'b) -> M 'regs unit -val MEMval_tag_conditional : forall 'regs 'a 'b. (bitvector 'a * integer * bool * bitvector 'b) -> M 'regs bool +val MEMval : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M 'regs unit +val MEMval_conditional : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M 'regs bool +val MEMval_tag : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * bool * 'b) -> M 'regs unit +val MEMval_tag_conditional : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => ('a * integer * bool * 'b) -> M 'regs bool -let MEMval (_,_,v) = write_mem_val (bvec_to_vec v) >>= fun _ -> return () -let MEMval_conditional (_,_,v) = write_mem_val (bvec_to_vec v) >>= fun b -> return (if b then true else false) -let MEMval_tag (_,_,t,v) = write_mem_val (bvec_to_vec v) >>= fun _ -> write_tag (bool_to_bitU t) >>= fun _ -> return () -let MEMval_tag_conditional (_,_,t,v) = write_mem_val (bvec_to_vec v) >>= fun b -> write_tag (bool_to_bitU t) >>= fun _ -> return (if b then true else false) +let MEMval (_,size,v) = write_mem_val v >>= fun _ -> return () +let MEMval_conditional (_,size,v) = write_mem_val v >>= fun b -> return (if b then true else false) +let MEMval_tag (_,size,t,v) = write_mem_val v >>= fun _ -> write_tag (bool_to_bitU t) >>= fun _ -> return () +let MEMval_tag_conditional (_,size,t,v) = write_mem_val v >>= fun b -> write_tag (bool_to_bitU t) >>= fun _ -> return (if b then true else false) val MEM_sync : forall 'regs. unit -> M 'regs unit |