Module Genarg

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

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.

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
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.

Projections
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
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 : functor (M : GenObj) -> sig ... end
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