From 449b26ff6d7259c2e494b830bff06d87a9ba43b8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 12 Jun 2024 16:19:09 +0200
Subject: [PATCH] hconstr v6: hcons in hconstr.of_constr

---
 kernel/hConstr.ml     | 27 +++++++++++++++++++++++++--
 kernel/safe_typing.ml |  2 +-
 kernel/typeops.ml     |  4 ++--
 3 files changed, 28 insertions(+), 5 deletions(-)

diff --git a/kernel/hConstr.ml b/kernel/hConstr.ml
index cbc5b55f3efba..ce23f04956ad5 100644
--- a/kernel/hConstr.ml
+++ b/kernel/hConstr.ml
@@ -406,6 +406,7 @@ type t = {
   kind : (t,t,Sorts.t,Instance.t,Sorts.relevance) kind_of_term;
   isRel : int (* 0 -> not a rel, otherwise unique identifier of that binder *);
   hash : int;
+  hcons_hash : int;
   mutable refcount : int;
 }
 
@@ -591,11 +592,30 @@ let hcons_inplace f a = Array.iteri (fun i x -> Array.unsafe_set a i (f x)) a
 let of_kind_nohashcons kind =
   let self = kind_to_constr kind in
   let hash = hash_kind hash kind in
+  let hcons_hash = hash_kind (fun x -> x.hcons_hash) kind in
   let () = match kind with
     | Rel _ -> assert false
     | _ -> ()
   in
-  { self; kind; hash; isRel = 0; refcount = 1 }
+  { self; kind; hash; hcons_hash; isRel = 0; refcount = 1 }
+
+let hcons_array a ka =
+  let h = hash_array (fun c -> c.hcons_hash) ka in
+  Array.iteri (fun i c -> Array.unsafe_set a i c.self) ka;
+  HashsetTermArray.repr h a term_array_table
+
+let hcons_arrays self kind =
+  match Constr.kind self, kind with
+  | App (h, args), App (_, kargs) ->
+    make @@ App (h, hcons_array args kargs)
+  | Case (v1,v2,pms,v3,v4,v5,v6), Case (_,_,kpms,_,_,_,_) ->
+    make @@ Case (v1,v2,hcons_array pms kpms,v3,v4,v5,v6)
+  | Fix (ln,(lna,tl,bl)), Fix (_,(_,ktl,kbl)) ->
+    make @@ Fix (ln, (lna,hcons_array tl ktl, hcons_array bl kbl))
+  | CoFix (ln,(lna,tl,bl)), CoFix (_,(_,ktl,kbl)) ->
+    make @@ CoFix (ln, (lna,hcons_array tl ktl, hcons_array bl kbl))
+  | Array (u,t,def,ty), Array (_,kt,_,_) -> make @@ Array (u,hcons_array t kt,def,ty)
+  | _ -> self
 
 let rec of_constr tbl local_env c =
   let c =
@@ -603,6 +623,9 @@ let rec of_constr tbl local_env c =
     let self = kind_to_constr kind in
     let self = if hasheq (Constr.kind self) (Constr.kind c) then c else self in
     let hash = hash_kind hash kind in
+    let hcons_hash = hash_kind (fun x -> x.hcons_hash) kind in
+    let self = hcons_arrays self kind in
+    let self = HashsetTerm.repr hcons_hash self term_table in
     let isRel, hash = match kind with
       | Rel n ->
         let uid = Range.get local_env.rels (n-1) in
@@ -610,7 +633,7 @@ let rec of_constr tbl local_env c =
         uid, Hashset.Combine.combine uid hash
       | _ -> 0, hash
     in
-    { self; kind; hash; isRel; refcount = 1 }
+    { self; kind; hash; hcons_hash; isRel; refcount = 1 }
   in
   match Tbl.find_opt tbl c with
   | Some c' -> c'.refcount <- c'.refcount + 1; c'
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a7825099e749c..2d492ae3cd6e4 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -670,7 +670,7 @@ let add_constant_aux senv (kn, cb) =
   let l = Constant.label kn in
   (* This is the only place where we hashcons the contents of a constant body *)
   let senv, cb = push_const_bytecode senv cb in
-  let cb = if sections_are_opened senv then cb else Declareops.hcons_const_body cb in
+  let cb = if true || sections_are_opened senv then cb else Declareops.hcons_const_body cb in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 2a063648bc5dd..44831a18324e2 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -916,7 +916,7 @@ let check_wellformed_universes env c =
 
 let infer env constr =
   let () = check_wellformed_universes env constr in
-  let _constr, t = execute env constr in
+  let constr, t = execute env constr in
   make_judge constr t
 
 let assumption_of_judgment env {uj_val=c; uj_type=t} =
@@ -928,7 +928,7 @@ let type_judgment env {uj_val=c; uj_type=t} =
 
 let infer_type env constr =
   let () = check_wellformed_universes env constr in
-  let _constr, t = execute env constr in
+  let constr, t = execute env constr in
   let s = check_type env constr t in
   {utj_val = constr; utj_type = s}