K,P debugging

2 files changed, 28 insertions, 0 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 049ca92d..06782451 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -4,6 +4,8 @@ import Instruction_extractor
 open import Interp_ast
 open import Interp_interface
 open import Pervasives
+open import Assert_extra
+
 
 val intern_value : value -> Interp.value
 val extern_value : interp_mode -> bool -> Interp.value -> (value * maybe (list reg_name))
@@ -130,6 +132,26 @@ let add_to_address value num =
 			(Interp.V_tuple [(intern_value value);Interp.V_lit (L_aux (L_num num) Interp_ast.Unknown)])))
 end
 
+
+let coerce_Bytevector_of_Bitvector (v: value) : value =
+  match v with
+  | Bitvector bs b i -> Bytevector (to_bytes bs)
+  | _ -> Assert_extra.failwith "coerce_Bytevector_of_Bitvector given non-Bitvector"
+  end
+
+let coerce_Bitvector_of_Bytevector (v: value) : value =
+  match v with
+  | Bytevector ws -> Bitvector 
+        (List.concatMap 
+           (fun w -> 
+             List.reverse 
+               (boolListFrombitSeq 8 (bitSeqFromNat w)))
+            ws)
+        true
+        0
+  | _ -> Assert_extra.failwith "coerce_Bitvector_of_Bitvector given non-Bytevector"
+  end
+
 let initial_instruction_state top_level main args = 
   let e_args = match args with
     | [] -> [E_aux (E_lit (L_aux L_unit Interp_ast.Unknown)) (Interp_ast.Unknown,Nothing)]
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index ed1b8875..4d3e4b35 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -141,6 +141,12 @@ val instruction_to_istate : context -> instruction -> i_state_or_error
 (* Augment an address by the given value *)
 val add_to_address : value -> nat -> value
 
+(* Coerce a Bitvector value (presumed a multiple of 8 bits long) to a Bytevector value *)
+val coerce_Bytevector_of_Bitvector : value -> value
+
+(* Coerce a Bytevector value to a Bitvector value, increasing and starting at zero *)
+val coerce_Bitvector_of_Bytevector : value -> value
+
 (* Slice a value into a smaller vector, starting at first number (wrt the indices of the bitvector value, not raw positions in its list of bits) and going to second (inclusive) according to order. 
    For bytevectors, assumes you are slicing at the byte level, not the bit level *)
 val slice_value : value -> nat -> nat -> value