diff options
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 149 |
1 files changed, 55 insertions, 94 deletions
diff --git a/library/global.ml b/library/global.ml index 22b69e4f2..fd6cce46f 100644 --- a/library/global.ml +++ b/library/global.ml @@ -9,20 +9,19 @@ open Names open Term open Environ -open Safe_typing -(* We introduce here the global environment of the system, and we declare it - as a synchronized table. *) +(** We introduce here the global environment of the system, + and we declare it as a synchronized table. *) module GlobalSafeEnv : sig - val safe_env : unit -> safe_environment - val set_safe_env : safe_environment -> unit + val safe_env : unit -> Safe_typing.safe_environment + val set_safe_env : Safe_typing.safe_environment -> unit val join_safe_environment : unit -> unit end = struct -let global_env = ref empty_environment +let global_env = ref Safe_typing.empty_environment let join_safe_environment () = global_env := Safe_typing.join_safe_environment !global_env @@ -37,7 +36,7 @@ let () = | `No -> !global_env | `Shallow -> prune_safe_environment !global_env); unfreeze_function = (fun fr -> global_env := fr); - init_function = (fun () -> global_env := empty_environment) } + init_function = (fun () -> global_env := Safe_typing.empty_environment) } let assert_not_parsing () = if !Flags.we_are_parsing then @@ -50,89 +49,57 @@ let set_safe_env e = global_env := e end -open GlobalSafeEnv -let safe_env = safe_env -let join_safe_environment = join_safe_environment +let safe_env = GlobalSafeEnv.safe_env +let join_safe_environment = GlobalSafeEnv.join_safe_environment -let env () = env_of_safe_env (safe_env ()) +let env () = Safe_typing.env_of_safe_env (safe_env ()) -let env_is_empty () = is_empty (safe_env ()) +let env_is_initial () = Safe_typing.is_initial (safe_env ()) -(* Then we export the functions of [Typing] on that environment. *) - -let universes () = universes (env()) -let named_context () = named_context (env()) -let named_context_val () = named_context_val (env()) - -let push_named_assum a = - let (cst,env) = push_named_assum a (safe_env ()) in - set_safe_env env; - cst -let push_named_def d = - let (cst,env) = push_named_def d (safe_env ()) in - set_safe_env env; - cst +(** Turn ops over the safe_environment state monad to ops on the global env *) +let globalize0 f = GlobalSafeEnv.set_safe_env (f (safe_env ())) -let add_thing add dir id thing = - let kn, newenv = add dir (Label.of_id id) thing (safe_env ()) in - set_safe_env newenv; - kn +let globalize f = + let res,env = f (safe_env ()) in GlobalSafeEnv.set_safe_env env; res -let add_constant = add_thing add_constant -let add_mind = add_thing add_mind -let add_modtype x y inl = add_thing (fun _ x y -> add_modtype x y inl) () x y +let globalize_with_summary fs f = + let res,env = f (safe_env ()) in + Summary.unfreeze_summaries fs; + GlobalSafeEnv.set_safe_env env; + res +(** [Safe_typing] operations, now operating on the global environment *) -let add_module id me inl = - let l = Label.of_id id in - let mp,resolve,new_env = add_module l me inl (safe_env ()) in - set_safe_env new_env; - mp,resolve - +let i2l = Label.of_id -let add_constraints c = set_safe_env (add_constraints c (safe_env ())) +let push_named_assum a = globalize (Safe_typing.push_named_assum a) +let push_named_def d = globalize (Safe_typing.push_named_def d) +let add_constraints c = globalize0 (Safe_typing.add_constraints c) +let set_engagement c = globalize0 (Safe_typing.set_engagement c) +let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) +let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) +let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) +let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) +let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) -let set_engagement c = set_safe_env (set_engagement c (safe_env ())) - -let add_include me is_module inl = - let resolve,newenv = add_include me is_module inl (safe_env ()) in - set_safe_env newenv; - resolve - -let start_module id = - let l = Label.of_id id in - let mp,newenv = start_module l (safe_env ()) in - set_safe_env newenv; - mp +let start_module id = globalize (Safe_typing.start_module (i2l id)) +let start_modtype id = globalize (Safe_typing.start_modtype (i2l id)) let end_module fs id mtyo = - let l = Label.of_id id in - let mp,resolve,newenv = end_module l mtyo (safe_env ()) in - Summary.unfreeze_summaries fs; - set_safe_env newenv; - mp,resolve + globalize_with_summary fs (Safe_typing.end_module (i2l id) mtyo) +let end_modtype fs id = + globalize_with_summary fs (Safe_typing.end_modtype (i2l id)) let add_module_parameter mbid mte inl = - let resolve,newenv = add_module_parameter mbid mte inl (safe_env ()) in - set_safe_env newenv; - resolve + globalize (Safe_typing.add_module_parameter mbid mte inl) +(** Queries on the global environment *) -let start_modtype id = - let l = Label.of_id id in - let mp,newenv = start_modtype l (safe_env ()) in - set_safe_env newenv; - mp - -let end_modtype fs id = - let l = Label.of_id id in - let kn,newenv = end_modtype l (safe_env ()) in - Summary.unfreeze_summaries fs; - set_safe_env newenv; - kn - +let universes () = universes (env()) +let named_context () = named_context (env()) +let named_context_val () = named_context_val (env()) let lookup_named id = lookup_named id (env()) let lookup_constant kn = lookup_constant kn (env()) @@ -142,35 +109,32 @@ let lookup_mind kn = lookup_mind kn (env()) let lookup_module mp = lookup_module mp (env()) let lookup_modtype kn = lookup_modtype kn (env()) +let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) + +(** Operations on kernel names *) + let constant_of_delta_kn kn = - let resolver,resolver_param = (delta_of_senv (safe_env ())) in + let resolver,resolver_param = Safe_typing.delta_of_senv (safe_env ()) + in (* TODO : are resolver and resolver_param orthogonal ? the effect of resolver is lost if resolver_param isn't trivial at that spot. *) Mod_subst.constant_of_deltas_kn resolver_param resolver kn let mind_of_delta_kn kn = - let resolver,resolver_param = (delta_of_senv (safe_env ())) in + let resolver,resolver_param = Safe_typing.delta_of_senv (safe_env ()) + in (* TODO idem *) Mod_subst.mind_of_deltas_kn resolver_param resolver kn -let exists_objlabel id = exists_objlabel id (safe_env ()) - -let start_library dir = - let mp,newenv = start_library dir (safe_env ()) in - set_safe_env newenv; - mp - -let export s = export (safe_env ()) s - -let import cenv digest = - let mp,newenv,values = import cenv digest (safe_env ()) in - set_safe_env newenv; - mp, values +(** Operations on libraries *) +let start_library dir = globalize (Safe_typing.start_library dir) +let export s = Safe_typing.export (safe_env ()) s +let import cenv digest = globalize (Safe_typing.import cenv digest) -(*s Function to get an environment from the constants part of the global +(** Function to get an environment from the constants part of the global environment and a given context. *) let env_of_context hyps = @@ -194,9 +158,6 @@ let type_of_global t = type_of_reference (env ()) t (* spiwack: register/unregister functions for retroknowledge *) let register field value by_clause = - let entry = kind_of_term value in - let senv = Safe_typing.register (safe_env ()) field entry by_clause in - set_safe_env senv + globalize0 (Safe_typing.register field (kind_of_term value) by_clause) -let register_inline c = - set_safe_env (Safe_typing.register_inline c (safe_env ())) +let register_inline c = globalize0 (Safe_typing.register_inline c) |