From 0ebf08a9d1db47616fe933b26376bc9ec0dae3b7 Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Mon, 7 Sep 2026 12:55:52 +0200 Subject: [PATCH 1/2] [section] skip the global dependency walk outside sections `check_op` and `check_tyd` walk the whole body of every global operator and type declaration to check that it only depends on things a global item may depend on. Outside a section that walk can never fail: `local` and `declare` items are rejected outside sections, so everything bound in the environment is `Global` there. `check_ax`, `check_modtype` and `check_module` already guard their `Global` branch with `scenv.sc_insec`; do the same for the two that were left out. The walk is proportional to the size of the term, so it costs little on hand-written developments and a lot on generated ones. On a file shaped like a Jasmin extraction of constant tables -- 20 `op` bodies of 5000 word literals each, ~1.9MB of source -- `require`ing the theory goes from 10.85s to 9.09s. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_016fkSDht523sZweUb7G7yR6 --- src/ecSection.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ecSection.ml b/src/ecSection.ml index 600a4507a..4de412bcb 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -1249,7 +1249,7 @@ let check_tyd scenv prefix name tyd = check_section scenv from; check_polymorph scenv from tyd.tyd_params; check_abstract scenv from (is_abstract_ty tyd.tyd_type) - | `Global -> + | `Global when scenv.sc_insec -> let cd = { d_ty = [`Declare; `Global]; d_op = [`Global]; @@ -1260,6 +1260,7 @@ let check_tyd scenv prefix name tyd = d_tc = [`Global]; } in on_tydecl (mkaenv scenv.sc_env (cb scenv from cd)) tyd + | `Global -> () let is_abstract_op op = match op.op_kind with @@ -1288,6 +1289,7 @@ let check_op scenv prefix name op = on_opdecl (mkaenv scenv.sc_env (cb scenv from cd)) op | `Global -> + if scenv.sc_insec then let cd = { d_ty = [`Declare; `Global]; d_op = [`Declare; `Global]; From 006ddb554b1f20f4635fe3f3dfbb3a16914de8bc Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Mon, 7 Sep 2026 12:55:53 +0200 Subject: [PATCH 2/2] [unify] build the expected type once per overloading query `select_op_outcomes` rebuilt `tfun_expected` inside the per-candidate loop, so each candidate allocated its own throw-away unification variable for the return type (plus the arrow type around it) even though the expected type is the same for all of them. Build it once, in a scratch unienv that every candidate is then forked from: the candidates stay independent, since `UniEnv.copy` still gives each one its own union-find. Also short-circuit `UniEnv.openty_r` when there is no type parameter to open and no explicit type argument: the substitution is the identity and there is no instance to report. A non-`None` `tvi` keeps the general path, which reports an arity mismatch rather than silently ignoring it. Overloaded symbols are resolved once per occurrence, which adds up on generated code. On 20 constant tables of 5000 negative word literals -- Jasmin extracts bytes signed, as `W8.of_int (-120)` -- `select_op` examines 1161954 candidates, and unary minus accounts for 900584 of them: it has nine definitions in scope once the word theories are imported, and eight are discarded at every literal. `require`ing the theory goes from 9.09s to 8.74s. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_016fkSDht523sZweUb7G7yR6 --- src/ecUnify.ml | 27 ++++++++++++++++++++++----- 1 file changed, 22 insertions(+), 5 deletions(-) diff --git a/src/ecUnify.ml b/src/ecUnify.ml index 55a9a0f67..c89a697a0 100644 --- a/src/ecUnify.ml +++ b/src/ecUnify.ml @@ -284,8 +284,17 @@ module UniEnv = struct List.map (fun tv -> subst (tvar tv)) params let openty_r (ue : unienv) (params : ty_params) (tvi : tvar_inst option) = - let subst = f_subst_init ~tv:(opentvi ue params tvi) () in - (subst, subst_tv (ty_subst subst) params) + match params, tvi with + | [], None -> + (* No type parameter to open: the substitution is the identity + and there is no instance to report. Worth special-casing, + [openty_r] is called once per overloading candidate. A + non-[None] [tvi] is left to the general path, which reports + an arity mismatch instead of silently ignoring it. *) + (Fsubst.f_subst_id, []) + | _ -> + let subst = f_subst_init ~tv:(opentvi ue params tvi) () in + (subst, subst_tv (ty_subst subst) params) let opentys (ue : unienv) (params : ty_params) (tvi : tvar_inst option) (tys : ty list) = let (subst, tvs) = openty_r ue params tvi in @@ -470,14 +479,22 @@ let select_op_outcomes (path, instance, op.D.op_ty, f) in + (* The expected type does not depend on the candidate, so build it + once in a scratch environment that every candidate is then forked + from. Building it per candidate allocated one throw-away + unification variable (and one arrow type) per candidate, which is + pure waste on the overloaded symbols: on a Jasmin extraction the + unary minus of an integer literal has nine candidates, eight of + which are discarded. *) + let ue0 = UniEnv.copy ue in + let texpected = tfun_expected ue0 ?retty psig in + let select (path, op) = - let subue = UniEnv.copy ue in + let subue = UniEnv.copy ue0 in let (tip, tvs) = UniEnv.openty_r subue op.D.op_tparams tvi in let top = ty_subst tip op.D.op_ty in - let texpected = tfun_expected subue ?retty psig in - match unify env subue top texpected with | () -> mk_ok (path, op) tip tvs top subue | exception UnificationFailure _ -> KO (lazy (classify (path, op)))