<commit_before>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \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 Globnames
open Tac2types
open Genredexpr
open Proofview.Notations

let return = Proofview.tclUNIT
let thaw r f = Tac2ffi.app_fun1 f Tac2ffi.unit r ()

let tactic_infer_flags with_evar = {
  Pretyping.use_typeclasses = true;
  Pretyping.solve_unification_constraints = true;
  Pretyping.use_hook = None;
  Pretyping.fail_evar = not with_evar;
  Pretyping.expand_evars = true }

(** FIXME: export a better interface in Tactics *)
let delayed_of_tactic tac env sigma =
  let _, pv = Proofview.init sigma [] in
  let c, pv, _, _ = Proofview.apply env tac pv in
  (sigma, c)

let delayed_of_thunk r tac env sigma =
  delayed_of_tactic (thaw r tac) env sigma

let mk_bindings = function
| ImplicitBindings l -> Misctypes.ImplicitBindings l
| ExplicitBindings l ->
  let l = List.map Loc.tag l in
  Misctypes.ExplicitBindings l
| NoBindings -> Misctypes.NoBindings

let mk_with_bindings (x, b) = (x, mk_bindings b)

let rec mk_intro_pattern = function
| IntroForthcoming b -> Loc.tag @@ Misctypes.IntroForthcoming b
| IntroNaming ipat -> Loc.tag @@ Misctypes.IntroNaming (mk_intro_pattern_naming ipat)
| IntroAction ipat -> Loc.tag @@ Misctypes.IntroAction (mk_intro_pattern_action ipat)

and mk_intro_pattern_naming = function
| IntroIdentifier id -> Misctypes.IntroIdentifier id
| IntroFresh id -> Misctypes.IntroFresh id
| IntroAnonymous -> Misctypes.IntroAnonymous

and mk_intro_pattern_action = function
| IntroWildcard -> Misctypes.IntroWildcard
| IntroOrAndPattern ipat -> Misctypes.IntroOrAndPattern (mk_or_and_intro_pattern ipat)
| IntroInjection ipats -> Misctypes.IntroInjection (List.map mk_intro_pattern ipats)
| IntroApplyOn (c, ipat) ->
  let c = Loc.tag @@ delayed_of_thunk Tac2ffi.constr c in
  Misctypes.IntroApplyOn (c, mk_intro_pattern ipat)
| IntroRewrite b -> Misctypes.IntroRewrite b

and mk_or_and_intro_pattern = function
| IntroOrPattern ipatss ->
  Misctypes.IntroOrPattern (List.map (fun ipat -> List.map mk_intro_pattern ipat) ipatss)
| IntroAndPattern ipats ->
  Misctypes.IntroAndPattern (List.map mk_intro_pattern ipats)

let mk_intro_patterns ipat = List.map mk_intro_pattern ipat

let mk_occurrences f = function
| AllOccurrences -> Locus.AllOccurrences
| AllOccurrencesBut l -> Locus.AllOccurrencesBut (List.map f l)
| NoOccurrences -> Locus.NoOccurrences
| OnlyOccurrences l -> Locus.OnlyOccurrences (List.map f l)

let mk_occurrences_expr occ =
  mk_occurrences (fun i -> Misctypes.ArgArg i) occ

let mk_hyp_location (id, occs, h) =
  ((mk_occurrences_expr occs, id), h)

let mk_clause cl = {
  Locus.onhyps = Option.map (fun l -> List.map mk_hyp_location l) cl.onhyps;
  Locus.concl_occs = mk_occurrences_expr cl.concl_occs;
}

let intros_patterns ev ipat =
  let ipat = mk_intro_patterns ipat in
  Tactics.intro_patterns ev ipat

let apply adv ev cb cl =
  let map c =<commit_msg>Fix the semantics of introducing with empty intro patterns.<commit_after>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \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 Globnames
open Tac2types
open Genredexpr
open Proofview.Notations

let return = Proofview.tclUNIT
let thaw r f = Tac2ffi.app_fun1 f Tac2ffi.unit r ()

let tactic_infer_flags with_evar = {
  Pretyping.use_typeclasses = true;
  Pretyping.solve_unification_constraints = true;
  Pretyping.use_hook = None;
  Pretyping.fail_evar = not with_evar;
  Pretyping.expand_evars = true }

(** FIXME: export a better interface in Tactics *)
let delayed_of_tactic tac env sigma =
  let _, pv = Proofview.init sigma [] in
  let c, pv, _, _ = Proofview.apply env tac pv in
  (sigma, c)

let delayed_of_thunk r tac env sigma =
  delayed_of_tactic (thaw r tac) env sigma

let mk_bindings = function
| ImplicitBindings l -> Misctypes.ImplicitBindings l
| ExplicitBindings l ->
  let l = List.map Loc.tag l in
  Misctypes.ExplicitBindings l
| NoBindings -> Misctypes.NoBindings

let mk_with_bindings (x, b) = (x, mk_bindings b)

let rec mk_intro_pattern = function
| IntroForthcoming b -> Loc.tag @@ Misctypes.IntroForthcoming b
| IntroNaming ipat -> Loc.tag @@ Misctypes.IntroNaming (mk_intro_pattern_naming ipat)
| IntroAction ipat -> Loc.tag @@ Misctypes.IntroAction (mk_intro_pattern_action ipat)

and mk_intro_pattern_naming = function
| IntroIdentifier id -> Misctypes.IntroIdentifier id
| IntroFresh id -> Misctypes.IntroFresh id
| IntroAnonymous -> Misctypes.IntroAnonymous

and mk_intro_pattern_action = function
| IntroWildcard -> Misctypes.IntroWildcard
| IntroOrAndPattern ipat -> Misctypes.IntroOrAndPattern (mk_or_and_intro_pattern ipat)
| IntroInjection ipats -> Misctypes.IntroInjection (List.map mk_intro_pattern ipats)
| IntroApplyOn (c, ipat) ->
  let c = Loc.tag @@ delayed_of_thunk Tac2ffi.constr c in
  Misctypes.IntroApplyOn (c, mk_intro_pattern ipat)
| IntroRewrite b -> Misctypes.IntroRewrite b

and mk_or_and_intro_pattern = function
| IntroOrPattern ipatss ->
  Misctypes.IntroOrPattern (List.map (fun ipat -> List.map mk_intro_pattern ipat) ipatss)
| IntroAndPattern ipats ->
  Misctypes.IntroAndPattern (List.map mk_intro_pattern ipats)

let mk_intro_patterns ipat = List.map mk_intro_pattern ipat

let mk_occurrences f = function
| AllOccurrences -> Locus.AllOccurrences
| AllOccurrencesBut l -> Locus.AllOccurrencesBut (List.map f l)
| NoOccurrences -> Locus.NoOccurrences
| OnlyOccurrences l -> Locus.OnlyOccurrences (List.map f l)

let mk_occurrences_expr occ =
  mk_occurrences (fun i -> Misctypes.ArgArg i) occ

let mk_hyp_location (id, occs, h) =
  ((mk_occurrences_expr occs, id), h)

let mk_clause cl = {
  Locus.onhyps = Option.map (fun l -> List.map mk_hyp_location l) cl.onhyps;
  Locus.concl_occs = mk_occurrences_expr cl.concl_occs;
}

let intros_patterns ev ipat =
  let ipat = mk_intro_patterns ipat in
  Tactics.intros_patterns ev ipat

let apply adv ev cb cl =
  let map c =
{'fraction_non_alphanumeric': 0.14147485705908225, 'fraction_numerical': 0.004398182084738308, 'mean_word_length': 4.414285714285715, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 49, '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': '6915939', 'n_tokens_mistral': 2499, 'n_tokens_neox': 2365, 'n_words': 618}