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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: declarations.ml,v 1.31.2.2 2005/11/29 21:40:51 letouzey Exp $ i*)
(*i*)
open Util
open Names
open Univ
open Term
open Sign
(*i*)
(* This module defines the types of global declarations. This includes
global constants/axioms and mutual inductive definitions *)
(*s Constants (internal representation) (Definition/Axiom) *)
type subst_internal =
| Constr of constr
| LazyConstr of substitution * constr
type constr_substituted = subst_internal ref
let from_val c = ref (Constr c)
let force cs = match !cs with
Constr c -> c
| LazyConstr (subst,c) ->
let c' = subst_mps subst c in
cs := Constr c';
c'
let subst_constr_subst subst cs = match !cs with
Constr c -> ref (LazyConstr (subst,c))
| LazyConstr (subst',c) ->
let subst'' = join subst' subst in
ref (LazyConstr (subst'',c))
type constant_body = {
const_hyps : section_context; (* New: younger hyp at top *)
const_body : constr_substituted option;
const_type : types;
const_constraints : constraints;
const_opaque : bool }
(*s Inductive types (internal representation with redundant
information). *)
type recarg =
| Norec
| Mrec of int
| Imbr of inductive
let subst_recarg sub r = match r with
| Norec | Mrec _ -> r
| Imbr (kn,i) -> let kn' = subst_kn sub kn in
if kn==kn' then r else Imbr (kn',i)
type wf_paths = recarg Rtree.t
let mk_norec = Rtree.mk_node Norec [||]
let mk_paths r recargs =
Rtree.mk_node r
(Array.map (fun l -> Rtree.mk_node Norec (Array.of_list l)) recargs)
let dest_recarg p = fst (Rtree.dest_node p)
let dest_subterms p =
let (_,cstrs) = Rtree.dest_node p in
Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs
let recarg_length p j =
let (_,cstrs) = Rtree.dest_node p in
Array.length (snd (Rtree.dest_node cstrs.(j-1)))
let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
(* [mind_typename] is the name of the inductive; [mind_arity] is
the arity generalized over global parameters; [mind_lc] is the list
of types of constructors generalized over global parameters and
relative to the global context enriched with the arities of the
inductives *)
type one_inductive_body = {
mind_typename : identifier;
mind_nparams : int;
mind_params_ctxt : rel_context;
mind_nrealargs : int;
mind_nf_arity : types;
mind_user_arity : types;
mind_sort : sorts;
mind_kelim : sorts_family list;
mind_consnames : identifier array;
mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *)
mind_user_lc : types array;
mind_recargs : wf_paths;
}
type mutual_inductive_body = {
mind_record : bool;
mind_finite : bool;
mind_ntypes : int;
mind_hyps : section_context;
mind_packets : one_inductive_body array;
mind_constraints : constraints;
mind_equiv : kernel_name option
}
(* TODO: should be changed to non-coping after Term.subst_mps *)
let subst_const_body sub cb =
{ const_body = option_app (subst_constr_subst sub) cb.const_body;
const_type = type_app (Term.subst_mps sub) cb.const_type;
const_hyps = (assert (cb.const_hyps=[]); []);
const_constraints = cb.const_constraints;
const_opaque = cb.const_opaque}
let subst_mind_packet sub mbp =
{ mind_consnames = mbp.mind_consnames;
mind_typename = mbp.mind_typename;
mind_nf_lc =
array_smartmap (type_app (Term.subst_mps sub)) mbp.mind_nf_lc;
mind_nf_arity = type_app (Term.subst_mps sub) mbp.mind_nf_arity;
mind_user_lc =
array_smartmap (type_app (Term.subst_mps sub)) mbp.mind_user_lc;
mind_user_arity = type_app (Term.subst_mps sub) mbp.mind_user_arity;
mind_sort = mbp.mind_sort;
mind_nrealargs = mbp.mind_nrealargs;
mind_kelim = mbp.mind_kelim;
mind_nparams = mbp.mind_nparams;
mind_params_ctxt =
map_rel_context (Term.subst_mps sub) mbp.mind_params_ctxt;
mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
}
let subst_mind sub mib =
{ mind_record = mib.mind_record ;
mind_finite = mib.mind_finite ;
mind_ntypes = mib.mind_ntypes ;
mind_hyps = (assert (mib.mind_hyps=[]); []) ;
mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
mind_constraints = mib.mind_constraints ;
mind_equiv = option_app (subst_kn sub) mib.mind_equiv;
}
(*s Modules: signature component specifications, module types, and
module declarations *)
type specification_body =
| SPBconst of constant_body
| SPBmind of mutual_inductive_body
| SPBmodule of module_specification_body
| SPBmodtype of module_type_body
and module_signature_body = (label * specification_body) list
and module_type_body =
| MTBident of kernel_name
| MTBfunsig of mod_bound_id * module_type_body * module_type_body
| MTBsig of mod_self_id * module_signature_body
and module_specification_body =
{ msb_modtype : module_type_body;
msb_equiv : module_path option;
msb_constraints : constraints }
type structure_elem_body =
| SEBconst of constant_body
| SEBmind of mutual_inductive_body
| SEBmodule of module_body
| SEBmodtype of module_type_body
and module_structure_body = (label * structure_elem_body) list
and module_expr_body =
| MEBident of module_path
| MEBfunctor of mod_bound_id * module_type_body * module_expr_body
| MEBstruct of mod_self_id * module_structure_body
| MEBapply of module_expr_body * module_expr_body
* constraints
and module_body =
{ mod_expr : module_expr_body option;
mod_user_type : module_type_body option;
mod_type : module_type_body;
mod_equiv : module_path option;
mod_constraints : constraints }
|
