Fixing yet a source of dependency on alphabetic order in unification.

[herbelin]

Kind: bug fix

Fixes #7256, refining c24bcae (PR #924) and 6304c84:

• c24bcae fixed the order in the heuristic governed by the choose flag
• 6304c84 improved the order by preferring projections

There remained a dependency in the alphabetic order in selecting unification candidates. This PR fixes it by radically changing the representation of the substitution to invert, using a map indexed on the rank in the signature rather than on the name of the variable. Note that more could be done to use numbers further, e.g. for representing aliases (but not a priority at the moment).

Added note: The fix seems to break things elsewhere. To be investigated. This PR now depends on PR #7274 for the compilation of the test-suite. (Updated 28 July 2018)

[herbelin]

@mattam82: is it asking you a lot to review this PR considering your schedule?

[ppedrot]

#7274 has been merged, can you rebase @herbelin?

[mattam82]

Looks good to me. Removing the choose function and rather returning the ordered list of possible projections makes the algorithm much clearer I think. I suppose the Notations.out change is unrelated right?

[herbelin]

I suppose the Notations.out change is unrelated right?

It is not unrelated. This was a case where the inference of the return predicate was dependent on the names of variables. The change in Notations.out reflects what is the canonical way to infer the predicate, independently of how the variables are named.

I added a note in CHANGES to clarify the potential incompatibilities.

I also removed the UniMath overlay, since this has been merged upstream.

PS: Thanks for the review.

[ppedrot]

@herbelin Are the CI failures related? Otherwise, can you rebase on a fresh master to check that everything is OK?

[herbelin]

Are the CI failures related?

Probably. No visibility though on when I can work on it.

[herbelin]

Note in passing: make ci-vst on MacOS X fails. The makefile sets $ARCH to Darwin and the .depend targer looks for compert/Darwin which does not exist. Maybe setting ARCH manually in dev/ci-vst.sh would work (if ever an accepted way to proceed).

[herbelin]

Note for myself: VST failing on a change of unification in the following (simplified) example:

Goal forall n, n = 0 -> exists p, p = n /\ p = 0.
intros. eexists ?[p]. split. rewrite H.
reflexivity.

Added: now fixed.

[herbelin]

@ CI experts: cross-crypto has an instance of unification which depends on the ASCII order, and which this PR fixes. The incompatibility is in the submodule FCF. Is there a way to make an overlay for a submodule or do I need instead to let upstream FCF first merge the (backwards-compatible) fix I made?

[SkySkimmer]

You can make an overlay updating the submodule but it's probably easier to just let them merge. Gaëtan Gilbert

…

On 14/09/2018 10:44, Hugo Herbelin wrote: @ CI experts: cross-crypto has an instance of unification which depends on the ASCII order, and which this PR fixes. The incompatibility is in the submodule FCF. Is there a way to make an overlay for a submodule or do I need instead to let upstream FCF first merge the (backwards-compatible) fix <https://github.com/herbelin/fcf/tree/master%2Bfix-coq7257-ascii-sensitive-unification> I made? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#7257 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACWQ7B4fJgKn9C3Lrn6WvXUmAbN2PB6oks5ua2yIgaJpZM4TVfC9>.

[herbelin]

@SkySkimmer: I went towards submitting a PR to FCF. If it takes too long, I'll do an overlay of cross-crypto linking to my own version of the submodule. Thanks!

[herbelin]

Finally, I made an overlay to cross-crypto to tell it which HEAD of FCF to get. Should I submit a PR to cross-crypto just for that or can I expect that cross-crypto updates the head of its submodule automatically?

Added: never mind, I saw that the last commit to cross-crypto was a submodule update, so I submitted a PR.

[herbelin]

Overlays merged upstream. Seems ready.