From a92a6573ea2d7cf88c1c7ac8dcc79a241aea0df7 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 4 Feb 2019 20:06:49 +0000
Subject: Test lem output by running end-to-end tests using ocaml via lem

---
 src/gen_lib/sail2_values.lem | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index fa1e8426..f21a4772 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -47,7 +47,11 @@ let power_real b e = realPowInteger b e*)
 
 val print_endline : string -> unit
 let print_endline _ = ()
-(* declare ocaml target_rep function print_endline = `print_endline` *)
+declare ocaml target_rep function print_endline = `print_endline`
+
+val print : string -> unit
+let print _ = ()
+declare ocaml target_rep function print = `print_string`
 
 val prerr_endline : string -> unit
 let prerr_endline _ = ()
@@ -631,6 +635,12 @@ let nat_of_bv v = Maybe.map nat_of_int (unsigned v)
 val string_of_bv : forall 'a. Bitvector 'a => 'a -> string
 let string_of_bv v = show_bitlist (bits_of v)
 
+val print_bits : forall 'a. Bitvector 'a => string -> 'a -> unit
+let print_bits str v = print_endline (str ^ string_of_bv v)
+
+val concat_str : string -> string -> string
+let concat_str str1 str2 = str1 ^ str2
+
 val int_of_bit : bitU -> integer
 let int_of_bit b =
   match b with
-- 
cgit v1.2.3