Skip to content

Speed up requiring large machine-generated theories #1118

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
bgregoir wants to merge 2 commits into
base: main
Choose a base branch
from
+25 −6
Open

Speed up requiring large machine-generated theories #1118

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0ebf08a
[section] skip the global dependency walk outside sections
bgregoir Sep 7, 2026
006ddb5
[unify] build the expected type once per overloading query
bgregoir Sep 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion src/ecSection.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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];
Expand All @@ -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
Expand Down Expand Up @@ -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];
Expand Down
27 changes: 22 additions & 5 deletions src/ecUnify.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)))
Expand Down
Loading