diff options
Diffstat (limited to 'mips_new_tc/mips_extras_embed_sequential.lem')
| -rw-r--r-- | mips_new_tc/mips_extras_embed_sequential.lem | 27 |
1 files changed, 13 insertions, 14 deletions
diff --git a/mips_new_tc/mips_extras_embed_sequential.lem b/mips_new_tc/mips_extras_embed_sequential.lem index ad567598..f9c6c92c 100644 --- a/mips_new_tc/mips_extras_embed_sequential.lem +++ b/mips_new_tc/mips_extras_embed_sequential.lem @@ -4,10 +4,10 @@ open import Sail_impl_base open import Sail_values open import State -val MEMr : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitvector 'b) -val MEMr_reserve : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitvector 'b) -val MEMr_tag : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitU * bitvector 'b) -val MEMr_tag_reserve : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitU * bitvector 'b) +val MEMr : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bitvector 'b) +val MEMr_reserve : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bitvector 'b) +val MEMr_tag : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bitU * bitvector 'b) +val MEMr_tag_reserve : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bitU * bitvector 'b) let MEMr (addr,size) = read_mem false Read_plain addr size let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size @@ -23,10 +23,10 @@ let MEMr_tag_reserve (addr,size) = return (t, v) -val MEMea : forall 'a. (bitvector 'a * integer) -> M unit -val MEMea_conditional : forall 'a. (bitvector 'a * integer) -> M unit -val MEMea_tag : forall 'a. (bitvector 'a * integer) -> M unit -val MEMea_tag_conditional : forall 'a. (bitvector 'a * integer) -> M unit +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 let MEMea (addr,size) = write_mem_ea Write_plain addr size let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size @@ -35,17 +35,16 @@ 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 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M unit -val MEMval_conditional : forall 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M bool -val MEMval_tag : forall 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M unit -val MEMval_tag_conditional : forall 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M bool +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 * bitU * bitvector 'b) -> M 'regs unit +val MEMval_tag_conditional : forall 'regs 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M 'regs 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) let MEMval_tag (_,_,t,v) = write_mem_val v >>= fun _ -> write_tag t >>= fun _ -> return () let MEMval_tag_conditional (_,_,t,v) = write_mem_val v >>= fun b -> write_tag t >>= fun _ -> return (if b then true else false) -val MEM_sync : unit -> M unit +val MEM_sync : forall 'regs. unit -> M 'regs unit let MEM_sync () = barrier Barrier_MIPS_SYNC - |