From 5bba63ce09eeac29f335223ab7d925d7e82b4702 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 15 Jun 2017 18:48:17 +0100
Subject: Pretty-print bitvector types

Next up: Expressions, patterns
---
 src/pretty_print_lem.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 9758b2de..65c679ff 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -160,8 +160,14 @@ let doc_typ_lem, doc_atomic_typ_lem =
          if atyp_needed then parens tpp else tpp
       | _ -> app_typ regtypes atyp_needed ty
     and app_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with
-      | Typ_app(Id_aux (Id "vector", _),[_;_;_;Typ_arg_aux (Typ_arg_typ typa, _)]) ->
-         let tpp = string "vector" ^^ space ^^ typ regtypes typa in
+      | Typ_app(Id_aux (Id "vector", _), [
+          Typ_arg_aux (Typ_arg_nexp n, _);
+          Typ_arg_aux (Typ_arg_nexp m, _);
+          Typ_arg_aux (Typ_arg_order ord, _);
+          Typ_arg_aux (Typ_arg_typ elem_typ, _)]) ->
+         let tpp = match elem_typ with
+           | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> string "bitvector" ^^ space ^^ doc_nexp m
+           | _ -> string "vector" ^^ space ^^ typ regtypes elem_typ in
          if atyp_needed then parens tpp else tpp
       | Typ_app(Id_aux (Id "range", _),_) ->
          (string "integer")
-- 
cgit v1.2.3