val emit_fstar_code_for_interpreter
      (en: env)
      (modul: string)
      (tds: list T.decl)
      (itds: list InterpreterTarget.decl)
      (all_modules: list string)
    : ML unit
let emit_fstar_code_for_interpreter (en:env)
                                    (modul:string)
                                    (tds:list T.decl)
                                    (itds:list InterpreterTarget.decl)
                                    (all_modules:list string)
  : ML unit
  = let _, en = en.translate_env in
    
    let impl, iface =
        InterpreterTarget.print_decls en modul itds
    in

    let has_external_types = has_output_types tds || has_extern_types tds in

    if has_external_types
    then begin
      let external_types_fsti_file =
        open_write_file
          (Printf.sprintf "%s/%s.ExternalTypes.fsti" (Options.get_output_dir ()) modul) in
      FStar.IO.write_string external_types_fsti_file (Target.print_external_types_fstar_interpreter modul tds);
      FStar.IO.close_write_file external_types_fsti_file
    end;

    let has_external_api =
      has_out_exprs tds ||
      has_extern_types tds || // FIXME: I added this to fix discrepancy with GenMakefile, does this make sense?
      has_extern_functions tds in

    if has_external_api
    then begin
      let external_api_fsti_file =
        open_write_file
          (Printf.sprintf "%s/%s.ExternalAPI.fsti" (Options.get_output_dir ()) modul) in
      FStar.IO.write_string external_api_fsti_file (Target.print_external_api_fstar_interpreter modul tds);
      FStar.IO.close_write_file external_api_fsti_file
    end;
 
    let maybe_open_external_api =
      if has_external_api
      then Printf.sprintf "open %s.ExternalAPI" modul
      else ""
    in
 
    let module_prefix = 
       FStar.Printf.sprintf "module %s\n\
                             open EverParse3d.Prelude\n\
                             open EverParse3d.Actions.All\n\
                             open EverParse3d.Interpreter\n\
                             %s\n\
                             module T = FStar.Tactics\n\
                             module A = EverParse3d.Actions.All\n\
                             module P = EverParse3d.Prelude\n\
                             #push-options \"--fuel 0 --ifuel 0\"\n\
                             #push-options \"--using_facts_from 'Prims FStar.UInt FStar.UInt8 \
                                                                 FStar.UInt16 FStar.UInt32 FStar.UInt64 \
                                                                 EverParse3d FStar.Int.Cast %s'\"\n"
                             modul maybe_open_external_api (all_modules |> String.concat " ")
    in

    let fst_file =
      open_write_file
        (Printf.sprintf "%s/%s.fst"
          (Options.get_output_dir())
          modul) in
    FStar.IO.write_string fst_file module_prefix;
    FStar.IO.write_string fst_file impl;    
    FStar.IO.close_write_file fst_file;
                             
    let fsti_file =
      open_write_file
        (Printf.sprintf "%s/%s.fsti"
          (Options.get_output_dir())
          modul) in
    FStar.IO.write_string fsti_file module_prefix;
    FStar.IO.write_string fsti_file iface;
    FStar.IO.close_write_file fsti_file;

    ()
val emit_fstar_code_for_interpreter
      (en: env)
      (modul: string)
      (tds: list T.decl)
      (itds: list InterpreterTarget.decl)
      (all_modules: list string)
    : ML unit
let emit_fstar_code_for_interpreter
      (en: env)
      (modul: string)
      (tds: list T.decl)
      (itds: list InterpreterTarget.decl)
      (all_modules: list string)
    : ML unit =
let _, en = en.translate_env in
let impl, iface = InterpreterTarget.print_decls en modul itds in
let has_external_types = has_output_types tds || has_extern_types tds in
if has_external_types
then
  (let external_types_fsti_file =
      open_write_file (Printf.sprintf "%s/%s.ExternalTypes.fsti" (Options.get_output_dir ()) modul)
    in
    FStar.IO.write_string external_types_fsti_file
      (Target.print_external_types_fstar_interpreter modul tds);
    FStar.IO.close_write_file external_types_fsti_file);
let has_external_api = has_out_exprs tds || has_extern_types tds || has_extern_functions tds in
if has_external_api
then
  (let external_api_fsti_file =
      open_write_file (Printf.sprintf "%s/%s.ExternalAPI.fsti" (Options.get_output_dir ()) modul)
    in
    FStar.IO.write_string external_api_fsti_file
      (Target.print_external_api_fstar_interpreter modul tds);
    FStar.IO.close_write_file external_api_fsti_file);
let maybe_open_external_api =
  if has_external_api then Printf.sprintf "open %s.ExternalAPI" modul else ""
in
let module_prefix =
  FStar.Printf.sprintf "module %s\nopen EverParse3d.Prelude\nopen EverParse3d.Actions.All\nopen EverParse3d.Interpreter\n%s\nmodule T = FStar.Tactics\nmodule A = EverParse3d.Actions.All\nmodule P = EverParse3d.Prelude\n#push-options \"--fuel 0 --ifuel 0\"\n#push-options \"--using_facts_from 'Prims FStar.UInt FStar.UInt8 FStar.UInt16 FStar.UInt32 FStar.UInt64 EverParse3d FStar.Int.Cast %s'\"\n"
    modul
    maybe_open_external_api
    (all_modules |> String.concat " ")
in
let fst_file = open_write_file (Printf.sprintf "%s/%s.fst" (Options.get_output_dir ()) modul) in
FStar.IO.write_string fst_file module_prefix;
FStar.IO.write_string fst_file impl;
FStar.IO.close_write_file fst_file;
let fsti_file = open_write_file (Printf.sprintf "%s/%s.fsti" (Options.get_output_dir ()) modul) in
FStar.IO.write_string fsti_file module_prefix;
FStar.IO.write_string fsti_file iface;
FStar.IO.close_write_file fsti_file;
()
Main.fst.checked
Z3TestGen.fst.checked Z3.fsti.checked TypeSizes.fsti.checked TranslateForInterpreter.fsti.checked Target.fsti.checked StaticAssertions.fst.checked Simplify.fsti.checked prims.fst.checked ParserDriver.fsti.checked OS.fsti.checked Options.fsti.checked JSON.fsti.checked InterpreterTarget.fsti.checked InlineSingletonRecords.fst.checked HashingOptions.fst.checked GenMakefile.fsti.checked FStar.String.fsti.checked FStar.ST.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked Desugar.fst.checked Deps.fsti.checked Config.fst.checked BitFields.fst.checked Binding.fsti.checked Batch.fsti.checked Ast.fst.checked
Main.fst
Main.env Prims.string Prims.list Target.decl InterpreterTarget.decl TranslateForInterpreter.translate_env InterpreterTarget.env Prims.unit FStar.IO.close_write_file FStar.IO.write_string FStar.IO.fd_write Main.open_write_file FStar.Printf.sprintf Options.get_output_dir FStar.All.op_Bar_Greater FStar.String.concat Prims.bool Target.print_external_api_fstar_interpreter Prims.op_BarBar Main.has_out_exprs Main.has_extern_types Main.has_extern_functions Target.print_external_types_fstar_interpreter Main.has_output_types FStar.Pervasives.Native.tuple2 InterpreterTarget.print_decls Main.__proj__Mkenv__item__translate_env
module Main
open FStar.IO
open FStar.All
open Ast
open ParserDriver
module T = Target
open FStar.ST
#push-options "--z3rlimit_factor 2"

let open_write_file (s:string) : ML FStar.IO.fd_write =
  FStar.IO.print_string (FStar.Printf.sprintf "Writing file %s\n" s);
  FStar.IO.open_write_file s

let parse_prog (fn:string) : ML prog =
  let decls, type_refinement_opt = ParserDriver.parse fn in
  if decls
     |> List.tryFind is_entrypoint_or_export
     |> Some?
  then decls, type_refinement_opt
  else raise (Error (Printf.sprintf "File %s does not have an entry point or an exported definition, exiting\n" fn))

noeq
type env = {
  binding_env : Binding.global_env;
  typesizes_env : TypeSizes.size_env;
  translate_env : (TranslateForInterpreter.translate_env & InterpreterTarget.env);
}

let initial_env () : ML env = {
  binding_env = Binding.initial_global_env ();
  typesizes_env = TypeSizes.initial_senv ();
  translate_env = 
    (TranslateForInterpreter.initial_translate_env(), InterpreterTarget.create_env());
}

let left (x:either 'a 'b)
  : ML 'a
  = match x with
    | Inl x -> x
    | _ -> failwith "Expected left"

let right (x:either 'a 'b)
  : ML 'b
  = match x with
    | Inr x -> x
    | _ -> failwith "Expected right"

type prune_actions = | PruneActions
type opt_prune_actions = option prune_actions

let parse_check_and_desugar (pa: opt_prune_actions) (en:env) (mname:string) (fn:string)
  : ML (list Ast.decl &
        StaticAssertions.static_asserts &
        env) =
  Options.debug_print_string (FStar.Printf.sprintf "Processing file: %s\nModule name: %s\n" fn mname);
  let decls, refinement =
    let p = parse_prog fn in
    if pa = Some PruneActions
    then prog_prune_actions p
    else p
  in

  Options.debug_print_string "=============After parsing=============\n";
  Options.debug_print_string (print_decls decls);
  Options.debug_print_string "\n";

  let decls, refinement = Desugar.desugar en.binding_env mname (decls, refinement) in

  Options.debug_print_string "=============After desugaring=============\n";
  Options.debug_print_string (print_decls decls);
  Options.debug_print_string "\n";

  let decls, benv = Binding.bind_decls en.binding_env decls in

  Options.debug_print_string "=============After binding=============\n";
  Options.debug_print_string (print_decls decls);
  Options.debug_print_string "\n";

  if Options.get_json()
  then (
    IO.print_string (JSON.prog_to_json (decls, refinement));
    IO.print_string "\n"
  );
  
  let decls = BitFields.eliminate_decls benv decls in
  
  Options.debug_print_string "=============After bitflds=============\n";
  Options.debug_print_string (print_decls decls);
  Options.debug_print_string "\n";
  
  let decls = TypeSizes.size_of_decls benv en.typesizes_env decls in

  Options.debug_print_string "=============Finished typesizes pass=============\n";

  let static_asserts = StaticAssertions.compute_static_asserts benv en.typesizes_env refinement in

  Options.debug_print_string "=============Finished static asserts pass=============\n";

  let decls = Simplify.simplify_prog benv en.typesizes_env decls in
  
  Options.debug_print_string "=============After simplify============\n";
  Options.debug_print_string (print_decls decls);
  Options.debug_print_string "\n";

  let decls = InlineSingletonRecords.simplify_prog decls in
  
  Options.debug_print_string "=============After inline singletons============\n";
  Options.debug_print_string (print_decls decls);
  Options.debug_print_string "\n";

  let en = {
    en with 
      binding_env = benv
  } in
  decls,
  static_asserts,
  en
  
let translate_module (pa: opt_prune_actions) (en:env) (mname:string) (fn:string)
  : ML (list Target.decl &
        option (list InterpreterTarget.decl) &
        StaticAssertions.static_asserts &
        env) =

  let decls, static_asserts, en = 
      parse_check_and_desugar pa en mname fn
  in      
      
  let t_decls, i_decls, tenv = 
      let env, env' = en.translate_env in
      let decls, env =
        TranslateForInterpreter.translate_decls en.binding_env en.typesizes_env env decls
      in
      let tds = InterpreterTarget.translate_decls env' decls in
      decls, Some tds, (env, env')
  in
  let en = { en with translate_env = tenv } in
  t_decls,
  i_decls,
  static_asserts,
  en

let has_output_types (t_decls:list Target.decl) : bool =
  List.Tot.existsb (fun (d, _) -> Target.Output_type? d) t_decls

let has_out_exprs (t_decls:list Target.decl) : bool =
  List.Tot.existsb (fun (d, _) -> Target.Output_type_expr? d) t_decls

let has_extern_types (t_decls:list Target.decl) : bool =
  List.Tot.existsb (fun (d, _) -> Target.Extern_type? d) t_decls

let has_extern_functions (t_decls:list Target.decl) : bool =
  List.Tot.existsb (fun (d, _) -> Target.Extern_fn? d) t_decls

let emit_fstar_code_for_interpreter (en:env)
                                    (modul:string)
                                    (tds:list T.decl)
                                    (itds:list InterpreterTarget.decl)
                                    (all_modules:list string)
val emit_fstar_code_for_interpreter
      (en: env)
      (modul: string)
      (tds: list T.decl)
      (itds: list InterpreterTarget.decl)
      (all_modules: list string)
    : ML unit

    en: Main.env ->
    modul: Prims.string ->
    tds: Prims.list Target.decl ->
    itds: Prims.list InterpreterTarget.decl ->
    all_modules: Prims.list Prims.string
  -> FStar.All.ML Prims.unit