Allow for different extern names for different backends

For example:

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

val main : unit -> unit

function main () = {
  test ();
}

for a backend not explicitly provided, the extern name would be simply
"test" in this case, i.e. the string version of the id.

Also fixed some bugs in the ocaml backend.

1 files changed, 8 insertions, 1 deletions

diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index efcfc8b9..edea1016 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -329,7 +329,14 @@ let doc_typdef (TD_aux(td,_)) = match td with
 
 let doc_spec (VS_aux(v,_)) =
   let doc_extern = function
-    | Some s -> equals ^^ space ^^ utf8string ("\"" ^ String.escaped s ^ "\"") ^^ space
+    | Some s ->
+       let ext_for backend = utf8string ("\"" ^ String.escaped (s backend) ^  "\"") in
+       let extern =
+         if s "ocaml" = s "lem"
+         then ext_for "ocaml"
+         else separate space [lbrace; string "ocaml:"; ext_for "ocaml"; string "lem:"; ext_for "lem"; rbrace]
+       in
+       equals ^^ space ^^ extern ^^ space
     | None -> empty
   in
   match v with