Hugo Herbelin (Aug 20 2021 at 15:34): Hugo Herbelin (Aug 20 2021 at 15:34):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.
Matthieu Sozeau (Sep 03 2021 at 10:37):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: Nov 29 2023 at 18:01 UTC