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: mod_typing.ml 11514 2008-10-28 13:39:02Z soubiran $ i*)
24
let path_of_mexpr = function
28
let rec list_split_assoc k rev_before = function
29
| [] -> raise Not_found
30
| (k',b)::after when k=k' -> rev_before,b,after
31
| h::tail -> list_split_assoc k (h::rev_before) tail
33
let rec list_fold_map2 f e = function
36
let e',h1',h2' = f e h in
37
let e'',t1',t2' = list_fold_map2 f e' t in
40
let rec rebuild_mp mp l =
43
| i::r -> rebuild_mp (MPdot(mp,i)) r
45
let type_of_struct env b meb =
46
let rec aux env = function
47
| SEBfunctor (mp,mtb,body) ->
48
let env = add_module (MPbound mp) (module_body_of_type mtb) env in
49
SEBfunctor(mp,mtb, aux env body)
51
strengthen env (lookup_modtype mp env).typ_expr mp
52
| SEBapply _ as mtb -> eval_struct env mtb
60
let rec bounded_str_expr = function
61
| SEBfunctor (mp,mtb,body) -> bounded_str_expr body
62
| SEBident mp -> (check_bound_mp mp)
63
| SEBapply (f,a,_)->(bounded_str_expr f)
66
let return_opt_type mp env mtb =
67
if (check_bound_mp mp) then
68
Some (strengthen env mtb.typ_expr mp)
72
let rec check_with env mtb with_decl =
74
| With_Definition (id,_) ->
75
let cb = check_with_aux_def env mtb with_decl in
76
SEBwith(mtb,With_definition_body(id,cb)),empty_subst
77
| With_Module (id,mp) ->
78
let cst,sub,typ_opt = check_with_aux_mod env mtb with_decl true in
79
SEBwith(mtb,With_module_body(id,mp,typ_opt,cst)),sub
81
and check_with_aux_def env mtb with_decl =
82
let msid,sig_b = match (eval_struct env mtb) with
83
| SEBstruct(msid,sig_b) ->
85
| _ -> error_signature_expected mtb
87
let id,idl = match with_decl with
88
| With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
89
| With_Definition ([],_) | With_Module ([],_) -> assert false
91
let l = label_of_id id in
93
let rev_before,spec,after = list_split_assoc l [] sig_b in
94
let before = List.rev rev_before in
95
let env' = Modops.add_signature (MPself msid) before env in
97
| With_Definition ([],_) -> assert false
98
| With_Definition ([id],c) ->
99
let cb = match spec with
101
| _ -> error_not_a_constant l
104
match cb.const_body with
106
let (j,cst1) = Typeops.infer env' c in
107
let typ = Typeops.type_of_constant_type env' cb.const_type in
108
let cst2 = Reduction.conv_leq env' j.uj_type typ in
111
(Constraint.union cb.const_constraints cst1)
113
let body = Some (Declarations.from_val j.uj_val) in
116
const_body_code = Cemitcodes.from_val
117
(compile_constant_body env' body false false);
118
const_constraints = cst} in
121
let cst1 = Reduction.conv env' c (Declarations.force b) in
122
let cst = Constraint.union cb.const_constraints cst1 in
123
let body = Some (Declarations.from_val c) in
126
const_body_code = Cemitcodes.from_val
127
(compile_constant_body env' body false false);
128
const_constraints = cst} in
131
| With_Definition (_::_,_) ->
132
let old = match spec with
134
| _ -> error_not_a_module (string_of_label l)
137
match old.mod_expr with
139
let new_with_decl = match with_decl with
140
With_Definition (_,c) -> With_Definition (idl,c)
141
| With_Module (_,c) -> With_Module (idl,c) in
142
check_with_aux_def env' (type_of_mb env old) new_with_decl
144
error_a_generative_module_expected l
146
| _ -> anomaly "Modtyping:incorrect use of with"
148
Not_found -> error_no_such_label l
149
| Reduction.NotConvertible -> error_with_incorrect l
151
and check_with_aux_mod env mtb with_decl now =
152
let initmsid,msid,sig_b = match (eval_struct env mtb) with
153
| SEBstruct(msid,sig_b) ->let msid'=(refresh_msid msid) in
154
msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b)
155
| _ -> error_signature_expected mtb
157
let id,idl = match with_decl with
158
| With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
159
| With_Definition ([],_) | With_Module ([],_) -> assert false
161
let l = label_of_id id in
163
let rev_before,spec,after = list_split_assoc l [] sig_b in
164
let before = List.rev rev_before in
165
let rec mp_rec = function
166
| [] -> MPself initmsid
167
| i::r -> MPdot(mp_rec r,label_of_id i)
169
let env' = Modops.add_signature (MPself msid) before env in
171
| With_Module ([],_) -> assert false
172
| With_Module ([id], mp) ->
173
let old,alias = match spec with
174
SFBmodule msb -> Some msb,None
175
| SFBalias (mp',_,cst) -> None,Some (mp',cst)
176
| _ -> error_not_a_module (string_of_label l)
178
let mtb' = lookup_modtype mp env' in
184
(check_subtypes env' mtb' (module_type_of_module None msb))
186
with Failure _ -> error_with_incorrect (label_of_id id)
188
| None,Some (mp',None) ->
189
check_modpath_equiv env' mp mp';
191
| None,Some (mp',Some cst) ->
192
check_modpath_equiv env' mp mp';
195
anomaly "Mod_typing:no implementation and no alias"
198
let mp' = scrape_alias mp env' in
199
let _,sub = Modops.update_subst env' (module_body_of_type mtb') mp' in
200
let up_subst = update_subst sub (map_mp (mp_rec [id]) mp') in
201
cst, (join (map_mp (mp_rec [id]) mp') up_subst),(return_opt_type mp env' mtb')
203
cst,empty_subst,(return_opt_type mp env' mtb')
204
| With_Module (_::_,mp) ->
205
let old,alias = match spec with
206
SFBmodule msb -> Some msb, None
207
| SFBalias (mpold,typ_opt,cst)->None, Some mpold
208
| _ -> error_not_a_module (string_of_label l)
212
let old = Option.get old in
213
match old.mod_expr with
215
let new_with_decl = match with_decl with
216
With_Definition (_,c) ->
217
With_Definition (idl,c)
218
| With_Module (_,c) -> With_Module (idl,c) in
220
check_with_aux_mod env'
221
(type_of_mb env' old) new_with_decl false in
223
let mtb' = lookup_modtype mp env' in
224
let mp' = scrape_alias mp env' in
225
let _,sub = Modops.update_subst env' (module_body_of_type mtb') mp' in
226
let up_subst = update_subst
227
sub (map_mp (mp_rec (List.rev (id::idl))) mp') in
229
(join (map_mp (mp_rec (List.rev (id::idl))) mp') up_subst),
232
cst,empty_subst,typ_opt
234
error_a_generative_module_expected l
236
let mpold = Option.get alias in
237
let mpnew = rebuild_mp mpold (List.map label_of_id idl) in
238
check_modpath_equiv env' mpnew mp;
239
let mtb' = lookup_modtype mp env' in
240
Constraint.empty,empty_subst,(return_opt_type mp env' mtb')
242
| _ -> anomaly "Modtyping:incorrect use of with"
244
Not_found -> error_no_such_label l
245
| Reduction.NotConvertible -> error_with_incorrect l
247
and translate_module env me =
248
match me.mod_entry_expr, me.mod_entry_type with
250
anomaly "Mod_typing.translate_module: empty type and expr in module entry"
252
let mtb,sub = translate_struct_entry env mte in
256
mod_constraints = Constraint.empty;
257
mod_retroknowledge = []}
259
let meb,sub1 = translate_struct_entry env mexpr in
260
let mod_typ,sub,cst =
261
match me.mod_entry_type with
263
(type_of_struct env (bounded_str_expr meb) meb)
264
,sub1,Constraint.empty
266
let mtb2,sub2 = translate_struct_entry env mte in
267
let cst = check_subtypes env
277
{ mod_type = mod_typ;
279
mod_constraints = cst;
281
mod_retroknowledge = []} (* spiwack: not so sure about that. It may
282
cause a bug when closing nested modules.
283
If it does, I don't really know how to
287
and translate_struct_entry env mse = match mse with
289
let mtb = lookup_modtype mp env in
290
SEBident mp,mtb.typ_alias
291
| MSEfunctor (arg_id, arg_e, body_expr) ->
292
let arg_b,sub = translate_struct_entry env arg_e in
297
let env' = add_module (MPbound arg_id) (module_body_of_type mtb) env in
298
let body_b,sub = translate_struct_entry env' body_expr in
299
SEBfunctor (arg_id, mtb, body_b),sub
300
| MSEapply (fexpr,mexpr) ->
301
let feb,sub1 = translate_struct_entry env fexpr in
302
let feb'= eval_struct env feb
304
let farg_id, farg_b, fbody_b = destr_functor env feb' in
307
let mp = scrape_alias (path_of_mexpr mexpr) env in
308
lookup_modtype mp env,mp
310
| Not_path -> error_application_to_not_path mexpr
311
(* place for nondep_supertype *) in
312
let meb,sub2= translate_struct_entry env (MSEident mp) in
313
if sub1 = empty_subst then
314
let cst = check_subtypes env mtb farg_b in
315
SEBapply(feb,meb,cst),sub1
317
let sub2 = match eval_struct env (SEBident mp) with
318
| SEBstruct (msid,sign) ->
320
(subst_key (map_msid msid mp) sub2)
323
let sub3 = join_alias sub1 (map_mbid farg_id mp None) in
324
let sub4 = update_subst sub2 sub3 in
325
let cst = check_subtypes env mtb farg_b in
326
SEBapply(feb,meb,cst),(join sub3 sub4)
327
| MSEwith(mte, with_decl) ->
328
let mtb,sub1 = translate_struct_entry env mte in
329
let mtb',sub2 = check_with env mtb with_decl in
333
let rec add_struct_expr_constraints env = function
336
| SEBfunctor (_,mtb,meb) ->
337
add_struct_expr_constraints
338
(add_modtype_constraints env mtb) meb
340
| SEBstruct (_,structure_body) ->
342
(fun env (l,item) -> add_struct_elem_constraints env item)
346
| SEBapply (meb1,meb2,cst) ->
347
Environ.add_constraints cst
348
(add_struct_expr_constraints
349
(add_struct_expr_constraints env meb1)
351
| SEBwith(meb,With_definition_body(_,cb))->
352
Environ.add_constraints cb.const_constraints
353
(add_struct_expr_constraints env meb)
354
| SEBwith(meb,With_module_body(_,_,_,cst))->
355
Environ.add_constraints cst
356
(add_struct_expr_constraints env meb)
358
and add_struct_elem_constraints env = function
359
| SFBconst cb -> Environ.add_constraints cb.const_constraints env
360
| SFBmind mib -> Environ.add_constraints mib.mind_constraints env
361
| SFBmodule mb -> add_module_constraints env mb
362
| SFBalias (mp,_,Some cst) -> Environ.add_constraints cst env
363
| SFBalias (mp,_,None) -> env
364
| SFBmodtype mtb -> add_modtype_constraints env mtb
366
and add_module_constraints env mb =
367
let env = match mb.mod_expr with
369
| Some meb -> add_struct_expr_constraints env meb
371
let env = match mb.mod_type with
374
add_struct_expr_constraints env mtb
376
Environ.add_constraints mb.mod_constraints env
378
and add_modtype_constraints env mtb =
379
add_struct_expr_constraints env mtb.typ_expr
382
let rec struct_expr_constraints cst = function
385
| SEBfunctor (_,mtb,meb) ->
386
struct_expr_constraints
387
(modtype_constraints cst mtb) meb
389
| SEBstruct (_,structure_body) ->
391
(fun cst (l,item) -> struct_elem_constraints cst item)
395
| SEBapply (meb1,meb2,cst1) ->
396
struct_expr_constraints
397
(struct_expr_constraints (Univ.Constraint.union cst1 cst) meb1)
399
| SEBwith(meb,With_definition_body(_,cb))->
400
struct_expr_constraints
401
(Univ.Constraint.union cb.const_constraints cst) meb
402
| SEBwith(meb,With_module_body(_,_,_,cst1))->
403
struct_expr_constraints (Univ.Constraint.union cst1 cst) meb
405
and struct_elem_constraints cst = function
408
| SFBmodule mb -> module_constraints cst mb
409
| SFBalias (mp,_,Some cst1) -> Univ.Constraint.union cst1 cst
410
| SFBalias (mp,_,None) -> cst
411
| SFBmodtype mtb -> modtype_constraints cst mtb
413
and module_constraints cst mb =
414
let cst = match mb.mod_expr with
416
| Some meb -> struct_expr_constraints cst meb in
417
let cst = match mb.mod_type with
419
| Some mtb -> struct_expr_constraints cst mtb in
420
Univ.Constraint.union mb.mod_constraints cst
422
and modtype_constraints cst mtb =
423
struct_expr_constraints cst mtb.typ_expr
426
let struct_expr_constraints = struct_expr_constraints Univ.Constraint.empty
427
let module_constraints = module_constraints Univ.Constraint.empty
added
removed
kernel/mod_typing.ml
