Declare prelude functions as extern

Also, rename a few functions for uniformity, e.g. bool_and -> and_bool

4 files changed, 73 insertions, 77 deletions

diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 524d7ef6..826ea98f 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -39,6 +39,7 @@ let cast_vec_bool v = bitU_to_bool (extract_only_element v)
 let cast_bit_vec_basic (start, len, b) = Vector (repeat [b] len) start false
 let cast_boolvec_bitvec (Vector bs start inc) =
   Vector (List.map bool_to_bitU bs) start inc
+let cast_vec_bl (Vector bs start inc) = bs
 
 let pp_bitu_vector (Vector elems start inc) =
   let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
@@ -50,8 +51,6 @@ let most_significant = function
   | _ -> failwith "most_significant applied to empty vector"
   end
 
-let bitwise_not_bitlist = List.map bitwise_not_bit
-
 let bitwise_not (Vector bs start is_inc) =
   Vector (bitwise_not_bitlist bs) start is_inc
 
@@ -63,18 +62,6 @@ let bitwise_and = bitwise_binop (&&)
 let bitwise_or = bitwise_binop (||)
 let bitwise_xor = bitwise_binop xor
 
-(*let unsigned (Vector bs _ _) : integer =
-  let (sum,_) =
-    List.foldr
-      (fun b (acc,exp) ->
-        match b with
-        | B1 -> (acc + integerPow 2 exp,exp + 1)
-        | B0 -> (acc, exp + 1)
-        | BU -> failwith "unsigned: vector has undefined bits"
-        end)
-      (0,0) bs in
-  sum*)
-
 let unsigned_big = unsigned
 
 let signed v : integer =
@@ -136,40 +123,9 @@ let get_min_representable_in _ (n : integer) : integer =
   else if n = 5 then min_5
   else 0 - (integerPow 2 (natFromInteger n))
 
-val to_bin_aux : natural -> list bitU
-let rec to_bin_aux x =
-  if x = 0 then []
-  else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
-let to_bin n = List.reverse (to_bin_aux n)
-
-val pad_zero : list bitU -> integer -> list bitU
-let rec pad_zero bits n =
-  if n <= 0 then bits else pad_zero (B0 :: bits) (n -1)
-
-
-let rec add_one_bit_ignore_overflow_aux bits = match bits with
-  | [] -> []
-  | B0 :: bits -> B1 :: bits
-  | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
-  | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
-end
-
-let add_one_bit_ignore_overflow bits =
-  List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
-  
-
 let to_norm_vec is_inc ((len : integer),(n : integer)) =
   let start = if is_inc then 0 else len - 1 in
-  let bits = to_bin (naturalFromInteger (abs n)) in
-  let len_bits = integerFromNat (List.length bits) in
-  let longer = len - len_bits in
-  let bits' =
-    if longer < 0 then drop (natFromInteger (abs (longer))) bits
-    else pad_zero bits longer in
-  if n > (0 : integer)
-  then Vector bits' start is_inc
-  else Vector (add_one_bit_ignore_overflow (bitwise_not_bitlist bits'))
-              start is_inc
+  Vector (bits_of_int (len, n)) start is_inc
 
 let to_vec_big = to_norm_vec
 
@@ -451,7 +407,6 @@ let gt = compare_op (>)
 let lteq = compare_op (<=)
 let gteq = compare_op (>=)
 
-
 let compare_op_vec op sign (l,r) =
   let (l',r') = (to_num sign l, to_num sign r) in
   compare_op op (l',r')
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 8fb55137..74d0acf7 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -65,7 +65,7 @@ let bvslice_raw bs i j =
 val bvupdate_aux : forall 'a 'b. Size 'a => bool -> integer -> bitvector 'a -> integer -> integer -> list bitU -> bitvector 'a
 let bvupdate_aux is_inc start bs i j bs' =
   let bits = update_aux is_inc start (List.map to_bitU (bitlistFromWord bs)) i j bs' in
-  wordFromBitlist (List.map from_bitU bits)
+  wordFromBitlist (List.map of_bitU bits)
   (*let iN = natFromInteger i in
   let jN = natFromInteger j in
   let startN = natFromInteger start in
@@ -110,6 +110,7 @@ let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
 let cast_bit_vec_basic (start, len, b) = vec_to_bvec (Vector [b] start false)
 let cast_boolvec_bitvec (Vector bs start inc) =
   vec_to_bvec (Vector (List.map bool_to_bitU bs) start inc)
+let cast_vec_bl v = List.map bool_to_bitU (bitlistFromWord v)
 
 let pp_bitu_vector (Vector elems start inc) =
   let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 45b73ab5..96886199 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -33,11 +33,14 @@ let negate_real r = realNegate r
 let abs_real r = realAbs r
 let power_real (b, e) = realPowInteger b e
 
-let bool_or (l, r) = (l || r)
-let bool_and (l, r) = (l && r)
-let bool_xor (l, r) = xor l r
+let or_bool (l, r) = (l || r)
+let and_bool (l, r) = (l && r)
+let xor_bool (l, r) = xor l r
 
 let list_append (l, r) = l ++ r
+let list_length xs = integerFromNat (List.length xs)
+let list_take (n, xs) = List.take (natFromInteger n) xs
+let list_drop (n, xs) = List.drop (natFromInteger n) xs
 
 val repeat : forall 'a. list 'a -> integer -> list 'a
 let rec repeat xs n =
@@ -70,12 +73,12 @@ end
 
 class (BitU 'a)
   val to_bitU : 'a -> bitU
-  val from_bitU : bitU -> 'a
+  val of_bitU : bitU -> 'a
 end
 
 instance (BitU bitU)
   let to_bitU b = b
-  let from_bitU b = b
+  let of_bitU b = b
 end
 
 let bitU_to_bool = function
@@ -88,7 +91,7 @@ let bool_to_bitU b = if b then B1 else B0
 
 instance (BitU bool)
   let to_bitU = bool_to_bitU
-  let from_bitU = bitU_to_bool
+  let of_bitU = bitU_to_bool
 end
 
 let cast_bit_bool = bitU_to_bool
@@ -153,6 +156,56 @@ let inline (|.) x y = bitwise_or_bit (x,y)
 val (+.) : bitU -> bitU -> bitU
 let inline (+.) x y = bitwise_xor_bit (x,y)
 
+val to_bin_aux : natural -> list bitU
+let rec to_bin_aux x =
+  if x = 0 then []
+  else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2)
+let to_bin n = List.reverse (to_bin_aux n)
+
+val of_bin : list bitU -> natural
+let of_bin bits =
+  let (sum,_) =
+    List.foldr
+      (fun b (acc,exp) ->
+        match b with
+        | B1 -> (acc + naturalPow 2 exp, exp + 1)
+        | B0 -> (acc, exp + 1)
+        | BU -> failwith "of_bin: bitvector has undefined bits"
+        end)
+      (0,0) bits in
+  sum
+
+val bitlist_to_integer : list bitU -> integer
+let bitlist_to_integer bs = integerFromNatural (of_bin bs)
+
+val pad_zero : list bitU -> integer -> list bitU
+let rec pad_zero bits n =
+  if n <= 0 then bits else pad_zero (B0 :: bits) (n -1)
+
+let bitwise_not_bitlist = List.map bitwise_not_bit
+
+let rec add_one_bit_ignore_overflow_aux bits = match bits with
+  | [] -> []
+  | B0 :: bits -> B1 :: bits
+  | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits
+  | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit"
+end
+
+let add_one_bit_ignore_overflow bits =
+  List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
+
+let bits_of_nat ((len : integer),(n : natural)) =
+  let bits = to_bin n in
+  let len_bits = integerFromNat (List.length bits) in
+  let longer = len - len_bits in
+  if longer < 0 then drop (natFromInteger (abs (longer))) bits
+  else pad_zero bits longer
+
+let bits_of_int ((len : integer),(n : integer)) =
+  let bits = bits_of_nat (len, naturalFromInteger (abs n)) in
+  if n > (0 : integer)
+  then bits
+  else (add_one_bit_ignore_overflow (bitwise_not_bitlist bits))
 
 
 (*** Vectors *)
@@ -292,47 +345,34 @@ class (Bitvector 'a)
   val set_bits : bool -> integer -> 'a -> integer -> integer -> list bitU -> 'a
 end
 
-val bitlist_to_integer : list bitU -> integer
-let bitlist_to_integer bs =
-  let (sum,_) =
-    List.foldr
-      (fun b (acc,exp) ->
-        match b with
-        | B1 -> (acc + integerPow 2 exp,exp + 1)
-        | B0 -> (acc, exp + 1)
-        | BU -> failwith "unsigned: vector has undefined bits"
-        end)
-      (0,0) bs in
-  sum
-
 instance forall 'a. BitU 'a => (Bitvector (list 'a))
   let bits_of v = List.map to_bitU v
-  let of_bits v = List.map from_bitU v
+  let of_bits v = List.map of_bitU v
   let unsigned v = bitlist_to_integer (List.map to_bitU v)
   let get_bit is_inc start v n = to_bitU (access_aux is_inc start v n)
-  let set_bit is_inc start v n b = update_aux is_inc start v n n [from_bitU b]
+  let set_bit is_inc start v n b = update_aux is_inc start v n n [of_bitU b]
   let get_bits is_inc start v i j = List.map to_bitU (slice_aux is_inc start v i j)
-  let set_bits is_inc start v i j v' = update_aux is_inc start v i j (List.map from_bitU v')
+  let set_bits is_inc start v i j v' = update_aux is_inc start v i j (List.map of_bitU v')
 end
 
 instance forall 'a. BitU 'a => (Bitvector (vector 'a))
   let bits_of v = List.map to_bitU (get_elems v)
-  let of_bits v = Vector (List.map from_bitU v) (integerFromNat (List.length v) - 1) false
+  let of_bits v = Vector (List.map of_bitU v) (integerFromNat (List.length v) - 1) false
   let unsigned v = unsigned (get_elems v)
   let get_bit is_inc start v n = to_bitU (access v n)
-  let set_bit is_inc start v n b = update_pos v n (from_bitU b)
+  let set_bit is_inc start v n b = update_pos v n (of_bitU b)
   let get_bits is_inc start v i j = List.map to_bitU (get_elems (slice v i j))
-  let set_bits is_inc start v i j v' = update v i j (Vector (List.map from_bitU v') (integerFromNat (List.length v') - 1) false)
+  let set_bits is_inc start v i j v' = update v i j (Vector (List.map of_bitU v') (integerFromNat (List.length v') - 1) false)
 end
 
 instance forall 'a. Size 'a => (Bitvector (mword 'a))
   let bits_of v = List.map to_bitU (bitlistFromWord v)
-  let of_bits v = wordFromBitlist (List.map from_bitU v)
+  let of_bits v = wordFromBitlist (List.map of_bitU v)
   let unsigned v = unsignedIntegerFromWord v
   let get_bit is_inc start v n = to_bitU (access_aux is_inc start (bitlistFromWord v) n)
-  let set_bit is_inc start v n b = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) n n [from_bitU b])
+  let set_bit is_inc start v n b = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) n n [of_bitU b])
   let get_bits is_inc start v i j = slice_aux is_inc start (List.map to_bitU (bitlistFromWord v)) i j
-  let set_bits is_inc start v i j v' = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) i j (List.map from_bitU v'))
+  let set_bits is_inc start v i j v' = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) i j (List.map of_bitU v'))
 end
 
 (*let showBitvector (Bitvector elems start inc) =
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 3cf017d1..e7bd6913 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1859,7 +1859,7 @@ let rewrite_guarded_clauses l cs =
 
 let bitwise_and_exp exp1 exp2 =
   let (E_aux (_,(l,_))) = exp1 in
-  let andid = Id_aux (Id "bool_and", gen_loc l) in
+  let andid = Id_aux (Id "and_bool", gen_loc l) in
   annot_exp (E_app(andid,[exp1;exp2])) l (env_of exp1) bool_typ
 
 let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with