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
|
(* $Id$ *)
open Util
open Names
open Univ
open Generic
open Term
open Sign
type recarg =
| Param of int
| Norec
| Mrec of int
| Imbr of inductive_path * recarg list
type mutual_inductive_packet = {
mind_consnames : identifier array;
mind_typename : identifier;
mind_lc : constr;
mind_arity : typed_type;
mind_kelim : sorts list;
mind_listrec : (recarg list) array;
mind_finite : bool }
type mutual_inductive_body = {
mind_kind : path_kind;
mind_ntypes : int;
mind_hyps : typed_type signature;
mind_packets : mutual_inductive_packet array;
mind_constraints : constraints;
mind_singl : constr option;
mind_nparams : int }
let mind_type_finite mib i = mib.mind_packets.(i).mind_finite
type mind_specif = {
mis_sp : section_path;
mis_mib : mutual_inductive_body;
mis_tyi : int;
mis_args : constr array;
mis_mip : mutual_inductive_packet }
let mis_ntypes mis = mis.mis_mib.mind_ntypes
let mis_nconstr mis = Array.length (mis.mis_mip.mind_consnames)
let mis_nparams mis = mis.mis_mib.mind_nparams
let mis_kelim mis = mis.mis_mip.mind_kelim
let mis_recargs mis =
Array.map (fun mip -> mip.mind_listrec) mis.mis_mib.mind_packets
let mis_recarg mis = mis.mis_mip.mind_listrec
let mis_typename mis = mis.mis_mip.mind_typename
let mis_consnames mis = mis.mis_mip.mind_consnames
type constructor_summary = {
cs_cstr : constructor;
cs_params : constr list;
cs_nargs : int;
cs_args : (name * constr) list;
cs_concl_realargs : constr array
}
(* A light version of mind_specif_of_mind with pre-splitted args *)
(* and a receipt to build a summary of constructors *)
type inductive_summary = {
fullmind : constr;
mind : inductive;
params : constr list;
realargs : constr list;
nparams : int;
nrealargs : int;
nconstr : int;
make_arity : inductive -> constr list -> (name * constr) list * sorts;
make_constrs : inductive -> constr list -> constructor_summary array
}
let is_recursive listind =
let rec one_is_rec rvec =
List.exists (function
| Mrec(i) -> List.mem i listind
| Imbr(_,lvec) -> one_is_rec lvec
| Norec -> false
| Param(_) -> false) rvec
in
array_exists one_is_rec
let mis_is_recursive mis =
is_recursive (interval 0 ((mis_ntypes mis)-1)) (mis_recarg mis)
let mind_nth_type_packet mib n = mib.mind_packets.(n)
(*s Declaration. *)
type mutual_inductive_entry = {
mind_entry_nparams : int;
mind_entry_finite : bool;
mind_entry_inds : (identifier * constr * identifier list * constr) list }
type inductive_error =
| NonPos of name list * constr * constr
| NotEnoughArgs of name list * constr * constr
| NotConstructor of name list * constr * constr
| NonPar of name list * constr * int * constr * constr
| SameNamesTypes of identifier
| SameNamesConstructors of identifier * identifier
| NotAnArity of identifier
| BadEntry
exception InductiveError of inductive_error
(* [check_constructors_names id s cl] checks that all the constructors names
appearing in [l] are not present in the set [s], and returns the new set
of names. The name [id] is the name of the current inductive type, used
when reporting the error. *)
let check_constructors_names id =
let rec check idset = function
| [] -> idset
| c::cl ->
if Idset.mem c idset then
raise (InductiveError (SameNamesConstructors (id,c)))
else
check (Idset.add c idset) cl
in
check
(* [mind_check_names mie] checks the names of an inductive types declaration,
and raises the corresponding exceptions when two types or two constructors
have the same name. *)
let mind_check_names mie =
let rec check indset cstset = function
| [] -> ()
| (id,_,cl,_)::inds ->
if Idset.mem id indset then
raise (InductiveError (SameNamesTypes id))
else
let cstset' = check_constructors_names id cstset cl in
check (Idset.add id indset) cstset' inds
in
check Idset.empty Idset.empty mie.mind_entry_inds
(* [mind_extract_params mie] extracts the params from an inductive types
declaration, and checks that they are all present (and all the same)
for all the given types. *)
let mind_extract_params n c =
let (l,c') = decompose_prod_n n c in (List.rev l,c')
let extract nparams c =
try mind_extract_params nparams c
with UserError _ -> raise (InductiveError BadEntry)
let check_params nparams params c =
let eparams = fst (extract nparams c) in
try
List.iter2
(fun (n1,t1) (n2,t2) ->
if n1 <> n2 || strip_all_casts t1 <> strip_all_casts t2 then
raise (InductiveError BadEntry))
eparams params
with Invalid_argument _ ->
raise (InductiveError BadEntry)
let mind_extract_and_check_params mie =
let nparams = mie.mind_entry_nparams in
match mie.mind_entry_inds with
| [] -> anomaly "empty inductive types declaration"
| (_,ar,_,_)::l ->
let (params,_) = extract nparams ar in
List.iter (fun (_,c,_,_) -> check_params nparams params c) l;
params
let mind_check_lc params mie =
let ntypes = List.length mie.mind_entry_inds in
let nparams = List.length params in
let check_lc (_,_,_,lc) =
let (lna,c) = decomp_all_DLAMV_name lc in
Array.iter (check_params nparams params) c;
if not (List.length lna = ntypes) then raise (InductiveError BadEntry)
in
List.iter check_lc mie.mind_entry_inds
let inductive_path_of_constructor_path (ind_sp,i) = ind_sp
let ith_constructor_path_of_inductive_path ind_sp i = (ind_sp,i)
let inductive_of_constructor ((ind_sp,i),args) = (ind_sp,args)
let ith_constructor_of_inductive (ind_sp,args) i = ((ind_sp,i),args)
let build_dependent_constructor cs =
applist
(mkMutConstruct cs.cs_cstr,
(List.map (lift cs.cs_nargs) cs.cs_params)@(rel_list 0 cs.cs_nargs))
let build_dependent_inductive is =
applist
(mkMutInd is.mind,
(List.map (lift is.nparams) is.params)@(rel_list 0 is.nrealargs))
|
