Simplify interp/constrintern.ml:sort_fields
#86
Conversation
Note that turning let boolean = not regular in if boolean && complete then ...; if boolean && complete then ...; into if not regular && complete then ...; if not regular && complete then ...; has absolutely no performance cost: negation inside a conditional is not computed as a boolean, it only flips the branches. The code is more readable because "boolean" was a terrible variable name.
The code was a big "try..with" defining all useful quantities at once. I tried to lift definitions out of this try..with to define them as early as possible: the record's information and the first field name are fetched before processing the other fields. There were two calls in the try..with body that could raise the Not_found exception (or at least I don't know the code well enough to be sure that either of them cannot): `shortest_qualid_of_global` and `build_patt`. They are now split in two separate try..with blocks, both raising the same exception (with a shared error message named `env_error_msg`). Someone familiar with the invariants at play could probably remove one of the two blocks, streamlining the code even further. I'm a bit surprised by the main logic part (the big (if .. else if .. else if ..) block in the new code), and there is a question in a comment. I hope to get it answered during code review and remove it (and maybe simplify the code). Finally, there was an apparently-stale comment in the code: (* insertion of Constextern.reference_global *) of course Constextern.reference_global corresponds to now function that I could find. After trying to understand the meaning of this comment, I decided to just remove it.
we already have
val remove_first : ('a -> bool) -> 'a list -> 'a list
(** Remove the first element satisfying a predicate, or raise [Not_found] *)
now we also have the more general
val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a
(** Remove and return the first element satisfying a predicate,
or raise [Not_found] *)
The implementation is tail-recursive. The code I'm hoping to factorize
reimplements extract_first in a tail-recursive way, so it seemed good
to preserve this. On the other hand remove_first is not tail-recursive
itself, and that gives better constant factors in real-life
cases. It's unclear what is the best choice.
The internal `add_pat` function is replaced by a call to `CList.extract_first`.
The type of the user-defined function "completer" changes to be
simpler and better reflect its purpose: provide values for missing
field assignments. In the future we may want to also pass the name of
the field as parameter (currently only the index is given, and both
uses of the function ignore it), in particular if we want to implement
{ r with x = ...; y = ... }.
(Because the function is private to the module, it is documented in the .ml rather than the .mli)
|
Hugo orally clarified my question-in-comments this morning: non- Some thing I still don't understand is whether the |
|
test build |
|
@gasche The holes could be for typeclass instances, or turned into obligations by Program or subgoals by refine for example. |
|
Merged, at last. Thanks a lot for this patch and sorry for the delay to merge it. We have become more reactive on pull requests since then :) |
|
@maximedenes no harm done on my side, this is not a feature-implementing patch anyway, and for me the value was more in the making (getting to understand this corner of Coq better) than in the integration itself. But hopefully it will pave the way for more record-related ideas, possibly going back to that Thanks! |
[dune] Full Dune support.
Rename the files holding the news
Background: at the end of the Coq Coding Sprint, I decided that a feature that would be within reach (unlike
fun <pattern> =>...) would be the ability to define records by reusing fields of an existing records, that is{| r with f1 = ...; f2 = ... |}.The function to use for this purpose is
sort_fieldsininterp/constrintern.ml. Unfortunately it is undocumented and its code was unclear enough that I could not understand what it does. (There was a boolean argument namedmodeand a local variable namedboolean, for example.)The current pull-request brings zero new feature, but is a series of simplification and changes to the code of
sort_fieldsthat allowed me to understand its semantics, culminating in a documentation comment. I suspect the code changes along the way could also help future readers, which is why I didn't just include the comment in the pull request.Note 1: it's quite hard to review all changes at once, because there are a many simultaneous changes going on. I would recommend looking at the commits one by one, I tried to make them as atomic as reasonably possible.
Note 2: there is a question in a commend prefixed by
(* G.S.:, if someone can answer it I think inline comments would be a good place to discuss it, otherwise I'll just remove the comment.Note 3: now that I do understand what the function does, I suspect there should be a more direct way to implement it (than the inherently quadratic processing being performed here), but I resisted the temptation to do it. My point was just to make the existing implementation clearer.
Note 4: I did a couple mistakes during my changes, and observed that Coq immediately fails to build
theories/Logic/ExtensionalityFacts.vo. I therefore suspect that Coq breaks in obvious way when this function is bugged, which gives me confidence that the new implementation is as bug-free as the previous one.Note 5: I was a bit frightened when I discovered that
make test-suitefails miserably in my feature branch, but then found out that it already fails ontrunkwith the same failures (included below), so I guess that is ok.