Module Genarg

Generic arguments used by the extension mechanisms of several Coq ASTs.

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 = ('aUtil.Empty.tUtil.Empty.t) genarg_type


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 -> ('arlevel) abstract_argument_type
| Glbwit : ('a'b'c) genarg_type -> ('bglevel) abstract_argument_type
| Topwit : ('a'b'c) genarg_type -> ('ctlevel) 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 = ('arlevel) abstract_argument_type

Specialized type at raw level.

type 'a glob_abstract_argument_type = ('aglevel) abstract_argument_type

Specialized type at globalized level.

type 'a typed_abstract_argument_type = ('atlevel) abstract_argument_type

Specialized type at internalized level.

val rawwit : ('a'b'c) genarg_type -> ('arlevel) abstract_argument_type

Projection on the raw type constructor.

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

Projection on the globalized type constructor.

val topwit : ('a'b'c) genarg_type -> ('ctlevel) 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
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
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 Coq.

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.

Substitution functions
type 'glb subst_fun = Mod_subst.substitution -> 'glb -> 'glb

The type of functions used for substituting generic arguments.

val substitute : ('raw'glb'top) genarg_type -> 'glb subst_fun
val generic_substitute : glob_generic_argument subst_fun
val register_subst0 : ('raw'glb'top) genarg_type -> 'glb subst_fun -> unit
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