Move relevance outside of case_info

Since sort poly made universe substitution affect it, it is IMO not
appropriate in the should-be-static case_info.

checker/values.ml

@@ -128,7 +128,7 @@ 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
-  v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_relevance;v_cprint|]
+  v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
 
 let v_cast = v_enum "cast_kind" 3
 
@@ -170,7 +170,7 @@ and v_case_invert = Sum ("case_inversion", 1, [|[|Array v_constr|]|])
 
 and v_case_branch = Tuple ("case_branch", [|Array (v_binder_annot v_name); v_constr|])
 
-and v_case_return = Tuple ("case_return", [|Array (v_binder_annot v_name); v_constr|])
+and v_case_return = Tuple ("case_return", [|Tuple ("case_return'", [|Array (v_binder_annot v_name); v_constr|]); v_relevance|])
 
 let v_rdecl = v_sum "rel_declaration" 0
     [| [|v_binder_annot v_name; v_constr|];               (* LocalAssum *)

dev/ci/user-overlays/18280-SkySkimmer-ci-relevance.sh

@@ -0,0 +1,23 @@
+overlay rewriter https://github.com/SkySkimmer/rewriter ci-relevance 18280
+
+overlay coqhammer https://github.com/SkySkimmer/coqhammer ci-relevance 18280
+
+overlay elpi https://github.com/SkySkimmer/coq-elpi ci-relevance 18280
+
+overlay equations https://github.com/SkySkimmer/Coq-Equations ci-relevance 18280
+
+overlay metacoq https://github.com/SkySkimmer/metacoq ci-relevance 18280
+
+overlay unicoq https://github.com/SkySkimmer/unicoq ci-relevance 18280
+
+overlay mtac2 https://github.com/SkySkimmer/Mtac2 ci-relevance 18280
+
+overlay paramcoq https://github.com/SkySkimmer/paramcoq ci-relevance 18280
+
+overlay serapi https://github.com/SkySkimmer/coq-serapi ci-relevance 18280
+
+overlay tactician https://github.com/SkySkimmer/coq-tactician ci-relevance 18280
+
+overlay waterproof https://github.com/SkySkimmer/coq-waterproof ci-relevance 18280
+
+overlay fiat_crypto https://github.com/SkySkimmer/fiat-crypto ci-relevance 18280

dev/top_printers.ml

@@ -348,7 +348,7 @@ let constr_display csr =
       "MutConstruct(("^(MutInd.to_string sp)^","^(string_of_int i)^"),"
       ^","^(universes_display u)^(string_of_int j)^")"
   | Proj (p, r, c) -> "Proj("^(Constant.to_string (Projection.constant p))^","^term_display c ^")"
-  | Case (ci,u,pms,(_,p),iv,c,bl) ->
+  | Case (ci,u,pms,((_,p),_),iv,c,bl) ->
       "MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
       ^(array_display (Array.map snd bl))^")"
   | Fix ((t,i),(lna,tl,bl)) ->
@@ -473,7 +473,7 @@ let print_pure_constr csr =
       print_int i; print_string ","; print_int j;
       print_string ","; universes_display u;
       print_string ")"
-  | Case (ci,u,pms,p,iv,c,bl) ->
+  | Case (ci,u,pms,(p,_),iv,c,bl) ->
       let pr_ctx (nas, c) =
         Array.iter (fun na -> print_cut (); name_display na) nas;
         print_string " |- ";

engine/eConstr.ml

@@ -437,15 +437,15 @@ let expand_case env _sigma (ci, u, pms, p, iv, c, bl) =
   let iv = unsafe_to_case_invert iv in
   let c = unsafe_to_constr c in
   let bl = unsafe_to_branches bl in
-  let (ci, p, iv, c, bl) = Inductive.expand_case env (ci, u, pms, p, iv, c, bl) in
+  let (ci, (p,r), iv, c, bl) = Inductive.expand_case env (ci, u, pms, p, iv, c, bl) in
   let p = of_constr p in
   let c = of_constr c in
   let iv = of_case_invert iv in
   let bl = of_constr_array bl in
-  (ci, p, iv, c, bl)
+  (ci, (p,r), iv, c, bl)
 
 let annotate_case env sigma (ci, u, pms, p, iv, c, bl as case) =
-  let (_, p, _, _, bl) = expand_case env sigma case in
+  let (_, (p,r), _, _, bl) = expand_case env sigma case in
   let p =
     (* Too bad we need to fetch this data in the environment, should be in the
       case_info instead. *)
@@ -454,7 +454,7 @@ let annotate_case env sigma (ci, u, pms, p, iv, c, bl as case) =
   in
   let mk_br c n = decompose_lambda_n_decls sigma n c in
   let bl = Array.map2 mk_br bl ci.ci_cstr_ndecls in
-  (ci, u, pms, p, iv, c, bl)
+  (ci, u, pms, (p,r), iv, c, bl)
 
 let expand_branch env _sigma u pms (ind, i) (nas, _br) =
   let open Declarations in
@@ -469,12 +469,12 @@ let expand_branch env _sigma u pms (ind, i) (nas, _br) =
   let ans : rel_context = match Evd.MiniEConstr.unsafe_eq with Refl -> ans in
   ans
 
-let contract_case env _sigma (ci, p, iv, c, bl) =
+let contract_case env _sigma (ci, (p,r), iv, c, bl) =
   let p = unsafe_to_constr p in
   let iv = unsafe_to_case_invert iv in
   let c = unsafe_to_constr c in
   let bl = unsafe_to_constr_array bl in
-  let (ci, u, pms, p, iv, c, bl) = Inductive.contract_case env (ci, p, iv, c, bl) in
+  let (ci, u, pms, p, iv, c, bl) = Inductive.contract_case env (ci, (p,r), iv, c, bl) in
   let u = EInstance.make u in
   let pms = of_constr_array pms in
   let p = of_return p in
@@ -497,7 +497,7 @@ let iter_with_full_binders env sigma g f n c =
     let l = Evd.expand_existential sigma ev in
     List.iter (fun c -> f n c) l
   | Case (ci,u,pms,p,iv,c,bl) ->
-    let (ci, _, pms, p, iv, c, bl) = annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+    let (ci, _, pms, (p,_), iv, c, bl) = annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
     let f_ctx (ctx, c) = f (List.fold_right g ctx n) c in
     Array.Fun1.iter f n pms; f_ctx p; iter_invert (f n) iv; f n c; Array.iter f_ctx bl
   | Proj (_,_,c) -> f n c
@@ -731,8 +731,8 @@ let fold_constr_relevance sigma f acc c =
   | Prod (na,_,_) | Lambda (na,_,_) | LetIn (na,_,_,_) ->
     fold_annot_relevance f acc na
 
-  | Case (ci,_u,_params,ret,_iv,_v,brs) ->
-    let acc = f acc ci.ci_relevance in
+  | Case (_,_u,_params,(ret,r),_iv,_v,brs) ->
+    let acc = f acc r in
     let acc = fold_case_under_context_relevance f acc ret in
     let acc = CArray.fold_left (fold_case_under_context_relevance f) acc brs in
     acc

engine/eConstr.mli

@@ -428,10 +428,10 @@ val is_global : Environ.env -> Evd.evar_map -> GlobRef.t -> t -> bool
 [@@ocaml.deprecated "Use [EConstr.isRefX] instead."]
 
 val expand_case : Environ.env -> Evd.evar_map ->
-  case -> (case_info * t * case_invert * t * t array)
+  case -> (t,t) Inductive.pexpanded_case
 
 val annotate_case : Environ.env -> Evd.evar_map -> case ->
-  case_info * EInstance.t * t array * (rel_context * t) * case_invert * t * (rel_context * t) array
+  case_info * EInstance.t * t array * ((rel_context * t) * Sorts.relevance) * case_invert * t * (rel_context * t) array
 (** Same as above, but doesn't turn contexts into binders *)
 
 val expand_branch : Environ.env -> Evd.evar_map ->
@@ -440,7 +440,7 @@ val expand_branch : Environ.env -> Evd.evar_map ->
     constructs the typed context in which the branch lives. *)
 
 val contract_case : Environ.env -> Evd.evar_map ->
-  (case_info * t * case_invert * t * t array) -> case
+  (t,t) Inductive.pexpanded_case -> case
 
 (** {5 Extra} *)
 

engine/termops.ml

@@ -649,8 +649,8 @@ let map_constr_with_binders_left_to_right env sigma g f l c =
   | Evar ev ->
     let ev' = EConstr.map_existential sigma (fun c -> f l c) ev in
     if ev' == ev then c else mkEvar ev'
-  | Case (ci,u,pms,p,iv,b,bl) ->
-      let (ci, _, pms, p0, _, b, bl0) = annotate_case env sigma (ci, u, pms, p, iv, b, bl) in
+  | Case (ci,u,pms,(p,r),iv,b,bl) ->
+      let (ci, _, pms, (p0,_), _, b, bl0) = annotate_case env sigma (ci, u, pms, (p,r), iv, b, bl) in
       let f_ctx (nas, _ as r) (ctx, c) =
         let c' = f (List.fold_right g ctx l) c in
         if c' == c then r else (nas, c')
@@ -662,7 +662,7 @@ let map_constr_with_binders_left_to_right env sigma g f l c =
       let iv' = map_invert (f l) iv in
       let bl' = Array.map_left (fun (c, c0) -> f_ctx c c0) (Array.map2 (fun x y -> (x, y)) bl bl0) in
         if b' == b && pms' == pms && p' == p && iv' == iv && bl' == bl then c
-        else mkCase (ci, u, pms', p', iv', b', bl')
+        else mkCase (ci, u, pms', (p',r), iv', b', bl')
   | Fix (ln,(lna,tl,bl as fx)) ->
       let l' = fold_rec_types g fx l in
       let (tl', bl') = map_left2 (f l) tl (f l') bl in
@@ -715,8 +715,8 @@ let map_constr_with_full_binders env sigma g f l cstr =
   | Evar ev ->
     let ev' = EConstr.map_existential sigma (fun c -> f l c) ev in
     if ev' == ev then cstr else mkEvar ev'
-  | Case (ci, u, pms, p, iv, c, bl) ->
-      let (ci, _, pms, p0, _, c, bl0) = annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+  | Case (ci, u, pms, (p,r), iv, c, bl) ->
+      let (ci, _, pms, (p0,_), _, c, bl0) = annotate_case env sigma (ci, u, pms, (p,r), iv, c, bl) in
       let f_ctx (nas, _ as r) (ctx, c) =
         let c' = f (List.fold_right g ctx l) c in
         if c' == c then r else (nas, c')
@@ -727,7 +727,7 @@ let map_constr_with_full_binders env sigma g f l cstr =
       let c' = f l c in
       let bl' = Array.map2 f_ctx bl bl0 in
       if pms==pms' && p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else
-        mkCase (ci, u, pms', p', iv', c', bl')
+        mkCase (ci, u, pms', (p',r), iv', c', bl')
   | Fix (ln,(lna,tl,bl as fx)) ->
       let tl' = Array.map (f l) tl in
       let l' = fold_rec_types g fx l in
@@ -770,7 +770,7 @@ let fold_constr_with_full_binders env sigma g f n acc c =
     let args = Evd.expand_existential sigma ev in
     List.fold_left (fun c -> f n c) acc args
   | Case (ci, u, pms, p, iv, c, bl) ->
-    let (ci, _, pms, p, _, c, bl) = EConstr.annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+    let (ci, _, pms, (p,_), _, c, bl) = EConstr.annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
     let f_ctx acc (ctx, c) = f (List.fold_right g ctx n) acc c in
     Array.fold_left f_ctx (f n (fold_invert (f n) (f_ctx (Array.fold_left (f n) acc pms) p) iv) c) bl
   | Fix (_,(lna,tl,bl)) ->

engine/univSubst.ml

@@ -190,19 +190,16 @@ let nf_evars_and_universes_opt_subst fevar fqual funiv c =
     | Sort s ->
       let s' = Sorts.subst_fn (fqual, subst_univs_universe funiv) s in
       if s' == s then c else mkSort s'
-    | Case (ci,u,pms,p,iv,t,br) ->
+    | Case (ci,u,pms,(p,rel),iv,t,br) ->
       let u' = Instance.subst_fn flevel u in
-      let ci' =
-        let rel' = frel ci.ci_relevance in
-        if rel' == ci.ci_relevance then ci else { ci with ci_relevance = rel' }
-      in
+      let rel' = frel rel in
       let pms' = Array.Smart.map aux pms in
       let p' = aux_ctx p in
       let iv' = map_invert aux iv in
       let t' = aux t in
       let br' = Array.Smart.map aux_ctx br in
-      if ci' == ci && u' == u && pms' == pms && p' == p && iv' == iv && t' == t && br' == br then c
-      else mkCase (ci', u', pms', p', iv', t', br')
+      if rel' == rel && u' == u && pms' == pms && p' == p && iv' == iv && t' == t && br' == br then c
+      else mkCase (ci, u', pms', (p',rel'), iv', t', br')
     | Array (u,elems,def,ty) ->
       let u' = Instance.subst_fn flevel u in
       let elems' = CArray.Smart.map aux elems in

kernel/cClosure.ml

@@ -264,11 +264,6 @@ let usubst_binder e x =
   let r' = usubst_relevance e r in
   if r == r' then x else { x with binder_relevance = r' }
 
-let usubst_case_info e ci =
-  let r = ci.ci_relevance in
-  let r' = usubst_relevance e r in
-  if r == r' then ci else { ci with ci_relevance = r' }
-
 let mk_lambda env t =
   let (rvars,t') = Term.decompose_lambda t in
   FLambda(List.length rvars, List.rev rvars, t', env)
@@ -534,11 +529,11 @@ let rec to_constr (lfts, usubst as ulfts) v =
     | FIrrelevant -> assert (!Flags.in_debugger); mkVar(Id.of_string"_IRRELEVANT_")
     | FLOCKED -> assert (!Flags.in_debugger); mkVar(Id.of_string"_LOCKED_")
 
-and to_constr_case (lfts,_ as ulfts) ci u pms p iv c ve env =
+and to_constr_case (lfts,_ as ulfts) ci u pms (p,r) iv c ve env =
   let subs = comp_subs ulfts env in
-  let ci = usubst_case_info subs ci in
+  let r = usubst_relevance subs r in
   if is_subs_id (fst env) && is_lift_id lfts then
-    mkCase (ci, usubst_instance subs u, pms, p, iv, to_constr ulfts c, ve)
+    mkCase (ci, usubst_instance subs u, pms, (p,r), iv, to_constr ulfts c, ve)
   else
     let f_ctx (nas, c) =
       let nas = Array.map (usubst_binder subs) nas in
@@ -548,7 +543,7 @@ and to_constr_case (lfts,_ as ulfts) ci u pms p iv c ve env =
     mkCase (ci,
             usubst_instance subs u,
             Array.map (fun c -> subst_constr subs c) pms,
-            f_ctx p,
+            (f_ctx p,r),
             iv,
             to_constr ulfts c,
             Array.map f_ctx ve)
@@ -1215,8 +1210,8 @@ let rec skip_irrelevant_stack info stk = match stk with
 | (Zfix _ | Zproj _) :: s ->
   (* Typing rules ensure that fix / proj over SProp is irrelevant *)
   skip_irrelevant_stack info s
-| ZcaseT (ci, _, _, _, _, e) :: s ->
-  let r = usubst_relevance e ci.ci_relevance in
+| ZcaseT (_, _, _, (_,r), _, e) :: s ->
+  let r = usubst_relevance e r in
   if is_irrelevant info r then skip_irrelevant_stack info s
   else stk
 | Zprimitive _ :: _ -> assert false (* no irrelevant primitives so far *)
@@ -1240,9 +1235,9 @@ let rec knh info m stk =
     | FCLOS(t,e) -> knht info e t (zupdate info m stk)
     | FLOCKED -> assert false
     | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk))
-    | FCaseT(ci,u,pms,p,t,br,e) ->
-      let r = usubst_relevance e ci.ci_relevance in
-      if is_irrelevant info r then
+    | FCaseT(ci,u,pms,(_,r as p),t,br,e) ->
+      let r' = usubst_relevance e r in
+      if is_irrelevant info r' then
         (mk_irrelevant, skip_irrelevant_stack info stk)
       else
         knh info t (ZcaseT(ci,u,pms,p,br,e)::zupdate info m stk)
@@ -1271,13 +1266,13 @@ and knht info e t stk =
   match kind t with
     | App(a,b) ->
         knht info e a (append_stack (mk_clos_vect e b) stk)
-    | Case(ci,u,pms,p,NoInvert,t,br) ->
-      if is_irrelevant info (usubst_relevance e ci.ci_relevance) then
+    | Case(ci,u,pms,(_,r as p),NoInvert,t,br) ->
+      if is_irrelevant info (usubst_relevance e r) then
         (mk_irrelevant, skip_irrelevant_stack info stk)
       else
         knht info e t (ZcaseT(ci, u, pms, p, br, e)::stk)
-    | Case(ci,u,pms,p,CaseInvert{indices},t,br) ->
-      if is_irrelevant info (usubst_relevance e ci.ci_relevance) then
+    | Case(ci,u,pms,(_,r as p),CaseInvert{indices},t,br) ->
+      if is_irrelevant info (usubst_relevance e r) then
         (mk_irrelevant, skip_irrelevant_stack info stk)
       else
         let term = FCaseInvert (ci, u, pms, p, (Array.map (mk_clos e) indices), mk_clos e t, br, e) in
@@ -1572,15 +1567,15 @@ and zip_term info tab m stk = match stk with
 | [] -> m
 | Zapp args :: s ->
     zip_term info tab (mkApp(m, Array.map (kl info tab) args)) s
-| ZcaseT(ci, u, pms, p, br, e) :: s ->
+| ZcaseT(ci, u, pms, (p,r), br, e) :: s ->
   let zip_ctx (nas, c) =
       let nas = Array.map (usubst_binder e) nas in
       let e = usubs_liftn (Array.length nas) e in
       (nas, klt info tab e c)
     in
-    let ci = usubst_case_info e ci in
+    let r = usubst_relevance e r in
     let u = usubst_instance e u in
-    let t = mkCase(ci, u, Array.map (fun c -> klt info tab e c) pms, zip_ctx p,
+    let t = mkCase(ci, u, Array.map (fun c -> klt info tab e c) pms, (zip_ctx p, r),
       NoInvert, m, Array.map zip_ctx br) in
     zip_term info tab t s
 | Zproj (p,r)::s ->