diff options
| author | Thomas Bauereiss | 2017-06-15 18:48:17 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-06-15 18:48:17 +0100 |
| commit | 5bba63ce09eeac29f335223ab7d925d7e82b4702 (patch) | |
| tree | eb54f77bb27116f074cd38bb4967e12371285da0 /src | |
| parent | 82cfbcb072ebbaa221095f8b4559b3177b71794a (diff) | |
Pretty-print bitvector types
Next up: Expressions, patterns
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_lem.ml | 10 |
1 files changed, 8 insertions, 2 deletions
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") |