Imported Upstream version 8.5~beta1+dfsg

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)