@Pierre-Marie Pédrot , @Emilio Jesús Gallego Arias : any objections if I move indrec.ml
, inductiveops.ml
, logic.ml
and similar files to EConstr
? At first view, it is only threading the sigma
(how costly could it be?) and possibly avoiding a few costly to_constr
. In particular, should I be afraid of a slowdown risk?
Beware with Logic, the other should be fine.
I remember that I had trouble with efficiency when trying to port Logic because there are a few critical calls to unsafe back and forth conversions in there
(Or maybe it was breaking? I don't remember, this was already quite a long time ago.)
But I distinctly remember porting Logic to EConstr already and not pushing it further
(Also I'd advise against wasting time on Logic. It's legacy code that is bound to disappear.)
My initial motivation was to use the API of inductiveops.ml
on EConstr
. I don't really care about logic.ml
, it arrives as a dependency of a change in inductiveops.mli
. So, maybe, I'll keep logic.ml
as it is then.
And is it essential that vnorm.ml
is in constr
?
Actually, I don't know how is perceived the Inductiveops
API. It avoids some inductive data routine massaging, but controlling the exact amount of job which is done is difficult.
Currently, Termops.lift_rel_context
and friends are on constr
. If I need a variant of them on EConstr
, do I add them to EConstr.Vars
, to EConstr
? Do I made a Constr
or EConstr
submodule to Termops
? Any idea? (By default, I may lean to add it eConstr.ml
.)
Or we split Termops
into Constrops
and EConstrops
?
Last updated: Oct 13 2024 at 01:02 UTC