The API for terms, contexts, lifting, substitution, replacing is sometimes appealing (e.g. I find context.mli
, vars.mli
, term.mli
, constr.mli
rather nice to some extent) but also sometimes deceiving (e.g. a function exists on econstr
but not on constr
, or vice-versa, or the terminology is inconsistent, or the function is not in the expected module, ...).
Is there some consensus or maybe some ongoing project on stabilizing an API which we are satisfied with?
A prior question is maybe about how we resolve the conflict between not having more than what the kernel needs in the kernel API and the convenience of having a unique name space for everything about terms or contexts (e.g. open Constr
on constr
and open EConstr
on econstr
), for everything about lift and substitutions (e.g. module CVars = Vars
on constr
and open EConstr
providing Vars
on econstr
).
Personally, I don't care about having functions with a clear semantics and documentation in the kernel even if not directly used by the kernel, but a system of reexport in the style of CList
which includes List
, or Nameops
which includes Name
is also ok.
To start with, splitting termops.mli
into what pertains to econstr
and what pertains to constr
would be nice. It could proceed by splitting the file, or by having two submodules, or by moving the econstr
part to EConstr
or EConstr.Vars
and having Termops
includes Term
...any opinion?
Another current limitation is inductiveops.mli
which does not directly support econstr
.
I would support having an etermops
or the like, at least I think that would be good for plugin writers. If that can be moved to EConstr then even better in my opinion. We should also have a wrapper einductiveops
for sure, I think most of the administrative back and forth between e- and non-e things in equations is because we lack this.
Last updated: Jun 08 2023 at 04:01 UTC