Merge PR#613: Cumulativity for inductive types

7 files changed, 138 insertions, 32 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 7d0edbc8b3..db3dbcbd92 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -158,7 +158,7 @@ let cache_constant ((sp,kn), obj) =
   assert (eq_constant kn' (constant_of_kn kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   let cst = Global.lookup_constant kn' in
-  add_section_constant cst.const_polymorphic kn' cst.const_hyps;
+  add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
   add_constant_kind (constant_of_kn kn) obj.cst_kind
 
@@ -325,7 +325,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   let kn' = Global.add_mind dir id mie in
   assert (eq_mind kn' (mind_of_kn kn));
   let mind = Global.lookup_mind kn' in
-  add_section_kn mind.mind_polymorphic kn' mind.mind_hyps;
+  add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
 
@@ -351,11 +351,27 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_record = None;
   mind_entry_finite = Decl_kinds.BiFinite;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
-  mind_entry_polymorphic = false;
-  mind_entry_universes = Univ.UContext.empty;
+  mind_entry_universes = Monomorphic_ind_entry Univ.UContext.empty;
   mind_entry_private = None;
 })
 
+(* reinfer subtyping constraints for inductive after section is dischared. *)
+let infer_inductive_subtyping (pth, mind_ent) =
+  match mind_ent.mind_entry_universes with
+  | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ ->
+    (pth, mind_ent)
+  | Cumulative_ind_entry cumi ->
+    begin
+      let env = Global.env () in
+      let env' =
+        Environ.push_context
+          (Univ.CumulativityInfo.univ_context cumi) env
+      in
+      (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
+      let evd = Evd.from_env env' in
+        (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent)
+    end
+
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
 
 let inInductive : inductive_obj -> obj =
@@ -365,7 +381,8 @@ let inInductive : inductive_obj -> obj =
     open_function = open_inductive;
     classify_function = (fun a -> Substitute (dummy_inductive_entry a));
     subst_function = ident_subst_function;
-    discharge_function = discharge_inductive }
+    discharge_function = discharge_inductive;
+    rebuild_function = infer_inductive_subtyping }
 
 let declare_projections mind =
   let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
diff --git a/library/global.ml b/library/global.ml
index 1ba86699d3..6d80012f47 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -176,19 +176,14 @@ let type_of_global_unsafe r =
        Vars.subst_instance_constr (Univ.UContext.instance univs) ty
   | IndRef ind ->
      let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-     let inst = 
-       if mib.Declarations.mind_polymorphic then 
-	 Univ.UContext.instance mib.Declarations.mind_universes
-       else Univ.Instance.empty
-     in
+     let inst = Declareops.inductive_polymorphic_instance mib in
        Inductive.type_of_inductive env (specif, inst)
   | ConstructRef cstr ->
      let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-     let inst = Univ.UContext.instance mib.Declarations.mind_universes in
-       Inductive.type_of_constructor (cstr,inst) specif
+     let inst = Declareops.inductive_polymorphic_instance mib in
+     Inductive.type_of_constructor (cstr,inst) specif
 
 let type_of_global_in_context env r = 
-  let open Declarations in
   match r with
   | VarRef id -> Environ.named_type id env, Univ.UContext.empty
   | ConstRef c -> 
@@ -199,21 +194,17 @@ let type_of_global_in_context env r =
        Typeops.type_of_constant_type env cb.Declarations.const_type, univs
   | IndRef ind ->
      let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-     let univs = 
-       if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes 
-       else Univ.UContext.empty
-     in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs
+     let univs = Declareops.inductive_polymorphic_context mib in
+     Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs
   | ConstructRef cstr ->
-     let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-     let univs = 
-       if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes 
-       else Univ.UContext.empty
-     in
-     let inst = Univ.UContext.instance univs in
-       Inductive.type_of_constructor (cstr,inst) specif, univs
+    let (mib,oib as specif) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr) 
+    in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    let inst = Univ.UContext.instance univs in
+    Inductive.type_of_constructor (cstr,inst) specif, univs
 
 let universes_of_global env r = 
-  let open Declarations in
     match r with
     | VarRef id -> Univ.UContext.empty
     | ConstRef c -> 
@@ -222,10 +213,11 @@ let universes_of_global env r =
           (Environ.opaque_tables env) cb
     | IndRef ind ->
       let (mib, oib) = Inductive.lookup_mind_specif env ind in
-	Univ.instantiate_univ_context mib.mind_universes 
+      Declareops.inductive_polymorphic_context mib
     | ConstructRef cstr ->
-      let (mib,oib) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-	Univ.instantiate_univ_context mib.mind_universes 
+      let (mib,oib) = 
+        Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+      Declareops.inductive_polymorphic_context mib
 
 let universes_of_global gr = 
   universes_of_global (env ()) gr
diff --git a/library/lib.ml b/library/lib.ml
index f22f53eadf..8127316d73 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -402,7 +402,7 @@ let find_opening_node id =
 type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
 
 type variable_context = variable_info list
-type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
+type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t
 		  
 type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
@@ -465,9 +465,9 @@ let add_section_replacement f g poly hyps =
     let () = check_same_poly poly vars in
     let sechyps,ctx = extract_hyps (vars,hyps) in
     let ctx = Univ.ContextSet.to_context ctx in
-    let subst, ctx = Univ.abstract_universes true ctx in
+    let subst, ctx = Univ.abstract_universes ctx in
     let args = instance_from_variable_context (List.rev sechyps) in
-    sectab := (vars,f (Univ.UContext.instance ctx,args) exps,
+    sectab := (vars,f (Univ.AUContext.instance ctx,args) exps,
 	      g (sechyps,subst,ctx) abs)::sl
 
 let add_section_kn poly kn =
diff --git a/library/lib.mli b/library/lib.mli
index f47d6e1a58..284d339801 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -157,7 +157,7 @@ val xml_close_section : (Names.Id.t -> unit) Hook.t
 (** {6 Section management for discharge } *)
 type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
 type variable_context = variable_info list 
-type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
+type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t
 
 val instance_from_variable_context : variable_context -> Names.Id.t array
 val named_of_variable_context : variable_context -> Context.Named.t
diff --git a/library/library.mllib b/library/library.mllib
index 6f433b77d1..d94fc22919 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -1,3 +1,4 @@
+Univops
 Nameops
 Libnames
 Globnames
diff --git a/library/univops.ml b/library/univops.ml
new file mode 100644
index 0000000000..60c12f0d81
--- /dev/null
+++ b/library/univops.ml
@@ -0,0 +1,79 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Term
+open Univ
+open Declarations
+
+let universes_of_constr c =
+  let rec aux s c = 
+    match kind_of_term c with
+    | Const (_, u) | Ind (_, u) | Construct (_, u) ->
+      LSet.fold LSet.add (Instance.levels u) s
+    | Sort u when not (Sorts.is_small u) -> 
+      let u = univ_of_sort u in
+      LSet.fold LSet.add (Universe.levels u) s
+    | _ -> fold_constr aux s c
+  in aux LSet.empty c
+
+let universes_of_inductive mind =
+  let process auctx =
+    let u = Univ.AUContext.instance auctx in
+    let univ_of_one_ind oind = 
+      let arity_univs =
+        Context.Rel.fold_outside
+          (fun decl unvs ->
+             Univ.LSet.union
+              (Context.Rel.Declaration.fold_constr
+                 (fun cnstr unvs ->
+                    let cnstr = Vars.subst_instance_constr u cnstr in
+                    Univ.LSet.union
+                      (universes_of_constr cnstr) unvs)
+              decl Univ.LSet.empty) unvs)
+        oind.mind_arity_ctxt ~init:Univ.LSet.empty
+      in
+      Array.fold_left (fun unvs cns ->
+          let cns = Vars.subst_instance_constr u cns in
+          Univ.LSet.union (universes_of_constr cns) unvs) arity_univs 
+       oind.mind_nf_lc
+    in
+    let univs = 
+      Array.fold_left
+        (fun unvs pk ->
+           Univ.LSet.union
+             (univ_of_one_ind pk) unvs
+        )
+        Univ.LSet.empty mind.mind_packets 
+    in
+    let mindcnt =  Univ.UContext.constraints (Univ.instantiate_univ_context auctx) in
+    let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in
+    univs
+  in
+  match mind.mind_universes with
+  | Monomorphic_ind _ -> LSet.empty
+  | Polymorphic_ind auctx -> process auctx
+  | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi)
+
+let restrict_universe_context (univs,csts) s =
+  (* Universes that are not necessary to typecheck the term.
+     E.g. univs introduced by tactics and not used in the proof term. *)
+  let diff = LSet.diff univs s in
+  let rec aux diff candid univs ness = 
+    let (diff', candid', univs', ness') = 
+      Constraint.fold
+	(fun (l, d, r as c) (diff, candid, univs, csts) ->
+	  if not (LSet.mem l diff) then
+	    (LSet.remove r diff, candid, univs, Constraint.add c csts)
+	  else if not (LSet.mem r diff) then
+	    (LSet.remove l diff, candid, univs, Constraint.add c csts)
+	  else (diff, Constraint.add c candid, univs, csts))
+	candid (diff, Constraint.empty, univs, ness)
+    in
+      if ness' == ness then (LSet.diff univs diff', ness)
+      else aux diff' candid' univs' ness'
+  in aux diff csts univs Constraint.empty
diff --git a/library/univops.mli b/library/univops.mli
new file mode 100644
index 0000000000..5b499c75bc
--- /dev/null
+++ b/library/univops.mli
@@ -0,0 +1,17 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Term
+open Univ
+open Declarations
+
+(** Shrink a universe context to a restricted set of variables *)
+
+val universes_of_constr : constr -> universe_set
+val universes_of_inductive : mutual_inductive_body -> universe_set
+val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set