Fill in some of the basic coercions

3 files changed, 29 insertions, 38 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 1719e47c..f979b9d9 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -30,16 +30,6 @@ let bit_to_ibit = function
   | Bitc_one -> (Interp.V_lit (L_aux L_one Interp_ast.Unknown))
 end
 
-let to_bit = function 
-  | Bitl_zero -> Bitc_zero 
-  | Bitl_one ->  Bitc_one
-end
-
-let to_lbit = function
-  | Bitc_zero -> Bitl_zero
-  | Bitc_one -> Bitl_one
-end
-
 let to_bool = function 
   | Bitl_zero -> false
   | Bitl_one ->  true
@@ -77,19 +67,10 @@ end
 let all_known l = List.all is_bool l
 let all_known_bytes l = List.all (fun (Byte_lifted bs) -> List.all is_bool bs) l
 
-let bits_to_byte b = 
+let bits_to_word8 b = 
   if ((List.length b) = 8) && (all_known b)
   then natFromInteger (integerFromBoolList (false,(List.reverse (List.map to_bool b))))
-  else Assert_extra.failwith "bits_to_byte given a non-8 list or one containing ? and u"
-
-(*let memval_to_regval v start dir = 
-  <| rv_bits=(List.concatMap (fun (Byte_lifted(bits)) -> bits) v);
-     rv_start=start; rv_dir = dir |>
-
-let opcode_to_regval (Opcode v) start dir =
-  (memval_to_regval (List.map (fun (Byte(bits)) -> Byte_lifted (List.map to_lbit bits)) v) start dir)
-
-let regval_to_ifield v = List.map to_bit v.rv_bits*)
+  else Assert_extra.failwith "bits_to_word8 given a non-8 list or one containing ? and u"
 
 (*All but reg_value should take a mode to get direction and start correct*)
 let intern_opcode (Opcode v) =
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index c729c7f4..211917b9 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -382,17 +382,11 @@ val rr_interp_exhaustive : interp_mode -> instruction_state -> list event -> (ou
 
 (** operations and coercions on basic values *)
 
-(*val num_to_bits : nat -> v_kind -> integer -> value*)
+val word8_to_bitls : word8 -> list bit_lifted
+val bitls_to_word8 : list bit_lifted -> word8
 
-val byte_to_bits : word8 -> list bit_lifted
-val bits_to_byte : list bit_lifted -> word8
-
-(* TODO: rename these, as clash  with the functions below that take types according to their names:
-val integer_of_byte_list : list word8 -> integer
-
-
-val byte_list_of_integer : integer -> integer -> list word8 
-*)
+val integer_of_word8_list : list word8 -> integer
+val word8_list_of_integer : integer -> integer -> list word8 
 
 (* constructing values *)
 
@@ -447,17 +441,33 @@ let bit_lifted_of_bit b =
 val byte_lifted_of_byte : byte -> byte_lifted
 let byte_lifted_of_byte (Byte bs) : byte_lifted = Byte_lifted (List.map bit_lifted_of_bit bs)
 
+val bytes_of_bits : list bit -> list byte (*assumes (length bits) mod 8 = 0*)
+let rec bytes_of_bits bits = match bits with
+  | [] -> []
+  | b1::b2::b3::b4::b5::b6::b7::b8::bits -> 
+    (Byte [b1;b2;b3;b4;b5;b6;b7;b8])::(bytes_of_bits bits)
+end
 
-val integer_of_byte_list : list byte -> integer 
-(* TODO *)let integer_of_byte_list (a:list byte):integer = failwith "TODO"
-val byte_list_of_integer : int -> integer -> list byte 
-(* TODO *)let byte_list_of_integer (len:int) (a:integer):list byte = failwith "TODO"
+let bit_to_bool = function
+  | Bitc_zero -> false
+  | Bitc_one -> true
+end
 
 val integer_of_bit_list : list bit -> integer 
-(* TODO *)let integer_of_bit_list (a:list bit):integer = failwith "TODO"
 val bit_list_of_integer : int -> integer -> list bit 
-(* TODO *)let bit_list_of_integer (len:int) (a:integer):list bit = failwith "TODO"
+let integer_of_bit_list b =
+  integerFromBoolList (false,(List.reverse (List.map bit_to_bool b)))
+
+let bit_list_of_integer len b = 
+  List.map (fun b -> if b then Bitc_one else Bitc_zero) 
+    (boolListFrombitSeq (natFromInt len) (bitSeqFromInteger Nothing b))
 
+val integer_of_byte_list : list byte -> integer 
+let integer_of_byte_list bytes = integer_of_bit_list (List.concatMap (fun (Byte bs) -> bs) bytes)
+
+val byte_list_of_integer : int -> integer -> list byte 
+let byte_list_of_integer (len:int) (a:integer):list byte = 
+  let bits = bit_list_of_integer (len * 8) a in bytes_of_bits bits
 
 val integer_of_address : address -> integer 
 let integer_of_address (a:address):integer = 
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index de6b24d5..7fc247a7 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -50,7 +50,7 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
 let bytes_to_string bytes = 
   (String.concat ""
      (List.map (fun i -> let s = (Printf.sprintf "%x" i) in if (String.length s = 1) then "0"^s else s) 
-	(List.map (fun (Byte_lifted bs) -> bits_to_byte bs) bytes)))
+	(List.map (fun (Byte_lifted bs) -> bits_to_word8 bs) bytes)))
 
 let bit_lifted_to_string = function
   | Bitl_zero -> "0"