From 501546a0727f52ddd95b47dbcf17afaf7bb3fcbe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 27 Jun 2024 16:57:46 +0200 Subject: [PATCH] Try to reuse partial hashconsing for definition bodies --- kernel/constant_typing.ml | 12 ++-- kernel/constant_typing.mli | 5 +- kernel/constr.ml | 116 ++++++++++++++++++++++++++----------- kernel/constr.mli | 17 ++++++ kernel/declareops.ml | 8 +-- kernel/declareops.mli | 3 +- kernel/hConstr.ml | 15 +++++ kernel/hConstr.mli | 2 + kernel/safe_typing.ml | 43 +++++++++----- kernel/typeops.ml | 16 +++-- kernel/typeops.mli | 1 + 11 files changed, 171 insertions(+), 67 deletions(-) diff --git a/kernel/constant_typing.ml b/kernel/constant_typing.ml index fecce595fe22b..8ae509e314e1c 100644 --- a/kernel/constant_typing.ml +++ b/kernel/constant_typing.ml @@ -214,7 +214,8 @@ let infer_parameter ~sec_univs env entry = let infer_definition ~sec_univs env entry = let env, usubst, _, univs = process_universes env entry.definition_entry_universes in - let j = Typeops.infer env entry.definition_entry_body in + let hbody = HConstr.of_constr env entry.definition_entry_body in + let j = Typeops.infer_hconstr env hbody in let typ = match entry.definition_entry_type with | None -> Vars.subst_univs_level_constr usubst j.uj_type @@ -224,9 +225,10 @@ let infer_definition ~sec_univs env entry = Vars.subst_univs_level_constr usubst tj.utj_val in let body = Vars.subst_univs_level_constr usubst j.uj_val in + let hbody = if body == j.uj_val then Some hbody else None in let def = Def body in let hyps = used_section_variables env entry.definition_entry_secctx (Some body) typ in - { + hbody, { const_hyps = hyps; const_univ_hyps = make_univ_hyps sec_univs; const_body = def; @@ -275,7 +277,8 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out in (* Note: non-trivial trusted side-effects only in monomorphic case *) let body,env,ectx = skip_trusted_seff valid_signatures body env in - let j = Typeops.infer env body in + let hbody = HConstr.of_constr env body in + let j = Typeops.infer_hconstr env hbody in let j = unzip ectx j in let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in let declared = @@ -285,7 +288,8 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out let () = assert (Id.Set.equal declared declared') in (* Note: non-trivial usubst only in polymorphic case *) let def = Vars.subst_univs_level_constr usubst j.uj_val in - def, univs + let hbody = if def == j.uj_val && List.is_empty ectx then Some hbody else None in + hbody, def, univs (*s Global and local constant declaration. *) diff --git a/kernel/constant_typing.mli b/kernel/constant_typing.mli index b54e89142b63e..d15df0ea45316 100644 --- a/kernel/constant_typing.mli +++ b/kernel/constant_typing.mli @@ -39,10 +39,11 @@ val infer_parameter : val infer_definition : sec_univs:UVars.Instance.t option -> env -> definition_entry -> - ('a, unit) pconstant_body + HConstr.t option * ('a, unit) pconstant_body val infer_opaque : sec_univs:UVars.Instance.t option -> env -> 'a opaque_entry -> (unit, unit) pconstant_body * typing_context -val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes) +val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> + HConstr.t option * Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes diff --git a/kernel/constr.ml b/kernel/constr.ml index 8face8549fc37..ed1ab91b84ed6 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -460,6 +460,10 @@ let destRef c = let open GlobRef in match kind c with | Construct (c,u) -> ConstructRef c, u | _ -> raise DestKO +let destArray c = match kind c with + | Array (u,ar,def,ty) -> u,ar,def,ty + | _ -> raise DestKO + (******************************************************************) (* Flattening and unflattening of embedded applications and casts *) (******************************************************************) @@ -1322,6 +1326,25 @@ module Hannot = Hashcons.Make(Hannotinfo) let hcons_annot = Hashcons.simple_hcons Hannot.generate Hannot.hcons Name.hcons +let dbg = CDebug.create ~name:"hcons" () + +module GenHCons(C:sig + type t + val kind : t -> (t, t, Sorts.t, Instance.t, Sorts.relevance) kind_of_term + val self : t -> constr + val refcount : t -> int + + val via_hconstr : bool + + module Tbl : sig + val find_opt : t -> (constr * int) option + val add : t -> constr * int -> unit + end + end) = struct +open C + +let steps = ref 0 + let rec hash_term (t : t) = match kind t with | Var i -> @@ -1346,12 +1369,11 @@ let rec hash_term (t : t) = let c, hc = sh_rec c in (LetIn (hcons_annot na, b, t, c), combinesmall 6 (combine4 (hash_annot Name.hash na) hb ht hc)) | App (c,l) -> + let _, cl = destApp (self t) in let c, hc = sh_rec c in - let l, hl = hash_term_array l in + let l, hl = hash_term_array cl l in (App (c,l), combinesmall 7 (combine hl hc)) - | Evar (e,l) -> - let l, hl = hash_list_array l in - (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl)) + | Evar _ -> assert false | Const (c,u) -> let c' = hcons_con c in let u', hu = Instance.share u in @@ -1374,9 +1396,10 @@ let rec hash_term (t : t) = (lna, c), combine hna hc in let u, hu = Instance.share u in - let pms,hpms = hash_term_array pms in + let _,_,cpms,_,civ,_,_ = destCase (self t) in + let pms,hpms = hash_term_array cpms pms in let p, hp = hcons_ctx p in - let iv, hiv = sh_invert iv in + let iv, hiv = sh_invert civ iv in let c, hc = sh_rec c in let fold accu c = let c, h = hcons_ctx c in @@ -1386,16 +1409,18 @@ let rec hash_term (t : t) = let hbl = combine (combine hc (combine hiv (combine hpms (combine hu hp)))) hbl in (Case (hcons_caseinfo ci, u, pms, (p,r), iv, c, bl), combinesmall 12 hbl) | Fix (ln,(lna,tl,bl)) -> - let bl,hbl = hash_term_array bl in - let tl,htl = hash_term_array tl in + let _, (_,ctl,cbl) = destFix (self t) in + let bl,hbl = hash_term_array cbl bl in + let tl,htl = hash_term_array ctl tl in let () = Array.iteri (fun i x -> Array.unsafe_set lna i (hcons_annot x)) lna in let fold accu na = combine (hash_annot Name.hash na) accu in let hna = Array.fold_left fold 0 lna in let h = combine3 hna hbl htl in (Fix (ln,(lna,tl,bl)), combinesmall 13 h) | CoFix(ln,(lna,tl,bl)) -> - let bl,hbl = hash_term_array bl in - let tl,htl = hash_term_array tl in + let _, (_,ctl,cbl) = destCoFix (self t) in + let bl,hbl = hash_term_array cbl bl in + let tl,htl = hash_term_array ctl tl in let () = Array.iteri (fun i x -> Array.unsafe_set lna i (hcons_annot x)) lna in let fold accu na = combine (hash_annot Name.hash na) accu in let hna = Array.fold_left fold 0 lna in @@ -1414,58 +1439,59 @@ let rec hash_term (t : t) = (t, combinesmall 18 (combine h l)) | Float f as t -> (t, combinesmall 19 (Float64.hash f)) | String s as t -> (t, combinesmall 20 (Pstring.hash s)) - | Array (u,t,def,ty) -> + | Array (u,ar,def,ty) -> + let _,car,_,_ = destArray (self t) in let u, hu = Instance.share u in - let t, ht = hash_term_array t in + let t, ht = hash_term_array car ar in let def, hdef = sh_rec def in let ty, hty = sh_rec ty in let h = combine4 hu ht hdef hty in (Array(u,t,def,ty), combinesmall 21 h) -and sh_invert = function - | NoInvert -> NoInvert, 0 - | CaseInvert {indices;} -> - let indices, ha = hash_term_array indices in +and sh_invert civ iv = match civ, iv with + | NoInvert, NoInvert -> NoInvert, 0 + | CaseInvert {indices=cindices}, CaseInvert {indices;} -> + let indices, ha = hash_term_array cindices indices in CaseInvert {indices;}, combinesmall 1 ha + | (NoInvert | CaseInvert _), _ -> assert false -and sh_rec t = +and sh_rec_main t = let (y, h) = hash_term t in (HashsetTerm.repr h (T y) term_table, h) +and sh_rec t = + incr steps; + if refcount t = 1 then sh_rec_main t + else match Tbl.find_opt t with + | Some res -> res + | None -> + let res = sh_rec_main t in + Tbl.add t res; + res + (* Note : During hash-cons of arrays, we modify them *in place* *) -and hash_term_array t = +and hash_term_array ct t = let accu = ref 0 in for i = 0 to Array.length t - 1 do let x, h = sh_rec (Array.unsafe_get t i) in accu := combine !accu h; - Array.unsafe_set t i x + Array.unsafe_set ct i x done; let h = !accu in - (HashsetTermArray.repr h t term_array_table, h) - -and hash_list_array l = - let fold accu c = - let c, h = sh_rec c in - (combine accu h, c) - in - let h, l = SList.Smart.fold_left_map fold 0 l in - (l, h) - - (* Make sure our statically allocated Rels (1 to 16) are considered - as canonical, and hence hash-consed to themselves *) -let () = ignore (hash_term_array rels) + (HashsetTermArray.repr h ct term_array_table, h) let hcons t = NewProfile.profile "Constr.hcons" (fun () -> fst (sh_rec t)) () -let dbg = CDebug.create ~name:"hcons" () - let hcons t = + steps := 0; let t = hcons t in dbg Pp.(fun () -> let open Hashset in let stats = HashsetTerm.stats term_table in v 0 ( + str "via hconstr = " ++ bool via_hconstr ++ spc() ++ + str "steps = " ++ int !steps ++ spc() ++ str "num_bindings = " ++ int stats.num_bindings ++ spc() ++ str "num_buckets = " ++ int stats.num_buckets ++ spc() ++ str "max_bucket_length = " ++ int stats.max_bucket_length @@ -1473,6 +1499,28 @@ let hcons t = ); t +end + +module HCons = GenHCons(struct + type t = constr + let kind = kind + let self x = x + let refcount _ = 1 + + let via_hconstr = false + + module Tbl = struct + let find_opt _ = None + let add _ _ : unit = assert false + end + end) + + (* Make sure our statically allocated Rels (1 to 16) are considered + as canonical, and hence hash-consed to themselves *) +let () = ignore (HCons.hash_term_array rels rels) + +let hcons = HCons.hcons + (* let hcons_types = hcons_constr *) type rel_declaration = (constr, types, Sorts.relevance) Context.Rel.Declaration.pt diff --git a/kernel/constr.mli b/kernel/constr.mli index f1d480724039f..629c655f01719 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -628,6 +628,23 @@ val case_info_hash : case_info -> int (*********************************************************************) +module GenHCons(C:sig + type t + val kind : t -> (t, t, Sorts.t, UVars.Instance.t, Sorts.relevance) kind_of_term + val self : t -> constr + val refcount : t -> int + + val via_hconstr : bool + + module Tbl : sig + val find_opt : t -> (constr * int) option + val add : t -> constr * int -> unit + end + end) : sig + val hcons : C.t -> constr +end + + val hcons : constr -> constr val hasheq_kind : (_ kind_of_term as 'k) -> 'k -> bool diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 0ed78b044b93c..7a34a9c01e8b7 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -136,12 +136,12 @@ let hcons_rel_decl = let hcons_rel_context l = List.Smart.map hcons_rel_decl l -let hcons_const_def = function +let hcons_const_def ?(hbody=Constr.hcons) = function | Undef inl -> Undef inl | Primitive p -> Primitive p | Symbol r -> Symbol r | Def l_constr -> - Def (Constr.hcons l_constr) + Def (hbody l_constr) | OpaqueDef _ as x -> x (* hashconsed when turned indirect *) let hcons_universes cbu = @@ -150,9 +150,9 @@ let hcons_universes cbu = | Polymorphic ctx -> Polymorphic (UVars.hcons_abstract_universe_context ctx) -let hcons_const_body cb = +let hcons_const_body ?hbody cb = { cb with - const_body = hcons_const_def cb.const_body; + const_body = hcons_const_def ?hbody cb.const_body; const_type = Constr.hcons cb.const_type; const_universes = hcons_universes cb.const_universes; } diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 84be152b80964..7b3be4bf1973f 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -88,7 +88,8 @@ val safe_flags : Conv_oracle.oracle -> typing_flags of the structure, but simply hash-cons all inner constr and other known elements *) -val hcons_const_body : ('a, 'b) pconstant_body -> ('a, 'b) pconstant_body +val hcons_const_body : ?hbody:(Constr.t -> Constr.t) -> + ('a, 'b) pconstant_body -> ('a, 'b) pconstant_body val hcons_mind : mutual_inductive_body -> mutual_inductive_body val hcons_module_body : module_body -> module_body val hcons_module_type : module_type_body -> module_type_body diff --git a/kernel/hConstr.ml b/kernel/hConstr.ml index 1b568e37a53fb..53b8ce2762a29 100644 --- a/kernel/hConstr.ml +++ b/kernel/hConstr.ml @@ -384,3 +384,18 @@ let of_constr env c = let of_constr env c = NewProfile.profile "HConstr.of_constr" (fun () -> of_constr env c) () let kind x = x.kind + +let hcons x = + let tbl = Tbl.create 47 in + let module HCons = GenHCons(struct + type nonrec t = t + let kind = kind + let self = self + let refcount = refcount + let via_hconstr = true + module Tbl = struct + let find_opt x = Tbl.find_opt tbl x + let add x y = Tbl.add tbl x y + end + end) in + HCons.hcons x diff --git a/kernel/hConstr.mli b/kernel/hConstr.mli index 08c4c12f1ef3d..b1e0cfe7f8125 100644 --- a/kernel/hConstr.mli +++ b/kernel/hConstr.mli @@ -57,3 +57,5 @@ module Tbl : sig val create : int -> 'a t end + +val hcons : t -> Constr.t diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 9d3b464c72fe6..039760999cbfa 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -662,11 +662,19 @@ let push_const_bytecode senv cb = let senv = set_vm_library vmtab senv in senv, cb -let add_constant_aux senv (kn, cb) = +let make_hbody = function + | None -> None + | Some hc -> Some (fun c -> + assert (c == HConstr.self hc); + HConstr.hcons hc) + +let add_constant_aux senv ?hbody (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 sections_are_opened senv then cb else + Declareops.hcons_const_body ?hbody:(make_hbody hbody) cb + in let senv' = add_field (l,SFBconst cb) (C kn) senv in let senv'' = match cb.const_body with | Undef (Some lev) -> @@ -830,7 +838,7 @@ let infer_direct_opaque ~sec_univs env ce = let cb, ctx = Constant_typing.infer_opaque ~sec_univs env ce in let body = ce.Entries.opaque_entry_body, Univ.ContextSet.empty in let handle _env c () = (c, Univ.ContextSet.empty, 0) in - let (c, u) = Constant_typing.check_delayed handle ctx (body, ()) in + let (_hbody, c, u) = Constant_typing.check_delayed handle ctx (body, ()) in (* No constraints can be generated, we set it empty everywhere *) let () = assert (is_empty_private u) in { cb with const_body = OpaqueDef c } @@ -864,11 +872,11 @@ let export_side_effects senv eff = let univs = Univ.ContextSet.union uctx univs in let env, cb = let ce = constant_entry_of_side_effect eff in - let cb = match ce with + let _hbody, cb = match ce with | DefinitionEff ce -> Constant_typing.infer_definition ~sec_univs env ce | OpaqueEff ce -> - infer_direct_opaque ~sec_univs env ce + None, infer_direct_opaque ~sec_univs env ce in let cb = compile_bytecode env cb in let eff = { eff with seff_body = cb } in @@ -910,7 +918,7 @@ let export_private_constants eff senv = let add_constant l decl senv = let kn = Constant.make2 senv.modpath l in - let senv, cb = + let senv, (hbody, cb) = let sec_univs = Option.map Section.all_poly_univs senv.sections in match decl with | Entries.OpaqueEntry ce -> @@ -921,23 +929,23 @@ let add_constant l decl senv = let nonce = Nonce.create () in let future_cst = HandleMap.add i (ctx, senv, nonce) senv.future_cst in let senv = { senv with future_cst } in - senv, { cb with const_body = OpaqueDef o } + senv, (None, { cb with const_body = OpaqueDef o }) | Entries.DefinitionEntry entry -> senv, Constant_typing.infer_definition ~sec_univs senv.env entry | Entries.ParameterEntry entry -> - senv, Constant_typing.infer_parameter ~sec_univs senv.env entry + senv, (None, Constant_typing.infer_parameter ~sec_univs senv.env entry) | Entries.PrimitiveEntry entry -> let senv = match entry with | { Entries.prim_entry_content = CPrimitives.OT_type t; _ } -> if sections_are_opened senv then CErrors.anomaly (Pp.str "Primitive type not allowed in sections"); add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv | _ -> senv in - senv, Constant_typing.infer_primitive senv.env entry + senv, (None, Constant_typing.infer_primitive senv.env entry) | Entries.SymbolEntry entry -> - senv, Constant_typing.infer_symbol senv.env entry + senv, (None, Constant_typing.infer_symbol senv.env entry) in let cb = compile_bytecode senv.env cb in - let senv = add_constant_aux senv (kn, cb) in + let senv = add_constant_aux senv ?hbody (kn, cb) in kn, senv let add_constant ?typing_flags l decl senv = @@ -965,8 +973,11 @@ let check_opaque senv (i : Opaqueproof.opaque_handle) pf = in body, uctx, trusted in - let (c, ctx) = Constant_typing.check_delayed handle ty_ctx pf in - let c = Constr.hcons c in + let (hbody, c, ctx) = Constant_typing.check_delayed handle ty_ctx pf in + let c = match hbody with + | Some hbody -> assert (c == HConstr.self hbody); HConstr.hcons hbody + | None -> Constr.hcons c + in let ctx = match ctx with | Opaqueproof.PrivateMonomorphic u -> Opaqueproof.PrivateMonomorphic (Univ.hcons_universe_context_set u) @@ -1007,12 +1018,12 @@ let check_constraints uctx = function let add_private_constant l uctx decl senv : (Constant.t * private_constants) * safe_environment = let kn = Constant.make2 senv.modpath l in let senv = push_context_set ~strict:true uctx senv in - let cb = + let hbody, cb = let sec_univs = Option.map Section.all_poly_univs senv.sections in match decl with | OpaqueEff ce -> let () = assert (check_constraints uctx ce.Entries.opaque_entry_universes) in - infer_direct_opaque ~sec_univs senv.env ce + None, infer_direct_opaque ~sec_univs senv.env ce | DefinitionEff ce -> let () = assert (check_constraints uctx ce.Entries.definition_entry_universes) in Constant_typing.infer_definition ~sec_univs senv.env ce @@ -1028,7 +1039,7 @@ let add_private_constant l uctx decl senv : (Constant.t * private_constants) * s { cb with const_body = Undef None } | Undef _ | Primitive _ | Symbol _ -> assert false in - let senv = add_constant_aux senv (kn, dcb) in + let senv = add_constant_aux senv ?hbody (kn, dcb) in let eff = let from_env = CEphemeron.create (Certificate.make senv) in let eff = { diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 26da7c678c7fd..ef5ccb03fbc1e 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -856,8 +856,7 @@ and execute_array tbl env cs = Array.map (fun c -> execute tbl env c) cs let execute env c = - let c = HConstr.of_constr env c in - NewProfile.profile "Typeops.execute" (fun () -> c, execute (HConstr.Tbl.create 57) env c) () + NewProfile.profile "Typeops.execute" (fun () -> execute (HConstr.Tbl.create 57) env c) () (* Derived functions *) @@ -877,12 +876,16 @@ let check_wellformed_universes env c = let check_wellformed_universes env c = NewProfile.profile "check-wf-univs" (fun () -> check_wellformed_universes env c) () -let infer env constr = - let () = check_wellformed_universes env constr in - let hconstr, t = execute env constr in +let infer_hconstr env hconstr = let constr = HConstr.self hconstr in + let () = check_wellformed_universes env constr in + let t = execute env hconstr in make_judge constr t +let infer env c = + let c = HConstr.of_constr env c in + infer_hconstr env c + let assumption_of_judgment env {uj_val=c; uj_type=t} = infer_assumption env c t @@ -892,8 +895,9 @@ let type_judgment env {uj_val=c; uj_type=t} = let infer_type env constr = let () = check_wellformed_universes env constr in - let hconstr, t = execute env constr in + let hconstr = HConstr.of_constr env constr in let constr = HConstr.self hconstr in + let t = execute env hconstr in let s = check_type env constr t in {utj_val = constr; utj_type = s} diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 1e40b77b77b86..42fdcf9cd068a 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -25,6 +25,7 @@ open Environ Do not discard the result. *) val infer : env -> constr -> unsafe_judgment +val infer_hconstr : env -> HConstr.t -> unsafe_judgment val infer_type : env -> types -> unsafe_type_judgment val check_context :