diff options
| author | Alasdair Armstrong | 2018-01-22 21:44:17 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-01-22 21:44:17 +0000 |
| commit | 4cafba567b6610b239ab6b82b89073a1a8a49632 (patch) | |
| tree | bbf1ffe9ca3da4c0efc3b440fcecb6b69176e127 /src/pretty_print_sail.ml | |
| parent | 6eee8747074539f77881cea90ce848cd8f4de1a5 (diff) | |
Added rewriter that specializes all function calls in a specification.
This removes all type polymorphism, so we can generate optimized
bitvector code and compile to languages without parametric
polymorphism.
Diffstat (limited to 'src/pretty_print_sail.ml')
| -rw-r--r-- | src/pretty_print_sail.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 43be7a00..b55448fa 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -477,11 +477,12 @@ let doc_typdef (TD_aux(td,_)) = match td with surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace] | _ -> string "TYPEDEF" + let doc_spec (VS_aux(v,_)) = let doc_extern ext = let doc_backend b = Util.option_map (fun id -> string (b ^ ":") ^^ space ^^ utf8string ("\"" ^ String.escaped id ^ "\"")) (ext b) in - let docs = Util.option_these (List.map doc_backend ["ocaml"; "lem"]) in + let docs = Util.option_these (List.map doc_backend ["ocaml"; "lem"; "smt"; "interpreter"]) in if docs = [] then empty else equals ^^ space ^^ braces (separate (comma ^^ space) docs) in match v with |