Module `Genarg`

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

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.

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.

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.

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

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

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

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