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, 2 insertions, 1 deletions

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index a870f454..710c9dac 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -411,7 +411,8 @@ let doc_spec (VS_aux(v,_)) = match v with
   | VS_val_spec(ts,id,ext_opt,is_cast) ->
      let cast_pp = if is_cast then [string "cast"] else [] in
      let extern_kwd_pp, id_pp = match ext_opt with
-       | Some ext -> [string "extern"], doc_op equals (doc_id id) (dquotes (string ext))
+       (* This sail syntax only supports a single extern name, so just use the ocaml version *)
+       | Some ext -> [string "extern"], doc_op equals (doc_id id) (dquotes (string (ext "ocaml")))
        | None -> [], doc_id id
      in
      separate space ([string "val"] @ cast_pp @ extern_kwd_pp @ [doc_typscm ts] @ [id_pp])