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.

11 files changed, 56 insertions, 28 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 2ccfee04..25b34402 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -921,7 +921,7 @@ let typschm_of_string order str =
   let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
   typschm
 
-let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, Some (string_of_id id), false))
+let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, Some (fun _ -> string_of_id id), false))
 
 let val_spec_ids (Defs defs) =
   let val_spec_id (VS_aux (vs_aux, _)) =
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index fada02a2..ea0662a3 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -331,7 +331,6 @@ let function_header () =
   then (first_function := false; string "let rec")
   else string "and"
 
-
 let funcls_id = function
   | [] -> failwith "Ocaml: empty function"
   | FCL_aux (FCL_Funcl (id, pat, exp),_) :: _ -> id
@@ -455,8 +454,6 @@ let ocaml_string_of_abbrev ctx id typq typ =
   separate space [string "let"; ocaml_string_of id; parens (arg ^^ space ^^ colon ^^ space ^^ zencode ctx id); equals]
   ^//^ ocaml_string_typ typ arg
 
-
-
 let ocaml_typedef ctx (TD_aux (td_aux, _)) =
   match td_aux with
   | TD_record (id, _, typq, fields, _) ->
@@ -483,7 +480,7 @@ let get_externs (Defs defs) =
   let extern_id (VS_aux (vs_aux, _)) =
     match vs_aux with
     | VS_val_spec (typschm, id, None, _) -> []
-    | VS_val_spec (typschm, id, Some ext, _) -> [(id, mk_id ext)]
+    | VS_val_spec (typschm, id, Some ext, _) -> [(id, mk_id (ext "ocaml"))]
   in
   let rec extern_ids = function
     | DEF_spec vs :: defs -> extern_id vs :: extern_ids defs
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index cfd749ba..fba0b1ec 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -423,7 +423,7 @@ type_def_aux =  (* Type definition body *)
 
 type 
 val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id * string option * bool
+   VS_val_spec of typschm * id * (string -> string) option * bool
 
 
 type 
diff --git a/src/parser.mly b/src/parser.mly
index 8c055b33..b204801f 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1057,21 +1057,21 @@ val_spec:
   | Val Cast typ id
     { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, None, true)) }
   | Val Extern typquant typ id
-    { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some (string_of_id $5), false)) }
+    { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some (fun _ -> string_of_id $5), false)) }
   | Val Extern typ id
-    { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, Some (string_of_id $4), false)) }
+    { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, Some (fun _ -> string_of_id $4), false)) }
   | Val Extern typquant typ id Eq String
-    { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some $7, false)) }
+    { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some (fun _ -> $7), false)) }
   | Val Extern typ id Eq String
-    { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, Some $6, false)) }
+    { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, Some (fun _ -> $6), false)) }
   | Val Cast Extern typquant typ id
-    { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, Some (string_of_id $6), true)) }
+    { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, Some (fun _ -> string_of_id $6), true)) }
   | Val Cast Extern typ id
-    { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4, $5, Some (string_of_id $5), true)) }
+    { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4, $5, Some (fun _ -> string_of_id $5), true)) }
   | Val Cast Extern typquant typ id Eq String
-    { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, Some $8, true)) }
+    { vloc (VS_val_spec (mk_typschm $4 $5 4 5,$6, Some (fun _ -> $8), true)) }
   | Val Cast Extern typ id Eq String
-    { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4,$5, Some $7, true)) }
+    { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $4 4 4,$5, Some (fun _ -> $7), true)) }
 
 kinded_id:
   | tyvar
diff --git a/src/parser2.mly b/src/parser2.mly
index 78724c4d..32b2a2b1 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -48,6 +48,18 @@ open Parse_ast
 
 let loc n m = Range (n, m)
 
+let default_opt x = function
+  | None -> x
+  | Some y -> y
+
+let assoc_opt key assocs =
+  try Some (List.assoc key assocs) with
+  | Not_found -> None
+
+let string_of_id = function
+  | Id_aux (Id str, _) -> str
+  | Id_aux (DeIid str, _) -> str
+
 let mk_id i n m = Id_aux (i, loc n m)
 let mk_kid str n m = Kid_aux (Var str, loc n m)
 
@@ -1033,19 +1045,29 @@ let_def:
   | Let_ letbind
     { $2 }
 
+externs:
+  | id Colon String
+    { [(string_of_id $1, $3)] }
+  | id Colon String Comma externs
+    { (string_of_id $1, $3) :: $5 }
+
 val_spec_def:
   | Val id Colon typschm
     { mk_vs (VS_val_spec ($4, $2, None, false)) $startpos $endpos }
   | Val Cast id Colon typschm
     { mk_vs (VS_val_spec ($5, $3, None, true)) $startpos $endpos }
   | Val id Eq String Colon typschm
-    { mk_vs (VS_val_spec ($6, $2, Some $4, false)) $startpos $endpos }
+    { mk_vs (VS_val_spec ($6, $2, Some (fun _ -> $4), false)) $startpos $endpos }
   | Val Cast id Eq String Colon typschm
-    { mk_vs (VS_val_spec ($7, $3, Some $5, true)) $startpos $endpos }
+    { mk_vs (VS_val_spec ($7, $3, Some (fun _ -> $5), true)) $startpos $endpos }
   | Val String Colon typschm
-    { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), Some $2, false)) $startpos $endpos }
+    { mk_vs (VS_val_spec ($4, mk_id (Id $2) $startpos($2) $endpos($2), Some (fun _ -> $2), false)) $startpos $endpos }
   | Val Cast String Colon typschm
-    { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), Some $3, true)) $startpos $endpos }
+    { mk_vs (VS_val_spec ($5, mk_id (Id $3) $startpos($3) $endpos($3), Some (fun _ -> $3), true)) $startpos $endpos }
+  | Val id Eq Lcurly externs Rcurly Colon typschm
+    { mk_vs (VS_val_spec ($8, $2, Some (fun backend -> default_opt (string_of_id $2) (assoc_opt backend $5)), false)) $startpos $endpos }
+  | Val Cast id Eq Lcurly externs Rcurly Colon typschm
+    { mk_vs (VS_val_spec ($9, $3, Some (fun backend -> default_opt (string_of_id $3) (assoc_opt backend $6)), true)) $startpos $endpos }
 
 register_def:
   | Register id Colon typ
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index b9ef1aec..0bb73aa5 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -739,7 +739,7 @@ let doc_exp_lem, doc_let_lem =
           | _ ->
              let call = match annot with
                | Some (env, _, _) when Env.is_extern f env ->
-                 string (Env.get_extern f env)
+                 string (Env.get_extern f env "lem")
                | _ -> doc_id_lem f in
              let argspp = match args with
                | [arg] -> expV true arg
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index fa387ad4..8031ba3e 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -533,7 +533,8 @@ let pp_lem_spec ppf (VS_aux(v,(l,annot))) =
   let print_spec ppf v =
     match v with
     | VS_val_spec(ts,id,ext_opt,is_cast) ->
-      fprintf ppf "@[<0>(%a %a %a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id (pp_option_lem quot_string) ext_opt pp_bool_lem is_cast
+       (* FIXME: None *)
+      fprintf ppf "@[<0>(%a %a %a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id (pp_option_lem quot_string) None pp_bool_lem is_cast
     | _ -> failwith "Invalid valspec"
   in
   fprintf ppf "@[<0>(VS_aux %a (%a, %a))@]" print_spec v pp_lem_l l pp_annot annot
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])
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
diff --git a/src/type_check.ml b/src/type_check.ml
index aede9c67..3dd251ca 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -375,8 +375,8 @@ module Env : sig
   val add_overloads : id -> id list -> t -> t
   val get_overloads : id -> t -> id list
   val is_extern : id -> t -> bool
-  val add_extern : id -> string -> t -> t
-  val get_extern : id -> t -> string
+  val add_extern : id -> (string -> string) -> t -> t
+  val get_extern : id -> t -> string -> string
   val get_default_order : t -> order
   val set_default_order_inc : t -> t
   val set_default_order_dec : t -> t
@@ -410,7 +410,7 @@ end = struct
       enums : IdSet.t Bindings.t;
       records : (typquant * (typ * id) list) Bindings.t;
       accessors : (typquant * typ) Bindings.t;
-      externs : string Bindings.t;
+      externs : (string -> string) Bindings.t;
       casts : id list;
       allow_casts : bool;
       constraints : n_constraint list;
@@ -934,13 +934,13 @@ let initial_env =
 
   (* Internal functions for Monomorphise.AtomToItself *)
 
-  |> Env.add_extern (mk_id "size_itself_int") "size_itself_int"
+  |> Env.add_extern (mk_id "size_itself_int") (fun _ -> "size_itself_int")
   |> Env.add_val_spec (mk_id "size_itself_int")
       (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
                                   Parse_ast.Unknown)],Parse_ast.Unknown),
        function_typ (app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))])
          (atom_typ (nvar (mk_kid "n"))) no_effect)
-  |> Env.add_extern (mk_id "make_the_value") "make_the_value"
+  |> Env.add_extern (mk_id "make_the_value") (fun _ -> "make_the_value")
   |> Env.add_val_spec (mk_id "make_the_value")
       (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
                                   Parse_ast.Unknown)],Parse_ast.Unknown),
diff --git a/src/type_check.mli b/src/type_check.mli
index f3e5e861..81cfd7fb 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -119,7 +119,7 @@ module Env : sig
 
   val is_extern : id -> t -> bool
 
-  val get_extern : id -> t -> string
+  val get_extern : id -> t -> string -> string
 
   (* Lookup id searchs for a specified id in the environment, and
      returns it's type and what kind of identifier it is, using the