diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 43 |
1 files changed, 4 insertions, 39 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index bd44b3967..5f8d8b977 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -85,9 +85,6 @@ open Declarations - [type_in_type] : does the universe hierarchy collapse? - [imports] : names and digests of Require'd libraries since big-bang. This field will only grow - - [loads] : list of libraries Require'd inside the current module. - They will be propagated to the upper module level when - the current module ends. - [local_retroknowledge] *) @@ -124,7 +121,6 @@ type safe_environment = engagement : engagement option; type_in_type : bool; imports : vodigest DPMap.t; - loads : (module_path * module_body) list; local_retroknowledge : Retroknowledge.action list } and modvariant = @@ -153,7 +149,6 @@ let empty_environment = engagement = None; type_in_type = false; imports = DPMap.empty; - loads = []; local_retroknowledge = [] } let is_initial senv = @@ -289,8 +284,7 @@ let check_empty_context senv = it must have been freshly started *) let check_empty_struct senv = - assert (List.is_empty senv.revstruct - && List.is_empty senv.loads) + assert (List.is_empty senv.revstruct) (** When starting a library, the current environment should be initial i.e. only composed of Require's *) @@ -565,12 +559,6 @@ let add_module_parameter mbid mte inl senv = let functorize params init = List.fold_left (fun e (mbid,mt) -> MoreFunctor(mbid,mt,e)) init params -let propagate_loads senv = - List.fold_left - (fun env (_,mb) -> full_add_module mb env) - senv - (List.rev senv.loads) - (** Build the module body of the current module, taking in account a possible return type (_:T) *) @@ -615,7 +603,6 @@ let propagate_senv newdef newenv newresolver senv oldsenv = (* engagement is propagated to the upper level *) engagement = senv.engagement; imports = senv.imports; - loads = senv.loads@oldsenv.loads; local_retroknowledge = senv.local_retroknowledge@oldsenv.local_retroknowledge } @@ -629,7 +616,7 @@ let end_module l restype senv = let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in let newenv = set_engagement_opt newenv senv.engagement in let senv'= - propagate_loads { senv with + { senv with env = newenv; univ = Univ.Constraint.union senv.univ mb.mod_constraints} in let newenv = Environ.add_constraints mb.mod_constraints senv'.env in @@ -651,7 +638,7 @@ let end_modtype l senv = let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in let newenv = Environ.add_constraints senv.univ newenv in let newenv = set_engagement_opt newenv senv.engagement in - let senv' = propagate_loads {senv with env=newenv} in + let senv' = {senv with env=newenv} in let mtb = { typ_mp = mp; typ_expr = functorize params auto_tb; @@ -799,8 +786,7 @@ let import lib cst vodigest senv = in Modops.add_linked_module mb linkinfo env); modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver; - imports = DPMap.add lib.comp_name vodigest senv.imports; - loads = (mp,mb)::senv.loads } + imports = DPMap.add lib.comp_name vodigest senv.imports } (** {6 Safe typing } *) @@ -844,27 +830,6 @@ let register_inline kn senv = let add_constraints c = add_constraints (Now c) - -(* NB: The next old comment probably refers to [propagate_loads] above. - When a Require is done inside a module, we'll redo this require - at the upper level after the module is ended, and so on. - This is probably not a big deal anyway, since these Require's - inside modules should be pretty rare. Maybe someday we could - brutally forbid this tricky "feature"... *) - -(* we have an inefficiency: Since loaded files are added to the -environment every time a module is closed, their components are -calculated many times. This could be avoided in several ways: - -1 - for each file create a dummy environment containing only this -file's components, merge this environment with the global -environment, and store for the future (instead of just its type) - -2 - create "persistent modules" environment table in Environ add put -loaded by side-effect once and for all (like it is done in OCaml). -Would this be correct with respect to undo's and stuff ? -*) - let set_strategy e k l = { e with env = (Environ.set_oracle e.env (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) } |