val parse_check_and_desugar (pa: opt_prune_actions) (en: env) (mname fn: string)
    : ML (list Ast.decl & StaticAssertions.static_asserts & env)
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
val parse_check_and_desugar (pa: opt_prune_actions) (en: env) (mname fn: string)
    : ML (list Ast.decl & StaticAssertions.static_asserts & env)
let parse_check_and_desugar (pa: opt_prune_actions) (en: env) (mname 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
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.opt_prune_actions Main.env Prims.string Prims.list Ast.decl FStar.Pervasives.Native.option Ast.type_refinement GlobalEnv.global_env FStar.Pervasives.Native.Mktuple3 StaticAssertions.static_asserts Main.Mkenv Main.__proj__Mkenv__item__typesizes_env Main.__proj__Mkenv__item__translate_env FStar.Pervasives.Native.tuple3 Prims.unit Options.debug_print_string Ast.print_decls InlineSingletonRecords.simplify_prog Simplify.simplify_prog StaticAssertions.compute_static_asserts TypeSizes.size_of_decls BitFields.eliminate_decls FStar.IO.print_string JSON.prog_to_json FStar.Pervasives.Native.Mktuple2 Prims.bool Options.get_json FStar.Pervasives.Native.tuple2 Binding.bind_decls Main.__proj__Mkenv__item__binding_env Ast.prog Desugar.desugar Prims.op_Equality Main.prune_actions FStar.Pervasives.Native.Some Main.PruneActions Ast.prog_prune_actions Main.parse_prog FStar.Printf.sprintf
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 &
val parse_check_and_desugar (pa: opt_prune_actions) (en: env) (mname fn: string)
    : ML (list Ast.decl & StaticAssertions.static_asserts & env)
pa: Main.opt_prune_actions -> en: Main.env -> mname: Prims.string -> fn: Prims.string
  -> FStar.All.ML ((Prims.list Ast.decl * StaticAssertions.static_asserts) * Main.env)