Module Genarg

Generic 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)

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

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.

Generic types
module ArgT : sig ... end
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_type

Generic types. The first parameter is the OCaml lowest level, the second one is the globalized level, and third one the internalized level.

type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type

Alias for concision when the three types agree.

type 'a vernac_genarg_type = ('a, Util.Empty.t, Util.Empty.t) genarg_type

Produced by VERNAC ARGUMENT EXTEND

val make0 : string -> ('raw, 'glob, 'top) genarg_type

Create a new generic type of argument: force to associate unique ML types at each of the three levels.

val create_arg : string -> ('raw, 'glob, 'top) genarg_type

Alias for make0.

Specialized types

All of rlevel, glevel and tlevel must be non convertible to ensure the injectivity of the GADT type inference.

type rlevel = [
| `rlevel
]
type glevel = [
| `glevel
]
type tlevel = [
| `tlevel
]
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_type

Generic types at a fixed level. The first parameter embeds the OCaml type and the second one the level.

type 'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type

Specialized type at raw level.

type 'a glob_abstract_argument_type = ('a, glevel) abstract_argument_type

Specialized type at globalized level.

type 'a typed_abstract_argument_type = ('a, tlevel) abstract_argument_type

Specialized type at internalized level.

Projections
val rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type

Projection on the raw type constructor.

val glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type

Projection on the globalized type constructor.

val topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type

Projection on the internalized type constructor.

Generic arguments
type 'l generic_argument =
| GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument(*

A inhabitant of 'level generic_argument is a inhabitant of some type at level 'level, together with the representation of this type.

*)
type raw_generic_argument = rlevel generic_argument
type glob_generic_argument = glevel generic_argument
type typed_generic_argument = tlevel generic_argument
Constructors
val in_gen : ('a, 'co) abstract_argument_type -> 'a -> 'co generic_argument

in_gen t x embeds an argument of type t into a generic argument.

val out_gen : ('a, 'co) abstract_argument_type -> 'co generic_argument -> 'a

out_gen t x recovers an argument of type t from a generic argument. It fails if x has not the right dynamic type.

val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool

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.

Type reification
type argument_type =
| ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type
Equalities
val argument_type_eq : argument_type -> argument_type -> bool
val genarg_type_eq : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'b1 * 'c1, 'a2 * 'b2 * 'c2) CSig.eq option
val abstract_argument_type_eq : ('a, 'l) abstract_argument_type -> ('b, 'l) abstract_argument_type -> ('a, 'b) CSig.eq option
val pr_argument_type : argument_type -> Pp.t

Print a human-readable representation for a given type.

val genarg_tag : 'a generic_argument -> argument_type
val unquote : ('a, 'co) abstract_argument_type -> argument_type
Registering genarg-manipulating functions

This is boilerplate code used here and there in the code of Rocq.

val get_arg_tag : ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c) ArgT.tag

Works only on base objects (ExtraArg), otherwise fails badly.

module type GenObj = sig ... end
module Register (M : GenObj) : sig ... end

Warning: although the following APIs use genarg_type the values must always be ExtraArg some_tag.

Compatibility layer

The functions below are aliases for generic_type constructors.

val wit_list : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type