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

(*i $Id$ i*)

open Util
open Names
open Term
open Libnames
open Rawterm
open Topconstr
open Term

type 'a and_short_name = 'a * identifier located option

(* In globalize tactics, we need to keep the initial [constr_expr] to recompute*)
(* in the environment by the effective calls to Intro, Inversion, etc *)
(* The [constr_expr] field is [None] in TacDef though *)
type rawconstr_and_expr = rawconstr * constr_expr option

type open_constr = Evd.evar_map * Term.constr
type open_constr_expr = unit * constr_expr
type open_rawconstr = unit * rawconstr_and_expr

type intro_pattern_expr =
  | IntroOrAndPattern of case_intro_pattern_expr
  | IntroWildcard
  | IntroIdentifier of identifier
  | IntroAnonymous
and case_intro_pattern_expr = intro_pattern_expr list list

val pr_intro_pattern : intro_pattern_expr -> Pp.std_ppcmds
val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds

(* The route of a generic argument, from parsing to evaluation

\begin{verbatim}
              parsing        in_raw                           out_raw
    char stream ----> rawtype ----> rawconstr generic_argument ---->
                                                                   |
                                                                   | interp
                                                                   V
                          type  <---- constr generic_argument  <----
                                  out                            in
\end{verbatim}

To distinguish between the uninterpreted (raw) and the interpreted
worlds, we annotate the type [generic_argument] by a phantom argument
which is either [constr_expr] or [constr] (actually we add also a second
argument [raw_tactic_expr] and [tactic], but this is only for technical
reasons, because these types are undefined at the type of compilation
of [Genarg]).

Transformation for each type :
\begin{verbatim}
tag                            raw open type            cooked closed type

BoolArgType                    bool                     bool
IntArgType                     int                      int
IntOrVarArgType                int or_var               int
StringArgType                  string (parsed w/ "")    string
PreIdentArgType                string (parsed w/o "")   (vernac only)
IdentArgType                   identifier               identifier
IntroPatternArgType            intro_pattern_expr       intro_pattern_expr
VarArgType                     identifier               constr
RefArgType                     reference                global_reference
ConstrArgType                  constr_expr              constr
ConstrMayEvalArgType           constr_expr may_eval     constr
QuantHypArgType                quantified_hypothesis    quantified_hypothesis
OpenConstrArgType              constr_expr              open_constr
ConstrBindingsArgType      constr_expr with_bindings constr with_bindings
List0ArgType of argument_type
List1ArgType of argument_type
OptArgType of argument_type
ExtraArgType of string         '_a                      '_b
\end{verbatim}
*)

(* All of [rlevel], [glevel] and [tlevel] must be non convertible 
   to ensure the injectivity of the type inference from type
   [('co,'ta) generic_argument] to [('a,'co,'ta) abstract_argument_type]
   is injective; this guarantees that, for 'b fixed, the type of
   out_gen is monomorphic over 'a, hence type-safe 
*)
<commit_msg>Légère mise à jour<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        *)
(************************************************************************)

(*i $Id$ i*)

open Util
open Names
open Term
open Libnames
open Rawterm
open Topconstr
open Term

type 'a and_short_name = 'a * identifier located option

(* In globalize tactics, we need to keep the initial [constr_expr] to recompute*)
(* in the environment by the effective calls to Intro, Inversion, etc *)
(* The [constr_expr] field is [None] in TacDef though *)
type rawconstr_and_expr = rawconstr * constr_expr option

type open_constr = Evd.evar_map * Term.constr
type open_constr_expr = unit * constr_expr
type open_rawconstr = unit * rawconstr_and_expr

type intro_pattern_expr =
  | IntroOrAndPattern of case_intro_pattern_expr
  | IntroWildcard
  | IntroIdentifier of identifier
  | IntroAnonymous
and case_intro_pattern_expr = intro_pattern_expr list list

val pr_intro_pattern : intro_pattern_expr -> Pp.std_ppcmds
val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds

(* The route of a generic argument, from parsing to evaluation

\begin{verbatim}
              parsing        in_raw                           out_raw
    char stream ----> rawtype ----> rawconstr generic_argument ---->
                                                                   |
                                                                   | interp
                                                                   V
                          type  <---- constr generic_argument  <----
                                  out                            in
\end{verbatim}

To distinguish between the uninterpreted (raw) and the interpreted
worlds, we annotate the type [generic_argument] by a phantom argument
which is either [constr_expr] or [constr] (actually we add also a second
argument [raw_tactic_expr] and [tactic], but this is only for technical
reasons, because these types are undefined at the type of compilation
of [Genarg]).

Transformation for each type :
\begin{verbatim}
tag                            raw open type            cooked closed type

BoolArgType                    bool                      bool
IntArgType                     int                       int
IntOrVarArgType                int or_var                int
StringArgType                  string (parsed w/ "")     string
PreIdentArgType                string (parsed w/o "")    (vernac only)
IdentArgType                   identifier                identifier
IntroPatternArgType            intro_pattern_expr        intro_pattern_expr
VarArgType                     identifier                identifier
RefArgType                     reference                 global_reference
QuantHypArgType                quantified_hypothesis     quantified_hypothesis
ConstrArgType                  constr_expr               constr
ConstrMayEvalArgType           constr_expr may_eval      constr
OpenConstrArgType              open_constr_expr          open_constr
ConstrWithBindingsArgType      constr_expr with_bindings constr with_bindings
BindingsArgType                constr_expr bindings      constr bindings
List0ArgType of argument_type
List1ArgType of argument_type
OptArgType of argument_type
ExtraArgType of string         '_a                      '_b
\end{verbatim}
*)

(* All of [rlevel], [glevel] and [tlevel] must be non convertible 
   to ensure the injectivity of the type inference from type
   [('co,'ta) generic_argument] to [('a,'co,'ta) abstract_argument_type]
   is injective; this guarantees that, for 'b fixed, the type of
   out_gen is monomorphic over 'a, hence type-safe 
*)

{'fraction_non_alphanumeric': 0.10388313147708828, 'fraction_numerical': 0.000998876264202772, 'mean_word_length': 2.0772185939300805, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 13, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 30, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2710007', 'n_tokens_mistral': 2034, 'n_tokens_neox': 1947, 'n_words': 668}