<commit_before>(*
   Copyright 2008-2016  <NAME> and Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
#light "off"

module FStar.Interactive.Ide
open FStar.ST
open FStar.Exn
open FStar.All
open FStar
open FStar.Range
open FStar.Util
open FStar.Getopt
open FStar.Ident
open FStar.Errors

open FStar.Universal
open FStar.TypeChecker.Env
open FStar.TypeChecker.Common
open FStar.Interactive

module SS = FStar.Syntax.Syntax
module DsEnv = FStar.ToSyntax.Env
module TcEnv = FStar.TypeChecker.Env
module CTable = FStar.Interactive.CompletionTable

exception ExitREPL of int

// A custom version of the function that's in FStar.Universal.fs just for the
// sake of the interactive mode
let tc_one_file (remaining:list<string>) (uenv:uenv) = //:((string option * string) * uenv * modul option * string list) =
  let dsenv, env = uenv in
  let (intf, impl), dsenv, env, remaining =
    match remaining with
    | intf :: impl :: remaining when needs_interleaving intf impl ->
      let _, dsenv, env = tc_one_file dsenv env (Some intf) impl in
      (Some intf, impl), dsenv, env, remaining
    | intf_or_impl :: remaining ->
      let _, dsenv, env = tc_one_file dsenv env None intf_or_impl in
      (None, intf_or_impl), dsenv, env, remaining
    | [] -> failwith "Impossible"
  in
  (intf, impl), (dsenv, env), remaining

type env_t = DsEnv.env * TcEnv.env

// Note: many of these functions are passing env around just for the sake of
// providing a link to the solver (to avoid a cross-project dependency). They're
// not actually doing anything useful with the environment you're passing it (e.g.
// pop).

let push env msg =
  let res = push_context env msg in
  Options.push();
  res

let pop env msg =
  pop_context (snd env) msg;
  Options.pop()

type push_kind = | SyntaxCheck | LaxCheck | FullCheck

let set_check_kind (dsenv, tcenv) check_kind =
  let tcenv = { tcenv with lax = (check_kind = LaxCheck) } in
  let dsenv = DsEnv.set_syntax_only dsenv (check_kind = SyntaxCheck) in
  (dsenv, tcenv)

let cleanup (dsenv, env) =
  TcEnv.cleanup_interactive env

let with_captured_errors' env f =
  let tcenv = snd env in<commit_msg>ide: (#912/update_deps) (1/8) Split tc_one_file into two phases<commit_after>(*
   Copyright 2008-2016  <NAME> and Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
#light "off"

module FStar.Interactive.Ide
open FStar.ST
open FStar.Exn
open FStar.All
open FStar
open FStar.Range
open FStar.Util
open FStar.Getopt
open FStar.Ident
open FStar.Errors

open FStar.Universal
open FStar.TypeChecker.Env
open FStar.TypeChecker.Common
open FStar.Interactive

module SS = FStar.Syntax.Syntax
module DsEnv = FStar.ToSyntax.Env
module TcEnv = FStar.TypeChecker.Env
module CTable = FStar.Interactive.CompletionTable

exception ExitREPL of int

type load_dependency_task =
  | LDInterleaved of string (* interface *) * string (* impl *)
  | LDSingle of string (* interface or implementation *)
  | LDInterfaceOfCurrentFile of string (* interface *)

type env_t = DsEnv.env * TcEnv.env

(** Like ``tc_one_file``, but only return the new environment **)
let tc_one ((dsenv, tcenv): env_t) intf_opt mod =
  let _, dsenv, tcenv = tc_one_file dsenv tcenv intf_opt mod in
  (dsenv, tcenv)

(** Load the file or files described by `task` **)
let load_one (env: env_t) (task: load_dependency_task) =
  match task with
  | LDInterleaved (intf, impl) -> tc_one env (Some intf) impl
  | LDSingle intf_or_impl -> tc_one env None intf_or_impl
  | LDInterfaceOfCurrentFile intf -> Universal.load_interface_decls env intf

(** Build a list of load tasks from a list of dependencies **)
let rec tasks_of_deps (deps: list string) =
  match deps with
  | intf :: impl :: deps' when needs_interleaving intf impl ->
    LDInterleaved (intf, impl) :: tasks_of_deps deps'
  | intf_or_impl :: deps' ->
    LDSingle intf_or_impl :: tasks_of_deps deps'
  | [] -> []

// Note: many of these functions are passing env around just for the sake of
// providing a link to the solver (to avoid a cross-project dependency). They're
// not actually doing anything useful with the environment you're passing it (e.g.
// pop).

let push env msg =
  let res = push_context env msg in
  Options.push();
  res

let pop env msg =
  pop_context (snd env) msg;
  Options.pop()

type push_kind = | SyntaxCheck | LaxCheck | FullCheck

let set_check_kind (dsenv, tcenv) check_kind =
  let tcenv = { tcenv with lax = (check_kind = LaxCheck) } in
  let dsenv = DsEnv.set_syntax_only dsenv (check_kind = SyntaxCheck) in
  (dsenv, tcenv)

let cleanup (dsenv, env) =
  TcEnv.cleanup_interactive env

let with_captured_errors' env f =
  let tcenv = snd env in
{'fraction_non_alphanumeric': 0.08330398027474463, 'fraction_numerical': 0.0051074321944346605, 'mean_word_length': 3.8455631399317407, 'pattern_counts': {'":': 0, '<': 6, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5404624', 'n_tokens_mistral': 1842, 'n_tokens_neox': 1826, 'n_words': 688}