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: subtyping.ml 10664 2008-03-14 11:27:37Z soubiran $ i*)
26
(* This local type is used to subtype a constant with a constructor or
27
an inductive type. It can also be useful to allow reorderings in
30
| Constant of constant_body
31
| IndType of inductive * mutual_inductive_body
32
| IndConstr of constructor * mutual_inductive_body
33
| Module of module_body
34
| Modtype of module_type_body
35
| Alias of module_path * struct_expr_body option
37
(* adds above information about one mutual inductive: all types and
40
let add_nameobjects_of_mib ln mib map =
41
let add_nameobjects_of_one j oib map =
46
Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map)
50
Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map
52
array_fold_right_i add_nameobjects_of_one mib.mind_packets map
55
(* creates namedobject map for the whole signature *)
57
let make_label_map mp list =
58
let add_one (l,e) map =
59
let add_map obj = Labmap.add l obj map in
61
| SFBconst cb -> add_map (Constant cb)
63
add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map
64
| SFBmodule mb -> add_map (Module mb)
65
| SFBmodtype mtb -> add_map (Modtype mtb)
66
| SFBalias (mp,t,cst) -> add_map (Alias (mp,t))
68
List.fold_right add_one list Labmap.empty
70
let check_conv_error error f env a1 a2 =
74
NotConvertible -> error ()
76
(* for now we do not allow reorderings *)
77
let check_inductive env msid1 l info1 mib2 spec2 =
78
let kn = make_kn (MPself msid1) empty_dirpath l in
79
let error () = error_not_match l spec2 in
80
let check_conv f = check_conv_error error f in
83
| IndType ((_,0), mib) -> mib
86
let check_inductive_type env t1 t2 =
88
(* Due to sort-polymorphism in inductive types, the conclusions of
89
t1 and t2, if in Type, are generated as the least upper bounds
90
of the types of the constructors.
92
By monotonicity of the infered l.u.b. wrt subtyping (i.e. if X:U
93
|- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each
94
universe in the conclusion of t1 has an bounding universe in
95
the conclusion of t2, so that we don't need to check the
96
subtyping of the conclusions of t1 and t2.
98
Even if we'd like to recheck it, the inference of constraints
99
is not designed to deal with algebraic constraints of the form
100
max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy
101
to recheck it (in short, we would need the actual graph of
102
constraints as input while type checking is currently designed
103
to output a set of constraints instead) *)
105
(* So we cheat and replace the subtyping problem on algebraic
106
constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n)
107
(that we know are necessary true) by trivial constraints that
108
the constraint generator knows how to deal with *)
110
let (ctx1,s1) = dest_arity env t1 in
111
let (ctx2,s2) = dest_arity env t2 in
114
| Type _, Type _ -> (* shortcut here *) Prop Null, Prop Null
115
| (Prop _, Type _) | (Type _,Prop _) -> error ()
117
check_conv conv_leq env
118
(mkArity (ctx1,s1)) (mkArity (ctx2,s2))
121
let check_packet p1 p2 =
122
let check f = if f p1 <> f p2 then error () in
123
check (fun p -> p.mind_consnames);
124
check (fun p -> p.mind_typename);
127
(* user_lc ignored *)
128
(* user_arity ignored *)
129
check (fun p -> p.mind_nrealargs);
131
(* listrec ignored *)
134
(* params_ctxt done because part of the inductive types *)
135
(* Don't check the sort of the type if polymorphic *)
136
check_inductive_type env
137
(type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
139
let check_cons_types i p1 p2 =
140
array_iter2 (check_conv conv env)
141
(arities_of_specif kn (mib1,p1))
142
(arities_of_specif kn (mib2,p2))
144
let check f = if f mib1 <> f mib2 then error () in
145
check (fun mib -> mib.mind_finite);
146
check (fun mib -> mib.mind_ntypes);
147
assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]);
148
assert (Array.length mib1.mind_packets >= 1
149
&& Array.length mib2.mind_packets >= 1);
151
(* Check that the expected numbers of uniform parameters are the same *)
152
(* No need to check the contexts of parameters: it is checked *)
153
(* at the time of checking the inductive arities in check_packet. *)
154
(* Notice that we don't expect the local definitions to match: only *)
155
(* the inductive types and constructors types have to be convertible *)
156
check (fun mib -> mib.mind_nparams);
159
match mib2.mind_equiv with
162
let kn2 = scrape_mind env kn2' in
163
let kn1 = match mib1.mind_equiv with
165
| Some kn1' -> scrape_mind env kn1'
167
if kn1 <> kn2 then error ()
169
(* we check that records and their field names are preserved. *)
170
check (fun mib -> mib.mind_record);
171
if mib1.mind_record then begin
172
let rec names_prod_letin t = match t with
173
| Prod(n,_,t) -> n::(names_prod_letin t)
174
| LetIn(n,_,_,t) -> n::(names_prod_letin t)
175
| Cast(t,_,_) -> names_prod_letin t
178
assert (Array.length mib1.mind_packets = 1);
179
assert (Array.length mib2.mind_packets = 1);
180
assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1);
181
assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1);
182
check (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0));
184
(* we first check simple things *)
185
array_iter2 check_packet mib1.mind_packets mib2.mind_packets;
186
(* and constructor types in the end *)
187
let _ = array_map2_i check_cons_types mib1.mind_packets mib2.mind_packets
190
let check_constant env msid1 l info1 cb2 spec2 =
191
let error () = error_not_match l spec2 in
192
let check_conv f = check_conv_error error f in
193
let check_type env t1 t2 =
195
(* If the type of a constant is generated, it may mention
196
non-variable algebraic universes that the general conversion
197
algorithm is not ready to handle. Anyway, generated types of
198
constants are functions of the body of the constant. If the
199
bodies are the same in environments that are subtypes one of
200
the other, the types are subtypes too (i.e. if Gamma <= Gamma',
201
Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
202
Hence they don't have to be checked again *)
206
let (ctx2,s2) = destArity t2 in
208
| Type v when not (is_univ_variable v) ->
209
(* The type in the interface is inferred and is made of algebraic
212
let (ctx1,s1) = dest_arity env t1 in
214
| Type u when not (is_univ_variable u) ->
215
(* Both types are inferred, no need to recheck them. We
216
cheat and collapse the types to Prop *)
217
mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
219
(* The type in the interface is inferred, it may be the case
220
that the type in the implementation is smaller because
221
the body is more reduced. We safely collapse the upper
223
mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
225
(* The type in the interface is inferred and the type in the
226
implementation is not inferred or is inferred but from a
227
more reduced body so that it is just a variable. Since
228
constraints of the form "univ <= max(...)" are not
229
expressible in the system of algebraic universes: we fail
230
(the user has to use an explicit type in the interface *)
232
with UserError _ (* "not an arity" *) ->
237
check_conv conv_leq env t1 t2
242
assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
243
(*Start by checking types*)
244
let typ1 = Typeops.type_of_constant_type env cb1.const_type in
245
let typ2 = Typeops.type_of_constant_type env cb2.const_type in
246
check_type env typ1 typ2;
247
let con = make_con (MPself msid1) empty_dirpath l in
249
| {const_body=Some lc2;const_opaque=false} ->
250
let c2 = force_constr lc2 in
251
let c1 = match cb1.const_body with
252
| Some lc1 -> force_constr lc1
255
check_conv conv env c1 c2
257
| IndType ((kn,i),mind1) ->
259
"The kernel does not recognize yet that a parameter can be " ^
260
"instantiated by an inductive type. Hint: you can rename the " ^
261
"inductive type and give a definition to map the old name to the new " ^
263
assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
264
if cb2.const_body <> None then error () ;
265
let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
266
let typ2 = Typeops.type_of_constant_type env cb2.const_type in
267
check_conv conv_leq env arity1 typ2
268
| IndConstr (((kn,i),j) as cstr,mind1) ->
270
"The kernel does not recognize yet that a parameter can be " ^
271
"instantiated by a constructor. Hint: you can rename the " ^
272
"constructor and give a definition to map the old name to the new " ^
274
assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
275
if cb2.const_body <> None then error () ;
276
let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
277
let ty2 = Typeops.type_of_constant_type env cb2.const_type in
278
check_conv conv env ty1 ty2
281
let rec check_modules env msid1 l msb1 msb2 =
282
let mp = (MPdot(MPself msid1,l)) in
283
let mty1 = module_type_of_module (Some mp) msb1 in
284
let mty2 = module_type_of_module None msb2 in
285
check_modtypes env mty1 mty2 false
288
and check_signatures env (msid1,sig1) alias (msid2,sig2') =
289
let mp1 = MPself msid1 in
290
let env = add_signature mp1 sig1 env in
291
let alias = update_subst_alias alias (map_msid msid2 mp1) in
292
let sig2 = subst_structure alias sig2' in
293
let sig2 = subst_signature_msid msid2 mp1 sig2 in
294
let map1 = make_label_map mp1 sig1 in
295
let check_one_body (l,spec2) =
300
Not_found -> error_no_such_label_sub l msid1 msid2
304
check_constant env msid1 l info1 cb2 spec2
306
check_inductive env msid1 l info1 mib2 spec2
310
| Module msb -> check_modules env msid1 l msb msb2
311
| Alias (mp,typ_opt) ->let msb =
312
{mod_expr = Some (SEBident mp);
314
mod_constraints = Constraint.empty;
315
mod_alias = (lookup_modtype mp env).typ_alias;
316
mod_retroknowledge = []} in
317
check_modules env msid1 l msb msb2
318
| _ -> error_not_match l spec2
320
| SFBalias (mp,typ_opt,_) ->
323
| Alias (mp1,_) -> check_modpath_equiv env mp mp1
326
{mod_expr = Some (SEBident mp);
328
mod_constraints = Constraint.empty;
329
mod_alias = (lookup_modtype mp env).typ_alias;
330
mod_retroknowledge = []} in
331
check_modules env msid1 l msb msb1
332
| _ -> error_not_match l spec2
338
| _ -> error_not_match l spec2
340
check_modtypes env mtb1 mtb2 true
342
List.iter check_one_body sig2
344
and check_modtypes env mtb1 mtb2 equiv =
345
if mtb1==mtb2 then () else (* just in case :) *)
347
(match mtb1.typ_strength with
348
None -> eval_struct env mtb1.typ_expr,
349
eval_struct env mtb2.typ_expr
350
| Some mp -> strengthen env mtb1.typ_expr mp,
351
eval_struct env mtb2.typ_expr) in
352
let rec check_structure env str1 str2 equiv =
353
match str1, str2 with
354
| SEBstruct (msid1,list1),
355
SEBstruct (msid2,list2) ->
357
(msid1,list1) mtb1.typ_alias (msid2,list2);
360
(msid2,list2) mtb2.typ_alias (msid1,list1)
361
| SEBfunctor (arg_id1,arg_t1,body_t1),
362
SEBfunctor (arg_id2,arg_t2,body_t2) ->
363
check_modtypes env arg_t2 arg_t1 equiv;
366
add_module (MPbound arg_id2) (module_body_of_type arg_t2) env
369
(* since we are just checking well-typedness we do not need
370
to expand any constant. Hence the identity resolver. *)
372
(map_mbid arg_id1 (MPbound arg_id2))
375
check_structure env (eval_struct env body_t1')
376
(eval_struct env body_t2) equiv
377
| _ , _ -> error_incompatible_modtypes mtb1 mtb2
379
if mtb1'== mtb2' then ()
380
else check_structure env mtb1' mtb2' equiv
382
let check_subtypes env sup super =
383
(*if sup<>super then*)
384
check_modtypes env sup super false
386
let check_equal env sup super =
387
(*if sup<>super then*)
388
check_modtypes env sup super true
added
removed
checker/subtyping.ml
