Source file sail2_prompt_monad.ml

(*Generated by Lem from sail2_prompt_monad.lem.*)
open Lem_pervasives_extra
(*open import Sail_impl_base*)
open Sail2_instr_kinds
open Sail2_values

type register_name = string
type address = bitU list

type( 'regval, 'a, 'e) monad =
  | Done of 'a
  (* Read a number of bytes from memory, returned in little endian order,
     with or without a tag.  The first nat specifies the address, the second
     the number of bytes. *)
  | Read_mem of read_kind * int * int * ( memory_byte list -> ('regval, 'a, 'e) monad)
  | Read_memt of read_kind * int * int * (( memory_byte list * bitU) -> ('regval, 'a, 'e) monad)
  (* Tell the system a write is imminent, at the given address and with the
     given size. *)
  | Write_ea of write_kind * int * int * ('regval, 'a, 'e) monad
  (* Request the result of store-exclusive *)
  | Excl_res of (bool -> ('regval, 'a, 'e) monad)
  (* Request to write a memory value of the given size at the given address,
     with or without a tag. *)
  | Write_mem of write_kind * int * int * memory_byte list * (bool -> ('regval, 'a, 'e) monad)
  | Write_memt of write_kind * int * int * memory_byte list * bitU * (bool -> ('regval, 'a, 'e) monad)
  (* Tell the system to dynamically recalculate dependency footprint *)
  | Footprint of ('regval, 'a, 'e) monad
  (* Request a memory barrier *)
  | Barrier of barrier_kind * ('regval, 'a, 'e) monad
  (* Request to read register, will track dependency when mode.track_values *)
  | Read_reg of register_name * ('regval -> ('regval, 'a, 'e) monad)
  (* Request to write register *)
  | Write_reg of register_name * 'regval * ('regval, 'a, 'e) monad
  (* Request to choose a (register) value, e.g. to resolve an undefined bit.
     The string argument may be used to provide information to the system
     about what the value is going to be used for. *)
  | Choose of string * ('regval -> ('regval, 'a, 'e) monad)
  (* Print debugging or tracing information *)
  | Print of string * ('regval, 'a, 'e) monad
  (*Result of a failed assert with possible error message to report*)
  | Fail of string
  (* Exception of type 'e *)
  | Exception of 'e

type 'regval event =
  | E_read_mem of read_kind * int * int * memory_byte list
  | E_read_memt of read_kind * int * int * ( memory_byte list * bitU)
  | E_write_mem of write_kind * int * int * memory_byte list * bool
  | E_write_memt of write_kind * int * int * memory_byte list * bitU * bool
  | E_write_ea of write_kind * int * int
  | E_excl_res of bool
  | E_barrier of barrier_kind
  | E_footprint
  | E_read_reg of register_name * 'regval
  | E_write_reg of register_name * 'regval
  | E_choose of string * 'regval
  | E_print of string

type 'regval trace = ( 'regval event) list

(*val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e*)
let return a:('rv,'a,'e)monad=  (Done a)

(*val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e*)
let rec bind m f:('rv,'b,'e)monad=  ((match m with
  | Done a -> f a
  | Read_mem( rk, a, sz, k) ->       Read_mem( rk, a, sz,       (fun v -> bind (k v) f))
  | Read_memt( rk, a, sz, k) ->      Read_memt( rk, a, sz,      (fun v -> bind (k v) f))
  | Write_mem( wk, a, sz, v, k) ->    Write_mem( wk, a, sz, v,    (fun v -> bind (k v) f))
  | Write_memt( wk, a, sz, v, t, k) -> Write_memt( wk, a, sz, v, t, (fun v -> bind (k v) f))
  | Read_reg( descr, k) ->         Read_reg( descr,         (fun v -> bind (k v) f))
  | Excl_res k ->               Excl_res               (fun v -> bind (k v) f)
  | Choose( descr, k) ->           Choose( descr,           (fun v -> bind (k v) f))
  | Write_ea( wk, a, sz, k) ->       Write_ea( wk, a, sz,       (bind k f))
  | Footprint k ->              Footprint              (bind k f)
  | Barrier( bk, k) ->             Barrier( bk,             (bind k f))
  | Write_reg( r, v, k) ->          Write_reg( r, v,          (bind k f))
  | Print( msg, k) ->              Print( msg,              (bind k f))
  | Fail descr ->               Fail descr
  | Exception e ->              Exception e
))

(*val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e*)
let exit ():('rv,'a,'e)monad=  (Fail "exit")

(*val assert_exp : forall 'rv 'e. bool -> string -> monad 'rv unit 'e*)
let assert_exp exp msg:('rv,(unit),'e)monad=  (if exp then Done () else Fail msg)

(*val throw : forall 'rv 'a 'e. 'e -> monad 'rv 'a 'e*)
let throw e:('rv,'a,'e)monad=  (Exception e)

(*val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 'e2) -> monad 'rv 'a 'e2*)
let rec try_catch m h:('rv,'a,'e2)monad=  ((match m with
  | Done a -> Done a
  | Read_mem( rk, a, sz, k) ->       Read_mem( rk, a, sz,       (fun v -> try_catch (k v) h))
  | Read_memt( rk, a, sz, k) ->      Read_memt( rk, a, sz,      (fun v -> try_catch (k v) h))
  | Write_mem( wk, a, sz, v, k) ->    Write_mem( wk, a, sz, v,    (fun v -> try_catch (k v) h))
  | Write_memt( wk, a, sz, v, t, k) -> Write_memt( wk, a, sz, v, t, (fun v -> try_catch (k v) h))
  | Read_reg( descr, k) ->         Read_reg( descr,         (fun v -> try_catch (k v) h))
  | Excl_res k ->               Excl_res               (fun v -> try_catch (k v) h)
  | Choose( descr, k) ->           Choose( descr,           (fun v -> try_catch (k v) h))
  | Write_ea( wk, a, sz, k) ->       Write_ea( wk, a, sz,       (try_catch k h))
  | Footprint k ->              Footprint              (try_catch k h)
  | Barrier( bk, k) ->             Barrier( bk,             (try_catch k h))
  | Write_reg( r, v, k) ->          Write_reg( r, v,          (try_catch k h))
  | Print( msg, k) ->              Print( msg,              (try_catch k h))
  | Fail descr ->               Fail descr
  | Exception e ->              h e
))

(* For early return, we abuse exceptions by throwing and catching
   the return value. The exception type is "either 'r 'e", where "Right e"
   represents a proper exception and "Left r" an early return of value "r". *)
type( 'rv, 'a, 'r, 'e) monadR = ('rv, 'a, ( ('r, 'e)Either.either)) monad

(*val early_return : forall 'rv 'a 'r 'e. 'r -> monadR 'rv 'a 'r 'e*)
let early_return r:('rv,'a,(('r,'e)Either.either))monad=  (throw (Either.Left r))

(*val catch_early_return : forall 'rv 'a 'e. monadR 'rv 'a 'a 'e -> monad 'rv 'a 'e*)
let catch_early_return m:('rv,'a,'e)monad=
   (try_catch m
    ((function
      | Either.Left a -> return a
      | Either.Right e -> throw e
     )))

(*val pure_early_return : forall 'a. either 'a 'a -> 'a*)
let pure_early_return:('a,'a)Either.either ->'a=  ((function
  | Either.Left a -> a
  | Either.Right a -> a
))

(*val either_bind : forall 'e 'a 'b. either 'e 'a -> ('a -> either 'e 'b) -> either 'e 'b*)
let either_bind m f:('e,'b)Either.either=
   ((match m with
  | Either.Left e -> Either.Left e
  | Either.Right x -> f x
  ))

(* Lift to monad with early return by wrapping exceptions *)
(*val liftR : forall 'rv 'a 'r 'e. monad 'rv 'a 'e -> monadR 'rv 'a 'r 'e*)
let liftR m:('rv,'a,(('r,'e)Either.either))monad=  (try_catch m (fun e -> throw (Either.Right e)))

(* Catch exceptions in the presence of early returns *)
(*val try_catchR : forall 'rv 'a 'r 'e1 'e2. monadR 'rv 'a 'r 'e1 -> ('e1 -> monadR 'rv 'a 'r 'e2) ->  monadR 'rv 'a 'r 'e2*)
let try_catchR m h:('rv,'a,(('r,'e2)Either.either))monad=
   (try_catch m
    ((function
      | Either.Left r -> throw (Either.Left r)
      | Either.Right e -> h e
     )))

(*val maybe_fail : forall 'rv 'a 'e. string -> maybe 'a -> monad 'rv 'a 'e*)
let maybe_fail msg:'a option ->('rv,'a,'e)monad=  ((function
  | Some a -> return a
  | None -> Fail msg
))

(*val choose_regval : forall 'rv 'e. string -> monad 'rv 'rv 'e*)
let choose_regval descr:('rv,'rv,'e)monad=  (Choose( descr, return))

(*val choose_convert : forall 'rv 'e 'a. ('rv -> maybe 'a) -> string -> monad 'rv 'a 'e*)
let choose_convert of_rv descr:('rv,'a,'e)monad=  (Choose( descr, (fun rv -> maybe_fail descr (of_rv rv))))

(*val choose_convert_default : forall 'rv 'e 'a. ('rv -> maybe 'a) -> 'a -> string -> monad 'rv 'a 'e*)
let choose_convert_default of_rv x descr:('rv,'a,'e)monad=  (Choose( descr, (fun rv -> return ((match of_rv rv with
    | Some a -> a
    | None -> x
  )))))

(*val choose_bool : forall 'rv 'e. Register_Value 'rv => string -> monad 'rv bool 'e*)
let choose_bool dict_Sail2_values_Register_Value_rv descr:('rv,(bool),'e)monad=  (choose_convert_default  
  dict_Sail2_values_Register_Value_rv.bool_of_regval_method false descr)

(*val choose_bit : forall 'rv 'e. Register_Value 'rv => string -> monad 'rv bitU 'e*)
let choose_bit dict_Sail2_values_Register_Value_rv descr:('rv,(bitU),'e)monad=  (bind (choose_bool 
  dict_Sail2_values_Register_Value_rv descr) (fun b -> return (bitU_of_bool b)))

(*val choose_int : forall 'rv 'e. Register_Value 'rv => string -> monad 'rv integer 'e*)
let choose_int dict_Sail2_values_Register_Value_rv descr:('rv,(Nat_big_num.num),'e)monad=  (choose_convert_default  
  dict_Sail2_values_Register_Value_rv.int_of_regval_method( (Nat_big_num.of_int 0)) descr)

(*val choose_real : forall 'rv 'e. Register_Value 'rv => string -> monad 'rv real 'e*)
let choose_real dict_Sail2_values_Register_Value_rv descr:('rv,(float),'e)monad=  (choose_convert_default  
  dict_Sail2_values_Register_Value_rv.real_of_regval_method((Nat_big_num.to_float (Nat_big_num.of_int 0))) descr)

(*val choose_string : forall 'rv 'e. Register_Value 'rv => string -> monad 'rv string 'e*)
let choose_string dict_Sail2_values_Register_Value_rv descr:('rv,(string),'e)monad=  (choose_convert_default  
  dict_Sail2_values_Register_Value_rv.string_of_regval_method "default" descr)

(*val headM : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e*)
let headM:'a list ->('rv,'a,'e)monad=  ((function
  | x :: _ -> return x
  | [] -> Fail "headM"
))

(*val tailM : forall 'rv 'a 'e. list 'a -> monad 'rv (list 'a) 'e*)
let tailM:'a list ->('rv,('a list),'e)monad=  ((function
  | _ :: xs -> return xs
  | [] -> Fail "tailM"
))

(*val read_memt_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e*)
let read_memt_bytes dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b rk addr sz:('rv,((memory_byte)list*bitU),'e)monad=
   (bind
    (maybe_fail "nat_of_bv" (nat_of_bv 
  dict_Sail2_values_Bitvector_a addr))
    (fun addr -> Read_memt( rk, addr, (nat_of_int sz), return)))

(*val read_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e*)
let read_memt dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b rk addr sz:('rv,('b*bitU),'e)monad=
   (bind
    (read_memt_bytes dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_a rk addr sz)
    (fun (bytes, tag) ->
       (match  dict_Sail2_values_Bitvector_b.of_bits_method (bits_of_mem_bytes bytes) with
         | Some v -> return (v, tag)
         | None -> Fail "bits_of_mem_bytes"
       )))

(*val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e*)
let read_mem_bytes dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b rk addr sz:('rv,((memory_byte)list),'e)monad=
   (bind
    (maybe_fail "nat_of_bv" (nat_of_bv 
  dict_Sail2_values_Bitvector_a addr))
    (fun addr -> Read_mem( rk, addr, (nat_of_int sz), return)))

(*val read_mem : forall 'rv 'a 'b 'e 'addrsize. Bitvector 'a, Bitvector 'b => read_kind -> 'addrsize -> 'a -> integer -> monad 'rv 'b 'e*)
let read_mem dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b rk _addr_sz addr sz:('rv,'b,'e)monad=
   (bind
    (read_mem_bytes dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_a rk addr sz)
    (fun bytes ->
       (match  dict_Sail2_values_Bitvector_b.of_bits_method (bits_of_mem_bytes bytes) with
         | Some v -> return v
         | None -> Fail "bits_of_mem_bytes"
       )))

(*val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e*)
let excl_result ():('rv,(bool),'e)monad=
   (let k successful=  (return successful) in
  Excl_res k)

(*val write_mem_ea : forall 'rv 'a 'e 'addrsize. Bitvector 'a => write_kind -> 'addrsize -> 'a -> integer -> monad 'rv unit 'e*)
let write_mem_ea dict_Sail2_values_Bitvector_a wk _addr_size addr sz:('rv,(unit),'e)monad=
   (bind
    (maybe_fail "nat_of_bv" (nat_of_bv 
  dict_Sail2_values_Bitvector_a addr))
    (fun addr -> Write_ea( wk, addr, (nat_of_int sz), (Done ()))))

(*val write_mem : forall 'rv 'a 'b 'e 'addrsize. Bitvector 'a, Bitvector 'b =>
  write_kind -> 'addrsize -> 'a -> integer -> 'b -> monad 'rv bool 'e*)
let write_mem dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b wk _addr_size addr sz v:('rv,(bool),'e)monad=
   ((match (mem_bytes_of_bits 
  dict_Sail2_values_Bitvector_b v, nat_of_bv dict_Sail2_values_Bitvector_a addr) with
    | (Some v, Some addr) ->
       Write_mem( wk, addr, (nat_of_int sz), v, return)
    | _ -> Fail "write_mem"
  ))

(*val write_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
  write_kind -> 'a -> integer -> 'b -> bitU -> monad 'rv bool 'e*)
let write_memt dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b wk addr sz v tag:('rv,(bool),'e)monad=
   ((match (mem_bytes_of_bits 
  dict_Sail2_values_Bitvector_b v, nat_of_bv dict_Sail2_values_Bitvector_a addr) with
    | (Some v, Some addr) ->
       Write_memt( wk, addr, (nat_of_int sz), v, tag, return)
    | _ -> Fail "write_mem"
  ))

(*val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e*)
let read_reg reg:('rv,'a,'e)monad=
   (let k v=
     ((match reg.of_regval v with
      | Some v -> Done v
      | None -> Fail "read_reg: unrecognised value"
    ))
  in
  Read_reg( reg.name, k))

(*val write_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> 'a -> monad 'rv unit 'e*)
let write_reg reg v:('rv,(unit),'e)monad=  (Write_reg( reg.name, (reg.regval_of v), (Done ())))

(* TODO
let write_reg reg v =
  write_reg_aux (external_reg_whole reg) v
let write_reg_range reg i j v =
  write_reg_aux (external_reg_slice reg (nat_of_int i,nat_of_int j)) v
let write_reg_pos reg i v =
  let iN = nat_of_int i in
  write_reg_aux (external_reg_slice reg (iN,iN)) [v]
let write_reg_bit = write_reg_pos
let write_reg_field reg regfield v =
  write_reg_aux (external_reg_field_whole reg regfield.field_name) v
let write_reg_field_bit reg regfield bit =
  write_reg_aux (external_reg_field_whole reg regfield.field_name)
                (Vector [bit] 0 (is_inc_of_reg reg))
let write_reg_field_range reg regfield i j v =
  write_reg_aux (external_reg_field_slice reg regfield.field_name (nat_of_int i,nat_of_int j)) v
let write_reg_field_pos reg regfield i v =
  write_reg_field_range reg regfield i i [v]
let write_reg_field_bit = write_reg_field_pos*)

(*val barrier : forall 'rv 'e. barrier_kind -> monad 'rv unit 'e*)
let barrier bk:('rv,(unit),'e)monad=  (Barrier( bk, (Done ())))

(*val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e*)
let footprint _:('rv,(unit),'e)monad=  (Footprint (Done ()))

(* Event traces *)

(*val emitEvent : forall 'regval 'a 'e. Eq 'regval => monad 'regval 'a 'e -> event 'regval -> maybe (monad 'regval 'a 'e)*)
let emitEvent dict_Basic_classes_Eq_regval m e:(('regval,'a,'e)monad)option=  ((match (e, m) with
  | (E_read_mem( rk, a, sz, v), Read_mem( rk', a', sz', k)) ->
     if (rk' = rk) && ((a' = a) && (sz' = sz)) then Some (k v) else None
  | (E_read_memt( rk, a, sz, vt), Read_memt( rk', a', sz', k)) ->
     if (rk' = rk) && ((a' = a) && (sz' = sz)) then Some (k vt) else None
  | (E_write_mem( wk, a, sz, v, r), Write_mem( wk', a', sz', v', k)) ->
     if (wk' = wk) && ((a' = a) && ((sz' = sz) && (listEqualBy (listEqualBy (=)) v' v))) then Some (k r) else None
  | (E_write_memt( wk, a, sz, v, tag, r), Write_memt( wk', a', sz', v', tag', k)) ->
     if (wk' = wk) && ((a' = a) && ((sz' = sz) && ((listEqualBy (listEqualBy (=)) v' v) && (tag' = tag)))) then Some (k r) else None
  | (E_read_reg( r, v), Read_reg( r', k)) ->
     if r' = r then Some (k v) else None
  | (E_write_reg( r, v), Write_reg( r', v', k)) ->
     if (r' = r) && dict_Basic_classes_Eq_regval.isEqual_method v' v then Some k else None
  | (E_write_ea( wk, a, sz), Write_ea( wk', a', sz', k)) ->
     if (wk' = wk) && ((a' = a) && (sz' = sz)) then Some k else None
  | (E_barrier bk, Barrier( bk', k)) ->
     if bk' = bk then Some k else None
  | (E_print m, Print( m', k)) ->
     if m' = m then Some k else None
  | (E_excl_res v, Excl_res k) -> Some (k v)
  | (E_choose( descr, v), Choose( descr', k)) -> if descr' = descr then Some (k v) else None
  | (E_footprint, Footprint k) -> Some k
  | _ -> None
))

(*val runTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> maybe (monad 'regval 'a 'e)*)
let rec runTrace dict_Basic_classes_Eq_regval t m:(('regval,'a,'e)monad)option=  ((match t with
  | [] -> Some m
  | e :: t' -> Lem.option_bind (emitEvent 
  dict_Basic_classes_Eq_regval m e) (runTrace dict_Basic_classes_Eq_regval t')
))

(*val final : forall 'regval 'a 'e. monad 'regval 'a 'e -> bool*)
let final:('regval,'a,'e)monad ->bool=  ((function
  | Done _ -> true
  | Fail _ -> true
  | Exception _ -> true
  | _ -> false
))

(*val hasTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool*)
let hasTrace dict_Basic_classes_Eq_regval t m:bool=  ((match runTrace 
  dict_Basic_classes_Eq_regval t m with
  | Some m -> final m
  | None -> false
))

(*val hasException : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool*)
let hasException dict_Basic_classes_Eq_regval t m:bool=  ((match runTrace 
  dict_Basic_classes_Eq_regval t m with
  | Some (Exception _) -> true
  | _ -> false
))

(*val hasFailure : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool*)
let hasFailure dict_Basic_classes_Eq_regval t m:bool=  ((match runTrace 
  dict_Basic_classes_Eq_regval t m with
  | Some (Fail _) -> true
  | _ -> false
))

(* Define a type synonym that also takes the register state as a type parameter,
   in order to make switching to the state monad without changing generated
   definitions easier, see also lib/hol/prompt_monad.lem. *)

type( 'regval, 'regstate, 'a, 'e) base_monad = ('regval, 'a, 'e) monad
type( 'regval, 'regstate, 'a, 'r, 'e) base_monadR = ('regval, 'a, 'r, 'e) monadR