Simplify fresh_foo_instance functions and pretyping of univ instance

7 files changed, 55 insertions, 94 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index d7b03a84f1..eafdc4cb46 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -818,7 +818,7 @@ let fresh_constructor_instance ?loc env evd c =
   with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c)
 
 let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
-  with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr)
+  with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr)
 
 let is_sort_variable evd s = UState.is_sort_variable evd.universes s
 
diff --git a/engine/univGen.ml b/engine/univGen.ml
index b07d4848ff..64789cb808 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -11,7 +11,6 @@
 open Sorts
 open Names
 open Constr
-open Environ
 open Univ
 
 (* Generator of levels *)
@@ -50,21 +49,20 @@ let fresh_instance ctx =
   let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
   in !ctx', inst
 
-let existing_instance ctx inst =
+let existing_instance ?loc ctx inst =
   let () =
     let len1 = Array.length (Instance.to_array inst)
     and len2 = AUContext.size ctx in
       if not (len1 == len2) then
-        CErrors.user_err ~hdr:"Universes"
-          Pp.(str "Polymorphic constant expected " ++ int len2 ++
-              str" levels but was given " ++ int len1)
+        CErrors.user_err ?loc ~hdr:"Universes"
+          Pp.(str "Universe instance should have length " ++ int len2 ++ str ".")
       else ()
   in LSet.empty, inst
 
-let fresh_instance_from ctx inst =
+let fresh_instance_from ?loc ctx inst =
   let ctx', inst =
     match inst with
-    | Some inst -> existing_instance ctx inst
+    | Some inst -> existing_instance ?loc ctx inst
     | None -> fresh_instance ctx
   in
   let constraints = AUContext.instantiate inst ctx in
@@ -72,63 +70,28 @@ let fresh_instance_from ctx inst =
 
 (** Fresh universe polymorphic construction *)
 
-let fresh_constant_instance env c inst =
-  let cb = lookup_constant c env in
-  match cb.Declarations.const_universes with
-  | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_const auctx ->
-    let inst, ctx =
-      fresh_instance_from auctx inst
-    in
-    ((c, inst), ctx)
-
-let fresh_inductive_instance env ind inst =
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  match mib.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ ->
-    ((ind,Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_ind uactx ->
-    let inst, ctx = (fresh_instance_from uactx) inst in
-     ((ind,inst), ctx)
-  | Declarations.Cumulative_ind acumi ->
-    let inst, ctx =
-      fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst
-    in ((ind,inst), ctx)
-
-let fresh_constructor_instance env (ind,i) inst =
-  let mib, mip = Inductive.lookup_mind_specif env ind in
-  match mib.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty)
-  | Declarations.Polymorphic_ind auctx ->
-    let inst, ctx = fresh_instance_from auctx  inst in
-        (((ind,i),inst), ctx)
-  | Declarations.Cumulative_ind acumi ->
-    let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
-    (((ind,i),inst), ctx)
-
 open Globnames
 
-let fresh_global_instance ?names env gr =
-  match gr with
-  | VarRef id -> mkVar id, ContextSet.empty
-  | ConstRef sp ->
-     let c, ctx = fresh_constant_instance env sp names in
-       mkConstU c, ctx
-  | ConstructRef sp ->
-     let c, ctx = fresh_constructor_instance env sp names in
-       mkConstructU c, ctx
-  | IndRef sp ->
-     let c, ctx = fresh_inductive_instance env sp names in
-       mkIndU c, ctx
-
-let fresh_constant_instance env sp =
-  fresh_constant_instance env sp None
-
-let fresh_inductive_instance env sp =
-  fresh_inductive_instance env sp None
-
-let fresh_constructor_instance env sp =
-  fresh_constructor_instance env sp None
+let fresh_global_instance ?loc ?names env gr =
+  let auctx = Environ.universes_of_global env gr in
+  let u, ctx = fresh_instance_from ?loc auctx names in
+  u, ctx
+
+let fresh_constant_instance env c =
+  let u, ctx = fresh_global_instance env (ConstRef c) in
+  (c, u), ctx
+
+let fresh_inductive_instance env ind =
+  let u, ctx = fresh_global_instance env (IndRef ind) in
+  (ind, u), ctx
+
+let fresh_constructor_instance env c =
+  let u, ctx = fresh_global_instance env (ConstructRef c) in
+  (c, u), ctx
+
+let fresh_global_instance ?loc ?names env gr =
+  let u, ctx = fresh_global_instance ?loc ?names env gr in
+  mkRef (gr, u), ctx
 
 let constr_of_global gr =
   let c, ctx = fresh_global_instance (Global.env ()) gr in
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 439424934c..4cfbb94775 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -36,7 +36,7 @@ val new_sort_in_family : Sorts.family -> Sorts.t
 val fresh_instance_from_context : AUContext.t ->
   Instance.t constrained
 
-val fresh_instance_from : AUContext.t -> Instance.t option ->
+val fresh_instance_from : ?loc:Loc.t -> AUContext.t -> Instance.t option ->
   Instance.t in_universe_context_set
 
 val fresh_sort_in_family : Sorts.family ->
@@ -48,7 +48,7 @@ val fresh_inductive_instance : env -> inductive ->
 val fresh_constructor_instance : env -> constructor ->
   pconstructor in_universe_context_set
 
-val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t ->
+val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t ->
   constr in_universe_context_set
 
 val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
diff --git a/kernel/constr.ml b/kernel/constr.ml
index c97969c0e0..7ffde3107b 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -227,6 +227,12 @@ let mkMeta  n =  Meta n
 (* Constructs a Variable named id *)
 let mkVar id = Var id
 
+let mkRef (gr,u) = let open GlobRef in match gr with
+  | ConstRef c -> mkConstU (c,u)
+  | IndRef ind -> mkIndU (ind,u)
+  | ConstructRef c -> mkConstructU (c,u)
+  | VarRef x -> mkVar x
+
 (************************************************************************)
 (*    kind_of_term = constructions as seen by the user                 *)
 (************************************************************************)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 3c9cc96a0d..12819ac39d 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -128,6 +128,9 @@ val mkConstruct : constructor -> constr
 val mkConstructU : pconstructor -> constr
 val mkConstructUi : pinductive * int -> constr
 
+(** Make a constant, inductive, constructor or variable. *)
+val mkRef : GlobRef.t Univ.puniverses -> constr
+
 (** Constructs a destructor of inductive type.
     
     [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 1feb47d387..757c8773b7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -419,12 +419,6 @@ let constant_type env (kn,u) =
     let csts = constraints_of cb u in
     (subst_instance_constr u cb.const_type, csts)
 
-let constant_context env kn =
-  let cb = lookup_constant kn env in
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.AUContext.empty
-  | Polymorphic_const ctx -> ctx
-
 type const_evaluation_result = NoBody | Opaque
 
 exception NotEvaluableConst of const_evaluation_result
@@ -551,13 +545,15 @@ let lookup_constructor_variables (ind,_) env =
   lookup_inductive_variables ind env
 
 (* Universes *)
+let constant_context env c =
+  let cb = lookup_constant c env in
+  Declareops.constant_polymorphic_context cb
+
 let universes_of_global env r =
   let open GlobRef in
     match r with
     | VarRef _ -> Univ.AUContext.empty
-    | ConstRef c ->
-      let cb = lookup_constant c env in
-      Declareops.constant_polymorphic_context cb
+    | ConstRef c -> constant_context env c
     | IndRef (mind,_) | ConstructRef ((mind,_),_) ->
       let mib = lookup_mind mind env in
       Declareops.inductive_polymorphic_context mib
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 495f5c0660..f2881e4a19 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -405,32 +405,25 @@ let interp_glob_level ?loc evd : glob_level -> _ = function
   | GSet -> evd, Univ.Level.set
   | GType s -> interp_level_info ?loc evd s
 
-let interp_instance ?loc evd ~len l =
-  if len != List.length l then
+let interp_instance ?loc evd l =
+  let evd, l' =
+    List.fold_left
+      (fun (evd, univs) l ->
+         let evd, l = interp_glob_level ?loc evd l in
+         (evd, l :: univs)) (evd, [])
+      l
+  in
+  if List.exists (fun l -> Univ.Level.is_prop l) l' then
     user_err ?loc ~hdr:"pretype"
-      (str "Universe instance should have length " ++ int len)
-  else
-    let evd, l' =
-      List.fold_left
-        (fun (evd, univs) l ->
-	  let evd, l = interp_glob_level ?loc evd l in
-	  (evd, l :: univs)) (evd, [])
-        l
-    in
-    if List.exists (fun l -> Univ.Level.is_prop l) l' then
-      user_err ?loc ~hdr:"pretype"
-	(str "Universe instances cannot contain Prop, polymorphic" ++
-	   str " universe instances must be greater or equal to Set.");
-    evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
+      (str "Universe instances cannot contain Prop, polymorphic" ++
+       str " universe instances must be greater or equal to Set.");
+  evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
 
 let pretype_global ?loc rigid env evd gr us = 
   let evd, instance = 
     match us with
     | None -> evd, None
-    | Some l -> 
-       let _, ctx = Global.constr_of_global_in_context !!env gr in
-       let len = Univ.AUContext.size ctx in
-       interp_instance ?loc evd ~len l
+    | Some l -> interp_instance ?loc evd l
   in
   Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr