blob: 204f506a63ac61909559dfddde5f7ad2abce1d35 (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
open Term
open Context
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 -> inductive -> types
(** Return type as quoted by the user *)
val type_of_constructor : env -> constructor -> types
val type_of_constructors : env -> inductive -> types array
(** Return constructor types in normal form *)
val arities_of_constructors : env -> inductive -> types array
(** An inductive type with its parameters *)
type inductive_family
val make_ind_family : inductive * constr list -> inductive_family
val dest_ind_family : inductive_family -> inductive * 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 :
inductive * mutual_inductive_body * one_inductive_body -> int -> constr
(** {6 Extract information from an inductive name}
Functions without env lookup in the globalenv. *)
(** Arity of constructors excluding parameters and local defs *)
val mis_constr_nargs : inductive -> int array
val mis_constr_nargs_env : env -> inductive -> int array
val nconstructors : inductive -> int
(** @return the lengths of parameters signature and real arguments signature
with letin *)
val inductive_nargs : inductive -> int * int
val inductive_nargs_env : env -> inductive -> int * int
(** @return nb of params without letin *)
val inductive_nparams : inductive -> int
(** @return param + args without letin *)
val mis_constructor_nargs : constructor -> int
val mis_constructor_nargs_env : env -> constructor -> int
(** @return param + args with letin *)
val mis_constructor_nhyps : constructor -> int
val mis_constructor_nhyps_env : env -> constructor -> int
(** @return args without letin *)
val constructor_nrealargs : env -> constructor -> int
(** @return args with letin *)
val constructor_nrealhyps : constructor -> int
(** Is there local defs in params or args ? *)
val mis_constructor_has_local_defs : constructor -> bool
val inductive_has_local_defs : inductive -> bool
val get_full_arity_sign : env -> inductive -> rel_context
val allowed_sorts : env -> inductive -> sorts_family list
(** Extract information from an inductive family *)
type constructor_summary = {
cs_cstr : constructor; (* internal name of the constructor *)
cs_params : constr list; (* parameters of the constructor in current ctx *)
cs_nargs : int; (* length of arguments signature (letin included) *)
cs_args : rel_context; (* 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 :
inductive * mutual_inductive_body * one_inductive_body * constr list ->
int -> constructor_summary
val get_arity : env -> inductive_family -> rel_context * sorts_family
val get_constructors : env -> inductive_family -> constructor_summary array
val build_dependent_constructor : constructor_summary -> constr
val build_dependent_inductive : env -> inductive_family -> constr
val make_arity_signature : env -> bool -> inductive_family -> rel_context
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 an valid inductive type *)
val extract_mrectype : constr -> inductive * constr list
val find_mrectype : env -> evar_map -> types -> inductive * constr list
val find_rectype : env -> evar_map -> types -> inductive_type
val find_inductive : env -> evar_map -> types -> inductive * constr list
val find_coinductive : env -> evar_map -> types -> inductive * 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 -> inductive * constr list -> constr -> constr ->
types array * types
(** Annotation for cases *)
val make_case_info : env -> inductive -> case_style -> case_info
(*i Compatibility
val make_default_case_info : env -> case_style -> inductive -> case_info
i*)
(********************)
val type_of_inductive_knowing_conclusion :
env -> one_inductive_body -> types -> types
(********************)
val control_only_guard : env -> types -> unit
val subst_inductive : Mod_subst.substitution -> inductive -> inductive
|
