From 7015d7f48b124c3329a3638b8d433d522b447b40 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 30 Aug 2017 15:16:44 +0100
Subject: Ocaml backend can now run ocamlbuild automatically to build ocaml
 files into runable executable.

---
 src/initial_check.mli |  2 ++
 src/ocaml_backend.ml  | 33 +++++++++++++++++++++++++++++----
 src/sail.ml           | 12 ++++--------
 3 files changed, 35 insertions(+), 12 deletions(-)

(limited to 'src')

diff --git a/src/initial_check.mli b/src/initial_check.mli
index ed4eb0bf..86b5ca3b 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -41,6 +41,8 @@
 (**************************************************************************)
 
 open Ast
+open Ast_util
 
 val process_ast : order -> Parse_ast.defs -> unit defs
 
+val val_spec_ids : 'a defs -> IdSet.t
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 60622aba..e73d98c1 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -234,6 +234,7 @@ let ocaml_typedef ctx (TD_aux (td_aux, _)) =
      ^//^ ocaml_enum ctx ids
   | TD_abbrev (id, _, TypSchm_aux (TypSchm_ts (typq, typ), _)) ->
      separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals; ocaml_typ ctx typ]
+  | _ -> failwith "Unsupported typedef"
 
 let get_externs (Defs defs) =
   let extern_id (VS_aux (vs_aux, _)) =
@@ -274,12 +275,36 @@ let ocaml_defs (Defs defs) =
   ^^ concat (List.map (ocaml_def ctx) defs)
   ^^ empty_reg_init
 
-let ocaml_main ctx spec =
-  concat [separate space [string "open"; string spec] ^^ ocaml_def_end;
+let ocaml_main spec =
+  concat [separate space [string "open"; string (String.capitalize spec)] ^^ ocaml_def_end;
           separate space [string "let"; string "()"; equals]
-          ^//^ (zencode ctx (mk_id "initialize_registers") ^^ string "()" ^^ semi
-                ^/^ zencode ctx (mk_id "main") ^^ string "()")
+          ^//^ (string "initialize_registers" ^^ string "()" ^^ semi
+                ^/^ string "zmain" ^^ string "()")
          ]
 
 let ocaml_pp_defs f defs =
   ToChannel.pretty 1. 80 f (ocaml_defs defs)
+
+let ocaml_compile spec defs =
+  let sail_lib_dir =
+    try Sys.getenv "SAILLIBDIR" with
+    | Not_found -> failwith "Environment variable SAILLIBDIR needs to be set"
+  in
+  if Sys.file_exists "_sbuild" then () else Unix.mkdir "_sbuild" 0o775;
+  let cwd = Unix.getcwd () in
+  Unix.chdir "_sbuild";
+  let _ = Unix.system ("cp " ^ sail_lib_dir ^ "/sail_lib.ml .") in
+  let out_chan = open_out (spec ^ ".ml") in
+  ocaml_pp_defs out_chan defs;
+  close_out out_chan;
+  if IdSet.mem (mk_id "main") (Initial_check.val_spec_ids defs)
+  then
+    let out_chan = open_out "main.ml" in
+    ToChannel.pretty 1. 80 out_chan (ocaml_main spec);
+    close_out out_chan;
+    let _ = Unix.system "ocamlbuild main.native" in
+    let _ = Unix.system ("cp main.native " ^ cwd ^ "/" ^ spec) in
+    ()
+  else ();
+  Unix.chdir cwd
+
diff --git a/src/sail.ml b/src/sail.ml
index 0f84db9f..5e979738 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -157,14 +157,10 @@ let main() =
        then output "" Lem_ast_out [out_name,ast]
        else ());
       (if !(opt_print_ocaml)
-       then let ast_ocaml = rewrite_ast_ocaml ast in
-            (* Pretty_print_sail.pp_defs stdout ast_ocaml; *)
-          Ocaml_backend.ocaml_pp_defs stdout ast_ocaml;
-            (*
-         if !(opt_libs_ocaml) = []
-         then output "" (Ocaml_out None) [out_name,ast_ocaml]
-         else output "" (Ocaml_out (Some (List.hd !opt_libs_ocaml))) [out_name,ast_ocaml]
-             *)
+       then
+         let ast_ocaml = rewrite_ast_ocaml ast in
+         let out = match !opt_file_out with None -> "out" | Some s -> s in
+         Ocaml_backend.ocaml_compile out ast_ocaml
        else ());
       (if !(opt_print_lem)
        then let ast_lem = rewrite_ast_lem ast in
-- 
cgit v1.2.3