anchor.diff:    s.buffer := !s.buffer @ [ read_chunk () ]
   
   let interactive_mode dsenv env =
  -    if Option.isSome !Options.codegen
  -    then (Util.print_warning "code-generation is not supported in interactive mode, ignoring the codegen flag");
  -
  -    let rec go (stack:stack) (curmod:option<modul>) dsenv env =
  -        begin match shift_chunk () with
  -            | Pop msg ->
  -              Parser.DesugarEnv.pop dsenv |> ignore;
  -              Tc.Env.pop env msg |> ignore;
  -              env.solver.refresh();
  -              Options.reset_options() |> ignore;
  -              let (curmod, dsenv, env), stack = match stack with
  -                | [] -> Util.print_error "too many pops"; exit 1
  -                | hd::tl -> hd, tl in
  -              go stack curmod dsenv env
  -
  -            | Push msg ->
  -              let stack = (curmod, dsenv, env)::stack in
  -              let dsenv = Parser.DesugarEnv.push dsenv in
  -              let env = Tc.Env.push env msg in
  -              go stack curmod dsenv env
  -
  -            | Code (text, (ok, fail)) ->
  -                let mark dsenv env =
  -                    let dsenv = Parser.DesugarEnv.mark dsenv in
  -                    let env = Tc.Env.mark env in
  -                    dsenv, env in
  -
  -                let reset_mark dsenv env =
  -                    let dsenv = Parser.DesugarEnv.reset_mark dsenv in
  -                    let env = Tc.Env.reset_mark env in
  -                    dsenv, env in
  -
  -                let commit_mark dsenv env =
  -                    let dsenv = Parser.DesugarEnv.commit_mark dsenv in
  -                    let env = Tc.Env.commit_mark env in
  -                    dsenv, env in
  -
  -                let fail curmod dsenv_mark env_mark =
  -                    Tc.Errors.report_all() |> ignore;
  -                    Tc.Errors.num_errs := 0;
  -                    Util.print1 "%s\n" fail;
  -                    let dsenv, env = reset_mark dsenv_mark env_mark in
  -                    go stack curmod dsenv env in
  -
  -              let dsenv_mark, env_mark = mark dsenv env in
  -              let res = tc_one_fragment curmod dsenv_mark env_mark text in
  -
  -              begin match res with
  -                | Some (curmod, dsenv, env) ->
  -                  if !Tc.Errors.num_errs=0
  -                  then begin
  -                     Util.print1 "\n%s\n" ok;
  -                     let dsenv, env = commit_mark dsenv env in
  -                     go stack curmod dsenv env
  +  if Option.isSome !Options.codegen then
  +    (Util.print_warning "code-generation is not supported in interactive mode, ignoring the codegen flag");
  +    let rec go (stack:stack) (curmod:option<modul>) dsenv env = begin
  +      match shift_chunk () with
  +      | Pop msg ->
  +          Parser.DesugarEnv.pop dsenv |> ignore;
  +          Tc.Env.pop env msg |> ignore;
  +          env.solver.refresh();
  +          Options.reset_options() |> ignore;
  +          let (curmod, dsenv, env), stack =
  +            match stack with
  +            | [] -> Util.print_error "too many pops"; exit 1
  +            | hd::tl -> hd, tl
  +          in
  +          go stack curmod dsenv env
  +      | Push msg ->
  +          let stack = (curmod, dsenv, env)::stack in
  +          let dsenv = Parser.DesugarEnv.push dsenv in
  +          let env = Tc.Env.push env msg in
  +          go stack curmod dsenv env
  +      | Code (text, (ok, fail)) ->
  +          let mark dsenv env =
  +            let dsenv = Parser.DesugarEnv.mark dsenv in
  +            let env = Tc.Env.mark env in
  +            dsenv, env in
  +          let reset_mark dsenv env =
  +            let dsenv = Parser.DesugarEnv.reset_mark dsenv in
  +            let env = Tc.Env.reset_mark env in
  +            dsenv, env in
  +          let commit_mark dsenv env =
  +            let dsenv = Parser.DesugarEnv.commit_mark dsenv in
  +            let env = Tc.Env.commit_mark env in
  +            dsenv, env in
  +          let fail curmod dsenv_mark env_mark =
  +            Tc.Errors.report_all() |> ignore;
  +            Tc.Errors.num_errs := 0;
  +            Util.print1 "%s\n" fail;
  +            let dsenv, env = reset_mark dsenv_mark env_mark in
  +            go stack curmod dsenv env in
  +          let dsenv_mark, env_mark = mark dsenv env in
  +          let res = tc_one_fragment curmod dsenv_mark env_mark text in begin
  +            match res with
  +            | Some (curmod, dsenv, env) ->
  +                if !Tc.Errors.num_errs = 0 then begin
  +                  Util.print1 "\n%s\n" ok;
  +                  let dsenv, env = commit_mark dsenv env in
  +                  go stack curmod dsenv env
                     end
  -                  else fail curmod dsenv_mark env_mark
  -
  -                | _ ->
  -                  fail curmod dsenv_mark env_mark
  -              end
  -        end in
  -
  +                else fail curmod dsenv_mark env_mark
  +            | _ -> fail curmod dsenv_mark env_mark
  +            end
  +    end in
       go [] None dsenv env
   
  -
  -let codegen fmods env=
  -    if !Options.codegen = Some "OCaml"
  -    || !Options.codegen = Some "FSharp"
  -    then begin
  -        let c, mllibs = Util.fold_map Extraction.ML.ExtractMod.extract (Extraction.ML.Env.mkContext env) fmods in
  -        let mllibs = List.flatten mllibs in
  -        let ext = if !Options.codegen = Some "FSharp" then ".fs" else ".ml" in
  -        let newDocs = List.collect Extraction.ML.Code.doc_of_mllib mllibs in
  -//                           else List.collect Extraction.OCaml.Code.doc_of_mllib mllibs, ".ml" in
  -        List.iter (fun (n,d) -> Util.write_file (Options.prependOutputDir (n^ext)) (FStar.Format.pretty 120 d)) newDocs
  +let codegen fmods env =
  +  if !Options.codegen = Some "OCaml" ||
  +     !Options.codegen = Some "FSharp"
  +  then begin
  +    let c, mllibs = Util.fold_map Extraction.ML.ExtractMod.extract (Extraction.ML.Env.mkContext env) fmods in
  +    let mllibs = List.flatten mllibs in
  +    let ext = if !Options.codegen = Some "FSharp" then ".fs" else ".ml" in
  +    let newDocs = List.collect Extraction.ML.Code.doc_of_mllib mllibs in
  +//else List.collect Extraction.OCaml.Code.doc_of_mllib mllibs, ".ml" in
  +    List.iter (fun (n,d) -> Util.write_file (Options.prependOutputDir (n^ext)) (FStar.Format.pretty 120 d)) newDocs
       end
   
   exception Found of string
  
positive.code: open FStar.Tc.Util
  open FStar.Ident
  
  let process_args () =
    let file_list = Util.mk_ref [] in
    let res = Getopt.parse_cmdline (Options.specs()) (fun i -> file_list := !file_list @ [i]) in
  
negative.code: 
  let has_prims_cache (l: list<string>) :bool = List.mem "Prims.cache" l
  
  
  open FStar.TypeChecker.Env
  let u_parse env fn =
    try
      match Parser.ParseIt.parse (Inl fn) with
      | Inl (Inl ast) ->
          Parser.ToSyntax.desugar_file env ast
      | Inl (Inr _) ->
          Util.print1_error "%s expected a module\n" fn;
          exit 1
      | Inr (msg, r) ->
          Util.print_string <| Print.format_error r msg;
          exit 1
      with e when (!Options.trace_error
                  && FStar.Syntax.Util.handleable e
                  && (FStar.Syntax.Util.handle_err false () e; false)) ->
                  failwith "Impossible"
          | e when (not !Options.trace_error && FStar.Syntax.Util.handleable e) ->
              FStar.Syntax.Util.handle_err false () e;
              exit 1
  
  let u_tc_prims () =
    let solver = if !Options.verify then SMTEncoding.Encode.solver else SMTEncoding.Encode.dummy in
    let env = FStar.TypeChecker.Env.initial_env
              FStar.TypeChecker.Tc.type_of
              solver
              Const.prims_lid in
    env.solver.init env;
    let p = Options.prims () in
    let dsenv, prims_mod = u_parse (Parser.Env.empty_env()) p in
    let prims_mod, env = FStar.TypeChecker.Tc.check_module env (List.hd prims_mod) in
    prims_mod, dsenv, env
  
  let test_universes filenames =
    try
      let prims_mod, dsenv, env = u_tc_prims() in
      let dsenv, mods, env =
        List.fold_left (fun (dsenv, fmods, env) fn ->
                       Util.print1 "Parsing file %s\n" fn;
                       let dsenv, mods = u_parse dsenv fn in
                       let _, env = TypeChecker.Tc.check_module env (List.hd mods) in
                       dsenv, mods@fmods, env) (dsenv, [], env) filenames in
      env.solver.finish();
      dsenv, mods, env
    with
    | Syntax.Syntax.Error(msg, r) when not (!Options.trace_error) ->
        Util.print_error (Util.format2 "%s\n%s\n" (Range.string_of_range r) msg);
        exit 1
  
  open FStar.Tc.Env
  let tc_prims () =
    let solver = if !Options.verify then ToSMT.Encode.solver else ToSMT.Encode.dummy in
    let env = Tc.Env.initial_env solver Const.prims_lid in
    env.solver.init env;
  
    let p = Options.prims () in
    let dsenv, prims_mod = Parser.Driver.parse_file (Parser.DesugarEnv.empty_env()) p in
    let prims_mod, env = Tc.Tc.check_module env (List.hd prims_mod) in
    prims_mod, dsenv, env
  
  let report_errors nopt =
    let errs =
      match nopt with
      | None -> Tc.Errors.get_err_count ()
      | Some n -> n in
    if errs > 0 then begin
      Util.print1_error "%s errors were reported (see above)\n" (string_of_int errs);
      exit 1
    end
  
  let report_universes_errors nopt =
    let errs =
      match nopt with
      | None -> TypeChecker.Errors.get_err_count ()
      | Some n -> n in
    if errs > 0 then begin
      Util.print1_error "%s errors were reported (see above)\n" (string_of_int errs);
      exit 1
    end
  
  let tc_one_file dsenv env fn =
    let dsenv, fmods = Parser.Driver.parse_file dsenv fn in
    let env, all_mods =
      fmods |> List.fold_left (fun (env, all_mods) m ->
                              let ms, env = Tc.Tc.check_module env m in
                              env, ms@all_mods) (env, []) in
    dsenv, env, List.rev all_mods
  
  let tc_one_fragment curmod dsenv env frag =
    try
      match Parser.Driver.parse_fragment curmod dsenv frag with
      | Parser.Driver.Empty ->
          Some (curmod, dsenv, env)
      | Parser.Driver.Modul (dsenv, modul) ->
          let env =
            match curmod with
            | None -> env
            | Some _ -> raise (Absyn.Syntax.Err("Interactive mode only supports a single module at the top-level")) in
          let modul, env = Tc.Tc.tc_partial_modul env modul in
          Some (Some modul, dsenv, env)
      | Parser.Driver.Decls (dsenv, decls) -> begin
          match curmod with
          | None -> Util.print_error "fragment without an enclosing module"; exit 1
          | Some modul ->
              let modul, env  = Tc.Tc.tc_more_partial_modul env modul decls in
              Some (Some modul, dsenv, env) end
      with
        | Absyn.Syntax.Error(msg, r) ->
            Tc.Errors.add_errors env [(msg,r)];
            None
        | Absyn.Syntax.Err msg ->
            Tc.Errors.add_errors env [(msg,Absyn.Syntax.dummyRange)];
            None
        | e -> raise e
  
  type input_chunks =
    | Push of string
    | Pop  of string
    | Code of string * (string * string)
  
  type stack_elt = (option<modul> * Parser.DesugarEnv.env * Tc.Env.env)
  type stack = list<stack_elt>
  
  let batch_mode_tc_no_prims dsenv env filenames admit_fsi =
    let all_mods, dsenv, env =
      filenames |> List.fold_left (fun (all_mods, dsenv, env) f ->
                                  Util.reset_gensym();
                                  let dsenv, env, ms = tc_one_file dsenv env f in
                                  all_mods@ms, dsenv, env)
                                  ([], dsenv, env) in
    if !Options.interactive && Tc.Errors.get_err_count () = 0
    then env.solver.refresh()
    else env.solver.finish();
    all_mods, dsenv, env
  
  let find_deps_if_needed files =
    if !Options.explicit_deps then
      files, []
    else
      let _, deps = Parser.Dep.collect files in
      let deps = List.rev deps in
      let deps =
        if basename (List.hd deps) = "prims.fst" then
          List.tl deps
        else begin
          Util.print_error "dependency analysis did not find prims.fst?!";
          exit 1
        end
      in
      let admit_fsi = ref [] in
      List.iter (fun d ->
                let d = basename d in
                if get_file_extension d = "fsti" then
                  admit_fsi := substring d 0 (String.length d - 5) :: !admit_fsi
                else if get_file_extension d = "fsi" then begin
                  admit_fsi := substring d 0 (String.length d - 4) :: !admit_fsi end
      ) deps;
      deps, !admit_fsi
  
  let batch_mode_tc filenames =
    let prims_mod, dsenv, env = tc_prims () in
    let filenames, admit_fsi = find_deps_if_needed filenames in
    let all_mods, dsenv, env = batch_mode_tc_no_prims dsenv env filenames admit_fsi in
    prims_mod @ all_mods, dsenv, env
  
  let finished_message fmods =
    if not !Options.silent then begin
      let msg =
        if !Options.verify then "Verifying"
        else if !Options.pretype then "Lax type-checked"
        else "Parsed and desugared" in
          fmods |> List.iter (fun m ->
                   let tag = if m.is_interface then "i'face" else "module" in
                   if Options.should_print_message m.name.str
                   then Util.print_string (Util.format3 "%s %s: %s\n" msg tag (Syntax.text_of_lid m.name)));
          print_string (Util.format1 "%s\n" (Util.colorize_bold "All verification conditions discharged successfully"))
      end
  
  type interactive_state = {
  