Updates to interpreter

Experimenting with porting riscv model to new typechecker

1 files changed, 0 insertions, 71 deletions

diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem
deleted file mode 100644
index 3c922268..00000000
--- a/risc-v/riscv_extras_embed_sequential.lem
+++ /dev/null
@@ -1,71 +0,0 @@
-open import Pervasives
-open import Pervasives_extra
-open import Sail_impl_base
-open import Sail_values
-open import State
-
-val MEMr                  : (vector bitU * integer) -> M (vector bitU)
-val MEMr_acquire          : (vector bitU * integer) -> M (vector bitU)
-val MEMr_strong_acquire   : (vector bitU * integer) -> M (vector bitU)
-val MEMr_reserved         : (vector bitU * integer) -> M (vector bitU)
-val MEMr_reserved_acquire : (vector bitU * integer) -> M (vector bitU)
-val MEMr_reserved_strong_acquire : (vector bitU * integer) -> M (vector bitU)
-
-let MEMr (addr,size)                  = read_mem false Read_plain addr size
-let MEMr_acquire (addr,size)          = read_mem false Read_RISCV_acquire addr size
-let MEMr_strong_acquire (addr,size)   = read_mem false Read_RISCV_strong_acquire addr size
-let MEMr_reserved (addr,size)         = read_mem false Read_RISCV_reserved addr size
-let MEMr_reserved_acquire (addr,size) = read_mem false Read_RISCV_reserved_acquire addr size
-let MEMr_reserved_strong_acquire (addr,size)
-                                      = read_mem false Read_RISCV_reserved_strong_acquire addr size
-
-val MEMea                     : (vector bitU * integer) -> M unit
-val MEMea_release             : (vector bitU * integer) -> M unit
-val MEMea_strong_release             : (vector bitU * integer) -> M unit
-val MEMea_conditional         : (vector bitU * integer) -> M unit
-val MEMea_conditional_release : (vector bitU * integer) -> M unit
-val MEMea_conditional_strong_release : (vector bitU * integer) -> M unit
-
-let MEMea (addr,size)                     = write_mem_ea Write_plain addr size
-let MEMea_release (addr,size)             = write_mem_ea Write_RISCV_release addr size
-let MEMea_strong_release (addr,size)      = write_mem_ea Write_RISCV_strong_release addr size
-let MEMea_conditional (addr,size)         = write_mem_ea Write_RISCV_conditional addr size
-let MEMea_conditional_release (addr,size) = write_mem_ea Write_RISCV_conditional_release addr size
-let MEMea_conditional_strong_release (addr,size)
-                                          = write_mem_ea Write_RISCV_conditional_strong_release addr size
-
-val MEMval                     : (vector bitU * integer * vector bitU) -> M unit
-val MEMval_release             : (vector bitU * integer * vector bitU) -> M unit
-val MEMval_strong_release      : (vector bitU * integer * vector bitU) -> M unit
-val MEMval_conditional         : (vector bitU * integer * vector bitU) -> M unit
-val MEMval_conditional_release : (vector bitU * integer * vector bitU) -> M unit
-val MEMval_conditional_strong_release : (vector bitU * integer * vector bitU) -> M unit
-
-let MEMval (_,_,v)                     = write_mem_val v >>= fun _ -> return ()
-let MEMval_release (_,_,v)             = write_mem_val v >>= fun _ -> return ()
-let MEMval_strong_release (_,_,v)      = write_mem_val v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v)         = write_mem_val v >>= fun _ -> return ()
-let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return ()
-let MEMval_conditional_strong_release (_,_,v)
-                                       = write_mem_val v >>= fun _ -> return ()
-
-let speculate_conditional_success () = excl_result () >>= fun b -> return (if b then B1 else B0)
-
-val MEM_fence_rw_rw : unit -> M unit
-val MEM_fence_r_rw  : unit -> M unit
-val MEM_fence_r_r   : unit -> M unit
-val MEM_fence_rw_w  : unit -> M unit
-val MEM_fence_w_w   : unit -> M unit
-val MEM_fence_i     : unit -> M unit
-
-let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
-let MEM_fence_r_rw  () = barrier Barrier_RISCV_r_rw
-let MEM_fence_r_r   () = barrier Barrier_RISCV_r_r
-let MEM_fence_rw_w  () = barrier Barrier_RISCV_rw_w
-let MEM_fence_w_w   () = barrier Barrier_RISCV_w_w
-let MEM_fence_i     () = barrier Barrier_RISCV_i
-
-let duplicate (bit,len) =
-  let bits = repeat [bit] len in
-  let start = len - 1 in
-  Vector bits start false