diff options
Diffstat (limited to 'mips_new_tc/mips_extras_embed_sequential.lem')
| -rw-r--r-- | mips_new_tc/mips_extras_embed_sequential.lem | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/mips_new_tc/mips_extras_embed_sequential.lem b/mips_new_tc/mips_extras_embed_sequential.lem index c32f297e..b50052dc 100644 --- a/mips_new_tc/mips_extras_embed_sequential.lem +++ b/mips_new_tc/mips_extras_embed_sequential.lem @@ -5,10 +5,10 @@ open import Sail_values open import Sail_operators_mwords open import State -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) +val MEMr : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs 'b 'e +val MEMr_reserve : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs 'b 'e +val MEMr_tag : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs (bool * 'b) 'e +val MEMr_tag_reserve : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer) -> M 'regs (bool * 'b) 'e let MEMr (addr,size) = read_mem false Read_plain addr size let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size @@ -24,10 +24,10 @@ let MEMr_tag_reserve (addr,size) = return (bitU_to_bool t, v) -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 +val MEMea : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e +val MEMea_conditional : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e +val MEMea_tag : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e +val MEMea_tag_conditional : forall 'regs 'a 'e. Bitvector 'a => ('a * integer) -> M 'regs unit 'e let MEMea (addr,size) = write_mem_ea Write_plain addr size let MEMea_conditional (addr,size) = write_mem_ea Write_conditional addr size @@ -36,16 +36,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 '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 +val MEMval : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M 'regs unit 'e +val MEMval_conditional : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * 'b) -> M 'regs bool 'e +val MEMval_tag : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * bool * 'b) -> M 'regs unit 'e +val MEMval_tag_conditional : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => ('a * integer * bool * 'b) -> M 'regs bool 'e 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 +val MEM_sync : forall 'regs 'e. unit -> M 'regs unit 'e let MEM_sync () = barrier Barrier_MIPS_SYNC |