From cd81acaf58db3edc4187e4cccc35f6aa76d6933d Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 24 Jan 2018 16:25:37 +0000
Subject: Fixed riscv ocaml compilation

---
 riscv/prelude.sail     |  5 ++++-
 riscv/riscv_types.sail | 12 ++++++------
 src/sail_lib.ml        |  2 ++
 3 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 6f37a6e3..6b58cd2b 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -139,7 +139,10 @@ val __SignExtendSlice = {lem: "exts_slice"} : forall 'm. (bits('m), int, int) ->
 
 val __ZeroExtendSlice = {lem: "extz_slice"} : forall 'm. (bits('m), int, int) -> bits('m)
 
-val cast "cast_unit_vec" : bit -> bits(1)
+val cast cast_unit_vec : bit -> bits(1)
+
+function cast_unit_vec bitzero = 0b0
+and cast_unit_vec bitone = 0b1
 
 val print = "prerr_endline" : string -> unit
 
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index e8f1c5bc..d338bab9 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -103,17 +103,17 @@ function mem_read (addr, width, aq, rl, res) = {
   }
 }
 
-val MEMea = {ocaml: "skip", lem: "MEMea"} : forall 'n.
+val MEMea = {ocaml: "memea", lem: "MEMea"} : forall 'n.
   (bits(64), atom('n)) -> unit effect {eamem}
-val MEMea_release = {ocaml: "skip", lem: "MEMea_release"} : forall 'n.
+val MEMea_release = {ocaml: "memea", lem: "MEMea_release"} : forall 'n.
   (bits(64), atom('n)) -> unit effect {eamem}
-val MEMea_strong_release = {ocaml: "skip", lem: "MEMea_strong_release"} : forall 'n.
+val MEMea_strong_release = {ocaml: "memea", lem: "MEMea_strong_release"} : forall 'n.
   (bits(64), atom('n)) -> unit effect {eamem}
-val MEMea_conditional = {ocaml: "skip", lem: "MEMea_conditional"} : forall 'n.
+val MEMea_conditional = {ocaml: "memea", lem: "MEMea_conditional"} : forall 'n.
   (bits(64), atom('n)) -> unit effect {eamem}
-val MEMea_conditional_release = {ocaml: "skip", lem: "MEMea_conditional_release"} : forall 'n.
+val MEMea_conditional_release = {ocaml: "memea", lem: "MEMea_conditional_release"} : forall 'n.
   (bits(64), atom('n)) -> unit effect {eamem}
-val MEMea_conditional_strong_release = {ocaml: "skip", lem: "MEMea_conditional_strong_release"} : forall 'n.
+val MEMea_conditional_strong_release = {ocaml: "memea", lem: "MEMea_conditional_strong_release"} : forall 'n.
   (bits(64), atom('n)) -> unit effect {eamem}
 
 val mem_write_ea : forall 'n. (bits(64), atom('n), bool, bool, bool) -> unit effect {eamem, escape}
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index c78b81a9..3cd8e18c 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -490,6 +490,8 @@ let rec string_of_list sep string_of = function
 
 let skip () = ()
 
+let memea (_, _) = ()
+
 let zero_extend (vec, n) =
   let m = Big_int.to_int n in
   if m <= List.length vec
-- 
cgit v1.2.3