Interactive: Refactor sail.ml

Rather than having a separate variable for each backend X,
opt_print_X, just have a single variable opt_print_target, where
target contains a string option, such as `Some "lem"` or `Some
"ocaml"`, then we have a function target that takes that string and
invokes the appropriate backend, so the main function in sail.ml goes
from being a giant if-then-else block to a single call to

target !opt_target ast env

This allows us to implement a :compile <target> command in the
interactive toplevel

Also implement a :rewrites <target> command which performs all the
rewrites for a specific target, so rather than doing e.g.

> sail -c -O -o out $FILES

one could instead interactively do

> sail -i
:option -undefined_gen
:load $FILES
:option -O
:option -o out
:rewrites c
:compile c
:quit

for the same result.

To support this the behavior of the interactive mode has changed
slightly. It no longer performs any rewrites at all, so a :rewrites
interpreter is currently needed to interpret functions in the
interactive toplevel, nor does it automatically set any other flags,
so -undefined_gen is needed in this case, which is usually implied by
the -c flag.

6 files changed, 212 insertions, 206 deletions

diff --git a/src/isail.ml b/src/isail.ml
index 2527df0e..e02427d6 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -148,7 +148,6 @@ let rec run () =
      end
 
 let rec run_steps n =
-  print_endline ("step " ^ string_of_int n);
   match !current_mode with
   | _ when n <= 0 -> ()
   | Normal | Emacs -> ()
@@ -172,50 +171,81 @@ let rec run_steps n =
           current_mode := Evaluation frame
      end
 
-let help = function
+let help =
+  let open Printf in
+  let open Util in
+  let color c str = str |> c |> clear in
+  function
   | ":t" | ":type" ->
-     "(:t | :type) <function name> - Print the type of a function."
+     sprintf "(:t | :type) %s - Print the type of a function."
+             (color yellow "<function name>")
   | ":q" | ":quit" ->
      "(:q | :quit) - Exit the interpreter."
   | ":i" | ":infer" ->
-     "(:i | :infer) <expression> - Infer the type of an expression."
+     sprintf "(:i | :infer) %s - Infer the type of an expression."
+             (color yellow "<expression>")
   | ":v" | ":verbose" ->
      "(:v | :verbose) - Increase the verbosity level, or reset to zero at max verbosity."
   | ":b" | ":bind" ->
-     "(:b | :bind) <id> : <typ> - Declare a variable of a specific type"
+     sprintf "(:b | :bind) %s : %s - Declare a variable of a specific type"
+             (color yellow "<id>") (color yellow "<type>")
   | ":let" ->
-     ":let <id> = <exp> - Bind a variable to expression"
+     sprintf ":let %s = %s - Bind a variable to expression"
+             (color yellow "<id>") (color yellow "<expression>")
   | ":def" ->
-     ":def <definition> - Evaluate a top-level definition"
+     sprintf ":def %s - Evaluate a top-level definition"
+             (color yellow "<definition>")
   | ":prove" ->
-     ":prove <constraint> - Try to prove a constraint in the top-level environment"
+     sprintf ":prove %s - Try to prove a constraint in the top-level environment"
+             (color yellow "<constraint>")
   | ":assume" ->
-     ":assume <constraint> - Add a constraint to the top-level environment"
+     sprintf ":assume %s - Add a constraint to the top-level environment"
+             (color yellow "<constraint>")
   | ":commands" ->
      ":commands - List all available commands."
   | ":help" ->
-     ":help <command> - Get a description of <command>. Commands are prefixed with a colon, e.g. :help :type."
+     sprintf ":help %s - Get a description of <command>. Commands are prefixed with a colon, e.g. %s."
+             (color yellow "<command>") (color green ":help :type")
   | ":elf" ->
-     ":elf <file> - Load an ELF file."
+     sprintf ":elf %s - Load an ELF file."
+             (color yellow "<file>")
   | ":r" | ":run" ->
      "(:r | :run) - Completely evaluate the currently evaluating expression."
   | ":s" | ":step" ->
-     "(:s | :step) <number> - Perform a number of evaluation steps."
+     sprintf "(:s | :step) %s - Perform a number of evaluation steps."
+             (color yellow "<number>")
   | ":n" | ":normal" ->
      "(:n | :normal) - Exit evaluation mode back to normal mode."
   | ":clear" ->
-     ":clear (on|off) - Set whether to clear the screen or not in evaluation mode."
+     sprintf ":clear %s - Set whether to clear the screen or not in evaluation mode."
+             (color yellow "(on|off)")
   | ":l" | ":load" -> String.concat "\n"
-     [ "(:l | :load) <files> - Load sail files and add their definitions to the interactive environment.";
+     [ sprintf "(:l | :load) %s - Load sail files and add their definitions to the interactive environment."
+               (color yellow "<files>");
        "Files containing scattered definitions must be loaded together." ]
   | ":u" | ":unload" ->
      "(:u | :unload) - Unload all loaded files."
   | ":output" ->
-     ":output <file> - Redirect evaluating expression output to a file."
+     sprintf ":output %s - Redirect evaluating expression output to a file."
+             (color yellow "<file>")
   | ":option" ->
-     ":option string - Parse string as if it was an option passed on the command line. Try :option -help."
+     sprintf ":option %s - Parse string as if it was an option passed on the command line. e.g. :option -help."
+             (color yellow "<string>")
+  | ":rewrite" ->
+     sprintf ":rewrite %s - Apply a rewrite to the AST. %s shows all possible rewrites. See also %s"
+             (color yellow "<rewrite> <args>") (color green ":list_rewrites") (color green ":rewrites")
+  | ":rewrites" ->
+     sprintf ":rewrites %s - Apply all rewrites for a specific target, valid targets are lem, coq, ocaml, c, and interpreter"
+             (color yellow "<target>")
+  | ":compile" ->
+     sprintf ":compile %s - Compile AST to a specified target, valid targets are lem, coq, ocaml, c, and ir (intermediate representation)"
+             (color yellow "<target>")
+  | "" ->
+     sprintf "Type %s for a list of commands, and %s %s for information about a specific command"
+             (color green ":commands") (color green ":help") (color yellow "<command>")
   | cmd ->
-     "Either invalid command passed to help, or no documentation for " ^ cmd ^ ". Try :help :help."
+     sprintf "Either invalid command passed to help, or no documentation for %s. Try %s."
+             (color green cmd) (color green ":help :help")
 
 let format_pos_emacs p1 p2 contents =
   let open Lexing in
@@ -242,7 +272,7 @@ let rec describe_rewrite =
   function
   | String_rewriter rw -> "<string>" :: describe_rewrite (rw "")
   | Bool_rewriter rw -> "<bool>" :: describe_rewrite (rw false)
-  | Literal_rewriter rw -> "<ocaml/lem/all>" :: describe_rewrite (rw (fun _ -> true))
+  | Literal_rewriter rw -> "(ocaml|lem|all)" :: describe_rewrite (rw (fun _ -> true))
   | Basic_rewriter rw -> []
 
 type session = {
@@ -351,7 +381,7 @@ let handle_input' input =
      | ":commands" ->
         let commands =
           [ "Universal commands - :(t)ype :(i)nfer :(q)uit :(v)erbose :prove :assume :clear :commands :help :output :option";
-            "Normal mode commands - :elf :(l)oad :(u)nload :let :def :(b)ind";
+            "Normal mode commands - :elf :(l)oad :(u)nload :let :def :(b)ind :rewrite :rewrites :list_rewrites :compile";
             "Evaluation mode commands - :(r)un :(s)tep :(n)ormal";
             "";
             ":(c)ommand can be called as either :c or :command." ]
@@ -407,7 +437,7 @@ let handle_input' input =
         | ":l" | ":load" ->
            let files = Util.split_on_char ' ' arg in
            let (_, ast, env) = load_files !Interactive.env files in
-           let ast = Process_file.rewrite_ast_interpreter !Interactive.env ast in
+           let ast = Process_file.rewrite_ast_target "interpreter" !Interactive.env ast in
            Interactive.ast := append_ast !Interactive.ast ast;
            interactive_state := initial_state !Interactive.ast Value.primops;
            Interactive.env := env;
@@ -495,10 +525,20 @@ let handle_input' input =
            | rw :: args ->
               let rw = List.assoc rw Rewrites.all_rewrites in
               let rw = parse_args rw args in
-              Interactive.ast := rw !Interactive.env !Interactive.ast
+              Interactive.ast := rw !Interactive.env !Interactive.ast;
+              interactive_state := initial_state !Interactive.ast Value.primops;
            | [] ->
               failwith "Must provide the name of a rewrite, use :list_rewrites for a list of possible rewrites"
            end
+        | ":rewrites" ->
+           Interactive.ast := Process_file.rewrite_ast_target arg !Interactive.env !Interactive.ast;
+           interactive_state := initial_state !Interactive.ast Value.primops;
+        | ":compile" ->
+           let out_name = match !opt_file_out with
+             | None -> "out.sail"
+             | Some f -> f ^ ".sail"
+           in
+           target (Some arg) out_name !Interactive.ast !Interactive.env
         | _ -> unrecognised_command cmd
         end
      | Expression str ->
@@ -674,6 +714,8 @@ let () =
       | ":def" -> hint "<definition>"
       | ":prove" -> hint "<constraint>"
       | ":assume" -> hint "<constraint>"
+      | ":compile" -> hint "<target>"
+      | ":rewrites" -> hint "<target>"
       | str ->
          let args = Str.split (Str.regexp " +") str in
          match args with
diff --git a/src/process_file.ml b/src/process_file.ml
index e7bf8d30..c6d900b4 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -402,14 +402,8 @@ let rewrite env rewriters defs =
   | Type_check.Type_error (_, l, err) ->
      raise (Reporting.err_typ l (Type_error.string_of_type_error err))
 
-let rewrite_ast env = rewrite env [("initial", fun _ -> Rewriter.rewrite_defs)]
-let rewrite_ast_lem env = rewrite env Rewrites.rewrite_defs_lem
-let rewrite_ast_coq env = rewrite env Rewrites.rewrite_defs_coq
-let rewrite_ast_ocaml env = rewrite env Rewrites.rewrite_defs_ocaml
-let rewrite_ast_c env ast =
-  ast
-  |> rewrite env Rewrites.rewrite_defs_c
-  |> rewrite env [("constant_fold", fun _ -> Constant_fold.rewrite_constant_function_calls)]
-
-let rewrite_ast_interpreter env = rewrite env Rewrites.rewrite_defs_interpreter
+let rewrite_ast_initial env = rewrite env [("initial", fun _ -> Rewriter.rewrite_defs)]
+
+let rewrite_ast_target tgt env = rewrite env (Rewrites.rewrite_defs_target tgt)
+
 let rewrite_ast_check env = rewrite env Rewrites.rewrite_defs_check
diff --git a/src/process_file.mli b/src/process_file.mli
index 0411464b..e144727e 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -55,13 +55,9 @@ val parse_file : ?loc:Parse_ast.l -> string -> Parse_ast.defs
 val clear_symbols : unit -> unit
 
 val preprocess_ast : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.defs -> Parse_ast.defs
-val check_ast: Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
-val rewrite_ast: Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_lem : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_coq : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_ocaml : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_c : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
-val rewrite_ast_interpreter : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val check_ast : Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
+val rewrite_ast_initial : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_ast_target : string -> Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
 val rewrite_ast_check : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
 
 val load_file_no_check : (Arg.key * Arg.spec * Arg.doc) list -> Ast.order -> string -> unit Ast.defs
diff --git a/src/rewrites.ml b/src/rewrites.ml
index f525cc63..30899950 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4745,6 +4745,7 @@ let all_rewrites = [
     ("simple_types", Basic_rewriter rewrite_simple_types);
     ("overload_cast", Basic_rewriter rewrite_overload_cast);
     ("top_sort_defs", Basic_rewriter (fun _ -> top_sort_defs));
+    ("constant_fold", Basic_rewriter (fun _ -> Constant_fold.rewrite_constant_function_calls));
     ("split", String_rewriter (fun str -> Basic_rewriter (rewrite_split_fun_ctor_pats str)))
   ]
 
@@ -4845,7 +4846,6 @@ let rewrites_coq = [
     ("recheck_defs", [])
   ]
 
-
 let rewrites_ocaml = [
     ("no_effect_check", []);
     ("realise_mappings", []);
@@ -4891,7 +4891,8 @@ let rewrites_c = [
     ("remove_bitvector_pats", []);
     ("exp_lift_assign", []);
     ("merge_function_clauses", []);
-    ("optimize_recheck_defs", [])
+    ("optimize_recheck_defs", []);
+    ("constant_fold", [])
   ]
 
 let rewrites_interpreter = [
@@ -4906,20 +4907,18 @@ let rewrites_interpreter = [
     ("simple_assignments", [])
   ]
 
-let rewrite_defs_coq =
-  List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) rewrites_coq
-
-let rewrite_defs_lem =
-  List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) rewrites_lem
-
-let rewrite_defs_ocaml =
-  List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) rewrites_ocaml
-
-let rewrite_defs_c =
-  List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) rewrites_c
+let rewrites_target tgt =
+  match tgt with
+  | "coq" -> rewrites_coq
+  | "lem" -> rewrites_lem
+  | "ocaml" -> rewrites_ocaml
+  | "c" -> rewrites_c
+  | "interpreter" -> rewrites_interpreter
+  | _ ->
+     raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ ("Invalid target for rewriting: " ^ tgt))
 
-let rewrite_defs_interpreter =
-  List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) rewrites_interpreter
+let rewrite_defs_target tgt =
+  List.map (fun (name, args) -> (name, instantiate_rewrite (List.assoc name all_rewrites) args)) (rewrites_target tgt)
 
 let rewrite_check_annot =
   let check_annot exp =
diff --git a/src/rewrites.mli b/src/rewrites.mli
index 656f5400..330f10b4 100644
--- a/src/rewrites.mli
+++ b/src/rewrites.mli
@@ -66,17 +66,8 @@ val fresh_id : string -> l -> id
 (* Re-write undefined to functions created by -undefined_gen flag *)
 val rewrite_undefined : bool -> Env.t -> tannot defs -> tannot defs
 
-(* Perform rewrites to exclude AST nodes not supported for ocaml out*)
-val rewrite_defs_ocaml : (string * (Env.t -> tannot defs -> tannot defs)) list
-
-(* Perform rewrites to exclude AST nodes not supported for interpreter *)
-val rewrite_defs_interpreter : (string * (Env.t -> tannot defs -> tannot defs)) list
-
-(* Perform rewrites to exclude AST nodes not supported for lem out*)
-val rewrite_defs_lem : (string * (Env.t -> tannot defs -> tannot defs)) list
-
-(* Perform rewrites to exclude AST nodes not supported for coq out*)
-val rewrite_defs_coq : (string * (Env.t -> tannot defs -> tannot defs)) list
+(* Perform rewrites to create an AST supported for a specific target *)
+val rewrite_defs_target : string -> (string * (Env.t -> tannot defs -> tannot defs)) list
 
 type rewriter =
   | Basic_rewriter of (Env.t -> tannot defs -> tannot defs)
@@ -100,9 +91,6 @@ val all_rewrites : (string * rewriter) list
    exhaustive *)
 val opt_coq_warn_nonexhaustive : bool ref
 
-(* Perform rewrites to exclude AST nodes not supported for C compilation *)
-val rewrite_defs_c : (string * (Env.t -> tannot defs -> tannot defs)) list
-
 (* This is a special rewriter pass that checks AST invariants without
    actually doing any re-writing *)
 val rewrite_defs_check : (string * (Env.t -> tannot defs -> tannot defs)) list
diff --git a/src/sail.ml b/src/sail.ml
index 7416aac2..eb4a829d 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -56,15 +56,7 @@ let lib = ref ([] : string list)
 let opt_file_out : string option ref = ref None
 let opt_interactive_script : string option ref = ref None
 let opt_print_version = ref false
-let opt_print_initial_env = ref false
-let opt_print_verbose = ref false
-let opt_print_lem = ref false
-let opt_print_ocaml = ref false
-let opt_print_c = ref false
-let opt_print_ir = ref false
-let opt_print_latex = ref false
-let opt_print_coq = ref false
-let opt_print_cgen = ref false
+let opt_target = ref None
 let opt_memo_z3 = ref false
 let opt_sanity = ref false
 let opt_includes_c = ref ([]:string list)
@@ -76,16 +68,17 @@ let opt_process_elf : string option ref = ref None
 let opt_ocaml_generators = ref ([]:string list)
 let opt_slice = ref ([]:string list)
 
+let set_target name = Arg.Unit (fun _ -> opt_target := Some name)
+
 let options = Arg.align ([
   ( "-o",
     Arg.String (fun f -> opt_file_out := Some f),
     "<prefix> select output filename prefix");
   ( "-i",
-    Arg.Tuple [Arg.Set Interactive.opt_interactive; Arg.Set Initial_check.opt_undefined_gen],
+    Arg.Tuple [Arg.Set Interactive.opt_interactive],
     " start interactive interpreter");
   ( "-is",
-    Arg.Tuple [Arg.Set Interactive.opt_interactive; Arg.Set Initial_check.opt_undefined_gen;
-               Arg.String (fun s -> opt_interactive_script := Some s)],
+    Arg.Tuple [Arg.Set Interactive.opt_interactive; Arg.String (fun s -> opt_interactive_script := Some s)],
     "<filename> start interactive interpreter and execute commands in script");
   ( "-iout",
     Arg.String (fun file -> Value.output_redirect (open_out file)),
@@ -97,13 +90,13 @@ let options = Arg.align ([
     Arg.Clear Util.opt_warnings,
     " do not print warnings");
   ( "-ocaml",
-    Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen],
+    Arg.Tuple [set_target "ocaml"; Arg.Set Initial_check.opt_undefined_gen],
     " output an OCaml translated version of the input");
   ( "-ocaml-nobuild",
     Arg.Set Ocaml_backend.opt_ocaml_nobuild,
     " do not build generated OCaml");
   ( "-ocaml_trace",
-    Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen; Arg.Set Ocaml_backend.opt_trace_ocaml],
+    Arg.Tuple [set_target "ocaml"; Arg.Set Initial_check.opt_undefined_gen; Arg.Set Ocaml_backend.opt_trace_ocaml],
     " output an OCaml translated version of the input with tracing instrumentation, implies -ocaml");
   ( "-ocaml_build_dir",
     Arg.String (fun dir -> Ocaml_backend.opt_ocaml_build_dir := dir),
@@ -121,7 +114,7 @@ let options = Arg.align ([
     Arg.Set Type_check.opt_smt_linearize,
     "(experimental) force linearization for constraints involving exponentials");
   ( "-latex",
-    Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec],
+    Arg.Tuple [set_target "latex"; Arg.Clear Type_check.opt_expand_valspec],
     " pretty print the input to LaTeX");
   ( "-latex_prefix",
     Arg.String (fun prefix -> Latex.opt_prefix := prefix),
@@ -130,10 +123,10 @@ let options = Arg.align ([
     Arg.Clear Latex.opt_simple_val,
     " print full valspecs in LaTeX output");
   ( "-ir",
-    Arg.Set opt_print_ir,
+    set_target "ir",
     " print intermediate representation");
   ( "-c",
-    Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen],
+    Arg.Tuple [set_target "c"; Arg.Set Initial_check.opt_undefined_gen],
     " output a C translated version of the input");
   ( "-c_include",
     Arg.String (fun i -> opt_includes_c := i::!opt_includes_c),
@@ -179,11 +172,8 @@ let options = Arg.align ([
   ( "-trace",
     Arg.Tuple [Arg.Set Ocaml_backend.opt_trace_ocaml],
     " instrument output with tracing");
-  ( "-cgen",
-    Arg.Set opt_print_cgen,
-    " generate CGEN source");
   ( "-lem",
-    Arg.Set opt_print_lem,
+    set_target "lem",
     " output a Lem translated version of the input");
   ( "-lem_output_dir",
     Arg.String (fun dir -> Process_file.opt_lem_output_dir := Some dir),
@@ -201,7 +191,7 @@ let options = Arg.align ([
     Arg.Set Pretty_print_lem.opt_mwords,
     " use native machine word library for Lem output");
   ( "-coq",
-    Arg.Set opt_print_coq,
+    set_target "coq",
     " output a Coq translated version of the input");
   ( "-coq_output_dir",
     Arg.String (fun dir -> Process_file.opt_coq_output_dir := Some dir),
@@ -278,7 +268,7 @@ let options = Arg.align ([
     Arg.Int (fun verbosity -> Util.opt_verbosity := verbosity),
     " produce verbose output");
   ( "-output_sail",
-    Arg.Set opt_print_verbose,
+    set_target "sail",
     " print Sail code after type checking and initial rewriting");
   ( "-ddump_tc_ast",
     Arg.Set opt_ddump_tc_ast,
@@ -359,7 +349,7 @@ let load_files ?check:(check=false) type_envs files =
     ("out.sail", ast, type_envs)
   else
     let ast = Scattered.descatter ast in
-    let ast = rewrite_ast type_envs ast in
+    let ast = rewrite_ast_initial type_envs ast in
 
     let out_name = match !opt_file_out with
       | None when parsed = [] -> "out.sail"
@@ -368,127 +358,124 @@ let load_files ?check:(check=false) type_envs files =
 
     (out_name, ast, type_envs)
 
-let main() =
+let target name out_name ast type_envs =
+  match name with
+  | None -> ()
+
+  | Some "sail" ->
+     Pretty_print_sail.pp_defs stdout ast
+
+  | Some "ocaml" ->
+     let ocaml_generator_info =
+       match !opt_ocaml_generators with
+       | [] -> None
+       | _ -> Some (Ocaml_backend.orig_types_for_ocaml_generator ast, !opt_ocaml_generators)
+     in
+     let ast_ocaml = rewrite_ast_target "ocaml" type_envs ast in
+     let out = match !opt_file_out with None -> "out" | Some s -> s in
+     Ocaml_backend.ocaml_compile out ast_ocaml ocaml_generator_info
+
+  | Some "c" ->
+     let ast_c = rewrite_ast_target "c" type_envs ast in
+     let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast_c type_envs) in
+     let ast_c, type_envs =
+       if !opt_specialize_c then
+         Specialize.(specialize' 2 int_specialization ast_c type_envs)
+       else
+         ast_c, type_envs
+     in
+     let close, output_chan = match !opt_file_out with Some f -> true, open_out (f ^ ".c") | None -> false, stdout in
+     Util.opt_warnings := true;
+     C_backend.compile_ast type_envs output_chan (!opt_includes_c) ast_c;
+     if close then close_out output_chan else ()
+
+  | Some "ir" ->
+     let ast_c = rewrite_ast_target "c" type_envs ast in
+     let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast_c type_envs) in
+     let ast_c, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_c type_envs) in
+     let close, output_chan =
+       match !opt_file_out with
+       | Some f -> Util.opt_colors := false; (true, open_out (f ^ ".ir.sail"))
+       | None -> false, stdout
+     in
+     Util.opt_warnings := true;
+     let cdefs, _ = C_backend.jib_of_ast type_envs ast_c in
+     let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_cdef cdefs) in
+     output_string output_chan (str ^ "\n");
+     if close then close_out output_chan else ()
+
+  | Some "lem" ->
+     let mwords = !Pretty_print_lem.opt_mwords in
+     let type_envs, ast_lem = State.add_regstate_defs mwords type_envs ast in
+     let ast_lem = rewrite_ast_target "lem" type_envs ast_lem in
+     output "" (Lem_out (!opt_libs_lem)) [(out_name, type_envs, ast_lem)]
+
+  | Some "coq" ->
+     let type_envs, ast_coq = State.add_regstate_defs true type_envs ast in
+     let ast_coq = rewrite_ast_target "coq" type_envs ast_coq in
+     output "" (Coq_out (!opt_libs_coq)) [(out_name, type_envs, ast_coq)]
+
+  | Some "latex" ->
+     Util.opt_warnings := true;
+     let latex_dir = match !opt_file_out with None -> "sail_latex" | Some s -> s in
+     begin
+       try
+         if not (Sys.is_directory latex_dir) then begin
+             prerr_endline ("Failure: latex output location exists and is not a directory: " ^ latex_dir);
+             exit 1
+           end
+       with Sys_error(_) -> Unix.mkdir latex_dir 0o755
+     end;
+     Latex.opt_directory := latex_dir;
+     let chan = open_out (Filename.concat latex_dir "commands.tex") in
+     output_string chan (Pretty_print_sail.to_string (Latex.defs ast));
+     close_out chan
+
+  | Some t ->
+     raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ ("Undefined target: " ^ t))
+
+let main () =
   if !opt_print_version then
     print_endline version
   else
-    let out_name, ast, type_envs = load_files Type_check.initial_env !opt_file_arguments in
-    Util.opt_warnings := false; (* Don't show warnings during re-writing for now *)
-
-    begin match !opt_process_elf, !opt_file_out with
-    | Some elf, Some out ->
-       begin
-         let open Elf_loader in
-         let chan = open_out out in
-         load_elf ~writer:(write_file chan) elf;
-         output_string chan "elf_entry\n";
-         output_string chan (Big_int.to_string !opt_elf_entry ^ "\n");
-         close_out chan;
-         exit 0
-       end
-    | Some _, None ->
-       prerr_endline "Failure: No output file given for processed ELF (option -o).";
-       exit 1
-    | None, _ -> ()
-    end;
-
-    let ocaml_generator_info =
-      match !opt_ocaml_generators with
-      | [] -> None
-      | _ -> Some (Ocaml_backend.orig_types_for_ocaml_generator ast, !opt_ocaml_generators)
-    in
-
     begin
-      (if !(Interactive.opt_interactive)
-       then
-         (Interactive.ast := Process_file.rewrite_ast_interpreter type_envs ast; Interactive.env := type_envs)
-       else ());
-      (if !(opt_sanity)
-       then
-         let _ = rewrite_ast_check type_envs ast in
-         ()
-       else ());
-      (if !(opt_print_verbose)
-       then ((Pretty_print_sail.pp_defs stdout) ast)
-       else ());
-      (match !opt_slice with
-       | [] -> ()
-       | ids ->
-          let ids = List.map Ast_util.mk_id ids in
-          let ids = Ast_util.IdSet.of_list ids in
-          Pretty_print_sail.pp_defs stdout (Specialize.slice_defs type_envs ast ids));
-      (if !(opt_print_ocaml)
-       then
-         let ast_ocaml = rewrite_ast_ocaml type_envs ast in
-         let out = match !opt_file_out with None -> "out" | Some s -> s in
-         Ocaml_backend.ocaml_compile out ast_ocaml ocaml_generator_info
-       else ());
-      (if !(opt_print_c)
-       then
-         let ast_c = rewrite_ast_c type_envs ast in
-         let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast_c type_envs) in
-         let ast_c, type_envs =
-           if !opt_specialize_c then
-             Specialize.(specialize' 2 int_specialization ast_c type_envs)
-           else
-             ast_c, type_envs
-         in
-         let output_chan = match !opt_file_out with Some f -> open_out (f ^ ".c") | None -> stdout in
-         Util.opt_warnings := true;
-         C_backend.compile_ast type_envs output_chan (!opt_includes_c) ast_c;
-         close_out output_chan
-       else ());
-      (if !(opt_print_ir)
-       then
-         let ast_c = rewrite_ast_c type_envs ast in
-         let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast_c type_envs) in
-         let ast_c, type_envs = Specialize.(specialize' 2 int_specialization_with_externs ast_c type_envs) in
-         let output_chan =
-           match !opt_file_out with
-           | Some f -> Util.opt_colors := false; open_out (f ^ ".ir.sail")
-           | None -> stdout
-         in
-         Util.opt_warnings := true;
-         let cdefs, _ = C_backend.jib_of_ast type_envs ast_c in
-         let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_cdef cdefs) in
-         output_string output_chan (str ^ "\n");
-         close_out output_chan
-       else ());
-      (if !(opt_print_cgen)
-       then Cgen_backend.output type_envs ast
-       else ());
-      (if !(opt_print_lem)
-       then
-         let mwords = !Pretty_print_lem.opt_mwords in
-         let type_envs, ast_lem = State.add_regstate_defs mwords type_envs ast in
-         let ast_lem = rewrite_ast_lem type_envs ast_lem in
-         output "" (Lem_out (!opt_libs_lem)) [out_name,type_envs,ast_lem]
-       else ());
-      (if !(opt_print_coq)
-       then
-         let type_envs, ast_coq = State.add_regstate_defs true type_envs ast in
-         let ast_coq = rewrite_ast_coq type_envs ast_coq in
-         output "" (Coq_out (!opt_libs_coq)) [out_name,type_envs,ast_coq]
-       else ());
-      (if !(opt_print_latex)
-       then
+      let out_name, ast, type_envs = load_files Type_check.initial_env !opt_file_arguments in
+      Util.opt_warnings := false; (* Don't show warnings during re-writing for now *)
+
+      begin match !opt_process_elf, !opt_file_out with
+      | Some elf, Some out ->
          begin
-           Util.opt_warnings := true;
-           let latex_dir = match !opt_file_out with None -> "sail_latex" | Some s -> s in
-           begin
-             try
-               if not (Sys.is_directory latex_dir) then begin
-                   prerr_endline ("Failure: latex output location exists and is not a directory: " ^ latex_dir);
-                   exit 1
-                 end
-             with Sys_error(_) -> Unix.mkdir latex_dir 0o755
-           end;
-           Latex.opt_directory := latex_dir;
-           let chan = open_out (Filename.concat latex_dir "commands.tex") in
-           output_string chan (Pretty_print_sail.to_string (Latex.defs ast));
-           close_out chan
+           let open Elf_loader in
+           let chan = open_out out in
+           load_elf ~writer:(write_file chan) elf;
+           output_string chan "elf_entry\n";
+           output_string chan (Big_int.to_string !opt_elf_entry ^ "\n");
+           close_out chan;
+           exit 0
          end
-       else ());
+      | Some _, None ->
+         prerr_endline "Failure: No output file given for processed ELF (option -o).";
+         exit 1
+      | None, _ -> ()
+      end;
+
+      if !opt_sanity then
+        ignore (rewrite_ast_check type_envs ast)
+      else ();
+
+      begin match !opt_slice with
+      | [] -> ()
+      | ids ->
+         let ids = List.map Ast_util.mk_id ids in
+         let ids = Ast_util.IdSet.of_list ids in
+         Pretty_print_sail.pp_defs stdout (Specialize.slice_defs type_envs ast ids)
+      end;
+
+      target !opt_target out_name ast type_envs;
+
+      if !Interactive.opt_interactive then
+        (Interactive.ast := ast; Interactive.env := type_envs)
+      else ();
 
       if !opt_memo_z3 then Constraint.save_digests () else ()
     end