lib/regfp.sail: new standard intrinsics for triggering memory effects

1 files changed, 20 insertions, 9 deletions

diff --git a/lib/regfp.sail b/lib/regfp.sail
index 731f1a8d..b2ecaa10 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -103,16 +103,27 @@ union instruction_kind = {
   IK_simple : unit
 }
 
-val __read_mem = { ocaml: "Platform.read_mem", _: "read_mem" } : forall 'n, 'n > 0. (read_kind, bits(64), int('n)) -> bits(8 * 'n) effect {rmem}
-val __write_ea = { ocaml: "Platform.write_ea", _: "write_ea" } : forall 'n, 'n > 0. (write_kind, bits(64), int('n)) -> unit effect {eamem}
-val __write_memv = { ocaml: "Platform.write_memv", _: "write_memv" } : forall 'n, 'n > 0. bits('n) -> bool effect {wmv}
-val __excl_res = { ocaml: "Platform.excl_res", _: "excl_res" }: unit -> bool effect {exmem}
-val __barrier = { ocaml: "Platform.barrier", _: "barrier" } : barrier_kind -> unit effect {barr}
+val __read_mem
+  = { ocaml: "Platform.read_mem", _: "read_mem" }
+  : forall 'n, 'n > 0. (read_kind, bits(64), int('n)) -> bits(8 * 'n) effect {rmem}
+val __write_mem_ea
+  = { ocaml: "Platform.write_mem_ea", _: "write_mem_ea" }
+  : forall 'n, 'n > 0. (write_kind, bits(64), int('n)) -> unit effect {eamem}
+val __write_mem
+  = { ocaml: "Platform.write_mem", _: "write_mem" }
+  : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {wmv}
+val __excl_res
+  = { ocaml: "Platform.excl_res", _: "excl_res" }
+  : unit -> bool effect {exmem}
+val __barrier
+  = { ocaml: "Platform.barrier", _: "barrier" }
+  : barrier_kind -> unit effect {barr}
 
-val __write_mem : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {eamem,wmv}
-function __write_mem (wk, addr, len, value) = {
-  __write_ea(wk, addr, len);
-  __write_memv(value)
+
+val __write : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {eamem,wmv}
+function __write (wk, addr, len, value) = {
+  __write_mem_ea(wk, addr, len);
+  __write_mem(wk, addr, len, value)
 }
 
 $endif