Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 71 insertions, 62 deletions

diff --git a/library/global.ml b/library/global.ml
index e748434d..dcb20a28 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Names
@@ -20,6 +22,7 @@ module GlobalSafeEnv : sig
   val set_safe_env : Safe_typing.safe_environment -> unit
   val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
   val is_joined_environment : unit -> bool
+  val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag
 
 end = struct
 
@@ -30,9 +33,9 @@ let join_safe_environment ?except () =
 
 let is_joined_environment () =
   Safe_typing.is_joined_environment !global_env
-  
-let () =
-  Summary.declare_summary global_env_summary_name
+
+let global_env_summary_tag =
+  Summary.declare_summary_tag global_env_summary_name
     { Summary.freeze_function = (function
         | `Yes -> join_safe_environment (); !global_env
         | `No -> !global_env
@@ -43,7 +46,7 @@ let () =
 let assert_not_parsing () =
   if !Flags.we_are_parsing then
     CErrors.anomaly (
-      Pp.strbrk"The global environment cannot be accessed during parsing")
+      Pp.strbrk"The global environment cannot be accessed during parsing.")
 
 let safe_env () = assert_not_parsing(); !global_env
 
@@ -51,6 +54,8 @@ let set_safe_env e = global_env := e
 
 end
 
+let global_env_summary_tag = GlobalSafeEnv.global_env_summary_tag
+
 let safe_env = GlobalSafeEnv.safe_env
 let join_safe_environment ?except () =
   GlobalSafeEnv.join_safe_environment ?except ()
@@ -78,13 +83,14 @@ let globalize_with_summary fs f =
 let i2l = Label.of_id
 
 let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
-let push_named_def d = globalize (Safe_typing.push_named_def d)
+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 b c = globalize0 (Safe_typing.push_context_set b c)
 let push_context b c = globalize0 (Safe_typing.push_context b c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
+let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
 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)
@@ -121,12 +127,22 @@ 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 instantiate cb c =
+  let open Declarations in
+  match cb.const_universes with
+  | Monomorphic_const _ -> c, Univ.AUContext.empty
+  | Polymorphic_const ctx -> c, ctx
+
+let body_of_constant_body cb =
+  let open Declarations in
+  let otab = opaque_tables () in
+  match cb.const_body with
+  | Undef _ -> None
+  | Def c -> Some (instantiate cb (Mod_subst.force_constr c))
+  | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o))
+
 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 *)
 
@@ -162,74 +178,64 @@ open Globnames
 (** 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
+let constr_of_global_in_context env r =
+  let open Constr in
   match r with
-  | VarRef id -> Environ.named_type id env
-  | 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
+  | VarRef id -> mkVar id, Univ.AUContext.empty
+  | ConstRef c ->
+    let cb = Environ.lookup_constant c env in
+    let univs = Declareops.constant_polymorphic_context cb in
+    mkConstU (c, Univ.make_abstract_instance univs), univs
   | IndRef ind ->
-     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)
+    let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    mkIndU (ind, Univ.make_abstract_instance univs), univs
   | ConstructRef cstr ->
-     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 (mib,oib as specif) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
+    in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    mkConstructU (cstr, Univ.make_abstract_instance univs), univs
 
 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
+  | VarRef id -> Environ.named_type id env, Univ.AUContext.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
+    let cb = Environ.lookup_constant c env in 
+    let univs = Declareops.constant_polymorphic_context cb in
+    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 Univ.instantiate_univ_context mib.mind_universes 
-       else Univ.UContext.empty
-     in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs
+    let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    let inst = Univ.make_abstract_instance univs in
+    let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in
+    Inductive.type_of_inductive env (specif, inst), 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 Univ.instantiate_univ_context mib.mind_universes 
-       else Univ.UContext.empty
-     in
-     let inst = Univ.UContext.instance univs in
-       Inductive.type_of_constructor (cstr,inst) specif, univs
+    let (mib,oib as specif) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr) 
+    in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    let inst = Univ.make_abstract_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
+    | VarRef id -> Univ.AUContext.empty
     | ConstRef c -> 
       let cb = Environ.lookup_constant c env in 
-	Declareops.universes_of_polymorphic_constant
-          (Environ.opaque_tables env) cb
+      Declareops.constant_polymorphic_context cb
     | IndRef ind ->
       let (mib, oib) = Inductive.lookup_mind_specif env ind in
-	Univ.instantiate_univ_context mib.mind_universes 
+      Declareops.inductive_polymorphic_context mib
     | ConstructRef cstr ->
-      let (mib,oib) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-	Univ.instantiate_univ_context mib.mind_universes 
+      let (mib,oib) = 
+        Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+      Declareops.inductive_polymorphic_context mib
 
 let universes_of_global gr = 
   universes_of_global (env ()) gr
 
-let is_polymorphic r = 
+let is_polymorphic r =
   let env = env() in 
   match r with
   | VarRef id -> false
@@ -241,7 +247,7 @@ let is_template_polymorphic r =
   let env = env() in 
   match r with
   | VarRef id -> false
-  | ConstRef c -> Environ.template_polymorphic_constant c env
+  | ConstRef c -> false
   | IndRef ind -> Environ.template_polymorphic_ind ind env
   | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env
 
@@ -253,6 +259,9 @@ let is_type_in_type r =
   | IndRef ind -> Environ.type_in_type_ind ind env
   | ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env
 
+let current_modpath () =
+  Safe_typing.current_modpath (safe_env ())
+
 let current_dirpath () = 
   Safe_typing.current_dirpath (safe_env ())