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: modops.ml 11923 2009-02-13 12:20:27Z soubiran $ i*)
24
let error_existing_label l =
25
error ("The label "^string_of_label l^" is already declared.")
27
let error_declaration_not_path _ = error "Declaration is not a path."
29
let error_application_to_not_path _ = error "Application to not path."
31
let error_not_a_functor _ = error "Application of not a functor."
33
let error_incompatible_modtypes _ _ = error "Incompatible module types."
35
let error_not_equal _ _ = error "Non equal modules."
37
let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match.")
39
let error_no_such_label l = error ("No such label "^string_of_label l^".")
41
let error_incompatible_labels l l' =
42
error ("Opening and closing labels are not the same: "
43
^string_of_label l^" <> "^string_of_label l'^" !")
45
let error_result_must_be_signature () =
46
error "The result module type must be a signature."
48
let error_signature_expected mtb =
49
error "Signature expected."
51
let error_no_module_to_end _ =
52
error "No open module to end."
54
let error_no_modtype_to_end _ =
55
error "No open module type to end."
57
let error_not_a_modtype_loc loc s =
58
user_err_loc (loc,"",str ("\""^s^"\" is not a module type."))
60
let error_not_a_module_loc loc s =
61
user_err_loc (loc,"",str ("\""^s^"\" is not a module."))
63
let error_not_a_module s = error_not_a_module_loc dummy_loc s
65
let error_not_a_constant l =
66
error ("\""^(string_of_label l)^"\" is not a constant.")
68
let error_with_incorrect l =
69
error ("Incorrect constraint for label \""^(string_of_label l)^"\".")
71
let error_a_generative_module_expected l =
72
error ("The module " ^ string_of_label l ^ " is not generative. Only " ^
73
"component of generative modules can be changed using the \"with\" " ^
76
let error_local_context lo =
79
error ("The local context is not empty.")
81
error ("The local context of the component "^
82
(string_of_label l)^" is not empty.")
85
let error_no_such_label_sub l l1 l2 =
86
error (l1^" is not a subtype of "^l2^".\nThe field "^(string_of_label l)^" is missing in "^l1^".")
90
let rec list_split_assoc k rev_before = function
91
| [] -> raise Not_found
92
| (k',b)::after when k=k' -> rev_before,b,after
93
| h::tail -> list_split_assoc k (h::rev_before) tail
95
let path_of_seb = function
97
| _ -> anomaly "Modops: evaluation failed."
100
let destr_functor env mtb =
102
| SEBfunctor (arg_id,arg_t,body_t) ->
103
(arg_id,arg_t,body_t)
104
| _ -> error_not_a_functor mtb
106
(* the constraints are not important here *)
108
let module_body_of_type mtb =
109
{ mod_type = Some mtb.typ_expr;
111
mod_constraints = Constraint.empty;
112
mod_alias = mtb.typ_alias;
113
mod_retroknowledge = []}
115
let module_type_of_module mp mb =
117
(match mb.mod_type with
118
| Some expr -> mp,expr
119
| None -> (match mb.mod_expr with
120
| Some (SEBident mp') ->(Some mp'),(SEBident mp')
121
| Some expr -> mp,expr
123
anomaly "Modops: empty expr and type")) in
125
typ_alias = mb.mod_alias;
129
let rec check_modpath_equiv env mp1 mp2 =
130
if mp1=mp2 then () else
131
let mp1 = scrape_alias mp1 env in
132
let mp2 = scrape_alias mp2 env in
135
error_not_equal mp1 mp2
137
let rec subst_with_body sub = function
138
| With_module_body(id,mp,typ_opt,cst) ->
139
With_module_body(id,subst_mp sub mp,Option.smartmap
140
(subst_struct_expr sub) typ_opt,cst)
141
| With_definition_body(id,cb) ->
142
With_definition_body( id,subst_const_body sub cb)
144
and subst_modtype sub mtb =
145
let typ_expr' = subst_struct_expr sub mtb.typ_expr in
146
if typ_expr'==mtb.typ_expr then
150
typ_expr = typ_expr'}
152
and subst_structure sub sign =
153
let subst_body = function
155
SFBconst (subst_const_body sub cb)
157
SFBmind (subst_mind sub mib)
159
SFBmodule (subst_module sub mb)
161
SFBmodtype (subst_modtype sub mtb)
162
| SFBalias (mp,typ_opt,cst) ->
163
SFBalias (subst_mp sub mp,Option.smartmap
164
(subst_struct_expr sub) typ_opt,cst)
166
List.map (fun (l,b) -> (l,subst_body b)) sign
168
and subst_module sub mb =
169
let mtb' = Option.smartmap (subst_struct_expr sub) mb.mod_type in
170
(* This is similar to the previous case. In this case we have
171
a module M in a signature that is knows to be equivalent to a module M'
172
(because the signature is "K with Module M := M'") and we are substituting
174
let me' = Option.smartmap (subst_struct_expr sub) mb.mod_expr in
175
let mb_alias = update_subst sub mb.mod_alias in
176
let mb_alias = if mb_alias = empty_subst then
177
join_alias mb.mod_alias sub
179
join mb_alias (join_alias mb.mod_alias sub)
181
if mtb'==mb.mod_type && mb.mod_expr == me'
182
&& mb_alias == mb.mod_alias
186
mod_constraints=mb.mod_constraints;
187
mod_alias = mb_alias;
188
mod_retroknowledge=mb.mod_retroknowledge}
191
and subst_struct_expr sub = function
192
| SEBident mp -> SEBident (subst_mp sub mp)
193
| SEBfunctor (msid, mtb, meb') ->
194
SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb')
195
| SEBstruct (msid,str)->
196
SEBstruct(msid, subst_structure sub str)
197
| SEBapply (meb1,meb2,cst)->
198
SEBapply(subst_struct_expr sub meb1,
199
subst_struct_expr sub meb2,
201
| SEBwith (meb,wdb)->
202
SEBwith(subst_struct_expr sub meb,
203
subst_with_body sub wdb)
206
let subst_signature_msid msid mp =
207
subst_structure (map_msid msid mp)
209
(* spiwack: here comes the function which takes care of importing
210
the retroknowledge declared in the library *)
211
(* lclrk : retroknowledge_action list, rkaction : retroknowledge action *)
212
let add_retroknowledge msid mp =
213
let subst = add_msid msid mp empty_subst in
214
let subst_and_perform rkaction env =
216
| Retroknowledge.RKRegister (f, e) ->
217
Environ.register env f
219
| Const kn -> kind_of_term (subst_mps subst (mkConst kn))
220
| Ind ind -> kind_of_term (subst_mps subst (mkInd ind))
221
| _ -> anomaly "Modops.add_retroknowledge: had to import an unsupported kind of term")
224
(* The order of the declaration matters, for instance (and it's at the
225
time this comment is being written, the only relevent instance) the
226
int31 type registration absolutely needs int31 bits to be registered.
227
Since the local_retroknowledge is stored in reverse order (each new
228
registration is added at the top of the list) we need a fold_right
229
for things to go right (the pun is not intented). So we lose
230
tail recursivity, but the world will have exploded before any module
231
imports 10 000 retroknowledge registration.*)
232
List.fold_right subst_and_perform lclrk env
236
let strengthen_const env mp l cb =
237
match cb.const_opaque, cb.const_body with
238
| false, Some _ -> cb
241
let const = mkConst (make_con mp empty_dirpath l) in
242
let const_subs = Some (Declarations.from_val const) in
244
const_body = const_subs;
245
const_opaque = false;
246
const_body_code = Cemitcodes.from_val
247
(compile_constant_body env const_subs false false)
250
let strengthen_mind env mp l mib = match mib.mind_equiv with
252
| None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)}
255
let rec eval_struct env = function
258
let mtb =lookup_modtype mp env in
259
match mtb.typ_expr,mtb.typ_strength with
260
mtb,None -> eval_struct env mtb
261
| mtb,Some mp -> strengthen_mtb env mp (eval_struct env mtb)
263
| SEBapply (seb1,seb2,_) ->
264
let svb1 = eval_struct env seb1 in
265
let farg_id, farg_b, fbody_b = destr_functor env svb1 in
266
let mp = path_of_seb seb2 in
267
let mp = scrape_alias mp env in
268
let sub_alias = (lookup_modtype mp env).typ_alias in
269
let sub_alias = match eval_struct env (SEBident mp) with
270
| SEBstruct (msid,sign) ->
272
(subst_key (map_msid msid mp) sub_alias)
275
let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in
276
let sub_alias1 = update_subst sub_alias
277
(map_mbid farg_id mp (Some resolve)) in
278
eval_struct env (subst_struct_expr
280
(map_mbid farg_id mp (Some resolve))) fbody_b)
281
| SEBwith (mtb,(With_definition_body _ as wdb)) ->
282
let mtb',_ = merge_with env mtb wdb empty_subst in
284
| SEBwith (mtb, (With_module_body (_,mp,_,_) as wdb)) ->
286
(lookup_modtype mp env).typ_alias in
287
let alias_in_mp = match eval_struct env (SEBident mp) with
288
| SEBstruct (msid,sign) -> subst_key (map_msid msid mp) alias_in_mp
289
| _ -> alias_in_mp in
290
let mtb',_ = merge_with env mtb wdb alias_in_mp in
292
(* | SEBfunctor(mbid,mtb,body) ->
293
let env = add_module (MPbound mbid) (module_body_of_type mtb) env in
294
SEBfunctor(mbid,mtb,eval_struct env body) *)
297
and type_of_mb env mb =
298
match mb.mod_type,mb.mod_expr with
299
None,Some b -> eval_struct env b
300
| Some t, _ -> eval_struct env t
302
"Modops: empty type and empty expr"
304
and merge_with env mtb with_decl alias=
305
let msid,sig_b = match (eval_struct env mtb) with
306
| SEBstruct(msid,sig_b) -> msid,sig_b
307
| _ -> error_signature_expected mtb
309
let id,idl = match with_decl with
310
| With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> id,idl
311
| With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
313
let l = label_of_id id in
315
let rev_before,spec,after = list_split_assoc l [] sig_b in
316
let before = List.rev rev_before in
317
let rec mp_rec = function
319
| i::r -> MPdot(mp_rec r,label_of_id i)
321
let env' = add_signature (MPself msid) before env in
322
let new_spec,subst = match with_decl with
323
| With_definition_body ([],_)
324
| With_module_body ([],_,_,_) -> assert false
325
| With_definition_body ([id],c) ->
327
| With_module_body ([id], mp,typ_opt,cst) ->
328
let mp' = scrape_alias mp env' in
329
let new_alias = update_subst alias (map_mp (mp_rec [id]) mp') in
330
SFBalias (mp,typ_opt,Some cst),
331
Some(join (map_mp (mp_rec [id]) mp') new_alias)
332
| With_definition_body (_::_,_)
333
| With_module_body (_::_,_,_,_) ->
334
let old,aliasold = match spec with
335
SFBmodule msb -> Some msb, None
336
| SFBalias (mpold,typ_opt,cst) ->None, Some (mpold,typ_opt,cst)
337
| _ -> error_not_a_module (string_of_label l)
339
if aliasold = None then
340
let old = Option.get old in
341
let new_with_decl,subst1 =
343
With_definition_body (_,c) -> With_definition_body (idl,c),None
344
| With_module_body (idc,mp,typ_opt,cst) ->
345
let mp' = scrape_alias mp env' in
346
With_module_body (idl,mp,typ_opt,cst),
347
Some(map_mp (mp_rec (List.rev idc)) mp')
349
let subst = match subst1 with
351
| Some s -> Some (join s (update_subst alias s)) in
352
let modtype,subst_msb =
353
merge_with env' (type_of_mb env' old) new_with_decl alias in
356
mod_type = Some modtype;
357
mod_constraints = old.mod_constraints;
363
mod_retroknowledge = old.mod_retroknowledge}
365
(SFBmodule msb),subst
367
let mpold,typ_opt,cst = Option.get aliasold in
368
SFBalias (mpold,typ_opt,cst),None
370
SEBstruct(msid, before@(l,new_spec)::
371
(Option.fold_right subst_structure subst after)),subst
373
Not_found -> error_no_such_label l
375
and add_signature mp sign env =
376
let add_one env (l,elem) =
377
let kn = make_kn mp empty_dirpath l in
378
let con = make_con mp empty_dirpath l in
380
| SFBconst cb -> Environ.add_constant con cb env
381
| SFBmind mib -> Environ.add_mind kn mib env
383
add_module (MPdot (mp,l)) mb env
384
(* adds components as well *)
385
| SFBalias (mp1,_,cst) ->
386
Environ.register_alias (MPdot(mp,l)) mp1 env
387
| SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l))
390
List.fold_left add_one env sign
392
and add_module mp mb env =
393
let env = Environ.shallow_add_module mp mb env in
395
Environ.add_modtype mp (module_type_of_module (Some mp) mb) env
397
let mod_typ = type_of_mb env mb in
399
| SEBstruct (msid,sign) ->
400
add_retroknowledge msid mp (mb.mod_retroknowledge)
401
(add_signature mp (subst_signature_msid msid mp sign) env)
402
| SEBfunctor _ -> env
403
| _ -> anomaly "Modops:the evaluation of the structure failed "
407
and constants_of_specification env mp sign =
408
let aux (env,res) (l,elem) =
410
| SFBconst cb -> env,((make_con mp empty_dirpath l),cb)::res
411
| SFBmind _ -> env,res
413
let new_env = add_module (MPdot (mp,l)) mb env in
414
new_env,(constants_of_modtype env (MPdot (mp,l))
415
(type_of_mb env mb)) @ res
416
| SFBalias (mp1,typ_opt,cst) ->
417
let new_env = register_alias (MPdot (mp,l)) mp1 env in
418
new_env,(constants_of_modtype env (MPdot (mp,l))
419
(eval_struct env (SEBident mp1))) @ res
421
(* module type dans un module type.
422
Il faut au moins mettre mtb dans l'environnement (avec le bon
423
kn pour pouvoir continuer aller deplier les modules utilisant ce
431
Declare Module M : T2.
433
si on ne rajoute pas T2 dans l'environement de typage
434
on va exploser au moment du Declare Module
436
let new_env = Environ.add_modtype (MPdot(mp,l)) mtb env in
437
new_env, (constants_of_modtype env (MPdot(mp,l)) mtb.typ_expr) @ res
439
snd (List.fold_left aux (env,[]) sign)
441
and constants_of_modtype env mp modtype =
442
match (eval_struct env modtype) with
443
SEBstruct (msid,sign) ->
444
constants_of_specification env mp
445
(subst_signature_msid msid mp sign)
447
| _ -> anomaly "Modops:the evaluation of the structure failed "
449
(* returns a resolver for kn that maps mbid to mp. We only keep
450
constants that have the inline flag *)
451
and resolver_of_environment mbid modtype mp alias env =
452
let constants = constants_of_modtype env (MPbound mbid) modtype.typ_expr in
453
let constants = List.map (fun (l,cb) -> (l,subst_const_body alias cb)) constants in
454
let rec make_resolve = function
456
| (con,expecteddef)::r ->
457
let con' = replace_mp_in_con (MPbound mbid) mp con in
458
let con',_ = subst_con alias con' in
459
(* let con' = replace_mp_in_con (MPbound mbid) mp con' in *)
461
if expecteddef.Declarations.const_inline then
462
let constant = lookup_constant con' env in
463
if (not constant.Declarations.const_opaque) then
464
let constr = Option.map Declarations.force
465
constant.Declarations.const_body in
466
(con,constr)::(make_resolve r)
469
with Not_found -> error_no_such_label (con_label con')
471
let resolve = make_resolve constants in
472
Mod_subst.make_resolver resolve
475
and strengthen_mtb env mp mtb =
476
let mtb1 = eval_struct env mtb in
478
| SEBfunctor _ -> mtb1
479
| SEBstruct (msid,sign) ->
480
SEBstruct (msid,strengthen_sig env msid sign mp)
481
| _ -> anomaly "Modops:the evaluation of the structure failed "
483
and strengthen_mod env mp mb =
484
let mod_typ = type_of_mb env mb in
485
{ mod_expr = mb.mod_expr;
486
mod_type = Some (strengthen_mtb env mp mod_typ);
487
mod_constraints = mb.mod_constraints;
488
mod_alias = mb.mod_alias;
489
mod_retroknowledge = mb.mod_retroknowledge}
491
and strengthen_sig env msid sign mp = match sign with
493
| (l,SFBconst cb) :: rest ->
494
let item' = l,SFBconst (strengthen_const env mp l cb) in
495
let rest' = strengthen_sig env msid rest mp in
497
| (l,SFBmind mib) :: rest ->
498
let item' = l,SFBmind (strengthen_mind env mp l mib) in
499
let rest' = strengthen_sig env msid rest mp in
501
| (l,SFBmodule mb) :: rest ->
502
let mp' = MPdot (mp,l) in
503
let item' = l,SFBmodule (strengthen_mod env mp' mb) in
504
let env' = add_module
505
(MPdot (MPself msid,l)) mb env in
506
let rest' = strengthen_sig env' msid rest mp in
508
| ((l,SFBalias (mp1,_,cst)) as item) :: rest ->
509
let env' = register_alias (MPdot(MPself msid,l)) mp1 env in
510
let rest' = strengthen_sig env' msid rest mp in
512
| (l,SFBmodtype mty as item) :: rest ->
513
let env' = add_modtype
514
(MPdot((MPself msid),l))
518
let rest' = strengthen_sig env' msid rest mp in
522
let strengthen env mtb mp = strengthen_mtb env mp mtb
525
let update_subst env mb mp =
526
match type_of_mb env mb with
527
| SEBstruct(msid,str) -> false, join_alias
528
(subst_key (map_msid msid mp) mb.mod_alias)
530
| _ -> true, mb.mod_alias
added
removed
kernel/modops.ml
