Merge PR #8842: Towards seeing Global purely as a wrapper on top of kernel functions

13 files changed, 63 insertions, 52 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 181efa0ade..52880846f8 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1179,7 +1179,7 @@ let isGlobalRef sigma c =
   | Const _ | Ind _ | Construct _ | Var _ -> true
   | _ -> false
 
-let is_template_polymorphic env sigma f =
+let is_template_polymorphic_ind env sigma f =
   match EConstr.kind sigma f with
   | Ind (ind, u) ->
     if not (EConstr.EInstance.is_empty u) then false
diff --git a/engine/termops.mli b/engine/termops.mli
index 1054fbbc5e..07c9541f25 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -282,7 +282,7 @@ val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool
 
 val isGlobalRef : Evd.evar_map -> constr -> bool
 
-val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool
+val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool
 
 val is_Prop : Evd.evar_map -> constr -> bool
 val is_Set : Evd.evar_map -> constr -> bool
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 3b7e3ae544..e341412294 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -440,6 +440,16 @@ let constant_value_and_type env (kn, u) =
 	| Undef _ -> None
       in b', cb.const_type, Univ.Constraint.empty
 
+let body_of_constant_body env cb =
+  let otab = opaque_tables env in
+  match cb.const_body with
+  | Undef _ ->
+     None
+  | Def c ->
+     Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
+  | OpaqueDef o ->
+     Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb)
+
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
    application. *)
@@ -694,6 +704,22 @@ let is_polymorphic env r =
   | IndRef ind -> polymorphic_ind ind env
   | ConstructRef cstr -> polymorphic_ind (inductive_of_constructor cstr) env
 
+let is_template_polymorphic env r =
+  let open Names.GlobRef in
+  match r with
+  | VarRef _id -> false
+  | ConstRef _c -> false
+  | IndRef ind -> template_polymorphic_ind ind env
+  | ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env
+
+let is_type_in_type env r =
+  let open Names.GlobRef in
+  match r with
+  | VarRef _id -> false
+  | ConstRef c -> type_in_type_constant c env
+  | IndRef ind -> type_in_type_ind ind env
+  | ConstructRef cstr -> type_in_type_ind (inductive_of_constructor cstr) env
+
 (*spiwack: the following functions assemble the pieces of the retroknowledge
    note that the "consistent" register function is available in the module
    Safetyping, Environ only synchronizes the proactive and the reactive parts*)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 43bfe7c2fb..0255581749 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -211,6 +211,12 @@ val constant_value_and_type : env -> Constant.t puniverses ->
     polymorphic *)
 val constant_context : env -> Constant.t -> Univ.AUContext.t
 
+(** Returns the body of the constant if it has any, and the polymorphic context
+    it lives in. For monomorphic constant, the latter is empty, and for
+    polymorphic constants, the term contains De Bruijn universe variables that
+    need to be instantiated. *)
+val body_of_constant_body : env -> constant_body -> (Constr.constr * Univ.AUContext.t) option
+
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
    application. *)
@@ -320,6 +326,8 @@ val apply_to_hyp : named_context_val -> variable ->
 val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val
 
 val is_polymorphic : env -> Names.GlobRef.t -> bool
+val is_template_polymorphic : env -> GlobRef.t -> bool
+val is_type_in_type : env -> GlobRef.t -> bool
 
 open Retroknowledge
 (** functions manipulating the retroknowledge 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 12f9592ab7..779e05ee0c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -194,6 +194,10 @@ let set_engagement c senv =
 let set_typing_flags c senv =
   { senv with env = Environ.set_typing_flags c senv.env }
 
+let set_share_reduction b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with share_reduction = b } senv
+
 (** Check that the engagement [c] expected by a library matches
     the current (initial) one *)
 let check_engagement env expected_impredicative_set =
@@ -1190,7 +1194,7 @@ loaded by side-effect once and for all (like it is done in OCaml).
 Would this be correct with respect to undo's and stuff ?
 *)
 
-let set_strategy e k l = { e with env =
+let set_strategy k l e = { e with env =
    (Environ.set_oracle e.env
       (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) }
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 26fa91adbd..443b5cfd73 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -137,6 +137,7 @@ val add_constraints :
 (** Setting the type theory flavor *)
 val set_engagement : Declarations.engagement -> safe_transformer0
 val set_typing_flags : Declarations.typing_flags -> safe_transformer0
+val set_share_reduction : bool -> safe_transformer0
 
 (** {6 Interactive module functions } *)
 
@@ -217,4 +218,4 @@ val register :
 val register_inline : Constant.t -> safe_transformer0
 
 val set_strategy :
-  safe_environment -> Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_environment
+  Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0
diff --git a/library/global.ml b/library/global.ml
index 3781ff3230..bfea6d3dea 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -128,19 +128,7 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ())
 
 let opaque_tables () = Environ.opaque_tables (env ())
 
-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_body ce = body_of_constant_body (env ()) ce
 
 let body_of_constant cst = body_of_constant_body (lookup_constant cst)
 
@@ -165,8 +153,6 @@ let import c u d = globalize (Safe_typing.import c u d)
 let env_of_context hyps =
   reset_with_named_context hyps (env())
 
-open Globnames
-
 let constr_of_global_in_context = Typeops.constr_of_global_in_context
 let type_of_global_in_context = Typeops.type_of_global_in_context
 
@@ -175,21 +161,9 @@ let universes_of_global gr =
 
 let is_polymorphic r = Environ.is_polymorphic (env()) r
 
-let is_template_polymorphic r = 
-  let env = env() in 
-  match r with
-  | VarRef id -> false
-  | ConstRef c -> false
-  | IndRef ind -> Environ.template_polymorphic_ind ind env
-  | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env
-
-let is_type_in_type r =
-  let env = env() in
-  match r with
-  | VarRef id -> false
-  | ConstRef c -> Environ.type_in_type_constant c env
-  | IndRef ind -> Environ.type_in_type_ind ind env
-  | ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env
+let is_template_polymorphic r = is_template_polymorphic (env ()) r
+
+let is_type_in_type r = is_type_in_type (env ()) r
 
 let current_modpath () =
   Safe_typing.current_modpath (safe_env ())
@@ -208,11 +182,7 @@ let register field value =
 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)
-
-let set_reduction_sharing b =
-  let env = safe_env () in
-  let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in
-  let flags = { flags with Declarations.share_reduction = b } in
-  let env = Safe_typing.set_typing_flags flags env in
-  GlobalSafeEnv.set_safe_env env
+  globalize0 (Safe_typing.set_strategy k l)
+
+let set_share_reduction b =
+  globalize0 (Safe_typing.set_share_reduction b)
diff --git a/library/global.mli b/library/global.mli
index 42a8005a4f..762a3f006d 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -150,7 +150,9 @@ val register_inline : Constant.t -> unit
 
 val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
 
-val set_reduction_sharing : bool -> unit
+(** {6 Conversion settings } *)
+
+val set_share_reduction : bool -> unit
 
 (* Modifies the global state, registering new universes *)
 
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index dd38ec6f64..96213af9c6 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -83,7 +83,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   (** Refresh the types of evars under template polymorphic references *)
   let rec refresh_term_evars ~onevars ~top t =
     match EConstr.kind !evdref t with
-    | App (f, args) when is_template_polymorphic env !evdref f ->
+    | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f ->
       let pos = get_polymorphic_positions !evdref f in
         refresh_polymorphic_positions args pos; t
     | App (f, args) when top && isEvar !evdref f -> 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 24767ca4d1..cba1533da5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -692,7 +692,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
     let sigma, resj =
       match EConstr.kind sigma resj.uj_val with
       | App (f,args) ->
-          if is_template_polymorphic !!env sigma f then
+          if Termops.is_template_polymorphic_ind !!env sigma f then
 	    (* Special case for inductive type applications that must be 
 	       refreshed right away. *)
             let c = mkApp (f, args) in
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 7e43c5e41d..62ad296ecb 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -130,7 +130,7 @@ let retype ?(polyprop=true) sigma =
          subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2)
     | Fix ((_,i),(_,tys,_)) -> tys.(i)
     | CoFix (i,(_,tys,_)) -> tys.(i)
-    | App(f,args) when is_template_polymorphic env sigma f ->
+    | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
 	let t = type_of_global_reference_knowing_parameters env f args in
         strip_outer_cast sigma (subst_type env sigma t (Array.to_list args))
     | App(f,args) ->
@@ -156,7 +156,7 @@ let retype ?(polyprop=true) sigma =
       let dom = sort_of env t in
       let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in
       Typeops.sort_of_product env dom rang
-    | App(f,args) when is_template_polymorphic env sigma f ->
+    | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
       let t = type_of_global_reference_knowing_parameters env f args in
         sort_of_atomic_type env sigma t args
     | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
@@ -190,14 +190,14 @@ let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t =
 	let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in
 	if not (is_impredicative_set env) &&
 	   s2 == InSet && sort_family_of env t == InType then InType else s2
-    | App(f,args) when is_template_polymorphic env sigma f ->
+    | App(f,args) when Termops.is_template_polymorphic_ind env sigma f ->
         if truncation_style then InType else
 	let t = type_of_global_reference_knowing_parameters env f args in
         Sorts.family (sort_of_atomic_type env sigma t args)
     | App(f,args) ->
 	Sorts.family (sort_of_atomic_type env sigma (type_of env f) args)
     | Lambda _ | Fix _ | Construct _ -> retype_error NotAType
-    | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType
+    | Ind _ when truncation_style && Termops.is_template_polymorphic_ind env sigma t -> InType
     | _ -> 
       Sorts.family (decomp_sort env sigma (type_of env t))
   in sort_family_of env t
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b8612cd2c0..4d5711c195 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -384,7 +384,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 
       | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
-	  if is_template_polymorphic env sigma (EConstr.of_constr f) then
+          if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f) then
 	    let ty = 
 	      (* Template polymorphism of definitions and inductive types *)
 	      let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in
@@ -447,7 +447,7 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
-	  if is_template_polymorphic env sigma (EConstr.of_constr f)
+          if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f)
 	  then
 	    let l' = meta_free_prefix sigma l in
 	   (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1190d73258..5eace14cbf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1536,7 +1536,7 @@ let _ =
       optname  = "kernel term sharing";
       optkey   = ["Kernel"; "Term"; "Sharing"];
       optread  = (fun () -> (Global.typing_flags ()).Declarations.share_reduction);
-      optwrite = (fun b -> Global.set_reduction_sharing b) }
+      optwrite = Global.set_share_reduction }
 
 let _ =
   declare_bool_option