diff options
| author | Robert Norton | 2017-04-21 17:03:23 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-04-21 17:05:28 +0100 |
| commit | a5d8b2dc56594c1c4d1f88b1017638b5eef69086 (patch) | |
| tree | 55337a03b43ad3323d6aeda617fb217f1688de3a /src/pretty_print_ocaml.ml | |
| parent | e55f01ec8a3b3e94818d1701e28d1e9fa6343166 (diff) | |
define some big_int literals in sail_values.ml to avoid lots of calls to bit_int_of_int. Likely very little performance benefit but slightly more readable.
Diffstat (limited to 'src/pretty_print_ocaml.ml')
| -rw-r--r-- | src/pretty_print_ocaml.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml index fb6dd99f..c8c0bb86 100644 --- a/src/pretty_print_ocaml.ml +++ b/src/pretty_print_ocaml.ml @@ -127,7 +127,12 @@ let doc_lit_ocaml in_pat (L_aux(l,_)) = | L_one -> "Vone" | L_true -> "Vone" | L_false -> "Vzero" - | L_num i -> "(big_int_of_int (" ^ (string_of_int i) ^ "))" + | L_num i -> + let s = string_of_int i in + if (i >= 0) && (i <= 257) then + "bi" ^ s + else + "(big_int_of_int (" ^ s ^ "))" | L_hex n -> "(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*) | L_bin n -> "(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*) | L_undef -> "failwith \"undef literal not supported\"" (* XXX Undef vectors get handled with to_vec_undef. We could support undef bit but would need to check type. For the moment treat as runtime error. *) |