diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /library/global.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'library/global.ml')
-rw-r--r-- | library/global.ml | 87 |
1 files changed, 50 insertions, 37 deletions
diff --git a/library/global.ml b/library/global.ml index b2f9e127..d5fafbb8 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: global.ml 10664 2008-03-14 11:27:37Z soubiran $ *) +(* $Id$ *) open Util open Names @@ -27,13 +27,11 @@ let env () = env_of_safe_env !global_env let env_is_empty () = is_empty !global_env -let _ = +let _ = declare_summary "Global environment" { freeze_function = (fun () -> !global_env); unfreeze_function = (fun fr -> global_env := fr); - init_function = (fun () -> global_env := empty_environment); - survive_module = true; - survive_section = false } + init_function = (fun () -> global_env := empty_environment) } (* Then we export the functions of [Typing] on that environment. *) @@ -50,31 +48,32 @@ let push_named_def d = global_env := env; cst -(*let add_thing add kn thing = - let _,dir,l = repr_kn kn in - let kn',newenv = add dir l thing !global_env in - if kn = kn' then - global_env := newenv - else - anomaly "Kernel names do not match." -*) -let add_thing add dir id thing = +let add_thing add dir id thing = let kn, newenv = add dir (label_of_id id) thing !global_env in global_env := newenv; kn -let add_constant = add_thing add_constant +let add_constant = add_thing add_constant let add_mind = add_thing add_mind -let add_modtype = add_thing (fun _ -> add_modtype) () -let add_module = add_thing (fun _ -> add_module) () -let add_alias = add_thing (fun _ -> add_alias) () +let add_modtype x y inl = add_thing (fun _ x y -> add_modtype x y inl) () x y + + +let add_module id me inl = + let l = label_of_id id in + let mp,resolve,new_env = add_module l me inl !global_env in + global_env := new_env; + mp,resolve + let add_constraints c = global_env := add_constraints c !global_env let set_engagement c = global_env := set_engagement c !global_env -let add_include me = global_env := add_include me !global_env +let add_include me is_module inl = + let resolve,newenv = add_include me is_module inl !global_env in + global_env := newenv; + resolve let start_module id = let l = label_of_id id in @@ -82,16 +81,18 @@ let start_module id = global_env := newenv; mp -let end_module id mtyo = +let end_module fs id mtyo = let l = label_of_id id in - let mp,newenv = end_module l mtyo !global_env in + let mp,resolve,newenv = end_module l mtyo !global_env in + Summary.unfreeze_summaries fs; global_env := newenv; - mp + mp,resolve -let add_module_parameter mbid mte = - let newenv = add_module_parameter mbid mte !global_env in - global_env := newenv +let add_module_parameter mbid mte inl = + let resolve,newenv = add_module_parameter mbid mte inl !global_env in + global_env := newenv; + resolve let start_modtype id = @@ -100,12 +101,15 @@ let start_modtype id = global_env := newenv; mp -let end_modtype id = +let end_modtype fs id = let l = label_of_id id in let kn,newenv = end_modtype l !global_env in + Summary.unfreeze_summaries fs; global_env := newenv; kn +let pack_module () = + pack_module !global_env @@ -117,19 +121,26 @@ 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 start_library dir = +let constant_of_delta con = + let resolver,resolver_param = (delta_of_senv !global_env) in + Mod_subst.constant_of_delta resolver_param + (Mod_subst.constant_of_delta resolver con) + +let mind_of_delta mind = + let resolver,resolver_param = (delta_of_senv !global_env) in + Mod_subst.mind_of_delta resolver_param + (Mod_subst.mind_of_delta resolver mind) + +let start_library dir = let mp,newenv = start_library dir !global_env in - global_env := newenv; + global_env := newenv; mp -let export s = snd (export !global_env s) +let export s = export !global_env s -let import cenv digest = - let mp,newenv = import cenv digest !global_env in - global_env := newenv; +let import cenv digest = + let mp,newenv = import cenv digest !global_env in + global_env := newenv; mp @@ -137,13 +148,13 @@ let import cenv digest = (*s Function to get an environment from the constants part of the global environment and a given context. *) -let env_of_context hyps = +let env_of_context hyps = reset_with_named_context hyps (env()) open Libnames let type_of_reference env = function - | VarRef id -> Environ.named_type id env + | VarRef id -> Environ.named_type id env | ConstRef c -> Typeops.type_of_constant env c | IndRef ind -> let specif = Inductive.lookup_mind_specif env ind in @@ -161,3 +172,5 @@ let register field value by_clause = let entry = kind_of_term value in let senv = Safe_typing.register !global_env field entry by_clause in global_env := senv + + |