Merge PR #18996: Remove the tag branch information from case_info.

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

checker/values.ml

@@ -122,11 +122,9 @@ let v_binder_annot x = v_tuple "binder_annot" [|x;v_relevance|]
 
 let v_puniverses v = v_tuple "punivs" [|v;v_instance|]
 
-let v_boollist = List v_bool
-
 let v_caseinfo =
   let v_cstyle = v_enum "case_style" 5 in
-  let v_cprint = v_tuple "case_printing" [|v_boollist;Array v_boollist;v_cstyle|] in
+  let v_cprint = v_tuple "case_printing" [|v_cstyle|] in
   v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
 
 let v_cast = v_enum "cast_kind" 3

dev/ci/user-overlays/18996-ppedrot-case-info-rm-tags.sh

@@ -0,0 +1,3 @@
+overlay paramcoq https://github.com/ppedrot/paramcoq case-info-rm-tags 18996
+
+overlay elpi https://github.com/ppedrot/coq-elpi case-info-rm-tags 18996

kernel/constr.ml

@@ -39,9 +39,7 @@ type cast_kind = VMcast | NATIVEcast | DEFAULTcast
 (* This defines Cases annotations *)
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 type case_printing =
-  { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *)
-    cstr_tags : bool list array; (* whether each pattern var of each constructor is a let-in (true) or not (false) *)
-    style     : case_style }
+  { style     : case_style }
 
 (* INVARIANT:
  * - Array.length ci_cstr_ndecls = Array.length ci_cstr_nargs
@@ -1270,8 +1268,6 @@ struct
   type u = inductive -> inductive
   let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind }
   let pp_info_equal info1 info2 =
-    List.equal (==) info1.ind_tags info2.ind_tags &&
-    Array.equal (List.equal (==)) info1.cstr_tags info2.cstr_tags &&
     info1.style == info2.style
   let eq ci ci' =
     ci.ci_ind == ci'.ci_ind &&
@@ -1280,18 +1276,14 @@ struct
     Array.equal Int.equal ci.ci_cstr_nargs ci'.ci_cstr_nargs && (* we use [Array.equal] on purpose *)
     pp_info_equal ci.ci_pp_info ci'.ci_pp_info  (* we use (=) on purpose *)
   open Hashset.Combine
-  let hash_bool b = if b then 0 else 1
-  let hash_bool_list = List.fold_left (fun n b -> combine n (hash_bool b))
   let hash_pp_info info =
     let h1 = match info.style with
     | LetStyle -> 0
     | IfStyle -> 1
     | LetPatternStyle -> 2
     | MatchStyle -> 3
     | RegularStyle -> 4 in
-    let h2 = hash_bool_list 0 info.ind_tags in
-    let h3 = Array.fold_left hash_bool_list 0 info.cstr_tags in
-    combine3 h1 h2 h3
+    h1
   let hash ci =
     let h1 = Ind.CanOrd.hash ci.ci_ind in
     let h2 = Int.hash ci.ci_npar in

kernel/constr.mli

@@ -25,9 +25,7 @@ type metavariable = int
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle
   | RegularStyle (** infer printing form from number of constructor *)
 type case_printing =
-  { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *)
-    cstr_tags : bool list array; (** tell whether letin or lambda in the signature of each constructor *)
-    style     : case_style }
+  { style     : case_style }
 
 (* INVARIANT:
  * - Array.length ci_cstr_ndecls = Array.length ci_cstr_nargs

plugins/extraction/extraction.ml

@@ -282,7 +282,7 @@ let fake_match_projection env p =
     let rctx, _ = decompose_prod_decls (Vars.substl subst cty) in
     List.chop mip.mind_consnrealdecls.(0) rctx
   in
-  let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
+  let ci_pp_info = { style = LetStyle } in
   let ci = {
     ci_ind = ind;
     ci_npar = mib.mind_nparams;

pretyping/detyping.ml

@@ -570,10 +570,9 @@ let rec build_tree na isgoal e sigma (ci, u, pms, cl) =
   let mkpat n rhs pl =
     let na = update_name sigma na rhs in
     na, DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,na) in
-  let cnl = ci.ci_pp_info.cstr_tags in
   List.flatten
     (List.init (Array.length cl)
-      (fun i -> contract_branch isgoal e sigma (cnl.(i),mkpat i,cl.(i))))
+      (fun i -> contract_branch isgoal e sigma (mkpat i,cl.(i))))
 
 and align_tree nal isgoal (e,c as rhs) sigma = match nal with
   | [] -> [Id.Set.empty,[],rhs]
@@ -596,7 +595,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
         let mat = align_tree nal isgoal rhs sigma in
         List.map (fun (ids,hd,rest) -> Nameops.Name.fold_right Id.Set.add na ids,pat::hd,rest) mat
 
-and contract_branch isgoal e sigma (cdn,mkpat,rhs) =
+and contract_branch isgoal e sigma (mkpat,rhs) =
   let nal,rhs = decomp_branch isgoal e sigma rhs in
   let mat = align_tree nal isgoal rhs sigma in
   List.map (fun (ids,hd,rhs) ->
@@ -643,6 +642,23 @@ let it_destRLambda_or_LetIn_names l c =
               | _ -> DAst.make @@ GApp (c,[a]))
   in aux l [] c
 
+let get_ind_tag env ind p =
+  if Environ.mem_mind (fst ind) env then
+    let (mib, mip) = Inductive.lookup_mind_specif env ind in
+    Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt)
+  else
+    let (nas, _), _ = p in
+    Array.map_to_list (fun _ -> false) nas
+
+let get_cstr_tags env ind bl =
+  if Environ.mem_mind (fst ind) env then
+    let (mib, mip) = Inductive.lookup_mind_specif env ind in
+    Array.map2 (fun (d, _) n -> Context.Rel.to_tags (List.firstn n d))
+      mip.mind_nf_lc mip.mind_consnrealdecls
+  else
+    let map (nas, _) = Array.map_to_list (fun _ -> false) nas in
+    Array.map map bl
+
 let detype_case computable detype detype_eqns avoid env sigma (ci, univs, params, p, iv, c, bl) =
   let synth_type = synthetize_type () in
   let tomatch = detype c in
@@ -667,10 +683,11 @@ let detype_case computable detype detype_eqns avoid env sigma (ci, univs, params
     then
       Anonymous, None, None
     else
+      let ind_tags = get_ind_tag (snd env) ci.ci_ind p in
       let (ctx, p) = RobustExpand.return_clause (snd env) sigma ci.ci_ind univs params p in
       let p = EConstr.it_mkLambda_or_LetIn p ctx in
       let p = detype p in
-      let nl,typ = it_destRLambda_or_LetIn_names ci.ci_pp_info.ind_tags p in
+      let nl,typ = it_destRLambda_or_LetIn_names ind_tags p in
       let n,typ = match DAst.get typ with
         | GLambda (x,_,_,t,c) -> x, c
         | _ -> Anonymous, typ in
@@ -694,13 +711,26 @@ let detype_case computable detype detype_eqns avoid env sigma (ci, univs, params
         st
     with Not_found -> st
   in
-  let constagsl = ci.ci_pp_info.cstr_tags in
   match tag, aliastyp with
   | LetStyle, None ->
+    if Coqlib.check_ref "core.detyping.unknown_inductive" (GlobRef.IndRef ci.ci_ind) then
+      (* This is a hack used by coq-elpi to implement destructuring let-bindings
+         on an unknown inductive type. *)
+      let () = assert (Int.equal (Array.length bl) 1) in
+      let _, b = bl.(0) in
+      let b' = detype b in
+      let rec decompose accu c = match DAst.get c with
+      | GLambda (na, _, _, _, c) -> decompose (na :: accu) c
+      | _ -> List.rev accu, c
+      in
+      let (nal, d) = decompose [] b' in
+      GLetTuple (nal,(alias,pred),tomatch,d)
+    else
       let map i br =
         let (ctx, body) = RobustExpand.branch (snd env) sigma (ci.ci_ind, i + 1) univs params br in
         EConstr.it_mkLambda_or_LetIn body ctx
       in
+      let constagsl = get_cstr_tags (snd env) ci.ci_ind bl in
       let bl = Array.mapi map bl in
       let bl' = Array.map detype bl in
       let (nal,d) = it_destRLambda_or_LetIn_names constagsl.(0) bl'.(0) in
@@ -711,15 +741,16 @@ let detype_case computable detype detype_eqns avoid env sigma (ci, univs, params
           let ctx, body = RobustExpand.branch (snd env) sigma (ci.ci_ind, i + 1) univs params br in
           EConstr.it_mkLambda_or_LetIn body ctx
         in
+        let constagsl = get_cstr_tags (snd env) ci.ci_ind bl in
         let bl = Array.mapi map bl in
         let bl' = Array.map detype bl in
         let nondepbrs = Array.map2 extract_nondep_branches bl' constagsl in
         GIf (tomatch,(alias,pred), nondepbrs.(0), nondepbrs.(1))
       else
-        let eqnl = detype_eqns constructs constagsl (ci, univs, params, bl) in
+        let eqnl = detype_eqns constructs (ci, univs, params, bl) in
         GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
   | _ ->
-      let eqnl = detype_eqns constructs constagsl (ci, univs, params, bl) in
+      let eqnl = detype_eqns constructs (ci, univs, params, bl) in
       GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
 let rec share_names detype flags n l avoid env sigma c t =
@@ -992,7 +1023,7 @@ and detype_r d flags avoid env sigma t =
       let u = detype_instance sigma u in
       GArray(u, t, def, ty)
 
-and detype_eqns d flags avoid env sigma computable constructs consnargsl bl =
+and detype_eqns d flags avoid env sigma computable constructs bl =
   try
     if !Flags.raw_print || not (reverse_matching ()) then raise_notrace Exit;
     let mat = build_tree Anonymous flags (avoid,env) sigma bl in
@@ -1002,9 +1033,9 @@ and detype_eqns d flags avoid env sigma computable constructs consnargsl bl =
   with e when CErrors.noncritical e ->
     let (ci, u, pms, bl) = bl in
     Array.to_list
-      (Array.map3 (detype_eqn d flags avoid env sigma u pms) constructs consnargsl bl)
+      (Array.map2 (detype_eqn d flags avoid env sigma u pms) constructs bl)
 
-and detype_eqn d flags avoid env sigma u pms constr construct_nargs br =
+and detype_eqn d flags avoid env sigma u pms constr br =
   let ctx, body = RobustExpand.branch (snd env) sigma constr u pms br in
   let branch = EConstr.it_mkLambda_or_LetIn body ctx in
   let make_pat decl avoid env b ids =

pretyping/inductiveops.ml

@@ -329,13 +329,7 @@ let has_dependent_elim (mib,mip) =
 (* Annotation for cases *)
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let ind_tags =
-    Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in
-  let cstr_tags =
-    Array.map2 (fun (d, _) n ->
-      Context.Rel.to_tags (List.firstn n d))
-      mip.mind_nf_lc mip.mind_consnrealdecls in
-  let print_info = { Constr.ind_tags; cstr_tags; style } in
+  let print_info = { Constr.style } in
   { Constr.ci_ind     = ind;
     ci_npar    = mib.mind_nparams;
     ci_cstr_ndecls = mip.mind_consnrealdecls;