From 15f965c9e4bd39eb7fe97552b9ac9db51a3cdbfb Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 18 Apr 2018 15:32:39 +0100
Subject: Move a few printing functions to sail_values.lem

They are used in various specs and test cases.
---
 aarch64/aarch64_extras.lem      | 11 -----------
 aarch64/mono/aarch64_extras.lem | 11 -----------
 mips/mips_extras.lem            | 11 -----------
 riscv/riscv_extras.lem          | 11 -----------
 src/gen_lib/sail_values.lem     | 11 +++++++++++
 5 files changed, 11 insertions(+), 44 deletions(-)

diff --git a/aarch64/aarch64_extras.lem b/aarch64/aarch64_extras.lem
index c9ea84e2..1994b4f8 100644
--- a/aarch64/aarch64_extras.lem
+++ b/aarch64/aarch64_extras.lem
@@ -15,17 +15,6 @@ type ty2048
 instance (Size ty2048) let size = 2048 end
 declare isabelle target_rep type ty2048 = `2048`
 
-val prerr_endline : string -> unit
-let prerr_endline _ = ()
-declare ocaml target_rep function prerr_endline = `prerr_endline`
-
-val print_int : string -> integer -> unit
-let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
-
-val putchar : integer -> unit
-let putchar _ = ()
-declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
-
 val slice : list bitU -> integer -> integer -> list bitU
 let slice v lo len =
   subrange_vec_dec v (lo + len - 1) lo
diff --git a/aarch64/mono/aarch64_extras.lem b/aarch64/mono/aarch64_extras.lem
index d2c95b64..3e9ee225 100644
--- a/aarch64/mono/aarch64_extras.lem
+++ b/aarch64/mono/aarch64_extras.lem
@@ -15,17 +15,6 @@ type ty2048
 instance (Size ty2048) let size = 2048 end
 declare isabelle target_rep type ty2048 = `2048`
 
-val prerr_endline : string -> unit
-let prerr_endline _ = ()
-declare ocaml target_rep function prerr_endline = `prerr_endline`
-
-val print_int : string -> integer -> unit
-let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
-
-val putchar : integer -> unit
-let putchar _ = ()
-declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
-
 val slice : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
 let slice v lo len =
   subrange_vec_dec v (lo + len - 1) lo
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index d4c79d7a..28fa07fb 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -80,17 +80,6 @@ let read_ram _ size _ addr = MEMr addr size
 let string_of_bits bs = string_of_bv (bits_of bs)
 let string_of_int = show
 
-val prerr_endline : string -> unit
-let prerr_endline _ = ()
-declare ocaml target_rep function prerr_endline = `prerr_endline`
-
-val print_int : string -> integer -> unit
-let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
-
-val putchar : integer -> unit
-let putchar _ = ()
-declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
-
 let _sign_extend bits len = maybe_failwith (of_bits (exts_bv len bits))
 let _zero_extend bits len = maybe_failwith (of_bits (extz_bv len bits))
 
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index 9d9ccf89..fb4f7f31 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -61,19 +61,8 @@ let shift_bits_right v m = shiftr v (uint m)
 val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
 let shift_bits_left v m = shiftl v (uint m)
 
-val prerr_endline : string -> unit
-let prerr_endline _ = ()
-declare ocaml target_rep function prerr_endline = `prerr_endline`
-
 val print_string : string -> string -> unit
 let print_string msg s = prerr_endline (msg ^ s)
 
-val print_int : string -> integer -> unit
-let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
-
 val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
 let print_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))
-
-val putchar : integer -> unit
-let putchar _ = ()
-declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index cb2c3379..819c11c5 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -45,6 +45,17 @@ let negate_real r = realNegate r
 let abs_real r = realAbs r
 let power_real b e = realPowInteger b e*)
 
+val prerr_endline : string -> unit
+let prerr_endline _ = ()
+declare ocaml target_rep function prerr_endline = `prerr_endline`
+
+val print_int : string -> integer -> unit
+let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
+
+val putchar : integer -> unit
+let putchar _ = ()
+declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
+
 val shr_int : ii -> ii -> ii
 let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
 
-- 
cgit v1.2.3