<commit_before>(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id$ *)

open Pp
open Util
open Stamps
open Names
open Sign
open Term
open Inductive
open Reduction
open Environ
open Declare
open Evd
open Pfedit
open Tacred
open Tacmach
open Proof_trees
open Proof_type
open Logic
open Evar_refiner
open Clenv
open Tacticals
open Hipattern
open Coqlib

exception Bound

(*********************************************)
(*                 Tactics                   *)
(*********************************************)

(****************************************)
(* General functions                    *)
(****************************************)

let get_pairs_from_bindings = 
  let pair_from_binding = function  
    | [(Bindings binds)] -> binds
    | _                  -> error "not a binding list!"
  in 
  List.map pair_from_binding

let rec string_head_bound x = match kind_of_term x with
  | IsConst _ -> string_of_id (basename (path_of_const x))
  | IsMutInd (ind_sp,args) -> 
      let mispec = Global.lookup_mind_specif (ind_sp,args) in 
      string_of_id (mis_typename mispec)
  | IsMutConstruct ((ind_sp,i),args) ->
       let mispec = Global.lookup_mind_specif (ind_sp,args) in 
       string_of_id (mis_consnames mispec).(i-1)
  | IsVar id -> string_of_id id
  | _ -> raise Bound

let string_head c = 
  try string_head_bound c with Bound -> error "Bound head variable"


let rec head_constr_bound t l =
  let t = strip_outer_cast(collapse_appl t) in
  match kind_of_term t with
    | IsProd (_,_,c2)  -> head_constr_bound c2 l 
    | IsLetIn (_,_,_,c2) -> head_constr_bound c2 l 
    | IsApp (f,args)  -> 
	head_constr_bound f (Array.fold_right (fun a l -> a::l) args l)
    | IsConst _        -> t::l
    | IsMutInd _       -> t::l
    | IsMutConstruct _ -> t::l
    | IsVar _          -> t::l
    | _                -> raise Bound

let head_constr c = 
  try head_constr_bound c [] with Bound -> error "Bound head variable"

let bad_tactic_args s l =
  raise (RefinerError (BadTacticArgs (s,l)))

(******************************************)
(*           Primitive tactics            *)
(******************************************)

let introduction    = Tacmach.introduction 
let intro_replacing = Tacmach.intro_replacing 
let refine          = Tacmach.refine
let convert_concl   = Tacmach.convert_concl
let convert_hyp     = Tacmach.convert_hyp
let thin            = Tacmach.thin 
let move_hyp        = Tacmach.move_hyp 

let mutual_fix   = Tacmach.mutual_fix
let fix f n      = mutual_fix [f] [n] []

let fix_noname n =  
  let id = Pfedit.get_current_proof_name () in
  fix id n

let dyn_mutual_fix argsl gl = 
  match argsl with 
    | [Integer n]                          -> fix_noname n gl
    | [Identifier id;Integer n]            -> fix id n gl
    | ((Identifier id)::(Integer n)::lfix) -> 
	let rec decomp lid ln lar = function
          | (Fixexp (id,n,ar)::rest) -> 
	      decomp (id::lid) (n::ln) (ar::lar) rest
          | [] -> (List.rev lid,List.rev ln,List.rev lar)
	  | _  -> bad_tactic_args "mutual_fix" argsl
	in
	let (lid,ln,lar) = decomp [] [] [] lfix in
	mutual_fix (id::lid) (n::ln) (List.map (pf_interp_constr gl) lar) gl
    | l -> bad_tactic_args "mutual_fix" l 

let mutual_cofix = Tacmach.mutual_cofix
let cofix f      =  mutual_cofix [f] []

let cofix_noname n =  
  let id = Pfedit.get_current_proof_name () in
  cofix id n

let dyn_mutual_cofix argsl gl = 
  match argsl with
    | []                       -> cofix_noname gl
    | [(Identifier id)]        -> cofix id gl
    | ((Identifier id)::lcofix) -> 
	let rec decomp lid lar = function 
          | (Cofixexp (id,ar)::rest) -> 
              decomp (id::lid) (ar::lar) rest
          | [] -> (List.rev lid,List.rev lar)
	  |  _ -> bad_tactic_args "mutual_cofix" argsl
	in
	let (lid,lar) = decomp [] [] lcofix in
        mutual_cofix (id::lid) (List.map (pf_interp_constr gl) lar) gl
   | l -> bad_tactic_args "mutual_cofix" l 


(**************************************************************)
(*          Reduction and conversion tactics                  *)
(**************************************************************)

type 'a tactic_reduction = env -> enamed_declarations -> constr -> constr

(* The following two tactics apply an arbitrary
   reduction function either to the conclusion or to a 
   certain hypothesis *)

let reduct_in_concl redfun gl = 
  convert_concl (pf_reduce redfun gl (pf_concl gl)) gl
    
let reduct_in_hyp redfun id gl  = 
  let ty = pf_get_hyp_typ gl id in
  let redfun' = under_casts (pf_reduce redfun gl) in
  convert_hyp id (redfun' ty) gl
    
let reduct_option redfun = function
  | Some id -> reduct_in_hyp   redfun id 
  | None    -> reduct_in_concl redfun 

(* The following tactic determines whether the reduction
   function has to be applied to the conclusion or
   to the hypotheses. *) 

let in_combinator tac1 tac2 = function 
  | [] -> tac1 
  | x  -> (tclMAP tac2 x)
	
let redin_combinator redfun = function 
  | [] ->  reduct_in_concl redfun 
  | x  -> (tclMAP (reduct_in_hyp redfun) x)


(* Now we introduce different instances of the previous tacticals *)
let change_hyp_and_check t env sigma c =
  if is_conv (Global.env()) sigma t c then 
    t
  else 
    errorlabstrm "convert-check-hyp" [< 'sTR "Not convertible" >]

let change_concl_and_check t env sigma c =
  if is_conv_leq (Global.env()) sigma t c then 
    t
  else 
    errorlabstrm "convert-check-concl" [< 'sTR "Not convertible" >]

let change_in_concl t = reduct_in_concl (change_concl_and_check t)
let change_in_hyp t   = reduct_in_hyp (change_hyp_and_check t)

let change_option t = function
  | Some id -> reduct_in_hyp   (change_hyp_and_check t) id
  | None    -> reduct_in_concl (change_concl_and_check t) 

(* Pour usage interne (le niveau User est pris en compte par dyn_reduce) *)
let red_in_concl        = reduct_in_concl red_product
let red_in_hyp          = reduct_in_hyp   red_product
let red_option          = reduct_option   red_product
let hnf_in_concl        = reduct_in_concl hnf_constr
let hnf_in_hyp          = reduct_in_hyp   hnf_constr
let hnf_option          = reduct_option   hnf_constr
let simpl_in_concl      = reduct_in_concl nf
let simpl_in_hyp        = reduct_in_hyp   nf
let simpl_option        = reduct_option   nf
let normalise_in_concl  = reduct_in_concl compute
let normalise_in_hyp    = reduct_in_hyp   compute
let normalise_option    = reduct_option   compute
let unfold_in_concl loccname   = reduct_in_concl (unfoldn loccname) 
let unfold_in_hyp   loccname   = reduct_in_hyp   (unfoldn loccname) 
let unfold_option   loccname   = reduct_option   (unfoldn loccname) 
let pattern_option l = reduct_option (pattern_occs l)

let dyn_change = function<commit_msg>Prise en compte env local (et defs locales) dans Change<commit_after>(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id$ *)

open Pp
open Util
open Stamps
open Names
open Sign
open Term
open Inductive
open Reduction
open Environ
open Declare
open Evd
open Pfedit
open Tacred
open Tacmach
open Proof_trees
open Proof_type
open Logic
open Evar_refiner
open Clenv
open Tacticals
open Hipattern
open Coqlib

exception Bound

(*********************************************)
(*                 Tactics                   *)
(*********************************************)

(****************************************)
(* General functions                    *)
(****************************************)

let get_pairs_from_bindings = 
  let pair_from_binding = function  
    | [(Bindings binds)] -> binds
    | _                  -> error "not a binding list!"
  in 
  List.map pair_from_binding

let rec string_head_bound x = match kind_of_term x with
  | IsConst _ -> string_of_id (basename (path_of_const x))
  | IsMutInd (ind_sp,args) -> 
      let mispec = Global.lookup_mind_specif (ind_sp,args) in 
      string_of_id (mis_typename mispec)
  | IsMutConstruct ((ind_sp,i),args) ->
       let mispec = Global.lookup_mind_specif (ind_sp,args) in 
       string_of_id (mis_consnames mispec).(i-1)
  | IsVar id -> string_of_id id
  | _ -> raise Bound

let string_head c = 
  try string_head_bound c with Bound -> error "Bound head variable"


let rec head_constr_bound t l =
  let t = strip_outer_cast(collapse_appl t) in
  match kind_of_term t with
    | IsProd (_,_,c2)  -> head_constr_bound c2 l 
    | IsLetIn (_,_,_,c2) -> head_constr_bound c2 l 
    | IsApp (f,args)  -> 
	head_constr_bound f (Array.fold_right (fun a l -> a::l) args l)
    | IsConst _        -> t::l
    | IsMutInd _       -> t::l
    | IsMutConstruct _ -> t::l
    | IsVar _          -> t::l
    | _                -> raise Bound

let head_constr c = 
  try head_constr_bound c [] with Bound -> error "Bound head variable"

let bad_tactic_args s l =
  raise (RefinerError (BadTacticArgs (s,l)))

(******************************************)
(*           Primitive tactics            *)
(******************************************)

let introduction    = Tacmach.introduction 
let intro_replacing = Tacmach.intro_replacing 
let refine          = Tacmach.refine
let convert_concl   = Tacmach.convert_concl
let convert_hyp     = Tacmach.convert_hyp
let thin            = Tacmach.thin 
let move_hyp        = Tacmach.move_hyp 

let mutual_fix   = Tacmach.mutual_fix
let fix f n      = mutual_fix [f] [n] []

let fix_noname n =  
  let id = Pfedit.get_current_proof_name () in
  fix id n

let dyn_mutual_fix argsl gl = 
  match argsl with 
    | [Integer n]                          -> fix_noname n gl
    | [Identifier id;Integer n]            -> fix id n gl
    | ((Identifier id)::(Integer n)::lfix) -> 
	let rec decomp lid ln lar = function
          | (Fixexp (id,n,ar)::rest) -> 
	      decomp (id::lid) (n::ln) (ar::lar) rest
          | [] -> (List.rev lid,List.rev ln,List.rev lar)
	  | _  -> bad_tactic_args "mutual_fix" argsl
	in
	let (lid,ln,lar) = decomp [] [] [] lfix in
	mutual_fix (id::lid) (n::ln) (List.map (pf_interp_constr gl) lar) gl
    | l -> bad_tactic_args "mutual_fix" l 

let mutual_cofix = Tacmach.mutual_cofix
let cofix f      =  mutual_cofix [f] []

let cofix_noname n =  
  let id = Pfedit.get_current_proof_name () in
  cofix id n

let dyn_mutual_cofix argsl gl = 
  match argsl with
    | []                       -> cofix_noname gl
    | [(Identifier id)]        -> cofix id gl
    | ((Identifier id)::lcofix) -> 
	let rec decomp lid lar = function 
          | (Cofixexp (id,ar)::rest) -> 
              decomp (id::lid) (ar::lar) rest
          | [] -> (List.rev lid,List.rev lar)
	  |  _ -> bad_tactic_args "mutual_cofix" argsl
	in
	let (lid,lar) = decomp [] [] lcofix in
        mutual_cofix (id::lid) (List.map (pf_interp_constr gl) lar) gl
   | l -> bad_tactic_args "mutual_cofix" l 


(**************************************************************)
(*          Reduction and conversion tactics                  *)
(**************************************************************)

type 'a tactic_reduction = env -> enamed_declarations -> constr -> constr

(* The following two tactics apply an arbitrary
   reduction function either to the conclusion or to a 
   certain hypothesis *)

let reduct_in_concl redfun gl = 
  convert_concl (pf_reduce redfun gl (pf_concl gl)) gl
    
let reduct_in_hyp redfun id gl  = 
  let ty = pf_get_hyp_typ gl id in
  let redfun' = under_casts (pf_reduce redfun gl) in
  convert_hyp id (redfun' ty) gl
    
let reduct_option redfun = function
  | Some id -> reduct_in_hyp   redfun id 
  | None    -> reduct_in_concl redfun 

(* The following tactic determines whether the reduction
   function has to be applied to the conclusion or
   to the hypotheses. *) 

let in_combinator tac1 tac2 = function 
  | [] -> tac1 
  | x  -> (tclMAP tac2 x)
	
let redin_combinator redfun = function 
  | [] ->  reduct_in_concl redfun 
  | x  -> (tclMAP (reduct_in_hyp redfun) x)


(* Now we introduce different instances of the previous tacticals *)
let change_hyp_and_check t env sigma c =
  if is_conv env sigma t c then 
    t
  else 
    errorlabstrm "convert-check-hyp" [< 'sTR "Not convertible" >]

let change_concl_and_check t env sigma c =
  if is_conv_leq env sigma t c then 
    t
  else 
    errorlabstrm "convert-check-concl" [< 'sTR "Not convertible" >]

let change_in_concl t = reduct_in_concl (change_concl_and_check t)
let change_in_hyp t   = reduct_in_hyp (change_hyp_and_check t)

let change_option t = function
  | Some id -> reduct_in_hyp   (change_hyp_and_check t) id
  | None    -> reduct_in_concl (change_concl_and_check t) 

(* Pour usage interne (le niveau User est pris en compte par dyn_reduce) *)
let red_in_concl        = reduct_in_concl red_product
let red_in_hyp          = reduct_in_hyp   red_product
let red_option          = reduct_option   red_product
let hnf_in_concl        = reduct_in_concl hnf_constr
let hnf_in_hyp          = reduct_in_hyp   hnf_constr
let hnf_option          = reduct_option   hnf_constr
let simpl_in_concl      = reduct_in_concl nf
let simpl_in_hyp        = reduct_in_hyp   nf
let simpl_option        = reduct_option   nf
let normalise_in_concl  = reduct_in_concl compute
let normalise_in_hyp    = reduct_in_hyp   compute
let normalise_option    = reduct_option   compute
let unfold_in_concl loccname   = reduct_in_concl (unfoldn loccname) 
let unfold_in_hyp   loccname   = reduct_in_hyp   (unfoldn loccname) 
let unfold_option   loccname   = reduct_option   (unfoldn loccname) 
let pattern_option l = reduct_option (pattern_occs l)

let dyn_change = function
{'fraction_non_alphanumeric': 0.16086051353226927, 'fraction_numerical': 0.0015267175572519084, 'mean_word_length': 3.000832870627429, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 93, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2804032', 'n_tokens_mistral': 5041, 'n_tokens_neox': 4687, 'n_words': 1332}