<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        *)
(************************************************************************)

(* $Id$ *)

open Global
open Pp
open Util
open Names
open Sign
open Evd
open Term
open Termops
open Reductionops
open Environ
open Type_errors
open Typeops
open Libnames
open Classops
open List
open Recordops 
open Evarutil
open Pretype_errors
open Rawterm
open Evarconv
open Pattern
open Dyn
open Vernacexpr

open Subtac_coercion
open Subtac_utils
open Coqlib
open Printer
open Subtac_errors
open Eterm

let require_library dirpath =
  let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
    Library.require_library [qualid] None

open Pp
open Ppconstr
open Decl_kinds
open Tacinterp
open Tacexpr

let start_proof_com env isevars sopt kind (bl,t) hook =
  let id = match sopt with
    | Some id ->
        (* We check existence here: it's a bit late at Qed time *)
        if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
          errorlabstrm "start_proof" (pr_id id ++ str " already exists");
        id
    | None ->
	next_global_ident_away false (id_of_string "Unnamed_thm")
 	  (Pfedit.get_all_proof_names ())
  in
  let evm, c, typ = 
    Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None 
  in
    if not (evm = Evd.empty) then 
      let stmt_id = Nameops.add_suffix id "_stmt" in
      let obls, c' = eterm_obligations env stmt_id !isevars evm 0 c (Some typ) in
	match Subtac_obligations.add_definition stmt_id c' typ obls with
	    Subtac_obligations.Defined cst -> Command.start_proof id kind (constant_value (Global.env()) cst) hook
	  | _ -> 
	      errorlabstrm "start_proof" 
		(str "The statement obligations could not be resolved automatically, " ++ spc () ++
		    str "write a statement definition first.")
    else
      let _ = Typeops.infer_type env c in
	Command.start_proof id kind c hook
      
let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()

let start_proof_and_print env isevars idopt k t hook =
  start_proof_com env isevars idopt k t hook;
  print_subgoals ()
	  
let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
  
let assumption_message id =
  Options.if_verbose message ((string_of_id id) ^ " is assumed")

let declare_assumption env isevars idl is_coe k bl c nl =
  if not (Pfedit.refining ()) then 
    let evm, c, typ = 
      Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None 
    in
      List.iter (Command.declare_one_assumption is_coe k c nl) idl
  else
    errorlabstrm "Command.Assumption"
	(str "Cannot declare an assumption while in proof editing mode.")

let vernac_assumption env isevars kind l nl =
  List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c nl) l


let subtac (loc, command) =
  check_required_library ["Coq";"Init";"Datatypes"];
  check_required_library ["Coq";"Init";"Specif"];
(*   check_required_library ["Coq";"Logic";"JMeq"]; *)
  require_library "Coq.Program.Wf";
  require_library "Coq.Program.Tactics";
  require_library "Coq.Logic.JMeq";
  let env = Global.env () in
  let isevars = ref (create_evar_defs Evd.empty) in
  try
  match command with
	VernacDefinition (defkind, (locid, id), expr, hook) -> 
	    (match expr with
		 ProveBody (bl, c) -> ignore(Subtac_pretyping.subtac_proof env isevars id bl c None)
	       | DefineBody (cbl, bl, _, c, tycon) -> 
		   ignore(Subtac_pretyping.subtac_proof env isevars id bl c tycon))
      | VernacFixpoint (l, b) -> 
	  let _ = trace (str "Building fixpoint") in
	    ignore(Subtac_command.build_recursive l b)

      | VernacStartTheoremProof (thkind, (locid, id), (bl, t), lettop, hook) ->
	  if not(Pfedit.refining ()) then
	    if lettop then
	      errorlabstrm "Subtac_command.StartProof"
		(str "Let declarations can only be used in proof editing mode");
	  if Lib.is_modtype () then
	    errorlabstrm "Subtac_command.StartProof"
	      (str "Proof editing mode not supported in module types");
	  start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook


      | VernacAssumption (stre,nl,l) -> 
	  vernac_assumption env isevars stre l nl<commit_msg>Fix define body bug<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        *)
(************************************************************************)

(* $Id$ *)

open Global
open Pp
open Util
open Names
open Sign
open Evd
open Term
open Termops
open Reductionops
open Environ
open Type_errors
open Typeops
open Libnames
open Classops
open List
open Recordops 
open Evarutil
open Pretype_errors
open Rawterm
open Evarconv
open Pattern
open Dyn
open Vernacexpr

open Subtac_coercion
open Subtac_utils
open Coqlib
open Printer
open Subtac_errors
open Eterm

let require_library dirpath =
  let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
    Library.require_library [qualid] None

open Pp
open Ppconstr
open Decl_kinds
open Tacinterp
open Tacexpr

let start_proof_com env isevars sopt kind (bl,t) hook =
  let id = match sopt with
    | Some id ->
        (* We check existence here: it's a bit late at Qed time *)
        if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
          errorlabstrm "start_proof" (pr_id id ++ str " already exists");
        id
    | None ->
	next_global_ident_away false (id_of_string "Unnamed_thm")
 	  (Pfedit.get_all_proof_names ())
  in
  let evm, c, typ = 
    Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None 
  in
    if not (evm = Evd.empty) then 
      let stmt_id = Nameops.add_suffix id "_stmt" in
      let obls, c' = eterm_obligations env stmt_id !isevars evm 0 c (Some typ) in
	match Subtac_obligations.add_definition stmt_id c' typ obls with
	    Subtac_obligations.Defined cst -> Command.start_proof id kind (constant_value (Global.env()) cst) hook
	  | _ -> 
	      errorlabstrm "start_proof" 
		(str "The statement obligations could not be resolved automatically, " ++ spc () ++
		    str "write a statement definition first.")
    else
      let _ = Typeops.infer_type env c in
	Command.start_proof id kind c hook
      
let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()

let start_proof_and_print env isevars idopt k t hook =
  start_proof_com env isevars idopt k t hook;
  print_subgoals ()
	  
let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
  
let assumption_message id =
  Options.if_verbose message ((string_of_id id) ^ " is assumed")

let declare_assumption env isevars idl is_coe k bl c nl =
  if not (Pfedit.refining ()) then 
    let evm, c, typ = 
      Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None 
    in
      List.iter (Command.declare_one_assumption is_coe k c nl) idl
  else
    errorlabstrm "Command.Assumption"
	(str "Cannot declare an assumption while in proof editing mode.")

let vernac_assumption env isevars kind l nl =
  List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c nl) l


let subtac (loc, command) =
  check_required_library ["Coq";"Init";"Datatypes"];
  check_required_library ["Coq";"Init";"Specif"];
(*   check_required_library ["Coq";"Logic";"JMeq"]; *)
  require_library "Coq.Program.Wf";
  require_library "Coq.Program.Tactics";
  require_library "Coq.Logic.JMeq";
  let env = Global.env () in
  let isevars = ref (create_evar_defs Evd.empty) in
  try
  match command with
	VernacDefinition (defkind, (locid, id), expr, hook) -> 
	    (match expr with
		 ProveBody (bl, c) -> ignore(Subtac_pretyping.subtac_proof env isevars id bl c None)
	       | DefineBody (cbl, bl, c, tycon) -> 
		   ignore(Subtac_pretyping.subtac_proof env isevars id bl c tycon))
      | VernacFixpoint (l, b) -> 
	  let _ = trace (str "Building fixpoint") in
	    ignore(Subtac_command.build_recursive l b)

      | VernacStartTheoremProof (thkind, (locid, id), (bl, t), lettop, hook) ->
	  if not(Pfedit.refining ()) then
	    if lettop then
	      errorlabstrm "Subtac_command.StartProof"
		(str "Let declarations can only be used in proof editing mode");
	  if Lib.is_modtype () then
	    errorlabstrm "Subtac_command.StartProof"
	      (str "Proof editing mode not supported in module types");
	  start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook


      | VernacAssumption (stre,nl,l) -> 
	  vernac_assumption env isevars stre l nl
{'fraction_non_alphanumeric': 0.12973714768288822, 'fraction_numerical': 0.0006333790773778106, 'mean_word_length': 3.748872180451128, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 29, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, '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': '3676887', 'n_tokens_mistral': 3295, 'n_tokens_neox': 3128, 'n_words': 980}