From 82b92b63962a7e60788e604e4d590cb9b79f91ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 9 Dec 2020 19:33:50 +0100 Subject: [PATCH 1/2] Introduce an efficient typing rule for let-bindings in Typeops. When the expand_let typing flag is set in the environment, we change the kernel typing rule for let-bindings from let x := t in u : T{x := t} to let x := t in u : let x := t in T. We cannot do this by default since it may change the inferred type for some expressions, which is returned when the expected type is not provided. To work around this, we statically set the flag in expressions for which the precise inferred type is not relevant. For now there is no user-facing flag that would allow setting this option in a more fine-grained way though, but it is easy to fix. This is a revival of #13606 and a partial fix of #11838. The latter still suffers from superlinear blowups in unrelated parts of the kernel, namely VM and native compilation. --- checker/checkFlags.ml | 1 + checker/values.ml | 2 +- kernel/constant_typing.ml | 26 ++++++++++++++++++++------ kernel/declarations.mli | 3 +++ kernel/declareops.ml | 1 + kernel/environ.ml | 2 ++ kernel/typeops.ml | 6 ++++-- 7 files changed, 32 insertions(+), 9 deletions(-) diff --git a/checker/checkFlags.ml b/checker/checkFlags.ml index b851234fa661..fd804ac461d6 100644 --- a/checker/checkFlags.ml +++ b/checker/checkFlags.ml @@ -23,6 +23,7 @@ let set_local_flags flags env = share_reduction = flags.share_reduction; unfold_dep_heuristic = flags.unfold_dep_heuristic; allow_uip = flags.allow_uip; + expand_let = flags.expand_let; (* These flags may not *) enable_VM = envflags.enable_VM; enable_native_compiler = envflags.enable_native_compiler; diff --git a/checker/values.ml b/checker/values.ml index 4e1d5111f6f4..d450eb821707 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -357,7 +357,7 @@ let v_typing_flags = v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; - v_bool; v_bool; v_bool; v_bool; v_bool; v_bool|] + v_bool; v_bool; v_bool; v_bool; v_bool; v_bool; v_bool|] let v_univs = v_sum "universes" 1 [|[|v_abs_context|]|] diff --git a/kernel/constant_typing.ml b/kernel/constant_typing.ml index 9771c26454e7..d525ceaea8bd 100644 --- a/kernel/constant_typing.ml +++ b/kernel/constant_typing.ml @@ -24,6 +24,12 @@ open UVars module NamedDecl = Context.Named.Declaration +(** Use this function when typing terms where the precise value of the inferred + type from the equivalence class of conversion does not matter. It makes it + more efficient. *) +let unset_let_expansion env = + Environ.set_typing_flags { (Environ.typing_flags env) with expand_let = false } env + (* Checks the section variables for the body. Returns the closure of the union with the variables in the type. *) @@ -174,7 +180,8 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } = let infer_symbol env { symb_entry_universes; symb_entry_unfold_fix; symb_entry_type } = let env, usubst, _, univs = process_universes env symb_entry_universes in let symb_entry_type = Vars.subst_univs_level_constr usubst symb_entry_type in - let j = Typeops.infer env symb_entry_type in + (* Inferred type is not returned *) + let j = Typeops.infer (unset_let_expansion env) symb_entry_type in let r = Typeops.assumption_of_judgment env j in { const_hyps = []; @@ -196,7 +203,8 @@ let make_univ_hyps = function let infer_parameter ~sec_univs env entry = let env, usubst, _, univs = process_universes env entry.parameter_entry_universes in let typ = Vars.subst_univs_level_constr usubst entry.parameter_entry_type in - let j = Typeops.infer env typ in + (* Inferred type is not returned *) + let j = Typeops.infer (unset_let_expansion env) typ in let r = Typeops.assumption_of_judgment env j in let typ = j.uj_val in let undef = Undef entry.parameter_entry_inline_code in @@ -217,7 +225,9 @@ let infer_definition ~sec_univs env entry = let env, usubst, _, univs = process_universes env entry.definition_entry_universes in let body = Vars.subst_univs_level_constr usubst entry.definition_entry_body in let hbody = HConstr.of_constr env body in - let j = Typeops.infer_hconstr env hbody in + (* When the expected type is provided, don't care about the inferred type *) + let jenv = if Option.is_empty entry.definition_entry_type then env else unset_let_expansion env in + let j = Typeops.infer_hconstr jenv hbody in let typ = match entry.definition_entry_type with | None -> j.uj_type @@ -284,7 +294,8 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out (* Note: non-trivial trusted side-effects only in monomorphic case *) let () = let eff_body, eff_env = skip_trusted_seff valid_signatures hbody env in - let j = Typeops.infer_hconstr eff_env eff_body in + (* Inferred type is not returned *) + let j = Typeops.infer_hconstr (unset_let_expansion eff_env) eff_body in let () = assert (HConstr.self eff_body == j.uj_val) in let j = { uj_val = HConstr.self hbody; uj_type = j.uj_type } in Typeops.check_cast eff_env j DEFAULTcast tyj @@ -302,12 +313,15 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out (*s Global and local constant declaration. *) let infer_local_assum env t = - let j = Typeops.infer env t in + (* Inferred type is not returned *) + let j = Typeops.infer (unset_let_expansion env) t in let t = Typeops.assumption_of_judgment env j in j.uj_val, t let infer_local_def env _id { secdef_body; secdef_type; } = - let j = Typeops.infer env secdef_body in + (* When the expected type is provided, don't care about the inferred type *) + let jenv = if Option.is_empty secdef_type then env else unset_let_expansion env in + let j = Typeops.infer jenv secdef_body in let typ = match secdef_type with | None -> j.uj_type | Some typ -> diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 080634139c36..8ffc9bac90ee 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -89,6 +89,9 @@ type typing_flags = { unfold_dep_heuristic : bool; (** If [true], use dependency heuristic when unfolding constants during conversion *) + expand_let : bool; + (** Whether to infer [let x := t in u : T{x := t}] or [let x := t in u : let x := t in T] *) + enable_VM : bool; (** If [false], all VM conversions fall back to interpreted ones *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 373dd0408724..75746cad9219 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -27,6 +27,7 @@ let safe_flags oracle = { conv_oracle = oracle; share_reduction = true; unfold_dep_heuristic = false; + expand_let = true; enable_VM = true; enable_native_compiler = true; indices_matter = true; diff --git a/kernel/environ.ml b/kernel/environ.ml index 65cd4df5fed2..d579e90afbc1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -577,6 +577,7 @@ let same_flags { indices_matter; share_reduction; unfold_dep_heuristic; + expand_let; enable_VM; enable_native_compiler; impredicative_set; @@ -591,6 +592,7 @@ let same_flags { indices_matter == alt.indices_matter && share_reduction == alt.share_reduction && unfold_dep_heuristic == alt.unfold_dep_heuristic && + expand_let == alt.expand_let && enable_VM == alt.enable_VM && enable_native_compiler == alt.enable_native_compiler && impredicative_set == alt.impredicative_set && diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 2f837f7afbb9..b5f6ed2745ac 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -733,7 +733,7 @@ and execute_aux tbl env cstr = let () = check_cast env c1 c1t DEFAULTcast c2 in let env1 = push_rel (LocalDef (name,c1,c2)) env in let c3t = execute tbl env1 c3 in - subst1 c1 c3t + if (Environ.typing_flags env).expand_let then subst1 c1 c3t else mkLetIn (name, c1, c2, c3t) | Cast (c,k,t) -> let ct = execute tbl env c in @@ -919,7 +919,9 @@ let infer_type env constr = let () = check_wellformed_universes env constr in let hconstr = HConstr.of_constr env constr in let constr = HConstr.self hconstr in - let t = execute env hconstr in + (* Returned j_type is not observable *) + let tenv = Environ.set_typing_flags { (Environ.typing_flags env) with expand_let = false } env in + let t = execute tenv hconstr in let s = check_type env constr t in {utj_val = constr; utj_type = s} From 18f11908779b0a6f37a795a699ed58e27fcd49eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Thu, 5 Mar 2026 11:33:51 +0100 Subject: [PATCH 2/2] Add a dummy overlay for minimization. --- .../21678-ppedrot-preserve-let-in-kernel-the-return.sh | 1 + 1 file changed, 1 insertion(+) create mode 100644 dev/ci/user-overlays/21678-ppedrot-preserve-let-in-kernel-the-return.sh diff --git a/dev/ci/user-overlays/21678-ppedrot-preserve-let-in-kernel-the-return.sh b/dev/ci/user-overlays/21678-ppedrot-preserve-let-in-kernel-the-return.sh new file mode 100644 index 000000000000..c48fbce82479 --- /dev/null +++ b/dev/ci/user-overlays/21678-ppedrot-preserve-let-in-kernel-the-return.sh @@ -0,0 +1 @@ +overlay fiat_crypto https://github.com/ppedrot/fiat-crypto preserve-let-in-kernel-the-return 21678