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
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
|
(************************************************************************)
(* 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 Declarations
open Environ
open Evd
(** The following three functions are similar to the ones defined in
Inductive, but they expect an env *)
val type_of_inductive : env -> pinductive -> types
(** Return type as quoted by the user *)
val type_of_constructor : env -> pconstructor -> types
val type_of_constructors : env -> pinductive -> types array
(** Return constructor types in normal form *)
val arities_of_constructors : env -> pinductive -> types array
(** An inductive type with its parameters (transparently supports
reasoning either with only recursively uniform parameters or with all
parameters including the recursively non-uniform ones *)
type inductive_family
val make_ind_family : inductive puniverses * constr list -> inductive_family
val dest_ind_family : inductive_family -> inductive puniverses * constr list
val map_ind_family : (constr -> constr) -> inductive_family -> inductive_family
val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
val lift_inductive_family : int -> inductive_family -> inductive_family
val substnl_ind_family :
constr list -> int -> inductive_family -> inductive_family
(** An inductive type with its parameters and real arguments *)
type inductive_type = IndType of inductive_family * constr list
val make_ind_type : inductive_family * constr list -> inductive_type
val dest_ind_type : inductive_type -> inductive_family * constr list
val map_inductive_type : (constr -> constr) -> inductive_type -> inductive_type
val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
val lift_inductive_type : int -> inductive_type -> inductive_type
val substnl_ind_type : constr list -> int -> inductive_type -> inductive_type
val mkAppliedInd : inductive_type -> constr
val mis_is_recursive_subset : int list -> wf_paths -> bool
val mis_is_recursive :
inductive * mutual_inductive_body * one_inductive_body -> bool
val mis_nf_constructor_type :
pinductive * mutual_inductive_body * one_inductive_body -> int -> constr
(** {6 Extract information from an inductive name} *)
(** @return number of constructors *)
val nconstructors : inductive -> int
val nconstructors_env : env -> inductive -> int
(** @return arity of constructors excluding parameters, excluding local defs *)
val constructors_nrealargs : inductive -> int array
val constructors_nrealargs_env : env -> inductive -> int array
(** @return arity of constructors excluding parameters, including local defs *)
val constructors_nrealdecls : inductive -> int array
val constructors_nrealdecls_env : env -> inductive -> int array
(** @return the arity, excluding params, excluding local defs *)
val inductive_nrealargs : inductive -> int
val inductive_nrealargs_env : env -> inductive -> int
(** @return the arity, excluding params, including local defs *)
val inductive_nrealdecls : inductive -> int
val inductive_nrealdecls_env : env -> inductive -> int
(** @return the arity, including params, excluding local defs *)
val inductive_nallargs : inductive -> int
val inductive_nallargs_env : env -> inductive -> int
(** @return the arity, including params, including local defs *)
val inductive_nalldecls : inductive -> int
val inductive_nalldecls_env : env -> inductive -> int
(** @return nb of params without local defs *)
val inductive_nparams : inductive -> int
val inductive_nparams_env : env -> inductive -> int
(** @return nb of params with local defs *)
val inductive_nparamdecls : inductive -> int
val inductive_nparamdecls_env : env -> inductive -> int
(** @return params context *)
val inductive_paramdecls : pinductive -> Context.Rel.t
val inductive_paramdecls_env : env -> pinductive -> Context.Rel.t
(** @return full arity context, hence with letin *)
val inductive_alldecls : pinductive -> Context.Rel.t
val inductive_alldecls_env : env -> pinductive -> Context.Rel.t
(** {7 Extract information from a constructor name} *)
(** @return param + args without letin *)
val constructor_nallargs : constructor -> int
val constructor_nallargs_env : env -> constructor -> int
(** @return param + args with letin *)
val constructor_nalldecls : constructor -> int
val constructor_nalldecls_env : env -> constructor -> int
(** @return args without letin *)
val constructor_nrealargs : constructor -> int
val constructor_nrealargs_env : env -> constructor -> int
(** @return args with letin *)
val constructor_nrealdecls : constructor -> int
val constructor_nrealdecls_env : env -> constructor -> int
(** Is there local defs in params or args ? *)
val constructor_has_local_defs : constructor -> bool
val inductive_has_local_defs : inductive -> bool
val allowed_sorts : env -> inductive -> sorts_family list
(** (Co)Inductive records with primitive projections do not have eta-conversion,
hence no dependent elimination. *)
val has_dependent_elim : mutual_inductive_body -> bool
(** Primitive projections *)
val projection_nparams : projection -> int
val projection_nparams_env : env -> projection -> int
val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
constr -> types -> types
(** Extract information from an inductive family *)
type constructor_summary = {
cs_cstr : pconstructor; (* internal name of the constructor plus universes *)
cs_params : constr list; (* parameters of the constructor in current ctx *)
cs_nargs : int; (* length of arguments signature (letin included) *)
cs_args : Context.Rel.t; (* signature of the arguments (letin included) *)
cs_concl_realargs : constr array; (* actual realargs in the concl of cstr *)
}
val lift_constructor : int -> constructor_summary -> constructor_summary
val get_constructor :
pinductive * mutual_inductive_body * one_inductive_body * constr list ->
int -> constructor_summary
val get_constructors : env -> inductive_family -> constructor_summary array
val get_projections : env -> inductive_family -> constant array option
(** [get_arity] returns the arity of the inductive family instantiated
with the parameters; if recursively non-uniform parameters are not
part of the inductive family, they appears in the arity *)
val get_arity : env -> inductive_family -> Context.Rel.t * sorts_family
val build_dependent_constructor : constructor_summary -> constr
val build_dependent_inductive : env -> inductive_family -> constr
val make_arity_signature : env -> bool -> inductive_family -> Context.Rel.t
val make_arity : env -> bool -> inductive_family -> sorts -> types
val build_branch_type : env -> bool -> constr -> constructor_summary -> types
(** Raise [Not_found] if not given a valid inductive type *)
val extract_mrectype : constr -> pinductive * constr list
val find_mrectype : env -> evar_map -> types -> pinductive * constr list
val find_mrectype_vect : env -> evar_map -> types -> pinductive * constr array
val find_rectype : env -> evar_map -> types -> inductive_type
val find_inductive : env -> evar_map -> types -> pinductive * constr list
val find_coinductive : env -> evar_map -> types -> pinductive * constr list
(********************)
(** Builds the case predicate arity (dependent or not) *)
val arity_of_case_predicate :
env -> inductive_family -> bool -> sorts -> types
val type_case_branches_with_names :
env -> pinductive * constr list -> constr -> constr -> types array * types
(** Annotation for cases *)
val make_case_info : env -> inductive -> case_style -> case_info
(** Make a case or substitute projections if the inductive type is a record
with primitive projections.
Fail with an error if the elimination is dependent while the
inductive type does not allow dependent elimination. *)
val make_case_or_project :
env -> inductive_family -> case_info ->
(* pred *) constr -> (* term *) constr -> (* branches *) constr array -> constr
(*i Compatibility
val make_default_case_info : env -> case_style -> inductive -> case_info
i*)
(********************)
val type_of_inductive_knowing_conclusion :
env -> evar_map -> Inductive.mind_specif puniverses -> types -> evar_map * types
(********************)
val control_only_guard : env -> types -> unit
|
