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
|
(************************************************************************)
(* * 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 Names
open Constr
open Univ
open UVars
open Declarations
open Environ
open CClosure
(** {6 Extracting an inductive type from a construction } *)
(** [find_m*type env sigma c] coerce [c] to an recursive type (I args).
[find_rectype], [find_inductive] and [find_coinductive]
respectively accepts any recursive type, only an inductive type and
only a coinductive type.
They raise [Not_found] if not convertible to a recursive type. *)
val find_rectype : ?evars:evar_handler -> env -> types -> pinductive * constr list
val find_inductive : ?evars:evar_handler -> env -> types -> pinductive * constr list
val find_coinductive : ?evars:evar_handler -> env -> types -> pinductive * constr list
(** {6 ... } *)
(** Fetching information in the environment about an inductive type.
Raises an anomaly if the inductive type is not found. *)
val lookup_mind_specif : env -> inductive -> mind_specif
(** {6 Functions to build standard types related to inductive } *)
(** Returns the parameters of an inductive type with universes instantiated *)
val inductive_paramdecls : mutual_inductive_body puniverses -> Constr.rel_context
(** Returns the parameters of an inductive type with universes
instantiated, splitting it into the contexts of recursively
uniform and recursively non-uniform parameters *)
val inductive_nonrec_rec_paramdecls : mutual_inductive_body puniverses -> Constr.rel_context * Constr.rel_context
val instantiate_inductive_constraints :
mutual_inductive_body -> Instance.t -> Constraints.t
type template_univ =
| TemplateProp
| TemplateUniv of Universe.t
type param_univs = (expected:Univ.Level.t -> template_univ) list
val constrained_type_of_inductive : mind_specif puniverses -> types constrained
val constrained_type_of_inductive_knowing_parameters :
mind_specif puniverses -> param_univs -> types constrained
val relevance_of_ind_body : one_inductive_body -> UVars.Instance.t -> Sorts.relevance
val relevance_of_inductive : env -> pinductive -> Sorts.relevance
val type_of_inductive : mind_specif puniverses -> types
val type_of_inductive_knowing_parameters :
?polyprop:bool -> mind_specif puniverses -> param_univs -> types
val quality_leq : Sorts.Quality.t -> Sorts.Quality.t -> bool
(** For squashing. *)
type squash = SquashToSet | SquashToQuality of Sorts.Quality.t
val is_squashed : mind_specif puniverses -> squash option
val is_allowed_elimination : mind_specif puniverses -> Sorts.t -> bool
val is_private : mind_specif -> bool
val is_primitive_record : mind_specif -> bool
(** Return type as quoted by the user *)
val constrained_type_of_constructor : pconstructor -> mind_specif -> types constrained
val type_of_constructor : pconstructor -> mind_specif -> types
(** Return constructor types in normal form *)
val arities_of_constructors : pinductive -> mind_specif -> types array
(** Return constructor types in user form *)
val type_of_constructors : pinductive -> mind_specif -> types array
(** Turns a constructor type recursively referring to inductive types
into the same constructor type referring instead to a context made
from the abstract declaration of the inductive types (e.g. turns
[nat->nat] into [mkArrowR (Rel 1) (Rel 2)]); takes as arguments the number
of inductive types in the block and the name of the block *)
val abstract_constructor_type_relatively_to_inductive_types_context :
int -> MutInd.t -> types -> types
val inductive_params : mind_specif -> int
(** Given an inductive type and its parameters, builds the context of the return
clause, including the inductive being eliminated. The additional binder
array is only used to set the names of the context variables, we use the
less general type to make it easy to use this function on Case nodes. *)
val expand_arity : mind_specif -> pinductive -> constr array ->
Name.t binder_annot array -> rel_context
(** Given an inductive type and its parameters, builds the context of the return
clause, including the inductive being eliminated. The additional binder
array is only used to set the names of the context variables, we use the
less general type to make it easy to use this function on Case nodes. *)
val expand_branch_contexts : mind_specif -> UVars.Instance.t -> constr array ->
(Name.t binder_annot array * 'a) array -> rel_context array
type ('constr,'types,'r) pexpanded_case =
(case_info * ('constr * 'r) * 'constr pcase_invert * 'constr * 'constr array)
type expanded_case = (constr,types,Sorts.relevance) pexpanded_case
(** Given a pattern-matching represented compactly, expands it so as to produce
lambda and let abstractions in front of the return clause and the pattern
branches. *)
val expand_case : env -> case -> expanded_case
val expand_case_specif : mutual_inductive_body -> case -> expanded_case
(** Dual operation of the above. Fails if the return clause or branch has not
the expected form. *)
val contract_case : env -> expanded_case -> case
(** [instantiate_context u subst nas ctx] applies both [u] and [subst]
to [ctx] while replacing names using [nas] (order reversed). In particular,
assumes that [ctx] and [nas] have the same length. *)
val instantiate_context : Instance.t -> Vars.substl -> Name.t binder_annot array ->
rel_context -> rel_context
val build_branches_type :
pinductive -> mutual_inductive_body * one_inductive_body ->
constr list -> constr -> types array
(** Check a [case_info] actually correspond to a Case expression on the
given inductive type. *)
val check_case_info : env -> pinductive -> case_info -> unit
(** {6 Guard conditions for fix and cofix-points. } *)
(** [is_primitive_positive_container env c] tells if the constant [c] is
registered as a primitive type that can be seen as a container where the
occurrences of its parameters are positive, in which case the positivity and
guard conditions are extended to allow inductive types to nest their subterms
in these containers. *)
val is_primitive_positive_container : env -> Constant.t -> bool
(** When [chk] is false, the guard condition is not actually
checked. *)
val check_fix : ?evars:evar_handler -> env -> fixpoint -> unit
val check_cofix : ?evars:evar_handler -> env -> cofixpoint -> unit
(** {6 Support for sort-polymorphic inductive types } *)
(** The "polyprop" optional argument below controls
the "Prop-polymorphism". By default, it is allowed.
But when "polyprop=false", the following exception is raised
when a polymorphic singleton inductive type becomes Prop due to
parameter instantiation. This is used by the Ocaml extraction,
which cannot handle (yet?) Prop-polymorphism. *)
exception SingletonInductiveBecomesProp of Id.t
val abstract_mind_lc : int -> int -> MutInd.t -> (rel_context * constr) array -> constr array
|
