From 423d32995427a289480fd5447d656754bcc58815 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Fri, 4 Jul 2014 13:08:38 +0100
Subject: Fix pretty printer for verbose printing

---
 src/pretty_print.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src')

diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index c70e18b7..2a24dc3e 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -875,6 +875,14 @@ let doc_exp, doc_let =
   | E_app_infix(l,op,r) ->
       failwith ("unexpected app_infix operator " ^ (pp_format_id op))
       (* doc_op (doc_id op) (exp l) (exp r) *)
+  | E_internal_exp (l, Base((_,t),_,_,_)) ->
+    (match t.t with
+      | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) ->
+	(match r.nexp with
+	  | Nconst bi -> utf8string (Big_int.string_of_big_int bi)
+          | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given vector without known length"))
+        | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given non-vector"))
+
   (* XXX missing case
      AAA internal_cast should never have an overload, if it's been seen it's a bug *)
   | E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false
-- 
cgit v1.2.3