blob: 8aaeee831b1d4fc92e865a02a7e51fba18048636 (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
open Constr
open Univ
open Declarations
open Environ
(** {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 : env -> types -> pinductive * constr list
val find_inductive : env -> types -> pinductive * constr list
val find_coinductive : env -> types -> pinductive * constr list
type mind_specif = mutual_inductive_body * one_inductive_body
(** {6 ... } *)
(** Fetching information in the environment about an inductive type.
Raises [Not_found] if the inductive type is not found. *)
val lookup_mind_specif : env -> inductive -> mind_specif
(** {6 Functions to build standard types related to inductive } *)
val ind_subst : MutInd.t -> mutual_inductive_body -> Instance.t -> constr list
val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t
val instantiate_inductive_constraints :
mutual_inductive_body -> Instance.t -> Constraint.t
val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained
val constrained_type_of_inductive_knowing_parameters :
env -> mind_specif puniverses -> types Lazy.t array -> types constrained
val type_of_inductive : env -> mind_specif puniverses -> types
val type_of_inductive_knowing_parameters :
env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types
val elim_sorts : mind_specif -> Sorts.family list
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
(** Transforms inductive specification into types (in nf) *)
val arities_of_specif : MutInd.t puniverses -> mind_specif -> types array
val inductive_params : mind_specif -> int
(** [type_case_branches env (I,args) (p:A) c] computes useful types
about the following Cases expression:
<p>Cases (c :: (I args)) of b1..bn end
It computes the type of every branch (pattern variables are
introduced by products), the type for the whole expression, and
the universe constraints generated.
*)
val type_case_branches :
env -> pinductive * constr list -> unsafe_judgment -> constr
-> types array * types
val build_branches_type :
pinductive -> mutual_inductive_body * one_inductive_body ->
constr list -> constr -> types array
(** Return the arity of an inductive type *)
val mind_arity : one_inductive_body -> Context.Rel.t * Sorts.family
val inductive_sort_family : one_inductive_body -> Sorts.family
(** 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. } *)
(** When [chk] is false, the guard condition is not actually
checked. *)
val check_fix : env -> fixpoint -> unit
val check_cofix : 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 max_inductive_sort : Sorts.t array -> Universe.t
val instantiate_universes : env -> Context.Rel.t ->
template_arity -> constr Lazy.t array -> Context.Rel.t * Sorts.t
(** {6 Debug} *)
type size = Large | Strict
type subterm_spec =
Subterm of (size * wf_paths)
| Dead_code
| Not_subterm
type guard_env =
{ env : env;
(** dB of last fixpoint *)
rel_min : int;
(** dB of variables denoting subterms *)
genv : subterm_spec Lazy.t list;
}
type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec
val lambda_implicit_lift : int -> constr -> constr
val abstract_mind_lc : int -> Int.t -> constr array -> constr array
|
