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
(* $Id: safe_typing.ml 12187 2009-06-13 19:36:59Z msozeau $ *)
32
| SIG of (* funsig params *) (mod_bound_id * module_type_body) list
33
| STRUCT of (* functor params *) (mod_bound_id * module_type_body) list
38
modpath : module_path;
39
seed : dir_path; (* the "seed" of unique identifier generator *)
42
alias_subst : substitution}
44
let check_label l labset =
45
if Labset.mem l labset then error_existing_label l
47
let set_engagement_opt oeng env =
49
Some eng -> set_engagement eng env
52
type library_info = dir_path * Digest.t
54
type safe_environment =
55
{ old : safe_environment;
57
modinfo : module_info;
59
revstruct : structure_body;
60
univ : Univ.constraints;
61
engagement : engagement option;
62
imports : library_info list;
63
loads : (module_path * module_body) list;
64
local_retroknowledge : Retroknowledge.action list}
69
modinfo = senv.modinfo;
72
imports = senv.imports ;
77
(* a small hack to avoid variants and an unused case in all functions *)
78
let rec empty_environment =
79
{ old = empty_environment;
83
modpath = initial_path;
87
alias_subst = empty_subst};
88
labset = Labset.empty;
90
univ = Univ.Constraint.empty;
94
local_retroknowledge = [] }
96
let env_of_safe_env senv = senv.env
97
let env_of_senv = env_of_safe_env
105
let add_constraints cst senv =
107
env = Environ.add_constraints cst senv.env;
108
univ = Univ.Constraint.union cst senv.univ }
111
(*spiwack: functions for safe retroknowledge *)
113
(* terms which are closed under the environnement env, i.e
114
terms which only depends on constant who are themselves closed *)
115
let closed env term =
116
ContextObjectMap.is_empty (assumptions full_transparent_state env term)
118
(* the set of safe terms in an environement any recursive set of
119
terms who are known not to prove inconsistent statement. It should
120
include at least all the closed terms. But it could contain other ones
121
like the axiom of excluded middle for instance *)
127
(* universal lifting, used for the "get" operations mostly *)
128
let retroknowledge f senv =
129
Environ.retroknowledge f (env_of_senv senv)
131
let register senv field value by_clause =
132
(* todo : value closed, by_clause safe, by_clause of the proper type*)
133
(* spiwack : updates the safe_env with the information that the register
134
action has to be performed (again) when the environement is imported *)
135
{senv with env = Environ.register senv.env field value;
136
local_retroknowledge =
137
Retroknowledge.RKRegister (field,value)::senv.local_retroknowledge
140
(* spiwack : currently unused *)
141
let unregister senv field =
142
(*spiwack: todo: do things properly or delete *)
143
{senv with env = Environ.unregister senv.env field}
155
(* Insertion of section variables. They are now typed before being
156
added to the environment. *)
158
(* Same as push_named, but check that the variable is not already
159
there. Should *not* be done in Environ because tactics add temporary
160
hypothesis many many times, and the check performed here would
162
let safe_push_named (id,_,_ as d) env =
165
let _ = lookup_named id env in
166
error ("Identifier "^string_of_id id^" already defined.")
167
with Not_found -> () in
168
Environ.push_named d env
170
let push_named_def (id,b,topt) senv =
171
let (c,typ,cst) = translate_local_def senv.env (b,topt) in
172
let senv' = add_constraints cst senv in
173
let env'' = safe_push_named (id,Some c,typ) senv'.env in
174
(cst, {senv' with env=env''})
176
let push_named_assum (id,t) senv =
177
let (t,cst) = translate_local_assum senv.env t in
178
let senv' = add_constraints cst senv in
179
let env'' = safe_push_named (id,None,t) senv'.env in
180
(cst, {senv' with env=env''})
183
(* Insertion of constants and parameters in environment. *)
185
type global_declaration =
186
| ConstantEntry of constant_entry
187
| GlobalRecipe of Cooking.recipe
189
let hcons_constant_type = function
190
| NonPolymorphicType t ->
191
NonPolymorphicType (hcons1_constr t)
192
| PolymorphicArity (ctx,s) ->
193
PolymorphicArity (map_rel_context hcons1_constr ctx,s)
195
let hcons_constant_body cb =
196
let body = match cb.const_body with
198
| Some l_constr -> let constr = Declarations.force l_constr in
199
Some (Declarations.from_val (hcons1_constr constr))
203
const_type = hcons_constant_type cb.const_type }
205
let add_constant dir l decl senv =
206
check_label l senv.labset;
207
let kn = make_con senv.modinfo.modpath dir l in
210
| ConstantEntry ce -> translate_constant senv.env kn ce
212
let cb = translate_recipe senv.env kn r in
213
if dir = empty_dirpath then hcons_constant_body cb else cb
215
let senv' = add_constraints cb.const_constraints senv in
216
let env'' = Environ.add_constant kn cb senv'.env in
217
kn, { old = senv'.old;
219
modinfo = senv'.modinfo;
220
labset = Labset.add l senv'.labset;
221
revstruct = (l,SFBconst cb)::senv'.revstruct;
223
engagement = senv'.engagement;
224
imports = senv'.imports;
225
loads = senv'.loads ;
226
local_retroknowledge = senv'.local_retroknowledge }
229
(* Insertion of inductive types. *)
231
let add_mind dir l mie senv =
232
if mie.mind_entry_inds = [] then
233
anomaly "empty inductive types declaration";
234
(* this test is repeated by translate_mind *)
235
let id = (List.nth mie.mind_entry_inds 0).mind_entry_typename in
236
if l <> label_of_id id then
237
anomaly ("the label of inductive packet and its first inductive"^
238
" type do not match");
239
check_label l senv.labset;
240
(* TODO: when we will allow reorderings we will have to verify
242
let mib = translate_mind senv.env mie in
243
let senv' = add_constraints mib.mind_constraints senv in
244
let kn = make_kn senv.modinfo.modpath dir l in
245
let env'' = Environ.add_mind kn mib senv'.env in
246
kn, { old = senv'.old;
248
modinfo = senv'.modinfo;
249
labset = Labset.add l senv'.labset; (* TODO: the same as above *)
250
revstruct = (l,SFBmind mib)::senv'.revstruct;
252
engagement = senv'.engagement;
253
imports = senv'.imports;
255
local_retroknowledge = senv'.local_retroknowledge }
257
(* Insertion of module types *)
259
let add_modtype l mte senv =
260
check_label l senv.labset;
261
let mtb_expr,sub = translate_struct_entry senv.env mte in
262
let mtb = { typ_expr = mtb_expr;
265
let senv' = add_constraints
266
(struct_expr_constraints mtb_expr) senv in
267
let mp = MPdot(senv.modinfo.modpath, l) in
268
let env'' = Environ.add_modtype mp mtb senv'.env in
269
mp, { old = senv'.old;
271
modinfo = senv'.modinfo;
272
labset = Labset.add l senv'.labset;
273
revstruct = (l,SFBmodtype mtb)::senv'.revstruct;
275
engagement = senv'.engagement;
276
imports = senv'.imports;
278
local_retroknowledge = senv'.local_retroknowledge }
281
(* full_add_module adds module with universes and constraints *)
282
let full_add_module mp mb senv =
283
let senv = add_constraints (module_constraints mb) senv in
284
let env = Modops.add_module mp mb senv.env in
285
{senv with env = env}
287
(* Insertion of modules *)
289
let add_module l me senv =
290
check_label l senv.labset;
291
let mb = translate_module senv.env me in
292
let mp = MPdot(senv.modinfo.modpath, l) in
293
let senv' = full_add_module mp mb senv in
294
let is_functor,sub = Modops.update_subst senv'.env mb mp in
295
mp, { old = senv'.old;
302
alias_subst = join senv'.modinfo.alias_subst sub};
303
labset = Labset.add l senv'.labset;
304
revstruct = (l,SFBmodule mb)::senv'.revstruct;
306
engagement = senv'.engagement;
307
imports = senv'.imports;
309
local_retroknowledge = senv'.local_retroknowledge }
311
let add_alias l mp senv =
312
check_label l senv.labset;
313
let mp' = MPdot(senv.modinfo.modpath, l) in
314
let mp1 = scrape_alias mp senv.env in
316
if check_bound_mp mp then
317
Some (strengthen senv.env
318
(lookup_modtype mp senv.env).typ_expr mp)
322
(* we get all updated alias substitution {mp1.K\M} that comes from mp1 *)
323
let _,sub = Modops.update_subst senv.env (lookup_module mp1 senv.env) mp1 in
324
(* transformation of {mp1.K\M} to {mp.K\M}*)
325
let sub = update_subst sub (map_mp mp' mp1) in
326
(* transformation of {mp.K\M} to {mp.K\M'} where M'=M{mp1\mp'}*)
327
let sub = join_alias sub (map_mp mp' mp1) in
328
(* we add the alias substitution *)
329
let sub = add_mp mp' mp1 sub in
330
let env' = register_alias mp' mp senv.env in
331
mp', { old = senv.old;
333
modinfo = { senv.modinfo with
335
senv.modinfo.alias_subst sub};
336
labset = Labset.add l senv.labset;
337
revstruct = (l,SFBalias (mp,typ_opt,None))::senv.revstruct;
339
engagement = senv.engagement;
340
imports = senv.imports;
342
local_retroknowledge = senv.local_retroknowledge }
344
(* Interactive modules *)
346
let start_module l senv =
347
check_label l senv.labset;
348
let msid = make_msid senv.modinfo.seed (string_of_label l) in
349
let mp = MPself msid in
350
let modinfo = { msid = msid;
352
seed = senv.modinfo.seed;
355
alias_subst = empty_subst}
360
labset = Labset.empty;
362
univ = Univ.Constraint.empty;
364
imports = senv.imports;
366
(* spiwack : not sure, but I hope it's correct *)
367
local_retroknowledge = [] }
369
let end_module l restype senv =
370
let oldsenv = senv.old in
371
let modinfo = senv.modinfo in
372
let restype = Option.map (translate_struct_entry senv.env) restype in
373
let params,is_functor =
374
match modinfo.variant with
375
| NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
376
| STRUCT params -> params, (List.length params > 0)
378
if l <> modinfo.label then error_incompatible_labels l modinfo.label;
379
if not (empty_context senv.env) then error_local_context None;
380
let functorize_struct tb =
382
(fun mtb (arg_id,arg_b) ->
383
SEBfunctor(arg_id,arg_b,mtb))
388
SEBstruct (modinfo.msid, List.rev senv.revstruct)
390
let mod_typ,subst,cst =
392
| None -> None,modinfo.alias_subst,Constraint.empty
393
| Some (res_tb,subst) ->
394
let cst = check_subtypes senv.env
397
typ_alias = modinfo.alias_subst}
400
typ_alias = subst} in
401
let mtb = functorize_struct res_tb in
404
let mexpr = functorize_struct auto_tb in
405
let cst = Constraint.union cst senv.univ in
407
{ mod_expr = Some mexpr;
409
mod_constraints = cst;
411
mod_retroknowledge = senv.local_retroknowledge }
413
let mp = MPdot (oldsenv.modinfo.modpath, l) in
414
let newenv = oldsenv.env in
415
let newenv = set_engagement_opt senv.engagement newenv in
416
let senv'= {senv with env=newenv} in
419
(fun env (mp,mb) -> full_add_module mp mb env)
421
(List.rev senv'.loads)
423
let newenv = Environ.add_constraints cst senv'.env in
425
Modops.add_module mp mb newenv
427
let is_functor,subst = Modops.update_subst newenv mb mp in
432
{ oldsenv.modinfo with
434
oldsenv.modinfo.alias_subst
437
mp, { old = oldsenv.old;
439
modinfo = newmodinfo;
440
labset = Labset.add l oldsenv.labset;
441
revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
442
univ = Univ.Constraint.union senv'.univ oldsenv.univ;
443
(* engagement is propagated to the upper level *)
444
engagement = senv'.engagement;
445
imports = senv'.imports;
446
loads = senv'.loads@oldsenv.loads;
447
local_retroknowledge = senv'.local_retroknowledge@oldsenv.local_retroknowledge }
450
(* Include for module and module type*)
451
let add_include me senv =
452
let struct_expr,_ = translate_struct_entry senv.env me in
453
let senv = add_constraints (struct_expr_constraints struct_expr) senv in
454
let msid,str = match (eval_struct senv.env struct_expr) with
455
| SEBstruct(msid,str_l) -> msid,str_l
456
| _ -> error ("You cannot Include a higher-order Module or Module Type.")
458
let mp_sup = senv.modinfo.modpath in
459
let str1 = subst_signature_msid msid mp_sup str in
460
let add senv (l,elem) =
461
check_label l senv.labset;
464
let con = make_con mp_sup empty_dirpath l in
465
let senv' = add_constraints cb.const_constraints senv in
466
let env'' = Environ.add_constant con cb senv'.env in
469
modinfo = senv'.modinfo;
470
labset = Labset.add l senv'.labset;
471
revstruct = (l,SFBconst cb)::senv'.revstruct;
473
engagement = senv'.engagement;
474
imports = senv'.imports;
475
loads = senv'.loads ;
476
local_retroknowledge = senv'.local_retroknowledge }
479
let kn = make_kn mp_sup empty_dirpath l in
480
let senv' = add_constraints mib.mind_constraints senv in
481
let env'' = Environ.add_mind kn mib senv'.env in
484
modinfo = senv'.modinfo;
485
labset = Labset.add l senv'.labset;
486
revstruct = (l,SFBmind mib)::senv'.revstruct;
488
engagement = senv'.engagement;
489
imports = senv'.imports;
491
local_retroknowledge = senv'.local_retroknowledge }
494
let mp = MPdot(senv.modinfo.modpath, l) in
495
let is_functor,sub = Modops.update_subst senv.env mb mp in
496
let senv' = full_add_module mp mb senv in
504
alias_subst = join senv'.modinfo.alias_subst sub};
505
labset = Labset.add l senv'.labset;
506
revstruct = (l,SFBmodule mb)::senv'.revstruct;
508
engagement = senv'.engagement;
509
imports = senv'.imports;
511
local_retroknowledge = senv'.local_retroknowledge }
512
| SFBalias (mp',typ_opt,cst) ->
513
let env' = Option.fold_right
514
Environ.add_constraints cst senv.env in
515
let mp = MPdot(senv.modinfo.modpath, l) in
516
let mp1 = scrape_alias mp' senv.env in
517
let _,sub = Modops.update_subst senv.env (lookup_module mp1 senv.env) mp1 in
518
let sub = update_subst sub (map_mp mp mp1) in
519
let sub = join_alias sub (map_mp mp mp1) in
520
let sub = add_mp mp mp1 sub in
521
let env' = register_alias mp mp' env' in
524
modinfo = { senv.modinfo with
526
senv.modinfo.alias_subst sub};
527
labset = Labset.add l senv.labset;
528
revstruct = (l,SFBalias (mp',typ_opt,cst))::senv.revstruct;
530
engagement = senv.engagement;
531
imports = senv.imports;
533
local_retroknowledge = senv.local_retroknowledge }
535
let env' = add_modtype_constraints senv.env mtb in
536
let mp = MPdot(senv.modinfo.modpath, l) in
537
let env'' = Environ.add_modtype mp mtb env' in
540
modinfo = senv.modinfo;
541
labset = Labset.add l senv.labset;
542
revstruct = (l,SFBmodtype mtb)::senv.revstruct;
544
engagement = senv.engagement;
545
imports = senv.imports;
547
local_retroknowledge = senv.local_retroknowledge }
549
List.fold_left add senv str1
551
(* Adding parameters to modules or module types *)
553
let add_module_parameter mbid mte senv =
554
if senv.revstruct <> [] or senv.loads <> [] then
555
anomaly "Cannot add a module parameter to a non empty module";
556
let mtb_expr,sub = translate_struct_entry senv.env mte in
557
let mtb = {typ_expr = mtb_expr;
560
let senv = full_add_module (MPbound mbid) (module_body_of_type mtb) senv
562
let new_variant = match senv.modinfo.variant with
563
| STRUCT params -> STRUCT ((mbid,mtb) :: params)
564
| SIG params -> SIG ((mbid,mtb) :: params)
566
anomaly "Module parameters can only be added to modules or signatures"
570
modinfo = { senv.modinfo with variant = new_variant };
571
labset = senv.labset;
574
engagement = senv.engagement;
575
imports = senv.imports;
577
local_retroknowledge = senv.local_retroknowledge }
580
(* Interactive module types *)
582
let start_modtype l senv =
583
check_label l senv.labset;
584
let msid = make_msid senv.modinfo.seed (string_of_label l) in
585
let mp = MPself msid in
586
let modinfo = { msid = msid;
588
seed = senv.modinfo.seed;
591
alias_subst = empty_subst }
596
labset = Labset.empty;
598
univ = Univ.Constraint.empty;
600
imports = senv.imports;
602
(* spiwack: not 100% sure, but I think it should be like that *)
603
local_retroknowledge = []}
605
let end_modtype l senv =
606
let oldsenv = senv.old in
607
let modinfo = senv.modinfo in
609
match modinfo.variant with
610
| LIBRARY _ | NONE | STRUCT _ -> error_no_modtype_to_end ()
611
| SIG params -> params
613
if l <> modinfo.label then error_incompatible_labels l modinfo.label;
614
if not (empty_context senv.env) then error_local_context None;
616
SEBstruct (modinfo.msid, List.rev senv.revstruct)
620
(fun mtb (arg_id,arg_b) ->
621
SEBfunctor(arg_id,arg_b,mtb))
625
let mp = MPdot (oldsenv.modinfo.modpath, l) in
626
let newenv = oldsenv.env in
627
(* since universes constraints cannot be stored in the modtype,
628
they are propagated to the upper level *)
629
let newenv = Environ.add_constraints senv.univ newenv in
630
let newenv = set_engagement_opt senv.engagement newenv in
631
let senv = {senv with env=newenv} in
634
(fun env (mp,mb) -> full_add_module mp mb env)
636
(List.rev senv.loads)
638
let subst = senv.modinfo.alias_subst in
639
let mtb = {typ_expr = mtb_expr;
641
typ_alias = subst} in
643
Environ.add_modtype mp mtb senv.env
645
mp, { old = oldsenv.old;
647
modinfo = oldsenv.modinfo;
648
labset = Labset.add l oldsenv.labset;
649
revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct;
650
univ = Univ.Constraint.union senv.univ oldsenv.univ;
651
engagement = senv.engagement;
652
imports = senv.imports;
653
loads = senv.loads@oldsenv.loads;
654
(* spiwack : if there is a bug with retroknowledge in nested modules
655
it's likely to come from here *)
656
local_retroknowledge =
657
senv.local_retroknowledge@oldsenv.local_retroknowledge}
660
let current_modpath senv = senv.modinfo.modpath
661
let current_msid senv = senv.modinfo.msid
664
(* Check that the engagement expected by a library matches the initial one *)
665
let check_engagement env c =
666
match Environ.engagement env, c with
667
| Some ImpredicativeSet, Some ImpredicativeSet -> ()
669
| _, Some ImpredicativeSet ->
670
error "Needs option -impredicative-set."
672
let set_engagement c senv =
674
env = Environ.set_engagement c senv.env;
675
engagement = Some c }
677
(* Libraries = Compiled modules *)
679
type compiled_library =
680
dir_path * module_body * library_info list * engagement option
682
(* We check that only initial state Require's were performed before
683
[start_library] was called *)
686
senv.revstruct = [] &&
687
senv.modinfo.msid = initial_msid &&
688
senv.modinfo.variant = NONE
690
let start_library dir senv =
691
if not (is_empty senv) then
692
anomaly "Safe_typing.start_library: environment should be empty";
694
match (repr_dirpath dir) with
695
[] -> anomaly "Empty dirpath in Safe_typing.start_library"
697
make_dirpath tl, label_of_id hd
699
let msid = make_msid dir_path (string_of_label l) in
700
let mp = MPself msid in
701
let modinfo = { msid = msid;
705
variant = LIBRARY dir;
706
alias_subst = empty_subst }
711
labset = Labset.empty;
713
univ = Univ.Constraint.empty;
715
imports = senv.imports;
717
local_retroknowledge = [] }
721
let export senv dir =
722
let modinfo = senv.modinfo in
724
match modinfo.variant with
727
anomaly "We are not exporting the right library!"
729
anomaly "We are not exporting the library"
731
(*if senv.modinfo.params <> [] || senv.modinfo.restype <> None then
732
(* error_export_simple *) (); *)
734
{ mod_expr = Some (SEBstruct (modinfo.msid, List.rev senv.revstruct));
736
mod_constraints = senv.univ;
737
mod_alias = senv.modinfo.alias_subst;
738
mod_retroknowledge = senv.local_retroknowledge}
740
modinfo.msid, (dir,mb,senv.imports,engagement senv.env)
743
let check_imports senv needed =
744
let imports = senv.imports in
745
let check (id,stamp) =
747
let actual_stamp = List.assoc id imports in
748
if stamp <> actual_stamp then
750
("Inconsistent assumptions over module "^(string_of_dirpath id)^".")
752
error ("Reference to unknown module "^(string_of_dirpath id)^".")
754
List.iter check needed
758
(* we have an inefficiency: Since loaded files are added to the
759
environment every time a module is closed, their components are
760
calculated many times. Thic could be avoided in several ways:
762
1 - for each file create a dummy environment containing only this
763
file's components, merge this environment with the global
764
environment, and store for the future (instead of just its type)
766
2 - create "persistent modules" environment table in Environ add put
767
loaded by side-effect once and for all (like it is done in OCaml).
768
Would this be correct with respect to undo's and stuff ?
771
let import (dp,mb,depends,engmt) digest senv =
772
check_imports senv depends;
773
check_engagement senv.env engmt;
774
let mp = MPfile dp in
775
let env = senv.env in
776
let env = Environ.add_constraints mb.mod_constraints env in
777
let env = Modops.add_module mp mb env in
780
imports = (dp,digest)::senv.imports;
781
loads = (mp,mb)::senv.loads }
784
(* Remove the body of opaque constants in modules *)
785
let rec lighten_module mb =
787
mod_expr = Option.map lighten_modexpr mb.mod_expr;
788
mod_type = Option.map lighten_modexpr mb.mod_type;
791
and lighten_struct struc =
792
let lighten_body (l,body) = (l,match body with
793
| SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None}
794
| (SFBconst _ | SFBmind _ | SFBalias _) as x -> x
795
| SFBmodule m -> SFBmodule (lighten_module m)
796
| SFBmodtype m -> SFBmodtype
798
typ_expr = lighten_modexpr m.typ_expr}))
800
List.map lighten_body struc
802
and lighten_modexpr = function
803
| SEBfunctor (mbid,mty,mexpr) ->
806
typ_expr = lighten_modexpr mty.typ_expr}),
807
lighten_modexpr mexpr)
808
| SEBident mp as x -> x
809
| SEBstruct (msid, struc) ->
810
SEBstruct (msid, lighten_struct struc)
811
| SEBapply (mexpr,marg,u) ->
812
SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
813
| SEBwith (seb,wdcl) ->
814
SEBwith (lighten_modexpr seb,wdcl)
816
let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s)
819
type judgment = unsafe_judgment
821
let j_val j = j.uj_val
822
let j_type j = j.uj_type
824
let safe_infer senv = infer (env_of_senv senv)
826
let typing senv = Typeops.typing (env_of_senv senv)
added
removed
kernel/safe_typing.ml
