Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.

Author: ppedrot

API/API.mli

@@ -2684,10 +2684,8 @@ sig
   val fresh_inductive_instance : Environ.env -> Names.inductive -> Term.pinductive Univ.in_universe_context_set
   val new_Type : Names.DirPath.t -> Term.types
   val type_of_global : Globnames.global_reference -> Term.types Univ.in_universe_context_set
-  val unsafe_type_of_global : Globnames.global_reference -> Term.types
   val constr_of_global : Prelude.global_reference -> Term.constr
   val new_univ_level : Names.DirPath.t -> Univ.Level.t
-  val unsafe_constr_of_global : Globnames.global_reference -> Term.constr Univ.in_universe_context
   val new_sort_in_family : Sorts.family -> Sorts.t
   val pr_with_global_universes : Univ.Level.t -> Pp.std_ppcmds
   val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
@@ -2713,6 +2711,8 @@ sig
   val env_of_context : Environ.named_context_val -> Environ.env
   val is_polymorphic : Globnames.global_reference -> bool
 
+  val constr_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t
+  val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t
   val type_of_global_unsafe : Globnames.global_reference -> Term.types
 
   val current_dirpath : unit -> Names.DirPath.t

engine/termops.ml

@@ -906,7 +906,7 @@ let collect_vars sigma c =
   aux Id.Set.empty c
 
 let vars_of_global_reference env gr =
-  let c, _ = Universes.unsafe_constr_of_global gr in
+  let c, _ = Global.constr_of_global_in_context env gr in
   vars_of_global (Global.env ()) c
 
 (* Tests whether [m] is a subterm of [t]:

engine/universes.ml

@@ -319,9 +319,6 @@ let fresh_instance_from ctx inst =
   let constraints = AUContext.instantiate inst ctx in
     inst, (ctx', constraints)
 
-let unsafe_instance_from ctx =
-  (Univ.AUContext.instance ctx, Univ.instantiate_univ_context ctx)
-    
 (** Fresh universe polymorphic construction *)
 
 let fresh_constant_instance env c inst =
@@ -358,34 +355,6 @@ let fresh_constructor_instance env (ind,i) inst =
     let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
     (((ind,i),inst), ctx)
 
-let unsafe_constant_instance env c =
-  let cb = lookup_constant c env in
-  match cb.Declarations.const_universes with
-  | Declarations.Monomorphic_const _ ->
-    ((c,Instance.empty), UContext.empty)
-  | Declarations.Polymorphic_const auctx ->
-    let inst, ctx = unsafe_instance_from auctx in ((c, inst), ctx)
-
-let unsafe_inductive_instance env ind = 
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  match mib.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ -> ((ind,Instance.empty), UContext.empty)
-  | Declarations.Polymorphic_ind auctx ->
-    let inst, ctx = unsafe_instance_from auctx in ((ind,inst), ctx)
-  | Declarations.Cumulative_ind acumi ->
-    let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in
-    ((ind,inst), ctx)
-
-let unsafe_constructor_instance env (ind,i) = 
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  match mib.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ -> (((ind, i),Instance.empty), UContext.empty)
-  | Declarations.Polymorphic_ind auctx ->
-    let inst, ctx = unsafe_instance_from auctx in (((ind, i),inst), ctx)
-  | Declarations.Cumulative_ind acumi ->
-    let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in
-    (((ind, i),inst), ctx)
-
 open Globnames
 
 let fresh_global_instance ?names env gr =
@@ -410,19 +379,6 @@ let fresh_inductive_instance env sp =
 let fresh_constructor_instance env sp = 
   fresh_constructor_instance env sp None
 
-let unsafe_global_instance env gr =
-  match gr with
-  | VarRef id -> mkVar id, UContext.empty
-  | ConstRef sp -> 
-     let c, ctx = unsafe_constant_instance env sp in
-       mkConstU c, ctx
-  | ConstructRef sp ->
-     let c, ctx = unsafe_constructor_instance env sp in
-       mkConstructU c, ctx
-  | IndRef sp -> 
-     let c, ctx = unsafe_inductive_instance env sp in
-       mkIndU c, ctx
-
 let constr_of_global gr =
   let c, ctx = fresh_global_instance (Global.env ()) gr in
     if not (Univ.ContextSet.is_empty ctx) then
@@ -437,9 +393,6 @@ let constr_of_global gr =
 
 let constr_of_reference = constr_of_global
 
-let unsafe_constr_of_global gr =
-  unsafe_global_instance (Global.env ()) gr
-
 let constr_of_global_univ (gr,u) =
   match gr with
   | VarRef id -> mkVar id
@@ -513,25 +466,6 @@ let type_of_reference env r =
 
 let type_of_global t = type_of_reference (Global.env ()) t
 
-let unsafe_type_of_reference env r =
-  match r with
-  | VarRef id -> Environ.named_type id env
-  | ConstRef c ->
-     let cb = Environ.lookup_constant c env in
-       Typeops.type_of_constant_type env cb.const_type
-
-  | IndRef ind ->
-     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-     let (_, inst), _ = unsafe_inductive_instance env ind in
-       Inductive.type_of_inductive env (specif, inst)
-
-  | ConstructRef (ind, _ as cstr) ->
-     let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-     let (_, inst), _ = unsafe_inductive_instance env ind in
-       Inductive.type_of_constructor (cstr,inst) specif
-
-let unsafe_type_of_global t = unsafe_type_of_reference (Global.env ()) t
-
 let fresh_sort_in_family env = function
   | InProp -> prop_sort, ContextSet.empty
   | InSet -> set_sort, ContextSet.empty

engine/universes.mli

@@ -189,22 +189,11 @@ val constr_of_global : Globnames.global_reference -> constr
 (** ** DEPRECATED ** synonym of [constr_of_global] *)
 val constr_of_reference : Globnames.global_reference -> constr
 
-(** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic
-    references by taking the original universe instance that is not recorded 
-    anywhere. The constraints are forgotten as well. DO NOT USE in new code. *)
-val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context
-
 (** Returns the type of the global reference, by creating a fresh instance of polymorphic 
     references and computing their instantiated universe context. (side-effect on the
     universe counter, use with care). *)
 val type_of_global : Globnames.global_reference -> types in_universe_context_set
 
-(** [unsafe_type_of_global gr] returns [gr]'s type, works on polymorphic
-    references by taking the original universe instance that is not recorded 
-    anywhere. The constraints are forgotten as well. 
-    USE with care. *)
-val unsafe_type_of_global : Globnames.global_reference -> types
-
 (** Full universes substitutions into terms *)
 
 val nf_evars_and_universes_opt_subst : (existential -> constr option) -> 

library/global.ml

@@ -191,6 +191,25 @@ let type_of_global_unsafe r =
     let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
     Inductive.type_of_constructor (cstr,inst) specif
 
+let constr_of_global_in_context env r =
+  let open Constr in
+  match r with
+  | 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 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 univs = Declareops.inductive_polymorphic_context mib in
+    mkConstructU (cstr, Univ.make_abstract_instance univs), univs
+
 let type_of_global_in_context env r = 
   match r with
   | VarRef id -> Environ.named_type id env, Univ.AUContext.empty

library/global.mli

@@ -122,6 +122,13 @@ val is_polymorphic : Globnames.global_reference -> bool
 val is_template_polymorphic : Globnames.global_reference -> bool
 val is_type_in_type : Globnames.global_reference -> bool
 
+val constr_of_global_in_context : Environ.env ->
+  Globnames.global_reference -> Constr.types * Univ.AUContext.t
+(** Returns the type of the constant in its local universe
+    context. The type should not be used without pushing it's universe
+    context in the environmnent of usage. For non-universe-polymorphic
+    constants, it does not matter. *)
+
 val type_of_global_in_context : Environ.env -> 
   Globnames.global_reference -> Constr.types * Univ.AUContext.t
 (** Returns the type of the constant in its local universe

plugins/funind/functional_principles_types.ml

@@ -651,7 +651,7 @@ let build_case_scheme fa =
 (*   in  *)
   let funs =
     let (_,f,_) = fa in
-    try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
+    try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f))
     with Not_found ->
       user_err ~hdr:"FunInd.build_case_scheme"
         (str "Cannot find " ++ Libnames.pr_reference f) in

plugins/funind/recdef.ml

@@ -90,7 +90,7 @@ let type_of_const sigma t =
     |_ -> assert false
 
 let constr_of_global x = 
-  fst (Universes.unsafe_constr_of_global x)
+  fst (Global.constr_of_global_in_context (Global.env ()) x)
 
 let constant sl s = constr_of_global (find_reference sl s)
 

plugins/ssr/ssrvernac.ml4

@@ -337,7 +337,8 @@ let coerce_search_pattern_to_sort hpat =
     Pattern.PApp (fp, args') in
   let hr, na = splay_search_pattern 0 hpat in
   let dc, ht =
-    Reductionops.splay_prod env sigma (EConstr.of_constr (Universes.unsafe_type_of_global hr)) in
+    let hr, _ = Global.type_of_global_in_context (Global.env ()) hr (** FIXME *) in
+    Reductionops.splay_prod env sigma (EConstr.of_constr hr) in
   let np = List.length dc in
   if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else
   let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in

pretyping/classops.ml

@@ -403,7 +403,7 @@ type coercion = {
 (* Computation of the class arity *)
 
 let reference_arity_length ref =
-  let t = Universes.unsafe_type_of_global ref in
+  let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
   List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *)
 
 let projection_arity_length p =

pretyping/pretyping.ml

@@ -511,8 +511,8 @@ let pretype_global ?loc rigid env evd gr us =
     match us with
     | None -> evd, None
     | Some l -> 
-       let _, ctx = Universes.unsafe_constr_of_global gr in
-       let len = Univ.UContext.size ctx in
+       let _, ctx = Global.constr_of_global_in_context env.ExtraEnv.env gr in
+       let len = Univ.AUContext.size ctx in
        interp_instance ?loc evd ~len l
   in
   let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in

printing/prettyp.ml

@@ -798,9 +798,11 @@ let print_opaque_name qid =
     | IndRef (sp,_) ->
         print_inductive sp
     | ConstructRef cstr as gr ->
-        let open EConstr in
-	let ty = Universes.unsafe_type_of_global gr in
+	let ty, ctx = Global.type_of_global_in_context env gr in
+	let inst = Univ.AUContext.instance ctx in
+	let ty = Vars.subst_instance_constr inst ty in
 	let ty = EConstr.of_constr ty in
+        let open EConstr in
 	print_typed_value (mkConstruct cstr, ty)
     | VarRef id ->
         env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl

tactics/tactics.ml

@@ -5004,7 +5004,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   in
   let cst = Impargs.with_implicit_protection cst () in
   (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *)
-  let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in
+  let lem, ctx = Global.constr_of_global_in_context (Global.env ()) (ConstRef cst) in
+  let inst = Univ.AUContext.instance ctx in
+  let lem = CVars.subst_instance_constr inst lem in
   let lem = EConstr.of_constr lem in
   let evd = Evd.set_universe_context evd ectx in
   let open Safe_typing in