package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.pretyping/Genarg/index.html

Module GenargSource

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

Generic arguments must be registered according to their usage:

(raw level printers are always useful for clearer -time output, for beautify, and some other debug prints)

  • extensible constr syntax beyond notations (eg ltac:(), ltac2:() and ltac2 $x). Such genargs appear in glob_term GGenarg and constrexpr CGenarg. They must be registered with Genintern.register_intern0 and GlobEnv.register_constr_interp0.

The glob level may be kept through notations and other operations like Ltac definitions (eg Ltac foo := exact ltac2:(foo)) in which case Gensubst.register_subst0 and a glob level printer are useful.

Other useful registrations are

  • Genintern.register_intern_pat and Patternops.register_interp_pat to be used in tactic patterns.
  • Genintern.register_ntn_subst0 to be used in notations (eg Notation "foo" := ltac2:(foo)).

NB: only the base ExtraArg is allowed here.

  • tactic arguments to commands defined without depending on ltac_plugin (VernacProof, HintsExtern, Hint Rewrite, etc).

Must be registered with Genintern.register_intern0 and Genintern.register_interp0.

The glob level can be kept (currently with Hint Extern and Hint Rewrite) so Gensubst.register_subst0 is also needed.

Currently AFAICT this is just Tacarg.wit_ltac.

NB: only the base ExtraArg is allowed here.

  • vernac arguments, used by vernac extend. Usually declared in mlg using VERNAC ARGUMENT EXTEND then used in VERNAC EXTEND.

With VERNAC ARGUMENT EXTEND the raw level printer is registered by including PRINTED BY.

Must be registered with Procq.register_grammar (handled by VERNAC ARGUMENT EXTEND when declared that way) as vernac extend only gets the genarg as argument so must get the grammar from the registration.

Unless combined with some other use, the glob and top levels will be empty (as in vernac_genarg_type).

  • Ltac tactic_extend arguments. Usually declared in mlg using ARGUMENT EXTEND then used in TACTIC EXTEND.

Must be registered with Genintern.register_intern0, Gensubst.register_subst0 and Genintern.register_interp0.

Must be registered with Procq.register_grammar as tactic extend only gets the genarg as argument so must get the grammar from the registration.

They must be associated with a Geninterp.Val.tag using Geninterp.register_val0 (which creates a fresh tag if passed None). Note: although Genintern.register_interp0 registers a producer of arbitrary Geninterp.Val.t, tactic_extend requires them to be of the tag registered by Geninterp.register_val0 to work properly.

They should also have all printer levels registered with Genprint.register_print0.

All registrations are handled by the arguments to ARGUMENT EXTEND when declared that way.

All of them can also be used as vernac_extend arguments since vernac_extend uses a subset of the registrations needed for tactic_extend.

  • some hack in Tacentries.ml_val_tactic_extend and its variant in Tac2core_ltac1 for Ltac1.lambda.

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
Sourcemodule ArgT : sig ... end
Sourcetype (_, _, _) 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.

Sourcetype 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type

Alias for concision when the three types agree.

Sourcetype 'a vernac_genarg_type = ('a, Util.Empty.t, Util.Empty.t) genarg_type

Produced by VERNAC ARGUMENT EXTEND

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

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

Sourcetype rlevel = [
  1. | `rlevel
]
Sourcetype glevel = [
  1. | `glevel
]
Sourcetype tlevel = [
  1. | `tlevel
]
Sourcetype (_, _) 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.

Sourcetype 'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type

Specialized type at raw level.

Sourcetype 'a glob_abstract_argument_type = ('a, glevel) abstract_argument_type

Specialized type at globalized level.

Sourcetype 'a typed_abstract_argument_type = ('a, tlevel) abstract_argument_type

Specialized type at internalized level.

Projections
Sourceval rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type

Projection on the raw type constructor.

Sourceval glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type

Projection on the globalized type constructor.

Sourceval topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type

Projection on the internalized type constructor.

Generic arguments
Sourcetype '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.

    *)
Sourcetype raw_generic_argument = rlevel generic_argument
Sourcetype glob_generic_argument = glevel generic_argument
Sourcetype typed_generic_argument = tlevel generic_argument
Constructors
Sourceval 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.

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

Sourceval 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
Sourcetype argument_type =
  1. | ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type
Equalities
Sourceval argument_type_eq : argument_type -> argument_type -> bool
Sourceval genarg_type_eq : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'b1 * 'c1, 'a2 * 'b2 * 'c2) CSig.eq option
Sourceval abstract_argument_type_eq : ('a, 'l) abstract_argument_type -> ('b, 'l) abstract_argument_type -> ('a, 'b) CSig.eq option
Sourceval pr_argument_type : argument_type -> Pp.t

Print a human-readable representation for a given type.

Sourceval genarg_tag : 'a generic_argument -> argument_type
Sourceval unquote : ('a, 'co) abstract_argument_type -> argument_type
Registering genarg-manipulating functions

This is boilerplate code used here and there in the code of Rocq.

Sourceval get_arg_tag : ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c) ArgT.tag

Works only on base objects (ExtraArg), otherwise fails badly.

Sourcemodule type GenObj = sig ... end
Sourcemodule Register (M : GenObj) : sig ... end

Warning: although the following APIs use genarg_type the values must always be ExtraArg some_tag.

Compatibility layer

The functions below are aliases for generic_type constructors.

Sourceval wit_list : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
Sourceval wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
Sourceval wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type