<commit_before>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open Util
open Names
open Nameops
open Sign
open Term
open Declarations
open Entries
open Environ
open Evd
open Typing
open Refiner
open Tacexpr
open Proof_type
open Lib
open Safe_typing

let refining = Proof_global.there_are_pending_proofs
let check_no_pending_proofs = Proof_global.check_no_pending_proof

let get_current_proof_name = Proof_global.get_current_proof_name
let get_all_proof_names = Proof_global.get_all_proof_names

type lemma_possible_guards = Proof_global.lemma_possible_guards

let delete_proof = Proof_global.discard
let delete_current_proof = Proof_global.discard_current
let delete_all_proofs = Proof_global.discard_all

let undo n = 
  let p = Proof_global.give_me_the_proof () in
  for i = 1 to n do
    Proof.undo p
  done

let current_proof_depth () =
  try
    let p = Proof_global.give_me_the_proof () in
    Proof.V82.depth p
  with Proof_global.NoCurrentProof -> -1

(* [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d
   is the depth of the focus stack). *)
let undo_todepth n =
  try
    undo ((current_proof_depth ()) - n )
  with Proof_global.NoCurrentProof  when n=0 -> ()

let set_undo _ = ()
let get_undo _ = None


let start_proof id str hyps c ?init_tac ?compute_guard hook = 
  let goals = [ (Global.env_of_context hyps , c) ] in
  let init_tac = Option.map Proofview.V82.tactic init_tac in
  Proof_global.start_proof id str goals ?compute_guard hook;
  Option.iter Proof_global.run_tactic init_tac

let restart_proof () =
  let p = Proof_global.give_me_the_proof () in
  try while true do
    Proof.undo p
  done with Proof.EmptyUndoStack -> ()

let resume_last_proof () = Proof_global.resume_last ()
let resume_proof (_,id) = Proof_global.resume id
let suspend_proof ()  =  Proof_global.suspend ()

let cook_proof hook =
  let prf = Proof_global.give_me_the_proof () in
  hook prf;
  match Proof_global.close_proof () with
  | (i,([e],cg,str,h)) -> (i,(e,cg,str,h))
  | _ -> Util.anomaly "Pfedit.cook_proof: more than one proof term."

let xml_cook_proof = ref (fun _ -> ())
let set_xml_cook_proof f = xml_cook_proof := f

let get_pftreestate () =
  Proof_global.give_me_the_proof ()

let set_end_tac tac =
  let tac = Proofview.V82.tactic tac in
  Proof_global.set_endline_tactic tac

let get_goal_context i =
  try
    let p = Proof_global.give_me_the_proof () in
    let { it=goals ; sigma = sigma } = Proof.V82.subgoals p in
    let goal = List.nth goals (i-1) in
    (sigma, Refiner.pf_env { it=goal ; sigma=sigma })
  with Proof_global.NoCurrentProof -> Util.error "No focused proof."

let get_current_goal_context () = get_goal_context 1

let current_proof_statement () =
  match Proof_global.V82.get_current_initial_conclusions () with
    | (id,([concl],strength,hook)) -> id,strength,concl,hook
    | _ -> Util.anomaly "Pfedit.current_proof_statement: more than one statement"

let solve_nth ?(with_end_tac=false) gi tac = 
  try 
    let tac = Proofview.V82.tactic tac in
    let tac = if with_end_tac then 
                Proof_global.with_end_tac tac
              else
		tac
    in<commit_msg>Fix: Pfedit.get_current_goal_context when no goal is focused.<commit_after>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open Util
open Names
open Nameops
open Sign
open Term
open Declarations
open Entries
open Environ
open Evd
open Typing
open Refiner
open Tacexpr
open Proof_type
open Lib
open Safe_typing

let refining = Proof_global.there_are_pending_proofs
let check_no_pending_proofs = Proof_global.check_no_pending_proof

let get_current_proof_name = Proof_global.get_current_proof_name
let get_all_proof_names = Proof_global.get_all_proof_names

type lemma_possible_guards = Proof_global.lemma_possible_guards

let delete_proof = Proof_global.discard
let delete_current_proof = Proof_global.discard_current
let delete_all_proofs = Proof_global.discard_all

let undo n = 
  let p = Proof_global.give_me_the_proof () in
  for i = 1 to n do
    Proof.undo p
  done

let current_proof_depth () =
  try
    let p = Proof_global.give_me_the_proof () in
    Proof.V82.depth p
  with Proof_global.NoCurrentProof -> -1

(* [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d
   is the depth of the focus stack). *)
let undo_todepth n =
  try
    undo ((current_proof_depth ()) - n )
  with Proof_global.NoCurrentProof  when n=0 -> ()

let set_undo _ = ()
let get_undo _ = None


let start_proof id str hyps c ?init_tac ?compute_guard hook = 
  let goals = [ (Global.env_of_context hyps , c) ] in
  let init_tac = Option.map Proofview.V82.tactic init_tac in
  Proof_global.start_proof id str goals ?compute_guard hook;
  Option.iter Proof_global.run_tactic init_tac

let restart_proof () =
  let p = Proof_global.give_me_the_proof () in
  try while true do
    Proof.undo p
  done with Proof.EmptyUndoStack -> ()

let resume_last_proof () = Proof_global.resume_last ()
let resume_proof (_,id) = Proof_global.resume id
let suspend_proof ()  =  Proof_global.suspend ()

let cook_proof hook =
  let prf = Proof_global.give_me_the_proof () in
  hook prf;
  match Proof_global.close_proof () with
  | (i,([e],cg,str,h)) -> (i,(e,cg,str,h))
  | _ -> Util.anomaly "Pfedit.cook_proof: more than one proof term."

let xml_cook_proof = ref (fun _ -> ())
let set_xml_cook_proof f = xml_cook_proof := f

let get_pftreestate () =
  Proof_global.give_me_the_proof ()

let set_end_tac tac =
  let tac = Proofview.V82.tactic tac in
  Proof_global.set_endline_tactic tac

exception NoSuchGoal
let get_nth_V82_goal i =
  let p = Proof_global.give_me_the_proof () in
  let { it=goals ; sigma = sigma } = Proof.V82.subgoals p in
  try
    { it=(List.nth goals (i-1)) ; sigma=sigma }
  with Failure _ -> raise NoSuchGoal
    
let get_goal_context_gen i =
  try
    let { it=goal ; sigma=sigma } =  get_nth_V82_goal i in
    (sigma, Refiner.pf_env { it=goal ; sigma=sigma })
  with Proof_global.NoCurrentProof -> Util.error "No focused proof."

let get_goal_context i =
  try get_goal_context_gen i
  with NoSuchGoal -> Util.error "No such goal."

let get_current_goal_context () =
  try get_goal_context_gen 1
  with NoSuchGoal ->
    (* spiwack: returning empty evar_map, since if there is no goal, under focus,
        there is no accessible evar either *)
    (Evd.empty, Global.env ())

let current_proof_statement () =
  match Proof_global.V82.get_current_initial_conclusions () with
    | (id,([concl],strength,hook)) -> id,strength,concl,hook
    | _ -> Util.anomaly "Pfedit.current_proof_statement: more than one statement"

let solve_nth ?(with_end_tac=false) gi tac = 
  try 
    let tac = Proofview.V82.tactic tac in
    let tac = if with_end_tac then 
                Proof_global.with_end_tac tac
              else
		tac
    in
{'fraction_non_alphanumeric': 0.13481118700863515, 'fraction_numerical': 0.005413068694419384, 'mean_word_length': 3.9020846493998738, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 24, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 6}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '867711', 'n_tokens_mistral': 2783, 'n_tokens_neox': 2579, 'n_words': 698}