1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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 with type 'a key = 'a Val.typ and type '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;
extra : TacStore.t }
type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun
val register_interp0 :
('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit
|
