lem_interp: remove broken val_to_string_internal functions, replace with string_of_value as used everywhere else

4 files changed, 11 insertions, 70 deletions

diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index a51598b3..9f1ea3e3 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -127,36 +127,6 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
   ;;
 
 
-let rec val_to_string_internal ((Interp.LMem (_,_,memory,_)) as mem) = function
- | Interp_ast.V_boxref(n, t) -> val_to_string_internal mem (Pmap.find n memory)
- | Interp_ast.V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l)
- | Interp_ast.V_tuple l ->
-     let repr = String.concat ", " (List.map (val_to_string_internal mem) l) in
-     sprintf "(%s)" repr
- | Interp_ast.V_list l ->
-     let repr = String.concat "; " (List.map (val_to_string_internal mem) l) in
-     sprintf "[||%s||]" repr
- | Interp_ast.V_vector (first_index, inc, l) ->
-     let last_index = (if (Interp_ast.IInc = inc) then List.length l - 1 else 1 - List.length l) + first_index  in
-     let repr =
-       try bitvec_to_string l
-       with Failure _ ->
-         sprintf "[%s]" (String.concat "; " (List.map (val_to_string_internal mem) l)) in
-     sprintf "%s [%s..%s]" repr (string_of_int first_index) (string_of_int last_index)
- | (Interp_ast.V_vector_sparse(first_index,last_index,inc,l,default) as v) -> 
-   val_to_string_internal mem (Interp_lib.fill_in_sparse v)
- | Interp_ast.V_record(_, l) ->
-     let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal mem value) in
-     let repr = String.concat "; " (List.map  pp l) in
-     sprintf "{%s}" repr
- | Interp_ast.V_ctor (id,_,_, value) ->
-     sprintf "%s %s" (id_to_string id) (val_to_string_internal mem value)
- | Interp_ast.V_register _ | Interp_ast.V_register_alias _ ->
-     sprintf "reg-as-value" 
- | Interp_ast.V_unknown -> "unknown"
- | Interp_ast.V_track(v,rs) -> (*"tainted by {" ^ (Interp_utilities.list_to_string Interp.string_of_reg_form "," rs) ^ "} --" ^ *) (val_to_string_internal mem v)
-;;
-
 (****************************************************************************
  * PPrint-based source-to-source pretty printer
 ****************************************************************************)
@@ -582,7 +552,7 @@ let doc_exp, doc_let =
   (* XXX missing case *)
   | E_comment _ | E_comment_struc _ -> string ""
   | E_internal_value v ->
-     string (val_to_string_internal mem v)
+     string (Interp.string_of_value v)
   | _-> failwith "internal expression escaped"
 
   and let_exp env mem add_red show_hole_contents (LB_aux(lb,_)) = match lb with
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 79a86113..a19256a2 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -49,7 +49,6 @@ open Interp_interface ;;
 
 open Nat_big_num ;;
 
-let val_to_string_internal = Pretty_interp.val_to_string_internal ;;
 let lit_to_string = Pretty_interp.lit_to_string ;;
 let id_to_string = Pretty_interp.id_to_string ;;
 let loc_to_string = Pretty_interp.loc_to_string ;;
@@ -451,7 +450,7 @@ let local_variables_to_string (IState(stack,_)) =
       String.concat ", " (option_map (fun (id,value)-> 
 	match id with
 	  | "0" -> None (*Let's not print out the context hole again*)
-	  | _ -> Some (id ^ "=" ^ val_to_string_internal mem value)) (Pmap.bindings_list env))
+	  | _ -> Some (id ^ "=" ^ Interp.string_of_value value)) (Pmap.bindings_list env))
 
 let instr_parm_to_string (name, typ, value) = 
   name ^"="^
diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli
index 85744d61..f1a0cd4a 100644
--- a/src/lem_interp/printing_functions.mli
+++ b/src/lem_interp/printing_functions.mli
@@ -10,7 +10,6 @@ val loc_to_string : l -> string
 val get_loc : tannot exp -> string
 (*interp_interface.value to string*)
 val reg_value_to_string : register_value -> string
-val val_to_string_internal : Interp.lmem -> Interp_ast.value -> string
 
 (*(*Force all representations to hex strings instead of a mixture of hex and binary strings*)
 val val_to_hex_string : value0 -> string*)
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 6f5ca07a..f61d9aaf 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -114,33 +114,6 @@ let rec reg_to_string = function
   | SubReg (id,r,_) -> sprintf "%s.%s" (reg_to_string r) (id_to_string id)
 ;;
 
-let rec val_to_string_internal = function
- | V_boxref(n, t) -> sprintf "boxref %d" n
- | V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l)
- | V_tuple l ->
-     let repr = String.concat ", " (List.map val_to_string_internal l) in
-     sprintf "(%s)" repr
- | V_list l ->
-     let repr = String.concat "; " (List.map val_to_string_internal l) in
-     sprintf "[||%s||]" repr
- | V_vector (first_index, inc, l) ->
-     let last_index = add_int_big_int (if inc then List.length l - 1 else 1 - List.length l) first_index  in
-     let repr =
-       try bitvec_to_string (* (if inc then l else List.rev l)*) l
-       with Failure _ ->
-         sprintf "[%s]" (String.concat "; " (List.map val_to_string_internal l)) in
-     sprintf "%s [%s..%s]" repr (string_of_big_int first_index) (string_of_big_int last_index)
- | V_record(_, l) ->
-     let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal value) in
-     let repr = String.concat "; " (List.map  pp l) in
-     sprintf "{%s}" repr
- | V_ctor (id,_, value) ->
-     sprintf "%s %s" (id_to_string id) (val_to_string_internal value)
- | V_register r ->
-     sprintf "reg-as-value %s" (reg_to_string r)
- | V_unknown -> "unknown"
-;;
-
 let rec top_frame_exp_state = function
   | Top -> raise (Invalid_argument "top_frame_exp")
   | Hole_frame(_, e, _, env, mem, Top) 
@@ -210,7 +183,7 @@ let id_compare i1 i2 =
 module Reg = struct
   include Map.Make(struct type t = id let compare = id_compare end)
   let to_string id v =
-    sprintf "%s -> %s" (id_to_string id) (val_to_string_internal v)
+    sprintf "%s -> %s" (id_to_string id) (string_of_value v)
   let find id m =
 (*    eprintf "reg_find called with %s\n" (id_to_string id);*)
     let v = find id m in
@@ -255,7 +228,7 @@ module Mem = struct
     v
   *)
   let to_string idx v =
-    sprintf "[%s] -> %s" (string_of_big_int idx) (val_to_string_internal v)
+    sprintf "[%s] -> %s" (string_of_big_int idx) (string_of_value v)
 end ;;
 
 
@@ -412,7 +385,7 @@ let run
   in
   let rec loop mode env = function
   | Value v ->
-      debugf "%s: %s %s\n" (grey name) (blue "return") (val_to_string_internal v);
+      debugf "%s: %s %s\n" (grey name) (blue "return") (string_of_value v);
       true, mode, env
   | Action (a, s) ->
       let (top_exp,(top_env,top_mem)) = top_frame_exp_state s in
@@ -429,25 +402,25 @@ let run
       let left = "<-" and right = "->" in
       let (mode',env',s) = begin match a with
       | Read_reg (reg, sub) ->
-          show "read_reg" (reg_to_string reg ^ sub_to_string sub) right (val_to_string_internal return);
+          show "read_reg" (reg_to_string reg ^ sub_to_string sub) right (string_of_value return);
           step (),env',s
       | Write_reg (reg, sub, value) ->
           assert (return = unit_lit);
-          show "write_reg" (reg_to_string reg ^ sub_to_string sub) left (val_to_string_internal value);
+          show "write_reg" (reg_to_string reg ^ sub_to_string sub) left (string_of_value value);
           step (),env',s
       | Read_mem (id, args, sub) ->
-          show "read_mem" (id_to_string id ^ val_to_string_internal args ^ sub_to_string sub) right (val_to_string_internal return);
+          show "read_mem" (id_to_string id ^ string_of_value args ^ sub_to_string sub) right (string_of_value return);
           step (),env',s
       | Write_mem (id, args, sub, value) ->
           assert (return = unit_lit);
-          show "write_mem" (id_to_string id ^ val_to_string_internal args ^ sub_to_string sub) left (val_to_string_internal value);
+          show "write_mem" (id_to_string id ^ string_of_value args ^ sub_to_string sub) left (string_of_value value);
           step (),env',s
       (* distinguish single argument for pretty-printing *)
       | Call_extern (f, (V_tuple _ as args)) ->
-          show "call_lib" (f ^ val_to_string_internal args) right (val_to_string_internal return);
+          show "call_lib" (f ^ string_of_value args) right (string_of_value return);
           step (),env',s
       | Call_extern (f, arg) ->
-          show "call_lib" (sprintf "%s(%s)" f (val_to_string_internal arg)) right (val_to_string_internal return);
+          show "call_lib" (sprintf "%s(%s)" f (string_of_value arg)) right (string_of_value return);
           step (),env',s
       | Interp.Step _ ->
           assert (return = unit_lit);