open import Pervasives
open import Vector
open import State
open import Sail_values

(*
let rec countLeadingZeros_helper bits =  
((match bits with
    | (Interp.V_lit (L_aux( L_zero, _)))::bits -> 
      let (Interp.V_lit (L_aux( (L_num n), loc))) = (countLeadingZeros_helper bits) in
      Interp.V_lit (L_aux( (L_num (Nat_big_num.add n(Nat_big_num.of_int 1))), loc))
    | _ -> Interp.V_lit (L_aux( (L_num(Nat_big_num.of_int 0)), Interp_ast.Unknown))
))
let rec countLeadingZeros (Interp.V_tuple v) = ((match v with
  | [Interp.V_track( v, r);Interp.V_track( v2, r2)] -> 
    Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) ( Pset.(union) r r2)
  | [Interp.V_track( v, r);v2] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r
  | [v;Interp.V_track( v2, r2)] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r2
  | [Interp.V_unknown;_] -> Interp.V_unknown
  | [_;Interp.V_unknown] -> Interp.V_unknown
  | [Interp.V_vector( _, _, bits);Interp.V_lit (L_aux( (L_num n), _))] -> 
    countLeadingZeros_helper (snd (Lem_list.split_at (abs (Nat_big_num.to_int n)) bits))
))
 *)

let MEMr (addr,l) = read_memory (unsigned addr) l
let MEMr_reserve (addr,l) = read_memory (unsigned addr) l

let MEMw_EA (addr,l) = write_writeEA (unsigned addr) l
let MEMw_EA_conditional (addr,l) = write_writeEA (unsigned addr) l
                                        
let MEMw (addr,l,value) = write_memory (unsigned addr) l value
let MEMw_conditional (addr,l,value) = write_memory (unsigned addr) l value >> return true

let I_Sync () = return ()
let H_Sync () = return ()
let LW_Sync () = return ()
let EIEIO_Sync () = return ()

let recalculate_dependency () = return ()

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

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