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 = ('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 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