Remove redundant univ and parameter info from CaseInvert

6 files changed, 67 insertions, 81 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 5613bf645e..a32c8f1cd1 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -357,7 +357,7 @@ and fterm =
   | FCLOS of constr * fconstr subs
   | FLOCKED
 
-and finvert = Univ.Instance.t * fconstr array
+and finvert = fconstr array
 
 let fterm_of v = v.term
 let set_ntrl v = v.mark <- Mark.set_ntrl v.mark
@@ -582,8 +582,8 @@ let rec to_constr lfts v =
     | FConstruct op -> mkConstructU op
     | FCaseT (ci, u, pms, p, c, ve, env) ->
       to_constr_case lfts ci u pms p NoInvert c ve env
-    | FCaseInvert (ci, u, pms, p, (univs, args), c, ve, env) ->
-      let iv = CaseInvert {univs;args=Array.map (to_constr lfts) args} in
+    | FCaseInvert (ci, u, pms, p, indices, c, ve, env) ->
+      let iv = CaseInvert {indices=Array.map (to_constr lfts) indices} in
       to_constr_case lfts ci u pms p iv c ve env
     | FFix ((op,(lna,tys,bds)) as fx, e) ->
       if is_subs_id e && is_lift_id lfts then
@@ -1370,8 +1370,8 @@ and knht info e t stk =
         knht info e a (append_stack (mk_clos_vect e b) stk)
     | Case(ci,u,pms,p,NoInvert,t,br) ->
         knht info e t (ZcaseT(ci, u, pms, p, br, e)::stk)
-    | Case(ci,u,pms,p,CaseInvert{univs;args},t,br) ->
-      let term = FCaseInvert (ci, u, pms, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in
+    | Case(ci,u,pms,p,CaseInvert{indices},t,br) ->
+      let term = FCaseInvert (ci, u, pms, p, (Array.map (mk_clos e) indices), mk_clos e t, br, e) in
       { mark = mark Red Unknown; term }, stk
     | Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk
     | Cast(a,_,_) -> knht info e a stk
@@ -1478,8 +1478,9 @@ let rec knr info tab m stk =
            kni info tab a (Zprimitive(op,c,rargs,nargs)::s)
              end
      | (_, _, s) -> (m, s))
-  | FCaseInvert (ci, _u, _pms, _p,iv,_c,v,env) when red_set info.i_flags fMATCH ->
-    begin match case_inversion info tab ci iv v with
+  | FCaseInvert (ci, u, pms, _p,iv,_c,v,env) when red_set info.i_flags fMATCH ->
+    let pms = mk_clos_vect env pms in
+    begin match case_inversion info tab ci u pms iv v with
       | Some c -> knit info tab env c stk
       | None -> (m, stk)
     end
@@ -1496,18 +1497,17 @@ and knit info tab e t stk =
   let (ht,s) = knht info e t stk in
   knr info tab ht s
 
-and case_inversion info tab ci (univs,args) v =
+and case_inversion info tab ci u params indices v =
   let open Declarations in
   (* No binders / lets at all in the unique branch *)
   let v = match v with
   | [| [||], v |] -> v
   | _ -> assert false
   in
-  if Array.is_empty args then Some v
+  if Array.is_empty indices then Some v
   else
     let env = info_env info in
     let ind = ci.ci_ind in
-    let params, indices = Array.chop ci.ci_npar args in
     let psubst = subs_consn params 0 ci.ci_npar (subs_id 0) in
     let mib = Environ.lookup_mind (fst ind) env in
     let mip = mib.mind_packets.(snd ind) in
@@ -1516,7 +1516,7 @@ and case_inversion info tab ci (univs,args) v =
     let _ind, expect_args = destApp expect in
     let check_index i index =
       let expected = expect_args.(ci.ci_npar + i) in
-      let expected = Vars.subst_instance_constr univs expected in
+      let expected = Vars.subst_instance_constr u expected in
       let expected = mk_clos psubst expected in
       !conv {info with i_flags=all} tab expected index
     in
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 0dc72025af..30542597c5 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -83,15 +83,15 @@ type pconstant = Constant.t puniverses
 type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
-type ('constr, 'univs) pcase_invert =
+type 'constr pcase_invert =
   | NoInvert
-  | CaseInvert of { univs : 'univs; args : 'constr array }
+  | CaseInvert of { indices : 'constr array }
 
 type 'constr pcase_branch = Name.t Context.binder_annot array * 'constr
 type 'types pcase_return = Name.t Context.binder_annot array * 'types
 
 type ('constr, 'types, 'univs) pcase =
-  case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array
+  case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array
 
 (* [Var] is used for named variables and [Rel] for variables as
    de Bruijn indices. *)
@@ -109,7 +109,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Const     of (Constant.t * 'univs)
   | Ind       of (inductive * 'univs)
   | Construct of (constructor * 'univs)
-  | Case      of case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array
+  | Case      of case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
   | Proj      of Projection.t * 'constr
@@ -125,7 +125,7 @@ type existential = existential_key * constr list
 
 type types = constr
 
-type case_invert = (constr, Instance.t) pcase_invert
+type case_invert = constr pcase_invert
 type case_return = types pcase_return
 type case_branch = constr pcase_branch
 type case = (constr, types, Instance.t) pcase
@@ -481,8 +481,8 @@ let decompose_appvect c =
 
 let fold_invert f acc = function
   | NoInvert -> acc
-  | CaseInvert {univs=_;args} ->
-    Array.fold_left f acc args
+  | CaseInvert {indices} ->
+    Array.fold_left f acc indices
 
 let fold f acc c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -509,8 +509,8 @@ let fold f acc c = match kind c with
 
 let iter_invert f = function
   | NoInvert -> ()
-  | CaseInvert {univs=_; args;} ->
-    Array.iter f args
+  | CaseInvert {indices;} ->
+    Array.iter f indices
 
 let iter f c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -624,10 +624,10 @@ let map_return_predicate_with_binders g f l p =
 
 let map_invert f = function
   | NoInvert -> NoInvert
-  | CaseInvert {univs;args;} as orig ->
-    let args' = Array.Smart.map f args in
-    if args == args' then orig
-    else CaseInvert {univs;args=args';}
+  | CaseInvert {indices;} as orig ->
+    let indices' = Array.Smart.map f indices in
+    if indices == indices' then orig
+    else CaseInvert {indices=indices';}
 
 let map f c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -695,10 +695,10 @@ let map f c = match kind c with
 
 let fold_map_invert f acc = function
   | NoInvert -> acc, NoInvert
-  | CaseInvert {univs;args;} as orig ->
-    let acc, args' = Array.fold_left_map f acc args in
-    if args==args' then acc, orig
-    else acc, CaseInvert {univs;args=args';}
+  | CaseInvert {indices;} as orig ->
+    let acc, indices' = Array.fold_left_map f acc indices in
+    if indices==indices' then acc, orig
+    else acc, CaseInvert {indices=indices';}
 
 let fold_map_under_context f accu d =
   let (nas, p) = d in
@@ -881,13 +881,12 @@ type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool
    optimisation that physically equal arrays are equals (hence the
    calls to {!Array.equal_norefl}). *)
 
-let eq_invert eq leq_universes iv1 iv2 =
+let eq_invert eq iv1 iv2 =
   match iv1, iv2 with
   | NoInvert, NoInvert -> true
   | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false
-  | CaseInvert {univs;args}, CaseInvert iv2 ->
-    leq_universes univs iv2.univs
-    && Array.equal eq args iv2.args
+  | CaseInvert {indices}, CaseInvert iv2 ->
+    Array.equal eq indices iv2.indices
 
 let eq_under_context eq (_nas1, p1) (_nas2, p2) =
   eq p1 p2
@@ -921,7 +920,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
     (** FIXME: what are we doing with u1 = u2 ? *)
     Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind && leq_universes (Some (GlobRef.IndRef ci1.ci_ind, 0)) u1 u2 &&
     Array.equal (eq 0) pms1 pms2 && eq_under_context (eq 0) p1 p2 &&
-    eq_invert (eq 0) (leq_universes None) iv1 iv2 &&
+    eq_invert (eq 0) iv1 iv2 &&
     eq 0 c1 c2 && Array.equal (eq_under_context (eq 0)) bl1 bl2
   | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
     Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
@@ -1060,8 +1059,7 @@ let compare_invert f iv1 iv2 =
   | NoInvert, CaseInvert _ -> -1
   | CaseInvert _, NoInvert -> 1
   | CaseInvert iv1, CaseInvert iv2 ->
-    (* univs ignored deliberately *)
-    Array.compare f iv1.args iv2.args
+    Array.compare f iv1.indices iv2.indices
 
 let constr_ord_int f t1 t2 =
   let (=?) f g i1 i2 j1 j2=
@@ -1190,9 +1188,8 @@ let invert_eqeq iv1 iv2 =
   match iv1, iv2 with
   | NoInvert, NoInvert -> true
   | NoInvert, CaseInvert _ | CaseInvert _, NoInvert -> false
-  | CaseInvert iv1, CaseInvert iv2 ->
-    iv1.univs == iv2.univs
-    && iv1.args == iv2.args
+  | CaseInvert {indices=i1}, CaseInvert {indices=i2} ->
+    i1 == i2
 
 let hasheq_ctx (nas1, c1) (nas2, c2) =
   array_eqeq nas1 nas2 && c1 == c2
@@ -1368,10 +1365,9 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
 
   and sh_invert = function
     | NoInvert -> NoInvert, 0
-    | CaseInvert {univs;args;} ->
-      let univs, hu = sh_instance univs in
-      let args, ha = hash_term_array args in
-      CaseInvert {univs;args;}, combinesmall 1 (combine hu ha)
+    | CaseInvert {indices;} ->
+      let indices, ha = hash_term_array indices in
+      CaseInvert {indices;}, combinesmall 1 ha
 
   and sh_rec t =
     let (y, h) = hash_term t in
@@ -1451,8 +1447,8 @@ let rec hash t =
 
 and hash_invert = function
   | NoInvert -> 0
-  | CaseInvert {univs;args;} ->
-    combinesmall 1 (combine (Instance.hash univs) (hash_term_array args))
+  | CaseInvert {indices;} ->
+    combinesmall 1 (hash_term_array indices)
 
 and hash_term_array t =
   Array.fold_left (fun acc t -> combine acc (hash t)) 0 t
@@ -1617,6 +1613,6 @@ let rec debug_print c =
 
 and debug_invert = let open Pp in function
   | NoInvert -> mt()
-  | CaseInvert {univs;args;} ->
-    spc() ++ str"Invert {univs=" ++ Instance.pr Level.pr univs ++
-    str "; args=" ++ prlist_with_sep spc debug_print (Array.to_list args) ++ str "} "
+  | CaseInvert {indices;} ->
+    spc() ++ str"Invert {indices=" ++
+    prlist_with_sep spc debug_print (Array.to_list indices) ++ str "} "
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 17c7da1cf6..57dd850ee7 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -49,11 +49,11 @@ type case_info =
     ci_pp_info    : case_printing   (* not interpreted by the kernel *)
   }
 
-type ('constr, 'univs) pcase_invert =
+type 'constr pcase_invert =
   | NoInvert
   (** Normal reduction: match when the scrutinee is a constructor. *)
 
-  | CaseInvert of { univs : 'univs; args : 'constr array; }
+  | CaseInvert of { indices : 'constr array; }
   (** Reduce when the indices match those of the unique constructor.
       (SProp to non SProp only) *)
 
@@ -168,9 +168,9 @@ type 'types pcase_return = Name.t Context.binder_annot array * 'types
 (** Names of the branches *)
 
 type ('constr, 'types, 'univs) pcase =
-  case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array
+  case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array
 
-type case_invert = (constr, Univ.Instance.t) pcase_invert
+type case_invert = constr pcase_invert
 type case_return = types pcase_return
 type case_branch = constr pcase_branch
 type case = (constr, types, Univ.Instance.t) pcase
@@ -259,7 +259,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
 
   | Ind       of (inductive * 'univs)                 (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
   | Construct of (constructor * 'univs)              (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
-  | Case      of case_info * 'univs * 'constr array * 'types pcase_return * ('constr,'univs) pcase_invert * 'constr * 'constr pcase_branch array
+  | Case      of case_info * 'univs * 'constr array * 'types pcase_return * 'constr pcase_invert * 'constr * 'constr pcase_branch array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
   | Proj      of Projection.t * 'constr
@@ -487,7 +487,7 @@ val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -
 
 val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
 
-val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) pcase_invert -> 'a
+val fold_invert : ('a -> 'b -> 'a) -> 'a -> 'b pcase_invert -> 'a
 
 (** [map f c] maps [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
@@ -495,14 +495,14 @@ val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) pcase_invert -> 'a
 
 val map : (constr -> constr) -> constr -> constr
 
-val map_invert : ('a -> 'a) -> ('a, 'b) pcase_invert -> ('a, 'b) pcase_invert
+val map_invert : ('a -> 'a) -> 'a pcase_invert -> 'a pcase_invert
 
 (** Like {!map}, but also has an additional accumulator. *)
 
 val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr
 
 val fold_map_invert : ('a -> 'b -> 'a * 'b) ->
-  'a -> ('b, 'c) pcase_invert -> 'a * ('b, 'c) pcase_invert
+  'a -> 'b pcase_invert -> 'a * 'b pcase_invert
 
 (** [map_with_binders g f n c] maps [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
@@ -519,7 +519,7 @@ val map_with_binders :
 
 val iter : (constr -> unit) -> constr -> unit
 
-val iter_invert : ('a -> unit) -> ('a, 'b) pcase_invert -> unit
+val iter_invert : ('a -> unit) -> 'a pcase_invert -> unit
 
 (** [iter_with_binders g f n c] iters [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
@@ -597,8 +597,8 @@ val compare_head_gen_leq : Univ.Instance.t instance_compare_fn ->
   constr constr_compare_fn ->
   constr constr_compare_fn
 
-val eq_invert : ('a -> 'a -> bool) -> ('b -> 'b -> bool)
-  -> ('a, 'b) pcase_invert -> ('a, 'b) pcase_invert -> bool
+val eq_invert : ('a -> 'a -> bool)
+  -> 'a pcase_invert -> 'a pcase_invert -> bool
 
 (** {6 Hashconsing} *)
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 930efa5d36..f82b754c59 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -88,13 +88,6 @@ let expmod_constr cache modlist c =
           let u = Instance.append u' u in
           let pms = Array.append prefix pms in
           let ci = { ci with ci_npar = ci.ci_npar + Array.length prefix } in
-          let iv = match iv with
-            | NoInvert -> NoInvert
-            | CaseInvert {univs; args;} ->
-              let univs = Instance.append u' univs in
-              let args = Array.append prefix args in
-              CaseInvert {univs; args;}
-          in
           Constr.map substrec (mkCase (ci,u,pms,p,iv,t,br))
         | exception Not_found ->
           Constr.map substrec c
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 83e41a63ec..741491c917 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -554,12 +554,14 @@ let rec execute env cstr =
         let c', ct = execute env c in
         let iv' = match iv with
           | NoInvert -> NoInvert
-          | CaseInvert {univs;args} ->
-            let ct' = mkApp (mkIndU (ci.ci_ind,univs), args) in
+          | CaseInvert {indices} ->
+            let args = Array.append pms indices in
+            let ct' = mkApp (mkIndU (ci.ci_ind,u), args) in
             let (ct', _) : constr * Sorts.t = execute_is_type env ct' in
             let () = conv_leq false env ct ct' in
             let _, args' = decompose_appvect ct' in
-            if args == args' then iv else CaseInvert {univs;args=args'}
+            if args == args' then iv
+            else CaseInvert {indices=Array.sub args' (Array.length pms) (Array.length indices)}
         in
         let p', pt = execute env p in
         let lf', lft = execute_array env lf in
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 0f71057787..b09577d4db 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -253,13 +253,12 @@ let subst_univs_level_constr subst c =
            if u' == u then t else
              (changed := true; mkSort (Sorts.sort_of_univ u'))
 
-      | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) ->
-        if Univ.Instance.is_empty u && Univ.Instance.is_empty univs then Constr.map aux t
+      | Case (ci, u, pms, p, CaseInvert {indices}, c, br) ->
+        if Univ.Instance.is_empty u then Constr.map aux t
         else
           let u' = f u in
-          let univs' = f univs in
-          if u' == u && univs' == univs then Constr.map aux t
-          else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br)))
+          if u' == u then Constr.map aux t
+          else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {indices},c,br)))
 
       | Case (ci, u, pms, p, NoInvert, c, br) ->
         if Univ.Instance.is_empty u then Constr.map aux t
@@ -314,11 +313,10 @@ let subst_instance_constr subst c =
           if u' == u then t else
             (mkSort (Sorts.sort_of_univ u'))
 
-      | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) ->
+      | Case (ci, u, pms, p, CaseInvert {indices}, c, br) ->
         let u' = f u in
-        let univs' = f univs in
-        if u' == u && univs' == univs then Constr.map aux t
-        else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br))
+        if u' == u then Constr.map aux t
+        else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {indices},c,br))
 
       | Case (ci, u, pms, p, NoInvert, c, br) ->
         if Univ.Instance.is_empty u then Constr.map aux t
@@ -366,11 +364,8 @@ let universes_of_constr c =
     | Array (u,_,_,_) ->
       let s = LSet.fold LSet.add (Instance.levels u) s in
       Constr.fold aux s c
-    | Case (_, u, _, _, CaseInvert {univs;args=_},_ ,_) ->
+    | Case (_, u, _, _, _,_ ,_) ->
       let s = LSet.fold LSet.add (Instance.levels u) s in
-      let s = LSet.fold LSet.add (Instance.levels univs) s in
       Constr.fold aux s c
-    | Case (_, u, _, _, NoInvert, _, _) ->
-      Constr.fold aux (LSet.fold LSet.add (Instance.levels u) s) c
     | _ -> Constr.fold aux s c
   in aux LSet.empty c