open import Pervasives
open import Sail_impl_base
open import Vector
open import Sail_values
open import Prompt

val MEMr         : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)
val MEMr_reserve : forall 'e. (vector bitU * integer) -> M 'e (vector bitU)

let MEMr (addr,size) = read_memory Read_plain addr size
let MEMr_reserve (addr,size) = read_memory Read_reserve addr size


val MEMw_EA      : forall 'e. (vector bitU * integer) -> M 'e unit
val MEMr_EA_cond : forall 'e. (vector bitU * integer) -> M 'e unit
                                                           
let MEMw_EA (addr,size) = write_memory_ea Write_plain addr size
let MEMw_EA_cond (addr,size) = write_memory_ea Write_conditional addr size


val MEMw             : forall 'e. (vector bitU * integer * vector bitU) -> M 'e unit
val MEMw_conditional : forall 'e. (vector bitU * integer * vector bitU) -> M 'e bitU

let MEMw (_,_,value) = write_memory_val value >>= fun _ -> return ()
let MEMw_conditional (_,_,value) = write_memory_val value >>= fun b -> return (bool_to_bit b)


val I_Sync     : forall 'e unit -> M 'e unit
val H_Sync     : forall 'e unit -> M 'e unit
val LW_Sync    : forall 'e unit -> M 'e unit
val EIEIO_Sync : forall 'e unit -> M 'e unit

let I_Sync ()     = barrier Isync
let H_Sync ()     = barrier Sync
let LW_Sync ()    = barrier LwSync
let EIEIO_Sync () = barrier Eieio

let recalculate_dependency () = footprint

let trap () = exit "error"
(* this needs to change, but for that we'd have to make the type checker know about trap 
 * as an effect *)

val countLeadingZeroes : vector bitU * integer -> integer
let countLeadingZeroes (Vector bits _ _ ,n)  = 
  let (_,bits) = List.splitAt (natFromInteger n) bits in
  integerFromNat (List.length (takeWhile ((=) O) bits))