Allow functions to be selectively declared external only for some backends

For example,

val test = { ocaml: "test_ocaml" } : unit -> unit

will only be external for OCaml. For other backends, it will have to be
defined.

1 files changed, 7 insertions, 2 deletions

diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index edea1016..ce64d1b4 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -328,7 +328,12 @@ let doc_typdef (TD_aux(td,_)) = match td with
   | _ -> string "TYPEDEF"
 
 let doc_spec (VS_aux(v,_)) =
-  let doc_extern = function
+  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
+    if docs = [] then empty else braces (separate (comma ^^ space) docs)
+    (* function
     | Some s ->
        let ext_for backend = utf8string ("\"" ^ String.escaped (s backend) ^  "\"") in
        let extern =
@@ -337,7 +342,7 @@ let doc_spec (VS_aux(v,_)) =
          else separate space [lbrace; string "ocaml:"; ext_for "ocaml"; string "lem:"; ext_for "lem"; rbrace]
        in
        equals ^^ space ^^ extern ^^ space
-    | None -> empty
+    | None -> empty *)
   in
   match v with
   | VS_val_spec(ts,id,ext,is_cast) ->