blob: c4b8c1e0ca15f54a223b80ba44b9124bfad08c52 (
plain)
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Genarg
open Names
open Libnames
open Nametab
open Tac2expr
(** Ltac2 global environment *)
(** {5 Toplevel definition of values} *)
val define_global : ltac_constant -> (glb_tacexpr * type_scheme) -> unit
val interp_global : ltac_constant -> (glb_tacexpr * valexpr * type_scheme)
(** {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 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_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 : 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 -> ml_tactic -> unit
val interp_primitive : ml_tactic_name -> ml_tactic
(** {5 ML primitive types} *)
type 'a ml_object = {
ml_type : type_constant;
ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic;
}
val define_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object -> unit
val interp_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object
(** {5 Absolute paths} *)
val coq_prefix : ModPath.t
(** Path where primitive datatypes are defined in Ltac2 plugin. *)
(** {5 Generic arguments} *)
val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type
|
