Better separate riscv-independent and riscv-specific parts between prelude and riscv_types.

Also remove an unused break().

2 files changed, 17 insertions, 19 deletions

diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 44791217..59f1b23e 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -332,13 +332,6 @@ val print_int = "print_int" : (string, int) -> unit
 val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit
 val print_string = "print_string" : (string, string) -> unit
 
-union exception = {
-  Error_not_implemented : string,
-  Error_misaligned_access : unit,
-  Error_EBREAK : unit,
-  Error_internal_error : unit
-}
-
 val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 
@@ -385,8 +378,6 @@ function vector64 n = __raw_GetSlice_int(64, n, 0)
 val to_bits : forall 'l.(atom('l), int) -> bits('l)
 function to_bits (l, n) = __raw_GetSlice_int(l, n, 0)
 
-function break () : unit -> unit = ()
-
 val vector_update_subrange_dec = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o.
   (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
@@ -394,3 +385,13 @@ val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrang
   (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit)
 
 overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc}
+
+/* Ideally these would be sail builtin */
+
+function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) =
+    let v128 : bits(128) = EXTS(v) in
+    (v128 >> shift)[63..0]
+
+function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) =
+    let v64 : bits(64) = EXTS(v) in
+    (v64 >> shift)[31..0]
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index 8799f580..1c11a32f 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -1,3 +1,10 @@
+union exception = {
+  Error_not_implemented : string,
+  Error_misaligned_access : unit,
+  Error_EBREAK : unit,
+  Error_internal_error : unit
+}
+
 val not_implemented : forall ('a : Type). string -> 'a effect {escape}
 
 function not_implemented message = throw(Error_not_implemented(message))
@@ -163,13 +170,3 @@ enum ropw = {RISCV_ADDW, RISCV_SUBW, RISCV_SLLW, RISCV_SRLW, RISCV_SRAW} /* reg-
 enum amoop = {AMOSWAP, AMOADD, AMOXOR, AMOAND, AMOOR, AMOMIN, AMOMAX, AMOMINU, AMOMAXU} /* AMO ops */
 enum csrop = {CSRRW, CSRRS, CSRRC}
 enum word_width = {BYTE, HALF, WORD, DOUBLE}
-
-/* Ideally these would be sail builtin */
-
-function shift_right_arith64 (v : xlenbits, shift : bits(6)) -> xlenbits =
-    let v128 : bits(128) = EXTS(v) in
-    (v128 >> shift)[63..0]
-
-function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) =
-    let v64 : xlenbits = EXTS(v) in
-    (v64 >> shift)[31..0]