Use specialized function for inductive subtyping inference.

This ensures by construction that we never infer constraints outside
the variance model.

1 files changed, 0 insertions, 123 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 23a4ade3f..275a079d5 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -656,126 +656,3 @@ 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, csts) (subst : constr -> constr) (arcn : types) is_arity (params : Context.Rel.t) =
-  let numchecked = ref 0 in
-  let numparams = Context.Rel.nhyps params in
-  let update_contexts (env, csts) csts' =
-    (Environ.add_constraints csts' env, Univ.Constraint.union csts csts')
-  in
-  let basic_check (env, csts) tp =
-    let result =
-      if !numchecked >= numparams then
-        let csts' =
-          Reduction.infer_conv_leq env (Environ.universes env) tp (subst tp)
-        in update_contexts (env, csts) csts'
-      else
-        (env, csts)
-    in
-    numchecked := !numchecked + 1; result
-  in
-  let infer_typ typ ctxs =
-   match typ with
-     | LocalAssum (_, typ') ->
-       begin
-         try
-           let (env, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, 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, csts) in
-  if not is_arity then basic_check last_contexts codom else last_contexts
-
-type ukind =
-  Global | Orig of int | New of int
-
-let make_variance uctx lmap csts =
-  let variance = Array.init (UContext.size uctx) (fun _ -> Variance.Irrelevant) in
-  let geti = Array.fold_left_i (fun i geti u -> LMap.add u i geti)
-      LMap.empty (Instance.to_array @@ UContext.instance uctx)
-  in
-  let lmap_rev = LMap.fold (fun u v lmap_rev -> LMap.add v u lmap_rev) lmap LMap.empty in
-  let analyse_univ u =
-    match LMap.find u lmap_rev with
-    | exception Not_found ->
-      begin match LMap.find u lmap with
-        | exception Not_found -> Global
-        | _ -> Orig (LMap.find u geti)
-      end
-    | uorig -> New (LMap.find uorig geti)
-  in
-  Constraint.iter (fun (l,d,r) ->
-      match analyse_univ l, analyse_univ r with
-      | Orig i, New j when Int.equal i j ->
-        begin match d with
-          | Lt -> anomaly ~label:"make_variance" Pp.(str "unexpected orig < new constraint")
-          | Eq -> variance.(i) <- Variance.sup variance.(i) Variance.Invariant
-          | Le -> variance.(i) <- Variance.sup variance.(i) Variance.Covariant
-        end
-      | New i, Orig j when Int.equal i j ->
-        begin match d with
-          | Lt -> anomaly ~label:"make_variance" Pp.(str "unexpected orig > new constraint")
-          | Eq -> variance.(i) <- Variance.sup variance.(i) Variance.Invariant
-          | Le -> anomaly ~label:"make_variance" Pp.(str "unexpected orig >= new constraint")
-        end
-      | (Global | Orig _ | New _), _ ->
-        anomaly ~label:"make_variance" Pp.(str "unexpected constraint between non copy universes")
-    ) csts;
-  variance
-
-let infer_inductive_subtyping env 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 = CumulativityInfo.univ_context cumi in
-        let env = Environ.push_context uctx env in
-        let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in
-        let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
-            LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
-        in
-        let dosubst = subst_univs_level_constr lmap in
-        let instance_other = Instance.of_array new_levels in
-        let constraints_other = 
-          Univ.subst_univs_level_constraints
-            lmap (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 (_, 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, Univ.Constraint.empty) entries
-        in
-        let variance = make_variance uctx lmap subtyp_constraints in
-        Entries.Cumulative_ind_entry
-          (Univ.CumulativityInfo.make 
-             (uctx, variance))
-      end
-  in {mind_ent with Entries.mind_entry_universes = uinfind;}