Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers

7 files changed, 42 insertions, 44 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 948aa26ca..078990a8c 100644
--- a/pretyping/classops.ml
+++ b/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 =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 87f29ba49..cb76df4e8 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -205,7 +205,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
       else match (Stack.strip_n_app (l_us-1) sk2_effective) with
       | None -> raise Not_found
       | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
-  let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
+  let u, ctx' = Universes.fresh_instance_from ctx None in
+  let subst = Univ.make_inverse_instance_subst u in
   let c = EConstr.of_constr c in
   let c' = subst_univs_level_constr subst c in
   let t' = EConstr.of_constr t' in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e166e0e9d..bfc6bf5cf 100644
--- a/pretyping/pretyping.ml
+++ b/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
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index c498089ca..a23579609 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -134,7 +134,7 @@ let find_projection = function
 
 type obj_typ = {
   o_DEF : constr;
-  o_CTX : Univ.ContextSet.t;
+  o_CTX : Univ.AUContext.t;
   o_INJ : int option;      (* position of trivial argument if any *)
   o_TABS : constr list;    (* ordered *)
   o_TPARAMS : constr list; (* ordered *)
@@ -203,10 +203,8 @@ let warn_projection_no_head_constant =
 let compute_canonical_projections warn (con,ind) =
   let env = Global.env () in
   let ctx = Environ.constant_context env con in
-  let u = Univ.AUContext.instance ctx in
-  let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
+  let u = Univ.make_abstract_instance ctx in
   let v = (mkConstU (con,u)) in
-  let ctx = Univ.ContextSet.of_context ctx in
   let c = Environ.constant_value_in env (con,u) in
   let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
   let t = EConstr.Unsafe.to_constr t in
@@ -302,7 +300,7 @@ let error_not_structure ref =
 let check_and_decompose_canonical_structure ref =
   let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
   let env = Global.env () in
-  let u = Univ.AUContext.instance (Environ.constant_context env sp) in
+  let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
   let vc = match Environ.constant_opt_value_in env (sp, u) with
     | Some vc -> vc
     | None -> error_not_structure ref in
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 27d1650af..de09edcdc 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -57,7 +57,7 @@ type cs_pattern =
 
 type obj_typ = {
   o_DEF : constr;
-  o_CTX : Univ.ContextSet.t;
+  o_CTX : Univ.AUContext.t;
   o_INJ : int option;      (** position of trivial argument *)
   o_TABS : constr list;    (** ordered *)
   o_TPARAMS : constr list; (** ordered *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index bae831b63..d4fa266c0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -57,6 +57,9 @@ type direction = Forward | Backward
 
 (* This module defines type-classes *)
 type typeclass = {
+  (* Universe quantification *)
+  cl_univs : Univ.AUContext.t;
+
   (* The class implementation *)
   cl_impl : global_reference;
 
@@ -111,23 +114,11 @@ let new_instance cl info glob poly impl =
 let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes"
 let instances : instances ref = Summary.ref Refmap.empty ~name:"instances"
 
-let typeclass_univ_instance (cl,u') =
-  let subst = 
-    let u = 
-      match cl.cl_impl with
-      | ConstRef c -> 
-        let cb = Global.lookup_constant c in
-        Univ.AUContext.instance (Declareops.constant_polymorphic_context cb)
-      | IndRef c ->
-         let mib,oib = Global.lookup_inductive c in
-         Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
-      | _ -> Univ.Instance.empty
-    in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) 
-      Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
-  in
-  let subst_ctx = Context.Rel.map (subst_univs_level_constr subst) in
-    { cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context);
-      cl_props = subst_ctx cl.cl_props}, u'
+let typeclass_univ_instance (cl, u) =
+  assert (Univ.AUContext.size cl.cl_univs == Univ.Instance.length u);
+  let subst_ctx c = Context.Rel.map (subst_instance_constr u) c in
+    { cl with cl_context = on_snd subst_ctx cl.cl_context;
+      cl_props = subst_ctx cl.cl_props}
 
 let class_info c =
   try Refmap.find c !classes
@@ -185,7 +176,8 @@ let subst_class (subst,cl) =
     do_subst_ctx ctx in
   let do_subst_projs projs = List.smartmap (fun (x, y, z) -> 
     (x, y, Option.smartmap do_subst_con z)) projs in
-  { cl_impl = do_subst_gr cl.cl_impl;
+  { cl_univs = cl.cl_univs;
+    cl_impl = do_subst_gr cl.cl_impl;
     cl_context = do_subst_context cl.cl_context;
     cl_props = do_subst_ctx cl.cl_props;
     cl_projs = do_subst_projs cl.cl_projs;
@@ -199,15 +191,14 @@ let discharge_class (_,cl) =
         let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in
 	(decl' :: ctx', NamedDecl.get_id decl :: subst)
     ) ctx ([], []) in
-  let discharge_rel_context subst n rel =
+  let discharge_rel_context (subst, usubst) n rel =
     let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
-    let ctx, _ =
-      List.fold_right
-	(fun decl (ctx, k) ->
-	   RelDecl.map_constr (substn_vars k subst) decl :: ctx, succ k
-	)
-	rel ([], n)
-    in ctx
+    let fold decl (ctx, k) =
+      let map c = subst_univs_level_constr usubst (substn_vars k subst c) in
+      RelDecl.map_constr map decl :: ctx, succ k
+    in
+    let ctx, _ = List.fold_right fold rel ([], n) in
+    ctx
   in
   let abs_context cl =
     match cl.cl_impl with
@@ -227,12 +218,14 @@ let discharge_class (_,cl) =
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
   let cl_impl' = Lib.discharge_global cl.cl_impl in
   if cl_impl' == cl.cl_impl then cl else
-    let ctx, usubst, uctx = abs_context cl in
+    let ctx, _, _ as info = abs_context cl in
     let ctx, subst = rel_of_variable_context ctx in
-    let context = discharge_context ctx subst cl.cl_context in
-    let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in
+    let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
+    let context = discharge_context ctx (subst, usubst) cl.cl_context in
+    let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
     let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in
-      { cl_impl = cl_impl';
+      { cl_univs = cl_univs';
+        cl_impl = cl_impl';
 	cl_context = context;
 	cl_props = props;
 	cl_projs = List.smartmap discharge_proj cl.cl_projs;
@@ -279,8 +272,10 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
         Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i))
   in
   let ty, ctx = Global.type_of_global_in_context env glob in
+  let inst, ctx = Universes.fresh_instance_from ctx None in
+  let ty = Vars.subst_instance_constr inst ty in
   let ty = EConstr.of_constr ty in
-  let sigma = Evd.merge_context_set Evd.univ_rigid sigma (Univ.ContextSet.of_context ctx) in
+  let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
   let rec aux pri c ty path =
       match class_of_constr sigma ty with
       | None -> []
@@ -317,7 +312,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
 	    hints @ (path', info, body) :: rest
 	in List.fold_left declare_proj [] projs 
   in
-  let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in
+  let term = Universes.constr_of_global_univ (glob, inst) in
     (*FIXME subclasses should now get substituted for each particular instance of
       the polymorphic superclass *)
     aux pri term ty [glob]
@@ -405,7 +400,7 @@ let remove_instance i =
   remove_instance_hint i.is_impl
 
 let declare_instance info local glob =
-  let ty = Global.type_of_global_unsafe glob in
+  let ty, _ = Global.type_of_global_in_context (Global.env ()) glob in
   let info = Option.default {hint_priority = None; hint_pattern = None} info in
     match class_of_constr Evd.empty (EConstr.of_constr ty) with
     | Some (rels, ((tc,_), args) as _cl) ->
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index a8e90ca17..99cdbd3a3 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -16,6 +16,10 @@ type direction = Forward | Backward
 
 (** This module defines type-classes *)
 type typeclass = {
+  (** The toplevel universe quantification in which the typeclass lives. In
+      particular, [cl_props] and [cl_context] are quantified over it. *)
+  cl_univs : Univ.AUContext.t;
+
   (** The class implementation: a record parameterized by the context with defs in it or a definition if
      the class is a singleton. This acts as the class' global identifier. *)
   cl_impl : global_reference;
@@ -64,7 +68,7 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c
 val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.EInstance.t) * constr list
 
 (** Get the instantiated typeclass structure for a given universe instance. *)
-val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses
+val typeclass_univ_instance : typeclass puniverses -> typeclass
 
 (** Just return None if not a class *)
 val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option