Merge PR#613: Cumulativity for inductive types

9 files changed, 297 insertions, 28 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 1bd03491a7..c7b37aba5c 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -43,7 +43,7 @@ let section_segment_of_reference = function
   | ConstRef con -> Lib.section_segment_of_constant con
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
       Lib.section_segment_of_mutual_inductive kn
-  | _ -> [], Univ.LMap.empty, Univ.UContext.empty
+  | _ -> [], Univ.LMap.empty, Univ.AUContext.empty
 
 let discharge_rename_args = function
   | _, (ReqGlobal (c, names), _ as req) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3757ba7e6d..d84363089d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -350,6 +350,26 @@ let exact_ise_stack2 env evd f sk1 sk2 =
     ise_stack2 evd (List.rev sk1) (List.rev sk2)
   else UnifFailure (evd, (* Dummy *) NotSameHead)
 
+let check_leq_inductives evd cumi u u' =
+  let u = EConstr.EInstance.kind evd u in
+  let u' = EConstr.EInstance.kind evd u' in
+  let length_ind_instance = 
+    Univ.Instance.length
+      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+  in
+  let ind_sbcst =  Univ.ACumulativityInfo.subtyp_context cumi in
+  if not ((length_ind_instance = Univ.Instance.length u) &&
+          (length_ind_instance = Univ.Instance.length u')) then
+     anomaly (Pp.str "Invalid inductive subtyping encountered!")
+  else
+    begin
+     let comp_subst = (Univ.Instance.append u u') in
+     let comp_cst = 
+       Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst)
+     in
+     Evd.add_constraints evd comp_cst
+    end
+
 let rec evar_conv_x ts env evd pbty term1 term2 =
   let term1 = whd_head_evar evd term1 in
   let term2 = whd_head_evar evd term2 in
@@ -439,16 +459,102 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     else evar_eqappr_x ts env' evd CONV out2 out1
   in
   let rigids env evd sk term sk' term' =
-    let univs = EConstr.eq_constr_universes evd term term' in
-    match univs with
-    | Some univs ->
-       ise_and evd [(fun i ->
-         let cstrs = Universes.to_constraints (Evd.universes i) univs in
-           try Success (Evd.add_constraints i cstrs)
-           with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
-                  (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
-    | None ->
-      UnifFailure (evd,NotSameHead)
+    let check_strict () =
+      let univs = EConstr.eq_constr_universes evd term term' in
+      match univs with
+      | Some univs ->
+        begin
+          let cstrs = Universes.to_constraints (Evd.universes evd) univs in
+          try Success (Evd.add_constraints evd cstrs)
+          with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
+        end
+      | None ->
+        UnifFailure (evd, NotSameHead)
+    in
+    let first_try_strict_check cond u u' try_subtyping_constraints =
+      if cond then
+        let univs = EConstr.eq_constr_universes evd term term' in
+        match univs with
+        | Some univs ->
+          begin
+            let cstrs = Universes.to_constraints (Evd.universes evd) univs in
+            try Success (Evd.add_constraints evd cstrs)
+            with Univ.UniverseInconsistency p -> try_subtyping_constraints ()
+          end
+        | None ->
+          UnifFailure (evd, NotSameHead)
+      else
+        UnifFailure (evd, NotSameHead)
+    in
+    let compare_heads evd = 
+      match EConstr.kind evd term, EConstr.kind evd term' with
+      | Const (c, u), Const (c', u') ->
+        check_strict ()
+      | Ind (ind, u), Ind (ind', u') ->
+        let check_subtyping_constraints () =
+          let nparamsaplied = Stack.args_size sk in
+          let nparamsaplied' = Stack.args_size sk' in
+          begin
+            let mind = Environ.lookup_mind (fst ind) env in
+            match mind.Declarations.mind_universes with
+            | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+              UnifFailure (evd, NotSameHead)
+            | Declarations.Cumulative_ind cumi ->
+              begin
+                let num_param_arity =
+                  mind.Declarations.mind_nparams + 
+                  mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
+                in
+                if not (num_param_arity = nparamsaplied
+                        && num_param_arity = nparamsaplied') then
+                  UnifFailure (evd, NotSameHead)
+                else
+                  begin
+                    let evd' = check_leq_inductives evd cumi u u' in
+                    Success (check_leq_inductives evd' cumi u' u)
+                  end
+              end
+          end
+        in
+        first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints
+      | Construct (cons, u), Construct (cons', u') ->
+        let check_subtyping_constraints () =
+          let ind, ind' = fst cons, fst cons' in
+          let j, j' = snd cons, snd cons' in
+          let nparamsaplied = Stack.args_size sk in
+          let nparamsaplied' = Stack.args_size sk' in
+          let mind = Environ.lookup_mind (fst ind) env in
+          match mind.Declarations.mind_universes with
+          | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+            UnifFailure (evd, NotSameHead)
+          | Declarations.Cumulative_ind cumi ->
+            begin
+              let num_cnstr_args =
+                let nparamsctxt =
+                  mind.Declarations.mind_nparams + 
+                  mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
+                in
+                nparamsctxt + 
+                mind.Declarations.mind_packets.(snd ind).
+                  Declarations.mind_consnrealargs.(j - 1)
+              in
+              if not (num_cnstr_args = nparamsaplied 
+                      && num_cnstr_args = nparamsaplied') then
+                UnifFailure (evd, NotSameHead)
+              else
+                begin
+                  let evd' = check_leq_inductives evd cumi u u' in
+                  Success (check_leq_inductives evd' cumi u' u)
+                end
+            end
+        in
+        first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints
+      | _, _ -> anomaly (Pp.str "")
+    in
+    ise_and evd [(fun i ->
+                try compare_heads i
+                with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
+                 (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
   in
   let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM =
     let switch f a b = if on_left then f a b else f b a in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d8252ea9bb..2ae7c0f809 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -655,3 +655,93 @@ let control_only_guard env c =
     iter_constr_with_full_binders push_rel iter env c
   in
   iter env c
+
+(* inference of subtyping condition for inductive types *)
+
+let infer_inductive_subtyping_arity_constructor
+    (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity (params : Context.Rel.t) =
+  let numchecked = ref 0 in
+  let numparams = Context.Rel.nhyps params in
+  let update_contexts (env, evd, csts) csts' =
+    (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts')
+  in
+  let basic_check (env, evd, csts) tp =
+    let result =
+      if !numchecked >= numparams then
+        let csts' =
+          Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp)
+        in update_contexts (env, evd, csts) csts'
+      else
+        (env, evd, csts)
+    in
+    numchecked := !numchecked + 1; result
+  in
+  let infer_typ typ ctxs =
+   match typ with
+     | LocalAssum (_, typ') ->
+       begin
+         try
+           let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts)
+         with Reduction.NotConvertible -> 
+           anomaly ~label:"inference of record/inductive subtyping relation failed"
+             (Pp.str "Can't infer subtyping for record/inductive type")
+       end
+     | _ -> anomaly (Pp.str "")
+  in
+  let arcn' = Term.it_mkProd_or_LetIn arcn params in
+  let typs, codom = Reduction.dest_prod env arcn' in
+  let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in
+  if not is_arity then basic_check last_contexts codom else last_contexts
+
+let infer_inductive_subtyping env evd mind_ent =
+  let { Entries.mind_entry_params = params;
+        Entries.mind_entry_inds = entries;
+        Entries.mind_entry_universes = ground_univs;
+      } = mind_ent
+  in
+  let uinfind =
+    match ground_univs with
+    | Entries.Monomorphic_ind_entry _
+    | Entries.Polymorphic_ind_entry _ -> ground_univs
+    | Entries.Cumulative_ind_entry cumi -> 
+      begin
+        let uctx = Univ.CumulativityInfo.univ_context cumi in
+        let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in
+        let dosubst = subst_univs_level_constr sbsubst in
+        let instance_other = 
+          Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) 
+        in
+        let constraints_other = 
+          Univ.subst_univs_level_constraints
+            sbsubst (Univ.UContext.constraints uctx) 
+        in
+        let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
+        let env = Environ.push_context uctx env in
+        let env = Environ.push_context uctx_other env in
+        let evd = 
+          Evd.merge_universe_context
+            evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) 
+        in
+        let (_, _, subtyp_constraints) =
+          List.fold_left
+            (fun ctxs indentry ->
+               let _, params = Typeops.infer_local_decls env params in
+               let ctxs' = infer_inductive_subtyping_arity_constructor
+                   ctxs dosubst indentry.Entries.mind_entry_arity true params
+               in
+               List.fold_left
+                 (fun ctxs cons ->
+                    infer_inductive_subtyping_arity_constructor
+                      ctxs dosubst cons false params
+                 )
+                 ctxs' indentry.Entries.mind_entry_lc
+            ) (env, evd, Univ.Constraint.empty) entries
+        in 
+        Entries.Cumulative_ind_entry
+          (Univ.CumulativityInfo.make 
+             (Univ.CumulativityInfo.univ_context cumi,
+              Univ.UContext.make
+                (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi),
+                 subtyp_constraints)))
+      end
+  in {mind_ent with Entries.mind_entry_universes = uinfind;}
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index bdb6f996b9..811f47f39a 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -199,3 +199,12 @@ val type_of_inductive_knowing_conclusion :
 
 (********************)
 val control_only_guard : env -> types -> unit
+
+(* inference of subtyping condition for inductive types *)
+(* for debugging purposes only to be removed *)
+val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t ->
+(Term.constr -> Term.constr) ->
+Term.types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t
+
+val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry ->
+  Entries.mutual_inductive_entry
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index bc9e3a1f46..283a1dcd18 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -197,7 +197,7 @@ let warn_projection_no_head_constant =
 (* Intended to always succeed *)
 let compute_canonical_projections warn (con,ind) =
   let env = Global.env () in
-  let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in
+  let ctx = Environ.constant_context env con in
   let u = Univ.UContext.instance ctx in
   let v = (mkConstU (con,u)) in
   let ctx = Univ.ContextSet.of_context ctx in
@@ -298,8 +298,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 ctx = Environ.constant_context env sp in
-  let u = Univ.UContext.instance ctx in
+  let u = Environ.constant_instance 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/reductionops.ml b/pretyping/reductionops.ml
index c2a6483012..123c610166 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1313,8 +1313,8 @@ let pb_equal = function
   | Reduction.CUMUL -> Reduction.CONV
   | Reduction.CONV -> Reduction.CONV
 
-let report_anomaly _ =
-  let e = UserError (None, Pp.str "Conversion test raised an anomaly") in
+let report_anomaly e =
+  let e = UserError (None, Pp.(str "Conversion test raised an anomaly" ++ print e)) in
   let e = CErrors.push e in
   iraise e
 
@@ -1361,9 +1361,81 @@ let sigma_compare_instances ~flex i0 i1 sigma =
      | Univ.UniverseInconsistency _ ->
 	raise Reduction.NotConvertible
 
+let sigma_check_inductive_instances cv_pb uinfind u u' sigma =
+  let ind_instance = 
+    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context uinfind) 
+  in
+  let ind_sbctx =  Univ.ACumulativityInfo.subtyp_context uinfind  in
+  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
+          (Univ.Instance.length ind_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_sbctx)
+    in
+    let comp_cst =
+      match cv_pb with
+        Reduction.CONV -> 
+        let comp_subst = (Univ.Instance.append u' u) in
+        let comp_cst' = 
+          Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx)
+        in
+        Univ.Constraint.union comp_cst comp_cst'
+      | Reduction.CUMUL -> comp_cst
+    in
+    try Evd.add_constraints sigma comp_cst
+    with Evd.UniversesDiffer
+       | Univ.UniverseInconsistency _ ->
+      raise Reduction.NotConvertible
+
+let sigma_conv_inductives
+    cv_pb (mind, ind) u1 sv1 u2 sv2 sigma =
+  try sigma_compare_instances ~flex:false u1 u2 sigma with
+    Reduction.NotConvertible ->
+    match mind.Declarations.mind_universes with
+    | Declarations.Monomorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Polymorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Cumulative_ind cumi ->
+      let num_param_arity =
+        mind.Declarations.mind_nparams + 
+        mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+      in
+      if not (num_param_arity = sv1 && num_param_arity = sv2) then
+        raise Reduction.NotConvertible
+      else
+        sigma_check_inductive_instances cv_pb cumi u1 u2 sigma 
+
+let sigma_conv_constructors
+    (mind, ind, cns) u1 sv1 u2 sv2 sigma =
+  try sigma_compare_instances ~flex:false u1 u2 sigma with
+    Reduction.NotConvertible ->
+    match mind.Declarations.mind_universes with
+    | Declarations.Monomorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Polymorphic_ind _ ->
+      raise Reduction.NotConvertible
+    | Declarations.Cumulative_ind cumi ->
+      let num_cnstr_args =
+        let nparamsctxt =
+          mind.Declarations.mind_nparams + 
+          mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+        in
+        nparamsctxt + 
+        mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
+      in
+      if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+        raise Reduction.NotConvertible
+      else
+        sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma
+
 let sigma_univ_state = 
   { Reduction.compare = sigma_compare_sorts;
-    Reduction.compare_instances = sigma_compare_instances }
+    Reduction.compare_instances = sigma_compare_instances;
+    Reduction.conv_inductives = sigma_conv_inductives;
+    Reduction.conv_constructors = sigma_conv_constructors}
 
 let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     ?(ts=full_transparent_state) env sigma x y =
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index af4ea3ac53..a4da19de75 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -66,7 +66,6 @@ module Cst_stack : sig
   val pr : t -> Pp.std_ppcmds
 end
 
-
 module Stack : sig
   type 'a app_node
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d7b4842810..f883e647b5 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -111,20 +111,16 @@ 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"
 
-open Declarations
-
 let typeclass_univ_instance (cl,u') =
   let subst = 
     let u = 
       match cl.cl_impl with
       | ConstRef c -> 
         let cb = Global.lookup_constant c in
-	  if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
-	  else Univ.Instance.empty
+        Declareops.constant_polymorphic_instance cb
       | IndRef c ->
          let mib,oib = Global.lookup_inductive c in
-	  if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes
-	  else Univ.Instance.empty
+         Declareops.inductive_polymorphic_instance 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')
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b08666483e..9e151fea25 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -174,8 +174,7 @@ and nf_whd env sigma whd typ =
   | Vatom_stk(Aind ((mi,i) as ind), stk) ->
      let mib = Environ.lookup_mind mi env in
      let nb_univs =
-       if mib.mind_polymorphic then Univ.UContext.size mib.mind_universes
-       else 0
+       Univ.Instance.length (Declareops.inductive_polymorphic_instance mib)
      in
      let mk u =
        let pind = (ind, u) in (mkIndU pind, type_of_ind env pind)
@@ -204,8 +203,7 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk =
   | ConstKey cst ->
      let cbody = Environ.lookup_constant cst env in
      let nb_univs =
-       if cbody.const_polymorphic then Univ.UContext.size cbody.const_universes
-       else 0
+       Univ.Instance.length (Declareops.constant_polymorphic_instance cbody)
      in
      let mk u =
        let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst)