val left (x: either 'a 'b) : ML 'a
let left (x:either 'a 'b)
  : ML 'a
  = match x with
    | Inl x -> x
    | _ -> failwith "Expected left"
val left (x: either 'a 'b) : ML 'a
let left (x: either 'a 'b) : ML 'a =
match x with
| Inl x -> x
| _ -> failwith "Expected left"
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
Ast.either FStar.All.failwith
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)
val left (x: either 'a 'b) : ML 'a
x: Ast.either 'a 'b -> FStar.All.ML 'a