GenargSourceGeneric arguments used by the extension mechanisms of several Rocq ASTs.
Generic arguments must be registered according to their usage:
(raw level printers are always useful for clearer -time output, for beautify, and some other debug prints)
ltac:(), ltac2:() and ltac2 $x). Such genargs appear in glob_term GGenarg and constrexpr CGenarg. They must be registered with Genintern.register_intern0 and GlobEnv.register_constr_interp0.The glob level may be kept through notations and other operations like Ltac definitions (eg Ltac foo := exact ltac2:(foo)) in which case Gensubst.register_subst0 and a glob level printer are useful.
Other useful registrations are
Genintern.register_intern_pat and Patternops.register_interp_pat to be used in tactic patterns.Genintern.register_ntn_subst0 to be used in notations (eg Notation "foo" := ltac2:(foo)).NB: only the base ExtraArg is allowed here.
Must be registered with Genintern.register_intern0 and Genintern.register_interp0.
The glob level can be kept (currently with Hint Extern and Hint Rewrite) so Gensubst.register_subst0 is also needed.
Currently AFAICT this is just Tacarg.wit_ltac.
NB: only the base ExtraArg is allowed here.
With VERNAC ARGUMENT EXTEND the raw level printer is registered by including PRINTED BY.
Must be registered with Procq.register_grammar (handled by VERNAC ARGUMENT EXTEND when declared that way) as vernac extend only gets the genarg as argument so must get the grammar from the registration.
Unless combined with some other use, the glob and top levels will be empty (as in vernac_genarg_type).
Must be registered with Genintern.register_intern0, Gensubst.register_subst0 and Genintern.register_interp0.
Must be registered with Procq.register_grammar as tactic extend only gets the genarg as argument so must get the grammar from the registration.
They must be associated with a Geninterp.Val.tag using Geninterp.register_val0 (which creates a fresh tag if passed None). Note: although Genintern.register_interp0 registers a producer of arbitrary Geninterp.Val.t, tactic_extend requires them to be of the tag registered by Geninterp.register_val0 to work properly.
They should also have all printer levels registered with Genprint.register_print0.
All registrations are handled by the arguments to ARGUMENT EXTEND when declared that way.
All of them can also be used as vernac_extend arguments since vernac_extend uses a subset of the registrations needed for tactic_extend.
The route of a generic argument, from parsing to evaluation. In the following diagram, "object" can be ltac_expr, constr, tactic_value, etc.
\begin{verbatim} parsing in_raw out_raw char stream ---> raw_object ---> raw_object generic_argument -------+ encapsulation decaps| | V raw_object | globalization | V glob_object | encaps | in_glob | V glob_object generic_argument | out in out_glob | object <--- object generic_argument <--- object <--- glob_object <---+ | decaps encaps interp decaps | V effective use \end{verbatim}
To distinguish between the uninterpreted, globalized and interpreted worlds, we annotate the type generic_argument by a phantom argument.
type (_, _, _) genarg_type = | ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type| ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option)
genarg_type| PairArg : ('a1, 'b1, 'c1) genarg_type
* ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2)
genarg_typeGeneric types. The first parameter is the OCaml lowest level, the second one is the globalized level, and third one the internalized level.
Alias for concision when the three types agree.
Produced by VERNAC ARGUMENT EXTEND
Create a new generic type of argument: force to associate unique ML types at each of the three levels.
Alias for make0.
All of rlevel, glevel and tlevel must be non convertible to ensure the injectivity of the GADT type inference.
type (_, _) abstract_argument_type = | Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_typeGeneric types at a fixed level. The first parameter embeds the OCaml type and the second one the level.
Specialized type at raw level.
Specialized type at globalized level.
Specialized type at internalized level.
Projection on the raw type constructor.
Projection on the globalized type constructor.
Projection on the internalized type constructor.
type 'l generic_argument = | GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argumentA inhabitant of 'level generic_argument is a inhabitant of some type at level 'level, together with the representation of this type.
in_gen t x embeds an argument of type t into a generic argument.
out_gen t x recovers an argument of type t from a generic argument. It fails if x has not the right dynamic type.
has_type v t tells whether v has type t. If true, it ensures that out_gen t v will not raise a dynamic type exception.
val genarg_type_eq :
('a1, 'b1, 'c1) genarg_type ->
('a2, 'b2, 'c2) genarg_type ->
('a1 * 'b1 * 'c1, 'a2 * 'b2 * 'c2) CSig.eq optionval abstract_argument_type_eq :
('a, 'l) abstract_argument_type ->
('b, 'l) abstract_argument_type ->
('a, 'b) CSig.eq optionPrint a human-readable representation for a given type.
This is boilerplate code used here and there in the code of Rocq.
Works only on base objects (ExtraArg), otherwise fails badly.
Warning: although the following APIs use genarg_type the values must always be ExtraArg some_tag.
The functions below are aliases for generic_type constructors.
val wit_pair :
('a1, 'b1, 'c1) genarg_type ->
('a2, 'b2, 'c2) genarg_type ->
('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type