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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq 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) *)
(************************************************************************)
open Genarg
open Names
open Libnames
open Nametab
open Tac2expr
open Tac2ffi
(** Ltac2 global environment *)
(** {5 Toplevel definition of values} *)
type global_data = {
gdata_expr : glb_tacexpr;
gdata_type : type_scheme;
gdata_mutable : bool;
gdata_deprecation : Deprecation.t option;
}
val define_global : ltac_constant -> global_data -> unit
val interp_global : ltac_constant -> global_data
(** {5 Toplevel definition of types} *)
val define_type : type_constant -> glb_quant_typedef -> unit
val interp_type : type_constant -> glb_quant_typedef
(** {5 Toplevel definition of algebraic constructors} *)
type constructor_data = {
cdata_prms : int;
(** Type parameters *)
cdata_type : type_constant;
(** Inductive definition to which the constructor pertains *)
cdata_args : int glb_typexpr list;
(** Types of the constructor arguments *)
cdata_indx : int option;
(** Index of the constructor in the ADT. Numbering is duplicated between
argumentless and argument-using constructors, e.g. in type ['a option]
[None] and [Some] have both index 0. This field is empty whenever the
constructor is a member of an open type. *)
}
val define_constructor : ltac_constructor -> constructor_data -> unit
val interp_constructor : ltac_constructor -> constructor_data
(** {5 Toplevel definition of projections} *)
type projection_data = {
pdata_prms : int;
(** Type parameters *)
pdata_type : type_constant;
(** Record definition to which the projection pertains *)
pdata_ptyp : int glb_typexpr;
(** Type of the projection *)
pdata_mutb : bool;
(** Whether the field is mutable *)
pdata_indx : int;
(** Index of the projection *)
}
val define_projection : ltac_projection -> projection_data -> unit
val interp_projection : ltac_projection -> projection_data
(** {5 Toplevel definition of aliases} *)
type alias_data = {
alias_body : raw_tacexpr;
alias_depr : Deprecation.t option;
}
val define_alias : ?deprecation:Deprecation.t -> ltac_constant -> raw_tacexpr -> unit
val interp_alias : ltac_constant -> alias_data
(** {5 Name management} *)
val push_ltac : visibility -> full_path -> tacref -> unit
val locate_ltac : qualid -> tacref
val locate_extended_all_ltac : qualid -> tacref list
val shortest_qualid_of_ltac : tacref -> qualid
val push_constructor : visibility -> full_path -> ltac_constructor -> unit
val locate_constructor : qualid -> ltac_constructor
val locate_extended_all_constructor : qualid -> ltac_constructor list
val shortest_qualid_of_constructor : ltac_constructor -> qualid
val push_type : visibility -> full_path -> type_constant -> unit
val locate_type : qualid -> type_constant
val locate_extended_all_type : qualid -> type_constant list
val shortest_qualid_of_type : ?loc:Loc.t -> type_constant -> qualid
val push_projection : visibility -> full_path -> ltac_projection -> unit
val locate_projection : qualid -> ltac_projection
val locate_extended_all_projection : qualid -> ltac_projection list
val shortest_qualid_of_projection : ltac_projection -> qualid
(** {5 Toplevel definitions of ML tactics} *)
(** This state is not part of the summary, contrarily to the ones above. It is
intended to be used from ML plugins to register ML-side functions. *)
val define_primitive : ml_tactic_name -> closure -> unit
val interp_primitive : ml_tactic_name -> closure
(** {5 ML primitive types} *)
type 'a or_glb_tacexpr =
| GlbVal of 'a
| GlbTacexpr of glb_tacexpr
type ('a, 'b, 'r) intern_fun = Genintern.glob_sign -> 'a -> 'b * 'r glb_typexpr
type environment = {
env_ist : valexpr Id.Map.t;
}
type ('a, 'b) ml_object = {
ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun;
ml_subst : Mod_subst.substitution -> 'b -> 'b;
ml_interp : environment -> 'b -> valexpr Proofview.tactic;
ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t;
}
val define_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object -> unit
val interp_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object
(** {5 Absolute paths} *)
val coq_prefix : ModPath.t
(** Path where primitive datatypes are defined in Ltac2 plugin. *)
val std_prefix : ModPath.t
(** Path where Ltac-specific datatypes are defined in Ltac2 plugin. *)
val ltac1_prefix : ModPath.t
(** Path where the Ltac1 legacy FFI is defined. *)
(** {5 Generic arguments} *)
val wit_ltac2 : (Id.t CAst.t list * raw_tacexpr, Id.t list * glb_tacexpr, Util.Empty.t) genarg_type
(** Ltac2 quotations in Ltac1 code *)
val wit_ltac2_val : (Util.Empty.t, unit, Util.Empty.t) genarg_type
(** Embedding Ltac2 closures of type [Ltac1.t -> Ltac1.t] inside Ltac1. There is
no relevant data because arguments are passed by conventional names. *)
val wit_ltac2_constr : (raw_tacexpr, Id.Set.t * glb_tacexpr, Util.Empty.t) genarg_type
(** Ltac2 quotations in Gallina terms *)
val wit_ltac2_quotation : (Id.t Loc.located, Id.t, Util.Empty.t) genarg_type
(** Ltac2 quotations for variables "$x" in Gallina terms *)
(** {5 Helper functions} *)
val is_constructor_id : Id.t -> bool
val is_constructor : qualid -> bool
|
