val parse_prog (fn: string) : ML prog
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))
val parse_prog (fn: string) : ML prog
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
      ))
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
Prims.string Prims.list Ast.decl FStar.Pervasives.Native.option Ast.type_refinement FStar.Pervasives.Native.Mktuple2 Ast.prog Prims.bool FStar.Exn.raise Ast.Error FStar.Printf.sprintf FStar.All.op_Bar_Greater FStar.Pervasives.Native.uu___is_Some FStar.List.tryFind Ast.is_entrypoint_or_export ParserDriver.parse
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
val parse_prog (fn: string) : ML prog
fn: Prims.string -> FStar.All.ML Ast.prog