Merge branch 'sail2' into mappings

(involved some manual tinkering with gitignore, type_check, riscv)

1 files changed, 16 insertions, 9 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 5c6dc593..0f384cab 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -45,12 +45,19 @@ let negate_real r = realNegate r
 let abs_real r = realAbs r
 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`
+
 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))
+let print_int msg i = print_endline (msg ^ (stringFromInteger i))
+
+val prerr_int : string -> integer -> unit
+let prerr_int msg i = prerr_endline (msg ^ (stringFromInteger i))
 
 val putchar : integer -> unit
 let putchar _ = ()
@@ -85,7 +92,7 @@ let rec replace bs (n : integer) b' = match bs with
      if n = 0 then b' :: bs
               else b :: replace bs (n - 1) b'
   end
-declare {isabelle} termination_argument replace = automatic
+declare {isabelle; hol} termination_argument replace = automatic
 
 let upper n = n
 
@@ -128,7 +135,7 @@ let rec just_list l = match l with
       | (_, _) -> Nothing
     end
   end
-declare {isabelle} termination_argument just_list = automatic
+declare {isabelle; hol} termination_argument just_list = automatic
 
 lemma just_list_spec:
   ((forall xs. (just_list xs = Nothing) <-> List.elem Nothing xs) &&
@@ -267,7 +274,7 @@ let rec nat_of_bools_aux acc bs = match bs with
   | true :: bs -> nat_of_bools_aux ((2 * acc) + 1) bs
   | false :: bs -> nat_of_bools_aux (2 * acc) bs
 end
-declare {isabelle} termination_argument nat_of_bools_aux = automatic
+declare {isabelle; hol} termination_argument nat_of_bools_aux = automatic
 let nat_of_bools bs = nat_of_bools_aux 0 bs
 
 val unsigned_of_bools : list bool -> integer
@@ -306,7 +313,7 @@ let rec add_one_bool_ignore_overflow_aux bits = match bits with
   | false :: bits -> true :: bits
   | true :: bits -> false :: add_one_bool_ignore_overflow_aux bits
 end
-declare {isabelle} termination_argument add_one_bool_ignore_overflow_aux = automatic
+declare {isabelle; hol} termination_argument add_one_bool_ignore_overflow_aux = automatic
 
 let add_one_bool_ignore_overflow bits =
   List.reverse (add_one_bool_ignore_overflow_aux (List.reverse bits))
@@ -369,7 +376,7 @@ let rec add_one_bit_ignore_overflow_aux bits = match bits with
   | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
   | BU :: bits -> BU :: List.map (fun _ -> BU) bits
 end
-declare {isabelle} termination_argument add_one_bit_ignore_overflow_aux = automatic
+declare {isabelle; hol} termination_argument add_one_bit_ignore_overflow_aux = automatic
 
 let add_one_bit_ignore_overflow bits =
   List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
@@ -417,7 +424,7 @@ let rec hexstring_of_bits bs = match bs with
   | [] -> Just []
   | _ -> Nothing
   end
-declare {isabelle} termination_argument hexstring_of_bits = automatic
+declare {isabelle; hol} termination_argument hexstring_of_bits = automatic
 
 let show_bitlist bs =
   match hexstring_of_bits bs with
@@ -630,7 +637,7 @@ let rec byte_chunks bs = match bs with
      Maybe.bind (byte_chunks rest) (fun rest -> Just ([a;b;c;d;e;f;g;h] :: rest))
   | _ -> Nothing
 end
-declare {isabelle} termination_argument byte_chunks = automatic
+declare {isabelle; hol} termination_argument byte_chunks = automatic
 
 val bytes_of_bits : forall 'a. Bitvector 'a => 'a -> maybe (list memory_byte)
 let bytes_of_bits bs = byte_chunks (bits_of bs)
@@ -854,7 +861,7 @@ let rec foreach l vars body =
     | (x :: xs) -> foreach xs (body x vars) body
   end
 
-declare {isabelle} termination_argument foreach = automatic
+declare {isabelle; hol} termination_argument foreach = automatic
 
 val index_list : integer -> integer -> integer -> list integer
 let rec index_list from to step =