sail2_concurrency_interface.lem

open import Pervasives_extra
open import Sail2_values
open import Sail2_string




type Access_variety = | AV_plain | AV_exclusive | AV_atomic_rmw



type Access_strength = | AS_normal | AS_rel_or_acq | AS_acq_rcpc



type Explicit_access_kind  =
  <| Explicit_access_kind_variety : Access_variety; Explicit_access_kind_strength : Access_strength; |>


type Access_kind 'arch_ak = | AK_explicit of (Explicit_access_kind) | AK_ifetch of (unit) | AK_ttw of (unit) | AK_arch of 'arch_ak



(* This is the type for read requests as Sail would generate, using
   machine words.  We also define a version with bitlists below and a
   conversion because we use the latter in the monad below due to a
   lack of support for variable/dependent bitvector lengths in
   Isabelle/HOL *)

type Mem_read_request 'vasize 'pa 'ts 'arch_ak =
  <| Mem_read_request_access_kind : (Access_kind 'arch_ak);
     Mem_read_request_va : maybe (mword 'vasize);
     Mem_read_request_pa : 'pa;
     Mem_read_request_translation : 'ts;
     Mem_read_request_size : integer;
     Mem_read_request_tag : bool; |>
declare isabelle target_sorts Mem_read_request = `len` _ _ _

type Mem_read_request_bl 'pa 'ts 'arch_ak =
  <| Mem_read_request_bl_access_kind : (Access_kind 'arch_ak);
     Mem_read_request_bl_va : maybe (list bitU);
     Mem_read_request_bl_pa : 'pa;
     Mem_read_request_bl_translation : 'ts;
     Mem_read_request_bl_size : integer;
     Mem_read_request_bl_tag : bool; |>

val mem_read_request_to_bl : forall  'vasize 'pa 'ts 'arch_ak. Size 'vasize => Mem_read_request  'vasize 'pa 'ts 'arch_ak -> Mem_read_request_bl 'pa 'ts 'arch_ak
let mem_read_request_to_bl req =
  <| Mem_read_request_bl_access_kind = req.Mem_read_request_access_kind;
     Mem_read_request_bl_va = Maybe.map bits_of req.Mem_read_request_va;
     Mem_read_request_bl_pa = req.Mem_read_request_pa;
     Mem_read_request_bl_translation = req.Mem_read_request_translation;
     Mem_read_request_bl_size = req.Mem_read_request_size;
     Mem_read_request_bl_tag = req.Mem_read_request_tag; |>

(* Similarly, we have machine word and bitlist versions of write requests. *)

type Mem_write_request 'vasize 'pa 'ts 'arch_ak 'p8_times_n =
  <| Mem_write_request_access_kind : Access_kind 'arch_ak;
     Mem_write_request_va : maybe (mword 'vasize);
     Mem_write_request_pa : 'pa;
     Mem_write_request_translation : 'ts;
     Mem_write_request_size : integer;
     Mem_write_request_value : maybe (mword 'p8_times_n);
     Mem_write_request_tag : maybe bool; |>
declare isabelle target_sorts Mem_write_request = `len` _ _ _ `len`

type Mem_write_request_bl 'pa 'ts 'arch_ak =
  <| Mem_write_request_bl_access_kind : (Access_kind 'arch_ak);
     Mem_write_request_bl_va : maybe (list bitU);
     Mem_write_request_bl_pa : 'pa;
     Mem_write_request_bl_translation : 'ts;
     Mem_write_request_bl_size : integer;
     Mem_write_request_bl_value : maybe (list bitU);
     Mem_write_request_bl_tag : maybe bool; |>

val mem_write_request_to_bl : forall  'vasize 'pa 'ts 'arch_ak 'p8_times_n. Size 'vasize, Size 'p8_times_n => Mem_write_request 'vasize 'pa 'ts 'arch_ak 'p8_times_n -> Mem_write_request_bl 'pa 'ts 'arch_ak
let mem_write_request_to_bl req =
  <| Mem_write_request_bl_access_kind = req.Mem_write_request_access_kind;
     Mem_write_request_bl_va = Maybe.map bits_of req.Mem_write_request_va;
     Mem_write_request_bl_pa = req.Mem_write_request_pa;
     Mem_write_request_bl_translation = req.Mem_write_request_translation;
     Mem_write_request_bl_size = req.Mem_write_request_size;
     Mem_write_request_bl_value = Maybe.map bits_of req.Mem_write_request_value;
     Mem_write_request_bl_tag = req.Mem_write_request_tag; |>

type Mem_write_announce_address 'pa =
  <| Mem_write_announce_address_pa : 'pa;
     Mem_write_announce_address_size : integer; |>


type monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e =
  | Done of 'a
  | Fail of string
  | Exception of 'e
  | Choose of string * ('regval -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e)
  | Read_reg of string * ('regval -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e)
  | Write_reg of string * 'regval * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e
  | Mem_read_request of Mem_read_request_bl 'pa 'translation_summary 'arch_ak * (result (list bitU * maybe bool) 'abort -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e)
  | Mem_write_request of Mem_write_request_bl 'pa 'translation_summary 'arch_ak * (result (maybe bool) 'abort -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e)
  | Mem_write_announce_address of Mem_write_announce_address 'pa * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e
  | Branch_announce_address of (list bitU) * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e
  | Barrier_request of 'barrier * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e
  | Cache_op_request of 'cache_op * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e
  | TLB_op_request of 'tlb_op * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e
  | Fault_announce of 'fault * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e
  | Eret_announce of 'pa * monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e

type event 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval =
  | E_choose of string * 'regval
  | E_read_reg of string * 'regval
  | E_write_reg of string * 'regval
  | E_mem_read_request of Mem_read_request_bl 'pa 'translation_summary 'arch_ak * result (list bitU * maybe bool) 'abort
  | E_mem_write_request of Mem_write_request_bl 'pa 'translation_summary 'arch_ak * result (maybe bool) 'abort
  | E_mem_write_announce_address of Mem_write_announce_address 'pa
  | E_branch_announce_address of (list bitU)
  | E_barrier_request of 'barrier
  | E_cache_op_request of 'cache_op
  | E_tlb_op_request of 'tlb_op
  | E_fault_announce of 'fault
  | E_eret_announce of 'pa

type trace 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval =
  list (event 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval)

val return : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e.
  'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e
let return a = Done a

val bind : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'b 'e.
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e ->
  ('a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'b 'e) ->
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'b 'e
let rec bind m f = match m with
  | Done a -> f a
  | Fail msg -> Fail msg
  | Exception e -> Exception e
  | Choose msg k -> Choose msg (fun v -> bind (k v) f)
  | Read_reg r k -> Read_reg r (fun v -> bind (k v) f)
  | Write_reg r v k -> Write_reg r v (bind k f)
  | Mem_read_request req k -> Mem_read_request req (fun v -> bind (k v) f)
  | Mem_write_request req k -> Mem_write_request req (fun v -> bind (k v) f)
  | Mem_write_announce_address a k -> Mem_write_announce_address a (bind k f)
  | Branch_announce_address addr k -> Branch_announce_address addr (bind k f)
  | Barrier_request b k -> Barrier_request b (bind k f)
  | Cache_op_request c k -> Cache_op_request c (bind k f)
  | TLB_op_request t k -> TLB_op_request t (bind k f)
  | Fault_announce fault k -> Fault_announce fault (bind k f)
  | Eret_announce pa k -> Eret_announce pa (bind k f)
end

val throw : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e.
  'e -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e
let throw e = Exception e

val try_catch : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e1 'e2.
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e1 ->
  ('e1 -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e2) ->
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e2
let rec try_catch m h = match m with
  | Done a -> Done a
  | Fail msg -> Fail msg
  | Exception e -> h e
  | Choose msg k -> Choose msg (fun v -> try_catch (k v) h)
  | Read_reg r k -> Read_reg r (fun v -> try_catch (k v) h)
  | Write_reg r v k -> Write_reg r v (try_catch k h)
  | Mem_read_request req k -> Mem_read_request req (fun v -> try_catch (k v) h)
  | Mem_write_request req k -> Mem_write_request req (fun v -> try_catch (k v) h)
  | Mem_write_announce_address a k -> Mem_write_announce_address a (try_catch k h)
  | Branch_announce_address addr k -> Branch_announce_address addr (try_catch k h)
  | Barrier_request b k -> Barrier_request b (try_catch k h)
  | Cache_op_request c k -> Cache_op_request c (try_catch k h)
  | TLB_op_request t k -> TLB_op_request t (try_catch k h)
  | Fault_announce fault k -> Fault_announce fault (try_catch k h)
  | Eret_announce pa k -> Eret_announce pa (try_catch k h)
end

(* 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 monadR 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'r 'e =
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a (either 'r 'e)

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

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

val pure_early_return : forall 'a. either 'a 'a -> 'a
let pure_early_return = function
  | Left a -> a
  | Right a -> a
end

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

(* 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 = try_catch m (fun e -> throw (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 =
  try_catch m
    (function
      | Left r -> throw (Left r)
      | Right e -> h e
     end)

(* val maybe_fail : forall 'rv 'a 'e. string -> maybe 'a -> monad 'rv 'a 'e *)
let maybe_fail msg = function
  | Just a -> return a
  | Nothing -> Fail msg
end

val assert_exp : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e.
  bool -> string -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e
let assert_exp exp msg = if exp then Done () else Fail msg

val exit : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e.
  unit -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e
let exit _ = Fail "exit"

val read_reg : forall 's 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e.
  register_ref 's 'regval 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e
let read_reg reg =
  let k v =
    match reg.of_regval v with
      | Just v -> Done v
      | Nothing -> Fail "read_reg: unrecognised value"
    end
  in
  Read_reg reg.name k

let inline reg_deref = read_reg

val write_reg : forall 's 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e.
  register_ref 's 'regval 'a -> 'a -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e
let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ())

val choose_regval : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'e.
  string -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'rv 'e
let choose_regval descr = Choose descr return

val choose_convert : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'e 'a.
  ('rv -> maybe 'a) -> string -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e
let choose_convert of_rv descr = Choose descr (fun rv -> maybe_fail descr (of_rv rv))

val choose_convert_default : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'e 'a.
  ('rv -> maybe 'a) -> 'a -> string -> monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'rv 'a 'e
let choose_convert_default of_rv x descr = Choose descr (fun rv -> return (match of_rv rv with
    | Just a -> a
    | Nothing -> x
  end))

let choose_bool descr = choose_convert_default bool_of_regval false descr
let choose_bit descr = bind (choose_bool descr) (fun b -> return (bitU_of_bool b))
let choose_int descr = choose_convert_default int_of_regval 0 descr
let choose_real descr = choose_convert_default real_of_regval 0 descr
let choose_string descr = choose_convert_default string_of_regval "default" descr

let headM = function
  | x :: _ -> return x
  | [] -> Fail "headM"
end

let tailM = function
  | _ :: xs -> return xs
  | [] -> Fail "tailM"
end

val sail_mem_read : forall 'vasize 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'bv 'e. Size 'vasize, Bitvector 'bv =>
  Mem_read_request 'vasize 'pa 'translation_summary 'arch_ak ->
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval (result ('bv * maybe bool) 'abort) 'e
let sail_mem_read req =
  let k = function
    | Ok (res, tag) ->
       match of_bits res with
       | Just res -> return (Ok (res, tag))
       | Nothing -> Fail "sail_mem_read_request: unrecognised value"
       end
    | Err e -> return (Err e)
  end in
  Mem_read_request (mem_read_request_to_bl req) k

val sail_mem_write : forall 'vasize 'valuesize 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e. Size 'vasize, Size 'valuesize =>
  Mem_write_request 'vasize 'pa 'translation_summary 'arch_ak 'valuesize ->
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval (result (maybe bool) 'abort) 'e
let sail_mem_write req = Mem_write_request (mem_write_request_to_bl req) return

val sail_mem_write_announce_address : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e.
  Mem_write_announce_address 'pa ->
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e
let sail_mem_write_announce_address req = Mem_write_announce_address req (return ())

val instr_announce : forall 'instr 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e.
  'instr ->
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e
let instr_announce pa = return () (* TODO *)

val branch_announce : forall 'addr 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e. Bitvector 'addr =>
  integer -> 'addr ->
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e
let branch_announce addr_size addr = Branch_announce_address (bits_of addr) (return ())

val sail_barrier : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e.
  'barrier ->
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e
let sail_barrier barrier = Barrier_request barrier (return ())

val sail_cache_op : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e.
  'cache_op ->
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e
let sail_cache_op cache_op = Cache_op_request cache_op (return ())

val sail_tlbi : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e.
  'tlb_op ->
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e
let sail_tlbi tlb_op = TLB_op_request tlb_op (return ())

val sail_take_exception : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e.
  'fault ->
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e
let sail_take_exception fault = Fault_announce fault (return ())

val sail_return_exception : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e.
  'pa ->
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e
let sail_return_exception pa = Eret_announce pa (return ())

val sail_instr_announce : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'e.
  'pa ->
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval unit 'e
let sail_instr_announce pa = return ()

(* Event traces *)

val emitEvent : forall 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e.
  Eq 'regval, Eq 'pa, Eq 'barrier, Eq 'cache_op, Eq 'tlb_op, Eq 'fault =>
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e
  -> event 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval
  -> maybe (monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e)
let emitEvent m e = match (e, m) with
  | (E_choose descr v, Choose descr' k) -> if descr' = descr then Just (k v) else Nothing
  | (E_read_reg r v, Read_reg r' k) ->
     if r' = r then Just (k v) else Nothing
  | (E_write_reg r v, Write_reg r' v' k) ->
     if r' = r && v' = v then Just k else Nothing
  | (E_mem_read_request req v, Mem_read_request req' k) ->
     if req' = req then Just (k v) else Nothing
  | (E_mem_write_request req r, Mem_write_request req' k) ->
     if req' = req then Just (k r) else Nothing
  | (E_mem_write_announce_address a, Mem_write_announce_address a' k) ->
     if a' = a then Just k else Nothing
  | (E_branch_announce_address addr, Branch_announce_address addr' k) ->
     if addr' = addr then Just k else Nothing
  | (E_barrier_request r, Barrier_request r' k) ->
     if r' = r then Just k else Nothing
  | (E_cache_op_request r, Cache_op_request r' k) ->
     if r' = r then Just k else Nothing
  | (E_tlb_op_request r, TLB_op_request r' k) ->
     if r' = r then Just k else Nothing
  | (E_fault_announce f, Fault_announce f' k) ->
     if f' = f then Just k else Nothing
  | (E_eret_announce pa, Eret_announce pa' k) ->
     if pa' = pa then Just k else Nothing
  (*| (E_barrier bk, Barrier bk' k) ->
     if bk' = bk then Just k else Nothing*)
  | _ -> Nothing
end

(*val runTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> maybe (monad 'regval 'a 'e)*)
let rec runTrace t m = match t with
  | [] -> Just m
  | e :: t' -> Maybe.bind (emitEvent m e) (runTrace t')
end

declare {isabelle} termination_argument runTrace = automatic

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

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

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

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

(* 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 base_monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'regstate 'a 'e =
  monad 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'e
type base_monadR 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'regstate 'a 'r 'e =
  monadR 'abort 'barrier 'cache_op 'fault 'pa 'tlb_op 'translation_summary 'arch_ak 'regval 'a 'r 'e