From f91f5c7b6610c59f7fd1ac4958cacfa2d6f249c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 12 Jun 2024 15:51:58 +0200 Subject: [PATCH] generalize hash_kind we could try to use it in hcons to reduce fragility, not sure if good idea (we would still need to deal with arrays somehow) --- kernel/hConstr.ml | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/kernel/hConstr.ml b/kernel/hConstr.ml index 58feacea2ea5a..85874a7ac73c5 100644 --- a/kernel/hConstr.ml +++ b/kernel/hConstr.ml @@ -524,15 +524,15 @@ let push_letin ~body ~typ env = let hash_array hashf a = Array.fold_left (fun hash x -> Hashset.Combine.combine hash (hashf x)) 0 a -let hash_kind = let open Hashset.Combine in function +let hash_kind (type a) (hash:a -> int) = let open Hashset.Combine in function | Var i -> combinesmall 1 (Id.hash i) | Sort s -> combinesmall 2 (Sorts.hash s) - | Cast (c,k,t) -> combinesmall 3 (combine3 c.hash (hash_cast_kind k) t.hash) - | Prod (na,t,c) -> combinesmall 4 (combine3 (hash_annot na) t.hash c.hash) - | Lambda (na,t,c) -> combinesmall 5 (combine3 (hash_annot na) t.hash c.hash) - | LetIn (na,b,t,c) -> combinesmall 6 (combine4 (hash_annot na) b.hash t.hash c.hash) + | Cast (c,k,t) -> combinesmall 3 (combine3 (hash c) (hash_cast_kind k) (hash t)) + | Prod (na,t,c) -> combinesmall 4 (combine3 (hash_annot na) (hash t) (hash c)) + | Lambda (na,t,c) -> combinesmall 5 (combine3 (hash_annot na) (hash t) (hash c)) + | LetIn (na,b,t,c) -> combinesmall 6 (combine4 (hash_annot na) (hash b) (hash t) (hash c)) | App (h,args) -> - combinesmall 7 (combine (hash_array hash args) h.hash) + combinesmall 7 (combine (hash_array hash args) (hash h)) | Evar _ -> assert false | Const (c,u) -> combinesmall 9 (combine (Constant.SyntacticOrd.hash c) (Instance.hash u)) | Ind (ind,u) -> combinesmall 10 (combine (Ind.SyntacticOrd.hash ind) (Instance.hash u)) @@ -540,11 +540,11 @@ let hash_kind = let open Hashset.Combine in function | Case (_,u,pms,(p,_),_,c,bl) -> let hash_ctx (bnd,c) = let hna = hash_array hash_annot bnd in - combine hna c.hash + combine hna (hash c) in let hpms = hash_array hash pms in let hbl = hash_array hash_ctx bl in - let h = combine5 (Instance.hash u) c.hash hpms (hash_ctx p) hbl in + let h = combine5 (Instance.hash u) (hash c) hpms (hash_ctx p) hbl in combinesmall 12 h | Fix (_,(lna,tl,bl)) -> combinesmall 13 (combine3 (hash_array hash_annot lna) (hash_array hash tl) (hash_array hash bl)) @@ -552,10 +552,10 @@ let hash_kind = let open Hashset.Combine in function combinesmall 14 (combine3 (hash_array hash_annot lna) (hash_array hash tl) (hash_array hash bl)) | Meta _ -> assert false | Rel n -> combinesmall 16 n - | Proj (p,_,c) -> combinesmall 17 (combine (Projection.SyntacticOrd.hash p) c.hash) + | Proj (p,_,c) -> combinesmall 17 (combine (Projection.SyntacticOrd.hash p) (hash c)) | Int i -> combinesmall 18 (Uint63.hash i) | Float f -> combinesmall 19 (Float64.hash f) - | Array (u,t,def,ty) -> combinesmall 20 (combine4 (Instance.hash u) (hash_array hash t) def.hash ty.hash) + | Array (u,t,def,ty) -> combinesmall 20 (combine4 (Instance.hash u) (hash_array hash t) (hash def) (hash ty)) let kind_to_constr = function | Rel n -> mkRel n @@ -590,7 +590,7 @@ 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 kind in + let hash = hash_kind hash kind in let () = match kind with | Rel _ -> assert false | _ -> () @@ -602,7 +602,7 @@ let rec of_constr tbl local_env c = let kind = of_constr_aux tbl local_env c in 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 kind in + let hash = hash_kind hash kind in let isRel, hash = match kind with | Rel n -> let uid = Range.get local_env.rels (n-1) in