1 files changed, 65 insertions, 59 deletions
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 894d028f..a5f0653b 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -456,70 +456,76 @@ let ocaml_funcls ctx =
   function
   | [] -> failwith "Ocaml: empty function"
   | [FCL_aux (FCL_Funcl (id, pexp),_)] ->
-     let arg_typs, ret_typ =
-       match Bindings.find id ctx.val_specs with
-       | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ)
-       | _ -> failwith "Found val spec which was not a function!"
-     in
-     (* Any remaining type variables after simple_typ rewrite should
-        indicate Type-polymorphism. If we have it, we need to generate
-        explicit type signatures with universal quantification. *)
-     let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in
-     let pat_sym = gensym () in
-     let pat, exp =
-       match pexp with
-       | Pat_aux (Pat_exp (pat, exp),_) -> pat,exp
-       | Pat_aux (Pat_when (pat, wh, exp),_) -> failwith "OCaml: top-level pattern guards not supported"
-     in
-     let annot_pat =
-       let pat =
+     if Bindings.mem id ctx.externs
+     then string ("(* Omitting externed function " ^ string_of_id id ^ " *)") ^^ hardline
+     else
+       let arg_typs, ret_typ =
+         match Bindings.find id ctx.val_specs with
+         | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ)
+         | _ -> failwith "Found val spec which was not a function!"
+       in
+       (* Any remaining type variables after simple_typ rewrite should
+        ind   icate Type-polymorphism. If we have it, we need to generate
+        explic      it type signatures with universal quantification. *)
+       let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in
+       let pat_sym = gensym () in
+       let pat, exp =
+         match pexp with
+         | Pat_aux (Pat_exp (pat, exp),_) -> pat,exp
+         | Pat_aux (Pat_when (pat, wh, exp),_) -> failwith "OCaml: top-level pattern guards not supported"
+       in
+       let annot_pat =
+         let pat =
+           if KidSet.is_empty kids then
+             parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs)))
+           else
+             ocaml_pat ctx pat
+         in
+         if !opt_trace_ocaml
+         then parens (separate space [pat; string "as"; pat_sym])
+         else pat
+       in
+       let call_header = function_header () in
+       let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in
+       let call =
          if KidSet.is_empty kids then
-           parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs)))
+           separate space [call_header; zencode ctx id;
+                           annot_pat; colon; ocaml_typ ctx ret_typ; equals;
+                           sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
+           ^//^ ocaml_exp ctx exp
+           ^^ rparen
          else
-           ocaml_pat ctx pat
+           separate space [call_header; zencode ctx id; colon;
+                           separate space (List.map zencode_kid (KidSet.elements kids)) ^^ dot;
+                           ocaml_typ ctx (mk_typ (Typ_tup arg_typs)); string "->"; ocaml_typ ctx ret_typ; equals;
+                           string "fun"; annot_pat; string "->";
+                           sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
+           ^//^ ocaml_exp ctx exp
+           ^^ rparen
        in
-       if !opt_trace_ocaml
-       then parens (separate space [pat; string "as"; pat_sym])
-       else pat
-     in
-     let call_header = function_header () in
-     let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in
-     let call =
-       if KidSet.is_empty kids then
-         separate space [call_header; zencode ctx id;
-                         annot_pat; colon; ocaml_typ ctx ret_typ; equals;
-                         sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
-         ^//^ ocaml_exp ctx exp
-         ^^ rparen
-       else
-         separate space [call_header; zencode ctx id; colon;
-                         separate space (List.map zencode_kid (KidSet.elements kids)) ^^ dot;
-                         ocaml_typ ctx (mk_typ (Typ_tup arg_typs)); string "->"; ocaml_typ ctx ret_typ; equals;
-                         string "fun"; annot_pat; string "->";
-                         sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
-         ^//^ ocaml_exp ctx exp
-         ^^ rparen
-     in
-     ocaml_funcl call string_of_arg string_of_ret
+       ocaml_funcl call string_of_arg string_of_ret
   | funcls ->
      let id = funcls_id funcls in
-     let arg_typs, ret_typ =
-       match Bindings.find id ctx.val_specs with
-       | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ)
-       | _ -> failwith "Found val spec which was not a function!"
-     in
-     let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in
-     if not (KidSet.is_empty kids) then failwith "Cannot handle polymorphic multi-clause function in OCaml backend" else ();
-     let pat_sym = gensym () in
-     let call_header = function_header () in
-     let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in
-     let call =
-       separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs))); equals;
-                       sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
-       ^//^ (separate space [string "match"; pat_sym; string "with"] ^^ hardline ^^ ocaml_funcl_matches ctx funcls)
-       ^^ rparen
-     in
-     ocaml_funcl call string_of_arg string_of_ret
+     if Bindings.mem id ctx.externs
+     then string ("(* Omitting externed function " ^ string_of_id id ^ " *)") ^^ hardline
+     else
+       let arg_typs, ret_typ =
+         match Bindings.find id ctx.val_specs with
+         | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ)
+         | _ -> failwith "Found val spec which was not a function!"
+       in
+       let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in
+       if not (KidSet.is_empty kids) then failwith "Cannot handle polymorphic multi-clause function in OCaml backend" else ();
+       let pat_sym = gensym () in
+       let call_header = function_header () in
+       let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in
+       let call =
+         separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs))); equals;
+                         sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
+         ^//^ (separate space [string "match"; pat_sym; string "with"] ^^ hardline ^^ ocaml_funcl_matches ctx funcls)
+         ^^ rparen
+       in
+       ocaml_funcl call string_of_arg string_of_ret
 
 let ocaml_fundef ctx (FD_aux (FD_function (_, _, _, funcls), _)) =
   ocaml_funcls ctx funcls