1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: inductive.mli 11301 2008-08-04 19:41:18Z herbelin $ i*)
19
(*s Extracting an inductive type from a construction *)
21
(* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
22
[find_rectype], [find_inductive] and [find_coinductive]
23
respectively accepts any recursive type, only an inductive type and
24
only a coinductive type.
25
They raise [Not_found] if not convertible to a recursive type. *)
27
val find_rectype : env -> types -> inductive * constr list
28
val find_inductive : env -> types -> inductive * constr list
29
val find_coinductive : env -> types -> inductive * constr list
31
type mind_specif = mutual_inductive_body * one_inductive_body
33
(*s Fetching information in the environment about an inductive type.
34
Raises [Not_found] if the inductive type is not found. *)
35
val lookup_mind_specif : env -> inductive -> mind_specif
37
(*s Functions to build standard types related to inductive *)
38
val ind_subst : mutual_inductive -> mutual_inductive_body -> constr list
40
val type_of_inductive : env -> mind_specif -> types
42
val elim_sorts : mind_specif -> sorts_family list
44
(* Return type as quoted by the user *)
45
val type_of_constructor : constructor -> mind_specif -> types
47
(* Return constructor types in normal form *)
48
val arities_of_constructors : inductive -> mind_specif -> types array
50
(* Return constructor types in user form *)
51
val type_of_constructors : inductive -> mind_specif -> types array
53
(* Transforms inductive specification into types (in nf) *)
54
val arities_of_specif : mutual_inductive -> mind_specif -> types array
57
(* [type_case_branches env (I,args) (p:A) c] computes useful types
58
about the following Cases expression:
59
<p>Cases (c :: (I args)) of b1..bn end
60
It computes the type of every branch (pattern variables are
61
introduced by products), the type for the whole expression, and
62
the universe constraints generated.
64
val type_case_branches :
65
env -> inductive * constr list -> unsafe_judgment -> constr
66
-> types array * types * constraints
68
(* Return the arity of an inductive type *)
69
val mind_arity : one_inductive_body -> Sign.rel_context * sorts_family
71
val inductive_sort_family : one_inductive_body -> sorts_family
73
(* Check a [case_info] actually correspond to a Case expression on the
74
given inductive type. *)
75
val check_case_info : env -> inductive -> case_info -> unit
77
(*s Guard conditions for fix and cofix-points. *)
78
val check_fix : env -> fixpoint -> unit
79
val check_cofix : env -> cofixpoint -> unit
81
(*s Support for sort-polymorphic inductive types *)
83
val type_of_inductive_knowing_parameters :
84
env -> one_inductive_body -> types array -> types
86
val max_inductive_sort : sorts array -> universe
88
val instantiate_universes : env -> Sign.rel_context ->
89
polymorphic_arity -> types array -> Sign.rel_context * sorts
91
(***************************************************************)
94
type size = Large | Strict
96
Subterm of (size * wf_paths)
101
(* dB of last fixpoint *)
103
(* inductive of recarg of each fixpoint *)
104
inds : inductive array;
105
(* the recarg information of inductive family *)
106
recvec : wf_paths array;
107
(* dB of variables denoting subterms *)
108
genv : subterm_spec list;
111
val subterm_specif : guard_env -> constr -> subterm_spec
112
val case_branches_specif : guard_env -> subterm_spec -> inductive ->
113
constr array -> (guard_env * constr) array