blob: 9bbc2fdac1e93004ce12024372bb8760041ab4a6 (
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
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
166
167
168
169
170
171
172
173
174
175
176
|
(************************************************************************)
(* 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 Names
open Term
open Entries
open Libnames
open Globnames
open Vernacexpr
open Constrexpr
open Decl_kinds
open Redexpr
open Pfedit
(** This file is about the interpretation of raw commands into typed
ones and top-level declaration of the main Gallina objects *)
val do_universe : polymorphic -> Id.t Loc.located list -> unit
val do_constraint : polymorphic ->
(Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> unit
(** {6 Hooks for Pcoq} *)
val set_declare_definition_hook : (Safe_typing.private_constants definition_entry -> unit) -> unit
val get_declare_definition_hook : unit -> (Safe_typing.private_constants definition_entry -> unit)
(** {6 Definitions/Let} *)
val interp_definition :
lident list option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
Universes.universe_binders * Impargs.manual_implicits
val declare_definition : Id.t -> definition_kind ->
Safe_typing.private_constants definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
val do_definition : Id.t -> definition_kind -> lident list option ->
local_binder_expr list -> red_expr option -> constr_expr ->
constr_expr option -> unit Lemmas.declaration_hook -> unit
(** {6 Parameters/Assumptions} *)
(* val interp_assumption : env -> evar_map ref -> *)
(* local_binder_expr list -> constr_expr -> *)
(* types Univ.in_universe_context_set * Impargs.manual_implicits *)
(** returns [false] if the assumption is neither local to a section,
nor in a module type and meant to be instantiated. *)
val declare_assumption : coercion_flag -> assumption_kind ->
types Univ.in_universe_context_set ->
Universes.universe_binders -> Impargs.manual_implicits ->
bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
global_reference * Univ.Instance.t * bool
val do_assumptions : locality * polymorphic * assumption_object_kind ->
Vernacexpr.inline -> (plident list * constr_expr) with_coercion list -> bool
(* val declare_assumptions : variable Loc.located list -> *)
(* coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> *)
(* Impargs.manual_implicits -> bool -> Vernacexpr.inline -> bool *)
(** {6 Inductive and coinductive types} *)
(** Extracting the semantical components out of the raw syntax of mutual
inductive declarations *)
type structured_one_inductive_expr = {
ind_name : Id.t;
ind_univs : lident list option;
ind_arity : constr_expr;
ind_lc : (Id.t * constr_expr) list
}
type structured_inductive_expr =
local_binder_expr list * structured_one_inductive_expr list
val extract_mutual_inductive_declaration_components :
(one_inductive_expr * decl_notation list) list ->
structured_inductive_expr * (*coercions:*) qualid list * decl_notation list
(** Typing mutual inductive definitions *)
type one_inductive_impls =
Impargs.manual_implicits (** for inds *)*
Impargs.manual_implicits list (** for constrs *)
val interp_mutual_inductive :
structured_inductive_expr -> decl_notation list -> polymorphic ->
private_flag -> Decl_kinds.recursivity_kind ->
mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
(** Registering a mutual inductive definition together with its
associated schemes *)
val declare_mutual_inductive_with_eliminations :
mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list ->
mutual_inductive
(** Entry points for the vernacular commands Inductive and CoInductive *)
val do_mutual_inductive :
(one_inductive_expr * decl_notation list) list -> polymorphic ->
private_flag -> Decl_kinds.recursivity_kind -> unit
(** {6 Fixpoints and cofixpoints} *)
type structured_fixpoint_expr = {
fix_name : Id.t;
fix_univs : lident list option;
fix_annot : Id.t Loc.located option;
fix_binders : local_binder_expr list;
fix_body : constr_expr option;
fix_type : constr_expr
}
(** Extracting the semantical components out of the raw syntax of
(co)fixpoints declarations *)
val extract_fixpoint_components : bool ->
(fixpoint_expr * decl_notation list) list ->
structured_fixpoint_expr list * decl_notation list
val extract_cofixpoint_components :
(cofixpoint_expr * decl_notation list) list ->
structured_fixpoint_expr list * decl_notation list
(** Typing global fixpoints and cofixpoint_expr *)
type recursive_preentry =
Id.t list * constr option list * types list
val interp_fixpoint :
structured_fixpoint_expr list -> decl_notation list ->
recursive_preentry * lident list option * Evd.evar_universe_context *
(EConstr.rel_context * Impargs.manual_implicits * int option) list
val interp_cofixpoint :
structured_fixpoint_expr list -> decl_notation list ->
recursive_preentry * lident list option * Evd.evar_universe_context *
(EConstr.rel_context * Impargs.manual_implicits * int option) list
(** Registering fixpoints and cofixpoints in the environment *)
val declare_fixpoint :
locality -> polymorphic ->
recursive_preentry * lident list option * Evd.evar_universe_context *
(Context.Rel.t * Impargs.manual_implicits * int option) list ->
lemma_possible_guards -> decl_notation list -> unit
val declare_cofixpoint : locality -> polymorphic ->
recursive_preentry * lident list option * Evd.evar_universe_context *
(Context.Rel.t * Impargs.manual_implicits * int option) list ->
decl_notation list -> unit
(** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
val do_fixpoint :
(* When [false], assume guarded. *)
locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
val do_cofixpoint :
(* When [false], assume guarded. *)
locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
(** Utils *)
val check_mutuality : Environ.env -> Evd.evar_map -> bool -> (Id.t * types) list -> unit
val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
|
