Boiler plate to generate an ml file from a sail spec. Now debugging the output of such

6 files changed, 110 insertions, 339 deletions

diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
new file mode 100644
index 00000000..b025d522
--- /dev/null
+++ b/src/gen_lib/sail_values.ml
@@ -0,0 +1,59 @@
+(* only expected to be 0, 1, 2; 2 represents undef *)
+type vbit = int
+type number = int64 (*Actually needs to be big_int_z but I forget the incantation for that right now*)
+
+type value =
+  | Vvector of vbit array * int * bool
+  | VvectorR of value array * int * bool
+  | Vregister of vbit array * int * bool * (string * (int * int)) list
+  | Vundef (*For a few circumstances of undefined registers in VvectorRs built with sparse vectors*)
+
+let to_bool = function
+  | 0 -> false
+  | 1 -> true
+  | _ -> assert false
+
+let get_barray  = function
+  | Vvector(a,_,_) 
+  | Vregister(a,_,_,_) -> a
+  | _ -> assert false
+
+let get_varray = function
+  | VvectorR(a,_,_) -> a
+  | _ -> assert false
+
+let vector_access v n = match v with
+  | VvectorR(array,start,is_inc) ->
+    if is_inc
+    then array.(n-start)
+    else array.(start-n)
+  | _ -> assert false
+      
+let bit_vector_access v n = match v with
+  | Vvector(array,start,is_inc) | Vregister(array,start,is_inc,_) ->
+    if is_inc
+    then array.(n-start)
+    else array.(start-n)
+  | _ -> assert false
+
+let vector_subrange v n m =
+  let builder array length offset default =
+    let new_array = Array.make length default in
+    begin
+      for x = 0 to length-1
+      do new_array.(x) <- array.(x+offset) 
+      done;
+      new_array
+    end
+  in
+  match v with
+  | VvectorR(array,start,is_inc) ->
+    let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
+    VvectorR(builder array length offset (VvectorR([||], 0, true)),n,is_inc)
+  | Vvector(array,start,is_inc) ->
+    let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
+    Vvector(builder array length offset 0,n,is_inc)
+  | Vregister(array,start,is_inc,fields) ->
+    let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
+    Vvector(builder array length offset 0,n,is_inc)
+  | _ -> v
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index d667a1ee..1d3947cd 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1374,7 +1374,8 @@ let doc_exp_ocaml, doc_let_ocaml =
       parens ((string "vector_subrange") ^^ space ^^ exp v ^^ space ^^ (exp e1) ^^ space ^^ (exp e2))
     | E_field((E_aux(_,(_,fannot)) as fexp),id) ->
       (match fannot with
-      | Base((_,{t= Tapp("register",_)}),External _,_,_,_) ->
+       | Base((_,{t= Tapp("register",_)}),_,_,_,_) |
+         Base((_,{t= Tabbrev(_,{t=Tapp("register",_)})}),_,_,_,_)->
         parens ((string "get_register_field") ^^ space ^^ exp fexp ^^ space ^^
                 (string "\"") ^^ (doc_id id) ^^ string "\"")
       | _ -> exp fexp ^^ dot ^^ doc_id id)
@@ -1541,10 +1542,10 @@ let doc_typdef_ocaml (TD_aux(td,_)) = match td with
       doc_op equals
         ((string "let") ^^ space ^^ doc_id_ocaml id ^^ space ^^ (string "init_val"))
         (separate space [string "Vregister";
-                         (separate comma_sp [string "init_val";
-                                             doc_nexp n1;
-                                             string (if dir then "true" else "false");
-                                             brackets doc_rids])])
+                         (parens (separate comma_sp [string "init_val";
+                                                     doc_nexp n1;
+                                                     string (if dir then "true" else "false");
+                                                     brackets doc_rids]))])
 
 let doc_rec_ocaml (Rec_aux(r,_)) = match r with
   | Rec_nonrec -> empty
diff --git a/src/process_file.ml b/src/process_file.ml
index efa755b9..726c9051 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -102,6 +102,7 @@ let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.
   Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env,Type_internal.nob,Envmap.empty)) defs 
 
 let rewrite_ast (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs defs
+let rewrite_ast_ocaml (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs_ocaml defs
 
 let open_output_with_check file_name =
   let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
@@ -171,12 +172,12 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo
 	end
       | Ocaml_out None ->
         let ((o,temp_file_name, filename) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in
-	begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["sail_values"];
+	begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Sail_values"];
         close_output_with_check ext_o
         end
       | Ocaml_out (Some lib) ->
         let ((o,temp_file_name, filename) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in
-	Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["sail_values"; lib];
+	Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Sail_values"; lib];
         close_output_with_check ext_o
 
 
diff --git a/src/process_file.mli b/src/process_file.mli
index 9f88178e..232727f1 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -48,6 +48,7 @@ val parse_file : string -> Parse_ast.defs
 val convert_ast : Parse_ast.defs -> Type_internal.tannot Ast.defs * Type_internal.kind Type_internal.Envmap.t * Ast.order
 val check_ast: Type_internal.tannot Ast.defs -> Type_internal.kind Type_internal.Envmap.t -> Ast.order -> Type_internal.tannot Ast.defs
 val rewrite_ast: Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
+val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
 
 type out_type =
   | Lem_ast_out
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 5207d880..7c89a8ac 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -416,7 +416,7 @@ let remove_vector_concat_pat pat =
     let letbind_vec (rootid,rannot) (child,cannot) (i,j) body =
       let index n =
         let typ = simple_annot {t = Tapp ("atom",[TA_nexp (mk_c (big_int_of_int n))])} in
-        E_aux (E_lit (L_aux (L_num n,Unknown)), (Parse_ast.Unknown,typ)) in
+        E_aux (E_lit (L_aux (L_num n,Parse_ast.Unknown)), (Parse_ast.Unknown,typ)) in
       let subv = E_aux (E_vector_subrange (E_aux (E_id rootid,rannot),index i,index j),cannot) in
       let typ = (Parse_ast.Unknown,simple_annot {t = Tid "unit"}) in
       E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_id child,cannot),subv),cannot),body),typ) in
@@ -563,7 +563,7 @@ let rewrite_exp_lift_assign_intro rewriters nmap ((E_aux (exp,(l,annot))) as ful
     rewrap (E_block (walker exps))
   | _ -> rewrite_base full_exp
 
-let rewrite_defs_ocaml defs = rewrite_defs_base
+let rewrite_defs_exp_lift_assign defs = rewrite_defs_base
     {rewrite_exp = rewrite_exp_lift_assign_intro;
      rewrite_pat = rewrite_pat;
      rewrite_let = rewrite_let;
@@ -571,3 +571,8 @@ let rewrite_defs_ocaml defs = rewrite_defs_base
      rewrite_fun = rewrite_fun;
      rewrite_def = rewrite_def;
      rewrite_defs = rewrite_defs_base} defs
+
+let rewrite_defs_ocaml defs =
+  let defs_vec_concat_removed = rewrite_defs_remove_vector_concat defs in
+  let defs_lifted_assign = rewrite_defs_exp_lift_assign defs_vec_concat_removed in
+  defs_lifted_assign
diff --git a/src/sail.ml b/src/sail.ml
index fbc339f0..0fa383ef 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -45,344 +45,41 @@
 (**************************************************************************)
 
 open Process_file
-(*open Debug
-
-let backends = ref []
-let opt_print_types = ref false
-let opt_print_version = ref false
-let opt_library = ref (Some (Build_directory.d^"/library"))
-let lib = ref []
-let ocaml_lib = ref []
-let hol_lib = ref []
-let coq_lib = ref []
-let isa_lib = ref []
-let isa_theory = ref None
-let opt_file_arguments = ref ([]:string list)
-
-let options = Arg.align ([
-  ( "-i",
-    Arg.String (fun l -> lib := l::!lib),
-    " treat the file as input only and generate no output for it");
-  ( "-tex",
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_tex)) !backends) then
-                backends := Some(Typed_ast.Target_tex)::!backends),
-    " generate LaTeX");
-  ( "-html",
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_html)) !backends) then
-                backends := Some(Typed_ast.Target_html)::!backends),
-    " generate Html");
-  ( "-hol",
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_hol)) !backends) then
-                backends := Some(Typed_ast.Target_hol)::!backends),
-    " generate HOL");
-  ( "-ocaml",
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_ocaml)) !backends) then
-                backends := Some(Typed_ast.Target_ocaml)::!backends),
-    " generate OCaml");
-  ( "-isa",
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_isa)) !backends) then
-                backends := Some(Typed_ast.Target_isa)::!backends),
-    " generate Isabelle");
-  ( "-coq",
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_coq)) !backends) then
-                backends := Some(Typed_ast.Target_coq)::!backends),
-    " generate Coq");
-  ( "-ident",
-    Arg.Unit (fun b -> if not (List.mem None !backends) then
-                backends := None::!backends),
-    " generate input on stdout");
-  ( "-print_types",
-    Arg.Unit (fun b -> opt_print_types := true),
-    " print types on stdout");
-  ( "-lib",
-    Arg.String (fun l -> opt_library := Some l),
-    " library path"^match !opt_library with None->"" | Some s -> " (default "^s^")");
-  ( "-ocaml_lib",
-    Arg.String (fun l -> ocaml_lib := l::!ocaml_lib),
-    " add to OCaml library");
-  ( "-hol_lib",
-    Arg.String (fun l -> hol_lib := l::!hol_lib),
-    " add to HOL library");
-  ( "-isa_lib",
-    Arg.String (fun l -> isa_lib := l::!isa_lib),
-    " add to Isabelle library");
-  ( "-isa_theory",
-    Arg.String (fun l -> isa_theory := Some l),
-    " Isabelle Lem theory");
-  ( "-coq_lib",
-    Arg.String (fun l -> coq_lib := l::!coq_lib),
-    " add to Coq library");
-  ( "-v",
-    Arg.Unit (fun b -> opt_print_version := true),
-    " print version");
-  ( "-ident_pat_compile",
-    Arg.Unit (fun b -> Target_trans.ident_force_pattern_compile := true; Reporting.ignore_pat_compile_warnings()),
-    " activates pattern compilation for the identity backend. This is used for debugging.");
-  ( "-only_changed_output",
-    Arg.Unit (fun b -> Process_file.always_replace_files := false),
-    " generate only output files, whose content really changed compared to the existing file");
-  ( "-extra_level",
-    Arg.Symbol (["none"; "auto"; "all"], (fun s ->
-     Backend.gen_extra_level := (match s with
-       | "none" -> 0
-       | "auto" -> 1
-       | _ -> 2))),
-    " generate no (none) extra-information, only extras that can be handled automatically (auto) or all (all) extra information")
-] @ Reporting.warn_opts)
-
-let usage_msg =
-    ("Lem " ^ Version.v ^ "\n"
-     ^ "example usage:       lem -hol -ocaml -lib ../lem/library test.lem\n"
-    )
-
-let _ =
-  Arg.parse options
-    (fun s ->
-      opt_file_arguments := (!opt_file_arguments) @ [s])
-    usage_msg
-
-
-let check_modules (def_info,env) modules =
-  (* The checks. Modify these lists to add more. *)
-  let exp_checks env = [Patterns.check_match_exp_warn env] in
-  let pat_checks env = [] in
-  let def_checks env = [Patterns.check_match_def_warn env] in
-
-  (* Use the Macro_expander to execute these checks *)
-  let (d,_) = def_info in
-  let module Ctxt = struct let avoid = None let check = Some(d) end in
-  let module M = Macro_expander.Expander(Ctxt) in
-  let exp_mac env = Macro_expander.list_to_mac (List.map (fun f e -> (let _ = f e in None)) (exp_checks env)) in
-  let exp_ty env ty = ty in
-  let exp_src_ty env src_t = src_t in
-  let exp_pat env = Macro_expander.list_to_bool_mac (List.map (fun f x p -> (let _ = f x p in None)) (pat_checks env)) in
-  let check_defs env defs = begin
-    let _ = M.expand_defs (List.rev defs) (exp_mac env, exp_ty env, exp_src_ty env, exp_pat env) in
-    let _ = List.map (fun d -> List.map (fun c -> c d) (def_checks env)) defs in
-    ()
-  end in
-  let check_module m = (let (defs, _) = m.Typed_ast.typed_ast in check_defs env defs) in
-  let _ = List.map check_module modules in
-  ()
-
-
-(* Do the transformations for a given target, and then generate the output files
- * *)
-let per_target libpath isa_thy modules (def_info,env) consts alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum targ =
-  let consts = List.assoc targ consts in
-  let module C = struct
-    let (d,i) = def_info
-  end
-  in
-  let module T = Target_trans.Make(C) in
-  let (trans,avoid) = T.get_transformation targ consts in
-    try
-      let (_,transformed_m) =
-        List.fold_left
-          (fun (env,new_mods) old_mod ->
-             let (env,m) = trans env old_mod in
-               (env,m::new_mods))
-          (env,[])
-          modules
-      in
-      let consts' = T.extend_consts targ consts transformed_m in
-      let transformed_m' = T.rename_def_params targ consts' transformed_m in
-        output libpath isa_thy targ (avoid consts') def_info (List.rev transformed_m') alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum
-    with
-      | Trans.Trans_error(l,msg) ->
-          raise (Reporting_basic.Fatal_error (Reporting_basic.Err_trans (l, msg)))
-      | Ident.No_type(l,msg) ->
-          raise (Reporting_basic.Fatal_error (Reporting_basic.Err_internal (l, msg)))
-      | Typed_ast.Renaming_error(ls,msg) ->
-          raise (Reporting_basic.Fatal_error (Reporting_basic.Err_rename (ls, msg)))
-
-
-let main () =
-  let _ = if !opt_print_version then print_string ("Lem " ^ Version.v ^ "\n") in
-  let lib_path =
-    match !opt_library with
-      | None -> (try
-                let lp = Sys.getenv("LEMLIB") in
-                if Filename.is_relative lp
-                then Filename.concat (Sys.getcwd ()) lp
-                else lp
-            with
-                | Not_found -> raise (Failure("must specify a -lib argument or have a LEMLIB environment variable")))
-      | Some lp ->
-          if Filename.is_relative lp then
-            Filename.concat (Sys.getcwd ()) lp
-          else
-            lp
-  in
-  let isa_thy =
-    match !isa_theory with
-      | None -> Filename.concat lib_path "../isabelle-lib/Lem"
-      | Some thy -> thy
-  in
-  let _ =
-    List.iter
-      (fun f ->
-         try
-           if String.compare ".lem" (String.sub f (String.length f - 4) 4) <> 0 then
-             raise (Failure("Files must have .lem extension"))
-         with
-           | Invalid_argument _ ->
-             raise (Failure("Files must have .lem extension")))
-      (!opt_file_arguments @ !lib @ !ocaml_lib @ !hol_lib @ !isa_lib @ !coq_lib)
-  in
-  let _ =
-    List.iter
-      (fun f ->
-         if not (Str.string_match (Str.regexp "[A-Za-z]") (Filename.basename f) 0) then
-           raise (Failure(".lem filenames must start with a letter")))
-      (!opt_file_arguments @ !lib @ !ocaml_lib @ !hol_lib @ !isa_lib @ !coq_lib)
-  in
-  let init =
-    try
-      let inchannel = open_in (Filename.concat lib_path "lib_cache") in
-      let v = input_value inchannel in
-        close_in inchannel;
-        v
-    with
-      | Sys_error _ ->
-          let module I = Initial_env.Initial_libs(struct let path = lib_path end) in
-          let outchannel = open_out (Filename.concat lib_path "lib_cache") in
-            output_value outchannel I.init;
-            close_out outchannel;
-            I.init
-  in
-  (* TODO: These should go into the sets of top-level constant names *)
-  let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_hol) !hol_lib init in
-  let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_ocaml) !ocaml_lib init in
-  let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_isa) !isa_lib init in
-  let init = List.fold_right (Initial_env.add_to_init Typed_ast.Target_coq) !coq_lib init in
-
-  let consts =
-    List.map
-      (fun (targ,cL) ->
-        let consts = List.fold_left
-              (fun s c -> Typed_ast.NameSet.add (Name.from_rope c) s)
-              Typed_ast.NameSet.empty
-              cL in
-         (targ,consts))
-      (snd init)
-  in
-  let type_info : (Types.type_defs * instances) * Typed_ast.env = fst init in
-  (* Parse and typecheck all of the .lem sources *)
-  let (modules, type_info, _) =
-    List.fold_left
-      (fun (mods, (def_info,env), previously_processed_modules) (f, add_to_modules) ->
-         let ast = parse_file f in
-         let f' = Filename.basename (Filename.chop_extension f) in
-         let mod_name = String.capitalize f' in
-         let mod_name_name = Name.from_rope (Ulib.Text.of_latin1 mod_name) in
-         let backend_set =
-           List.fold_right
-             (fun x s ->
-                match x with
-                  | None -> s
-                  | Some(Typed_ast.Target_tex) -> s
-                  | Some(Typed_ast.Target_html) -> s
-                  | Some(t) -> Typed_ast.Targetset.add t s)
-             !backends
-             Typed_ast.Targetset.empty
-         in
-         let ((tdefs,instances,new_instances),new_env,tast) =
-           check_ast backend_set [mod_name_name] (def_info,env) ast
-         in
-         let md = { Typed_ast.mod_env = new_env; Typed_ast.mod_binding = Path.mk_path [] mod_name_name } in
-         let e = { env with Typed_ast.m_env = Typed_ast.Nfmap.insert env.Typed_ast.m_env (mod_name_name,md) } in
-         let module_record =
-           { Typed_ast.filename = f;
-             Typed_ast.module_name = mod_name;
-             Typed_ast.predecessor_modules = previously_processed_modules;
-             Typed_ast.untyped_ast = ast;
-             Typed_ast.typed_ast = tast; }
-         in
-           if !opt_print_types then
-             begin
-               (*
-               Format.fprintf Format.std_formatter "%s@\nlibrary:@\n" f;
-               Typed_ast.pp_env Format.std_formatter (snd type_info);
-                *)
-               Format.fprintf Format.std_formatter "%s@\nenvironment:@\n" f;
-               Typed_ast.pp_env Format.std_formatter new_env;
-               Format.fprintf Format.std_formatter "@\ninstances:@\n";
-               Typed_ast.pp_instances Format.std_formatter new_instances;
-               Format.fprintf Format.std_formatter "@\n@\n"
-             end;
-           ((if add_to_modules then
-             module_record::mods
-               else
-             mods),
-            ((tdefs,instances),e), mod_name::previously_processed_modules))
-      ([],type_info,[])
-      (* We don't want to add the files in !lib to the resulting module ASTs,
-       * because we don't want to put them throught the back end *)
-      (List.map (fun x -> (x, false)) (List.rev !lib) @
-       List.map (fun x -> (x, true)) !opt_file_arguments)
-  in
-
-  (* Check the parsed source and produce warnings for various things. Currently:
-     - non-exhaustive and redundant patterns
-  *)
-  let _ = check_modules type_info modules in
-
-  let alldoc_accum = ref ([] : Ulib.Text.t list) in
-  let alldoc_inc_accum = ref ([] : Ulib.Text.t list) in
-  let alldoc_inc_usage_accum = ref ([] : Ulib.Text.t list) in
-    ignore (List.iter (per_target lib_path isa_thy (List.rev modules) type_info consts alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum) !backends);
-    (if List.mem (Some(Typed_ast.Target_tex)) !backends then
-       output_alldoc "alldoc" (String.concat " " !opt_file_arguments) alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum)
-
-let _ =
-  try
-    begin
-      try ignore(main ())
-      with  Failure(s) -> raise (Reporting_basic.err_general false Ast.Unknown ("Failure "^s))
-    end
-  with Reporting_basic.Fatal_error e -> Reporting_basic.report_error e
-
-*)
 
 let lib = ref []
 let opt_print_version = ref false
 let opt_print_verbose = ref false
 let opt_print_lem = ref false
+let opt_print_ocaml = ref false
+let opt_libs_ocaml = ref ([]:string list)
 let opt_file_arguments = ref ([]:string list)
 let options = Arg.align ([
   ( "-i",
     Arg.String (fun l -> lib := l::!lib),
     " treat the file as input only and generate no output for it");
-  (*( "-tex",
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_tex)) !backends) then
-                backends := Some(Typed_ast.Target_tex)::!backends),
-    " generate LaTeX");
-  ( "-html",
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_html)) !backends) then
-                backends := Some(Typed_ast.Target_html)::!backends),
-    " generate Html");
-  ( "-ident",
-    Arg.Unit (fun b -> if not (List.mem None !backends) then
-                backends := None::!backends),
-    " generate input on stdout");*)
   ( "-verbose",
     Arg.Unit (fun b -> opt_print_verbose := true),
     " pretty-print out the file");
   ( "-lem_ast",
     Arg.Unit (fun b -> opt_print_lem := true),
     " pretty-print a Lem AST representation of the file");
+  ( "-ocaml",
+    Arg.Unit (fun b -> opt_print_ocaml := true),
+    " print an Ocaml translated version of the specification");
   ( "-skip_constraints",
     Arg.Clear Type_internal.do_resolve_constraints,
     " skip constraint resolution in type-checking");
+  ( "-ocaml_lib",
+    Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml),
+    " provide additional library to open in Ocaml output");
   ( "-v",
     Arg.Unit (fun b -> opt_print_version := true),
     " print version");
 ] )
 
 let usage_msg =
-    ("L2 " ^ "pre alpha" ^ "\n"
-     ^ "example usage:       l2 test.ltwo\n"
+    ("Sail " ^ "pre beta" ^ "\n"
+     ^ "example usage:       sail test.sail\n"
     )
 
 let _ =
@@ -393,23 +90,30 @@ let _ =
 
 let main() =
   if !(opt_print_version)
-  then Printf.printf "L2 private release \n"
-  else let parsed = (List.map (fun f -> (f,(parse_file f)))  !opt_file_arguments) in
-       let ast = 
-	 List.fold_right (fun (_,(Parse_ast.Defs ast_nodes)) (Parse_ast.Defs later_nodes) 
-	 -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
-       let (ast,kenv,ord) = convert_ast ast in
-       let ast = check_ast ast kenv ord in 
-       let ast = rewrite_ast ast in
-       (*let _ = Printf.eprintf "Type checked, next to pretty print" in*)
-       begin 
-	 (if !(opt_print_verbose)
-	  then ((Pretty_print.pp_defs stdout) ast)
-	  else ());
-	 (if !(opt_print_lem)
-	  then output "" Lem_ast_out [(fst (List.hd parsed)),ast]
-	  else ());
-       end
+  then Printf.printf "Sail private release \n"
+  else
+    let parsed = (List.map (fun f -> (f,(parse_file f)))  !opt_file_arguments) in
+    let ast = 
+      List.fold_right (fun (_,(Parse_ast.Defs ast_nodes)) (Parse_ast.Defs later_nodes) 
+                        -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
+    let (ast,kenv,ord) = convert_ast ast in
+    let ast = check_ast ast kenv ord in 
+    let ast = rewrite_ast ast in
+    (*let _ = Printf.eprintf "Type checked, next to pretty print" in*)
+    begin 
+      (if !(opt_print_verbose)
+       then ((Pretty_print.pp_defs stdout) ast)
+       else ());
+      (if !(opt_print_lem)
+       then output "" Lem_ast_out [(fst (List.hd parsed)),ast]
+       else ());
+      (if !(opt_print_ocaml)
+       then let ast_ocaml = rewrite_ast_ocaml ast in
+         if !(opt_libs_ocaml) = []
+         then output "" (Ocaml_out None) [(fst (List.hd parsed)),ast_ocaml]
+         else output "" (Ocaml_out (Some (List.hd !opt_libs_ocaml))) [(fst (List.hd parsed)),ast_ocaml]
+       else ());
+    end
 
 let _ =  try
     begin