package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b
doc/coq-core.lib/Genarg/index.html
Module GenargSource
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
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.
Alias for concision when the three types agree.
Create a new generic type of argument: force to associate unique ML types at each of the three levels.
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 (_, _) 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.
Specialized type at raw level.
Specialized type at globalized level.
Specialized type at internalized level.
Projections
Projection on the raw type constructor.
Projection on the globalized type constructor.
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_argumentis a inhabitant of some type at level'level, together with the representation of this type.
Constructors
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.
Type reification
Equalities
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.
Registering genarg-manipulating functions
This is boilerplate code used here and there in the code of Coq.
Works only on base objects (ExtraArg), otherwise fails badly.
Compatibility layer
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