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
|
(* $Id$ *)
open Util
open Names
open Univ
open Generic
open Term
open Sign
type recarg =
| Param of int
| Norec
| Mrec of int
| Imbr of section_path * int * (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 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 int
| NotEnoughArgs of int
| NotConstructor
| NonPar of int * int
| 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 = decompose_prod_n
let extract nparams c =
try mind_extract_params nparams c
with UserError _ -> raise (InductiveError (NotEnoughArgs nparams))
let check_params nparams params c =
if not (fst (extract nparams c) = params) then
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
|
