From 6519becfbcd1a2c4ab634b92b31ef4d491f3489e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 26 Jul 2024 13:48:46 +0200
Subject: [PATCH] hconstr don't use push_unknown_rel for matches

---
 kernel/hConstr.ml | 36 ++++++++++++++++++++++++++++++------
 1 file changed, 30 insertions(+), 6 deletions(-)

diff --git a/kernel/hConstr.ml b/kernel/hConstr.ml
index 3d651dad71c5b..da67bbc63e8cf 100644
--- a/kernel/hConstr.ml
+++ b/kernel/hConstr.ml
@@ -109,6 +109,8 @@ module Tbl = struct
 end
 
 type local_env = {
+  (* only used for globals, rel context is not correct *)
+  globals : Environ.env;
   (* unique identifiers for each binder crossed *)
   rels : int Range.t;
   (* global counter *)
@@ -120,7 +122,8 @@ type local_env = {
   letin_uids : int Tbl.t Tbl.t;
 }
 
-let empty_env () = {
+let empty_env env = {
+  globals = env;
   rels = Range.empty;
   cnt = ref 0;
   unknown_cnt = ref 0;
@@ -128,6 +131,7 @@ let empty_env () = {
   letin_uids = Tbl.create 47;
 }
 
+(* still used in fixpoint *)
 let push_unknown_rel env =
   incr env.cnt;
   incr env.unknown_cnt;
@@ -172,6 +176,12 @@ let push_letin ~body ~typ env =
   in
   { env with rels = Range.cons uid env.rels }
 
+module RelDecl = Context.Rel.Declaration
+
+let push_decl d env = match d with
+  | RelDecl.LocalAssum (_,t) -> push_assum t env
+  | RelDecl.LocalDef (_,body,typ) -> push_letin ~body ~typ env
+
 let hash_annot = hash_annot Name.hash
 
 let hash_array hashf a = Array.fold_left (fun hash x -> Hashset.Combine.combine hash (hashf x)) 0 a
@@ -337,22 +347,29 @@ and of_constr_aux tbl local_env c =
     let u = UVars.Instance.hcons u in
     Construct (c,u)
   | Case (ci,u,pms,(p,r),iv,c,bl) ->
-    let of_ctx (bnd, c) =
+    let p', bl' =
+      let mib, mip = Inductive.lookup_mind_specif local_env.globals ci.ci_ind in
+      let (_, (p,_), _, _, bl) = Inductive.expand_case_specif mib (ci,u,pms,(p,r),iv,c,bl) in
+      let p = Term.decompose_lambda_n_decls (mip.Declarations.mind_nrealdecls + 1) p in
+      let bl = Array.map2 Term.decompose_lambda_n_decls ci.ci_cstr_ndecls bl in
+      p, bl
+    in
+    let of_ctx (bnd, c) (bnd', _) =
       let () = hcons_inplace hcons_annot bnd in
-      let local_env = Array.fold_left (fun local_env _ -> push_unknown_rel local_env) local_env bnd in
+      let local_env = push_rel_context tbl local_env bnd' in
       let c = of_constr tbl local_env c in
       bnd, c
     in
     let ci = hcons_caseinfo ci in
     let u = UVars.Instance.hcons u in
     let pms = Array.map (of_constr tbl local_env) pms in
-    let p = of_ctx p in
+    let p = of_ctx p p' in
     let iv = match iv with
       | NoInvert -> NoInvert
       | CaseInvert {indices} -> CaseInvert {indices=Array.map (of_constr tbl local_env) indices}
     in
     let c = of_constr tbl local_env c in
-    let bl = Array.map of_ctx bl in
+    let bl = Array.map2 of_ctx bl bl' in
     Case (ci,u,pms,(p,r),iv,c,bl)
   | Fix (ln,(lna,tl,bl)) ->
     let () = hcons_inplace hcons_annot lna in
@@ -380,6 +397,13 @@ and of_constr_aux tbl local_env c =
     let ty = of_constr tbl local_env ty in
     Array (u,t,def,ty)
 
+and push_rel_context tbl local_env ctx =
+  List.fold_right (fun d local_env ->
+      let d = RelDecl.map_constr_het (fun r -> r) (of_constr tbl local_env) d in
+      push_decl d local_env)
+    ctx
+    local_env
+
 let dbg = CDebug.create ~name:"hconstr" ()
 
 let tree_size c =
@@ -389,7 +413,7 @@ let tree_size c =
   aux 0 c
 
 let of_constr env c =
-  let local_env = empty_env () in
+  let local_env = empty_env env in
   let local_env = iterate push_unknown_rel (Environ.nb_rel env) local_env in
   let tbl = Tbl.create 57 in
   let c = of_constr tbl local_env c in