Merge PR coq#870: Prepare De Bruijn universe abstractions, Episode I:…

… Kernel

API/API.mli

@@ -4669,8 +4669,6 @@ sig
   val constant_has_body : Declarations.constant_body -> bool
   val is_opaque : Declarations.constant_body -> bool
   val eq_recarg : Declarations.recarg -> Declarations.recarg -> bool
-  val body_of_constant :
-    Opaqueproof.opaquetab -> Declarations.constant_body -> Term.constr option
 end
 
 module Constr :

checker/environ.ml

@@ -122,8 +122,7 @@ type const_evaluation_result = NoBody | Opaque | IsProj
 let constraints_of cb u =
   match cb.const_universes with
   | Monomorphic_const _ -> Univ.Constraint.empty
-  | Polymorphic_const ctx -> 
-    Univ.UContext.constraints (Univ.subst_instance_context u ctx)
+  | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
 
 let map_regular_arity f = function
   | RegularArity a as ar -> 

checker/inductive.ml

@@ -66,20 +66,6 @@ let inductive_is_cumulative mib =
   | Polymorphic_ind ctx -> false
   | Cumulative_ind cumi -> true
 
-let inductive_polymorphic_instance mib =
-  match mib.mind_universes with
-  | Monomorphic_ind _ -> Univ.Instance.empty
-  | Polymorphic_ind ctx -> Univ.AUContext.instance ctx
-  | Cumulative_ind cumi -> 
-    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)
-
-let inductive_polymorphic_context mib =
-  match mib.mind_universes with
-  | Monomorphic_ind _ -> Univ.UContext.empty
-  | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx
-  | Cumulative_ind cumi -> 
-    Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
-
 (************************************************************************)
 
 (* Build the substitution that replaces Rels by the appropriate *)

checker/inductive.mli

@@ -26,10 +26,6 @@ val inductive_is_polymorphic : mutual_inductive_body -> bool
 
 val inductive_is_cumulative : mutual_inductive_body -> bool
 
-val inductive_polymorphic_instance : mutual_inductive_body -> Univ.universe_instance
-
-val inductive_polymorphic_context : mutual_inductive_body -> Univ.universe_context
-
 val type_of_inductive : env -> mind_specif puniverses -> constr
 
 (* Return type as quoted by the user *)

checker/reduction.ml

@@ -157,25 +157,23 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
   else raise NotConvertible
 
 let convert_inductive_instances cv_pb cumi u u' univs =
-  let ind_instance =
-      Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) in
+  let len_instance =
+      Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in
   let ind_subtypctx =  Univ.ACumulativityInfo.subtyp_context cumi in
-  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
-          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+  if not ((len_instance = Univ.Instance.length u) &&
+          (len_instance = Univ.Instance.length u')) then
     anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.UContext.constraints
-      (Univ.subst_instance_context comp_subst ind_subtypctx)
+      Univ.AUContext.instantiate comp_subst ind_subtypctx
     in
     let comp_cst =
       match cv_pb with
         CONV ->
         let comp_cst' =
           let comp_subst = (Univ.Instance.append u' u) in
-          Univ.UContext.constraints
-            (Univ.subst_instance_context comp_subst ind_subtypctx)
+          Univ.AUContext.instantiate comp_subst ind_subtypctx
         in
         Univ.Constraint.union comp_cst comp_cst'
       | CUMUL -> comp_cst

checker/subtyping.ml

@@ -81,6 +81,14 @@ let check_conv_error error f env a1 a2 =
   with
       NotConvertible -> error ()
 
+let check_polymorphic_instance error env auctx1 auctx2 =
+  if not (Univ.AUContext.size auctx1 == Univ.AUContext.size auctx2) then
+    error ()
+  else if not (Univ.check_subtype (Environ.universes env) auctx2 auctx1) then
+    error ()
+  else
+    Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
+
 (* for now we do not allow reorderings *)
 let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2= 
   let kn = MutInd.make2 mp1 l in
@@ -93,19 +101,17 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   in
   let mib2 = subst_mind subst2 mib2 in
   let check eq f = if not (eq (f mib1) (f mib2)) then error () in
-  let u =
-    let process inst inst' =
-      if Univ.Instance.equal inst inst' then inst else error ()
-    in
+  let env, u =
     match mib1.mind_universes, mib2.mind_universes with
-    | Monomorphic_ind _, Monomorphic_ind _ -> Univ.Instance.empty
+    | Monomorphic_ind _, Monomorphic_ind _ -> env, Univ.Instance.empty
     | Polymorphic_ind auctx, Polymorphic_ind auctx' ->
-      process
-        (Univ.AUContext.instance auctx) (Univ.AUContext.instance auctx')
+      let env = check_polymorphic_instance error env auctx auctx' in
+      env, Univ.make_abstract_instance auctx'
     | Cumulative_ind cumi, Cumulative_ind cumi' ->
-      process
-        (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
-        (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi'))
+      let auctx = Univ.ACumulativityInfo.univ_context cumi in
+      let auctx' = Univ.ACumulativityInfo.univ_context cumi' in
+      let env = check_polymorphic_instance error env auctx auctx' in
+      env, Univ.make_abstract_instance auctx'
     | _ -> error ()
   in
   let eq_projection_body p1 p2 =
@@ -118,7 +124,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     check (eq_constr) (fun x -> snd x.proj_eta);
     check (eq_constr) (fun x -> x.proj_body); true
   in
-  let check_inductive_type env t1 t2 =
+  let check_inductive_type t1 t2 =
 
     (* Due to template polymorphism, the conclusions of
        t1 and t2, if in Type, are generated as the least upper bounds
@@ -170,8 +176,8 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
       (* nparams done *)
       (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
-      check_inductive_type env
-        (type_of_inductive env ((mib1,p1),u)) (type_of_inductive env ((mib2,p2),u))
+      check_inductive_type
+        (type_of_inductive env ((mib1,p1), u)) (type_of_inductive env ((mib2,p2),u))
   in
   let check_cons_types i p1 p2 =
     Array.iter2 (check_conv conv env)
@@ -309,27 +315,17 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
 		let c2 = force_constr lc2 in
 		check_conv conv env c1 c2))
       | IndType ((kn,i),mind1) ->
-	  ignore (CErrors.user_err (Pp.str (
+        CErrors.user_err (Pp.str (
 		    "The kernel does not recognize yet that a parameter can be " ^
 		      "instantiated by an inductive type. Hint: you can rename the " ^
 		      "inductive type and give a definition to map the old name to the new " ^
-		      "name.")));
-      if constant_has_body cb2 then error () ;
-      let u = inductive_polymorphic_instance mind1 in
-      let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in
-      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
-       check_conv conv_leq env arity1 typ2
-   | IndConstr (((kn,i),j) as cstr,mind1) ->
-      ignore (CErrors.user_err (Pp.str (
+		      "name."))
+   | IndConstr (((kn,i),j),mind1) ->
+      CErrors.user_err (Pp.str (
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by a constructor. Hint: you can rename the " ^
        "constructor and give a definition to map the old name to the new " ^
-       "name.")));
-      if constant_has_body cb2 then error () ;
-      let u1 = inductive_polymorphic_instance mind1 in
-      let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
-      let ty2 = Typeops.type_of_constant_type env cb2.const_type in
-       check_conv conv env ty1 ty2
+       "name."))
 
 let rec check_modules  env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module None msb1 in

checker/univ.ml

@@ -1160,6 +1160,33 @@ struct
 
 end
 
+(** Substitute instance inst for ctx in csts *)
+
+let subst_instance_level s l =
+  match l.Level.data with
+  | Level.Var n -> s.(n) 
+  | _ -> l
+
+let subst_instance_instance s i = 
+  Array.smartmap (fun l -> subst_instance_level s l) i
+
+let subst_instance_universe s u =
+  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
+  let u' = Universe.smartmap f u in
+    if u == u' then u
+    else Universe.sort u'
+
+let subst_instance_constraint s (u,d,v as c) =
+  let u' = subst_instance_level s u in
+  let v' = subst_instance_level s v in
+    if u' == u && v' == v then c
+    else (u',d,v')
+
+let subst_instance_constraints s csts =
+  Constraint.fold 
+    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
+    csts Constraint.empty
+
 type universe_instance = Instance.t
 
 type 'a puniverses = 'a * Instance.t
@@ -1175,6 +1202,7 @@ struct
   let make x = x
   let instance (univs, cst) = univs
   let constraints (univs, cst) = cst
+  let size (univs, _) = Instance.length univs
 
   let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
   let pr prl (univs, cst as ctx) =
@@ -1184,7 +1212,18 @@ end
 
 type universe_context = UContext.t
 
-module AUContext = UContext
+module AUContext =
+struct
+  include UContext
+
+  let repr (inst, cst) =
+    (Array.mapi (fun i l -> Level.var i) inst, cst)
+
+  let instantiate inst (u, cst) =
+    assert (Array.length u = Array.length inst);
+    subst_instance_constraints inst cst
+
+end
 
 type abstract_universe_context = AUContext.t
 
@@ -1242,7 +1281,17 @@ struct
 end
 type universe_context_set = ContextSet.t
 
+(** Instance subtyping *)
 
+let check_subtype univs ctxT ctx =
+  if AUContext.size ctx == AUContext.size ctx then
+    let (inst, cst) = AUContext.repr ctx in
+    let cstT = UContext.constraints (AUContext.repr ctxT) in
+    let push accu v = add_universe v false accu in
+    let univs = Array.fold_left push univs inst in
+    let univs = merge_constraints cstT univs in
+    check_constraints cst univs
+  else false
 
 (** Substitutions. *)
 
@@ -1263,36 +1312,6 @@ let subst_univs_level_universe subst u =
     if u == u' then u
     else Universe.sort u'
 
-(** Substitute instance inst for ctx in csts *)
-
-let subst_instance_level s l =
-  match l.Level.data with
-  | Level.Var n -> s.(n) 
-  | _ -> l
-
-let subst_instance_instance s i = 
-  Array.smartmap (fun l -> subst_instance_level s l) i
-
-let subst_instance_universe s u =
-  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
-  let u' = Universe.smartmap f u in
-    if u == u' then u
-    else Universe.sort u'
-
-let subst_instance_constraint s (u,d,v as c) =
-  let u' = subst_instance_level s u in
-  let v' = subst_instance_level s v in
-    if u' == u && v' == v then c
-    else (u',d,v')
-
-let subst_instance_constraints s csts =
-  Constraint.fold 
-    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
-    csts Constraint.empty
-
-let subst_instance_context inst (inner_inst, inner_constr) =
-  (inner_inst, subst_instance_constraints inst inner_constr)
-
 let make_abstract_instance (ctx, _) = 
   Array.mapi (fun i l -> Level.var i) ctx
 

checker/univ.mli

@@ -209,6 +209,10 @@ sig
   type t
 
   val instance : t -> Instance.t
+  val size : t -> int
+
+  val instantiate : Instance.t -> t -> Constraint.t
+  val repr : t -> UContext.t
 
 end
 
@@ -276,7 +280,6 @@ val subst_univs_universe : universe_subst_fn -> universe -> universe
 (** Substitution of instances *)
 val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
 val subst_instance_universe : universe_instance -> universe -> universe
-val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context
 
 (* val make_instance_subst : universe_instance -> universe_level_subst *)
 (* val make_inverse_instance_subst : universe_instance -> universe_level_subst *)
@@ -287,7 +290,10 @@ val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_i
 
 (** Build the relative instance corresponding to the context *)
 val make_abstract_instance : abstract_universe_context -> universe_instance
-
+
+(** Check instance subtyping *)
+val check_subtype : universes -> AUContext.t -> AUContext.t -> bool
+
 (** {6 Pretty-printing of universes. } *)
 
 val pr_constraint_type : constraint_type -> Pp.std_ppcmds

engine/universes.ml

@@ -282,28 +282,27 @@ let new_Type dp = mkType (new_univ dp)
 let new_Type_sort dp = Type (new_univ dp)
 
 let fresh_universe_instance ctx =
-  Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ())) 
-    (AUContext.instance ctx)
+  let init _ = new_univ_level (Global.current_dirpath ()) in
+  Instance.of_array (Array.init (AUContext.size ctx) init)
 
 let fresh_instance_from_context ctx =
   let inst = fresh_universe_instance ctx in
-  let constraints = UContext.constraints (subst_instance_context inst ctx) in
+  let constraints = AUContext.instantiate inst ctx in
     inst, constraints
 
 let fresh_instance ctx =
   let ctx' = ref LSet.empty in
-  let inst = 
-    Instance.subst_fn (fun v -> 
-      let u = new_univ_level (Global.current_dirpath ()) in
-	ctx' := LSet.add u !ctx'; u) 
-      (AUContext.instance ctx)
+  let init _ =
+    let u = new_univ_level (Global.current_dirpath ()) in
+    ctx' := LSet.add u !ctx'; u
+  in
+  let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
   in !ctx', inst
 
 let existing_instance ctx inst = 
   let () = 
-    let a1 = Instance.to_array inst 
-    and a2 = Instance.to_array (AUContext.instance ctx) in
-    let len1 = Array.length a1 and len2 = Array.length a2 in 
+    let len1 = Array.length (Instance.to_array inst)
+    and len2 = AUContext.size ctx in
       if not (len1 == len2) then
 	CErrors.user_err ~hdr:"Universes"
 	  (str "Polymorphic constant expected " ++ int len2 ++ 
@@ -317,7 +316,7 @@ let fresh_instance_from ctx inst =
     | Some inst -> existing_instance ctx inst
     | None -> fresh_instance ctx 
   in
-  let constraints = UContext.constraints (subst_instance_context inst ctx) in
+  let constraints = AUContext.instantiate inst ctx in
     inst, (ctx', constraints)
 
 let unsafe_instance_from ctx =