diff options
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 294 |
1 files changed, 186 insertions, 108 deletions
diff --git a/library/global.ml b/library/global.ml index 96e522a7..875097e4 100644 --- a/library/global.ml +++ b/library/global.ml @@ -1,180 +1,258 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Names -open Term -open Sign open Environ -open Safe_typing -open Summary -(* 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. *) -let global_env = ref empty_environment +let global_env_summary_name = "Global environment" -let safe_env () = !global_env +module GlobalSafeEnv : sig -let env () = env_of_safe_env !global_env + val safe_env : unit -> Safe_typing.safe_environment + val set_safe_env : Safe_typing.safe_environment -> unit + val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit -let env_is_empty () = is_empty !global_env +end = struct -let _ = - declare_summary "Global environment" - { freeze_function = (fun () -> !global_env); +let global_env = ref Safe_typing.empty_environment + +let join_safe_environment ?except () = + global_env := Safe_typing.join_safe_environment ?except !global_env + +let () = + Summary.declare_summary global_env_summary_name + { Summary.freeze_function = (function + | `Yes -> join_safe_environment (); !global_env + | `No -> !global_env + | `Shallow -> !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) } -(* Then we export the functions of [Typing] on that environment. *) +let assert_not_parsing () = + if !Flags.we_are_parsing then + Errors.anomaly ( + Pp.strbrk"The global environment cannot be accessed during parsing") -let universes () = universes (env()) -let named_context () = named_context (env()) -let named_context_val () = named_context_val (env()) +let safe_env () = assert_not_parsing(); !global_env -let push_named_assum a = - let (cst,env) = push_named_assum a !global_env in - global_env := env; - cst -let push_named_def d = - let (cst,env) = push_named_def d !global_env in - global_env := env; - cst +let set_safe_env e = global_env := e +end -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 safe_env = GlobalSafeEnv.safe_env +let join_safe_environment ?except () = + GlobalSafeEnv.join_safe_environment ?except () -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 env () = Safe_typing.env_of_safe_env (safe_env ()) +let env_is_initial () = Safe_typing.is_initial (safe_env ()) -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 - +(** Turn ops over the safe_environment state monad to ops on the global env *) -let add_constraints c = global_env := add_constraints c !global_env +let globalize0 f = GlobalSafeEnv.set_safe_env (f (safe_env ())) -let set_engagement c = global_env := set_engagement c !global_env +let globalize f = + let res,env = f (safe_env ()) in GlobalSafeEnv.set_safe_env env; res -let add_include me is_module inl = - let resolve,newenv = add_include me is_module inl !global_env in - global_env := newenv; - resolve +let globalize_with_summary fs f = + let res,env = f (safe_env ()) in + Summary.unfreeze_summaries fs; + GlobalSafeEnv.set_safe_env env; + res -let start_module id = - let l = label_of_id id in - let mp,newenv = start_module l !global_env in - global_env := newenv; - mp +(** [Safe_typing] operations, now operating on the global environment *) -let end_module fs id mtyo = - let l = label_of_id id in - let mp,resolve,newenv = end_module l mtyo !global_env in - Summary.unfreeze_summaries fs; - global_env := newenv; - mp,resolve +let i2l = Label.of_id +let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) +let push_named_def d = globalize0 (Safe_typing.push_named_def d) +let add_constraints c = globalize0 (Safe_typing.add_constraints c) +let push_context_set c = globalize0 (Safe_typing.push_context_set c) +let push_context c = globalize0 (Safe_typing.push_context c) -let add_module_parameter mbid mte inl = - let resolve,newenv = add_module_parameter mbid mte inl !global_env in - global_env := newenv; - resolve +let set_engagement c = globalize0 (Safe_typing.set_engagement c) +let set_type_in_type () = globalize0 (Safe_typing.set_type_in_type) +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 start_module id = globalize (Safe_typing.start_module (i2l id)) +let start_modtype id = globalize (Safe_typing.start_modtype (i2l id)) -let start_modtype id = - let l = label_of_id id in - let mp,newenv = start_modtype l !global_env in - global_env := newenv; - mp +let end_module fs id mtyo = + globalize_with_summary fs (Safe_typing.end_module (i2l id) mtyo) 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 + globalize_with_summary fs (Safe_typing.end_modtype (i2l id)) -let pack_module () = - pack_module !global_env +let add_module_parameter mbid mte inl = + globalize (Safe_typing.add_module_parameter mbid mte inl) +(** Queries on the global environment *) +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()) let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind +let lookup_pinductive (ind,_) = Inductive.lookup_mind_specif (env()) ind 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 ()) + +let opaque_tables () = Environ.opaque_tables (env ()) +let body_of_constant_body cb = Declareops.body_of_constant (opaque_tables ()) cb +let body_of_constant cst = body_of_constant_body (lookup_constant cst) +let constraints_of_constant_body cb = + Declareops.constraints_of_constant (opaque_tables ()) cb +let universes_of_constant_body cb = + Declareops.universes_of_constant (opaque_tables ()) cb + +(** Operations on kernel names *) + let constant_of_delta_kn kn = - let resolver,resolver_param = (delta_of_senv !global_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_delta resolver_param - (Mod_subst.constant_of_delta_kn resolver kn) + Mod_subst.constant_of_deltas_kn resolver_param resolver kn let mind_of_delta_kn kn = - let resolver,resolver_param = (delta_of_senv !global_env) in + let resolver,resolver_param = Safe_typing.delta_of_senv (safe_env ()) + in (* TODO idem *) - Mod_subst.mind_of_delta resolver_param - (Mod_subst.mind_of_delta_kn resolver kn) - -let exists_objlabel id = exists_objlabel id !global_env - -let start_library dir = - let mp,newenv = start_library dir !global_env in - global_env := newenv; - mp - -let export s = export !global_env s + Mod_subst.mind_of_deltas_kn resolver_param resolver kn -let import cenv digest = - let mp,newenv = import cenv digest !global_env in - global_env := newenv; - mp +(** Operations on libraries *) +let start_library dir = globalize (Safe_typing.start_library dir) +let export ?except s = Safe_typing.export ?except (safe_env ()) s +let import c u d = globalize (Safe_typing.import c u d) -(*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 = reset_with_named_context hyps (env()) -open Libnames +open Globnames -let type_of_reference env = function +(** Build a fresh instance for a given context, its associated substitution and + the instantiated constraints. *) + +let type_of_global_unsafe r = + let env = env() in + match r with | VarRef id -> Environ.named_type id env - | ConstRef c -> Typeops.type_of_constant env c + | ConstRef c -> + let cb = Environ.lookup_constant c env in + let univs = + Declareops.universes_of_polymorphic_constant + (Environ.opaque_tables env) cb in + let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in + Vars.subst_instance_constr (Univ.UContext.instance univs) ty | IndRef ind -> - let specif = Inductive.lookup_mind_specif env ind in - Inductive.type_of_inductive env specif + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + let inst = + if mib.Declarations.mind_polymorphic then + Univ.UContext.instance mib.Declarations.mind_universes + else Univ.Instance.empty + in + Inductive.type_of_inductive env (specif, inst) | ConstructRef cstr -> - let specif = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Inductive.type_of_constructor cstr specif - -let type_of_global t = type_of_reference (env ()) t - + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + let inst = Univ.UContext.instance mib.Declarations.mind_universes in + Inductive.type_of_constructor (cstr,inst) specif + +let type_of_global_in_context env r = + let open Declarations in + match r with + | VarRef id -> Environ.named_type id env, Univ.UContext.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + let univs = + Declareops.universes_of_polymorphic_constant + (Environ.opaque_tables env) cb in + Typeops.type_of_constant_type env cb.Declarations.const_type, univs + | IndRef ind -> + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + let univs = + if mib.mind_polymorphic then mib.mind_universes + else Univ.UContext.empty + in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs + | ConstructRef cstr -> + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + let univs = + if mib.mind_polymorphic then mib.mind_universes + else Univ.UContext.empty + in + let inst = Univ.UContext.instance univs in + Inductive.type_of_constructor (cstr,inst) specif, univs + +let universes_of_global env r = + let open Declarations in + match r with + | VarRef id -> Univ.UContext.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + Declareops.universes_of_polymorphic_constant + (Environ.opaque_tables env) cb + | IndRef ind -> + let (mib, oib) = Inductive.lookup_mind_specif env ind in + Univ.instantiate_univ_context mib.mind_universes + | ConstructRef cstr -> + let (mib,oib) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + Univ.instantiate_univ_context mib.mind_universes + +let universes_of_global gr = + universes_of_global (env ()) gr + +let is_polymorphic r = + let env = env() in + match r with + | VarRef id -> false + | ConstRef c -> Environ.polymorphic_constant c env + | IndRef ind -> Environ.polymorphic_ind ind env + | ConstructRef cstr -> Environ.polymorphic_ind (inductive_of_constructor cstr) env + +let is_template_polymorphic r = + let env = env() in + match r with + | VarRef id -> false + | ConstRef c -> Environ.template_polymorphic_constant c env + | IndRef ind -> Environ.template_polymorphic_ind ind env + | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env + +let current_dirpath () = + Safe_typing.current_dirpath (safe_env ()) + +let with_global f = + let (a, ctx) = f (env ()) (current_dirpath ()) in + push_context_set ctx; a (* spiwack: register/unregister functions for retroknowledge *) 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 + globalize0 (Safe_typing.register field value by_clause) + +let register_inline c = globalize0 (Safe_typing.register_inline c) +let set_strategy k l = + GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l) |