package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 =
  1. | ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
  2. | ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
  3. | OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
  4. | 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

All of rlevel, glevel and tlevel must be non convertible to ensure the injectivity of the GADT type inference.

type rlevel = [
  1. | `rlevel
]
type glevel = [
  1. | `glevel
]
type tlevel = [
  1. | `tlevel
]
type (_, _) abstract_argument_type =
  1. | Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
  2. | Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
  3. | 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 =
  1. | 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 =
  1. | 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
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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct