(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)
(** Interpretation functions for generic arguments and interpreted Ltac
values. *)
open Names open Genarg
(** {6 Dynamic toplevel values} *)
module Val : sig type'a typ
val create : string -> 'a typ
type _ tag =
| Base : 'a typ -> 'a tag
| List : 'a tag -> 'a list tag
| Opt : 'a tag -> 'a option tag
| Pair : 'a tag * 'b tag -> ('a * 'b) tag
type t = Dyn : 'a typ * 'a -> t
val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option val repr : 'a typ -> string val pr : 'a typ -> Pp.t
val typ_list : t list typ val typ_opt : t option typ val typ_pair : (t * t) typ
val inject : 'a tag -> 'a -> t
end
module ValTMap (Value : Dyn.ValueS) :
Dyn.MapS withtype'a key = 'a Val.typ andtype'a value = 'a Value.t
(** Dynamic types for toplevel values. While the generic types permit to relate objects at various levels of interpretation, toplevel values are wearing their own type regardless of where they came from. This allows to use the
same runtime representation for several generic types. *)
val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag (** Retrieve the dynamic type associated to a toplevel genarg. *)
val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> unit (** Register the representation of a generic argument. If no tag is given as argument, a new fresh tag with the same name as the argument is associated
to the generic type. *)
(** {6 Interpretation functions} *)
module TacStore : Store.S
type interp_sign =
{ lfun : Val.t Id.Map.t
; poly : bool
; extra : TacStore.t }
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
